understanding strict/nested Positivity · Coq users

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:

Inductive seq (T: Type) : Type :=
| nil : seq T
| cons: T -> seq T -> seq T.

Inductive False.

Inductive bar : Type :=
| base : (False -> seq bar) -> bar.

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 barby 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,

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

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

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

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

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 ?

Stream: Coq users

Topic: understanding strict/nested Positivity

walker (Apr 27 2023 at 14:52):