The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

I just finished implementing the CIC positivity checker as specified in the 
Coq
docs, but the docs seem under specified about how the strict positivity
algorithm should work.

  https://coq.inria.fr/doc/language/cic.html#positivity-condition

If I try to implement the rules as specified, I get stuck in an infinite loop
when checking nested inductive types.

Consider rose trees:

Inductive List (A : Set) : Set :=
| nil : List A
| cons : A -> List A -> List A.

Inductive Rose (A : Set) : Set :=
| rose : (List (Rose A)) -> Rose A.

I must show `Rose` occurs strictly positively in `(List (Rose A))`, from the
type of the constructor `rose`.

Loop:
To show that `Rose` occurs strictly positively in `List (Rose A)`,
since `List (Rose A)` is of the form `(I p_0 ... p_m u ...)` and `List` is not
mutually inductive, we must show the nested positivity condition for each
constructor of `List` after instantiating the types of the constructors with 
the
parameter `(Rose A)`.

There are two cases:
- nil : `(List (Rose A))` satisfies nested positivity w.r.t. `Rose` trivially.

- cons : `Rose A -> List (Rose A) -> List (Rose A)`
To show this satisfies nested positivity w.r.t. `Rose`, we must show that 
`Rose`
occurs strictly positively in `List (Rose A)`.
goto Loop


For now, I've "fixed" this by allowing myself to assume strict positivity 
holds
for `List (Rose A)` while checking nested positivity.
This seems okay, in a vague, intuitive, "something something greatest
fixpoints?" kind of way, but I'd like to be a little more formal than that.

Does anyone know what's missing from the Coq docs or what reference I should
look at?

I usually start from the Coq docs as they have the most readable and complete
CIC spec in one place.
I tried reading the Coq kernel code but.. failed.
I also tried Paulin-Mohring's "Inductive Definitions in the system Coq Rules 
and
Properties", but can't find anything about nested inductive types.

--
William J. Bowman