TPPmark2014のAgda版解説 ref: http://qiita.com/masahiro_sakai/items/ecd83bad7ac8425f22a3

file4.txt

begin_ : ∀ {x y} → x ≡ y → x ≡ y

_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y ≡ z → x ≡ z

_∎ : ∀ x → x ≡ x

file5.txt

rem≡0⇒∣ : ∀ {a n} → (a mod suc n ≡ Fin.zero) → (suc n ∣ a)

3∣²⇒3∣ : ∀ {a} → (3 ∣ a ²) → (3 ∣ a)

file8.txt

a² + b² = 3c²
⇔ (3a’)² + (3b’)² = 3(3c’)²
⇔ 9 a’² + 9b’² = 9*3c’²
⇔ a’² + b’² = 3c’²

test.agda

begin_ : ∀ {x y} → x ≡ y → x ≡ y

_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y ≡ z → x ≡ z

_∎ : ∀ x → x ≡ x

TPPmark2014

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

TPPmark2014.agda

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