Почему evn (S (S n)) уменьшает число, а не увеличивает его?

Question

Я проходил курс по основам программного обеспечения и увидел следующий простой код:

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

однако при использовании тактики apply ev_SS. для доказательства того, что ev 4верно:

Theorem ev_4 : ev 4.
Proof.  (* goal: ev 4*)
  apply ev_SS. (* goal changed to: ev 2, why??? *)
  apply ev_SS. 
  apply ev_0. 
Qed.

применение ev_SS. смущает меня.Если я подключу число к «правилу вывода», я получу, что оно увеличивается, а не уменьшается:

ev 2 == ev 2 -> ev (S (S 2)).

что я неправильно понимаю?

---

Точно так же, что здесь происходит?:

Theorem ev_4' : ev 4.
Proof. 
  apply (ev_SS 2 (ev_SS 0 ev_0)). 
Qed.

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

Answer 1

Когда вы оцениваете термин «n увеличится», но когда вы делаете индуктивное доказательство, вы спрашиваете «как я сюда попал?»И, если у вас есть доказательство того, что ev (S (S n)) верно, то единственный способ, которым вы могли бы прийти туда (если ваша логика верна), это то, что ev n также верно.

Answer 2

После прочтения большей части документации Coq по тактике Я думаю, что в целом я был сбит с толку больше о тактике Coq, чем об этом конкретном примере.Из моего прочтения видно, что tactics implement backward reasoning., как сказано в документации.Из документов: “to prove this I have to prove this and this”. For instance, to prove A ∧ B, I have to prove A and I have to prove B. Итак, чтобы доказать ev 4, нам нужно доказать ev 2 и так далее.«Применить» просто пытается сопоставить текущую цель с тем термином, которым мы ее кормим, и произвести определенное количество подцелей, которое нам нужно доказать, доказать или сопоставить.

Я думаю, что главное в том, что из-за определения ev_SS мы знаем, что если ev 2 истинно, то, поскольку мы определили значение для истинности ev 2 => ev 4, тогда мы можем заключить ev 4.Так что нам действительно нужно только проверить, что ev 2 верно.Если мы докажем это, то по Модусу Поненсу (МП) мы узнаем, что ev 4 верно.Вот почему обратное рассуждение «работает», потому что мы сопоставляем цели с выводом некоторого истинного правила вывода и, таким образом, цель является истинной, когда мы показываем, что предпосылки истинны (из-заправило вывода).Я говорю это, потому что мне показалось странным начинать с цели, потому что мы не знали, что это правда (пока).Хотя теперь я вижу, что мы показываем цель истинной, просто показывая предпосылки и соответствуя правильным правилам вывода.По крайней мере, для этого примера.

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

Answer 3

Тактика apply пытается использовать функцию / лемму / и т.д.доказать текущую цель.В вашем случае текущая цель была ev 4, поэтому для использования ev_SS нам нужно сопоставить вывод из ev_SS с целью.ev_SS : forall n : nat, ev n -> ev (S (S n))., поэтому вывод ev (S (S n)).Чтобы сопоставить это с ev 4, n должно быть 2.

Как только apply выяснит, что вам еще нужно доказать, это сделает эти вещи новыми целями.В этом случае ev_SS принимает в качестве помещения натуральное число n и что-то типа ev n.Так как выяснилось, что n должно быть 2, цель остается ev 2.Следующее использование apply использует n := 0, поэтому оставшаяся цель - ev 0.Наконец, ev_0 не имеет никаких предпосылок, поэтому использование apply ev_0 не оставляет оставшихся целей.

Если это не поможет, подумайте о том, как будет выглядеть неофициальное доказательство этого.По определению ноль - четное число, а если n - четное число, n + 2 - четное.Как мы докажем, что 4 четно?Ну, это даже потому, что 2 четный.Зачем?2 четное, потому что 0 четное.Зачем?0 по определению четно.

Теорема ev_4' содержит сразу весь доказательский член.apply видит, что доказывать нечего, поэтому новых целей нет.Это применение apply точно так же, как и тактика exact.

. Чтобы узнать подробности работы тактики, я рекомендую прочитать документацию .Однако, поскольку документация часто носит технический характер и не содержит примеров, важно прочитать сценарии Coq других людей и просто поэкспериментировать самостоятельно.

---

По поводу ваших комментариев:

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

Можно работать из помещения, а не из цели, используя что-то вроде set (ev_2 := ev_SS ev_0), затем exact (ev_SS ev_2).Это может составить хороший отдельный вопрос.

и почему ev_0: ev 0 рассматривается как истинное предложение?Это потому, что это часть индуктивного определения?

Да.Помните, что ev определяется как

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

, поэтому ev_0 : ev 0 по определению.

Вы также можете объяснить мне, какой синтаксис применяется (ev_SS 2 (ev_SS 0 ev_0)).средства?

Это означает "вызвать тактику apply с аргументом (ev_SS 2 (ev_SS 0 ev_0)). Если вы еще не поняли, Coq использует синтаксис f x вместо того, что обычно пишется f(x)в математике. Coq также использует curry для представления функций с несколькими аргументами. Вместо f(x, y) мы пишем f x y. Это действительно означает что-то вроде f(x)(y), так что f(x) - это функция, котораяпринимает в качестве аргумента y. Если бы мы переписали эту строку с использованием более обычного синтаксиса, это было бы apply(ev_SS(2, ev_SS(0, ev_0))).