Stream: Coq devs & plugin devs

Topic: Positivity checker and constructors


view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 01 2022 at 09:31):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 01 2022 at 09:34):

Hmm, nope same issue.

view this post on Zulip Gaëtan Gilbert (Jun 01 2022 at 09:37):

this looks inductive-inductive ish

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Jun 02 2022 at 08:37):

the problem is that @None foo appears in an index

view this post on Zulip 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: Dec 01 2023 at 07:01 UTC