Definitions completed with proof scripts are opaque, how to make them compute

Using Coq
1

I’d like to pass a proof that n > 0 into hd because the type signature t A (S n) -> A is causing me issues and I have a spare proof of my n > 0 lying around.

I’ve been experimenting with filling out Definitions by writing proofs instead of specifying the combinator, because another function I wrote only worked that way for reasons I’ll tell you another time. But this seems to have gone well:

  Definition hd_proof {A : Type} {n : nat} (v : t A n) (H : n > 0) : A.
  Proof.
    induction n; try lia.
    remember (hd v) as x.
    simpl in x.
    apply x.
  Qed.

My understanding is that the proof script is manipulating and ultimately creating a proof object, which is a sort of combinator. So I figured it would apply.

  Lemma fourgtone : 4 > 0. Proof. lia. Qed.
  Compute hd_proof [1;2;3;4] fourgtone.
(* response: 
= hd_proof [1; 2; 3; 4] fourgtone
     : nat
*)

Can I Make Compute actually compute and terminate at 1?

2

Use Defined instead of Qed.

1 Like
3

Alternatively, check out this blog post on computing with Opaque proofs that I wrote a while back; it works well for decidable properties like > (you’d still have to use Defined for the hd_proof, but not the 4 > 0).