TPPmark2014のAgda版解説

TPPmark2014のAgda版解説
======================

この記事は[Theorem Prover Advent Calendar 2014](http://qiita.com/advent-calendar/2014/theorem_prover)の12/14(日)の記事です。

[TPP (Theorem proving and provers for reliable theory and implementations) 2014](http://imi.kyushu-u.ac.jp/lasm/tpp2014/) という定理証明系に関するワークショップでのお題の問題 [TPPmark2014](http://imi.kyushu-u.ac.jp/lasm/tpp2014/tppmark2014-2.pdf) をAgdaで解いた解答について簡単に紹介します。

すでに[tmiya_さんがCoqでの解答](http://study-func-prog.blogspot.jp/2014/12/coq-tppmark2014-theorem-prover-advent.html)について投稿していて、問題の概略についてはすでにそちらに解説があるので、そちらを参照。この記事では[酒井のAgda版解答](https://github.com/msakai/TPPmark2014/blob/master/TPPmark2014.agda)について解説する。 他の解答については[レポジトリ](https://github.com/KyushuUniversityMathematics/TPP2014/)を参照してください。

全体
---

今回利用した環境は Agda-2.4.2.1 と agda-stdlib-0.9 。

行数は約500行ほど。 SSreflectで数十行程度の証明があることを思うとかなり長めで、その理由の１つは、Presburger算術の自動証明(e.g. CoqのOmega)等が存在しないため、雑多な補題が多く必要になってしまったこと。 

基本的な定義など
-------------

基本的な定義は基本的に `Data.Nat`, `Data.Nat.DivMod`, `Data.Nat.Divisibility` などにあるので、それを使う。`mod` は自然数型 ℕ の値を返すのではなく、有限集合 {0, 1, …, n-1} の型である `Fin n` の値を返すので注意。

その他には二乗を表す後置の演算子を定義しておく。 

```agda:TPPmark2014.agda
_² : ℕ → ℕ
_² n = n * n
```

その他、雑多な補題が沢山あるけど、省略。

(i) For any a ∈ N, (a² mod 3) = 0 or (a² mod 3) = 1.
----------------------------------------------------

最初の問題の回答部分を以下に示す（`⊎` は Haskell での `Either` に相当）。

```agda:TPPmark2014.agda
prop1 : ∀ a → (a ² mod 3 ≡ Fin.zero) ⊎ (a ² mod 3 ≡ Fin.suc (Fin.zero))
prop1 a rewrite mod-dist-* {2} a a with a mod 3
... | Fin.zero = inj₁ refl
... | Fin.suc Fin.zero = inj₂ refl
... | Fin.suc (Fin.suc Fin.zero) = inj₂ refl
... | Fin.suc (Fin.suc (Fin.suc ()))
```

まず、用意していた補題

```agda:TPPmark2014.agda
mod-dist-* : ∀ {n} a b → (a * b) mod suc n ≡ (toℕ (a mod suc n) * toℕ (b mod suc n)) mod suc n
```

を用いてrewriteすることで、ゴールの型を `(a ² mod 3 ≡ Fin.zero) ⊎ (a ² mod 3 ≡ Fin.suc (Fin.zero))` から
`((toℕ (a mod 3) * toℕ (a mod 3)) mod 3 ≡ Fin.zero) ⊎ ((toℕ (a mod 3) * toℕ (a mod 3)) mod 3 ≡ Fin.suc (Fin.zero))` へと書き換える。

そのうえで、`a mod 3` で場合分けを行っていて、

1. `Fin.zero` の場合、ゴールの型は `((toℕ Fin.zero * toℕ Fin.zero) mod 3 ≡ Fin.zero) ⊎ ((toℕ Fin.zero * toℕ Fin.zero) mod 3 ≡ Fin.suc (Fin.zero))` すなわち `Fin.zero ≡ Fin.zero ⊎ Fin.zero ≡ Fin.suc (Fin.zero))` となるので、`refl : Fin.zero ≡ Fin.zero` を `inj₁ : A → A ⊎ B` で入射すればok。 β簡約他が definitional equality に含まれているので、明示的に unfold したりする必要はない。
2. `Fin.suc Fin.zero` の場合と` Fin.suc (Fin.suc Fin.zero)` の場合も同様。
3. 最後に、パターンマッチ的には `Fin.suc (Fin.suc (Fin.suc x))` という場合もあり得るのだけれど、このようなパターンは `Fin 3` という型を持ち得ないので、あり得ないことを absurd pattern `()` であり得ないということを表現している。あり得ないので、右辺は不要。

簡単だね！

(ii) Let a ∈ N, b ∈ N and c ∈ N. If a² + b² = 3c² then (3 | a), (3 | b) and (3 | c).
------------------------------------------------------------------------------------

a, b, c のそれぞれが3で割り切れることを証明するので、まずは a の場合の全体像を以下に示す。

```agda:TPPmark2014.agda
prop2a : ∀ a b c → (a ² + b ² ≡ 3 * c ²) → (3 ∣ a)
prop2a a b c a²+b²≡3c² = 3∣²⇒3∣ 3∣a²
  where
    open ≡-Reasoning

    lem1 : (toℕ (a ² mod 3) + toℕ (b ² mod 3)) mod 3 ≡ Fin.zero
    lem1 = begin
        (toℕ (a ² mod 3) + toℕ (b ² mod 3)) mod 3
          ≡⟨ sym (mod-dist-+ (a ²) (b ²)) ⟩
        (a ² + b ²) mod 3
          ≡⟨ cong (λ x → x mod 3) a²+b²≡3c² ⟩
        (3 * c ²) mod 3
          ≡⟨ mod-dist-* 3 (c ²) ⟩
        Fin.zero
          ∎
    
    a²mod3≡0 : a ² mod 3 ≡ Fin.zero
    a²mod3≡0 = ?

    3∣a² : 3 ∣ a ²
    3∣a² = rem≡0⇒∣ a²mod3≡0
```

「a ² + b ² ≡ 3 * c ²」という型の引数には、`a²+b²≡3c²`という名前を付けている。このように式から空白を取り除いて連結したものを識別子として用いることが、Agdaではよくある（特に命題の証明項など値を気にしない場合）、

`open ≡-Reasoning` は等式推論を構造化して書くためのコンビネータを利用するための宣言で、これを使うと`lem1`でのような書き方ができる。実装は大雑把には以下のような型の演算子が定義されているだけ（実際には型推論の都合上、少し違うけど）。

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

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

_∎ : ∀ x → x ≡ x
```

`a²mod3≡0 : a ² mod 3 ≡ Fin.zero` は、`lem1` に対して `prop1 a : (a ² mod 3 ≡ Fin.zero) ⊎ (a ² mod 3 ≡ Fin.suc (Fin.zero))` と `prop1 b : (b ² mod 3 ≡ Fin.zero) ⊎ (b ² mod 3 ≡ Fin.suc (Fin.zero))` による場合分けを行って `a ² mod 3 ≡ Fin.zero` の場合以外を潰すことで示しているが、細かいので略。

最後に、用意していた以下の補題(「剰余が0ならば割り切れる」「a²が3で割り切れるなら、a自体も3で割り切れる」)を適用することで、求める証明が得られる。

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

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

次に、bが3で割り切れることは、`prop2a`の引数を入れ替えてあげるだけでOK（ちなみに、`$`はHaskellと同じで、結合順位の低い関数適用）。

```agda:TPPmark2014.agda
prop2b : ∀ a b c → (a ² + b ² ≡ 3 * c ²) → (3 ∣ b)
prop2b a b c a²+b²≡3c² = prop2a b a c $
    begin
      b ² + a ²
    ≡⟨ CS.+-comm (b ²) (a ²) ⟩
      a ² + b ²
    ≡⟨ a²+b²≡3c² ⟩
      3 * c ²
    ∎
  where
    open ≡-Reasoning
```

最後にcが3で割り切れることは、`prop2a`と`prop2b`を組み合わせれば証明できる。

```agda:TPPmark2014.agda
prop2c : ∀ a b c → (a ² + b ² ≡ 3 * c ²) → (3 ∣ c)
prop2c a b c a²+b²≡3c² = 3∣²⇒3∣ 3∣c²
  where
    9∣a² : 9 ∣ a ²
    9∣a² = ∣⇒²∣² (prop2a a b c a²+b²≡3c²)

    9∣b² : 9 ∣ b ²
    9∣b² = ∣⇒²∣² (prop2b a b c a²+b²≡3c²)

    9∣a²+b² : 9 ∣ a ² + b ²
    9∣a²+b² = ∣-+ 9∣a² 9∣b²

    9∣3*c² : 9 ∣ 3 * c ²
    9∣3*c² = subst (λ x → 9 ∣ x) a²+b²≡3c² 9∣a²+b²

    3∣c² : 3 ∣ c ²
    3∣c² = /-cong 2 9∣3*c²
```

(iii) Let a ∈ N, b ∈ N and c ∈ N. If a² + b² = 3c² then a = b = c = 0.
----------------------------------------------------------------------

a² + b² = 3c² ならば (ii) の結果から a = 3 * a', b = 3 * b', c = 3 * c' のはずで、


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

となる（ソースコード中の`prop3-lemma`）。

そして、もし a が 0 でなければ a' < a となるので、`∀ b c → a ² + b ² ≡ 3 c ² → a ≡ 0` を `a` に関する整礎帰納法(well-founded induction) で証明する。

```agda: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
```

b=0 は`prop3a`と同様にしても良いのだけれど、例によって`prop3a`の引数をひっくり返すだけで証明できる。

c=0 は`prop3a`と同様。

QED