The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Obviously not part of the CIC spec, but you might want to try Andreas Abel's thesis work "Termination Checking with Types", which describes a type system for handling these types of positivity constraints (and more complicated ones!). You can ignore the size types for now, though one might argue that they lead to a more robust termination analysis in any case.

The big missing component from this work is the dependent indices, but in a first approximation these can be erased.

Best,

Cody

On Tue, Aug 6, 2019 at 11:01 PM William J. Bowman <wjb AT williamjbowman.com> wrote:

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