Sqrt 2 by trigott

module Theorem where

open import Data.Nat
open import Data.Nat.Properties
-- open import Data.Nat.Properties.Simple
open import Data.Nat.Divisibility
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Induction.Nat
open import Relation.Binary.PropositionalEquality
open import Function
open SemiringSolver

-- Data.Nat.Properties.Simple

+-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
+-assoc zero    _ _ = refl
+-assoc (suc m) n o = cong suc $ +-assoc m n o

+-right-identity : ∀ n → n + 0 ≡ n
+-right-identity zero = refl
+-right-identity (suc n) = cong suc $ +-right-identity n

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm zero    n = sym $ +-right-identity n
+-comm (suc m) n =
  begin
    suc m + n
  ≡⟨ refl ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨ sym (+-suc n m) ⟩
    n + suc m
  ∎
  where open ≡-Reasoning

+-*-suc : ∀ m n → m * suc n ≡ m + m * n
+-*-suc zero    n = refl
+-*-suc (suc m) n =
  begin
    suc m * suc n
  ≡⟨ refl ⟩
    suc n + m * suc n
  ≡⟨ cong (λ x → suc n + x) (+-*-suc m n) ⟩
    suc n + (m + m * n)
  ≡⟨ refl ⟩
    suc (n + (m + m * n))
  ≡⟨ cong suc (sym $ +-assoc n m (m * n)) ⟩
    suc (n + m + m * n)
  ≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
    suc (m + n + m * n)
  ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
    suc (m + (n + m * n))
  ≡⟨ refl ⟩
    suc m + suc m * n
  ∎
  where open ≡-Reasoning

*-right-zero : ∀ n → n * 0 ≡ 0
*-right-zero zero = refl
*-right-zero (suc n) = *-right-zero n

*-comm : ∀ m n → m * n ≡ n * m
*-comm zero    n = sym $ *-right-zero n
*-comm (suc m) n =
  begin
    suc m * n
  ≡⟨ refl ⟩
    n + m * n
  ≡⟨ cong (λ x → n + x) (*-comm m n) ⟩
    n + n * m
  ≡⟨ sym (+-*-suc n m) ⟩
    n * suc m
  ∎
  where open ≡-Reasoning

distribʳ-*-+ : ∀ m n o → (n + o) * m ≡ n * m + o * m
distribʳ-*-+ m zero    o = refl
distribʳ-*-+ m (suc n) o =
  begin
    (suc n + o) * m
  ≡⟨ refl ⟩
    m + (n + o) * m
  ≡⟨ cong (_+_ m) $ distribʳ-*-+ m n o ⟩
    m + (n * m + o * m)
  ≡⟨ sym $ +-assoc m (n * m) (o * m) ⟩
    m + n * m + o * m
  ≡⟨ refl ⟩
    suc n * m + o * m
  ∎
  where open ≡-Reasoning

*-assoc : ∀ m n o → (m * n) * o ≡ m * (n * o)
*-assoc zero    n o = refl
*-assoc (suc m) n o =
  begin
    (suc m * n) * o
  ≡⟨ refl ⟩
    (n + m * n) * o
  ≡⟨ distribʳ-*-+ o n (m * n) ⟩
    n * o + (m * n) * o
  ≡⟨ cong (λ x → n * o + x) $ *-assoc m n o ⟩
    n * o + m * (n * o)
  ≡⟨ refl ⟩
    suc m * (n * o)
  ∎
  where open ≡-Reasoning

--

∣-∸ʳ : ∀ {i m n} → i ∣ m + n → i ∣ n → i ∣ m
∣-∸ʳ {i} {m} {n} d+ d rewrite +-comm m n = ∣-∸ d+ d

∣-mid : ∀ {k} a b → k ∣ a * k * b
∣-mid {k} a b rewrite *-assoc a k b
                    | *-comm k b
                    | sym $ *-assoc a b k = ∣-* (a * b)

remove-1+ : ∀ {x y} → suc x ≡ suc y → x ≡ y
remove-1+ refl = refl

remove-k+ : ∀ {x y} k → k + x ≡ k + y → x ≡ y
remove-k+ zero    eq = eq
remove-k+ (suc k) eq = remove-k+ k (remove-1+ eq)

remove-*1+k : ∀ {x y} k → x * (suc k) ≡ y * (suc k) → x ≡ y
remove-*1+k {zero}  {zero}  k eq = refl
remove-*1+k {zero}  {suc y} k ()
remove-*1+k {suc x} {zero}  k ()
remove-*1+k {suc x} {suc y} k eq = cong suc $ remove-*1+k k (remove-k+ (1 + k) eq)

data Parity : ℕ → Set where
  even : (k : ℕ) → Parity (k * 2)
  odd  : (k : ℕ) → Parity (1 + k * 2)

parity : (n : ℕ) → Parity n
parity zero = even zero
parity (suc n) with parity n
parity (suc ._) | even k = odd k
parity (suc ._) | odd  k = even (suc k)

trivial₆ : ∀ k → 2 ∣ suc (suc (k * 2 + k * 2 * suc (k * 2)))
trivial₆ k = ∣-+ (∣-+ (divides 1 refl) (∣-* k)) (∣-mid k (1 + k * 2))

parity² : (n : ℕ) → 2 ∣ n * n ⊎ 2 ∣ 1 + n * n
parity² n with parity n
parity² .(k * 2) | even k
  rewrite sym $ *-assoc (k * 2) k 2 = inj₁ (divides (k * 2 * k) refl)
parity² .(suc (k * 2)) | odd k = inj₂ (trivial₆ k)

trivial₇ : ∀ k → 2 ∣ suc (k * 2 + k * 2 * suc (k * 2)) → 2 ∣ 1
trivial₇ k div = ∣-∸ʳ div (∣-+ (∣-* k) (∣-mid k (1 + k * 2)))

