I would like to write a tactic with an optional variable name. The original tactic looks like this:
Require Import Classical.
Ltac save :=
let H := fresh in
apply NNPP;
intro H;
apply H.
I would like to give the user an opportunity to choose the name he wants and use it like: save a for example.
I wrote a variation using this solution:
Require Import Classical.
Inductive ltac_No_arg : Set :=
| ltac_no_arg : ltac_No_arg.
Ltac savetactic h :=
match type of h with
| ltac_No_arg => let H := fresh in
apply NNPP;
intro H;
apply H
| _ => apply NNPP;
intro h;
apply h
end.
Tactic Notation "save" := savetactic ltac_no_arg.
Tactic Notation "save" ident(x) := savetactic x.
However this proof fails on save h:
Lemma te (A B : Prop) : A \/ ~A.
Proof.
save h.
right.
intro a.
apply h.
left.
exact a.
Qed.
The error message:
In nested Ltac calls to "save (ident)", "savetactic" and "h", last term evaluation failed.
In nested Ltac calls to "save (ident)", "savetactic" and "h", last term evaluation failed.
Variable h should be bound to a term but is bound to a ident.
I guess I must make sure that h is fresh, but I am unsure on how to do that.
The problem is that that solution involved an argument that was a term (a constr), whereas you have a name (an identifier). However, you can solve your problem more simply with a tactic notation that provides a fresh identifier.
Require Import Classical_Prop.
Ltac savetactic h :=
apply NNPP;
intro h;
apply h.
Tactic Notation "save" := let H := fresh in savetactic H.
Tactic Notation "save" ident(x) := savetactic x.
Lemma te (A B : Prop) : A \/ ~A.
Proof.
save h.
right.
intro a.
apply h.
left.
exact a.
Qed.
The one problem with this solution is that it calls fresh before running savetactic at all, which won't work if you wanted that h to be fresh after doing some other work inside savetactic. The only difference this would make is in the auto-generated names, though, I think.