The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

I suggest the following. Prove:


Lemma pia1 : forall A B, A/\B -> A.
intros A B [a _]; trivial.
Defined.


Lemma pia2 : forall A B, A/\B -> B.
intros A B [_ b]; trivial.
Defined.

Lemma surj_conj : forall A B, forall c : A/\B,
                c = (conj (pia1 _ _ c)(pia2 _ _ c)).
intros A B [a b]; trivial.
Qed.


Then each time you are stuck, you simply have to do
 rewrite (surj_conj c)
where c is the proof of the conjunction.

Cheers,

Benjamin



Le 6 mars 07 à 14:10, Edsko de Vries a écrit :

> Hi,
>
> I'm probably doing something that isn't allowed, but here goes:
> somewhere in a proof, I get the following subgoal (this is a reduced,
> self-contained example):
>
> 1 subgoal
> list : Set
> P : list -> Prop
> Q : list -> Prop
> x0 : list
> p0 : P x0 /\ Q x0
> H : P x0
> H1 : Qc (exist (fun l : list => P l) x0 H)
> ______________________________________(1/1)
> Qc
>   (and_rec (fun (H0 : P x0) (_ : Q x0) => exist (fun l : list => P  
> l) x0 H0)
>      p0)
>
> I should think that this should be trivial to prove, since I should  
> think that
> the and_rec can be reduced to its result (in which case the proof  
> can be
> completed by assumption H1); but calling simpl doesn't do anything.
>
> The problem is (I think) is that and_rec can only be reduced if the
> argument has the form (conj _ _). Now, p0 does not have that form, but
> the type of p0 is (P x0 /\ Q x0). Given the definition of /\:
>
> Inductive and (A : Prop) (B : Prop) : Prop :=  conj : A -> B -> A /\ B
>
> I would think if if I have a proof of type A /\ B, I must be able to
> show that the structure of that proof must be conj _ _; and hence, I
> should be able to simplify my and_rec, above. But I don't seem to be
> able to prove the following lemma:
>
> Lemma and_conj : forall (A B:Prop) (pf : A /\ B),
>   exists pa : A, exists pb : B, pf = conj pa pb.
>
> Is there a good reason why I can't prove that, other than the fact  
> that
> I'm still very much a beginner with Coq?
>
> Thanks!
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club