Как индуктивное суждение работает в Coq?

Question

Я проходил через IndProp в основах программного обеспечения и в главе 4 книги Адама Члипалы, и у меня были трудности с пониманием индуктивных предложений.

Для примера приведем:

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

Мне кажется, я понимаю "нормальные" типы, используя Set, например:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

и такие вещи, как O, просто возвращают один объект типа nat, а S O берет объект типа nat и возвращает другой другой объект того же типа nat.Под другим объектом я предполагаю, что они имеют разные значения.

Что меня смущает, так это то, как конструкторы для индуктивных реквизитов отличаются от индуктивных типов Set.Для Set кажется, что они просто ведут себя как функция, функция, которая принимает значения и возвращает больше значений этого типа.Но для индуктивных предложений мне трудно понять, что они делают.

Например, возьмем ev_0 в качестве простого примера.Я предполагаю, что это имя для пропозиционального объекта (значения) ev 0.Поскольку оно само по себе ev 0 должно быть Prop предложением.Но что именно делает это правдой?Я полагаю, что если это предложение, оно может быть ложным.Я предполагаю, что индукция сбивает меня с толку.ev - это «функция, которая возвращает объекты некоторого типа (предложения)», поэтому ev 0 - это просто предложение, но мы не сказали, что должно означать ev 0 (в отличие от моего определения натурального числа, базовый случай ясенчто он делает).В Python я ожидал бы увидеть

n == 0: return True

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

Также меня смущает название.В nat имя O имело решающее значение для строительства / строительства объектов.Но в индуктивном определении ev_0 больше похоже на метку / указатель на действительное значение ev 0.Так что я бы предположил, что ev_SS == ev_0 -? ev 2 на самом деле не имеет смысла, но я не знаю почему.Чем метки здесь отличаются от меток в индуктивных типах, использующих set?

Для ev_SS, что еще более запутанно.Поскольку я не знаю, что делают ярлыки, конечно, это сбивает меня с толку, но посмотрите, как это указывает:

forall n : nat, ev n -> ev (S (S n))

, поэтому, учитывая натуральное число n, я предполагаю, что оно возвращает предложение ev n -> ev (S (S n)) (IЯ предполагаю, что forall n : nat не является частью объекта предложения и просто указывает, когда работает конструктор, который возвращает предложения).Так что forall n : nat, ev n -> ev (S (S n)) на самом деле не предложение, а ev n -> ev (S (S n)).

Может кто-нибудь помочь мне прояснить, как тип индуктивного предложения действительно работает в Coq?

---

Заметьте, я не совсем понимаю разницу между Set против Type, но я считаю, чтобыл бы совсем другой пост сам по себе.

---

Еще несколько комментариев:

Я немного поиграл с этим и сделал:

Check ev_SS

имое удивление получилось:

ev_SS
     : forall n : nat, ev n -> ev (S (S n))

Я думаю, что это неожиданно, потому что я не ожидал, что тип ev_SS (если я не неправильно понимаю, что должен делать Check) будет определениемсама функция.Я думал, что ev_SS был конструктором, поэтому я подумал, что в этом случае будет отображаться nat -> Prop, поэтому, конечно, это тот тип, который я ожидал.

Answer 1

Если вы замените Prop на Set, тогда вы скажете, что понимаете определение:

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

Для каждого n : nat мы думаем о ev' n как о типе, который имеет некоторые элементы, иливозможно нет.Поскольку это индуктивное определение, мы можем сказать, что представляют собой элементы ev' 0: единственным элементом является ev_0' (или, точнее, каждый закрытый член типа ev' 0 вычисляется до ev_0;).Нет элементов ev_0 1, но есть элемент ev 2', а именно ev_SS' 0 ev_0'.На самом деле, немного размышлений показывает, что ev n является либо пустым, либо одиночным, в зависимости от того, является ли n четным или нечетным.

Это точно так же, когда мы переключаемся с Set на Prop, за исключением того, что чтение отличается: Set - это (большой) тип типов, Prop также является типом типов (это юниверсы ).Каждый элемент Prop является типом (но мы предпочитаем называть его «предложением»), который имеет некоторые элементы (но мы предпочитаем называть их «доказательствами»).Итак, рассмотрим следующее:

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

Для каждого n : nat мы считаем ev n утверждением, что n обладает свойством ev, каким бы оно ни было.Для любого предложения n может существовать доказательство ev n, в этом случае n имеет свойство ev, или может не быть такого доказательства, и в этом случае n не имеет свойства ev.Поскольку это индуктивное определение, мы можем сказать, каковы доказательства ev_0: все они вычисляются до ev_0'.Доказательств ev_0 1 нет, но есть доказательство ev 2, а именно ev_SS 0 ev_0.На самом деле, немного размышлений показывает, что ev n имеет доказательство тогда и только тогда, когда n четно.Теперь мы понимаем, что ev является свойством быть «четным».

