Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理：Rainy Day Codings：So-net blog

	ブログをはじめるログイン

Agdaによる「プログラミング言語の基礎..｜Agdaによる「プログラミング言語の基礎.. ブログトップ

Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理　[Agda] [編集]

第1章で定義した導出システムNatについてのメタ定理を証明していく。

module igarashi2 where

open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; subst)
open import Data.Product
  using (_×_; proj₁; proj₂; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import igarashi1

定理2.1 加算の単位元

定理2.1はゼロが加算の単位元であることを左右それぞれ証明する。

-- +-identityˡ
theorem2-1-1 : ∀ {n : ℕ}
    ----------------
  → NatJudgement (0 plus n is n)

theorem2-1-1 {n} = P-ZERO {n}

-- +-identityʳ
theorem2-1-2 : ∀ {n : ℕ}
    ----------------
  → NatJudgement (n plus 0 is n)

theorem2-1-2 {zero} = P-ZERO {0}
theorem2-1-2 {suc n} = P-SUCC {n} {0} {n} (theorem2-1-2 {n})

これらの証明は実のところ全部自動でできる。

Agdaで証明を始めるときには型を書いたあと全体がHoleであるような証明をまず書いてしまうとよい。theorem2-1-2の場合はまずこのように書く。

theorem2-1-2 = ?

ここでCtrl+c, Ctrl+c, Enterすると引数を追加してくれる（中括弧引数と小括弧引数がある場合はまず小括弧引数が補完され、2回めに中括弧引数が保管される）。

theorem2-1-2 {n} = { }0

ここでCtrl+c, Ctrl+c, n, Enterすると引数nについて場合分けを行うということになり、引数の定義（この場合ペアノ自然数の定義）に従って場合分けをやってくれる。

theorem2-1-2 {zero} = { }0
theorem2-1-2 {suc n} = { }1

この状態から2つのHoleに対してCtrl+c, Ctrl+aで自動証明してくれる。

定理2.2

定理2.2は加算の結果が一意であることを示す。

theorem2-2 : ∀ {n1 n2 n3 n4 : ℕ}
  → NatJudgement (n1 plus n2 is n3)
  → NatJudgement (n1 plus n2 is n4)
    ----------------
  → n3 ≡ n4

theorem2-2 {zero} {_} {_} {_} P-ZERO P-ZERO = refl
theorem2-2 {suc _} {_} {_} {_} (P-SUCC d1) (P-SUCC d2) =
  cong suc (theorem2-2 d1 d2)

これも証明の過程を見ていこう。まずCtrl+c, Ctrl+c, Enterを繰り返すと、ここまで行く。

theorem2-2 {n1} {n2} {n3} {n4} x x₁ = { }0

ここでいったんx₁をASCIIの範囲の文字に直しておく。これはユニコード文字が含まれているとその引数を場合分けしたいときにCtrl+c, Ctrl+cに続けて変数名を入力できないためだ。

theorem2-2 {n1} {n2} {n3} {n4} x y = { }0

n1で場合分けする。

theorem2-2 {zero} {n2} {n3} {n4} x y = { }0
theorem2-2 {suc n1} {n2} {n3} {n4} x y = { }1

1つ目のHoleに移動してCtrl+c, Ctrl+c, xでxを場合分けすると次のようになる。

theorem2-2 {zero} {n2} {n3} {n4} P-ZERO y = { }0
theorem2-2 {suc n1} {n2} {n3} {n4} x y = { }1

場合分けが増えていないが、これは1つ目のケースではP-ZEROしかありえないということをAgdaが推論してくれたためだ。残りについても行うとこうなる。

theorem2-2 {zero} {n2} {.n2} {.n2} P-ZERO P-ZERO = { }0
theorem2-2 {suc n1} {n2} {.(suc _)} {.(suc _)} (P-SUCC x) (P-SUCC y) = { }1

ここで1つ目のHoleに移動してCtrl+c, Ctrl+,を押すとGoalがn2 ≡ n2であることがわかる。 ≡の左右が同じ値であるような型については常にreflをエビデンスとして与えることができる。 Ctrl+c, Ctrl+aでも埋めてくれる。

theorem2-2 {zero} {n2} {.n2} {.n2} P-ZERO P-ZERO = refl

2つ目のHoleに移動してCtrl+c, Ctrl+,を押すとこのような表示になる。

Goal: suc n₃ ≡ suc n₄
————————————————————————————————————————————————————————————
y : NatJudgement (n1 plus n2 is n₄)
x : NatJudgement (n1 plus n2 is n₃)

ここでxとyをtheorem2-2に再帰的に適用すればn₃ ≡ n₄が手に入ることがわかる。 n₃ ≡ n₄からsuc n₃ ≡ suc n₄を得るにはcongを使うことができる。 cong f x≡yの形で、x≡yの両辺に関数fを適用した等式を作ることができる。以上を総合すると次のように書けばいいことになる。

theorem2-2 {suc n1} {n2} {.(suc _)} {.(suc _)} (P-SUCC x) (P-SUCC y) =
  cong suc (theorem2-2 x y)

定理2.3 加算の閉包性

定義2.3は自然数の加算の結果として何かしらの自然数が存在すること。数学用語でいえば「閉じている」ということを証明する。

theorem2-3 : ∀ {n1 n2 : ℕ}
    ----------------
  → ∃[ n3 ] (NatJudgement (n1 plus n2 is n3))

theorem2-3 {zero} {n2} = ⟨ n2 , P-ZERO ⟩
theorem2-3 {suc n1} {n2} with theorem2-3 {n1} {n2}
...                         | ⟨ n , d ⟩ = ⟨ suc n , P-SUCC d ⟩

ここではAgdaの存在量化の構文を使って型を書いている。 ⟨ n2 , P-ZERO ⟩ は ∃[ n3 ] (NatJudgement (n1 plus n2 is n3)) 型の値なのである。 Agdaの値とはその型が表現する命題のエビデンスとして提示するものだった。そしてある値n3が存在することをエビデンスとして示すためにはその具体的な値を構成して提示する必要がある。。そういうわけでAgdaの存在量化型 ∃[ x ] P xの値は、値xとP xの組ということになる。

最初の場合わけではn1=0だから、PはNatJudgement 0 plus n2 is n3である。この型の値はP-ZEROコンストラクタで構築することができるが、そのときNatJudgement 0 plus n2 is n2となるから、提示したかったn3とはn2のことである。

2つ目の場合わけではwithを使っている。withは関数定義以外の場所でパターンマッチを行いたいときに用いる。再帰的にtheorem2-3を呼ぶと組が得られるが、それを分解して取り出して使いたいのでパターンマッチをする必要がある。

ところでこの証明を

theorem2-3 = ?

から初めてCtrl+c, Ctrl+c, Enterするとこうなる。

proj₁ theorem2-3 = { }0
proj₂ theorem2-3 = { }1

これは組の片方ずつを別々に書いた表現なのだが、ちょっとわかりにくいので手動で

theorem2-3 = ⟨ ? , ? ⟩

と書いてしまったほうがよい。この場合最後に使うのは組のコンストラクタであるとわかっているからとりあえずそれを書いておいて、コンストラクタを適用する値はHoleにしておいて後回しにできる。

また中括弧引数も何故かこの状態から空欄Enterでは補完してくれないのでCtrl+c, Ctrl+c, n1とCtrl+c, Ctrl+c, n2で補完する（あるいはこれも手で書いてしまう）。

theorem2-3 {n1} {n2} = ⟨ { }0 , { }1 ⟩

定理2.4 加算の可換性

次の定理2.4は加算の可換性を証明する。補題を経由して証明している。

-- +-succʳ
lemma2-4 : ∀ {n1 n2 n3 : ℕ}
  → NatJudgement (n1 plus n2 is n3)
    ----------------
  → NatJudgement (n1 plus suc n2 is suc n3)
lemma2-4 {zero} {n2} {.n2} P-ZERO = P-ZERO
lemma2-4 {suc n1} {n2} {suc n3} (P-SUCC d) = P-SUCC (lemma2-4 d)

-- +-comm
theorem2-4 : ∀ {n1 n2 n3 : ℕ}
  → NatJudgement (n1 plus n2 is n3)
    ----------------
  → NatJudgement (n2 plus n1 is n3)

theorem2-4 {zero} {n2} {.n2} P-ZERO = theorem2-1-2
theorem2-4 {suc n1} {n2} {suc n3} (P-SUCC d) = lemma2-4 (theorem2-4 d)

定理2.5 加算の結合性

定義2.5は次のような命題の証明である。

theorem2-5 : ∀ {n1 n2 n3 n4 n5 : ℕ}
  → NatJudgement (n1 plus n2 is n4)
  → NatJudgement (n4 plus n3 is n5)
    ----------------
  → ∃[ n6 ] (NatJudgement (n2 plus n3 is n6)
           × NatJudgement (n1 plus n6 is n5))

これは何を言っているかちょっとわかりにくいのだが、加算の結合性を表している。つまり (n1 + n2) + n3 ならば n1 + (n2 + n3) であるということを中間的な変数を使って表している。ここで使っている × は命題の論理積を表す型である。この型の値はそれぞれの命題の値の組である。

lemma2-5-1 : ∀ {n1 n2 : ℕ}
  → n2 ≡ n1
    -------
  → NatJudgement (0 plus n1 is n2)

lemma2-5-1 refl = P-ZERO

lemma2-5-2 : ∀ {n1 n2 n3 n4 n5 n6 : ℕ}
  → NatJudgement (n1 plus n2 is n3)
  → NatJudgement (n4 plus n2 is n5)
  → NatJudgement (n4 plus n3 is n6)
    ----------------
  → NatJudgement (n1 plus n5 is n6)

lemma2-5-2 {n1} {n2} {n3} {zero} {.n2} {.n3} d1 P-ZERO P-ZERO = d1
lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4 -- +-comm
... | d5 with P-SUCC d5
... | d6 with theorem2-4 d6 -- +-comm
... | d7 = d7

-- +-assoc
theorem2-5 : ∀ {n1 n2 n3 n4 n5 : ℕ}
  → NatJudgement (n1 plus n2 is n4)
  → NatJudgement (n4 plus n3 is n5)
    ----------------
  → ∃[ n6 ] (NatJudgement (n2 plus n3 is n6)
           × NatJudgement (n1 plus n6 is n5))

theorem2-5 {zero} {n2} {n3} {.n2} {n5} P-ZERO d2 with theorem2-3 {n2} {n3}
... | ⟨ n6 , d ⟩ = ⟨ n6 , ⟨ d , lemma2-5-1 (theorem2-2 d2 d) ⟩ ⟩
theorem2-5 {suc n1} {n2} {n3} {n4} {n5} d1 d2 with theorem2-3 {n2} {n3}
... | ⟨ n6 , d ⟩ = ⟨ n6 , ⟨ d , lemma2-5-2 d1 (theorem2-4 d) (theorem2-4 d2) ⟩ ⟩

withのパターンマッチは主に構造を持つデータ（組や場合分けのあるデータ）を取り出すときに使うが、lemma2-5-2では単純な値をパターンマッチで受けている。ここを少し説明したい。

Agdaで証明を書くとき、普通に関数適用の構文で書くと、「最後に適用される関数・コンストラクタ」を最初に書くことになる。これは証明の末尾から遡って考えるということだ（このときまだわかっていない部分はHoleにすることができる）。

Goal: Z
————————————————————————————————————————————————————————————
x : X
y : Y

例えばこういう文脈だったとしてZ型を構築できるのは何だろうと考えて、それが例えばZConsというコンストラクタだと思ったら

_ = ZCons ?

と書いておく。Holeが新しいGoalになるからそこからまた遡る。

しかし証明を順方向に考えたいときもある。手元にあるxとyに何かを適用してZ型の値に近づけていけないだろうかということだ。こういう思考モードのときにはwithでその関数適用をしておくと手持ちの駒を増やしていくことができる。

lemma2-5-2の2つ目の場合分けでは最初このような文脈になる。

lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) = { }0

Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)

