coq - 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)，而您有一个名称(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.

这个解决方案的一个问题是它在运行 savetactic 之前调用了 fresh，如果你想要那个 h 它就不会工作> 在 savetactic 中完成一些其他工作后保持新鲜。不过，我认为这唯一的区别在于自动生成的名称。