refactor(algebra/floor): Rename floor and ceil functions (#9590)

This renames
* `floor` -> `int.floor`
* `ceil` -> `int.ceil`
* `fract` -> `int.fract`
* `nat_floor` -> `nat.floor`
* `nat_ceil` -> `nat.ceil`

archive/imo/imo2013_q5.lean

@@ -121,15 +121,15 @@ lemma fx_gt_xm1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 ≤ x)
 begin
   have hx0 :=
     calc (x - 1 : ℝ)
-          < ⌊x⌋₊   : by exact_mod_cast sub_one_lt_nat_floor x
-      ... ≤ f ⌊x⌋₊ : H4 _ (nat_floor_pos.2 hx),
+          < ⌊x⌋₊   : by exact_mod_cast nat.sub_one_lt_floor x
+      ... ≤ f ⌊x⌋₊ : H4 _ (nat.floor_pos.2 hx),
 
-  obtain h_eq | h_lt := (nat_floor_le $ zero_le_one.trans hx).eq_or_lt,
+  obtain h_eq | h_lt := (nat.floor_le $ zero_le_one.trans hx).eq_or_lt,
   { rwa h_eq at hx0 },
 
   calc (x - 1 : ℝ) < f ⌊x⌋₊ : hx0
     ... < f (x - ⌊x⌋₊) + f ⌊x⌋₊ : lt_add_of_pos_left _ (f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
-    ... ≤ f (x - ⌊x⌋₊ + ⌊x⌋₊)   : H2 _ _ (sub_pos.mpr h_lt) (nat.cast_pos.2 (nat_floor_pos.2 hx))
+    ... ≤ f (x - ⌊x⌋₊ + ⌊x⌋₊)   : H2 _ _ (sub_pos.mpr h_lt) (nat.cast_pos.2 (nat.floor_pos.2 hx))
     ... = f x                   : by rw sub_add_cancel
 end
 

src/algebra/archimedean.lean

@@ -28,6 +28,8 @@ number `n` such that `x ≤ n • y`.
 * `ℕ`, `ℤ`, and `ℚ` are archimedean.
 -/
 
+open int
+
 variables {α : Type*}
 
 /-- An ordered additive commutative monoid is called `archimedean` if for any two elements `x`, `y`
@@ -159,7 +161,7 @@ let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy in
 let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy in
   have hb: ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b, from
     ⟨M, λ m hm, le_of_not_lt (λ hlt, not_lt_of_ge
-  (fpow_le_of_le (le_of_lt hy) (le_of_lt hlt))
+  (fpow_le_of_le hy.le hlt.le)
     (lt_of_le_of_lt hm (by rwa ← gpow_coe_nat at hM)))⟩,
 let ⟨n, hn₁, hn₂⟩ := int.exists_greatest_of_bdd hb he in
   ⟨n, hn₁, lt_of_not_ge (λ hge, not_le_of_gt (int.lt_succ _) (hn₂ _ hge))⟩
@@ -262,7 +264,7 @@ theorem archimedean_iff_rat_lt :
   λ H, archimedean_iff_nat_lt.2 $ λ x,
   let ⟨q, h⟩ := H x in
   ⟨⌈q⌉₊, lt_of_lt_of_le h $
-    by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (le_nat_ceil _)⟩⟩
+    by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (nat.le_ceil _)⟩⟩
 
 theorem archimedean_iff_rat_le :
   archimedean α ↔ ∀ x : α, ∃ q : ℚ, x ≤ q :=

src/algebra/continued_fractions/computation/approximations.lean

@@ -45,7 +45,7 @@ the error term indeed gets smaller. As a corollary, we will be able to show that
 -/
 
 namespace generalized_continued_fraction
-open generalized_continued_fraction as gcf
+open generalized_continued_fraction as gcf int
 
 variables {K : Type*} {v : K} {n : ℕ} [linear_ordered_field K] [floor_ring K]
 
@@ -63,10 +63,12 @@ begin
   cases n,
   case nat.zero
   { have : int_fract_pair.of v = ifp_n, by injection nth_stream_eq,
-    simp [fract_lt_one, fract_nonneg, int_fract_pair.of, this.symm] },
+    rw [←this, int_fract_pair.of],
+    exact ⟨fract_nonneg _, fract_lt_one _⟩ },
   case nat.succ
   { rcases (succ_nth_stream_eq_some_iff.elim_left nth_stream_eq) with ⟨_, _, _, ifp_of_eq_ifp_n⟩,
-    simp [fract_lt_one, fract_nonneg, int_fract_pair.of, ifp_of_eq_ifp_n.symm] }
+    rw [←ifp_of_eq_ifp_n, int_fract_pair.of],
+    exact ⟨fract_nonneg _, fract_lt_one _⟩ }
 end
 
 /-- Shows that the fractional parts of the stream are nonnegative. -/

