Смертельный алмаз смерти в Кок

Question

Я пытаюсь создать довольно простую иерархию типов. Вот минимальный рабочий пример:

Record R0 : Type := {
  R0_S :> Type
}.

Record R1 : Type := {
  R1_S   : Type;
  op1    : R1_S -> R1_S
}.

Record R2 : Type := {
  R2_S   : Type;
  op2    : R2_S -> R2_S
}.

Record R12: Type := {
  R12_S   : Type;
  R12_op1 : R12_S -> R12_S;
  R12_op2 : R12_S -> R12_S
}.

Definition R1_0 (r1: R1) := (Build_R0 (R1_S r1)).
Coercion   R1_0 : R1 >-> R0.

Definition R2_0 (r2: R2) := (Build_R0 (R2_S r2)).
Coercion   R2_0 : R2 >-> R0.

Definition R12_1 (r12: R12) := (Build_R1 (R12_S r12) (R12_op1 r12)).
Coercion   R12_1 : R12 >-> R1.

Definition R12_2 (r12: R12) := (Build_R2 (R12_S r12) (R12_op2 r12)).
Coercion   R12_2 : R12 >-> R2.  (* Warning *)

Это последнее принуждение генерирует следующее предупреждение:

Ambiguous paths:
[R12_2; R2_0] : R12 >-> R0
[R12_2; R2_0; R0_S] : R12 >-> Sortclass
R12_2 is now a coercion

Действительно, принуждение от R12 в R0 (или же Sortclass) может идти двумя разными путями. И я понимаю, почему Coq запретил бы это в общем случае. Потому что... какой из них будет использован?

Однако в этом случае можно показать, что принуждение обоими путями R1_0 (R12_1 r12) а также R2_0 (R12_2 r12) точно так же. Но все же я не могу добавить следующие, казалось бы, действительные аксиомы:

Parameter r12 : R12.
Parameter x : r12.
Axiom id1 : (op1 _ x) = x.  (* OK    *)
Axiom id2 : (op2 _ x) = x.  (* Error *)

Вопрос: Так есть ли способ убедить Coq, что это нормально?

Answer 1

Я считаю, что нет никакого способа убедить Coq, что это нормально. Тем не менее, вы достигаете аналогичного эффекта, используя другие функции, такие как канонические структуры или классы типов. Вот как можно перевести ваш пример с классами типов, например:

Class R1 T :=
{
  op1 : T -> T
}.

Class R2 T :=
{
  op2 : T -> T
}.

Class R12 T `{R1 T} `{R2 T} :=
{}.

Section S.

Context T `{R12 T}.
Variable x : T.

Hypothesis id1 : op1 x = x.
Hypothesis id2 : op2 x = x.

End S.

Обратите внимание на этот класс R12 не имеет собственных методов, но требует типа T быть примером обоих R1 а также R2, что приводит морально к тому же. Context Декларация заставляет Coq принимать экземпляры для R1 а также R2 автоматически, в силу этих требований.

Редактировать:

Если вы попытаетесь добавить R0 класс, чтобы завершить диаграмму, вы можете получить странную ошибку, вызванную ошибочным выводом класса типа. Одним из решений является отключение автоматического обобщения в R12 (т.е. убрать обратные кавычки) и принудительно R1 а также R2 основываться на том же R0 пример:

Class R0 (T : Type) := {}.

Class R1 T `{R0 T} :=
{
  op1 : T -> T
}.

Class R2 T `{R0 T} :=
{
  op2 : T -> T
}.

Class R12 T `{R0 T} {r1:R1 T} {r2:R2 T} :=
{}.

Section S.

Context T `{R12 T}.
Variable x : T.

Hypothesis id1 : op1 x = x.
Hypothesis id2 : op2 x = x.

End S.

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