The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

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!