帰納を使うほうの場合分けだからとりあえず再帰をしてみようと思ってこのように書く。

lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 = { }0

すると再帰適用の結果が新たな前提として利用できるようになる。

Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d4 : NatJudgement (n1 plus n5 is n6)
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)

Goalを見ると、n5とn6にsucをつけたものが必要になりそうだ。項にsucをつけるのはP-SUCCが使えそうだが、P-SUCCの形式にアダプトするにはd4をひっくり返した形式でなければならない。

lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4 -- +-comm
... | d5 = { }0

Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
d5 : NatJudgement (n5 plus n1 is n6)
d4 : NatJudgement (n1 plus n5 is n6)

得られた NatJudgement (n5 plus n1 is n6) にP-SUCCを適用すると NatJudgement (suc n5 plus n1 is suc n6) が得られる。

lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4
... | d5 with P-SUCC d5
... | d6 = { }0

Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
d4 : NatJudgement (n1 plus n5 is n6)
d6 : NatJudgement (suc n5 plus n1 is suc n6)
d5 : NatJudgement (n5 plus n1 is n6)

ここまで来ると NatJudgement (suc n5 plus n1 is suc n6) をひっくり返せばGoalが得られることがわかる。もう一度可換性を使う。

lemma2-5-2 {n1} {n2} {n3} {suc n4} {suc n5} {suc n6} d1 (P-SUCC d2) (P-SUCC d3) with lemma2-5-2 d1 d2 d3
... | d4 with theorem2-4 d4
... | d5 with P-SUCC d5
... | d6 with theorem2-4 d6 -- +-comm
... | d7 = { }0

