Ltac: optional variable name

Question

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.

Tej Chajed · Accepted Answer · 2018-03-30T14:47:43.690

8

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.

edited Mar 30 '18 at 14:47

answered Mar 29 '18 at 14:52

Tej Chajed

3,749
14
18

Thanks for your answer. In your last paragraph, do you mean if I would use a tactic that creates variables like intro before using h? – Tom Mar 29 '18 at 18:23
Yes, exactly. You might introduce variables with `intro` or `intros`, or you might use `assert` or `pose proof`. – Tej Chajed Mar 30 '18 at 14:47
And what did involve my argument to be a constr? Because of match with? – Tom Mar 30 '18 at 18:17
1

I think it's actually `type of h`, which doesn't make sense when `h` is an identifier and so you get a dynamic type error. – Tej Chajed Mar 30 '18 at 20:33

Ltac: optional variable name

1 Answers1