Как мне прочитать определение ex_intro?

Я читаю вводный урок Майка Нахаса по Coq, в котором говорится:

Аргументы для ex_intro:

  • предикат
  • свидетель
  • доказательство предиката, вызванного со свидетелем

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

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

и у меня возникли проблемы с анализом. Какие части выражения forall x:A, P x -> ex (A:=A) P соответствуют этим трем аргументам (предикат, свидетель и доказательство)?

Источник

2 ответа

Решение

Чтобы понять, что имел в виду Майк, лучше запустить интерпретатор Coq и запросить тип ex_intro:

Check ex_intro.

Затем вы должны увидеть:

ex_intro
     : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x

Это говорит о том, что ex_intro принимает не только 3, но 4 аргумента:

  • тип вещи, которую вы определяете количественно, A;
  • предикат P : A -> Prop;
  • свидетель x : A; а также
  • доказательство P xутверждая, что x является действительным свидетелем.

Если вы объедините все эти вещи, вы получите доказательство exists x : A, P x, Например, @ex_intro nat (fun n => n = 3) 3 eq_refl является доказательством exists n, n = 3,

Таким образом, разница между фактическим типом ex_intro и тот, который вы прочитали в определении, состоит в том, что первый включает в себя все параметры, которые даны в заголовке - в этом случае, A а также P,

Источник

Да, эти определения индуктивного типа могут быть трудными для чтения.

Первая часть:

Inductive ex (A:Type) (P:A -> Prop) : Prop :=

Это то, что связано с самим типом. Поэтому каждый раз, когда вы видите exбудет иметь A и и P и ex будет иметь тип Prop, Пропуская A на данный момент, давайте сосредоточимся на P который является предикатом. Итак, если мы используем в качестве нашего примера "существует натуральное число, которое является простым", P возможно is_prime, где is_prime занимает nat (натуральное число) в качестве аргумента, и может существовать доказательство этого, если nat прост.

В этом примере A было бы nat, В учебнике, A не упоминается, потому что Coq всегда может вывести это. Учитывая предикат, Coq может получить тип A глядя на тип аргумента предиката.

Подводя итог, здесь, в нашем примере, тип будет ex nat is_prime, Это говорит о том, что существует nat, который является простым, но он не говорит, какой nat. Когда мы строим ex nat is_primeнам нужно будет сказать, какой из них - нам понадобится "свидетель". И это приводит нас к определению конструктора:

ex_intro : forall x:A, P x -> ex (A:=A) P.

Конструктор назван ex_intro, Хитрость здесь в том, что конструктор имеет все параметры для типа. Итак, прежде чем мы перейдем к перечисленным ex_introмы должны включить те для типа: A а также P,

После этих параметров идут те, которые перечислены после ex_intro: xкоторый является свидетелем, и P x, что является доказательством того, что предикат верен для свидетеля. Используя наш пример, x может быть 2 и P x будет доказательством (is_prime 2),

Конструктор должен указать параметры для типа ex что это строит. Вот что происходит после стрелки (->). Они не должны соответствовать параметрам, используемым при вызове конструктора, но обычно они соответствуют. Чтобы достичь этого, аргумент A не выводится - это передается явно. (A:=A) говорит что параметр A в ex должен быть равен A в вызове конструктору. Аналогично, параметры P из ex устанавливается на P от звонка до конструктора.

Итак, если бы мы имели proof_that_2_is_prime с типом (prime 2)мы можем позвонить ex_intro is_prime 2 proof_that_2_is_prime и это будет иметь тип ex nat is_prime, Что является нашим доказательством того, что существует натуральное число, которое является простым.

Чтобы ответить на ваш вопрос напрямую: в выражении forall x:A, P x -> ex (A:=A), x:A является свидетелем и P x является доказательством того, что свидетель является правдой. Выражение не содержит предикат, потому что это часть параметров типа, которые должны быть переданы в конструктор ex_intro, Список параметров учебника не включает A, потому что выводится Coq.

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

Источник
Другие вопросы по тегам