Square 2 is irrational

sqrt2.agda

{- agda 2.6.0.1, stdlib v1.1 -}
open import Data.Nat renaming (_*_ to _*ℕ_; _+_ to _+ℕ_; suc to sucℕ)
open import Data.Nat.Properties
open import Data.Nat.Coprimality renaming (sym to coprime-sym)
open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Integer renaming (_*_ to _*ℤ_)
open import Data.Product
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

data Even : ℕ → Set where
  evenZero : Even 0
  even+2 : ∀ {n} → Even n → Even (sucℕ (sucℕ n))

DecEven : ∀ a → Dec (Even a)
DecEven zero = yes evenZero
DecEven (sucℕ zero) = no (λ ())
DecEven (sucℕ (sucℕ a)) with DecEven a
DecEven (sucℕ (sucℕ a)) | yes p = yes (even+2 p)
DecEven (sucℕ (sucℕ a)) | no ¬p = no (λ { (even+2 x) → ⊥-elim (¬p x) })


a≡2*b-even : ∀ a b → a ≡ 2 *ℕ b → Even a
a≡2*b-even zero b p = evenZero
a≡2*b-even (sucℕ zero) b p rewrite +-identityʳ b = ⊥-elim (lem {b} p)
  where
    lem : ∀ {b} → ¬ 1 ≡ b +ℕ b
    lem {sucℕ zero} ()
    lem {sucℕ (sucℕ b)} ()
a≡2*b-even (sucℕ (sucℕ a)) (sucℕ b) p rewrite +-comm b (sucℕ (b +ℕ zero))
                                             | +-identityʳ b = even+2 (a≡2*b-even a b (subst (λ x → a ≡ b +ℕ x)
                                                                                         (sym (+-identityʳ b)) (suc-injective (suc-injective p))))


even-a≡2*b : ∀ a → Even a → ∃ (λ b → a ≡ 2 *ℕ b)
even-a≡2*b .0 evenZero = zero , refl
even-a≡2*b (sucℕ (sucℕ n)) (even+2 ev) with even-a≡2*b n ev
even-a≡2*b (sucℕ (sucℕ n)) (even+2 ev) | fst , refl rewrite +-identityʳ fst = (sucℕ fst) , lem
  where
   lem : sucℕ (sucℕ (fst +ℕ fst)) ≡ sucℕ (fst +ℕ sucℕ (fst +ℕ 0))
   lem rewrite +-identityʳ fst
             | +-comm fst (sucℕ fst) = refl

neg-even-inj : ∀ z → ¬ Even (sucℕ (sucℕ z)) → ¬ Even z
neg-even-inj z neg = λ x → neg (even+2 x)

Even-decomp : ∀ a b → Even (a +ℕ b) → Even a → Even b
Even-decomp zero b ev evb = ev
Even-decomp (sucℕ (sucℕ a)) b (even+2 ev) (even+2 evb) = Even-decomp a b ev evb

evenAdd : ∀ a → Even (a +ℕ a)
evenAdd zero = evenZero
evenAdd (sucℕ z) rewrite +-comm z (sucℕ z) = even+2 (evenAdd z)

