了解专门的策略

Question

试图理解@keep_learning的答案，我逐步浏览了此代码：

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Example test_nostutter_4: not (nostutter [3;1;1;4]).
Proof.
  intro.
  inversion_clear H.
  inversion_clear H0.
  unfold not in H2.
  (* We are here *)
  specialize (H2 eq_refl).
  apply H2.
Qed.

这是我们在辩护之前所拥有的

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
============================
False

这是EQ Prop，其构造函数eq_refl用于专业：

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.

我无法解释，该命令是如何工作的：

specialize (H2 eq_refl).

我阅读了有关参考手册的专业信息，但是那里的解释太广泛了。据我所知，它看到了" 1 = 1"。H2中的表达满足eq_refl构造函数，因此EQ命题是正确的。然后它简化了表达式：

True -> False => False

我们得到

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : False
============================
False

有人可以为我提供一个最小的例子，并说明specialize在做什么，以便我可以自由使用它？

update

试图模仿使用Applip的专业工作的工作方式，我做了以下操作：

Example specialize {A B: Type} (H: A -> B) (a: A): B.
Proof.
  apply H in a.

这给出了：

A : Type
B : Type
H : A -> B
a : B
============================
B

几乎与specialize相同，只有不同的假设名称。

在test_nostutter_4定理中，我尝试了此操作：

remember (@eq_refl nat 1) as Heq.
apply H2 in Heq as H3.

它给了我们：

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
Heq : 1 = 1
H3 : False
HeqHeq : Heq = eq_refl
============================
False

这个更复杂，我们必须引入一个新的假设HEQ。但是我们得到了我们需要的东西-H3最后。

专业化是否在内部使用诸如记住之类的东西？还是可以使用应用程序解决但不记得吗？

Answer 1

specialize，最简单的形式，只需用应用于其他术语的假设代替给定的假设。

在此证明中，

Example specialize {A B: Type} (H: A -> B) (a: A): B.
Proof.
  specialize (H a).
  exact H.
Qed.

我们最初有假设H: A -> B。当我们调用specialize (H a)时，我们将H应用于a(在功能应用程序中应用(。这给了我们类型的B。然后，specialize为我们提供了旧的H，并用应用程序的结果代替了它。它给出了新的假设相同的名称：H。

在您的情况下，我们有H2: 1 = 1 -> False，它是从类型1 = 1到类型False的功能。这意味着应用于eq_refl的H2是False类型，即H2 eq_refl: False。当我们使用Tactic specialize (H2 eq_refl).时，旧的H2将被清除并用新术语(H2 eq_refl(替换，该术语是False。它保留了旧名称 H2。

specialize当您确定仅使用一次假设时，因为它会自动摆脱旧假设，因此很有用。一个缺点是旧名称可能不符合新假设的含义。但是，就您的情况而言，在我的示例中，H是一个通用的名称，它可以用任何方式工作。

---

到您的更新...

specialize是直接在LTAC插件中定义的核心策略。它在内部不使用任何其他策略，因为它是其内部。

如果要保留假设，则可以使用as修饰符，该修饰符适用于specialize和apply。在证明

中

Example specialize {A B: Type} (H: A -> B) (a: A): B.
Proof.

如果您执行specialize (H a) as H0.，而不是清除H，则将引入一个新的假设H0: B。apply H in a as H0.具有相同的效果。