The Coq mailing list

[Fr�d�ric Besson <fbesson AT irisa.fr>]

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