Hello, I want to verify some OCaml piece of code that doesn't require to check for strict positivity in types definition.

The code I want to write look something like this :

```
Parameter J : Type -> Type.
Inductive K (a : Type) : Type -> Type :=
| Kc {b : Type} : J a -> K (M a) b -> J a -> K a b
with L (a : Type) : Type :=
| Lc {b : Type} : K a b -> L b -> L a
with M (a : Type) : Type :=
| Mc : J a -> L (M a) -> M a.
```

But it returns the error : 'Non strictly positive occurrence of "M" in "forall b : Type, J a -> K (M a) b -> J a -> K a b".'

I can't wrap my head around this problem, is it really a non-strictly positive occurrence of M, and in this case, how do we prove that implementing it leads to inconsistency ?

Otherwise, is there a way to work around this issue ?

If you let `J a := a -> bool`

then you will find a recursive negative occurrence of `M`

.

And if J is an inductive type of the form `Inductive J (A : Type) : Type := Jc : A -> J A. `

?

I guess that would be fine but then you need a way smarter condition than "strict positivity" (and find someone to implement it)

In this case you're just building a stack of `M`

s so you can encode this type with a `nat`

parameter to avoid the recursion in parameters

```
(* iter : nat -> (A -> A) -> A -> A somewhere in the stdlib *)
Inductive Kn (n : nat) (a : Type) (b : Type) : Type := Kc : J (iter n M a) -> Kn (S n) -> J (iter n M a) -> K a b
...
Definition K := Kn 0.
```

Ah, nvm, since M is also defined mutually recursively that's still too naive...

Last updated: Jun 23 2024 at 04:03 UTC