Это известно как «суждения как типы».

Мы заметили, что ev' 0 содержит только один элемент ev_0'.Тип unit также содержит только один элемент tt.Значит ли это, что ev' 0 и unit равны?Нет, но они эквивалентны , потому что мы можем предоставить функции ev' 0 -> unit и unit -> ev' 0, которые являются противоположными друг другу.

Мы можем задать тот же вопрос о ev 0:равно True?Нет, но они эквивалентны , потому что мы можем доказать значения ev 0 -> True и True -> ev' 0.

. Вы начинаете задумываться, в чем разница между Prop и Set.Для типа P : Prop все его элементы считаются равными, т. Е. Coq не позволяет нам различать их.(Это немного педагогическая ложь, потому что на самом деле Coq агностик о том, считаются ли все элементы P равными, но, возможно, сейчас лучше этого не делать.)

Answer 2

Итак, во-первых, это нормально для вас, чтобы быть смущенным этим, но это может быть проще, чем вы думаете!

Есть два различных понятия, которые вы запутали, поэтому давайте рассмотрим их по одномувремя.Во-первых, вы упоминаете, что ev 0 - это предложение, и удивляетесь, что делает его правдивым.В какой-то момент вы узнаете, что суждения и типы - это одно и то же, и различие между Prop и Set и Type не в том, что эти вещи по своей сути различны.

Итак, когда вы определяететип (или предложение) nat, вы создаете новый тип и описываете, какие значения существуют в нем.Вы заявляете, что существует значение O, то есть nat.И вы объявляете, что есть параметризованное значение S, то есть nat, когда передано nat.

Таким же образом, когда вы определяете тип (или предложение) evвы создаете новый тип (ну, на самом деле это семейство типов, индексируемых значениями типа nat) и описываете, какие значения существуют в этих ev типах.Вы заявляете, что существует значение ev_0, то есть ev 0.И вы заявляете, что есть параметризованное значение ev_SS, то есть ev (S (S n)), когда передано n : nat и ev n.

Итак, вы сделали предложениеправда, имея способы создания ценностей внутри него.Вы также можете определить ложное предложение, не имея конструкторов или имея конструкторы, которые никогда не могут быть вызваны:

Inductive MyFalse1 := . (* no constructor! *)

Inductive MyFalse2 :=
| TryToConstructMe : False ->  MyFalse2
| ThisWontWorkEither : 0 = 1 -> MyFalse2
.

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

---

Что касается именования вещей, ev_0, ev_SS, O и S все одинаковывид объекта: конструктор.Я не уверен, почему вы думаете, что ev_0 является указателем на значение ev 0.

Нет смысла присваивать ev n в качестве предложения, кроме того, что это предложение может бытьЗначение true, если существует способ для создания значения с типом ev n, и может быть ложным, если нет способа создать значение с типом ev n.

Однако обратите внимание, что ev n былтщательно продуманный, чтобы быть обитаемым ровно для тех n с, которые являются четными, и необитаемыми именно для тех n с, которые являются нечетными.В этом смысле ev фиксирует предложение.Если вы получаете значение типа ev n, оно по существу утверждает, что n является четным числом, поскольку тип ev n содержит жителей только для четных значений:

• ev 0 содержит 1житель (ev_0)
• ev 1 содержит 0 жителей
• ev 2 содержит 1 жителя (ev_SS 0 ev_0)
• ev 3 содержит 0 жителей
• ev 4 содержит 1 жителя (ev_SS 2 (ev_SS 0 ev_0))
• и т. Д.

---

Наконец, для разницы между Set, Prop и Type, это все вселенные, в которых вы можете создавать индуктивные типы, но они имеют определенные ограничения.

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

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

Вы действительно должны стараться не думать о Prop как о волшебной вещи, отличной от Set.

---

Вам может помочь следующее: мы могли бы переписать определения nat и ev, полностью эквивалентным образом, как:

Inductive nat1 : Set :=
| O : nat1
| S : nat1 -> nat1
.
(* is the same as *)
Inductive nat1 : Set :=
| O : nat1
| S : forall (n : nat1), nat1
.

(* and *)
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall (n : nat), ev n -> ev (S (S n))
.
(* is the same as *)
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall (n : nat) (e : ev n), ev (S (S n))
.

Каждый раз, когда вы видите тип, похожий на a -> b, это действительно сокращение для forall (_ : a), b, то есть мы ожидаем ввод типа a и возвращаем вывод типа b.

Причина, по которой мы пишем forall (n : nat) в ev_SS, заключается в том, что у нас есть для присвоения имени первому аргументу, поскольку тип второго аргумента будет зависеть от него (второй аргумент имеетвведите ev n).