refactor(data/seq): scope seq and wseq to namespace stream (#18284)

arienmalec · kim-em · arienmalec · commit a7e36e48519a · 2023-03-29T02:46:56.000Z
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 &lt;scott.morrison@gmail.com&gt;
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
