了解专精战术

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.

这是我们在执行 specialize 之前所拥有的

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

这是 eq Prop 其构造函数eq_refl用于 specialize：

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).

我读过关于专业参考手册，但那里的解释太宽泛了。据我所知，H2 中的“1 = 1”表达式满足eq_refl构造函数，因此 eq 命题为真。然后它简化了表达式：

True -> False => False

我们得到

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

有人可以向我提供一个解释正在specialize做什么的最小示例，以便我可以自由使用它吗？

更新

尝试使用 apply 模仿 specialize 的工作方式，我执行了以下操作：

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。

专业内部是否使用诸如记忆之类的东西？或者是否可以通过apply解决它但没有记住？

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，这是从 type1 = 1到 type的函数False。这意味着H2应用于eq_refl类型为False，即H2 eq_refl: False。当我们使用这个策略时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.有同样的效果。