IndProp test_nostutter_4 - PullRequest
Новая
       29

IndProp test_nostutter_4

0 голосов
/ 26 июня 2019

Авторы книги предоставили доказательства некоторых модульных тестов для упражнений на ностальтеру. К сожалению, они не дали объяснения, как они работают. Я смог понять все доказательства, кроме одного: 

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 переменная и |- символ?

1 Ответ

2 голосов
/ 26 июня 2019

Позвольте мне сначала доказать это трудным способом.

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_(symbol)

...