coq - 指定模块类型中的极性

Question

Coq 接受以下 U 的归纳定义，因为它可以看到 U 在 M.T U -> U 中出现的次数是严格积极。

Module M.

Definition T (A : Type) : Type := unit -> A.

End M.

Module N.

Inductive U : Type :=
| c : M.T U -> U.

End N.

另一方面，Coq 不接受以下 U 的归纳定义，因为根据 M.T 的定义，它可能会出现非严格正的情况.

Module Type S.

Parameter T : Type -> Type.

End S.

Module N (M : S).

Fail Inductive U : Type :=
| c : M.T U -> U.

End N.

如何在签名 S 中指定 T 的参数只能严格出现负数？从而防止 U 在其定义中出现任何非严格正向的情况。

Answer 1

这个U类型可以看作M.T的最小不动点。另一种常见的编码是

Definition Mu (T : Type -> Type) := forall A, (T A -> A) -> A.
Definition U := Mu M.T.

假设T是一个仿函数(这可能意味着严格的积极性？):

Parameter map : forall A B, (A -> B) -> T A -> T B. (* in module M *)

我们有一个构造函数和析构函数:

Definition c : M.T U -> U := fun x A f =>
   f (M.map _ _ (fun y => y _ f) x).

Definition d : U -> M.T U := fun y => y _ (fun x => M.map _ _ c x).

显示它们是逆的需要参数化，因此没有直接的方法来证明它。如果您不想将其公理化，您可以丰富 T 和 U 以携带参数性证据。

<小时/>

本质上，上面要求 T 是仿函数的要求是严格正性条件的语义替换/近似，这是语法上的。

<小时/>

还可以使用这个新插件关闭积极性检查:

https://github.com/SimonBoulier/TypingFlags