0

The authors of the book have provided proofs for some unit tests for nostutter exercise. Unfortunately, they didn't provide explanations how they work. I was able to understand all the proofs but one:

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.

After intro we have the following:

1 subgoal (ID 454)

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

When I remove repeat and run match once, I get this:

1 subgoal (ID 519)

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

So it tries to recursively find, where the list in H2 doesn't match any of nostutter constructors.

Can somebody explain me, how does this match work step by step? What is goal variable and |- symbol?

4

1 回答 1

2

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

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

并且“匹配目标”是目标上的模式匹配。最上面的一切（======）都是假设，下面是我们需要证明的东西。Ltac 没有使用线 (======) 将假设与目标分开，而是使用旋转门（假设 |- 目标 [2]）。我希望我足够清楚，但如果有不清楚的地方请告诉我。

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

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

于 2019-06-26T13:23:38.817 回答