The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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!