Rudy Peterson (Oct 11 2022 at 20:27): 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!
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
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.
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.
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.
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.
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
Pierre Castéran (Oct 12 2022 at 08:09):Is the approach using primitive projections also suitable for types like "finite or infinite lists" ?
Pierre-Marie Pédrot (Oct 12 2022 at 08:11):You'll have to use a nested type, but yes.
Pierre-Marie Pédrot (Oct 12 2022 at 08:11):like this
CoInductive colist (A : Type) := { node : option (A * colist A) }.
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.
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).
@Pierre Castéran see example by Li-yao here
It gives a general recipe to convert positive coind types to negative ones.
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
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: Oct 13 2024 at 01:02 UTC