Goal: NatJudgement (n1 plus suc n5 is suc n6)
————————————————————————————————————————————————————————————
d3 : NatJudgement (n4 plus n3 is n6)
d2 : NatJudgement (n4 plus n2 is n5)
d1 : NatJudgement (n1 plus n2 is n3)
d4 : NatJudgement (n1 plus n5 is n6)
d5 : NatJudgement (n5 plus n1 is n6)
d7 : NatJudgement (n1 plus suc n5 is suc n6)
d6 : NatJudgement (suc n5 plus n1 is suc n6)

d7がGoalそのものだからCtrl+c, Ctrl+aで自動補完できる。このようにwithを連鎖させると順方向で証明を進めやすくなる。

定理2.6

定理2.6は乗算の結果が一意であることを示す。

theorem2-6 : ∀ {n1 n2 n3 n4 : ℕ}
  → NatJudgement (n1 times n2 is n3)
  → NatJudgement (n1 times n2 is n4)
    ----------------
  → n3 ≡ n4

theorem2-6 {zero} {n2} {.0} {.0} T-ZERO T-ZERO = refl
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
      with theorem2-6 y1 x1
... | refl
      with theorem2-2 y2 x2
... | refl = refl

reflばかりになるのがちょっとわかりにくい。まずCtrl+c, Ctrl+cの場合分けで次の状態まで行く。

