1

为了理解@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。然后它简化了表达式：

True -> False => False

我们得到

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

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

更新

尝试使用 apply 来模仿 special 的工作原理，我做了以下操作：

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 但不记得来解决它？

4

1 回答 1

6

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.有同样的效果。

于 2019-06-30T23:48:47.097 回答