The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

I sometimes use the below tactic notations to proof the preconditions of a hypothesis one by one:

 

Definition GetFirstArg {A B : Type} (f : A -> B) := A.

 

Tactic Notation "AssertFirstArg" hyp(H) "as" ident(id) :=

  assert(GetFirstArg H) as id; unfold GetFirstArg.

 

Tactic Notation "AssertFirstArg" hyp(H) "as" ident(id) "by" tactic(tac) :=

  assert(GetFirstArg H) as id by (unfold GetFirstArg; tac); unfold GetFirstArg in id.

 

Example Ex1 A B : A -> (A->B) -> B.

  intros H1 H2.

  AssertFirstArg H2 as H3 by assumption. specialize (H2 H3). assumption.

Qed.

 

It would make sense to combine the assert and the specialize in one tactic script, but when I try this:

 

Tactic Notation "SpecializeFirstArg" hyp(H) "by" tactic(tac) :=

  let H' := fresh "FirstArg" in

    (assert(GetFirstArg H) as H' by (unfold GetFirstArg; tac)); specialize (H H') .

 

Example Ex2 A B : A -> (A->B) -> B.

  intros H1 H2.

  SpecializeFirstArg H2 by assumption.

Qed.

 

I get the error message

 

Error: Cannot change H2, it is used in hypothesis FirstArg.

 

and I can’t find a way around this. Can someone help me with this?

 

Thanks & best regards,

 

Michael