Coq:绕过统一继承条件

Question

我很难理解(的)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 *)

问题:我在这里错过了什么？

Answer 1

I've trouble understanding the (point of the) gauntlet one has to pass to bypass the uniform inheritance condition (UIC).

直觉上，统一继承条件(粗略地)说“在语法上可以仅从源参数的类型确定强制函数的每个参数”。

如果假定统一继承条件，添加强制转换的开发人员发现(我推测)编写实现强制转换的代码会更容易。我确定 pull request欢迎放宽此约束并正确实现更一般的强制转换!

也就是说，请注意，当您声明违反 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 来做到这一点。 (您也可以通过使用不同的类型签名定义现有强制的副本，并声明该强制转换来做到这一点。但是如果您有一些引理提到一个强制，而一些引理提到另一个，重写会有问题。)

Identity Coercion 的另一个用例是，当您的源不是归纳类型时，您可以将它们用于折叠，而不仅仅是展开标识符，通过使用Module和Module Type来耍花招；见this comment on #3115举个例子。

不过，总的来说，据我所知，没有一种方法可以绕过统一继承条件。