theorem2-6 {zero} {n2} {.0} {.0} T-ZERO T-ZERO = { }0
theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2) = { }1

１つ目は自動で証明できる。2つ目の文脈は次のようになる。

Goal: n3 ≡ n4
————————————————————————————————————————————————————————————
y2 : NatJudgement (n2 plus n₄ is n4)
y1 : NatJudgement (n1 times n2 is n₄)
x2 : NatJudgement (n2 plus n₃ is n3)
x1 : NatJudgement (n1 times n2 is n₃)

x1とy1に再帰的にtheorem2-6を適用できそうだということがわかる。

theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
      with theorem2-6 y1 x1
... | x = { }0

Goal: n3 ≡ n4
————————————————————————————————————————————————————————————
y2 : NatJudgement (n2 plus n₄ is n4)
x2 : NatJudgement (n2 plus n₃ is n3)
x  : n₄ ≡ n₃
y1 : NatJudgement (n1 times n2 is n₄)
x1 : NatJudgement (n1 times n2 is n₃)

ここで次に目をつけたいのはx2とy2に定理2.2を適用できないかということだ。すでにn₄ ≡ n₃であるということはわかっているが、 x2とy2の形式はtheorem2-2と一致していないのでこのままでは適用できない。

そこでCtrl+c, Ctrl+c, xでxを場合分けする。するとこうなる。

theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
      with theorem2-6 y1 x1
... | refl = { }0

Goal: n3 ≡ n4
————————————————————————————————————————————————————————————
y2 : NatJudgement (n2 plus n₃ is n4)
x2 : NatJudgement (n2 plus n₃ is n3)
y1 : NatJudgement (n1 times n2 is n₃)
x1 : NatJudgement (n1 times n2 is n₃)

等式のエビデンスはつねにreflなのでxはreflになった。それとともに x : n₄ ≡ n₃ も文脈から消えてx2とy2が同じ形式になってくれた。このように等式で終わるエビデンスはパターンマッチを使ってreflで受けるようにするとよい（そうでなければsubstを使って式変形することになるが、これは書きにくい）。

定理2.2を同様に適用すると次のようになるが、この時点でGoalがn3 ≡ n3になるのでreflを与えれば良いことがわかる。

theorem2-6 {suc n1} {n2} {n3} {n4} (T-SUCC x1 x2) (T-SUCC y1 y2)
      with theorem2-6 y1 x1
... | refl
      with theorem2-2 y2 x2
... | refl = { }0

定理2.7 乗算の閉包性

定理2.7は乗算が閉じていることを示す。

theorem2-7 : ∀ {n1 n2 : ℕ}
    ----------------
  → ∃[ n3 ] (NatJudgement (n1 times n2 is n3))

theorem2-7 {zero} {n2} = ⟨ zero , T-ZERO ⟩
theorem2-7 {suc n1} {n2} with theorem2-7 {n1} {n2}
... | ⟨ n4 , d1 ⟩ with theorem2-3 {n2} {n4}
...   | ⟨ n3 , d2 ⟩ = ⟨ n3 , T-SUCC d1 d2 ⟩

定理2.8 乗算の右ゼロと左ゼロ

定理2.8は左右に0をかけると0になることを示す。

-- *-zeroˡ
theorem2-8-1 : ∀ {n : ℕ}
    ----------------
  → NatJudgement (0 times n is 0)

theorem2-8-1 {n} = T-ZERO

theorem2-8-2 : ∀ {n : ℕ}
    ----------------
  → NatJudgement (n times 0 is 0)

-- *-zeroʳ
theorem2-8-2 {zero} = T-ZERO
theorem2-8-2 {suc n} = T-SUCC theorem2-8-2 P-ZERO

定理2.9 乗算の可換性

定理2.9は乗算の交換法則の証明である。これは難しかった。補題として乗算の右辺にsucをつけるもの（T-SUCCとは逆）を証明する必要があるのだが、この証明自体苦労した。

-- *-succʳ
lemma2-9 : ∀ {n1 n2 n3 n4 : ℕ}
  → NatJudgement (n1 times n2 is n3)
  → NatJudgement (n1 plus n3 is n4)
  ----------------
  → NatJudgement (n1 times suc n2 is n4)

この証明について、式を変形していく発想で行ったので、その注釈をつけながら見ていく。

lemma2-9 {zero} {n2} {.0} {.0} T-ZERO P-ZERO = T-ZERO
lemma2-9 {suc n1} {n2} {n3} {suc n4}
         (T-SUCC {n1} {n2} {m1} {n3} n1×n2=m1 n2+m1=n3)
         (P-SUCC n1+n3=n4)

