## Stream: Coq users

### Topic: understanding strict/nested Positivity

#### walker (Apr 27 2023 at 14:52):

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 ?

#### Gaëtan Gilbert (Apr 27 2023 at 15:25):

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)"

#### Gaëtan Gilbert (Apr 27 2023 at 15:28):

also non recursively uniform parameters count as indices for positivity

#### walker (Apr 27 2023 at 16:03):

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`

#### walker (Apr 27 2023 at 16:06):

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 ?

#### Gaëtan Gilbert (Apr 27 2023 at 16:15):

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

#### walker (Apr 27 2023 at 16:23):

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

#### Li-yao (Apr 27 2023 at 19:54):

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

#### walker (Apr 27 2023 at 20:00):

which definition are we talking about here ?

#### Li-yao (Apr 27 2023 at 20:14):

The definition of the positivity condition

#### walker (Apr 27 2023 at 20:36):

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

#### Li-yao (Apr 27 2023 at 23:27):

When you see `bar |++> seq bar` for the first time you remember it, when you see it again you just accept it.

#### walker (Apr 28 2023 at 09:09):

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 ?

#### walker (Apr 28 2023 at 09:17):

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.

#### Gaëtan Gilbert (Apr 28 2023 at 09:18):

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

#### walker (Apr 28 2023 at 09:20):

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.

#### Gaëtan Gilbert (Apr 28 2023 at 09:31):

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)

#### walker (Apr 28 2023 at 11:03):

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` ?

#### Gaëtan Gilbert (Apr 28 2023 at 11:27):

I believe https://github.com/coq/coq/wiki/OCamldebug is up to date
please report any inaccuracies or issues encountered

Last updated: Oct 04 2023 at 23:01 UTC