The Coq mailing list

[Hans Jacob Fehrmann Rojas <hans.jfehrmann AT gmail.com>]

Hi William,

I'm not an expert but a very sutil interpretation of the rules seems that the nested positive condition should be applied only considering the arity of the inductives without the parameters as if the `List (Rose A)` would be a new inductive.

So for your example:

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

Should check the positivity condition with respect to (assuming is a valid declaration)

Inductive ListRose : Set :=
| nil : ListRose
| cons : Rose A -> ListRose -> ListRose.

 

This is the argument in Certified Programming with Dependent Types (3.8 Nested Inductive Types)

Also, it seems that the check of the positive condition for an inductive definition is done in coq sources in checker/indtype.ml, specifically the function `check_positivity` and it seems that the parameters are not taking in consideration when checking the positivity condition, so the arguments of Chlipala seems right

Hope these helps

Best,

Hans.

On Tue, Aug 6, 2019 at 11:00 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