Ltac:可选变量名

Question

我想写一个带有可选变量名的策略。最初的策略如下：

Require Import Classical.

Ltac save := 
  let H := fresh in
  apply NNPP;
  intro H;
  apply H.

我想让用户有机会选择他想要的名称，并像这样使用它:例如，save a。

我用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.

然而，这个证明在save h上失败了

Lemma te (A B : Prop) : A \/ ~A.
Proof.
save h.
right.
intro a.
apply h.
left.
exact a.
Qed.

错误信息：

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.

我想我必须确保h是新鲜的，但我不确定如何做到这一点。

Answer 1

问题是，该解决方案涉及一个术语( constr)的论点，而您有一个名称(一个ident符)。但是，您可以通过提供新标识符的策略符号来更简单地解决问题。

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.

这个解决方案的一个问题是，它在运行savetactic之前调用了savetactic，如果您希望在savetactic中执行其他一些工作之后，h是新鲜的，那么它将无法工作。不过，我认为，唯一不同的是自动生成的名字。