refactor(data/real/irrational): review (#2304)

* refactor(data/real/irrational): review

* Update src/data/real/irrational.lean

* Update src/data/real/irrational.lean

* Apply suggestions from code review

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/real/irrational.lean

@@ -1,35 +1,53 @@
 /-
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne.
+Authors: Mario Carneiro, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Yury Kudryashov.
+-/
+import data.real.basic algebra.gcd_domain ring_theory.multiplicity tactic.alias
+/-!
+# Irrational real numbers
+
+In this file we define a predicate `irrational` on `ℝ`, prove that the `n`-th root of an integer
+number is irrational if it is not integer, and that `sqrt q` is irrational if and only if
+`rat.sqrt q * rat.sqrt q ≠ q ∧ 0 ≤ q`.
 
-Irrationality of real numbers.
+We also provide dot-style constructors like `irrational.add_rat`, `irrational.rat_sub` etc.
 -/
-import data.real.basic data.padics.padic_norm
 
 open rat real multiplicity
 
-def irrational (x : ℝ) := ¬ ∃ q : ℚ, x = q
+/-- A real number is irrational if it is not equal to any rational number. -/
+def irrational (x : ℝ) := x ∉ set.range (coe : ℚ → ℝ)
+
+/-!
+### Irrationality of roots of integer and rational numbers
+-/
 
-theorem irr_nrt_of_notint_nrt {x : ℝ} (n : ℕ) (m : ℤ)
+/-- If `x^n`, `n > 0`, is integer and is not the `n`-th power of an integer, then
+`x` is irrational. -/
+theorem irrational_nrt_of_notint_nrt {x : ℝ} (n : ℕ) (m : ℤ)
   (hxr : x ^ n = m) (hv : ¬ ∃ y : ℤ, x = y) (hnpos : 0 < n) :
-  irrational x
-| ⟨q, e⟩ := begin
-  rw [e, ← cast_pow] at hxr, cases q with N D P C,
+  irrational x :=
+begin
+  rintros ⟨⟨N, D, P, C⟩, rfl⟩,
+  rw [← cast_pow] at hxr,
   have c1 : ((D : ℤ) : ℝ) ≠ 0,
   { rw [int.cast_ne_zero, int.coe_nat_ne_zero], exact ne_of_gt P },
   have c2 : ((D : ℤ) : ℝ) ^ n ≠ 0 := pow_ne_zero _ c1,
   rw [num_denom', cast_pow, cast_mk, div_pow, div_eq_iff_mul_eq c2,
       ← int.cast_pow, ← int.cast_pow, ← int.cast_mul, int.cast_inj] at hxr,
   have hdivn : ↑D ^ n ∣ N ^ n := dvd.intro_left m hxr,
-  rw [← int.dvd_nat_abs, ← int.coe_nat_pow, int.coe_nat_dvd, int.nat_abs_pow, nat.pow_dvd_pow_iff hnpos] at hdivn,
-  have hdivn' : nat.gcd N.nat_abs D = D := nat.gcd_eq_right hdivn,
+  rw [← int.dvd_nat_abs, ← int.coe_nat_pow, int.coe_nat_dvd, int.nat_abs_pow,
+    nat.pow_dvd_pow_iff hnpos] at hdivn,
+  have hD : D = 1 := by rw [← nat.gcd_eq_right hdivn, C.gcd_eq_one],
+  subst D,
   refine hv ⟨N, _⟩,
-  rwa [num_denom', ← hdivn', C.gcd_eq_one, int.coe_nat_one, mk_eq_div,
-      int.cast_one, div_one, cast_coe_int] at e
+  rw [num_denom', int.coe_nat_one, mk_eq_div, int.cast_one, div_one, cast_coe_int]
 end
 
-theorem irr_nrt_of_n_not_dvd_multiplicity {x : ℝ} (n : ℕ) {m : ℤ} (hm : m ≠ 0) (p : ℕ)
+/-- If `x^n = m` is an integer and `n` does not divide the `multiplicity p m`, then `x`
+is irrational. -/
+theorem irrational_nrt_of_n_not_dvd_multiplicity {x : ℝ} (n : ℕ) {m : ℤ} (hm : m ≠ 0) (p : ℕ)
   [hp : nat.prime p] (hxr : x ^ n = m)
   (hv : (multiplicity (p : ℤ) m).get (finite_int_iff.2 ⟨hp.ne_one, hm⟩) % n ≠ 0) :
   irrational x :=
@@ -38,7 +56,7 @@ begin
   { rw [eq_comm, pow_zero, ← int.cast_one, int.cast_inj] at hxr,
     simpa [hxr, multiplicity.one_right (mt is_unit_iff_dvd_one.1
       (mt int.coe_nat_dvd.1 hp.not_dvd_one)), nat.zero_mod] using hv },
-  refine irr_nrt_of_notint_nrt _ _ hxr _ hnpos,
+  refine irrational_nrt_of_notint_nrt _ _ hxr _ hnpos,
   rintro ⟨y, rfl⟩,
   rw [← int.cast_pow, int.cast_inj] at hxr, subst m,
   have : y ≠ 0, { rintro rfl, rw zero_pow hnpos at hm, exact hm rfl },
@@ -47,58 +65,158 @@ begin
   exact hv rfl
 end
 
-theorem irr_sqrt_of_multiplicity_odd (m : ℤ) (hm : 0 < m)
+theorem irrational_sqrt_of_multiplicity_odd (m : ℤ) (hm : 0 < m)
   (p : ℕ) [hp : nat.prime p]
-  (Hpv : (multiplicity (p : ℤ) m).get (finite_int_iff.2 ⟨hp.ne_one, ne.symm (ne_of_lt hm)⟩) % 2 = 1) :
+  (Hpv : (multiplicity (p : ℤ) m).get (finite_int_iff.2 ⟨hp.ne_one, (ne_of_lt hm).symm⟩) % 2 = 1) :
   irrational (sqrt m) :=
-irr_nrt_of_n_not_dvd_multiplicity 2 (ne.symm (ne_of_lt hm)) p
+@irrational_nrt_of_n_not_dvd_multiplicity _ 2 _ (ne.symm (ne_of_lt hm)) p hp
   (sqr_sqrt (int.cast_nonneg.2 $ le_of_lt hm))
   (by rw Hpv; exact one_ne_zero)
 
-theorem irr_sqrt_of_prime (p : ℕ) (hp : nat.prime p) : irrational (sqrt p) :=
-irr_sqrt_of_multiplicity_odd p (int.coe_nat_pos.2 hp.pos) p $
+theorem nat.prime.irrational_sqrt {p : ℕ} (hp : nat.prime p) : irrational (sqrt p) :=
+@irrational_sqrt_of_multiplicity_odd p (int.coe_nat_pos.2 hp.pos) p hp $
 by simp [multiplicity_self (mt is_unit_iff_dvd_one.1 (mt int.coe_nat_dvd.1 hp.not_dvd_one) : _)];
   refl
 
-theorem irr_sqrt_two : irrational (sqrt 2) :=
-by simpa using irr_sqrt_of_prime 2 nat.prime_two
+theorem irrational_sqrt_two : irrational (sqrt 2) :=
+by simpa using nat.prime_two.irrational_sqrt
 
-theorem irr_sqrt_rat_iff (q : ℚ) : irrational (sqrt q) ↔
+theorem irrational_sqrt_rat_iff (q : ℚ) : irrational (sqrt q) ↔
   rat.sqrt q * rat.sqrt q ≠ q ∧ 0 ≤ q :=
 if H1 : rat.sqrt q * rat.sqrt q = q
 then iff_of_false (not_not_intro ⟨rat.sqrt q,
   by rw [← H1, cast_mul, sqrt_mul_self (cast_nonneg.2 $ rat.sqrt_nonneg q),
          sqrt_eq, abs_of_nonneg (rat.sqrt_nonneg q)]⟩) (λ h, h.1 H1)
 else if H2 : 0 ≤ q
 then iff_of_true (λ ⟨r, hr⟩, H1 $ (exists_mul_self _).1 ⟨r,
-  by rwa [sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul, cast_inj] at hr;
+  by rwa [eq_comm, sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul, cast_inj] at hr;
   rw [← hr]; exact real.sqrt_nonneg _⟩) ⟨H1, H2⟩
 else iff_of_false (not_not_intro ⟨0,
-  by rw cast_zero; exact sqrt_eq_zero_of_nonpos (rat.cast_nonpos.2 $ le_of_not_le H2)⟩)
+  by rw cast_zero; exact (sqrt_eq_zero_of_nonpos (rat.cast_nonpos.2 $ le_of_not_le H2)).symm⟩)
   (λ h, H2 h.2)
 
 instance (q : ℚ) : decidable (irrational (sqrt q)) :=
-decidable_of_iff' _ (irr_sqrt_rat_iff q)
+decidable_of_iff' _ (irrational_sqrt_rat_iff q)
+
+/-!
+### Adding/subtracting/multiplying by rational numbers
+-/
+
+lemma rat.not_irrational (q : ℚ) : ¬irrational q := λ h, h ⟨q, rfl⟩
+
+namespace irrational
+
+variables (q : ℚ) {x y : ℝ}
+
+open_locale classical
+
+theorem add_cases : irrational (x + y) → irrational x ∨ irrational y :=
+begin
+  delta irrational,
+  contrapose!,
+  rintros ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩,
+  exact ⟨rx + ry, cast_add rx ry⟩
+end
+
+theorem of_rat_add (h : irrational (q + x)) : irrational x :=
+h.add_cases.elim (λ h, absurd h q.not_irrational) id
+
+theorem rat_add (h : irrational x) : irrational (q + x) :=
+of_rat_add (-q) $ by rwa [cast_neg, neg_add_cancel_left]
+
+theorem of_add_rat : irrational (x + q) → irrational x :=
+add_comm ↑q x ▸ of_rat_add q
+
+theorem add_rat (h : irrational x) : irrational (x + q) :=
+add_comm ↑q x ▸ h.rat_add q
+
+theorem of_neg (h : irrational (-x)) : irrational x :=
+λ ⟨q, hx⟩, h ⟨-q, by rw [cast_neg, hx]⟩
+
+protected theorem neg (h : irrational x) : irrational (-x) :=
+of_neg $ by rwa neg_neg
+
+theorem sub_rat (h : irrational x) : irrational (x - q) :=
+by simpa only [cast_neg] using h.add_rat (-q)
 
+theorem rat_sub (h : irrational x) : irrational (q - x) :=
+h.neg.rat_add q
+
+theorem of_sub_rat (h : irrational (x - q)) : irrational x :=
+of_add_rat (-q) $ by simpa only [cast_neg]
+
+theorem of_rat_sub (h : irrational (q - x)) : irrational x :=
+(h.of_rat_add _).of_neg
+
+theorem mul_cases : irrational (x * y) → irrational x ∨ irrational y :=
+begin
+  delta irrational,
+  contrapose!,
+  rintros ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩,
+  exact ⟨rx * ry, cast_mul rx ry⟩
+end
+
+theorem of_mul_rat (h : irrational (x * q)) : irrational x :=
+h.mul_cases.elim id (λ h, absurd h q.not_irrational)
+
+theorem mul_rat (h : irrational x) {q : ℚ} (hq : q ≠ 0) : irrational (x * q) :=
+of_mul_rat q⁻¹ $ by rwa [mul_assoc, ← cast_mul, mul_inv_cancel hq, cast_one, mul_one]
+
+theorem of_rat_mul : irrational (q * x) → irrational x :=
+mul_comm x q ▸ of_mul_rat q
+
+theorem rat_mul (h : irrational x) {q : ℚ} (hq : q ≠ 0) : irrational (q * x) :=
+mul_comm x q ▸ h.mul_rat hq
+
+theorem of_mul_self (h : irrational (x * x)) : irrational x :=
+h.mul_cases.elim id id
+
+theorem of_inv (h : irrational x⁻¹) : irrational x :=
+λ ⟨q, hq⟩, h $ hq ▸ ⟨q⁻¹, q.cast_inv⟩
+
+protected theorem inv (h : irrational x) : irrational x⁻¹ :=
+of_inv $ by rwa inv_inv'
+
+theorem div_cases (h : irrational (x / y)) : irrational x ∨ irrational y :=
+h.mul_cases.imp id of_inv
+
+theorem of_rat_div (h : irrational (q / x)) : irrational x :=
+(h.of_rat_mul q).of_inv
+
+theorem of_one_div (h : irrational (1 / x)) : irrational x :=
+of_rat_div 1 $ by rwa [cast_one]
+
+theorem of_pow : ∀ n : ℕ, irrational (x^n) → irrational x
+| 0 := λ h, (h ⟨1, cast_one⟩).elim
+| (n+1) := λ h, h.mul_cases.elim id (of_pow n)
+
+theorem of_fpow : ∀ m : ℤ, irrational (x^m) → irrational x
+| (n:ℕ) := of_pow n
+| -[1+n] := λ h, h.of_one_div.of_pow _
+
+end irrational
+
+section
 variables {q : ℚ} {x : ℝ}
 
-theorem irr_rat_add_of_irr : irrational x → irrational (q + x) :=
-mt $ λ ⟨a, h⟩, ⟨-q + a, by rw [rat.cast_add, ← h, rat.cast_neg, neg_add_cancel_left]⟩
+open irrational
+
+@[simp] theorem irrational_rat_add_iff : irrational (q + x) ↔ irrational x :=
+⟨of_rat_add q, rat_add q⟩
 
-@[simp] theorem irr_rat_add_iff_irr : irrational (q + x) ↔ irrational x :=
-⟨by simpa only [cast_neg, neg_add_cancel_left] using @irr_rat_add_of_irr (-q) (q+x),
-irr_rat_add_of_irr⟩
+@[simp] theorem irrational_add_rat_iff : irrational (x + q) ↔ irrational x :=
+⟨of_add_rat q, add_rat q⟩
 
-@[simp] theorem irr_add_rat_iff_irr : irrational (x + q) ↔ irrational x :=
-by rw [add_comm, irr_rat_add_iff_irr]
+@[simp] theorem irrational_rat_sub_iff : irrational (q - x) ↔ irrational x :=
+⟨of_rat_sub q, rat_sub q⟩
 
-theorem irr_mul_rat_iff_irr (Hqn0 : q ≠ 0) : irrational (x * ↑q) ↔ irrational x :=
-⟨mt $ λ ⟨r, hr⟩, ⟨r * q, hr.symm ▸ (rat.cast_mul _ _).symm⟩,
-mt $ λ ⟨r, hr⟩, ⟨r / q, by rw [cast_div, ← hr, mul_div_cancel]; rwa cast_ne_zero⟩⟩
+@[simp] theorem irrational_sub_rat_iff : irrational (x - q) ↔ irrational x :=
+⟨of_sub_rat q, sub_rat q⟩
 
-theorem irr_of_irr_mul_self : irrational (x * x) → irrational x :=
-mt $ λ ⟨p, e⟩, ⟨p * p, by rw [e, cast_mul]⟩
+@[simp] theorem irrational_neg_iff : irrational (-x) ↔ irrational x :=
+⟨of_neg, irrational.neg⟩
 
-@[simp] theorem irr_neg : irrational (-x) ↔ irrational x :=
-⟨λ hn ⟨q, hx⟩, hn ⟨-q, by rw [hx, cast_neg]⟩,
- λ hx ⟨q, hn⟩, hx ⟨-q, by rw [←neg_neg x, hn, cast_neg]⟩⟩
+@[simp] theorem irrational_inv_iff : irrational x⁻¹ ↔ irrational x :=
+⟨of_inv, irrational.inv⟩
+
+end