Why does the positivity checker consider constructor arguments to be non-positive occurrences? Is there any way to make something like this work?
Inductive t1 := q1 (v : option t1) (pf : v = v). Inductive t2 := q2 (v : option t2) (pf : v = None). (* Error: Non strictly positive occurrence of "t2" in "forall v : option t2, v = None -> t2". *)
(See https://github.com/coq/coq/issues/16120 for a slightly more realistic example)
(The context for this is that I'm trying to write a general trie data structure satisfying the FMap interface and then instantiate it with various sorts of data, see https://github.com/mit-plv/fiat-crypto/compare/master...JasonGross:fmap-trie?expand=1)
Interesting limitation. The first one succeeds because t1 is a parameter in the equality type.
You can probably hack this by hardwiring a "isNone" inductive type there.
Hmm, nope same issue.
this looks inductive-inductive ish
@Pierre-Marie Pédrot The "isNone" version is what I started with and am actually wanting to make work:
Inductive tree_NonEmpty elt : PositiveMap.t elt -> Prop := | Node_l_NonEmpty l v r : tree_NonEmpty l -> tree_NonEmpty (PositiveMap.Node l v r) | Node_r_NonEmpty l v r : tree_NonEmpty r -> tree_NonEmpty (PositiveMap.Node l v r) | Node_m_NonEmpty l v r : tree_NonEmpty (PositiveMap.Node l (Some v) r).
cc @Yannick Forster @Matthieu Sozeau who were thinking about termination checkers in Metacoq. What do you think?
I'm cc-ing my cc to @Lennard Gäher who implemented the (unmerged) termination checker for MetaCoq
is this the same as https://sympa.inria.fr/sympa/arc/coq-club/2012-05/msg00032.html? Those scenarios are accepted in Agda, but through complex reasoning (https://lists.chalmers.se/pipermail/agda/2012/004026.html)
@Paolo Giarrusso , no, that message is about a generalization of https://github.com/coq/coq/issues/1433, the positivity checker being able to see through
match statements and recursion. This is about the positivity checker considering that, e.g.,
foo occurs in a positive position in
@None foo (and more generally that parameters of inductive types that are positive in the inductive itself should also be positive when passed to constructors of that inductive)
the problem is that
@None foo appears in an index
@Gaëtan Gilbert The issue occurs even when
@None foo appears only in parameters and not in indices:
Inductive t1 := q1 (v : option t1) (pf : v = v). Inductive t2 := q2 (v : option t2) (pf : None = v). (* Error: Non strictly positive occurrence of "t2" in "forall v : option t2, None = v -> t2". *)
Last updated: Jun 04 2023 at 19:30 UTC