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

Using Coq
1

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?

2

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