The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You are looking for the [open_constr] tag for tactic notation:

Tactic Notation "rename_hyp" open_constr(Pattern) ident(H) :=

  match goal with

    | [ H' : Pattern |- _ ] => rename H' into H

  end.

Note that you do not need the [clear].

As for your other question, you probably want to look at the [fresh] tactic, which generates a fresh name not currently used as a hypothesis.  So you could replace [rename H' into H] with something like [let H := fresh in rename H' into H].

-Jason

On Tuesday, July 16, 2013, Leonardo Rodriguez wrote:

Hi

I'm relatively new in Coq. I wonder how to write proofs which
are independent of the name generation algorithm of Coq.

For example, consider this tactic and the following lemma (a simplified version of my actual code)

Ltac rename_hyp Pattern H :=
  match goal with
      | [H' : Pattern |- _]
        => rename H' into H  ; clear H'
  end.

Inductive T : Prop :=
| a : T
| b : T.

Axiom P : Prop.
Axiom Q : T -> Prop.
Axiom R : T -> Prop.

Lemma whatever : P -> Q a -> Q b -> R b -> True.
  intros.
  rename_hyp P new_name_for_P.
  rename_hyp (Q a) new_name_for_Q_a.
  (* Doesn't work : *)
  rename_hyp (R _) new_name_for_R.

I want to write (or use) a tactic which can take any pattern as an argument.

But I also want  to ask in general, how to write proof independent of the names
generated by Coq.

Thank you!