Stream: Coq users

Topic: Simplifying CoFixpoints


view this post on Zulip Rudy Peterson (Oct 11 2022 at 20:27):

Hello!

I am new to coninductive data-types and I have been trying to prove a seemingly trivial fact about streams but I get stuck:

CoInductive stream := Stream : nat -> stream -> stream.

CoFixpoint stream_map (f : nat -> nat) (s : stream)
  : stream :=
  match s with
  | Stream n s => Stream (f n) (stream_map f s)
  end.

CoInductive stream_eq : stream -> stream -> Prop :=
| Stream_eq n s1 s2 :
  stream_eq s1 s2 ->
  stream_eq (Stream n s1) (Stream n s2).

Lemma stream_map_id : forall s,
    stream_eq (stream_map (fun x => x) s) s.
Proof.
  cofix C.
  intros [n s].
  compute.
Abort.

When I try to prove stream_map_id I want stream_map (fun x => x) (Stream n s) to simplify to Stream n (stream_map (fun x => x) s) but I am not sure how to do that.

Thank you!

view this post on Zulip Pierre-Marie Pédrot (Oct 11 2022 at 20:33):

You're hitting right into an issue with positive coinductive types. The way you phrased stream_eq forces you to perform an eta-expansion, which is provable for positive streams but very unwieldy

view this post on Zulip Pierre-Marie Pédrot (Oct 11 2022 at 20:34):

here is the proof:

Lemma stream_eta : forall s : stream,
  s = Stream (match s with Stream n s => n end) (match s with Stream n s => s end).
Proof.
intros s.
destruct s; reflexivity.
Qed.

Lemma stream_map_id : forall s,
    stream_eq (stream_map (fun x => x) s) s.
Proof.
  cofix C.
  intros [n s].
  match goal with [ |- stream_eq ?s _ ] => rewrite (stream_eta s) end.
  simpl.
  constructor.
  apply C.
Qed.

view this post on Zulip Pierre-Marie Pédrot (Oct 11 2022 at 20:36):

A more natural definition is to perform the eta-expansion directly in the stream_eq definition like this:

CoInductive stream := Stream : nat -> stream -> stream.

CoFixpoint stream_map (f : nat -> nat) (s : stream)
  : stream :=
  match s with
  | Stream n s => Stream (f n) (stream_map f s)
  end.

Definition hd s := match s with Stream n _ => n end.
Definition tl s := match s with Stream _ s => s end.

CoInductive stream_eq : stream -> stream -> Prop :=
| Stream_eq s1 s2 : hd s1 = hd s2 -> stream_eq (tl s1) (tl s2) -> stream_eq s1 s2.

Lemma stream_map_id : forall s,
    stream_eq (stream_map (fun x => x) s) s.
Proof.
  cofix C.
  intros [n s].
  constructor; simpl.
  + reflexivity.
  + apply C.
Qed.

view this post on Zulip Pierre-Marie Pédrot (Oct 11 2022 at 20:37):

As a general rule of thumb, you should never write equalities (or indexed inductive types) over streams, because you'll face hard to prove statements, or even outright unprovable.

view this post on Zulip Rudy Peterson (Oct 12 2022 at 00:29):

Thanks this is super helpful!
Is there a good alternative to writing equalities or inductive types over streams?
Thanks again.

view this post on Zulip Karl Palmskog (Oct 12 2022 at 06:53):

there are two general approaches to using coinductive types which affects equality, see answer here: https://proofassistants.stackexchange.com/questions/583/what-is-the-state-of-coinductive-types-and-reasoning-in-coq

view this post on Zulip Pierre Castéran (Oct 12 2022 at 08:09):

Is the approach using primitive projections also suitable for types like "finite or infinite lists" ?

view this post on Zulip Pierre-Marie Pédrot (Oct 12 2022 at 08:11):

You'll have to use a nested type, but yes.

view this post on Zulip Pierre-Marie Pédrot (Oct 12 2022 at 08:11):

like this

CoInductive colist (A : Type) := { node : option (A * colist A) }.

view this post on Zulip Meven Lennon-Bertrand (Oct 12 2022 at 09:19):

If you do not want to encode the functor "by hand" using sums and products, you can also do the following, which might be slightly nicer, as it lets you still use pattern-matching:

Variant list_fun (A : Type) (X : Type) :=
  | nil : list_fun A X
  | cons : A -> X -> list_fun A X.

Arguments cons {_ _}.
Arguments nil {_ _}.

CoInductive colist (A : Type) :=
  { node : list_fun A (colist A) }.

CoFixpoint ones : colist nat :=
  {| node := cons 1 ones |}.

Arguments node {_}.

Definition head {A : Type} (l : colist A) : option A :=
  match l.(node) with
    | nil => None
    | cons a _ => Some a
  end.

view this post on Zulip Pierre Castéran (Oct 12 2022 at 16:34):

Ups, I didn't find the negative equivalent of the definition (from the old tutorial) yet

CoInductive Infinite (A:Type) : colist A ->  Prop :=
    Lcons_inf : forall a l, Infinite A l -> Infinite A (LCons a l).

view this post on Zulip Karl Palmskog (Oct 12 2022 at 16:50):

@Pierre Castéran see example by Li-yao here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Where.20to.20learn.20about.20co.20induction/near/273537431

It gives a general recipe to convert positive coind types to negative ones.

view this post on Zulip Karl Palmskog (Oct 12 2022 at 16:53):

a blogpost with some more examples (of coind negative style): https://blog.poisson.chat/posts/2021-10-26-proving-lists-infinite.html

view this post on Zulip Karl Palmskog (Oct 12 2022 at 16:56):

my view: the usual way of writing the neg coind types is not at all user-friendly, we need ways to "compile" the usual equational-style coind definitions to the negative style


Last updated: Feb 06 2023 at 12:04 UTC