coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using apply on a hypothesis with universal quantification

From: Rui Baptista <rpgcbaptista AT gmail.com>
To: Laurent Théry <Laurent.Thery AT inria.fr>
Cc: "Soegtrop, Michael" <michael.soegtrop AT intel.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Using apply on a hypothesis with universal quantification
Date: Thu, 7 Nov 2013 13:45:11 +0000

If it becomes too difficult, you can prove it with tactics.

Example Test2: forall c d:nat, ( forall a b:nat, a = b -> a+a=b+b) -> c = d.

intros c d H.

assert (forall a b : nat, a = b -> S a + a = S b + b).

info_eauto.

On Thu, Nov 7, 2013 at 1:07 PM, Laurent Théry <Laurent.Thery AT inria.fr> wrote:

On 11/07/2013 02:03 PM, Soegtrop, Michael wrote:

Test2: forall c d:nat, ( forall a b:nat, a = b -> a+a=b+b) -> c = d.
intros c d H.

when I want to leave t

You still can but it is more difficult to build blindly ;-)

assert (G := fun a b H1 => (f_equal S (H a b H1))).

[Coq-Club] Using apply on a hypotheis with universal quantification, michael.soegtrop, 11/07/2013
- Re: [Coq-Club] Using apply on a hypotheis with universal quantification, Laurent Théry, 11/07/2013
  - RE: [Coq-Club] Using apply on a hypothesis with universal quantification, Soegtrop, Michael, 11/07/2013
    - Re: [Coq-Club] Using apply on a hypothesis with universal quantification, Laurent Théry, 11/07/2013
      - Re: [Coq-Club] Using apply on a hypothesis with universal quantification, Rui Baptista, 11/07/2013