Coq：绕过统一继承条件
Coq: Bypassing the uniform inheritance condition
我很难理解 gauntlet 必须通过以绕过统一继承条件 (UIC) 的（要点）。根据说明
Let /.../ f: forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘ be a
function which does not verify the uniform inheritance condition. To
declare f as coercion, one has first to declare a subclass C' of 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' *)
然而，除了将 :> 声明为强制转换外，我不需要做任何事情。也许手套会以某种方式帮助避免破坏 UIC？不是这样：
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 *)
问题：我在这里错过了什么？
I've trouble understanding the (point of the) gauntlet one has to pass to bypass the uniform inheritance condition (UIC).
直觉上，统一继承条件表示（大致）"it's syntactically possible to determine every argument to the coercion function just from the type of the source argument"。
添加强制转换的开发人员发现，如果假定统一继承条件，则更容易（我推测）编写实现强制转换的代码。我确信 pull request 放宽此约束并正确实施更一般的强制转换会受到欢迎！
也就是说，请注意，当您声明违反 UIC 的强制转换时，会出现 警告 消息（不是错误消息）。它仍然会将其添加到强制转换的 table 中。根据您的 Coq 版本，强制转换可能永远不会触发，或者当应用强制转换的代码构建错误类型的术语时，您可能会在类型推断时收到错误消息，因为它会假设 UIC 实际上成立时尝试应用强制转换不会，或者（在旧版本的 Coq 中）您会遇到异常情况（例如，参见错误报告 #4114, #4507, #4635, #3373, and #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 玩花样；有关示例，请参阅 this comment on #3115。
不过，一般来说，据我所知，没有一种方法可以绕过统一继承条件。
我很难理解 gauntlet 必须通过以绕过统一继承条件 (UIC) 的（要点）。根据说明
Let /.../
f: forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘbe a function which does not verify the uniform inheritance condition. To declarefas coercion, one has first to declare a subclassC'ofC/.../
在下面的代码中，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' *)
然而，除了将 :> 声明为强制转换外，我不需要做任何事情。也许手套会以某种方式帮助避免破坏 UIC？不是这样：
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 *)
问题：我在这里错过了什么？
I've trouble understanding the (point of the) gauntlet one has to pass to bypass the uniform inheritance condition (UIC).
直觉上，统一继承条件表示（大致）"it's syntactically possible to determine every argument to the coercion function just from the type of the source argument"。
添加强制转换的开发人员发现，如果假定统一继承条件，则更容易（我推测）编写实现强制转换的代码。我确信 pull request 放宽此约束并正确实施更一般的强制转换会受到欢迎！
也就是说，请注意，当您声明违反 UIC 的强制转换时，会出现 警告 消息（不是错误消息）。它仍然会将其添加到强制转换的 table 中。根据您的 Coq 版本，强制转换可能永远不会触发，或者当应用强制转换的代码构建错误类型的术语时，您可能会在类型推断时收到错误消息，因为它会假设 UIC 实际上成立时尝试应用强制转换不会，或者（在旧版本的 Coq 中）您会遇到异常情况（例如，参见错误报告 #4114, #4507, #4635, #3373, and #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 玩花样；有关示例，请参阅 this comment on #3115。
不过，一般来说，据我所知，没有一种方法可以绕过统一继承条件。