Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] existential variables in tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] existential variables in tactics


chronological Thread 
  • 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:

Hello

I have been trying to define a tactic to compose a negated hypothesis like ~(Q a)
and a lemma with dependent arguments like forall x, P x -> Q x into a new
hypothesis ~(P a). To get from a goal of false to a goal of P a just
requires apply H; apply lem. Constructively, I then expect to be able to
prove ~(P a), but I took a while to build the tactic, mostly
trying to get existential variables instantiated.

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





Archive powered by MhonArc 2.6.16.

Top of Page