coq - 为什么 FMapAVL 在参数中的使用不是严格正数，而列表却是严格正数？

Question

考虑以下代码:

Require Import FMapAVL.
Require Import Coq.Structures.OrderedTypeEx.

Module NatMap := FMapAVL.Make(Nat_as_OT).

Inductive ttree (K : Type) (V : Type) :=
| tleaf : ttree K V
| tnode : ttree K V -> K -> V -> ttree K V -> nat -> ttree K V.

Inductive test :=
| test1 : test
| test2 : ttree nat test -> test   
| test3 : list test -> test
| test4 : NatMap.t test -> test.

在 Coq 8.6 中，我得到错误:“NatMap.t test -> test”中“test”的非严格正数出现。如果没有 test4，我不会得到任何错误.

为什么将 NatMap.t(带有 nat 键的 FMapAVL)构造函数应用于我的 test 归纳类型在应用 list 构造函数甚至 ttree 构造函数(就像 FMapAVL 的内部结构)时创建一个非严格正的事件，好吗？

如果我想要示例中的 test4 之类的内容，最好是不需要我自己制作像 ttree 这样的 map 实现，那么常见的解决方法是什么？

Answer 1

问题是 Coq 无法将某些高阶归纳类型作为嵌套归纳处理 - 我不确信我完全理解这些限制，但我进行了一些调查。

有助于解释该行为的一个重要事实是 Coq 对将归纳类型传递给类型构造函数有特殊支持。 CPDT's Inductive Types本章在嵌套归纳类型部分对此进行了解释:Coq 创建专门用于 test 的 list 或 ttree 版本，并假装您正在定义 tree 和这些具有互归纳功能的专门归纳法。这通常工作得很好(例如对于您的 list 甚至 ttree 定义)。它甚至适用于模块，只要它们使用“transparent ascription ”(并且 FMapAVL.Make 就是这样做的)。但是，当类型是索引而不是参数时(即，当 Type 位于冒号右侧而不是左侧时)，它似乎会崩溃:

Module Type Transformer.
  Axiom T:Type -> Type.
End Transformer.

Module IdOpaque : Transformer.
  Definition T (t:Type) := t.
End IdOpaque.

Inductive transformer : Type -> Type :=
| MkT : forall t, t -> transformer t .

(* make the argument a parameter *)
Inductive transformer' (t:Type) : Type :=
| MkT' : t -> transformer' t.

Module IdInd <: Transformer.
  Definition T : Type -> Type := transformer.
End IdInd.

Module IdTransparent <: Transformer.
  Definition T (t:Type) : Type := t.
End IdTransparent.

(* works with a simple definition, even inside a module, as long as its
transparent *)
Inductive test1 :=
| mkTest1 (_:IdTransparent.T test1).

(* not strictly positive (Coq can't see definition) *)
Fail Inductive test2 :=
| mkTest2 (_:IdOpaque.T test2).

(* this is pretty much what happens with FMapAVL.Make *)
Fail Inductive test3 :=
| mkTest3 (_:IdInd.T test3).

(* even this fails *)
Fail Inductive test4 :=
| mkTest4 (_:transformer test4).

(* this finally works *)
Inductive test5 :=
| mkTest5 (_:transformer' test5).