Почему должны быть взаимно индуктивные типы, имеющие одинаковые параметры?

Question

Следуя Arthur's suggestion, я изменил отношение к взаимному соотношению Inductive, которое «создает» различные сравнения между играми, а не «сверление».

Но теперь я получаю совершенно новое сообщение об ошибке:

Error: Parameters should be syntactically the same for each inductive type. 

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

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

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

(Определения всех типов и такие термины, как compare_quest, игры, и т.д. g1side не отличаются от того, что они были в моей first question.

Inductive gameCompare (c : compare_quest) : game -> game -> Prop := 
| igc : forall g1 g2 : game, 
    innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 -> 
    gameCompare c g1 g2 
with innerGCompare (next_c : compare_quest) (cbn : combiner) (g1s g2s : side) 
    : game -> game -> Prop := 
| compBoth : forall g1 g2 : game, 
    cbn (listGameCompare next_c cbn (g1s g1) g2) 
     (gameListCompare next_c cbn g1 (g2s g2)) -> 
    innerGCompare next_c cbn g1s g2s g1 g2 
with listGameCompare (c : compare_quest) (cbn : combiner) : gamelist -> game -> Prop := 
| emptylgCompare : cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2 
| otlgCompare : forall (g1_cdr : gamelist) (g1_car g2 : game), 
    (cbn (listGameCompare c cbn g1_cdr g2) (gameCompare c g1_car g2)) -> 
    listGameCompare c cbn (listCons g1_car g1_cdr) g2 
with gameListCompare (c : compare_quest) (cbn : combiner) : game -> gamelist -> Prop := 
| emptyglCompare : cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist 
| otglCompare : forall (g1 g2_car : game) (g2_cdr : gamelist), 
    (cbn (gameListCompare c cbn g1 g2_cdr) (gameCompare c g1 g2_car)) -> 
    gameListCompare c cbn g1 (listCons g2_car g2_cdr). 

В ВКТ, как правило, два игрока (названные Left и Right) по очереди играет в игру, в которой побеждает игрок, чтобы сделать последний ход. Каждая игра (то есть каждая позиция в игре) может быть прочитана как набор опций Left и набор опций Right, написанный как {G_L | G_R}. сравнивая две игры, они могут сравниваться любым из четырех способов: <, >, =, или ||.

Игра A < B если B строго лучше, чем A для Left, независимо от того, кто идет первым. A > B, если A лучше, чем B для Left. A = B, если две игры эквивалентны (в том смысле, что сумма игр A + -B - это игра с нулевой игрой, так что проигравший игрок проиграет). И, A || B, если какая-то игра лучше для Left зависит от того, кто идет первым.

Один из способов проверить сравнение между двумя играми заключается в следующем:

• A <= B если все A «s Left детей <| B и A <| все B» правильных детей s.

• A <| B если A имеет правильный ребенок, который <= B или если A <= любой из левых детей B «s.

• И, аналогично для >= и >|.

Итак, то, видя, какая пара этих отношений относится к двум играм A и B, можно определить, является ли A < B (A<=B и A<|B), A=B (A<=B и A>=B) A > B (A>=B и A>|B) , или A || B (A<|B и A>|B).

Вот wiki article on CGT.

Answer 1

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

Возможно, это должно быть отправлено в список рассылки Coq Club? :)

Вам не нужно ставить все справа от стрелки, чтобы заставить это работать. Единственное, что вы можете сделать, это поместить все, кроме параметра compare_quest, вправо. При использовании индуктивной того же типа, что вы определяете в конструкторе, параметр вы даете не должны быть такими же, как тот, который вы даете на заголовок, так что все нормально:

Inductive gameCompare (c : compare_quest) : game -> game -> Prop := 
| igc : forall g1 g2 : game, 
    innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 -> 
    gameCompare c g1 g2 

with innerGCompare (c : compare_quest) : combiner -> side -> side -> 
    game -> game -> Prop := 
| compBoth : forall cbn g1s g2s (g1 g2 : game), 
    cbn (listGameCompare c cbn (g1s g1) g2) 
     (gameListCompare c cbn g1 (g2s g2)) -> 
    innerGCompare c cbn g1s g2s g1 g2 

with listGameCompare (c : compare_quest) : combiner -> gamelist -> game -> Prop := 
| emptylgCompare : forall cbn, cbn_init cbn -> forall g2 : game, listGameCompare c cbn emptylist g2 
| otlgCompare : forall cbn (g1_cdr : gamelist) (g1_car g2 : game), 
    (cbn (listGameCompare c cbn g1_cdr g2) (gameCompare c g1_car g2)) -> 
    listGameCompare c cbn (listCons g1_car g1_cdr) g2 

with gameListCompare (c : compare_quest) : combiner -> game -> gamelist -> Prop := 
| emptyglCompare : forall cbn, cbn_init cbn -> forall g1 : game, gameListCompare c cbn g1 emptylist 
| otglCompare : forall cbn (g1 g2_car : game) (g2_cdr : gamelist), 
    (cbn (gameListCompare c cbn g1 g2_cdr) (gameCompare c g1 g2_car)) -> 
    gameListCompare c cbn g1 (listCons g2_car g2_cdr). 

К сожалению , пытаясь оценить это дает новую ошибку :(

Error: Non strictly positive occurrence of "listGameCompare" in 
"forall (cbn : Prop -> Prop -> Prop) (g1s g2s : game -> gamelist) 
    (g1 g2 : game), 
    cbn (listGameCompare c cbn (g1s g1) g2) (gameListCompare c cbn g1 (g2s g2)) -> 
    innerGCompare c cbn g1s g2s g1 g2". 

Эта ошибка является гораздо более распространенным в Coq. Она жалуется, что вы передаете типа вы определяете в качестве аргумента cbn потому, что может приводить к тому, тип находится на слева стрелки (отрицательное вхождение), которое, как известно, приводит к логическому i nconsistencies.

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

ОБНОВЛЕНИЕ: Я начал серию статей о формализации некоторых из CGT в Coq. Вы можете найти первый номер here.