-- The square root of two is irrational
-- 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.NumberTheory.RootTwo
import Nat.Parity
import Nat.Least

-- The square of an odd number is odd.
theorem Odd.square (n : Set)
  requires odd : Odd(n)
  shows Odd(n * n)
proof
  obtain ⟨k, kMember, equation⟩ := odd
  have kNat := nat.omega.backward with kMember
  have m : Nat(add(add(mul(k, k), mul(k, k)), add(k, k))) by typecheck
  witness add(add(mul(k, k), mul(k, k)), add(k, k))
  constructor
  . exact nat.omega.forward at add(add(mul(k, k), mul(k, k)), add(k, k)) with m
  . rw equation
    ring

-- A number whose square is even is even.
theorem Even.of_square (n : Nat)
  requires even : Even(n * n)
  shows Even(n)
proof
  have shape := parity.exhaustive with *
  cases shape with evenN | oddN
  . exact evenN
  . exfalso
    have oddSquare := Odd.square with oddN
    exact Odd.not_even with *, even

-- The naturals p with p² = 2q² for some positive q.
def rootTwoNumerators : Set :=
  { p ∈ ℕ | ∃ q ∈ ℕ, q ≠ 0 ∧ p * p = 2 * (q * q) }

theorem rootTwoNumerators.subset_naturals
  shows rootTwoNumerators ⊆ ℕ
proof
  intros p member
  obtain ⟨natural, rest⟩ := rootTwoNumerators.membership.forward with member
  exact natural

-- From p² = 2q² with q positive, p is even, p = 2j, and then q² = 2j² with
-- j positive and q < p. So q is a smaller member of the same set.
theorem rootTwoNumerators.descent (p q : Nat)
  requires positive : q ≠ 0
  requires equation : p * p = 2 * (q * q)
  shows q ∈ rootTwoNumerators ∧ q < p
proof
  have evenSquare : Even(p * p)
    witness q * q
    constructor
    . have qq : Nat(q * q)
        typecheck
      exact nat.omega.forward with qq
    . rw equation
      exact mul.two_left with *
  have evenP := Even.of_square with *
  obtain ⟨j, jMember, pShape⟩ := evenP
  have jNat := nat.omega.backward with jMember
  have halved : q * q = 2 * (j * j)
    have doubled : 2 * (q * q) = 2 * (2 * (j * j))
      rw [← equation, pShape]
      simp [mul.two_left]
      ring
    have twoNonzero : 2 ≠ 0
      intro bad
      have positiveTwo : 0 < 2 by arith
      rw bad at positiveTwo
      exact Less.irreflexive with *, positiveTwo
    exact mul.left_cancel_positive with *
  have jPositive : j ≠ 0
    intro jZero
    rw jZero at halved
    have qq : q * q = 0
      rw halved
      compute
    have split := mul.eq_zero with *, qq
    cases split with left | right
    . exact positive with left
    . exact positive with right
  have smaller : q < p
    have shape := Less.trichotomy at q, p with *
    rcases shape with less | equal | greater
    . exact less
    . exfalso
      rw [equal, pShape] at halved
      have two := mul.two_left at j * j with *
      rw two at halved
      have expand : (j + j) * (j + j) = (j * j + j * j) + (j * j + j * j) by ring
      rw expand at halved
      have upper : j * j ≤ 0 by arith
      have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at j * j with *
      have jj := LessEqual.antisymmetric at j * j, 0 with *
      have split := mul.eq_zero with *, jj
      cases split with first | second
      . exact jPositive with first
      . exact jPositive with second
    . exfalso
      have le := Less.implies_LessEqual with *
      have first := LessEqual.mul_left at p, q, p with *
      have second := LessEqual.mul_left at p, q, q with *
      have commuted := mul.commutative at q, p with *
      have two := mul.two_left at q * q with *
      rw two at equation
      have upper : q * q ≤ 0 by arith
      have lower := Grace.Cumulus.Nat.Order.LessEqual.zero at q * q with *
      have zero := LessEqual.antisymmetric at q * q, 0 with *
      have split := mul.eq_zero with *, zero
      cases split with left | right
      . exact positive with left
      . exact positive with right
  constructor
  . apply rootTwoNumerators.membership.backward at q
    constructor
    . exact nat.omega.forward at q with assumption
    . witness j
      refine ⟨jMember, jPositive, halved⟩
  . exact smaller

-- No natural p and positive q satisfy p² = 2q²: the least such p would give
-- a smaller one.
theorem rootTwo.irrational (p q : Nat)
  requires positive : q ≠ 0
  shows p * p ≠ 2 * (q * q)
proof
  intro equation
  have member : p ∈ rootTwoNumerators
    apply rootTwoNumerators.membership.backward
    constructor
    . exact nat.omega.forward at p with assumption
    . witness q
      have qMember := nat.omega.forward at q with assumption
      refine ⟨qMember, positive, equation⟩
  have inhabited : Nonempty(rootTwoNumerators) := ⟨p, member⟩
  have naturals := rootTwoNumerators.subset_naturals
  have least := leastNatural.member at rootTwoNumerators with *
  obtain ⟨leastMember, r, rMember, rPositive, rEquation⟩ := rootTwoNumerators.membership.forward with least
  have leastNat := nat.omega.backward with leastMember
  have rNat := nat.omega.backward with rMember
  have descent := rootTwoNumerators.descent at leastNatural(rootTwoNumerators), r with *
  rcases descent with ⟨rIn, rSmaller⟩
  have bound := leastNatural.least at rootTwoNumerators, r with *
  have bad : r < r by arith
  exact Less.irreflexive with *, bad