n1で場合分けするが1つ目は容易なので説明を省く。 2つ目についてn1をsuc n1、n4をsuc n4と置き換えたので、補題の型から、次の式を出発点とすることになる。

      suc n1 + (suc n1 × n2)
             |         |
         suc n4        n3

前提の1つ目の乗算をT-SUCCで分解したことにより、次の式が得られる。

      suc n1 + (n2 + (n1 × n2))
             |     |     |
         suc n4    n3    m1

前提の2つ目の加算をP-SUCCで分解したことにより、次の式を得る。

          n1 + (n2 + (n1 × n2))
             |     |     |
             n4    n3    m1

まずはこの式全体をひっくり返す。

      with theorem2-4 n1+n3=n4 -- +-comm
... | n3+n1=n4

このような式になったということだ。

          (n2 + (n1 × n2)) + n1
              |     |      |
              n3    m1     n4

結合法則を使って括弧の対応を変える。

      with theorem2-5 n2+m1=n3 n3+n1=n4 -- +-assoc
... | ⟨ m2 , ⟨ m1+n1=m2 , n2+m2=n4 ⟩ ⟩

           n2 + ((n1 × n2) + n1)
              |      |     |
              n4     m1    m2

内側の加算をひっくり返す。

      with theorem2-4 m1+n1=m2 -- +-comm
... | n1+m1=m2

           n2 + (n1 + (n1 × n2))
              |     |     |
              n4    m2    m1

こうすると補題を再帰適用することができるようになる。

      with lemma2-9 n1×n2=m1 n1+m1=m2 -- *-succʳ
... | n1×suc_n2=m2

           n2 + (n1 × suc 2)
              |     |
              n4    m2

全体にP-SUCCを適用する。

      with P-SUCC n2+m2=n4
... | suc_n2+m2=suc_n4

するとこの式が得られる。

       suc n2 + (n1 × suc 2)
              |     |
          suc n4    m2

ここまで来るとT-SUCCと手持ちの式を使ってGoalを作ることができる。

      = T-SUCC n1×suc_n2=m2 suc_n2+m2=suc_n4

       suc n1 × suc n2
              |
          suc n4

この補題を使うともともと証明したかった乗算の交換法則を証明することができる。

-- *-comm
theorem2-9 : ∀ {n1 n2 n3 : ℕ}
  → NatJudgement (n1 times n2 is n3)
    ----------------
  → NatJudgement (n2 times n1 is n3)

theorem2-9 {zero} {n2} {zero} T-ZERO = theorem2-8-2 -- *-zeroʳ
theorem2-9 {suc n1} {n2} {n3} (T-SUCC {n1} {n2} {m3} d1 d2)
      with theorem2-9 d1
... | d3 = lemma2-9 d3 d2

定理2.10 乗算の結合性

加算乗算システムについての最後のメタ定理として、乗算の結合性を証明する。だが、証明しようとすると加算と乗算の分配法則が必要なことに気づくのでまずはそれからだ。

補題加算と乗算の分配

-- *-distrib-+
lemma2-10 : ∀ {n1 n2 n3 n4 n5 : ℕ}
  → NatJudgement (n1 plus n2 is n4)
  → NatJudgement (n4 times n3 is n5)
    -------------------------------
  → ∃[ n6 ] (∃[ n7 ] (NatJudgement (n1 times n3 is n6)
                    × NatJudgement (n2 times n3 is n7)
                    × NatJudgement (n6 plus n7 is n5)))

lemma2-10 {zero} {n2} {n3} {.n2} {n5} P-ZERO n2×n3=n5
  = ⟨ 0 , ⟨ n5 , ⟨ T-ZERO , ⟨ n2×n3=n5 , P-ZERO ⟩ ⟩ ⟩ ⟩
