The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Because [AC (Build_C (Some c')) t] reduces to [AC c' t], by definition.

Of course, usually, you may need the [t] returned by [FIX c'], then you can do something along the lines of

generalize (FIX c').
intros [t r].
exists (f t). (* for a good choice of [f] *)
exact r.

Or something.

On 5 February 2014 06:42, Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk> wrote:

Dear Arnaud,

Just to clarify, why does [exact (FIX c')] prove the following goal? I know it does, but why?

FIX : forall c : C, exists t : T, AC c t

c' : C

______________________________________(1/1)

exists t : T, AC (Build_C (Some c')) t

Regards,
Jeff.

On 4 Feb 2014, at 17:16, Terrell, Jeffrey wrote:

Thanks, the trick works well in L2, but unfortunately not in my main proof. In fact, the error reported, i.e.

The term "FIX c prefix" has type

 "exists t : Table, AttributeToColumn c t prefix"

 while it is expected to have type

 "exists t : Table,

    AttributeToColumn (Build_Class oid super (Some c) attributes) t prefix".

is similar to the one I would have expected [exact (FIX c')] to produce in L2, because (FIX c') is of type exists t : T, AC c' t, not exists t : T, AC (Build_C (Some c')) t. Here's the current goal just before [exact (FIX c')] is invoked.

FIX : forall c : C, exists t : T, AC c t

c' : C

______________________________________(1/1)

exists t : T, AC (Build_C (Some c')) t

Any thoughts on what could be wrong?

Regards,
Jeff.

On 4 Feb 2014, at 16:07, Arnaud Spiwack wrote:

The trick is to refrain from choosing a witness too early:

Lemma L2 : forall c : C, exists t : T, AC c t.
Proof.
   fix FIX 1.
   intros [[ c' | ]].
   + exact (FIX c').
   + exists Build_T.
     exact I.
Qed.

On 4 February 2014 16:55, Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk> wrote:

Could someone help me to solve L2? I've tried ex_intro but I can't seem to get it to work. Many thanks.

Regards,
Jeff.

Inductive C : Set :=
   Build_C : option C -> C.

Inductive T : Set :=
   Build_T : T.

Fixpoint AC (c : C) (t : T) {struct c} : Prop :=
   match c with
      Build_C None => True |
      Build_C (Some c') => AC c' t
   end.

Lemma L1 : forall c : C, forall t : T, AC c t.
Proof.
   fix FIX 1.
   intros c t.
   destruct c as [o].
   destruct o as [c' |].
   {
      simpl.
      exact (FIX c' t).
   }
   simpl.
   trivial.
Qed.

Lemma L2 : forall c : C, exists t : T, AC c t.
Proof.
   fix FIX 1.
   intro c.
   exists (Build_T).
   destruct c as [o].
   destruct o as [c' |].
   simpl.
   {
      admit.
   }
   simpl.
   trivial.
Qed.