Sqrt 2 by notogawa

module Theorem where

open import Function
open import Data.Nat
open import Data.Nat.Properties
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; _≢_; refl; cong; sym; subst)
import Induction.WellFounded as WF
open import Induction.Nat
open import Data.Sum
open import Data.Product hiding (map)
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-assoc; +-comm; *-assoc; *-comm)
open import Data.Empty
open SemiringSolver

n≡2*k⊎n≡1+2*k : (n : ℕ) → ∃ λ k → n ≡ 2 * k ⊎ n ≡ 1 + 2 * k
n≡2*k⊎n≡1+2*k 0 = 0 , inj₁ refl
n≡2*k⊎n≡1+2*k 1 = 0 , inj₂ refl
n≡2*k⊎n≡1+2*k (suc (suc n)) with n≡2*k⊎n≡1+2*k n
n≡2*k⊎n≡1+2*k (suc (suc n)) | k , x = suc k , map (lemma 0) (lemma 1) x
  where
    lemma : ∀ x → n ≡ x + 2 * k → suc (suc n) ≡ x + 2 * suc k
    lemma x n≡x+2*k
      rewrite n≡x+2*k
            = solve 2 (λ x₁ k₁ →
                           con 1 :+ (con 1 :+ (x₁ :+ con 2 :* k₁)) :=
                           x₁ :+ con 2 :* (con 1 :+ k₁)) refl x k

m≤′n⊎n<′m : ∀ m n → m ≤′ n ⊎ n <′ m
m≤′n⊎n<′m zero zero = inj₁ ≤′-refl
m≤′n⊎n<′m zero (suc n) = inj₁ (≤⇒≤′ z≤n)
m≤′n⊎n<′m (suc m) zero = inj₂ (≤⇒≤′ (s≤s z≤n))
m≤′n⊎n<′m (suc m) (suc n) = map s≤′s s≤′s (m≤′n⊎n<′m m n)

2*n≤n→n≡0 : ∀ n → 2 * n ≤ n → n ≡ 0
2*n≤n→n≡0 n 2*n≤n with ∸-mono {u = n} {v = n} 2*n≤n (≤′⇒≤ ≤′-refl)
... | n≤z
  rewrite +-comm n 0
        | +-∸-assoc n {n} {n} (≤′⇒≤ ≤′-refl)
        | n∸n≡0 n
        | +-comm n 0
        = antisym n≤z z≤n
  where
    open import Relation.Binary
    open DecTotalOrder decTotalOrder

n*n≡0→n≡0 : ∀ n → n * n ≡ 0 → n ≡ 0
n*n≡0→n≡0 n = [ id , id ]′ ∘ i*j≡0⇒i≡0∨j≡0 n

n*n≡2*m*m→n*n≤m*m→n≡0×m≡0 : ∀ n m → n * n ≡ 2 * m * m → n * n ≤ m * m → n ≡ 0 × m ≡ 0
n*n≡2*m*m→n*n≤m*m→n≡0×m≡0 n m n*n≡2*m*m n*n≤m*m
  rewrite n*n≡2*m*m
        | *-assoc 2 m m
        | n*n≡0→n≡0 m (2*n≤n→n≡0 (m * m) n*n≤m*m)
        | n*n≡0→n≡0 n n*n≡2*m*m
        = refl , refl

n*n≡2*m*m→n≡0×m≡0⊎m<′n : ∀ n m → n * n ≡ 2 * m * m → (n ≡ 0 × m ≡ 0) ⊎ m <′ n
n*n≡2*m*m→n≡0×m≡0⊎m<′n n m n*n≡2*m*m
  = map (λ x → n*n≡2*m*m→n*n≤m*m→n≡0×m≡0 n m n*n≡2*m*m (≤′⇒≤ x *-mono ≤′⇒≤ x)) id (m≤′n⊎n<′m n m)

1+2*i≢2*j : ∀ i j → suc (2 * i) ≢ 2 * j
1+2*i≢2*j i zero ()
1+2*i≢2*j i (suc j) 1+2*i≡2*j
  rewrite solve 1 (λ j → j :+ (con 1 :+ (j :+ con 0)) := con 1 :+ con 2 :* j) refl j
        = 1+2*i≢2*j j i (sym (cong pred 1+2*i≡2*j))

sqrt2-is-irrational : ℕ → Set
sqrt2-is-irrational n = ∀ m → n * n ≡ 2 * m * m → n ≡ 0 × m ≡ 0

sqrt2-lemma : ∀ n → sqrt2-is-irrational n
sqrt2-lemma = <-rec sqrt2-is-irrational sqrt2-wf
  where
    open WF.All <-well-founded
    sqrt2-wf : ∀ n → <-Rec sqrt2-is-irrational n → sqrt2-is-irrational n
    sqrt2-wf n rec m n*n≡2*m*m with n≡2*k⊎n≡1+2*k n
    sqrt2-wf n rec m n*n≡2*m*m | k , inj₁ n≡2*k with n*n≡2*m*m→n≡0×m≡0⊎m<′n n m n*n≡2*m*m
    sqrt2-wf n rec m n*n≡2*m*m | k , inj₁ n≡2*k | inj₁ n≡0×m≡0 = n≡0×m≡0
    sqrt2-wf n rec m n*n≡2*m*m | k , inj₁ n≡2*k | inj₂ m<′n = n≡0 , m≡0
      where
        n*n≡2*m*m→m≡0×k≡0 : n * n ≡ 2 * m * m → m ≡ 0 × k ≡ 0
        n*n≡2*m*m→m≡0×k≡0 n*n≡2*m*m
          rewrite n≡2*k
                | solve 1 (λ k → (con 2 :* k) :* (con 2 :* k) := (con 2 :* k :* k) :* con 2) refl k
                | solve 1 (λ m → con 2 :* m :* m := m :* m :* con 2) refl m
                = rec m m<′n k (sym (cancel-*-right (2 * k * k) (m * m) n*n≡2*m*m))
        m≡0×k≡0 = n*n≡2*m*m→m≡0×k≡0 n*n≡2*m*m
        n≡0 = subst (λ x → n ≡ 2 * x) (proj₂ m≡0×k≡0) n≡2*k
        m≡0 = proj₁ m≡0×k≡0
    sqrt2-wf n rec m n*n≡2*m*m | k , inj₂ n≡1+2*k
      rewrite n≡1+2*k
            | solve 1 (λ k → (con 1 :+ con 2 :* k) :* (con 1 :+ con 2 :* k) := con 1 :+ con 2 :* (con 2 :* k :+ con 2 :* k :* k)) refl k
            | solve 1 (λ m → con 2 :* m :* m := con 2 :* (m :* m)) refl m
            = ⊥-elim (1+2*i≢2*j (2 * k + 2 * k * k) (m * m) n*n≡2*m*m)

sqrt2 : (n m : ℕ) → n * n ≡ 2 * m * m → m ≡ 0
sqrt2 n m = proj₂ ∘ sqrt2-lemma n m