coq - 放宽 Coq 的严格肯定性检查器不查看正在定义的归纳类型的类型索引是否不一致？

Question

写作

Inductive Foo : Type -> Type :=
| foo : Foo Bar
with
Bar := .

给

Error: Non strictly positive occurrence of "Bar" in "Foo Bar".

我知道为什么需要严格的积极性的标准例子；如果我有

Inductive Fix :=
| fFix : (Fix -> Fix) -> Fix.

带消除器

Fix_rect : forall (P : Fix -> Type) (v : forall f, (forall x, P (f x)) -> P (fFix f)) (f : Fix), P f

然后我可以证明荒谬

Fix_rect (fun _ => False) (fun f H => H (fFix id)) (fFix id) : False

(旁白:如果消除器是

Fix_rect : forall (P : Fix -> Type) (v : forall f, (forall x, P x -> P (f x)) -> P (fFix f)) (f : Fix), P f

？)

但是，我没有看到使用仅出现在索引中的事件的方法。如果类型索引中允许出现非严格正的情况，是否有办法推导出类似的矛盾？

Answer 1

与错误消息相反，这似乎不是一个积极的问题。相反，因为你有相互索引，这是一种归纳归纳类型(一个奇怪的“大”类型)，Coq 不支持。

您可以尝试定义非索引类型，并将递归定义的“格式良好”关系分开，这些关系编码正确的索引。例如

Inductive PreFoo : Type :=
| foo : PreFoo.

Inductive Bar : Type :=.

Fixpoint FooWf (f : PreFoo) (t : Type) : Prop :=
  match f with
  | foo => (t = Bar)
  end.

Definition Foo (t : Type) := sig (fun f => FooWf f t).  

这类似于您可能如何为类型理论或具有单独类型关系的外部预语法索引内在语法。