2

我想写一个带有可选变量名的策略。原来的战术是这样的：

Require Import Classical.

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

我想让用户有机会选择他想要的名称并使用它：save a例如。

我使用此解决方案编写了一个变体：

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是新鲜的，但我不确定如何做到这一点。

4

1 回答 1

8

问题是该解决方案涉及一个作为术语（a 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.

这个解决方案的一个问题是它fresh在运行之前调用savetactic，如果你想让它h在里面做一些其他工作之后是新鲜的，这是行不通的savetactic。不过，我认为唯一的区别在于自动生成的名称。

于 2018-03-29T14:52:30.137 回答