Kenji Maillard (Jul 19 2021 at 09:12): Kenji Maillard (Jul 19 2021 at 09:12):I stumbled on a strict positivity failure in Coq that I don't understand with (negative) coinductive types. I am trying to define streams parametrized by conatural numbers (potentially infinite numbers) maintaining the "length" of the stream (so that we can't extract the head of a stream parametrized by 0):
Set Primitive Projections.
(* CoNatural numbers *)
CoInductive natω :=
{ top : unit + natω }.
(* Zero and Successor function on conatural numbers; not necessary for the following def*)
Definition zω : natω := {| top := inl tt |}.
Definition sω : natω -> natω :=
fun k => {| top := inr k |}.
Set Printing All.
Fail CoInductive Pstr2 (A : Type) (n : natω) : Type :=
{ hd2 : match n.(top) return Type with
| inl _ => False
| inr k => A
end ;
tl2 : match n.(top) return Type with
| inl _ => False
| inr k => Pstr2 A k
end
}.
(*
The command has indeed failed with message:
Non strictly positive occurrence of "Pstr2" in
"forall (_ : match top n return Type with
| inl _ => False
| inr _ => A
end)
(_ : match top n return Type with
| inl _ => False
| inr k => Pstr2 A k
end), Pstr2 A n".
*)
I don't understand what's supposed to fail: the error message seems to be showing the type of a constructor for the type I want to define, but I was expecting strict positivity to be checked on the observations hd2 and tl2...
Just to check, I tried the non-parametrized variant, and another variant using functions types (that should be extensionally equivalent) and they both go through.
(* Non-parametrized variant (sanity check) *)
CoInductive Pstr (A : Type) : Type :=
{ hd : A ;
tl : Pstr A
}.
Inductive empty : Type :=.
Definition is_suc (n : natω) : Type :=
match n.(top) with | inl _ => empty | inr _ => unit end.
Definition pred (n : natω) :=
match n.(top) with
| inl _ => zω
| inr k => k
end.
(* Variant with function types *)
CoInductive Pstr' (A : Type) (n : natω) : Type :=
{
hd' : is_suc n -> A ;
tl' : is_suc n -> Pstr' A (pred n)
}.
Positivity doesn't go through pattern matchings.
Pierre-Marie Pédrot (Jul 19 2021 at 09:15):https://github.com/coq/coq/issues/1433
Pierre-Marie Pédrot (Jul 19 2021 at 09:16):As hinted in the bug report you can encode it with nested inductive types though.
Kenji Maillard (Jul 19 2021 at 09:43):It works better indeed:
Inductive sum_dispatch {A B} DA DB : A + B -> Type :=
| dispatch_inl : forall a : A, DA a -> sum_dispatch DA DB (inl a)
| dispatch_inr : forall b : B, DB b -> sum_dispatch DA DB (inr b).
Definition on_inr {A B} DB :=
@sum_dispatch A B (fun _ => False) DB.
CoInductive Pstr2 (A : Type) (n : natω) : Type :=
{ hd2 : on_inr (fun _ => A) n.(top) ;
tl2 : on_inr (Pstr2 A) n.(top)
}.
Thanks for the pointer and explanation
Last updated: Oct 13 2024 at 01:02 UTC