src/algebra/continued_fractions/computation/basic.lean

@@ -111,7 +111,7 @@ end coe
 variables [linear_ordered_field K] [floor_ring K]
 
 /-- Creates the integer and fractional part of a value `v`, i.e. `⟨⌊v⌋, v - ⌊v⌋⟩`. -/
-protected def of (v : K) : int_fract_pair K := ⟨⌊v⌋, fract v⟩
+protected def of (v : K) : int_fract_pair K := ⟨⌊v⌋, int.fract v⟩
 
 /--
 Creates the stream of integer and fractional parts of a value `v` needed to obtain the continued

src/algebra/continued_fractions/computation/correctness_terminating.lean

@@ -69,9 +69,9 @@ variable [floor_ring K]
 
 /-- Just a computational lemma we need for the next main proof. -/
 protected lemma comp_exact_value_correctness_of_stream_eq_some_aux_comp {a : K} (b c : K)
-  (fract_a_ne_zero : fract a ≠ 0) :
-  ((⌊a⌋ : K) * b + c) / (fract a) + b = (b * a + c) / fract a :=
-by { field_simp [fract_a_ne_zero], rw [fract], ring }
+  (fract_a_ne_zero : int.fract a ≠ 0) :
+  ((⌊a⌋ : K) * b + c) / (int.fract a) + b = (b * a + c) / int.fract a :=
+by { field_simp [fract_a_ne_zero], rw int.fract, ring }
 
 open generalized_continued_fraction as gcf
 
@@ -105,13 +105,13 @@ begin
     { have : int_fract_pair.stream v 0 = some (int_fract_pair.of v), from rfl,
       simpa only [this] using stream_zero_eq },
     cases this,
-    cases decidable.em (fract v = 0) with fract_eq_zero fract_ne_zero,
-    -- fract v = 0; we must then have `v = ⌊v⌋`
+    cases decidable.em (int.fract v = 0) with fract_eq_zero fract_ne_zero,
+    -- int.fract v = 0; we must then have `v = ⌊v⌋`
     { suffices : v = ⌊v⌋, by simpa [continuants_aux, fract_eq_zero, gcf.comp_exact_value],
       calc
-          v = fract v + ⌊v⌋ : by rw fract_add_floor
+          v = int.fract v + ⌊v⌋ : by rw int.fract_add_floor
         ... = ⌊v⌋           : by simp [fract_eq_zero] },
