coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] specializing without repeating large expressions

From: Damien Pous <Damien.Pous AT ens-lyon.fr>
To: Adam Koprowski <adam.koprowski AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] specializing without repeating large expressions
Date: Mon, 15 Mar 2010 15:04:23 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=sgAfN1PQa9oaZKp+KIFyi/uLnQXx1OuShsly8Tbyf8QVePakDaVk9/057FBk64JRrc My3HpXo+Wd35zzXVRmUSqrm15fifRhmFdyzTgsk412mp+7ZeUga/0R5dcYYg7b4GXFUL Qv/6Wm62YmLBXQp7i+bjByQ51loRXCs+xtlxo=

A possibility is to use apply or eapply with the following term:

Definition apply A (x: A) B (f: A -> B) := f x.

Lemma Lem : forall (x : nat), (x = 3).
Proof.
intros.
assert (forall (y : nat), (x = y) ->
forall (z : nat), (x = z) -> (x = 3)).
admit.
eapply apply in H.
eapply apply in H.
assumption.
...
...

Hope this helps,
Damien

[Coq-Club] specializing without repeating large expressions, Ian Lynagh
- Re: [Coq-Club] specializing without repeating large expressions, Adam Chlipala
  - Re: [Coq-Club] specializing without repeating large expressions, Adam Koprowski
    - Re: [Coq-Club] specializing without repeating large expressions, Damien Pous
- Re: [Coq-Club] specializing without repeating large expressions, Guillaume Melquiond
  - Re: [Coq-Club] specializing without repeating large expressions, Ian Lynagh