Skip to content

Instantly share code, notes, and snippets.

@msakai
Last active Aug 29, 2015
Embed
What would you like to do?
begin_ : ∀ {x y} → x ≡ y → x ≡ y
_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y ≡ z → x ≡ z
_∎ : ∀ x → x ≡ x
rem≡0⇒∣ : ∀ {a n} → (a mod suc n ≡ Fin.zero) → (suc n ∣ a)
3∣²⇒3∣ : ∀ {a} → (3 ∣ a ²) → (3 ∣ a)
a² + b² = 3c²
⇔ (3a’)² + (3b’)² = 3(3c’)²
⇔ 9 a’² + 9b’² = 9*3c’²
⇔ a’² + b’² = 3c’²
begin_ : {x y} x ≡ y x ≡ y
_≡⟨_⟩_ : x {y z} x ≡ y y ≡ z x ≡ z
_∎ : x x ≡ x
prop3a-step
: ∀ a
→ (∀ a' → (a' <′ a) → ∀ b' c' → (a' ² + b' ² ≡ 3 * c' ²) → a' ≡ 0)
→ ∀ b c → (a ² + b ² ≡ 3 * c ²) → a ≡ 0
prop3a-step zero rec b c P = refl
prop3a-step (suc n) rec b c P = body
where
open ≡-Reasoning
a = suc n
body : a ≡ 0
body with (prop2a a b c P) | (prop2b a b c P) | (prop2c a b c P)
... | divides a' a≡a'*3 | divides b' b≡b'*3 | divides c' c≡c'*3 =
begin
a
≡⟨ a≡a'*3 ⟩
a' * 3
≡⟨ cong (λ x → x * 3) a'≡0 ⟩
0 * 3
≡⟨ refl ⟩
0
where
a'≡0 : a' ≡ 0
a'≡0 = rec a' (≤⇒≤′ a'<a) b' c' lem2
where
lem1 : (a' * 3) ² + (b' * 3) ² ≡ 3 * (c' * 3) ²
lem1 rewrite (sym a≡a'*3) | (sym b≡b'*3) | (sym c≡c'*3) = P
lem2 : a' ² + b' ² ≡ 3 * c' ²
lem2 = prop3-lemma a' b' c' lem1
a'<a : a' < a
a'<a = 2+m∣1+n⇒quot<1+n (divides a' a≡a'*3)
prop3a : ∀ a b c → (a ² + b ² ≡ 3 * c ²) → a ≡ 0
prop3a a = <-rec (λ n → ∀ b c → (n ² + b ² ≡ 3 * c ²) → n ≡ 0) prop3a-step a
prop3a-step
: a
( a' (a' <′ a) b' c' (a' ² + b' ² ≡ 3 * c' ²) a' ≡ 0)
b c (a ² + b ² ≡ 3 * c ²) a ≡ 0
prop3a-step zero rec b c P = refl
prop3a-step (suc n) rec b c P = body
where
open ≡-Reasoning
a = suc n
body : a ≡ 0
body with (prop2a a b c P) | (prop2b a b c P) | (prop2c a b c P)
... | divides a' a≡a'*3 | divides b' b≡b'*3 | divides c' c≡c'*3 =
begin
a
≡⟨ a≡a'*3 ⟩
a' * 3
≡⟨ cong (λ x x * 3) a'≡0 ⟩
0 * 3
≡⟨ refl ⟩
0
where
a'≡0 : a' ≡ 0
a'≡0 = rec a' (≤⇒≤′ a'<a) b' c' lem2
where
lem1 : (a' * 3) ² + (b' * 3) ² ≡ 3 * (c' * 3) ²
lem1 rewrite (sym a≡a'*3) | (sym b≡b'*3) | (sym c≡c'*3) = P
lem2 : a' ² + b' ² ≡ 3 * c' ²
lem2 = prop3-lemma a' b' c' lem1
a'<a : a' < a
a'<a = 2+m∣1+n⇒quot<1+n (divides a' a≡a'*3)
prop3a : a b c (a ² + b ² ≡ 3 * c ²) a ≡ 0
prop3a a = <-rec (λ n b c (n ² + b ² ≡ 3 * c ²) n ≡ 0) prop3a-step a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment