From a7e36e48519ab281320c4d192da6a7b348ce40ad Mon Sep 17 00:00:00 2001 From: arienmalec Date: Wed, 29 Mar 2023 02:46:56 +0000 Subject: [PATCH] refactor(data/seq): scope seq and wseq to namespace stream (#18284) Adds namespace `stream` to `seq` and `wseq` to ease the Mathlib4 port (as `Seq` now name clashes with class `Seq` (`has_seq` in Lean 3). This requires disambiguation between `stream` and `computation` where lemmas in each namespace have the same name, and requires explicit scoping to mathlib files that reference `seq` and `wseq` (often by `open stream.seq as seq`) Co-authored-by: Scott Morrison --- docs/overview.yaml | 6 +- src/algebra/continued_fractions/basic.lean | 1 + .../computation/approximations.lean | 4 +- .../computation/basic.lean | 8 +- .../computation/terminates_iff_rat.lean | 1 + .../computation/translations.lean | 3 +- .../convergents_equiv.lean | 1 + .../terminated_stable.lean | 1 + .../continued_fractions/translations.lean | 1 + src/data/seq/parallel.lean | 11 +-- src/data/seq/seq.lean | 24 +++--- src/data/seq/wseq.lean | 74 +++++++++++-------- 12 files changed, 80 insertions(+), 55 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index 1857a175084bf..f5178f64aff7e 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -138,7 +138,7 @@ General algebra: perfection of a ring: 'ring.perfection' Transcendental numbers: Liouville's theorem on existence of transcendental numbers: liouville.is_transcendental - + Representation theory: representation : 'representation' category of finite dimensional representations : 'fdRep' @@ -445,8 +445,8 @@ Data structures: difference list: 'dlist' lazy list: 'lazy_list' stream: 'stream' - sequence: 'seq' - weak sequence: 'wseq' + sequence: 'stream.seq' + weak sequence: 'stream.wseq' Sets: set: 'set' diff --git a/src/algebra/continued_fractions/basic.lean b/src/algebra/continued_fractions/basic.lean index 643a4d8a3a99c..dfb55dd60930f 100644 --- a/src/algebra/continued_fractions/basic.lean +++ b/src/algebra/continued_fractions/basic.lean @@ -47,6 +47,7 @@ variable (α : Type*) protected structure generalized_continued_fraction.pair := (a : α) (b : α) open generalized_continued_fraction +open stream.seq as seq /-! Interlude: define some expected coercions and instances. -/ namespace generalized_continued_fraction.pair diff --git a/src/algebra/continued_fractions/computation/approximations.lean b/src/algebra/continued_fractions/computation/approximations.lean index 99a04f2f26d94..19ca7909b95c2 100644 --- a/src/algebra/continued_fractions/computation/approximations.lean +++ b/src/algebra/continued_fractions/computation/approximations.lean @@ -296,9 +296,9 @@ theorem of_denom_mono : (of v).denominators n ≤ (of v).denominators (n + 1) := begin let g := of v, cases (decidable.em $ g.partial_denominators.terminated_at n) with terminated not_terminated, - { have : g.partial_denominators.nth n = none, by rwa seq.terminated_at at terminated, + { have : g.partial_denominators.nth n = none, by rwa stream.seq.terminated_at at terminated, have : g.terminated_at n, from - terminated_at_iff_part_denom_none.elim_right (by rwa seq.terminated_at at terminated), + terminated_at_iff_part_denom_none.elim_right (by rwa stream.seq.terminated_at at terminated), have : g.denominators (n + 1) = g.denominators n, from denominators_stable_of_terminated n.le_succ this, rw this }, diff --git a/src/algebra/continued_fractions/computation/basic.lean b/src/algebra/continued_fractions/computation/basic.lean index 61ac955115559..eef0b6a89ce59 100644 --- a/src/algebra/continued_fractions/computation/basic.lean +++ b/src/algebra/continued_fractions/computation/basic.lean @@ -131,6 +131,7 @@ protected def stream (v : K) : stream $ option (int_fract_pair K) | (n + 1) := (stream n).bind $ λ ap_n, if ap_n.fr = 0 then none else some (int_fract_pair.of ap_n.fr⁻¹) + /-- Shows that `int_fract_pair.stream` has the sequence property, that is once we return `none` at position `n`, we also return `none` at `n + 1`. @@ -147,10 +148,11 @@ This is just an intermediate representation and users should not (need to) direc it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in `algebra.continued_fractions.computation.translations`. -/ -protected def seq1 (v : K) : seq1 $ int_fract_pair K := +protected def seq1 (v : K) : stream.seq1 $ int_fract_pair K := ⟨ int_fract_pair.of v,--the head - seq.tail -- take the tail of `int_fract_pair.stream` since the first element is already in the - -- head create a sequence from `int_fract_pair.stream` + stream.seq.tail -- take the tail of `int_fract_pair.stream` since the first element is already in + -- the head + -- create a sequence from `int_fract_pair.stream` ⟨ int_fract_pair.stream v, -- the underlying stream @stream_is_seq _ _ _ v ⟩ ⟩ -- the proof that the stream is a sequence diff --git a/src/algebra/continued_fractions/computation/terminates_iff_rat.lean b/src/algebra/continued_fractions/computation/terminates_iff_rat.lean index 53e9232e5047a..d4977bd208740 100644 --- a/src/algebra/continued_fractions/computation/terminates_iff_rat.lean +++ b/src/algebra/continued_fractions/computation/terminates_iff_rat.lean @@ -28,6 +28,7 @@ rational, continued fraction, termination -/ namespace generalized_continued_fraction +open stream.seq as seq open generalized_continued_fraction (of) diff --git a/src/algebra/continued_fractions/computation/translations.lean b/src/algebra/continued_fractions/computation/translations.lean index 3d999f84a89ae..2d7683d10376a 100644 --- a/src/algebra/continued_fractions/computation/translations.lean +++ b/src/algebra/continued_fractions/computation/translations.lean @@ -38,6 +38,7 @@ of three sections: namespace generalized_continued_fraction open generalized_continued_fraction (of) +open stream.seq as seq /- Fix a discrete linear ordered floor field and a value `v`. -/ variables {K : Type*} [linear_ordered_field K] [floor_ring K] {v : K} @@ -193,7 +194,7 @@ option.map_eq_none lemma of_terminated_at_n_iff_succ_nth_int_fract_pair_stream_eq_none : (of v).terminated_at n ↔ int_fract_pair.stream v (n + 1) = none := -by rw [of_terminated_at_iff_int_fract_pair_seq1_terminated_at, seq.terminated_at, +by rw [of_terminated_at_iff_int_fract_pair_seq1_terminated_at, stream.seq.terminated_at, int_fract_pair.nth_seq1_eq_succ_nth_stream] end termination diff --git a/src/algebra/continued_fractions/convergents_equiv.lean b/src/algebra/continued_fractions/convergents_equiv.lean index 244c9e843532a..bc5d40a4f6e8b 100644 --- a/src/algebra/continued_fractions/convergents_equiv.lean +++ b/src/algebra/continued_fractions/convergents_equiv.lean @@ -65,6 +65,7 @@ fractions, recurrence, equivalence variables {K : Type*} {n : ℕ} namespace generalized_continued_fraction +open stream.seq as seq variables {g : generalized_continued_fraction K} {s : seq $ pair K} diff --git a/src/algebra/continued_fractions/terminated_stable.lean b/src/algebra/continued_fractions/terminated_stable.lean index 0bdcae77dd778..097b544df7a02 100644 --- a/src/algebra/continued_fractions/terminated_stable.lean +++ b/src/algebra/continued_fractions/terminated_stable.lean @@ -13,6 +13,7 @@ We show that the continuants and convergents of a gcf stabilise once the gcf ter -/ namespace generalized_continued_fraction +open stream.seq as seq variables {K : Type*} {g : generalized_continued_fraction K} {n m : ℕ} diff --git a/src/algebra/continued_fractions/translations.lean b/src/algebra/continued_fractions/translations.lean index 3a1f74dc5a8dc..dc8bfb1a2c62b 100644 --- a/src/algebra/continued_fractions/translations.lean +++ b/src/algebra/continued_fractions/translations.lean @@ -14,6 +14,7 @@ Some simple translation lemmas between the different definitions of functions de -/ namespace generalized_continued_fraction +open stream.seq as seq section general /-! diff --git a/src/data/seq/parallel.lean b/src/data/seq/parallel.lean index 80f7dfc0832e7..38b38a046354b 100644 --- a/src/data/seq/parallel.lean +++ b/src/data/seq/parallel.lean @@ -14,7 +14,8 @@ import data.seq.wseq universes u v namespace computation -open wseq +open stream.wseq as wseq +open stream.seq as seq variables {α : Type u} {β : Type v} def parallel.aux2 : list (computation α) → α ⊕ list (computation α) := @@ -26,7 +27,7 @@ end) (sum.inr []) def parallel.aux1 : list (computation α) × wseq (computation α) → α ⊕ list (computation α) × wseq (computation α) | (l, S) := rmap (λ l', match seq.destruct S with - | none := (l', nil) + | none := (l', seq.nil) | some (none, S') := (l', S') | some (some c, S') := (c::l', S') end) (parallel.aux2 l) @@ -156,7 +157,7 @@ begin exact ⟨c, or.inl cl, ac⟩ }, { induction e : seq.destruct S with a; rw e at h', { exact let ⟨d, o, ad⟩ := IH _ _ h', - ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (not_mem_nil _), ad⟩ in + ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (wseq.not_mem_nil _), ad⟩ in ⟨c, or.inl cl, ac⟩ }, { cases a with o S', cases o with c; simp [parallel.aux1] at h'; rcases IH _ _ h' with ⟨d, dl | dS', ad⟩, @@ -196,8 +197,8 @@ theorem parallel_empty (S : wseq (computation α)) (h : S.head ~> none) : parallel S = empty _ := eq_empty_of_not_terminates $ λ ⟨⟨a, m⟩⟩, let ⟨c, cs, ac⟩ := exists_of_mem_parallel m, - ⟨n, nm⟩ := exists_nth_of_mem cs, - ⟨c', h'⟩ := head_some_of_nth_some nm in by injection h h' + ⟨n, nm⟩ := wseq.exists_nth_of_mem cs, + ⟨c', h'⟩ := wseq.head_some_of_nth_some nm in by injection h h' -- The reason this isn't trivial from exists_of_mem_parallel is because it eliminates to Sort def parallel_rec {S : wseq (computation α)} (C : α → Sort v) diff --git a/src/data/seq/seq.lean b/src/data/seq/seq.lean index 4571c0c1a4020..182edc11ec884 100644 --- a/src/data/seq/seq.lean +++ b/src/data/seq/seq.lean @@ -9,6 +9,7 @@ import data.nat.basic import data.stream.init import data.seq.computation +namespace stream universes u v w /- @@ -20,7 +21,7 @@ coinductive seq (α : Type u) : Type u /-- A stream `s : option α` is a sequence if `s.nth n = none` implies `s.nth (n + 1) = none`. -/ -def stream.is_seq {α : Type u} (s : stream (option α)) : Prop := +def is_seq {α : Type u} (s : stream (option α)) : Prop := ∀ {n : ℕ}, s n = none → s (n + 1) = none /-- `seq α` is the type of possibly infinite lists (referred here as sequences). @@ -95,6 +96,7 @@ def head (s : seq α) : option α := nth s 0 /-- Get the tail of a sequence (or `nil` if the sequence is `nil`) -/ def tail (s : seq α) : seq α := ⟨s.1.tail, λ n, by { cases s with f al, exact al }⟩ +/-- member definition for `seq`-/ protected def mem (a : α) (s : seq α) := some a ∈ s.1 instance : has_mem α (seq α) := @@ -209,6 +211,7 @@ begin apply h1 _ _ (or.inr (IH e)) } end +/-- Corecursor over pairs of `option` values-/ def corec.F (f : β → option (α × β)) : option β → option α × option β | none := (none, none) | (some b) := match f b with none := (none, none) | some (a, b') := (some a, some b') end @@ -252,12 +255,14 @@ section bisim local infix (name := R) ` ~ `:50 := R + /-- Bisimilarity relation over `option` of `seq1 α`-/ def bisim_o : option (seq1 α) → option (seq1 α) → Prop | none none := true | (some (a, s)) (some (a', s')) := a = a' ∧ R s s' | _ _ := false attribute [simp] bisim_o + /-- a relation is bisimiar if it meets the `bisim_o` test-/ def is_bisimulation := ∀ ⦃s₁ s₂⦄, s₁ ~ s₂ → bisim_o R (destruct s₁) (destruct s₂) -- If two streams are bisimilar, then they are equal @@ -667,11 +672,11 @@ end seq namespace seq1 variables {α : Type u} {β : Type v} {γ : Type w} -open seq +open stream.seq /-- Convert a `seq1` to a sequence. -/ def to_seq : seq1 α → seq α -| (a, s) := cons a s +| (a, s) := seq.cons a s instance coe_seq : has_coe (seq1 α) (seq α) := ⟨to_seq⟩ @@ -685,13 +690,13 @@ theorem map_id : ∀ (s : seq1 α), map id s = s | ⟨a, s⟩ := by simp [map] def join : seq1 (seq1 α) → seq1 α | ((a, s), S) := match destruct s with | none := (a, seq.join S) - | some s' := (a, seq.join (cons s' S)) + | some s' := (a, seq.join (seq.cons s' S)) end @[simp] theorem join_nil (a : α) (S) : join ((a, nil), S) = (a, seq.join S) := rfl @[simp] theorem join_cons (a b : α) (s S) : - join ((a, cons b s), S) = (a, seq.join (cons (b, s) S)) := + join ((a, seq.cons b s), S) = (a, seq.join (seq.cons (b, s) S)) := by dsimp [join]; rw [destruct_cons]; refl /-- The `return` operator for the `seq1` monad, @@ -726,8 +731,8 @@ end @[simp] theorem map_join' (f : α → β) (S) : seq.map f (seq.join S) = seq.join (seq.map (map f) S) := begin - apply eq_of_bisim (λ s1 s2, - ∃ s S, s1 = append s (seq.map f (seq.join S)) ∧ + apply seq.eq_of_bisim (λ s1 s2, + ∃ s S, s1 = seq.append s (seq.map f (seq.join S)) ∧ s2 = append s (seq.join (seq.map (map f) S))), { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, rfl, rfl⟩ := begin apply rec_on s; simp, @@ -745,7 +750,7 @@ end @[simp] theorem join_join (SS : seq (seq1 (seq1 α))) : seq.join (seq.join SS) = seq.join (seq.map join SS) := begin - apply eq_of_bisim (λ s1 s2, + apply seq.eq_of_bisim (λ s1 s2, ∃ s SS, s1 = seq.append s (seq.join (seq.join SS)) ∧ s2 = seq.append s (seq.join (seq.map join SS))), { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, SS, rfl, rfl⟩ := begin @@ -755,7 +760,7 @@ begin apply rec_on s; simp, { exact ⟨_, _, rfl, rfl⟩ }, { intros x s, - refine ⟨cons x (append s (seq.join S)), SS, _, _⟩; simp } } }, + refine ⟨seq.cons x (append s (seq.join S)), SS, _, _⟩; simp } } }, { intros x s, exact ⟨s, SS, rfl, rfl⟩ } end end }, { refine ⟨nil, SS, _, _⟩; simp } @@ -788,3 +793,4 @@ instance : is_lawful_monad seq1 := bind_assoc := @bind_assoc } end seq1 +end stream diff --git a/src/data/seq/wseq.lean b/src/data/seq/wseq.lean index 4182c7fe937a7..c55be3a1b2301 100644 --- a/src/data/seq/wseq.lean +++ b/src/data/seq/wseq.lean @@ -6,6 +6,7 @@ Authors: Mario Carneiro import data.list.basic import data.seq.seq +namespace stream open function universes u v w @@ -71,6 +72,7 @@ def rec_on {C : wseq α → Sort v} (s : wseq α) (h1 : C nil) (h2 : ∀ x s, C (cons x s)) (h3 : ∀ s, C (think s)) : C s := seq.rec_on s h1 (λ o, option.rec_on o h3 h2) +/-- membership for weak sequences-/ protected def mem (a : α) (s : wseq α) := seq.mem (some a) s instance : has_mem α (wseq α) := @@ -324,6 +326,7 @@ seq.join ((λ o : option (wseq α), match o with def bind (s : wseq α) (f : α → wseq β) : wseq β := join (map f s) +/-- lift a relation to a relation over weak sequences -/ @[simp] def lift_rel_o (R : α → β → Prop) (C : wseq α → wseq β → Prop) : option (α × wseq α) → option (β × wseq β) → Prop | none none := true @@ -342,6 +345,7 @@ theorem lift_rel_o.imp_right (R : α → β → Prop) {C D : wseq α → wseq β (H : ∀ s t, C s t → D s t) {o p} : lift_rel_o R C o p → lift_rel_o R D o p := lift_rel_o.imp (λ _ _, id) H +/-- Definitino of bisimilarity for weak sequences-/ @[simp] def bisim_o (R : wseq α → wseq α → Prop) : option (α × wseq α) → option (α × wseq α) → Prop := lift_rel_o (=) R @@ -557,6 +561,7 @@ by { simp [think, join], unfold functor.map, simp [join, cons, append] } @[simp] theorem append_assoc (s t u : wseq α) : append (append s t) u = append s (append t u) := seq.append_assoc _ _ _ +/-- auxilary defintion of tail over weak sequences-/ @[simp] def tail.aux : option (α × wseq α) → computation (option (α × wseq α)) | none := return none | (some (a, s)) := destruct s @@ -569,6 +574,7 @@ begin apply (@pure_bind computation _ _ _ _ _ _).trans _; simp end +/-- auxilary defintion of drop over weak sequences-/ @[simp] def drop.aux : ℕ → option (α × wseq α) → computation (option (α × wseq α)) | 0 := return | (n+1) := λ a, tail.aux a >>= drop.aux n @@ -591,7 +597,7 @@ theorem head_terminates_of_head_tail_terminates (s : wseq α) [T : terminates (h simp [tail] at h, rcases exists_of_mem_bind h with ⟨s', h1, h2⟩, unfold functor.map at h1, - exact let ⟨t, h3, h4⟩ := exists_of_mem_map h1 in terminates_of_mem h3 + exact let ⟨t, h3, h4⟩ := computation.exists_of_mem_map h1 in computation.terminates_of_mem h3 end theorem destruct_some_of_destruct_tail_some {s : wseq α} {a} @@ -599,7 +605,7 @@ theorem destruct_some_of_destruct_tail_some {s : wseq α} {a} begin unfold tail functor.map at h, simp at h, rcases exists_of_mem_bind h with ⟨t, tm, td⟩, clear h, - rcases exists_of_mem_map tm with ⟨t', ht', ht2⟩, clear tm, + rcases computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩, clear tm, cases t' with t'; rw ←ht2 at td; simp at td, { have := mem_unique td (ret_mem _), contradiction }, { exact ⟨_, ht'⟩ } @@ -609,10 +615,10 @@ theorem head_some_of_head_tail_some {s : wseq α} {a} (h : some a ∈ head (tail s)) : ∃ a', some a' ∈ head s := begin unfold head at h, - rcases exists_of_mem_map h with ⟨o, md, e⟩, clear h, + rcases computation.exists_of_mem_map h with ⟨o, md, e⟩, clear h, cases o with o; injection e with h', clear e h', cases destruct_some_of_destruct_tail_some md with a am, - exact ⟨_, mem_map ((<$>) (@prod.fst α (wseq α))) am⟩ + exact ⟨_, computation.mem_map ((<$>) (@prod.fst α (wseq α))) am⟩ end theorem head_some_of_nth_some {s : wseq α} {a n} @@ -719,7 +725,7 @@ theorem mem_of_mem_dropn {s : wseq α} {a} : ∀ {n}, a ∈ drop s n → a ∈ s theorem nth_mem {s : wseq α} {a n} : some a ∈ nth s n → a ∈ s := begin revert s, induction n with n IH; intros s h, - { rcases exists_of_mem_map h with ⟨o, h1, h2⟩, + { rcases computation.exists_of_mem_map h with ⟨o, h1, h2⟩, cases o with o; injection h2 with h', cases o with a' s', exact (eq_or_mem_iff_mem h1).2 (or.inl h'.symm) }, @@ -742,7 +748,7 @@ theorem exists_dropn_of_mem {s : wseq α} {a} (h : a ∈ s) : ∃ n s', some (a, s') ∈ destruct (drop s n) := let ⟨n, h⟩ := exists_nth_of_mem h in ⟨n, begin rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩, - have := mem_unique (mem_map _ om) h, + have := computation.mem_unique (computation.mem_map _ om) h, cases o with o; injection this with i, cases o with a' s', dsimp at i, rw i at om, exact ⟨_, om⟩ @@ -765,9 +771,9 @@ end theorem exists_of_lift_rel_left {R : α → β → Prop} {s t} (H : lift_rel R s t) {a} (h : a ∈ s) : ∃ {b}, b ∈ t ∧ R a b := let ⟨n, h⟩ := exists_nth_of_mem h, - ⟨some (._, s'), sd, rfl⟩ := exists_of_mem_map h, + ⟨some (._, s'), sd, rfl⟩ := computation.exists_of_mem_map h, ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (lift_rel_dropn_destruct H n).left sd in -⟨b, nth_mem (mem_map ((<$>) prod.fst.{v v}) td), ab⟩ +⟨b, nth_mem (computation.mem_map ((<$>) prod.fst.{v v}) td), ab⟩ theorem exists_of_lift_rel_right {R : α → β → Prop} {s t} (H : lift_rel R s t) {b} (h : b ∈ t) : ∃ {a}, a ∈ s ∧ R a b := @@ -807,7 +813,7 @@ by unfold equiv; simp; exact h theorem think_equiv (s : wseq α) : think s ~ s := by unfold equiv; simp; apply equiv.refl -theorem think_congr {s t : wseq α} (a : α) (h : s ~ t) : think s ~ think t := +theorem think_congr {s t : wseq α} (h : s ~ t) : think s ~ think t := by unfold equiv; simp; exact h theorem head_congr : ∀ {s t : wseq α}, s ~ t → head s ~ head t := @@ -820,11 +826,11 @@ begin cases destruct_congr h with l r, rcases l dsm with ⟨dt, dtm, dst⟩, cases ds with a; cases dt with b, - { apply mem_map _ dtm }, + { apply computation.mem_map _ dtm }, { cases b, cases dst }, { cases a, cases dst }, { cases a with a s', cases b with b t', rw dst.left, - exact @mem_map _ _ (@functor.map _ _ (α × wseq α) _ prod.fst) + exact @computation.mem_map _ _ (@functor.map _ _ (α × wseq α) _ prod.fst) _ (destruct t) dtm } end @@ -885,23 +891,24 @@ theorem equiv.ext {s t : wseq α} (h : ∀ n, nth s n ~ nth t n) : s ~ t := { intros a b ma mb, cases a with a; cases b with b, { trivial }, - { injection mem_unique (mem_map _ ma) ((h 0 _).2 (mem_map _ mb)) }, - { injection mem_unique (mem_map _ ma) ((h 0 _).2 (mem_map _ mb)) }, + { injection mem_unique (computation.mem_map _ ma) ((h 0 _).2 (computation.mem_map _ mb)) }, + { injection mem_unique (computation.mem_map _ ma) ((h 0 _).2 (computation.mem_map _ mb)) }, { cases a with a s', cases b with b t', - injection mem_unique (mem_map _ ma) ((h 0 _).2 (mem_map _ mb)) with ab, + injection mem_unique + (computation.mem_map _ ma) ((h 0 _).2 (computation.mem_map _ mb)) with ab, refine ⟨ab, λ n, _⟩, - refine (nth_congr (flatten_equiv (mem_map _ ma)) n).symm.trans + refine (nth_congr (flatten_equiv (computation.mem_map _ ma)) n).symm.trans ((_ : nth (tail s) n ~ nth (tail t) n).trans - (nth_congr (flatten_equiv (mem_map _ mb)) n)), + (nth_congr (flatten_equiv (computation.mem_map _ mb)) n)), rw [nth_tail, nth_tail], apply h } } end⟩ theorem length_eq_map (s : wseq α) : length s = computation.map list.length (to_list s) := begin - refine eq_of_bisim + refine computation.eq_of_bisim (λ c1 c2, ∃ (l : list α) (s : wseq α), - c1 = corec length._match_2 (l.length, s) ∧ - c2 = computation.map list.length (corec to_list._match_2 (l, s))) + c1 = computation.corec length._match_2 (l.length, s) ∧ + c2 = computation.map list.length (computation.corec to_list._match_2 (l, s))) _ ⟨[], s, rfl, rfl⟩, intros s1 s2 h, rcases h with ⟨l, s, h⟩, rw [h.left, h.right], apply s.rec_on _ (λ a s, _) (λ s, _); @@ -918,27 +925,27 @@ show seq.map some (seq.of_list (a :: l)) = seq.cons (some a) (seq.map some (seq.of_list l)), by simp @[simp] theorem to_list'_nil (l : list α) : - corec to_list._match_2 (l, nil) = return l.reverse := + computation.corec to_list._match_2 (l, nil) = return l.reverse := destruct_eq_ret rfl @[simp] theorem to_list'_cons (l : list α) (s : wseq α) (a : α) : - corec to_list._match_2 (l, cons a s) = - (corec to_list._match_2 (a::l, s)).think := + computation.corec to_list._match_2 (l, cons a s) = + (computation.corec to_list._match_2 (a::l, s)).think := destruct_eq_think $ by simp [to_list, cons] @[simp] theorem to_list'_think (l : list α) (s : wseq α) : - corec to_list._match_2 (l, think s) = - (corec to_list._match_2 (l, s)).think := + computation.corec to_list._match_2 (l, think s) = + (computation.corec to_list._match_2 (l, s)).think := destruct_eq_think $ by simp [to_list, think] theorem to_list'_map (l : list α) (s : wseq α) : - corec to_list._match_2 (l, s) = + computation.corec to_list._match_2 (l, s) = ((++) l.reverse) <$> to_list s := begin - refine eq_of_bisim + refine computation.eq_of_bisim (λ c1 c2, ∃ (l' : list α) (s : wseq α), - c1 = corec to_list._match_2 (l' ++ l, s) ∧ - c2 = computation.map ((++) l.reverse) (corec to_list._match_2 (l', s))) + c1 = computation.corec to_list._match_2 (l' ++ l, s) ∧ + c2 = computation.map ((++) l.reverse) (computation.corec to_list._match_2 (l', s))) _ ⟨[], s, rfl, rfl⟩, intros s1 s2 h, rcases h with ⟨l', s, h⟩, rw [h.left, h.right], apply s.rec_on _ (λ a s, _) (λ s, _); @@ -955,7 +962,7 @@ destruct_eq_think $ by unfold to_list; simp; rw to_list'_map; simp; refl destruct_eq_ret rfl theorem to_list_of_list (l : list α) : l ∈ to_list (of_list l) := -by induction l with a l IH; simp [ret_mem]; exact think_mem (mem_map _ IH) +by induction l with a l IH; simp [ret_mem]; exact think_mem (computation.mem_map _ IH) @[simp] theorem destruct_of_seq (s : seq α) : destruct (of_seq s) = return (s.head.map $ λ a, (a, of_seq s.tail)) := @@ -1061,7 +1068,7 @@ let ⟨t, tm, bt⟩ := exists_of_mem_join h, theorem destruct_map (f : α → β) (s : wseq α) : destruct (map f s) = computation.map (option.map (prod.map f (map f))) (destruct s) := begin - apply eq_of_bisim (λ c1 c2, ∃ s, c1 = destruct (map f s) ∧ + apply computation.eq_of_bisim (λ c1 c2, ∃ s, c1 = destruct (map f s) ∧ c2 = computation.map (option.map (prod.map f (map f))) (destruct s)), { intros c1 c2 h, cases h with s h, rw [h.left, h.right], apply s.rec_on _ (λ a s, _) (λ s, _); simp, @@ -1089,6 +1096,7 @@ end end⟩ theorem map_congr (f : α → β) {s t : wseq α} (h : s ~ t) : map f s ~ map f t := lift_rel_map _ _ h (λ _ _, congr_arg _) +/-- auxilary defintion of `destruct_append` over weak sequences-/ @[simp] def destruct_append.aux (t : wseq α) : option (α × wseq α) → computation (option (α × wseq α)) | none := destruct t @@ -1097,7 +1105,7 @@ lift_rel_map _ _ h (λ _ _, congr_arg _) theorem destruct_append (s t : wseq α) : destruct (append s t) = (destruct s).bind (destruct_append.aux t) := begin - apply eq_of_bisim (λ c1 c2, ∃ s t, c1 = destruct (append s t) ∧ + apply computation.eq_of_bisim (λ c1 c2, ∃ s t, c1 = destruct (append s t) ∧ c2 = (destruct s).bind (destruct_append.aux t)) _ ⟨s, t, rfl, rfl⟩, intros c1 c2 h, rcases h with ⟨s, t, h⟩, rw [h.left, h.right], apply s.rec_on _ (λ a s, _) (λ s, _); simp, @@ -1106,6 +1114,7 @@ begin { exact ⟨s, t, rfl, rfl⟩ } end +/-- auxilary defintion of `destruct_join` over weak sequences-/ @[simp] def destruct_join.aux : option (wseq α × wseq (wseq α)) → computation (option (α × wseq α)) | none := return none | (some (s, S)) := (destruct (append s (join S))).think @@ -1113,7 +1122,7 @@ end theorem destruct_join (S : wseq (wseq α)) : destruct (join S) = (destruct S).bind destruct_join.aux := begin - apply eq_of_bisim (λ c1 c2, c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ + apply computation.eq_of_bisim (λ c1 c2, c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux) _ (or.inr ⟨S, rfl, rfl⟩), intros c1 c2 h, exact match c1, c2, h with | _, _, (or.inl $ eq.refl c) := by cases c.destruct; simp @@ -1359,3 +1368,4 @@ instance : is_lawful_monad wseq := -/ end wseq +end stream