The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thanks -- first solution is exactly what I wnated. For some stupid reason, I used to think Program only worked with Fixpoint.

On Sun, Sep 1, 2013 at 5:23 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

Program Definition a' := Build_Foo 5 _.

Next Obligation.

  exact lem__5_lt_10.

Qed.

(* or *)

Definition a'' : Foo.

Proof.

  refine (Build_Foo 5 _).

  exact lem__5_lt_10.

Defined.

-Jason

On Sunday, September 1, 2013, t x wrote:

Hi,

  Here is my min fail case.

Require Import ZArith Omega.
Local Open Scope Z_scope.

Record Foo :=
  { n : Z;
    H : n < 10 }.


Lemma lem__5_lt_10: 5 < 10.
Proof. omega. Qed.


(* this line works *)
Definition a := Build_Foo 5 lem__5_lt_10.


(* this line does not work *)
Definition a' := Build_Foo 5 _.

(*  Question: is there a way to use Program / refine
    so that I can write the above?

In particular, I want to:
  * fill in the proof after the "Build_Foo"

I do NOT want to:
  * define a lemma before hand to use.

 *)

  Is the above possible?

Thanks!