Coq: Обход условия равномерного наследования

Мне трудно понять (пункт) перчатку нужно пройти, чтобы обойти условие единого наследования (UIC). По инструкции

Пусть /.../ f: forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘ — функция, не проверяющая условие равномерного наследования. Чтобы объявить f как принуждение, нужно сначала объявить подкласс C' из C /.../

В приведенном ниже коде f является такой функцией:

Parameter C: nat -> Type.
Parameter D: nat -> Prop.
Parameter f: forall {x y}(z:C x), D y.
Parameter f':> forall {x y}(z:C x), D y. (*violates uic*)
Print Coercions. (* @f' *)

Тем не менее, мне не нужно ничего делать, кроме как поставить :>, чтобы объявить это принуждением. Может, перчатка как-то поможет избежать взлома УИК? Не так:

Definition C' := fun x => C x.
Fail Definition Id_C_f := fun x d (y: C' x) => (y: C d). (*attempt to define Id_C_f as in the manual*)
Identity Coercion Id_C_f: C' >-> C.
Fail Coercion f: C' >-> D. (*Cannot recognize C' as a source class of f*)
Coercion f'' {x y}(z:C' x): D y := f z. (*violates uic*)
Print Coercions. (* @f' @f'' Id_C_f *)

Вопрос: Что мне здесь не хватает?


subtype coercion coq
person jaam    schedule 08.05.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Мне трудно понять (точку) перчатку, которую нужно пройти, чтобы обойти условие единого наследования (UIC).

Интуитивно условие равномерного наследования говорит (примерно) «синтаксически возможно определить каждый аргумент функции принуждения только из типа исходного аргумента».

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

При этом обратите внимание, что при объявлении приведения, нарушающего UIC, появляется предупреждающее сообщение (а не сообщение об ошибке). Он все равно добавит его в таблицу приведения. В зависимости от вашей версии Coq приведение может никогда не срабатывать, или вы можете получить сообщение об ошибке во время вывода типа, когда код, применяющий приведение, создает термин с неправильным типом, потому что он пытается применить приведение, предполагая, что UIC сохраняется, когда он на самом деле нет, или (в более старых версиях Coq) вы можете получить аномалии (см., например, отчеты об ошибках #4114, #4507, #4635, #3373 и #2828).

Тем не менее вот пример, когда Identity Coercion полезны:

Require Import Coq.PArith.PArith. (* positive *)
Require Import Coq.FSets.FMapPositive.

Definition lookup {A} (map : PositiveMap.t A) (idx : positive) : option A
  := PositiveMap.find idx map.

(* allows us to apply maps as if they were functions *)
Coercion lookup : PositiveMap.t >-> Funclass.

Definition nat_tree := PositiveMap.t nat.
Axiom mymap1 : PositiveMap.t nat.
Axiom mymap2 : nat_tree.

Local Open Scope positive_scope. (* let 1 mean 1:positive *)

Check mymap1 1. (* mymap1 1 : option nat *)
Fail Check mymap2 1.
(* The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "mymap2" of type "nat_tree"
cannot be applied to the term
 "1" : "positive" *)
Identity Coercion Id_nat_tree : nat_tree >-> PositiveMap.t.
Check mymap2 1. (* mymap2 1 : option nat *)

По сути, в очень ограниченном случае, когда у вас есть идентификатор, который будет распознан как источник существующего приведения, если вы немного развернете его тип, вы можете использовать Identity Coercion для этого. (Вы также можете сделать это, определив копию вашего существующего приведения с другой сигнатурой типа и объявив, что это тоже приведение. Но тогда, если у вас есть несколько лемм, в которых упоминается одно приведение, и несколько лемм, в которых упоминается другое, rewrite будет иметь вопросы.)

Существует еще один вариант использования Identity Coercions: когда ваш источник не является индуктивным типом, вы можете использовать их для свертывания, а не только для развертывания идентификаторов, играя трюки с Modules и Module Types; в качестве примера см. этот комментарий к #3115.

В общем, я не знаю способа обойти условие равномерного наследования.

person Jason Gross    schedule 10.05.2018