Skip to content

Instantly share code, notes, and snippets.

@krtx
Created July 5, 2017 10:52
Show Gist options
  • Save krtx/6cb43e0d2fe6935fd047c443ef5a9696 to your computer and use it in GitHub Desktop.
Save krtx/6cb43e0d2fe6935fd047c443ef5a9696 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment