The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  You may use "fresh" for generating names that are not
bound in the context yet.
Here is a small example:

Pierre



Ltac bool_case b :=
 let h_true := fresh "Ht" in
 let h_false := fresh "Hf" in
   case_eq b ;[intro h_true|intro h_false].


Goal forall (P: Prop) b, b = negb(negb b).
intros Ht  b; bool_case b.
(*
2 subgoals, subgoal 1 (ID 16)

  Ht : Prop
  b : bool
  Ht0 : b = true   *** Ht has been renamed to Ht0 because Ht is already used
                   in the context ***
  ============================
   true = negb (negb true)

subgoal 2 (ID 17) is:
 false = negb (negb false)
*)
reflexivity.
reflexivity.

Qed.





Quoting Math Prover 
<mathprover AT gmail.com>:

> Hi,
>
>   1) In a previous question, I learned that I can do:
>
>     destruct <expr> eqn:<naming intro pattern>
>
>   2) To avoid the use of local variable names, I would like to wrap this in
> a ltac. However, I need to provide a name to "eqn: ... ".
>
> Thus, my question -- what is the Coq equiv of gen-sym?
>
> Thanks!