tppmark2014.agda

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

-- lemmas

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)

distribˡ-*-+ : ∀ m n o → m * (n + o) ≡ m * n + m * o
distribˡ-*-+ m n o = begin
  m * (n + o)
    ≡⟨ *-comm m (n + o) ⟩
  (n + o) * m
    ≡⟨ distribʳ-*-+ m n o ⟩
  n * m + o * m
    ≡⟨ cong (λ x → x + o * m) (*-comm n m) ⟩
  m * n + o * m
    ≡⟨ cong (λ x → m * n + x) (*-comm o m) ⟩
  m * n + m * o
    ∎
  where
    open ≡-Reasoning

∣-≡ : ∀ {k a b} → k ∣ a → a ≡ b → k ∣ b
∣-≡ div eq rewrite eq = div

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

∣-reduce : ∀ {a} k l → k * l ∣ a → k ∣ a
∣-reduce {a} k l (divides q eq) rewrite *-assoc q l k
                                      | *-comm k l
                                      | sym $ *-assoc q l k = divides (q * l) eq

/-congʳ : ∀ {i j} k → i * suc k ∣ j * suc k → i ∣ j
/-congʳ {i} {j} k div rewrite *-comm i (suc k)
                            | *-comm j (suc k) = /-cong k div

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

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

¬3∣4 : 3 ∣ 4 → ⊥
¬3∣4 (divides zero          ())
¬3∣4 (divides (suc zero)    ())
¬3∣4 (divides (suc (suc _)) ())

¬3∣x∧3∣2+x : ∀ {x} → 3 ∣ x → 3 ∣ 2 + x → ⊥
¬3∣x∧3∣2+x d₁ d₂ = ¬3∣2 (∣-∸ʳ d₂ d₁)

¬3∣x∧3∣1+x : ∀ {x} → 3 ∣ x → 3 ∣ 1 + x → ⊥
¬3∣x∧3∣1+x d₁ d₂ = ¬3∣1 (∣-∸ʳ d₂ d₁)

-- eq lemmas

lem-eq₁ : ∀ k → k * 3 + k * 3 * suc (k * 3) ≡ (k + k * suc (k * 3)) * 3
lem-eq₁ = solve 1 (λ k → k :* con 3 :+ k :* con 3 :* (con 1 :+ (k :* con 3)) := (k :+ k :* (con 1 :+ (k :* con 3))) :* con 3) refl

lem-eq₂ : ∀ k → k * 3 + (2 + (k * 3 + k * 3 * (2 + k * 3))) ≡
                2 + ((2 * k + k * 2 + k * 3 * k) * 3)
lem-eq₂ = solve 1 (λ k → k :* con 3 :+ (con 2 :+ (k :* con 3 :+ k :* con 3 :* (con 2 :+ k :* con 3))) := con 2 :+ ((con 2 :* k :+ k :* con 2 :+ k :* con 3 :* k) :* con 3)) refl

lem-eq₃ : ∀ a k → a * k * (a * k) ≡ a * a * (k * k)
lem-eq₃ = solve 2 (λ a k → a :* k :* (a :* k) := a :* a :* (k :* k)) refl

lem-eq₄ : ∀ a k → a * k * (a * k) * k ≡ a * a * k * (k * k)
lem-eq₄ = solve 2 (λ a k → a :* k :* (a :* k) :* k := a :* a :* k :* (k :* k)) refl

lem-eq₅ : ∀ k → 2 + (k * 3 + (2 + (k * 3 + k * 3 * (2 + (k * 3))))) ≡
                4 + (k + (k + k * (2 + k * 3))) * 3
lem-eq₅ = solve 1 (λ k → con 2 :+ (k :* con 3 :+ (con 2 :+ (k :* con 3 :+ k :* con 3 :* (con 2 :+ (k :* con 3))))) := con 4 :+ (k :+ (k :+ k :* (con 2 :+ k :* con 3))) :* con 3) refl

lem-eq₆ : ∀ a b → (2 + a) + (2 + b) ≡ 4 + (a + b)
lem-eq₆ = solve 2 (λ a b → con 2 :+ a :+ (con 2 :+ b) := con 4 :+ (a :+ b)) refl

lem-eq₇ : ∀ p → p * 3 * (p * 3) ≡ p * p * 9
lem-eq₇ = solve 1 (λ p → p :* con 3 :* (p :* con 3) := p :* p :* con 9) refl

lem-eq₈ : ∀ p → p * 3 * (p * 3) * 3 ≡ p * p * 3 * 9
lem-eq₈ = solve 1 (λ p → p :* con 3 :* (p :* con 3) :* con 3 := p :* p :* con 3 :* con 9) refl

-- trivial lemmas

lem₁ : ∀ a b → 3 ∣ a * 3 * b
lem₁ a b rewrite *-assoc a 3 b
                  | *-comm 3 b
                  | sym $ *-assoc a b 3 = divides (a * b) refl

