From 8685e8ad7e56052f6aeec8c4a2c984fff10f2256 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 23 May 2015 14:32:52 -0700
Subject: [PATCH] feat(library/data/stream): define corec for infinite streams

---
 library/data/stream.lean | 61 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 59 insertions(+), 2 deletions(-)

diff --git a/library/data/stream.lean b/library/data/stream.lean
index 337800b8bc..6b6710359a 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -3,8 +3,8 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import data.nat
-open nat
+import data.nat algebra.function
+open nat function
 
 definition stream (A : Type) := nat → A
 
@@ -33,12 +33,21 @@ s n
 protected theorem eta (s : stream A) : cons (head s) (tail s) = s :=
 funext (λ i, begin cases i, repeat reflexivity end)
 
+theorem head_cons (a : A) (s : stream A) : head (cons a s) = a :=
+rfl
+
+theorem tail_cons (a : A) (s : stream A) : tail (cons a s) = s :=
+rfl
+
 theorem tail_nth_tail (n : nat) (s : stream A) : tail (nth_tail n s) = nth_tail n (tail s) :=
 funext (λ i, begin esimp [tail, nth_tail], congruence, rewrite add.right_comm end)
 
 theorem nth_nth_tail (n m : nat) (s : stream A) : nth n (nth_tail m s) = nth (n+m) s :=
 rfl
 
+theorem tail_eq_nth_tail (s : stream A) : tail s = nth_tail 1 s :=
+rfl
+
 theorem nth_tail_nth_tail (n m : nat) (s : stream A) : nth_tail n (nth_tail m s) = nth_tail (n+m) s :=
 funext (λ i, begin esimp [nth_tail], rewrite add.assoc end)
 
@@ -69,6 +78,9 @@ stream.ext (λ i, rfl)
 
 theorem nth_map (n : nat) (s : stream A) : nth n (map f s) = f (nth n s) :=
 rfl
+
+theorem tail_map (s : stream A) : tail (map f s) = map f (tail s) :=
+begin rewrite tail_eq_nth_tail end
 end map
 
 section zip
@@ -87,6 +99,12 @@ end zip
 definition repeat (a : A) : stream A :=
 λ n, a
 
+theorem repeat_eq (a : A) : repeat a = cons a (repeat a) :=
+begin
+  apply stream.ext, intro n,
+  cases n, repeat reflexivity
+end
+
 theorem nth_repeat (n : nat) (a : A) : nth n (repeat a) = a :=
 rfl
 
@@ -109,6 +127,11 @@ begin
      esimp at *, rewrite IH}
 end
 
+theorem iterate_eq (f : A → A) (a : A) : iterate f a = cons a (iterate f (f a)) :=
+begin
+  rewrite [-stream.eta], congruence, exact !tail_iterate
+end
+
 theorem nth_zero_iterate (f : A → A) (a : A) : nth 0 (iterate f a) = a :=
 rfl
 
@@ -139,4 +162,38 @@ section bisim
   theorem eq_of_bisim  : ∀ {s₁ s₂}, s₁ ~ s₂ → s₁ = s₂ :=
   λ s₁ s₂ r, stream.ext (λ n, and.elim_left (nth_of_bisim bisim n r))
 end bisim
+
+section corec
+  definition corec (f : A → B) (g : A → A) : A → stream B :=
+  λ a, map f (iterate g a)
+
+  theorem corec_def (f : A → B) (g : A → A) (a : A) : corec f g a = map f (iterate g a) :=
+  rfl
+
+  theorem corec_eq (f : A → B) (g : A → A) (a : A) : corec f g a = cons (f a) (corec f g (g a)) :=
+  begin
+    apply stream.ext, intro n,
+    cases n,
+      {reflexivity},
+      {esimp [corec] at *,
+       rewrite [*nth_succ, tail_cons, tail_map, tail_iterate]}
+  end
+
+  theorem corec_id_id_eq_repeat (a : A) : corec id id a = repeat a :=
+  begin
+    apply stream.ext, intro n,
+    induction n with n' ih,
+      {reflexivity},
+      {rewrite [corec_eq, repeat_eq, *nth_succ, *tail_cons], esimp,
+       exact ih}
+  end
+
+  theorem corec_id_f_eq_iterate (f : A → A) (a : A) : corec id f a = iterate f a :=
+  begin
+    apply stream.ext, intro n,
+    cases n,
+      {reflexivity},
+      {rewrite [corec_eq, *nth_succ, tail_iterate]}
+  end
+end corec
 end stream