Stream: Coq users

Topic: Non strictly positive occurrence for nested types


view this post on Zulip Jules Viennot (Apr 25 2024 at 11:12):

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 ?

view this post on Zulip Li-yao (Apr 25 2024 at 11:28):

If you let J a := a -> bool then you will find a recursive negative occurrence of M.

view this post on Zulip Jules Viennot (Apr 25 2024 at 12:21):

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

view this post on Zulip Li-yao (Apr 25 2024 at 12:29):

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

view this post on Zulip Li-yao (Apr 25 2024 at 12:33):

In this case you're just building a stack of Ms 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.

view this post on Zulip Li-yao (Apr 25 2024 at 12:34):

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


Last updated: Jun 23 2024 at 04:03 UTC