The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Quoting Edsko de Vries 
<devriese AT cs.tcd.ie>:

Hi,
  You can also derive another elimination principle, then use it with elim:

 Lemma and_rect2 : forall (A B:Prop)(P:A/\B->Type),
    (forall a b, P (conj a b)) -> forall c:A/\B, P c.

 Proof.
 intros A B P H c;case c.
 auto.
 Qed.


 Lemma and_conj : forall (A B:Prop) (pf : A /\ B),
  exists pa : A, exists pb : B, pf = conj pa pb.
Proof.
  intros.
  elim pf using and_rect2.
  intros a b; exists a; exists b; auto.
Qed.


It seems that the tactic "elim" (whithout "using") applies a default
elimination principle, which is not always the useful one, whereas
"case" is more basic.

Pierre




> On Tue, Mar 06, 2007 at 02:51:52PM +0100, 
> jean-francois.monin AT imag.fr
>  wrote:
> > Hi,
> >
> > I did'nt read the complicated part, but at least:
> > > 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.
> >
> > intros. case pf. intros a b.
> > exists a. exists b.
> > reflexivity.
> > Qed.
>
> Aaargh. Okay. That was easy :) Thanks! I had tried both (elim pf) and
> (inversion pf), but neither worked; I hadn't tried (case pf). I don't
> really understand why (case pf) works, but the other two don't. I guess
> it's back to Coq'Art for me :)
>
> 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



Pierre Castéran