Stream: Coq devs & plugin devs

Topic: Positivity checker and constructors

Jason Gross (May 31 2022 at 22:01):

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)

Jason Gross (May 31 2022 at 22:21):

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

Pierre-Marie Pédrot (Jun 01 2022 at 09:30):

Interesting limitation. The first one succeeds because t1 is a parameter in the equality type.

Pierre-Marie Pédrot (Jun 01 2022 at 09:31):

You can probably hack this by hardwiring a "isNone" inductive type there.

Pierre-Marie Pédrot (Jun 01 2022 at 09:34):

Hmm, nope same issue.

Gaëtan Gilbert (Jun 01 2022 at 09:37):

this looks inductive-inductive ish

Jason Gross (Jun 01 2022 at 13:38):

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

Ali Caglayan (Jun 01 2022 at 13:43):

cc @Yannick Forster @Matthieu Sozeau who were thinking about termination checkers in Metacoq. What do you think?

Yannick Forster (Jun 01 2022 at 13:45):

I'm cc-ing my cc to @Lennard Gäher who implemented the (unmerged) termination checker for MetaCoq

Paolo Giarrusso (Jun 01 2022 at 14:00):

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)

Jason Gross (Jun 01 2022 at 22:55):

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

Gaëtan Gilbert (Jun 02 2022 at 08:37):

the problem is that @None foo appears in an index

Jason Gross (Jun 03 2022 at 04:19):

@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