IndProp test_nostutter_4

Question

本书的作者已经为 nostutter 练习的一些单元测试提供了证明。不幸的是，他们没有解释它们是如何工作的。除了一个，我能够理解所有证明：

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.
  repeat match goal with
    h: nostutter _ |- _ => inversion h; clear h; subst
         end.
  contradiction.
Qed.

介绍后我们有以下内容：

1 subgoal (ID 454)

H : nostutter [3; 1; 1; 4]
============================
False

当我删除 repeat 和运行匹配一次时，我得到这个：

1 subgoal (ID 519)

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

因此它尝试递归查找，其中 H2 中的列表与任何 nostutter 构造函数都不匹配。

谁能给我解释一下，这场比赛是如何一步步进行的？什么是 goal 变量和 |- 符号？

Answer 1

让我首先用困难的方式证明这一点。

Example test_nostutter_4:      not (nostutter [3;1;1;4]).
Proof.
  intro.
  (* You can think of this inversion H as 
     destructing nostutter [3; 1; 1; 4] into 
     ns_cons 3 1 [1; 4] (Trm : nostutter [1 :: 1 :: 4]) (Prf : 3 <> 1) *)
  inversion H.
  (* Let's invert Trm again. The process is same and I am leaving it for you to figure out*)
  inversion H2.
  (* At this point, you can easily that H9 say that 1 <> 1 which is off-course a false 
     assumption*)
  unfold not in H9.
  specialize (H9 eq_refl).
  Print False. (* False is inductive data type with no constructor*)
  inversion H9.
Qed.

如你所见，我的证明有很多重复，我们可以很容易地将它们自动化。 Coq 有称为 Ltac 的策略语言来组合策略 [1]。在你的证明中，目标是

1 subgoal (ID 454)

H : nostutter [3; 1; 1; 4]
============================
False

和"match goal with"是目标模式匹配。行顶部的所有内容 (======) 都是假设，下面是我们需要证明的内容。 Ltac 没有使用线 (======) 将假设与目标分开，而是使用转门（假设 |- 目标 [2]）。我希望我足够清楚，但如果有什么不清楚的地方，请告诉我。

[1] https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.match-goal

[2] https://en.wikipedia.org/wiki/Turnstile_(symbol)

IndProp test_nostutter_4

IndProp test_nostutter_4

coq

logical-foundations