refactor(algebra/continued_fractions): remove use of open ... as (#9847)

Lean 4 doesn't support the use of `open ... as ...`, so let's get rid of the few uses from mathlib rather than automating it in mathport.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/continued_fractions/basic.lean

@@ -46,33 +46,32 @@ variable (α : Type*)
 @[derive inhabited]
 protected structure generalized_continued_fraction.pair := (a : α) (b : α)
 
+open generalized_continued_fraction
+
 /-! Interlude: define some expected coercions and instances. -/
 namespace generalized_continued_fraction.pair
-open generalized_continued_fraction as gcf
 
 variable {α}
 
 /-- Make a `gcf.pair` printable. -/
-instance [has_repr α] : has_repr (gcf.pair α) :=
+instance [has_repr α] : has_repr (pair α) :=
 ⟨λ p, "(a : " ++ (repr p.a) ++ ", b : " ++ (repr p.b) ++ ")"⟩
 
 /-- Maps a function `f` on both components of a given pair. -/
-def map {β : Type*} (f : α → β) (gp : gcf.pair α) : gcf.pair β :=
+def map {β : Type*} (f : α → β) (gp : pair α) : pair β :=
 ⟨f gp.a, f gp.b⟩
 
 section coe
 /- Fix another type `β` which we will convert to. -/
 variables {β : Type*} [has_coe α β]
 
 /-- Coerce a pair by elementwise coercion. -/
-instance has_coe_to_generalized_continued_fraction_pair :
-  has_coe (gcf.pair α) (gcf.pair β) :=
+instance has_coe_to_generalized_continued_fraction_pair : has_coe (pair α) (pair β) :=
 ⟨map coe⟩
 
 @[simp, norm_cast]
 lemma coe_to_generalized_continued_fraction_pair {a b : α} :
-  (↑(gcf.pair.mk a b) : gcf.pair β) = gcf.pair.mk (a : β) (b : β) :=
-rfl
+  (↑(pair.mk a b) : pair β) = pair.mk (a : β) (b : β) := rfl
 
 end coe
 end generalized_continued_fraction.pair
@@ -99,46 +98,50 @@ generalized_continued_fraction.pairs `s`.
 For convenience, one often writes `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`.
 -/
 structure generalized_continued_fraction :=
-(h : α) (s : seq $ generalized_continued_fraction.pair α)
+(h : α) (s : seq $ pair α)
 
 variable {α}
 
 namespace generalized_continued_fraction
-open generalized_continued_fraction as gcf
 
 /-- Constructs a generalized continued fraction without fractional part. -/
-def of_integer (a : α) : gcf α :=
+def of_integer (a : α) : generalized_continued_fraction α :=
 ⟨a, seq.nil⟩
 
-instance [inhabited α] : inhabited (gcf α) := ⟨of_integer (default _)⟩
+instance [inhabited α] : inhabited (generalized_continued_fraction α) := ⟨of_integer (default _)⟩
 
 /-- Returns the sequence of partial numerators `aᵢ` of `g`. -/
-def partial_numerators (g : gcf α) : seq α := g.s.map gcf.pair.a
+def partial_numerators (g : generalized_continued_fraction α) : seq α :=
+g.s.map pair.a
 /-- Returns the sequence of partial denominators `bᵢ` of `g`. -/
-def partial_denominators (g : gcf α) : seq α := g.s.map gcf.pair.b
+def partial_denominators (g : generalized_continued_fraction α) : seq α :=
+g.s.map pair.b
 
 /-- A gcf terminated at position `n` if its sequence terminates at position `n`. -/
-def terminated_at (g : gcf α) (n : ℕ) : Prop := g.s.terminated_at n
+def terminated_at (g : generalized_continued_fraction α) (n : ℕ) : Prop := g.s.terminated_at n
 
 /-- It is decidable whether a gcf terminated at a given position. -/
-instance terminated_at_decidable (g : gcf α) (n : ℕ) : decidable (g.terminated_at n) :=
+instance terminated_at_decidable (g : generalized_continued_fraction α) (n : ℕ) :
+  decidable (g.terminated_at n) :=
 by { unfold terminated_at, apply_instance }
 
 /-- A gcf terminates if its sequence terminates. -/
-def terminates (g : gcf α) : Prop := g.s.terminates
+def terminates (g : generalized_continued_fraction α) : Prop := g.s.terminates
 
 section coe
 /-! Interlude: define some expected coercions. -/
 /- Fix another type `β` which we will convert to. -/
 variables {β : Type*} [has_coe α β]
 
 /-- Coerce a gcf by elementwise coercion. -/
-instance has_coe_to_generalized_continued_fraction : has_coe (gcf α) (gcf β) :=
-⟨λ g, ⟨(g.h : β), (g.s.map coe : seq $ gcf.pair β)⟩⟩
+instance has_coe_to_generalized_continued_fraction :
+  has_coe (generalized_continued_fraction α) (generalized_continued_fraction β) :=
+⟨λ g, ⟨(g.h : β), (g.s.map coe : seq $ pair β)⟩⟩
 
 @[simp, norm_cast]
-lemma coe_to_generalized_continued_fraction {g : gcf α} :
-  (↑(g : gcf α) : gcf β) = ⟨(g.h : β), (g.s.map coe : seq $ gcf.pair β)⟩ :=
+lemma coe_to_generalized_continued_fraction {g : generalized_continued_fraction α} :
+  (↑(g : generalized_continued_fraction α) : generalized_continued_fraction β) =
+    ⟨(g.h : β), (g.s.map coe : seq $ pair β)⟩ :=
 rfl
 
 end coe
@@ -188,21 +191,22 @@ def simple_continued_fraction [has_one α] :=
 variable {α}
 /- Interlude: define some expected coercions. -/
 namespace simple_continued_fraction
-open generalized_continued_fraction as gcf
-open simple_continued_fraction as scf
+
 variable [has_one α]
 
 /-- Constructs a simple continued fraction without fractional part. -/
-def of_integer (a : α) : scf α :=
-⟨gcf.of_integer a, λ n aₙ h, by cases h⟩
+def of_integer (a : α) : simple_continued_fraction α :=
+⟨generalized_continued_fraction.of_integer a, λ n aₙ h, by cases h⟩
 
-instance : inhabited (scf α) := ⟨of_integer 1⟩
+instance : inhabited (simple_continued_fraction α) := ⟨of_integer 1⟩
 
 /-- Lift a scf to a gcf using the inclusion map. -/
-instance has_coe_to_generalized_continued_fraction : has_coe (scf α) (gcf α) :=
-by {unfold scf, apply_instance}
+instance has_coe_to_generalized_continued_fraction :
+  has_coe (simple_continued_fraction α) (generalized_continued_fraction α) :=
+by {unfold simple_continued_fraction, apply_instance}
 
-lemma coe_to_generalized_continued_fraction {s : scf α} : (↑s : gcf α) = s.val := rfl
+lemma coe_to_generalized_continued_fraction {s : simple_continued_fraction α} :
+  (↑s : generalized_continued_fraction α) = s.val := rfl
 
 end simple_continued_fraction
 
@@ -229,27 +233,30 @@ variable {α}
 
 /-! Interlude: define some expected coercions. -/
 namespace continued_fraction
-open generalized_continued_fraction as gcf
-open simple_continued_fraction as scf
-open continued_fraction as cf
+
 variables [has_one α] [has_zero α] [has_lt α]
 
 /-- Constructs a continued fraction without fractional part. -/
-def of_integer (a : α) : cf α :=
-⟨scf.of_integer a, λ n bₙ h, by cases h⟩
+def of_integer (a : α) : continued_fraction α :=
+⟨simple_continued_fraction.of_integer a, λ n bₙ h, by cases h⟩
 
-instance : inhabited (cf α) := ⟨of_integer 0⟩
+instance : inhabited (continued_fraction α) := ⟨of_integer 0⟩
 
 /-- Lift a cf to a scf using the inclusion map. -/
-instance has_coe_to_simple_continued_fraction : has_coe (cf α) (scf α) :=
-by {unfold cf, apply_instance}
+instance has_coe_to_simple_continued_fraction :
+  has_coe (continued_fraction α) (simple_continued_fraction α) :=
+by {unfold continued_fraction, apply_instance}
 
-lemma coe_to_simple_continued_fraction {c : cf α} : (↑c : scf α) = c.val := rfl
+lemma coe_to_simple_continued_fraction {c : continued_fraction α} :
+  (↑c : simple_continued_fraction α) = c.val := rfl
 
 /-- Lift a cf to a scf using the inclusion map. -/
-instance has_coe_to_generalized_continued_fraction : has_coe (cf α) (gcf α) := ⟨λ c, ↑(↑c : scf α)⟩
+instance has_coe_to_generalized_continued_fraction :
+  has_coe (continued_fraction α) (generalized_continued_fraction α) :=
+⟨λ c, ↑(↑c : simple_continued_fraction α)⟩
 
-lemma coe_to_generalized_continued_fraction {c : cf α} : (↑c : gcf α) = c.val := rfl
+lemma coe_to_generalized_continued_fraction {c : continued_fraction α} :
+  (↑c : generalized_continued_fraction α) = c.val := rfl
 
 end continued_fraction
 
@@ -262,7 +269,6 @@ directly evaluating the (infinite) fraction described by the gcf or using a recu
 For (r)cfs, these computations are equivalent as shown in
 `algebra.continued_fractions.convergents_equiv`.
 -/
-open generalized_continued_fraction as gcf
 
 -- Fix a division ring for the computations.
 variables {K : Type*} [division_ring K]
@@ -292,11 +298,11 @@ def next_denominator (aₙ bₙ ppredB predB : K) : K := bₙ * predB + aₙ * p
 Returns the next continuants `⟨Aₙ, Bₙ⟩` using `next_numerator` and `next_denominator`, where `pred`
 is `⟨Aₙ₋₁, Bₙ₋₁⟩`, `ppred` is `⟨Aₙ₋₂, Bₙ₋₂⟩`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
-def next_continuants (a b : K) (ppred pred : gcf.pair K) : gcf.pair K :=
+def next_continuants (a b : K) (ppred pred : pair K) : pair K :=
 ⟨next_numerator a b ppred.a pred.a, next_denominator a b ppred.b pred.b⟩
 
 /-- Returns the continuants `⟨Aₙ₋₁, Bₙ₋₁⟩` of `g`. -/
-def continuants_aux (g : gcf K) : stream (gcf.pair K)
+def continuants_aux (g : generalized_continued_fraction K) : stream (pair K)
 | 0 := ⟨1, 0⟩
 | 1 := ⟨g.h, 1⟩
 | (n + 2) :=
@@ -306,23 +312,27 @@ def continuants_aux (g : gcf K) : stream (gcf.pair K)
   end
 
 /-- Returns the continuants `⟨Aₙ, Bₙ⟩` of `g`. -/
-def continuants (g : gcf K) : stream (gcf.pair K) := g.continuants_aux.tail
+def continuants (g : generalized_continued_fraction K) : stream (pair K) :=
+g.continuants_aux.tail
 
 /-- Returns the numerators `Aₙ` of `g`. -/
-def numerators (g : gcf K) : stream K := g.continuants.map gcf.pair.a
+def numerators (g : generalized_continued_fraction K) : stream K :=
+g.continuants.map pair.a
 
 /-- Returns the denominators `Bₙ` of `g`. -/
-def denominators (g : gcf K) : stream K := g.continuants.map gcf.pair.b
+def denominators (g : generalized_continued_fraction K) : stream K :=
+g.continuants.map pair.b
 
 /-- Returns the convergents `Aₙ / Bₙ` of `g`, where `Aₙ, Bₙ` are the nth continuants of `g`. -/
-def convergents (g : gcf K) : stream K := λ (n : ℕ), (g.numerators n) / (g.denominators n)
+def convergents (g : generalized_continued_fraction K) : stream K :=
+λ (n : ℕ), (g.numerators n) / (g.denominators n)
 
 /--
 Returns the approximation of the fraction described by the given sequence up to a given position n.
 For example, `convergents'_aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4)` and
 `convergents'_aux [(1, 2), (3, 4), (5, 6)] 0 = 0`.
 -/
-def convergents'_aux : seq (gcf.pair K) → ℕ → K
+def convergents'_aux : seq (pair K) → ℕ → K
 | s 0 := 0
 | s (n + 1) := match s.head with
   | none := 0
@@ -334,20 +344,21 @@ Returns the convergents of `g` by evaluating the fraction described by `g` up to
 position `n`. For example, `convergents' [9; (1, 2), (3, 4), (5, 6)] 2 = 9 + 1 / (2 + 3 / 4)` and
 `convergents' [9; (1, 2), (3, 4), (5, 6)] 0 = 9`
 -/
-def convergents' (g : gcf K) (n : ℕ) : K := g.h + convergents'_aux g.s n
+def convergents' (g : generalized_continued_fraction K) (n : ℕ) : K := g.h + convergents'_aux g.s n
 
 end generalized_continued_fraction
 
 -- Now, some basic, general theorems
 namespace generalized_continued_fraction
-open generalized_continued_fraction as gcf
 
 /-- Two gcfs `g` and `g'` are equal if and only if their components are equal. -/
-protected lemma ext_iff {g g' : gcf α} : g = g' ↔ g.h = g'.h ∧ g.s = g'.s :=
+protected lemma ext_iff {g g' : generalized_continued_fraction α} :
+  g = g' ↔ g.h = g'.h ∧ g.s = g'.s :=
 by { cases g, cases g', simp }
 
 @[ext]
-protected lemma ext {g g' : gcf α} (hyp : g.h = g'.h ∧ g.s = g'.s) : g = g' :=
+protected lemma ext {g g' : generalized_continued_fraction α} (hyp : g.h = g'.h ∧ g.s = g'.s) :
+  g = g' :=
 generalized_continued_fraction.ext_iff.elim_right hyp
 
 end generalized_continued_fraction

src/algebra/continued_fractions/computation/approximation_corollaries.lean

@@ -37,31 +37,32 @@ convergence, fractions
 -/
 
 variables {K : Type*} (v : K) [linear_ordered_field K] [floor_ring K]
-open generalized_continued_fraction as gcf
+
+open generalized_continued_fraction (of)
+open generalized_continued_fraction
 
 lemma generalized_continued_fraction.of_is_simple_continued_fraction :
-  (gcf.of v).is_simple_continued_fraction :=
-(λ _ _ nth_part_num_eq, gcf.of_part_num_eq_one nth_part_num_eq)
+  (of v).is_simple_continued_fraction :=
+(λ _ _ nth_part_num_eq, of_part_num_eq_one nth_part_num_eq)
 
 /-- Creates the simple continued fraction of a value. -/
 def simple_continued_fraction.of : simple_continued_fraction K :=
-⟨gcf.of v, generalized_continued_fraction.of_is_simple_continued_fraction v⟩
+⟨of v, generalized_continued_fraction.of_is_simple_continued_fraction v⟩
 
 lemma simple_continued_fraction.of_is_continued_fraction :
   (simple_continued_fraction.of v).is_continued_fraction :=
-(λ _ denom nth_part_denom_eq,
-  lt_of_lt_of_le zero_lt_one(gcf.of_one_le_nth_part_denom nth_part_denom_eq))
+(λ _ denom nth_part_denom_eq, lt_of_lt_of_le zero_lt_one
+  (of_one_le_nth_part_denom nth_part_denom_eq))
 
 /-- Creates the continued fraction of a value. -/
 def continued_fraction.of : continued_fraction K :=
 ⟨simple_continued_fraction.of v, simple_continued_fraction.of_is_continued_fraction v⟩
 
 namespace generalized_continued_fraction
 
-open continued_fraction as cf
-
-lemma of_convergents_eq_convergents' : (gcf.of v).convergents = (gcf.of v).convergents' :=
-@cf.convergents_eq_convergents'  _ _ (continued_fraction.of v)
+lemma of_convergents_eq_convergents' :
+  (of v).convergents = (of v).convergents' :=
+@continued_fraction.convergents_eq_convergents'  _ _ (continued_fraction.of v)
 
 section convergence
 /-!
@@ -74,15 +75,15 @@ variable [archimedean K]
 open nat
 
 theorem of_convergence_epsilon :
-  ∀ (ε > (0 : K)), ∃ (N : ℕ), ∀ (n ≥ N), |v - (gcf.of v).convergents n| < ε :=
+  ∀ (ε > (0 : K)), ∃ (N : ℕ), ∀ (n ≥ N), |v - (of v).convergents n| < ε :=
 begin
   assume ε ε_pos,
   -- use the archimedean property to obtian a suitable N
   rcases (exists_nat_gt (1 / ε) : ∃ (N' : ℕ), 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩,
   let N := max N' 5, -- set minimum to 5 to have N ≤ fib N work
   existsi N,
   assume n n_ge_N,
-  let g := gcf.of v,
+  let g := of v,
   cases decidable.em (g.terminated_at n) with terminated_at_n not_terminated_at_n,
   { have : v = g.convergents n, from of_correctness_of_terminated_at terminated_at_n,
     have : v - g.convergents n = 0, from sub_eq_zero.elim_right this,
@@ -136,7 +137,7 @@ end
 local attribute [instance] preorder.topology
 
 theorem of_convergence [order_topology K] :
-  filter.tendsto ((gcf.of v).convergents) filter.at_top $ nhds v :=
+  filter.tendsto ((of v).convergents) filter.at_top $ nhds v :=
 by simpa [linear_ordered_add_comm_group.tendsto_nhds, abs_sub_comm] using (of_convergence_epsilon v)
 
 end convergence