TPPmark2014のAgda版解説

この記事はTheorem Prover Advent Calendar 2014の12/14(日)の記事です。

TPP (Theorem proving and provers for reliable theory and implementations) 2014 という定理証明系に関するワークショップでのお題の問題 TPPmark2014 をAgdaで解いた解答について簡単に紹介します。

すでにtmiya_さんがCoqでの解答について投稿していて、問題の概略についてはすでにそちらに解説があるので、そちらを参照。この記事では酒井のAgda版解答について解説する。他の解答についてはレポジトリを参照してください。

全体

今回利用した環境は 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 の値を返すので注意。

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

TPPmark2014.agda

_² : ℕ → ℕ
_² n = n * n

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

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

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

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 ()))

まず、用意していた補題

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 で場合分けを行っていて、

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 したりする必要はない。
Fin.suc Fin.zero の場合とFin.suc (Fin.suc Fin.zero) の場合も同様。
最後に、パターンマッチ的には 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 の場合の全体像を以下に示す。

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でのような書き方ができる。実装は大雑把には以下のような型の演算子が定義されているだけ（実際には型推論の都合上、少し違うけど）。

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で割り切れる」)を適用することで、求める証明が得られる。

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と同じで、結合順位の低い関数適用）。

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を組み合わせれば証明できる。

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) で証明する。

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