lem₂ : ∀ k → 3 ∣ suc (k * 3 + k * 3 * suc (k * 3)) → 3 ∣ 1
lem₂ k div rewrite +-comm 1 (k * 3 + k * 3 * suc (k * 3))
                 | +-assoc (k * 3) (k * 3 * suc (k * 3)) 1
  = ∣-∸ (∣-∸ div (divides k refl)) (lem₁ k (suc (k * 3)))

lem₃ : ∀ k → 3 ∣ 2 + (k * 3 + (2 + (k * 3 + k * 3 * (2 + (k * 3))))) → 3 ∣ 4
lem₃ k div rewrite lem-eq₅ k = ∣-∸ʳ div (divides (k + (k + k * (2 + k * 3))) refl)

lem₄ : ∀ a p → suc a ≡ p * 3 → suc p ≤′ suc a
lem₄ a zero    ()
lem₄ a (suc p) eq rewrite eq
                        | *-comm p 3
                        | +-comm p 0
                        | sym $ +-assoc p p p
                  = s≤′s (s≤′s (n≤′m+n (suc p + p) p ))

lem₅ : ∀ a b c p q r → a ≡ p * 3 → b ≡ q * 3 → c ≡ r * 3 → a * a + b * b ≡ c * c * 3 → p * p + q * q ≡ r * r * 3
lem₅ a b c p q r eq₁ eq₂ eq₃ eq rewrite eq₁
                                      | eq₂
                                      | eq₃
                                      | lem-eq₇ p
                                      | lem-eq₇ q
                                      | lem-eq₈ r
                                      | sym $ distribʳ-*-+ 9 (p * p) (q * q)
                                      = remove-*1+k {p * p + q * q} {r * r * 3} 8 eq

-- preliminary

data Rem₃ : ℕ → Set where
  tr-zero : (k : ℕ) → Rem₃ (k * 3)
  tr-one  : (k : ℕ) → Rem₃ (1 + k * 3)
  tr-two  : (k : ℕ) → Rem₃ (2 + k * 3)

rem₃ : (n : ℕ) → Rem₃ n
rem₃ zero = tr-zero 0
rem₃ (suc n) with rem₃ n
rem₃ (suc .(k * 3))             | tr-zero k = tr-one k
rem₃ (suc .(suc (k * 3)))       | tr-one  k = tr-two k
rem₃ (suc .(suc (suc (k * 3)))) | tr-two  k = tr-zero (1 + k)

data _mod_≡_ : ℕ → ℕ → ℕ → Set where
  remains : {m n r : ℕ} (q : ℕ) (eq : m ≡ r + q * n) → m mod n ≡ r

nmod3≡1⇔3∣2+n : ∀ {n} → (n mod 3 ≡ 1 → 3 ∣ 2 + n) × (3 ∣ 2 + n → n mod 3 ≡ 1)
nmod3≡1⇔3∣2+n = nmod3≡1⇒3∣2+n , 3∣2+n⇒nmod3≡1
  where
    nmod3≡1⇒3∣2+n : ∀ {n} → n mod 3 ≡ 1 → 3 ∣ 2 + n
    nmod3≡1⇒3∣2+n (remains q eq) rewrite eq = divides (1 + q) refl

    3∣2+n⇒nmod3≡1 : ∀ {n} → 3 ∣ 2 + n → n mod 3 ≡ 1
    3∣2+n⇒nmod3≡1 (divides zero    ())
    3∣2+n⇒nmod3≡1 (divides (suc q) eq) = remains q (remove-k+ 2 eq)

div-sq-3 : ∀ x → 3 ∣ x * x → 3 ∣ x
div-sq-3 x div with rem₃ x
div-sq-3 .(k * 3)     div | tr-zero k = divides k refl
div-sq-3 .(1 + k * 3) div | tr-one  k = ⊥-elim $ ¬3∣1 (lem₂ k div)
div-sq-3 .(2 + k * 3) div | tr-two  k = ⊥-elim $ ¬3∣4 (lem₃ k div)

--

p₁′ : ∀ a → 9 ∣ a * a ⊎ 3 ∣ 2 + a * a
p₁′ a with rem₃ a
p₁′ .(k * 3)     | tr-zero k rewrite lem-eq₃ k 3 = inj₁ (divides (k * k) refl)
p₁′ .(1 + k * 3) | tr-one  k
  = inj₂ (divides (1 + k + k * suc (k * 3))
                  (cong (λ x → 3 + x) $ lem-eq₁ k))
p₁′ .(2 + k * 3) | tr-two  k
  = inj₂ (divides (2 + 2 * k + k * 2 + k * 3 * k)
                  (cong (λ x → 4 + x) $ lem-eq₂ k))

p₁ : ∀ a → 3 ∣ a * a ⊎ 3 ∣ 2 + a * a
p₁ a with p₁′ a
... | inj₁ u = inj₁ (∣-reduce 3 3 u)
... | inj₂ u = inj₂ u

