The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Klaus,

Destructive intros patterns are VERY good at doing what you want. 

Goal forall a b (p : nat * nat),
a = b -> fst p = a -> p = (b, snd p).
Proof.
  intros ? ? [] [] []; reflexivity.
Qed.

But of course you need to understand what it means to
destruct/pattern match an equality type. This is
very interesting in any case.

subst may be easier to work with.

Goal forall a b (p : nat * nat),
a = b -> fst p = a -> p = (b, snd p).
Proof.
  intros a b [? ?] ? ?; subst a b; reflexivity.
Qed.

Best

Dominique

----- Mail original -----
> De: "Klaus Ostermann" 
> <klaus.ostermann AT uni-tuebingen.de>
> À: 
> coq-club AT inria.fr
> Envoyé: Mardi 18 Octobre 2016 17:20:35
> Objet: Re: [Coq-Club] Destructing and constructing inductive types
> 
> Hello Dominique,
> 
> my problem is presumably merely caused by my lack of expertise,
> but to illustrate my point, what is the simplest way to prove
> trivial lemmas like this one?
> 
> Goal forall a b (p : nat * nat),
> a = b -> fst p = a -> p = (b, snd p).
> 
> Klaus
> 
> 
> Am 18/10/16 um 12:40 schrieb Dominique Larchey-Wendling:
> > On 10/18/2016 12:10 PM, Klaus Ostermann wrote:
> >> Lemmas like this can be formulated for every inductive datatypes:
> >>
> >> forall p, (fst p, snd p) = p
> >>
> >> I find that I often need such lemmas for rewriting terms while proving
> >> stuff in Coq.
> >>
> >> It is annoying to prove such lemmas by hand for every datatype.
> > destruct p does not fit your needs ?
> >
> > Dominique
> 
>