Вы не можете использовать индуктивные типы, чтобы получить что-то, что воплощает в точности первые два принципа, не получив двух других. Причина в том, что индуктивные типы данных Coq автоматически поддерживают строго зависимое исключение, что означает, что типу результата разрешено ссылаться на удаляемый элемент. Это то, что вы видите в последних двух наборах правил, которые вы дали: типу C разрешено ссылаться на доказательство p того, что две точки a и b равны. Любой разумно определенный индуктивно определенный тип равенства будет автоматически поддерживать правила 3 и 4 и, следовательно, 1 и 2, которые являются более слабыми. Например, вот как вы получаете 1 и 2 при стандартном равенстве Coq.
Section Gentzen.
Variables (A : Type) (C : A -> A -> Type).
Definition e_id_g {a b : A} (p : a = b) (c : C a a) : C a b :=
match p with eq_refl => fun c => c end c.
Definition c_id_g (a : A) (c : C a a) : e_id_g (eq_refl a) c = c :=
eq_refl.
End Gentzen.
Section Leibniz.
Variables (A : Type) (C : A -> A -> Type).
Definition e_id_l {a b : A} (p : a = b) (c : forall x, C x x) : C a b :=
match p with eq_refl => c a end.
Definition c_id_l (a : A) (c : forall x, C x x) :
e_id_l (eq_refl a) c = c a :=
eq_refl.
End Leibniz.
Можно дать другое определение, которое поддерживает только правила 1 и 2, но не 3 и 4, используя кодировку Чёрча равенства:
Definition eq {A} (a b : A) : Prop :=
forall P : A -> Prop, P a -> P b.
Definition refl {A} (a : A) : eq a a :=
fun P x => x.
Идея здесь - как и в аналогичных кодировках для типов данных в лямбда-исчислении - состоит в том, чтобы определить тип как тип его (независимого) элиминатора или свертки. Это определение иногда известно как равенство Лейбница, и оно действительно обеспечивает те же правила доказательства, что и в пунктах 1 и 2, как показано в следующем сценарии.
Section Gentzen.
Variables (A : Type) (C : A -> A -> Prop).
Definition e_id_g {a b : A} (p : eq a b) (c : C a a) : C a b :=
p (C a) c.
Definition c_id_g (a : A) (c : C a a) : e_id_g (refl a) c = c :=
eq_refl.
End Gentzen.
Section Leibniz.
Variables (A : Type) (C : A -> A -> Prop).
Definition e_id_l {a b : A} (p : eq a b) (c : forall x, C x x) : C a b :=
p (C a) (c a).
Definition c_id_l (a : A) (c : forall x, C x x) :
e_id_l (refl a) c = c a :=
eq_refl.
End Leibniz.
(На самом деле эти принципы немного отличаются: они ограничены Prop из-за ограничений базовой теории Coq, связанных с чем-то, называемым непредсказуемостью. Но это ортогональная проблема.)
Без утверждения дополнительных аксиом невозможно получить принципы 3 и 4 для этой новой кодировки равенства. Для доказательства этого потребовалось бы провести анализ случая для элементов типа forall P, P a -> P b и доказать, что все эти элементы имеют форму refl, применимую к чему-либо. Однако это тип функций, и в базовой теории Кока нет способа провести анализ случаев для них. Обратите внимание, что этот аргумент лежит за пределами теории Кока: не противоречит утверждать в качестве дополнительной аксиомы, что 3 и 4 действительны для этого нового типа; это просто невозможно доказать без этих аксиом.
person
Arthur Azevedo De Amorim
schedule
03.08.2017
