AB 3 by trigott

module Theorem where

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Nat.Properties using (m+n∸n≡m; *-distrib-∸ʳ)
-- open import Data.Nat.Properties.Simple
--   using (+-comm; distribʳ-*-+; *-assoc; *-comm; +-assoc)
open import Data.Sum
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- from Data.Nat.Properties.Simple
module Simple where
  open import Function
  
  +-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
    ∎
  
  +-*-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
    ∎
  
  *-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
    ∎
  
  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
    ∎
  
  *-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)
    ∎

open Simple

data Trity : ℕ → Set where
  trity-0 : (k : ℕ) → Trity (k * 3)
  trity-1 : (k : ℕ) → Trity (1 + k * 3)
  trity-2 : (k : ℕ) → Trity (2 + k * 3)

trity : (n : ℕ) → Trity n
trity zero = trity-0 zero
trity (suc n) with trity n
trity (suc .(k * 3))     | trity-0 k = trity-1 k
trity (suc .(1 + k * 3)) | trity-1 k = trity-2 k
trity (suc .(2 + k * 3)) | trity-2 k = trity-0 (suc k)

lem : ∀ {a b} n → a ≡ b → a ∸ n ≡ b ∸ n
lem _ refl = refl

lem-divˡ : ∀ {m n p} → (p ∣ m) → (p ∣ m + n) → (p ∣ n)
lem-divˡ {m} {n} {p} (divides q eq) (divides q₁ eq₁)
  rewrite eq with lem (q * p) eq₁
... | u rewrite +-comm (q * p) n
              | m+n∸n≡m n (q * p)
              | sym (*-distrib-∸ʳ p q₁ q) = divides (q₁ ∸ q) u

lem-divʳ : ∀ {m n p} → (p ∣ n) → (p ∣ m + n) → (p ∣ m)
lem-divʳ {m} {n} p∣n p∣m+n rewrite +-comm m n = lem-divˡ p∣n p∣m+n

m*n*o≡m*o*n : ∀ m n o → m * n * o ≡ m * o * n
m*n*o≡m*o*n m n o = begin
    m * n * o   ≡⟨ *-assoc m n o ⟩
    m * (n * o) ≡⟨ cong (_*_ m) (*-comm n o) ⟩
    m * (o * n) ≡⟨ sym (*-assoc m o n) ⟩
    m * o * n   ∎

3∤1 :  3 ∣ 1 → ⊥
3∤1 (divides zero ())
3∤1 (divides (suc q) ())

3∤2 : 3 ∣ 2 → ⊥
3∤2 (divides zero ())
3∤2 (divides (suc q) ())

ab3 : (a b : ℕ) → 3 ∣ a * b → 3 ∣ a ⊎ 3 ∣ b
ab3 a b div with trity a | trity b
ab3 .(k * 3) _ _ | trity-0 k | _ = inj₁ (divides k refl)
ab3 _ .(l * 3) _ | _ | trity-0 l = inj₂ (divides l refl)
ab3 .(1 + k * 3) .(1 + l * 3) div | trity-1 k | trity-1 l
  rewrite m*n*o≡m*o*n k 3 (1 + l * 3)
        | sym (distribʳ-*-+ 3 l (k * (1 + l * 3)))
  with lem-divʳ {1} (divides {3} (l + k * (1 + l * 3)) refl) div
... | u = ⊥-elim (3∤1 u)
ab3 .(1 + k * 3) .(2 + l * 3) div | trity-1 k | trity-2 l
  rewrite m*n*o≡m*o*n k 3 (2 + l * 3)
        | sym (distribʳ-*-+ 3 l (k * (2 + l * 3)))
  with lem-divʳ {2} (divides {3} (l + k * (2 + l * 3)) refl) div
... | u = ⊥-elim (3∤2 u)
ab3 .(2 + k * 3) .(1 + l * 3) div | trity-2 k | trity-1 l
  rewrite begin
    suc (l * 3 + suc (l * 3 + k * 3 * suc (l * 3)))
      ≡⟨ cong (λ x → x + suc (l * 3 + k * 3 * suc (l * 3))) (+-comm 1 (l * 3)) ⟩
    (l * 3 + 1) + suc (l * 3 + k * 3 * suc (l * 3))
      ≡⟨ +-assoc (l * 3) 1 (suc (l * 3 + k * 3 * suc (l * 3))) ⟩
    l * 3 + (1 + suc (l * 3 + k * 3 * suc (l * 3)))
      ∎
  with lem-divˡ {l * 3} {2 + l * 3 + k * 3 * suc (l * 3)} {3} (divides {3} l refl) div
... | div′
  rewrite begin
    2 + l * 3 + k * 3 * suc (l * 3)
      ≡⟨ cong (λ x → x + k * 3 * suc (l * 3)) (+-comm 2 (l * 3)) ⟩
    (l * 3 + 2) + k * 3 * suc (l * 3)
      ≡⟨ +-assoc (l * 3) 2 (k * 3 * suc (l * 3)) ⟩
    l * 3 + (2 + k * 3 * suc (l * 3))
      ∎
  with lem-divˡ {l * 3} {2 + k * 3 * suc (l * 3)} (divides {3} l refl) div′
... | div″
  rewrite m*n*o≡m*o*n k 3 (suc (l * 3))
  with lem-divʳ {2} {k * suc (l * 3) * 3} (divides {3} (k * suc (l * 3)) refl) div″
... | 3∣2 = ⊥-elim (3∤2 3∣2)

ab3 .(2 + k * 3) .(2 + l * 3) div | trity-2 k | trity-2 l
  rewrite begin
    2 + l * 3 + (2 + l * 3 + k * 3 * (2 + l * 3))
      ≡⟨ cong (λ x → x + (2 + l * 3 + k * 3 * (2 + l * 3))) (+-comm 2 (l * 3)) ⟩
    (l * 3 + 2) + (2 + l * 3 + k * 3 * (2 + l * 3))
      ≡⟨ +-assoc (l * 3) 2 (2 + l * 3 + k * 3 * (2 + l * 3)) ⟩
    l * 3 + (2 + (2 + l * 3 + k * 3 * (2 + l * 3)))
      ∎
  with lem-divˡ {l * 3} {4 + l * 3 + k * 3 * (2 + l * 3)} (divides {3} l refl) div
... | div′
  rewrite m*n*o≡m*o*n k 3 (2 + l * 3)
  with lem-divʳ {4 + l * 3} (divides {3} (k * (2 + l * 3)) refl) div′
... | div″
  with lem-divʳ {4} (divides {3} l refl) div″
... | div‴
  with lem-divʳ {1} (divides {3} 1 refl) div‴
... | 3∣1 = ⊥-elim (3∤1 3∣1)