coq - 由于多态性功能而出现非阳性现象

Question

我正在尝试使用带有列表的构造函数定义数据类型，并包含有关此列表的命题。

这工作正常:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive Foo :=  MkFoo : list Foo -> Foo.

这也是:

Inductive Foo :=  MkFoo : forall (l : list Foo), Foo.

但这失败了

Inductive Foo :=  MkFoo : forall (l : list Foo), l <> [] -> Foo.

与

Non strictly positive occurrence of "Foo"
in "forall l : list Foo, l <> [] -> Foo".

我认为这是因为 [] 实际上是 @nil Foo 并且 Coq 不喜欢 Foo 的出现。

我目前正在使用矢量来解决这个问题，就像这样

Require Import Coq.Vectors.Vector.

Inductive Foo :=  MkFoo : forall n (l : Vector.t Foo n), n <> 0 -> Foo.

但是由于在 Coq 中使用依赖数据结构而出现的复杂性让我想知道:

有没有一种方法可以在 MkFoo 中使用普通列表，并且仍然包含有关该列表的命题？

Answer 1

不幸的是，我认为没有办法直接在定义中包含该约束。我看到两条前进的道路:

1. 更改 mkFoo 的定义，以便它将列表的头部作为附加参数:

   mkFoo : Foo -> list Foo -> Foo
   

2. 定义没有任何限制的Foo，并定义一个单独的格式良好谓词:

   Require Import Coq.Lists.List.
   
   Inductive Foo := mkFoo : list Foo -> Foo.
   
   Definition isEmpty {T : Type} (x : list T) :=
     match x with
     | nil => true
     | _   => false
     end.
   
   Fixpoint wfFoo (x : Foo) : Foo :=
     match x with
     | mkFoo xs => negb (isEmpty xs) && forallb wfFoo xs
     end.
   

   然后，您可以表明您关心的 Foo 上的所有函数都尊重 wfFoo。还可以使用子集类型将 Foo 的成员与 wfFoo 的证明打包在一起，保证 Foo 的客户端永远不必碰坏 -形成的元素。由于 wfFoo 被定义为 bool 属性，因此等式 wfFoo x = true 是证明无关的，这保证了类型 { x : Foo | wfFoo x = true } 表现良好。 Mathematical Components library为此类 build 提供了良好的支撑。