Test.agda

module Test where

open import Function
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod using (_divMod_; _mod_; result)
open import Data.Fin using (zero; suc; toℕ)
open import Data.Sum
open import Data.Product
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality
import Algebra
open Algebra.CommutativeSemiring commutativeSemiring using (+-assoc; +-comm; *-assoc; *-comm; distribʳ)
open SemiringSolver

Sn*3≢m*3×SSn*3≢m*3 : (n m : ℕ) → suc (n * 3) ≢ m * 3 × suc (suc (n * 3)) ≢ m * 3
Sn*3≢m*3×SSn*3≢m*3 n zero = (λ ()) , (λ ())
Sn*3≢m*3×SSn*3≢m*3 n (suc m) = (proj₂ p ∘ cancel-+-left 1 ∘ sym) , (proj₁ p ∘ cancel-+-left 2 ∘ sym) where
  p = Sn*3≢m*3×SSn*3≢m*3 m n

Sn*3≢m*3 : (n m : ℕ) → suc (n * 3) ≢ m * 3
Sn*3≢m*3 n m = proj₁ $ Sn*3≢m*3×SSn*3≢m*3 n m

SSn*3≢m*3 : (n m : ℕ) → suc (suc (n * 3)) ≢ m * 3
SSn*3≢m*3 n m = proj₂ $ Sn*3≢m*3×SSn*3≢m*3 n m

3+n%3≡n%3 : (n : ℕ) → (3 + n) mod 3 ≡ n mod 3
3+n%3≡n%3 n with (3 + n) divMod 3 | n divMod 3
3+n%3≡n%3 n | result quotient zero property | result quotient₁ zero property₁ = refl
3+n%3≡n%3 n | result quotient zero property | result quotient₁ (suc zero) property₁ rewrite property₁ = ⊥-elim $ Sn*3≢m*3 (suc quotient₁) quotient property
3+n%3≡n%3 n | result quotient zero property | result quotient₁ (suc (suc zero)) property₁ rewrite property₁ = ⊥-elim $ SSn*3≢m*3 (suc quotient₁) quotient property
3+n%3≡n%3 n | result quotient zero property | result quotient₁ (suc (suc (suc ()))) property₁
3+n%3≡n%3 n | result quotient (suc zero) property | result quotient₁ zero property₁ rewrite property₁ = ⊥-elim $ Sn*3≢m*3 quotient (suc quotient₁) $ sym property
3+n%3≡n%3 n | result quotient (suc zero) property | result quotient₁ (suc zero) property₁ = refl
3+n%3≡n%3 n | result quotient (suc zero) property | result quotient₁ (suc (suc zero)) property₁ rewrite property₁ = ⊥-elim $ Sn*3≢m*3 (suc quotient₁) quotient $ cancel-+-left 1 property
3+n%3≡n%3 n | result quotient (suc zero) property | result quotient₁ (suc (suc (suc ()))) property₁
3+n%3≡n%3 n | result quotient (suc (suc zero)) property | result quotient₁ zero property₁ rewrite property₁ = ⊥-elim $ SSn*3≢m*3 quotient (suc quotient₁) $ sym property
3+n%3≡n%3 n | result quotient (suc (suc zero)) property | result quotient₁ (suc zero) property₁ rewrite property₁ = ⊥-elim $ SSn*3≢m*3 quotient₁ quotient $ cancel-+-left 2 property
3+n%3≡n%3 n | result quotient (suc (suc zero)) property | result quotient₁ (suc (suc zero)) property₁ = refl
3+n%3≡n%3 n | result quotient (suc (suc zero)) property | result quotient₁ (suc (suc (suc ()))) property₁
3+n%3≡n%3 n | result quotient (suc (suc (suc ()))) property | result quotient₁ remainder₁ property₁

%-idempotent : (n : ℕ) → toℕ (n mod 3) mod 3 ≡ n mod 3
%-idempotent n with n mod 3
%-idempotent n | zero = refl
%-idempotent n | suc zero = refl
%-idempotent n | suc (suc zero) = refl
%-idempotent n | suc (suc (suc ()))

distrib-%-+ : (m n : ℕ) → (m + n) mod 3 ≡ (toℕ (m mod 3) + toℕ (n mod 3)) mod 3
distrib-%-+ zero n
  rewrite %-idempotent n
        = refl
distrib-%-+ (suc zero) zero = refl
distrib-%-+ (suc zero) (suc zero) = refl
distrib-%-+ (suc zero) (suc (suc zero)) = refl
distrib-%-+ (suc zero) (suc (suc (suc n)))
  rewrite 3+n%3≡n%3 n
        | 3+n%3≡n%3 (suc n)
        = distrib-%-+ (suc zero) n
distrib-%-+ (suc (suc zero)) zero = refl
distrib-%-+ (suc (suc zero)) (suc zero) = refl
distrib-%-+ (suc (suc zero)) (suc (suc zero)) = refl
distrib-%-+ (suc (suc zero)) (suc (suc (suc n)))
  rewrite 3+n%3≡n%3 n
        | 3+n%3≡n%3 (suc (suc n))
        = distrib-%-+ (suc (suc zero)) n
distrib-%-+ (suc (suc (suc m))) n
  rewrite 3+n%3≡n%3 (m + n)
        | 3+n%3≡n%3 m
        = distrib-%-+ m n

3*n%3≡0 : (n : ℕ) → (3 * n) mod 3 ≡ zero
3*n%3≡0 zero = refl
3*n%3≡0 (suc n)
  rewrite cong (λ x → x mod 3) (solve 1 (λ x → con 3 :* (con 1 :+ x) := con 3 :+ con 3 :* x) refl n)
        | 3+n%3≡n%3 (3 * n)
        = 3*n%3≡0 n

