The 4th rule of the strict positivity does not make sense to me So I have a short example where intuitively it does not work even though it should:

So here is the example which coq accepts:

```
Inductive seq (T: Type) : Type :=
| nil : seq T
| cons: T -> seq T -> seq T.
Inductive False.
Inductive bar : Type :=
| base : (False -> seq bar) -> bar.
```

Now I am going to follow the rules here:

image.png

I will refer to constructors by the type signature so when the rule says: `const`

will be said to satisfy the positivity condition for a `seq`

I will just say `seq |+> T -> seq T -> seq T`

. Also `|+>`

will mean positivity, while `|++>`

will mean strict positivity, and `||+>>`

for nested positivity.

So Here I will start to show that `base`

satisfies positivity with respect to `bar`

:

`bar |+> (False -> seq bar) -> bar`

using 2nd rule of positivity

`bar |+> bar`

(discharged by 1st rule of positivity) `/\`

`bar |++> False -> seq bar`

using 3rd rule of strict positivity

bar does not occur in `False`

(trivial) `/\`

`bar |++> seq bar`

`bar |++> seq bar`

is the problem for me. So requires the nested positivity rule, So lets start by the second constructor `cons: T -> seq T -> seq T`

The goal is to prove `bar ||+>> bar -> seq bar -> seq bar`

by second rule of nested pos.

`bar |++> bar`

(trivial) and `bar ||+>> seq bar -> seq bar`

by applying second rule of nested positivity again we get

`bar |++> seq bar`

and `bar ||+>> seq bar`

note the first obligation was the first one which just called out at the problematic one, so we can go again forever,

So how would the positivity check algorithm handle this case ?

I think when it does "the instantiated constructors of I" it also instantiates `I p1 .. pm`

with a fresh variable

so it looks at `bar ||+>> bar -> SEQBAR -> SEQBAR`

where SEQBAR is a variable

the first condition of nested positivity "T = I ... and X doesn't appear in the indices" becomes "T = the fresh variable applied to stuff and X doesn't appear in its arguments (which used to be indices)"

also non recursively uniform parameters count as indices for positivity

I am slightly confused, in `bar ||+>> bar -> SEQBAR -> SEQBAR`

, shouldn't it be thatonly the second rule of nested positivity applied ? because it is `forall x:A, B`

Also, I am not sure I understand the mechanics of renaming variables here, so more formally (I will abuse `bar`

as the inductive type and its name as well, but I am literally implementing all that so the distinction is clear )I have

```
bar ||+>> (pi 0 (pi (seq 1) (seq 2))).[bar]
```

This is the instantiation of `cons`

constructor with `bar`

as the type `T`

in `seq T`

, numbers here are for debruijn.

That should simplify according to debruijn rules to

```
bar ||+>> pi bar (pi (seq bar) (seq bar))
```

How could you replace `seq bar `

with a variable ?

I mean the doc is incorrect / incomplete, it's missing a step which replaces `seq bar`

with a variable

I can fix it, but can you point me to where i can find correct positivity check requirements ?

Maybe another way to think about it is that the definition is coinductive, so it's fine to circle back.

which definition are we talking about here ?

The definition of the positivity condition

but how would that help constructing the positivity check algorithm? my knowledge with co-inductive types is limited

When you see `bar |++> seq bar`

for the first time you remember it, when you see it again you just accept it.

I like the idea but I am not sure how to realize it in coq:

This is my implementation for `|++>`

and `||+>>`

, code is not complete because it will not be huge (debruijn stuff + ast + lots of not necessary thing for the purpose of this question).

```
CoInductive StrictPositivity: InductiveType -> Term -> Prop :=
| StrictPositivity_free I t:
~ PIn (induct_name I) (collect_induct t) ->
I |++> t
| StrictPositivity_base I t inds:
(induct (induct_name I), inds) = split_base_args t ->
~ PIn (induct_name I) (flatten (map collect_induct inds)) ->
I |++> t
| StrictPositivity_pi I A B:
~ PIn (induct_name I) (collect_induct A) ->
I |++> B ->
I |++> pi A B
| StrictPositivity_nested t I I' inds:
(induct (induct_name I'), inds) = split_base_args t ->
~PIn (induct_name I) (flatten (map collect_induct (drop (induct_n I') inds))) ->
(* same as seq_forall (fun c => I' ||+>> ClosedIndCtorType c) (induct_constrs I) -> *)
(* but the seq_forall version makes the positivity checker unhappy :( how irocnic *)
(forall c, PIn c (induct_constrs I') -> I ||+>> (ClosedIndCtorType c).[params_to_subst inds (induct_n I')]) ->
I |++> t
where " I '|++>' t" := (StrictPositivity I t)
with NestedPositivity: InductiveType -> Term -> Prop :=
| NestedPositivity_base t I I' inds:
(induct (induct_name I'), inds) = split_base_args t ->
~ PIn (induct_name I) (flatten (map collect_induct (drop (induct_n I') inds))) ->
I ||+>> t
| NestedPositivity_pi I A B:
I |++> A ->
I ||+>> B ->
I ||+>> pi A B
where " I '||+>>' t" := (NestedPositivity I t).
```

I am not sure what should be doing when I see `bar |++> seq bar`

for the first time in coq so that it remembers it for the second time ?

What I do is `apply StrictPositivity_nested`

which will eventually gives `bar ||+>> pi bar (pi (appl seq bar) (appl seq bar))`

I do a `apply: NestedPositivity_pi`

which gives easy to solve `bar |++> bar`

and `bar ||+>> pi (appl seq bar) (appl seq bar)`

If I do `apply: NestedPositivity_pi`

again I will get the original `bar |++> seq bar`

and coq cannot remember that it saw this type before because it is a coinduction.

it's not coinductive, you just ignore the parameters of the nested inductive when checking nested positivity

to make sure I understand what you mean, I just **do not** substitute `bar`

for T in `T -> seq T -> seq T`

, right? I just leave it as an open term.

this is the code https://github.com/coq/coq/blob/9857c851d6010d46b167dc4e5a2fa5de6d898f7d/kernel/indtypes.ml#L264

the `abstract_mind_lc`

replaces the inductive applied to parameters with a variable

then it checks positivity `check_constructors`

with `head = false`

meaning instead of "`T = I params indices`

with X not appearing in indices" it wants "`T = Foo args`

with X not appearing in args" (because the nested inductive already had positivity checked, Foo is guaranteed to be the variable which replaced it)

well this is a follow up coq/ocaml question because I don't know much ocaml if at all, but usually I learn alot by running C/C++ code in debugger and see how functions work together, is there a quick and easy way to run coq itself in the ocaml equivalent of gdb so that I can have better understanding of the types an interactions happening inside `check_positivity_nested`

?

I believe https://github.com/coq/coq/wiki/OCamldebug is up to date

please report any inaccuracies or issues encountered

Last updated: Jun 18 2024 at 22:01 UTC