-    -- fract v ≠ 0; the claim then easily follows by unfolding a single computation step
+    -- int.fract v ≠ 0; the claim then easily follows by unfolding a single computation step
     { field_simp [continuants_aux, next_continuants, next_numerator, next_denominator,
         gcf.of_h_eq_floor, gcf.comp_exact_value, fract_ne_zero] } },
   { assume ifp_succ_n succ_nth_stream_eq,  -- nat.succ
@@ -172,7 +172,7 @@ begin
       have tmp_calc' := gcf.comp_exact_value_correctness_of_stream_eq_some_aux_comp
         pB ppB ifp_succ_n_fr_ne_zero,
       rw inv_eq_one_div at tmp_calc tmp_calc',
-      have : fract (1 / ifp_n.fr) ≠ 0, by simpa using ifp_succ_n_fr_ne_zero,
+      have : int.fract (1 / ifp_n.fr) ≠ 0, by simpa using ifp_succ_n_fr_ne_zero,
       -- now unfold the recurrence one step and simplify both sides to arrive at the conclusion
       field_simp [conts, gcf.comp_exact_value,
         (gcf.continuants_aux_recurrence s_nth_eq ppconts_eq pconts_eq), next_continuants,

src/algebra/continued_fractions/computation/terminates_iff_rat.lean

@@ -162,7 +162,7 @@ namespace int_fract_pair
 
 lemma coe_of_rat_eq :
   ((int_fract_pair.of q).mapFr coe : int_fract_pair K) = int_fract_pair.of v :=
-by simp [int_fract_pair.of, v_eq_q, fract]
+by simp [int_fract_pair.of, v_eq_q, int.fract]
 
 lemma coe_stream_nth_rat_eq :
     ((int_fract_pair.stream q n).map (mapFr coe) : option $ int_fract_pair K)
@@ -246,10 +246,10 @@ section terminates_of_rat
 
 Finally, we show that the continued fraction of a rational number terminates.
 
-The crucial insight is that, given any `q : ℚ` with `0 < q < 1`, the numerator of `fract q` is
+The crucial insight is that, given any `q : ℚ` with `0 < q < 1`, the numerator of `int.fract q` is
 smaller than the numerator of `q`. As the continued fraction computation recursively operates on
-the fractional part of a value `v` and `0 ≤ fract v < 1`, we infer that the numerator of the
-fractional part in the computation decreases by at least one in each step. As `0 ≤ fract v`,
+the fractional part of a value `v` and `0 ≤ int.fract v < 1`, we infer that the numerator of the
+fractional part in the computation decreases by at least one in each step. As `0 ≤ int.fract v`,
 this process must stop after finite number of steps, and the computation hence terminates.
 -/
 
@@ -306,15 +306,15 @@ end
 
 lemma exists_nth_stream_eq_none_of_rat (q : ℚ) : ∃ (n : ℕ), int_fract_pair.stream q n = none :=
 begin
-  let fract_q_num := (fract q).num, let n := fract_q_num.nat_abs + 1,
+  let fract_q_num := (int.fract q).num, let n := fract_q_num.nat_abs + 1,
   cases stream_nth_eq : (int_fract_pair.stream q n) with ifp,
   { use n, exact stream_nth_eq },
   { -- arrive at a contradiction since the numerator decreased num + 1 times but every fractional
     -- value is nonnegative.
     have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n, from
       stream_nth_fr_num_le_fr_num_sub_n_rat stream_nth_eq,
     have : fract_q_num - n = -1, by
-    { have : 0 ≤ fract_q_num, from rat.num_nonneg_iff_zero_le.elim_right (fract_nonneg q),
+    { have : 0 ≤ fract_q_num, from rat.num_nonneg_iff_zero_le.elim_right (int.fract_nonneg q),
       simp [(int.nat_abs_of_nonneg this), sub_add_eq_sub_sub_swap, sub_right_comm] },
     have : ifp.fr.num ≤ -1, by rwa this at ifp_fr_num_le_q_fr_num_sub_n,
     have : 0 ≤ ifp.fr, from (nth_stream_fr_nonneg_lt_one stream_nth_eq).left,

src/algebra/continued_fractions/computation/translations.lean

@@ -125,11 +125,11 @@ begin
   have : int_fract_pair.of ifp_n_fr⁻¹ = ifp_succ_n, by finish,
   cases ifp_succ_n with _ ifp_succ_n_fr,
   change ifp_succ_n_fr = 0 at succ_nth_fr_eq_zero,
-  have : fract ifp_n_fr⁻¹ = ifp_succ_n_fr, by injection this,
-  have : fract ifp_n_fr⁻¹ = 0, by rwa [succ_nth_fr_eq_zero] at this,
+  have : int.fract ifp_n_fr⁻¹ = ifp_succ_n_fr, by injection this,
+  have : int.fract ifp_n_fr⁻¹ = 0, by rwa [succ_nth_fr_eq_zero] at this,
   calc
-    ifp_n_fr⁻¹ = fract ifp_n_fr⁻¹ + ⌊ifp_n_fr⁻¹⌋ : by rw (fract_add_floor ifp_n_fr⁻¹)
-           ... = ⌊ifp_n_fr⁻¹⌋                    : by simp [‹fract ifp_n_fr⁻¹ = 0›]
+    ifp_n_fr⁻¹ = int.fract ifp_n_fr⁻¹ + ⌊ifp_n_fr⁻¹⌋ : by rw (int.fract_add_floor ifp_n_fr⁻¹)
+           ... = ⌊ifp_n_fr⁻¹⌋                    : by simp [‹int.fract ifp_n_fr⁻¹ = 0›]
 end
 
 end int_fract_pair