The Coq mailing list

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

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.