coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Destructing and constructing inductive types

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Destructing and constructing inductive types
Date: Tue, 18 Oct 2016 17:27:43 +0200

On 10/18/2016 05:20 PM, Klaus Ostermann wrote:

Goal forall a b (p : nat * nat),
a = b -> fst p = a -> p = (b, snd p).

Goal forall a b (p : nat * nat),
a = b -> fst p = a -> p = (b, snd p).
intros a b p.
destruct p as [a1 b1].
intros H1 H2.
rewrite <-H1, <-H2.
trivial.

Goal forall a b (p : nat * nat),
a = b -> fst p = a -> p = (b, snd p).
now intros a b [a1 b1] -> <-.

--
Laurent

[Coq-Club] Destructing and constructing inductive types, Klaus Ostermann, 10/18/2016
- Re: [Coq-Club] Destructing and constructing inductive types, Dominique Larchey-Wendling, 10/18/2016
  - Re: [Coq-Club] Destructing and constructing inductive types, Klaus Ostermann, 10/18/2016
    - Re: [Coq-Club] Destructing and constructing inductive types, Laurent Thery, 10/18/2016
    - Re: [Coq-Club] Destructing and constructing inductive types, Dominique Larchey-Wendling, 10/18/2016
- Re: [Coq-Club] Destructing and constructing inductive types, Emilio Jesús Gallego Arias, 10/19/2016