¬2∣1 : 2 ∣ 1 → ⊥
¬2∣1 (divides zero    ())
¬2∣1 (divides (suc _) ())

trivial₅ : ∀ n → 2 ∣ n * n → 2 ∣ n
trivial₅ n div with parity n
trivial₅ .(k * 2)     div | even k = divides k refl
trivial₅ .(1 + k * 2) div | odd  k = ⊥-elim $ ¬2∣1 (trivial₇ k div)

lem-n : ∀ n m → n * n ≡ m * m * 2 → 2 ∣ n
lem-n n m eq with parity² n
lem-n n m eq | inj₁ x = trivial₅ n x
lem-n n m eq | inj₂ y = ⊥-elim $ ¬2∣1 (∣-∸ʳ {m = 1} y (divides (m * m) eq))

trivial₈ : ∀ q m → q * 2 * (q * 2) ≡ m * m * 2 → q * q * 2 ≡ m * m
trivial₈ q m eq rewrite *-assoc q 2 (q * 2)
                      | *-comm 2 (q * 2)
                      | sym $ *-assoc q (q * 2) 2
                      | sym $ *-assoc q q 2
                      = remove-*1+k 1 eq

lemma : ∀ n m → n * n ≡ m * m * 2 → 2 ∣ n × 2 ∣ m
lemma n m d with lem-n n m d
lemma n m d | divides q eq rewrite eq = divides q refl , trivial₅ m (divides (q * q) (sym $ trivial₈ q m d))

1+n≢0 : ∀ {n} → 1 + n ≡ 0 → ⊥
1+n≢0 ()

1+n≤′1+m : ∀ {n m} → n ≤′ m → suc n ≤′ suc m
1+n≤′1+m ≤′-refl        = ≤′-refl
1+n≤′1+m (≤′-step n≤′m) = ≤′-step (1+n≤′1+m n≤′m)

k+n≤′k+m : ∀ {n m} k → n ≤′ m → k + n ≤′ k + m
k+n≤′k+m zero    n≤′m = n≤′m
k+n≤′k+m (suc k) n≤′m = 1+n≤′1+m (k+n≤′k+m k n≤′m)

n≤′k+n : ∀ {n} k → n ≤′ k + n
n≤′k+n zero    = ≤′-refl
n≤′k+n (suc k) = ≤′-step (n≤′k+n k)

n*1≡n : ∀ n → n * 1 ≡ n
n*1≡n n rewrite *-comm n 1 | +-comm n 0 = refl

≡-suc : ∀ {n m} → suc n ≡ suc m → n ≡ m
≡-suc refl = refl

≡-k+ : ∀ {n m} k → k + n ≡ k + m → n ≡ m
≡-k+ zero    eq = eq
≡-k+ (suc k) eq = ≡-k+ k (≡-suc eq)

≡-div : ∀ {n m} k → n * (suc k) ≡ m * (suc k) → n ≡ m
≡-div {zero}  {zero}  k eq = refl
≡-div {zero}  {suc m} k ()
≡-div {suc n} {zero}  k ()
≡-div {suc n} {suc m} k eq = cong suc $ ≡-div k (≡-k+ (suc k) eq)

trivial₁ : ∀ n p → suc n ≡ p * 2 → suc p ≤′ suc n
trivial₁ n zero ()
trivial₁ n (suc p) eq rewrite eq
                            | *-comm p 2
                            | +-comm p 0 = k+n≤′k+m 2 (n≤′k+n p)

trivial₂ : ∀ p → p * 2 * (p * 2) ≡ (p * p) * 4
trivial₂ = solve 1 (λ p → p :* con 2 :* (p :* con 2) := p :* p :* con 4) refl

trivial₃ : ∀ q → q * 2 * (q * 2) * 2 ≡ (q * q * 2) * 4
trivial₃ = solve 1 (λ q → q :* con 2 :* (q :* con 2) :* con 2 := q :* q :* con 2 :* con 4) refl

trivial₄ : ∀ (n m p q : ℕ)
           → (eq₁ : n ≡ p * 2) (eq₂ : m ≡ q * 2)
           → n * n ≡ m * m * 2
           → p * p ≡ q * q * 2
trivial₄ n m p q eq₁ eq₂ hyp rewrite eq₁ | eq₂ | trivial₂ p | trivial₃ q = ≡-div 3 hyp

sqrt2-step : (n : ℕ)
             → (rec : (x : ℕ) (x<n : x <′ n)
                      → (y : ℕ) (hyp : x * x ≡ y * y * 2)
                      → x ≡ 0 × y ≡ 0)
             → (m : ℕ) (hyp : n * n ≡ m * m * 2)
             → n ≡ 0 × m ≡ 0
sqrt2-step zero    _   zero    _ = refl , refl
sqrt2-step zero    _   (suc _) ()
sqrt2-step (suc n) rec zero    ()
sqrt2-step (suc n) rec (suc m) hyp with lemma (suc n) (suc m) hyp
... | divides p eq₁ , divides q eq₂ with rec p (trivial₁ n p eq₁) q
                                             (trivial₄ (suc n) (suc m) p q eq₁ eq₂ hyp)
... | u , v rewrite u = ⊥-elim (1+n≢0 eq₁)

sqrt2′ : (n m : ℕ) → n * n ≡ m * m * 2 → n ≡ 0 × m ≡ 0
sqrt2′ = <-rec _ sqrt2-step

sqrt2 : (n m : ℕ) → n * n ≡ 2 * m * m → m ≡ 0
sqrt2 n m eq rewrite *-assoc 2 m m
                   | *-comm 2 (m * m)
                   = proj₂ (sqrt2′ n m eq)