distrib-%-* : (m n : ℕ) → (m * n) mod 3 ≡ (toℕ (m mod 3) * toℕ (n mod 3)) mod 3
distrib-%-* zero n = refl
distrib-%-* (suc zero) n
  rewrite +-comm n 0
        | +-comm (toℕ (n mod 3)) 0
        | %-idempotent n
        = refl
distrib-%-* (suc (suc zero)) n
  rewrite +-comm n 0
        | +-comm (toℕ (n mod 3)) 0
        | distrib-%-+ n n
        = refl
distrib-%-* (suc (suc (suc m))) n
  rewrite distribʳ n 3 m
        | distrib-%-+ (3 * n) (m * n)
        | 3+n%3≡n%3 m
        | 3*n%3≡0 n
        | %-idempotent (m * n)
        = distrib-%-* m n

p1 : (a : ℕ) → (a * a) mod 3 ≡ zero ⊎ (a * a) mod 3 ≡ suc zero
p1 a = p1' (distrib-%-* a a) where
  p1' : (a * a) mod 3 ≡ (toℕ (a mod 3) * toℕ (a mod 3)) mod 3 → (a * a) mod 3 ≡ zero ⊎ (a * a) mod 3 ≡ suc zero
  p1' eq with a divMod 3
  p1' eq | result quotient zero property = inj₁ eq
  p1' eq | result quotient (suc zero) property = inj₂ eq
  p1' eq | result quotient (suc (suc zero)) property = inj₂ eq
  p1' eq | result quotient (suc (suc (suc ()))) property

n*n%3≡0→n%3≡0 : (n : ℕ) → (n * n) mod 3 ≡ zero → n mod 3 ≡ zero
n*n%3≡0→n%3≡0 n eq rewrite distrib-%-* n n = lemma eq where
  lemma : (toℕ (n mod 3) * toℕ (n mod 3)) mod 3 ≡ zero → n mod 3 ≡ zero
  lemma eq' with n divMod 3
  lemma eq' | result quotient zero property = refl
  lemma () | result quotient (suc zero) property
  lemma () | result quotient (suc (suc zero)) property
  lemma eq' | result quotient (suc (suc (suc ()))) property

1%3≢0 : 1 mod 3 ≢ zero
1%3≢0 ()

2%3≢0 : 2 mod 3 ≢ zero
2%3≢0 ()

n%3≡0→n=3*k : (n : ℕ) → n mod 3 ≡ zero → Σ[ k ∈ ℕ ] n ≡ 3 * k
n%3≡0→n=3*k n eq with n divMod 3
n%3≡0→n=3*k n eq | result quotient zero property rewrite *-comm quotient 3 = quotient , property
n%3≡0→n=3*k n () | result quotient (suc zero) property
n%3≡0→n=3*k n () | result quotient (suc (suc zero)) property
n%3≡0→n=3*k n eq | result quotient (suc (suc (suc ()))) property

p2 : (a b c : ℕ) → a * a + b * b ≡ 3 * (c * c) → a mod 3 ≡ zero × b mod 3 ≡ zero × c mod 3 ≡ zero
p2 a b c eq = a%3≡0 , b%3≡0 , c%3≡0 where
  a%3≡0×b%3≡0 = p2' $ cong (λ n → n mod 3) eq where
    p2' : (a * a + b * b) mod 3 ≡ (3 * (c * c)) mod 3 → a mod 3 ≡ zero × b mod 3 ≡ zero
    p2' eq'
      rewrite 3*n%3≡0 (c * c)
            | distrib-%-+ (a * a) (b * b)
            = p2'' eq' where
      p2'' : (toℕ ((a * a) mod 3) + toℕ ((b * b) mod 3)) mod 3 ≡ zero → a mod 3 ≡ zero × b mod 3 ≡ zero
      p2'' eq'' with p1 a | p1 b
      p2'' eq'' | inj₁ x | inj₁ x₁ = (n*n%3≡0→n%3≡0 a x) , (n*n%3≡0→n%3≡0 b x₁)
      p2'' eq'' | inj₁ x | inj₂ y   rewrite x | y = ⊥-elim $ 1%3≢0 eq''
      p2'' eq'' | inj₂ y | inj₁ x   rewrite y | x = ⊥-elim $ 1%3≢0 eq''
      p2'' eq'' | inj₂ y | inj₂ y₁  rewrite y | y₁ = ⊥-elim $ 2%3≢0 eq''
  a%3≡0 = proj₁ a%3≡0×b%3≡0
  b%3≡0 = proj₂ a%3≡0×b%3≡0
  c%3≡0 = p2' eq (n%3≡0→n=3*k a a%3≡0) (n%3≡0→n=3*k b b%3≡0) where
    p2' : a * a + b * b ≡ 3 * (c * c) → Σ[ a' ∈ ℕ ] a ≡ 3 * a' → Σ[ b' ∈ ℕ ] b ≡ 3 * b' → c mod 3 ≡ zero
    p2' eq' (a' , a≡3*a') (b' , b≡3*b')
      rewrite a≡3*a'
            | b≡3*b'
            | solve 2 (λ x y → con 3 :* x :* (con 3 :* x) :+ con 3 :* y :* (con 3 :* y) := con 3 :* (x :* x :+ y :* y) :* con 3) refl a' b'
            | *-comm 3 (c * c)
            = p2'' $
                cong (λ n → n mod 3) $
                cancel-*-right (3 * (a' * a' + b' * b')) (c * c) eq' where
      p2'' : (3 * (a' * a' + b' * b')) mod 3 ≡ (c * c) mod 3 → c mod 3 ≡ zero
      p2'' eq''
        rewrite 3*n%3≡0 (a' * a' + b' * b')
              = n*n%3≡0→n%3≡0 c $ sym eq''