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

Question

У меня проблемы с пониманием (точка) рукавицы , которую нужно пройти, чтобы обойти условие равномерного наследования (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 *)

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

Answer 1

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

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

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

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

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

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 Coercion с, который заключается в том, что, когда ваш источник не индуктивного типа, вы можете использовать их для свертывания , а не только разворачивания идентификаторы, играя трюки с Module с и Module Type с; см. этот комментарий к # 3115 для примера.

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