# Can I access Coq's way of generating readable names from inside tactics?

If I `destruct` a thing involving a `bool` (or `remember` a `bool`), the resulting bool will most likely be called `b`, `b0`, `b1`, …; a natural number will be `n`, …; and so on. Can I access the same name generation mechanism from `Ltac`? `fresh` defaults to `H` no matter what, I can only pass in a name or string (or several) to use in place of `H`. What if I don’t have any?

The concrete context I currently want that in is writing a `remember` variant that flips the equality. (Both `rewrite` and most library theorems expect the equality to have the opposite direction from what `remember` generates, and I don’t want to deal with using `rewrite <-` or `symmetry in` or whatever all. the. time.)

So far I have:

``````Tactic Notation "remember'" constr(t) "as" ident(x) "eqn" ":" ident(H) :=
(* NB: using "eqn:" instead of "eqn" ":" in the Notation messes up the grammar *)
remember t as x eqn:H; symmetry in H.
Tactic Notation "remember'" constr(t) "as" ident(x) :=
let H := fresh "Heq" x in remember' t as x eqn:H.
``````

Now I’d also like to have a `Tactic Notation "remember'" constr(t) := …` that makes nice names like `remember` does, but I don’t know how to access the name generation mechanism. Any pointers?

No real pointer, a few things:

### `fresh` can take several arguments

So you can build complex names with it:

``````Lemma Foo: forall x y , x < y -> y >= x.
Proof.
let nme := fresh "inf_" x "_" y in intros x y nme.
``````

gives the goal:

``````  x, y : nat
inf_x_y : x < y
============================
y >= x
``````

So you can play with that in your Ltac. Which is preciselt what I have done in LibHyps:

### You can try LibHyps

I wrote this small library of tactics, where there is a tactic `autorename h` which does more or less what you suggest.

``````Require Import LibHyps.LibHyps.
Lemma Foo: forall x y , x < y -> y >= x.
Proof.
intros.
autorename H.
(* or equivalently : *)
intros ; { autorename }.

x, y : nat
h_lt_x_y_ : x < y
============================
y >= x
``````