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

Question

Я пытался пройти через знаменитую и замечательную книгу об основах программного обеспечения, но попал в пример, где 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. документация, но, будучи новичком в этом, я действительно не знал, что искал, и мне было трудно понять, что было полезно...

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

---

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

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

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

Answer 1

Один из способов сломать оценку - дать аргумент 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,

Answer 2

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

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