coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fr�d�ric Besson <fbesson AT irisa.fr>
- To: Brandon Moore <brandon_m_moore AT yahoo.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] existential variables in tactics
- Date: Thu, 6 Dec 2007 15:12:40 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On 5 déc. 07, at 20:56, Brandon Moore wrote:
If I understand correctly, you would like to transform a goal like H1 : ~ Q a H2 : forall x, Px -> Q x <bla1> ------------------- <bla2> into <bla1> Hnew : ~ P a ----------------- <bla2> To do that, I would proceed as follows: 1) Prove a lemma that does most of the job 2) Use a tactic to match the hypotheses and apply the lemma Lemma do_it : forall (A : Set) (Q : A -> Prop) (P: A -> Prop) (a:A), (forall x, P x -> Q x) -> ~ Q a -> ~ P a. Proof. intros. red ; intro. apply H0. apply H ; auto. Qed. Ltac do_it_tac := match goal with | Hneg : ~ ?Q ?A , Hlem : forall x, ?P x -> ?Q x |- _ => generalize (do_it _ Q P A Hlem Hneg) ; clear Hneg Hlem ; intro end. Regards, -- Frédéric Besson |
- [Coq-Club] existential variables in tactics, Brandon Moore
- Re: [Coq-Club] existential variables in tactics, Frédéric Besson
- Re: [Coq-Club] existential variables in tactics, Aaron Bohannon
- <Possible follow-ups>
- Re: [Coq-Club] existential variables in tactics, Brandon Moore
- Re: [Coq-Club] existential variables in tactics, Aaron Bohannon
Archive powered by MhonArc 2.6.16.