lemma2-10 {suc n1} {n2} {n3} {suc n4} {n5}
          (P-SUCC {n1} {n2} {n4} n1+n2=n4)
          (T-SUCC {n4} {n3} {m1} {n5} n4×n3=m1 n3+m1=n5)

場合分けの2つ目の出発点とゴールは次のようになる。

  (suc n1 + n2) × n3 → (suc 1 × n3) + (n2 × n3)
          |     |             |     |     |
      suc n4    n5            n6    n5    n7

P-SUCCとT-SUCCの分解によって次の式が得られる。

n3 + ((n1 + n2) × n3)
   |      |     |
   n5     n4    m1

さっそくだが右側の部分に再帰的に分配法則を適用する。

      with lemma2-10 n1+n2=n4 n4×n3=m1
... | ⟨ m2 , ⟨ n7 , ⟨ n1×n3=m2 , ⟨ n2×n3=n7 , m2+n7=m1 ⟩ ⟩ ⟩ ⟩

n2 × n3はゴールでいうn7に対応するからこの時点でそのように名前をつけた。

n3 + ((n1 × n3) + (n2 × n3))
   |      |     |     |
   n5     m2    m1    n7

ゴールではn2 × n3が独立して現れるからこれを外に出したい。結合法則を利用したいところだが、定義2.5とは向きが異なるので交換法則を使って形を合わせる。

      with theorem2-4 n3+m1=n5
... | m1+n3=n5

((n1 × n3) + (n2 × n3)) + n3
     |     |     |      |
     m2    m1    n7     n5

      with theorem2-4 m2+n7=m1
... | n7+m2=m1

((n2 × n3) + (n1 × n3)) + n3
     |     |     |      |
     n7    m1    m2     n5

      with theorem2-5 n7+m2=m1 m1+n3=n5
... | ⟨ n6 , ⟨ m2+n3=n6 , n7+n6=n5 ⟩ ⟩

(n2 × n3) + ((n1 × n3) + n3)
    |     |      |     |
    n7    n5     m2    n6

これでn2 × n3が外に出せた。直観的にn2 × n3じゃない方の部分はGoalのn6になるはずなのでそういう名前にしておく。

この右側の部分はT-SUCCが使えそうな形に見えるがやはり向きが合わないので入れ替えて合わせる。

      with theorem2-4 m2+n3=n6
... | n3+m2=n6

(n2 × n3) + (n3 + (n1 × n3))
    |     |     |     |
    n7    n5    n6    m2

      with T-SUCC n1×n3=m2 n3+m2=n6
... | suc_n1×n3=n6

(n2 × n3) + (suc n1 × n3)
    |     |         |
    n7    n5        n6

n6をGoalの形式にすることができた。全体をひっくり返せばGoalになる。

      with theorem2-4 n7+n6=n5
... | n6+n7=n5 = ⟨ n6 , ⟨ n7 , ⟨ suc_n1×n3=n6 , ⟨ n2×n3=n7 , n6+n7=n5 ⟩ ⟩ ⟩ ⟩

これで乗算の結合性を証明する準備ができた。

乗算の結合性

-- *-assoc
theorem2-10 : ∀ {n1 n2 n3 n4 n5 : ℕ}
  → NatJudgement (n1 times n2 is n4)
  → NatJudgement (n4 times n3 is n5)
    ----------------
  → ∃[ n6 ] (NatJudgement (n2 times n3 is n6)
           × NatJudgement (n1 times n6 is n5))

この命題はこういうことを言っている。

(n1 × n2) × n3 → n1 × (n2 × n3)
    |     |         |     |
    n4    n5        n5    n6

例によってn1で場合分けする。

theorem2-10 {zero} {n2} {n3} {zero} {zero} T-ZERO T-ZERO
      with theorem2-7 {n2} {n3}
... | ⟨ n , d ⟩ = ⟨ n , ⟨ d , T-ZERO ⟩ ⟩
theorem2-10 {suc n1} {n2} {n3} {n4} {n5} (T-SUCC {n1} {n2} {m1} {n4} n1×n2=m1 n2+m1=n4) n4×n3=n5

