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:
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 |+> (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
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,
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
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
||+>>, 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
abstract_mind_lc replaces the inductive applied to parameters with a variable
then it checks positivity
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
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