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: Oct 13 2024 at 01:02 UTC