Stream: Coq users

Topic: Unexpected failure of strict positivity in a coinductive


view this post on Zulip 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  : natω := {| top := inl tt |}.
Definition  : 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 _ => 
  | 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)
  }.

view this post on Zulip Pierre-Marie Pédrot (Jul 19 2021 at 09:14):

Positivity doesn't go through pattern matchings.

view this post on Zulip Pierre-Marie Pédrot (Jul 19 2021 at 09:15):

https://github.com/coq/coq/issues/1433

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

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC