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

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`?

Use `Defined` instead of `Qed`.

1 Like

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`).