-- The real square root of two is not a quotient of natural numbers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.RootTwo
import Sqrt
import Natural
import NumberTheory.RootTwo

theorem realNat.nonnegative (n : Nat)
  shows (0:R) ≤ realNat(n)
proof
  induction n
  | zero =>
    rw realNat.zero
    linarith
  | succ(k) using ih =>
    rw realNat.succ
    have one := realZero.lt_one
    linarith

theorem realNat.lt_of_lt (m n : Nat)
  requires less : m < n
  shows realNat(m) < realNat(n)
proof
  obtain ⟨k, kNat, equation⟩ := less
  rw [← equation, realNat.add, realNat.succ]
  have nonnegativeK := realNat.nonnegative at k with *
  have one := realZero.lt_one
  linarith

theorem realNat.injective (m n : Nat)
  requires equal : realNat(m) = realNat(n)
  shows m = n
proof
  have shape := Less.trichotomy at m, n with *
  rcases shape with less | same | greater
  . exfalso
    have strict := realNat.lt_of_lt with *
    rw equal at strict
    exact realLess.not_self with *, strict
  . exact same
  . exfalso
    have strict := realNat.lt_of_lt with *
    rw equal at strict
    exact realLess.not_self with *, strict

theorem realNat.nonzero (n : Nat)
  requires nonzero : n ≠ 0
  shows realNat(n) ≠ (0:R)
proof
  intro zero
  rw ← realNat.zero at zero
  have equal := realNat.injective at n, 0 with *
  exact nonzero with equal

theorem realNat.two
  shows realNat(2) = (2:R)
proof
  rw [realNat.succ, realNat.one]
  ring

-- The real number √2 is not p/q for any naturals p and q. Since √2 is
-- positive, that rules out every rational.
theorem sqrtTwo.ne_quotient (p q : Nat)
  requires positive : q ≠ 0
  shows √2 ≠ realNat(p) / realNat(q)
proof
  intro equation
  have qNonzero := realNat.nonzero with *
  have one := realZero.lt_one
  have twoLe : (0:R) ≤ (2:R) by linarith
  have twoNonnegative := NonnegativeReal.of_le with *
  have square := sqrt.square with *
  have scaled : √(2:R) * realNat(q) = realNat(p)
    rw equation
    exact realDiv.mul_right with *
  have squares : (√(2:R) * realNat(q)) * (√(2:R) * realNat(q)) = realNat(p) * realNat(p)
    rw scaled
    rfl
  have expand : (√(2:R) * realNat(q)) * (√(2:R) * realNat(q)) = (√(2:R) * √(2:R)) * (realNat(q) * realNat(q))
    ring
  rw [expand, square] at squares
  have left : realNat(2 * (q * q)) = (2:R) * (realNat(q) * realNat(q))
    rw [realNat.mul, realNat.mul, realNat.two]
    rfl
  have right : realNat(p * p) = realNat(p) * realNat(p)
    exact realNat.mul with *
  have natural : realNat(2 * (q * q)) = realNat(p * p) by rwa [left, right]
  have equalNaturals := realNat.injective with *
  have contradiction := rootTwo.irrational at p, q with *
  symm at equalNaturals
  exact contradiction with equalNaturals