¬Even-z-¬Even-z*z : ∀ z → ¬ Even z → ¬ Even (z *ℕ z)
¬Even-z-¬Even-z*z zero neqev ev = neqev ev
¬Even-z-¬Even-z*z (sucℕ (sucℕ z)) neqev (even+2 ev) rewrite +-comm z (sucℕ (sucℕ (z +ℕ z *ℕ sucℕ (sucℕ z))))
                                                           | *-comm z (sucℕ (sucℕ z)) = lem ev
  where
    lem : Even (sucℕ (sucℕ (z +ℕ (z +ℕ (z +ℕ z *ℕ z)) +ℕ z))) → ⊥
    lem (even+2 ev') rewrite sym (+-assoc z z (z +ℕ z *ℕ z))
                           | +-assoc (z +ℕ z) (z +ℕ z *ℕ z) z with Even-decomp (z +ℕ z) _ ev' (evenAdd z)
    ... | decom rewrite +-assoc z (z *ℕ z) z
                      | +-comm (z *ℕ z) z
                      | sym (+-assoc z z (z *ℕ z)) with Even-decomp (z +ℕ z) _ decom (evenAdd z)
    ... | decom' = ¬Even-z-¬Even-z*z  z (neg-even-inj _ neqev) decom'

a+a≡b+b⇒a≡b : ∀ a b → a +ℕ a ≡ b +ℕ b → a ≡ b
a+a≡b+b⇒a≡b zero zero p = refl
a+a≡b+b⇒a≡b (sucℕ a) (sucℕ b) p = cong sucℕ (a+a≡b+b⇒a≡b a b lem)
  where
    lem : a +ℕ a ≡ b +ℕ b
    lem rewrite +-comm a (sucℕ a)
              | +-comm b (sucℕ b) = suc-injective (suc-injective p)

Even-p*p⇒Even-p : ∀ p → Even (p *ℕ p) → Even p
Even-p*p⇒Even-p z ev with DecEven z
Even-p*p⇒Even-p z ev | yes p = p
Even-p*p⇒Even-p z ev | no ¬p = ⊥-elim (¬Even-z-¬Even-z*z _ ¬p ev)

evenNom : ∀ (p : ℕ) (q : ℕ) → p *ℕ p ≡ 2 *ℕ (q *ℕ q) → Even p
evenNom p q prf = Even-p*p⇒Even-p p (a≡2*b-even _ (q *ℕ q) prf)


evenDenom : ∀ (p q : ℕ) → Even p → p *ℕ p ≡ 2 *ℕ (q *ℕ q) → Even q
evenDenom p q ev prf with even-a≡2*b _ ev
... | b , refl rewrite *-distribʳ-+ (b +ℕ (b +ℕ 0)) b (b +ℕ 0)
                     | +-identityʳ b
                     | +-identityʳ (q *ℕ q) with a+a≡b+b⇒a≡b (b *ℕ (b +ℕ b)) (q *ℕ q) prf
... | lem₁ rewrite *-distribˡ-+ b b b with a≡2*b-even (q *ℕ q) (b *ℕ b) (sym (subst (λ x → b *ℕ b +ℕ x ≡ q *ℕ q) (sym (+-identityʳ (b *ℕ b))) lem₁))
... | lem₂ = Even-p*p⇒Even-p _ lem₂


lem₁ : ∀ (p q : ℕ) → p *ℕ p ≡ 2 *ℕ (q *ℕ q) → ¬ Coprime p q
lem₁ p q prf cop with evenNom p q prf
... | evenp with evenDenom p q evenp prf
... | evenq with even-a≡2*b _ evenp | even-a≡2*b _ evenq
... | b₁ , prf₁ | b₂ , prf₂
            with cop {2} ((divides b₁ (subst (λ x → p ≡ x) (sym (*-comm b₁ 2)) prf₁))
                          , divides b₂ (subst (λ x → q ≡ x) (sym (*-comm b₂ 2)) prf₂))
... | ()


ℤ-sqeq : ∀ p → p *ℤ p ≡ + (∣ p ∣ *ℕ ∣ p ∣)
ℤ-sqeq (+_ zero) = refl
ℤ-sqeq +[1+ n ] = refl
ℤ-sqeq (-[1+_] n) = refl

sqrt2-irrational : ∀ (p : ℤ) (q : ℕ) → Coprime ∣ p ∣  q → ¬ p *ℤ p ≡ + (2 *ℕ (q *ℕ q))
sqrt2-irrational p q cop prf = lem₁ ∣ p ∣ q lem cop
  where
    lem' : + (∣ p ∣ *ℕ ∣ p ∣) ≡ + (q *ℕ q +ℕ (q *ℕ q +ℕ 0)) → ∣ p ∣ *ℕ ∣ p ∣ ≡ q *ℕ q +ℕ (q *ℕ q +ℕ 0)
    lem' prf = cong (λ { (+ n) → n ; (-[1+ n ]) → n}) prf
    
    lem : ∣ p ∣ *ℕ ∣ p ∣ ≡ q *ℕ q +ℕ (q *ℕ q +ℕ zero)
    lem rewrite ℤ-sqeq p = lem' prf