p₂ : ∀ a b c → a * a + b * b ≡ (c * c) * 3 → 3 ∣ a × 3 ∣ b × 3 ∣ c
p₂ a b c eq with p₁′ a | p₁′ b | p₁′ c
p₂ a b c eq | inj₁ u | inj₁ v | inj₁ w =
  9∣a*a→3∣a a u , 9∣a*a→3∣a b v , 9∣a*a→3∣a c w
  where
    9∣a*a→3∣a : ∀ a → 9 ∣ a * a → 3 ∣ a
    9∣a*a→3∣a a div = div-sq-3 a $ ∣-reduce 3 3 div
p₂ a b c eq | inj₁ u | inj₁ v | inj₂ w =
  ⊥-elim (¬3∣2 (∣-∸ʳ {m = 2} w (/-congʳ {3} {c * c} 2 (∣-≡ (∣-+ u v) eq))))
p₂ a b c eq | inj₁ u | inj₂ v | _      = ⊥-elim $ ¬3∣x∧3∣2+x l₀ v
  where
    l₀ : 3 ∣ b * b
    l₀ = ∣-∸ (∣-≡ (divides (c * c) refl) (sym eq)) (∣-reduce 3 3 u)
p₂ a b c eq | inj₂ u | inj₁ v | _      = ⊥-elim $ ¬3∣x∧3∣2+x l₀ u
  where
    l₀ : 3 ∣ a * a
    l₀ = ∣-∸ʳ (∣-≡ (divides (c * c) refl) (sym eq)) (∣-reduce 3 3 v)
p₂ a b c eq | inj₂ u | inj₂ v | _      = ⊥-elim $ ¬3∣x∧3∣1+x 3∣x 3∣1+x
  where
    3∣x : 3 ∣ a * a + b * b
    3∣x = (∣-≡ (divides (c * c) refl) (sym eq))

    3∣1+x : 3 ∣ 1 + a * a + b * b
    3∣1+x = (∣-∸ (∣-≡ (∣-+ u v) (lem-eq₆ (a * a) (b * b))) (divides 1 refl))

p₃′-step : ∀ a
           → (rec : ∀ x → x <′ a → ∀ y → x * x ≡ y * y * 3 → x ≡ 0 × y ≡ 0)
           → ∀ b
           → a * a ≡ b * b * 3
           → a ≡ 0 × b ≡ 0
p₃′-step zero    _   zero    _  = refl , refl
p₃′-step zero    _   (suc _) ()
p₃′-step (suc _) _   zero    ()
p₃′-step (suc a) _   (suc b) eq with p₂ 0 (suc a) (suc b) eq
p₃′-step (suc a) rec (suc b) eq | _ , divides p eq₁ , divides q eq₂ with rec p (lem₄ a p eq₁) q (lem₅ 0 (suc a) (suc b) 0 p q refl eq₁ eq₂ eq)
p₃′-step (suc a) rec (suc b) eq | _ , divides zero ()   , divides _ _ | _ , _
p₃′-step (suc a) rec (suc b) eq | _ , divides (suc _) _ , divides _ _ | () , _

p₃′ : ∀ a b → a * a ≡ b * b * 3 → a ≡ 0 × b ≡ 0
p₃′ = <-rec _ p₃′-step

p₃-step : ∀ a
          → (rec : ∀ x → x <′ a → ∀ y z → x * x + y * y ≡ z * z * 3 → x ≡ 0 × y ≡ 0 × z ≡ 0)
          → ∀ b c
          → a * a + b * b ≡ c * c * 3
          → a ≡ 0 × b ≡ 0 × c ≡ 0
p₃-step zero    rec zero    zero    eq = refl , refl , refl
p₃-step zero    rec zero    (suc c) ()
p₃-step zero    rec (suc b) zero    ()
p₃-step zero    rec (suc b) (suc c) eq with p₃′ (suc b) (suc c) eq
... | eq₁ , eq₂ = refl , eq₁ , eq₂
p₃-step (suc a) rec zero    zero    ()
p₃-step (suc a) rec zero    (suc c) eq rewrite +-comm (a + a * suc a) 0
                                       with p₃′ (suc a) (suc c) eq
... | eq₁ , eq₂ = eq₁ , refl , eq₂
p₃-step (suc a) rec (suc b) zero    ()
p₃-step (suc a) rec (suc b) (suc c) eq with p₂ (suc a) (suc b) (suc c) eq
... | divides p eq₁ , divides q eq₂ , divides r eq₃ with rec p (lem₄ a p eq₁) q r (lem₅ (suc a) (suc b) (suc c) p q r eq₁ eq₂ eq₃ eq)
p₃-step (suc a) rec (suc b) (suc c) eq | divides zero ()     , divides q eq₂ , divides r eq₃ | _  , _
p₃-step (suc a) rec (suc b) (suc c) eq | divides (suc p) eq₁ , divides q eq₂ , divides r eq₃ | () , _

p₃ : ∀ a b c → a * a + b * b ≡ (c * c) * 3 → a ≡ 0 × b ≡ 0 × c ≡ 0
p₃ = <-rec _ p₃-step