Как можно шаг за шагом проверить, что делает более сложная тактика в Coq? - PullRequest
Новая
       9

Как можно шаг за шагом проверить, что делает более сложная тактика в Coq?

0 голосов
/ 05 января 2019

Я пытался просмотреть знаменитую и замечательную книгу по основам программного обеспечения , но попал в пример, где simpl. и reflexivity. просто много делают под одеялом и мешают моему обучению и пониманию ,

Я проходил следующую теорему: 

Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false. (* n+1 != 0 *)
Proof.
  intros n.
  destruct n as [| n'].
    -simpl. reflexivity.
    -simpl. reflexivity.
Qed.

что я действительно хочу, так это то, что позволяет мне шаг за шагом проходить то, что делали simpl. и reflexivity.. Есть ли что-то, что позволяет мне это сделать?

Предполагается, что Destruct решит следующую проблему:

потому что первый аргумент beq_nat (который просто not equal т.е. !=) выполняет сопоставление, но первый вход зависит от неизвестной переменной n и то же самое для +, поэтому сопоставление не может ничего сделать так что simpl. застревает (по какой-то причине).

что он явно должен разрешить это, так как Coq позже принимает доказательство. Но если внимательно посмотреть, какова вторая цель, то, похоже, вновь возникает та же проблема, что и выше: 

2 subgoals
______________________________________(1/2)
beq_nat (0 + 1) 0 = false
______________________________________(2/2)
beq_nat (S n' + 1) 0 = false

теперь у нас есть n' в качестве первого аргумента для beq_nat и + снова. Однако для такого новичка, как я, simpl. чудесным образом работает на этот раз по какой-то таинственной причине. Я, очевидно, прочитал simpl. документацию , но, будучи новичком в этом, я действительно не знал, что искал, и мне было трудно понять, что было полезно ...

В любом случае, почему это работает здесь? Причина, по которой я спрашиваю, заключается в том, что мне никогда бы не пришло в голову использовать destruct в этом примере доказательства, особенно потому, что n' возникла неизвестная переменная, и кажется, что я смог увидеть, что на самом деле произошло или что было иначе было бы полезно. Поэтому я подумал, что было бы полезно проверить пошаговую разбивку подобных вещей (вместо того, чтобы публиковать новый вопрос SO через день).

Обратите внимание, я видел этот вопрос:

Пошаговое упрощение в coq?

но я не смог найти способ сделать его полезным для меня, так как он был специально адаптирован для этого конкретного примера. Надеюсь, мой вопрос не станет сужаться до моего конкретного примера, хотя, возможно, так как пошаговое разбиение может оказаться невозможным без знания того, как simpl. (или reflexivity.) уже работает (или, по крайней мере, вышеупомянутые ответы на вопрос выше произвел на меня такое впечатление).

Ответы [ 2 ]

0 голосов
/ 07 января 2019

Один из способов разбить оценку - дать аргумент simpl, как предложено в вопросе, который вы связали . simpl f позволяет упростить только те подвыражения, которые появляются при вызовах к f. В этом случае simpl Nat.add (или simpl plus или simpl "+") упрощает S n' + 1 до S (n' + 1). Тогда simpl beq_nat превращает beq_nat (S (n' + 1)) 0 в false.

Что касается reflexivity, он может заключить, что два сравниваемых термина равны упрощению, что означает, что, если я не ошибаюсь, вы всегда можете заменить simpl; reflexivity просто reflexivity.

0 голосов
/ 06 января 2019

Сокращение этого шага за шагом: 

beq_nat (S n' + 1) 0 = false

  (* Without the `+` notation, which is purely for pretty-printing: *)

beq_nat (plus (S n') 1) 0 = false

  (* by definition of plus:   plus (S n') 1 = S (plus n' 1) *)

beq_nat (S (plus n' 1)) 0 = false

  (* by definition of `beq_nat`,

     beq_nat (S (plus n' 1)) 0 =
     = match S (plus n' 1) with
       | O => ... (* unreachable *)
       | S m => match 0 with
                | O => false
                | S _ => ...
                end
       end
     = match 0 with
       | O => false
       | S _ => ...
       end
     = false
  *)

false = false
...