49 lines
1.1 KiB
Coq
49 lines
1.1 KiB
Coq
Require Import Streams.
|
|
|
|
CoInductive stream_eq {A:Type} : Stream A -> Stream A -> Prop :=
|
|
| Stream_eq : forall (h:A) (tl1 tl2:Stream A),
|
|
stream_eq tl1 tl2 -> stream_eq (Cons h tl1) (Cons h tl2).
|
|
|
|
CoFixpoint zeros : Stream nat := Cons 0 zeros.
|
|
CoFixpoint ones : Stream nat := Cons 1 ones.
|
|
Definition ones' := map S zeros.
|
|
|
|
Definition sUnfold {A:Type} (s:Stream A) : Stream A :=
|
|
match s with
|
|
| Cons x xs => Cons x xs
|
|
end.
|
|
|
|
|
|
(* From Pierre Castéran *)
|
|
Lemma stm_unfold {A: Type} (s: Stream A) :
|
|
s = match s with Cons a s' => Cons a s' end.
|
|
Proof.
|
|
now destruct s.
|
|
Qed.
|
|
|
|
Inductive starts_with {A: Type} (a:A): Stream A -> Prop :=
|
|
starts_hd : forall s, starts_with a (Cons a s).
|
|
|
|
Goal Streams.Exists (starts_with 3) (const 3).
|
|
left; rewrite (stm_unfold (const 3)); split.
|
|
Qed.
|
|
|
|
Goal Streams.Exists (starts_with 3) (Cons 4 (const 3)).
|
|
right; left.
|
|
rewrite (stm_unfold (const 3)).
|
|
split.
|
|
Qed.
|
|
|
|
|
|
(*
|
|
By the way, here's an infinite list
|
|
|
|
This is like `foo = 3 : foo` in Haskell.
|
|
*)
|
|
CoFixpoint incStream (n:nat):Stream nat :=
|
|
Cons n (incStream (S n)).
|
|
|
|
|
|
Compute Streams.hd (Streams.tl (incStream 1)).
|
|
|