2つめの場合分けの出発点とゴールは次の通り。

(suc n1 × n2) × n3 → suc n1 × (n2 × n3)
        |     |             |     |
        n4    n5            n5    n6

T-SUCCの分解でこの式が得られる。

(n2 + (n1 × n2)) × n3
    |     |      |
    n4    m1     n5

早速分配法則を使う。

      with lemma2-10 n2+m1=n4 n4×n3=n5
... | ⟨ n6 , ⟨ m2 , ⟨ n2×n3=n6 , ⟨ m1×n3=m2 , n6+m2=n5 ⟩ ⟩ ⟩ ⟩

(n2 × n3) + ((n1 × n2) × n3)
    |     |      |     |
    n6    n5     m1    m2

右側にもn2 × n3を作るとよさそうだ。そこで結合法則を再帰的に適用する。

      with theorem2-10 n1×n2=m1 m1×n3=m2
... | ⟨ m3 , ⟨ n2×n3=m3 , n1×m3=m2 ⟩ ⟩

(n2 × n3) + (n1 × (n2 × n3))
    |     |     |     |
    n6    n5    m2    m3

ここでm3は明らかにn6と同じなのだがAgdaはそれを認識していない。定理2.6を使って同じであることを教えてあげる。

     with theorem2-6 n2×n3=n6 n2×n3=m3
... | refl

最後に全体にT-SUCCを適用すればGoalが作れる。

      with T-SUCC n1×m3=m2 n6+m2=n5
... | suc_n1×n6=n5 = ⟨ n6 , ⟨ n2×n3=n6 , suc_n1×n6=n5 ⟩ ⟩

2020-08-16 21:29 nice!(0) コメント(0)

nice! 0

コメントを書く

Agdaによる「プログラミング言語の基礎..｜Agdaによる「プログラミング言語の基礎.. ブログトップ

日	月	火	水	木	金	土
	1	2	3	4	5	6
7	8	9	10	11	12	13
14	15	16	17	18	19	20
21	22	23	24	25	26	27
28	29	30

RSS1.0 | RSS2.0

Rainy Day Codings

Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理　[Agda] [編集]

定理2.1 加算の単位元

定理2.2

定理2.3 加算の閉包性

定理2.4 加算の可換性

定理2.5 加算の結合性

定理2.6

定理2.7 乗算の閉包性

定理2.8 乗算の右ゼロと左ゼロ

定理2.9 乗算の可換性

定理2.10 乗算の結合性

補題加算と乗算の分配

乗算の結合性

nice! 0

コメント 0

コメントを書く

ether さん

--

カレンダー

記事検索

最新記事一覧

カテゴリー

最近のコメント

最近トラックバックされた記事

ether さんの記事をnice!と思った人 (全27人)

シリーズ記事

Essentials of Programming Languages (EOPL)

ScalaCheck を試す

OCaml vs. Scala

Tcl 8.5 の新機能

Rainy Day Codings

Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理 [Agda] [編集]

定理2.1 加算の単位元

定理2.2

定理2.3 加算の閉包性

定理2.4 加算の可換性

定理2.5 加算の結合性

定理2.6

定理2.7 乗算の閉包性

定理2.8 乗算の右ゼロと左ゼロ

定理2.9 乗算の可換性

定理2.10 乗算の結合性

補題 加算と乗算の分配

乗算の結合性

nice! 0

コメント 0

コメントを書く

ether さん

--

カレンダー

記事検索

最新記事一覧

カテゴリー

最近のコメント

最近トラックバックされた記事

ether さんの記事をnice!と思った人 (全27人)

シリーズ記事

Essentials of Programming Languages (EOPL)

ScalaCheck を試す

OCaml vs. Scala

Tcl 8.5 の新機能

Agdaによる「プログラミング言語の基礎概念」 - 導出システムNatのメタ定理　[Agda] [編集]

補題加算と乗算の分配