Software Engineering Lecture s04
Menu
Agda
Agda は Curry Howard 対応にそった定理証明支援システム。これを使った簡単な証明を学ぶ。
Agda の install の方法
Mac 上では Homebrew を使うのが良いそうです。
brew install agda/opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/standard-library.agda-lib とかに入るので
echo standard-library > ~/.agda/defaults echo /opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/standard-library.agda-lib > ~/.agda/libraries
VSCode で使う
Emacs を使う場合
brew tap caskroom/cask brew cask install emacsなどになるので、~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。
agda.el を installGUI 側で使わないと文字化けすることがあるようです。ews.el とか。
C-C control と C を同時に押す M-X esc を押してから X を押すC-X C-F で、Agda1.agda file を開けます。
M-X help-for-help M で、Agda のコマンドの一覧が出ます。C-X o で buffer を切り替えて読みます。
neovim で使う
普通の vim では動かないです。プログラムを書く
Haskell と似たような、それでいて少し違う。そういうもので記述していきます。agda1.agda というファイルを開けます。
module agda1 where
と先頭に書きます。ファイル名と同じでないとだめです。
注意
: の前後は空白を開ける
全角スペースが入らないように気を付ける。
indent で、前の行と繋げる
空白を空けないと一つのワードになる
-> の前後にも空白が必要
-> の優先順位 a -> b -> c は a -> ( b -> c )
() と {} は特別扱いされる
C-C C-L で構文チェック。親切なエラーメッセージに従って直そう。
ex. Parse Error
以下では、この例題を使う。
A → B → A
A → B → A の証明を思い出そう。 A → B → A は、 A → ( B → A ) だった。Goal を一番下に書き、線を引く。
?
----------------
A → B → A
→があるので、→I を使う。つまり、結論部分を上に書く。仮定を使えるようになる。
B → A
---------------- →I
A → B → A
まだ→があるので、繰り返す。
A
---------------- →I2
B → A
---------------- →I1
A → B → A
A → B → A に l1 という名前を付ける。l1 の型が A → B → A である。l1 は証明に相当するλ式を値として持つ。
l1 = λ (x : A ) → λ (y : B ) → xこの時に最後の x は、A という型を持つ項であれば何でも良い。例えば、 ( λ x → x ) x でも良い。つまり、論理式に対する証明は一意ではない。
Agada での A → B → A の証明
まず、A とか B は何かという問題がある。Agda には基本の型として Set がある。A と B が Set であると仮定する。
postulate A B : Set
これは A B という変数が Set という型を持つことを仮定する。
l1 : A → B → A
これは l1 が A → B → A という型を持つことを示す。: は前後に空白がある必要がある。→は -> でも良い。
これだけだと、l1 に値がないと文句を言われる
l1 = ?
とする。ここで emacs で、C-C C-L すると、
?0 : A → B → Aと Agda の buffer に表示される。つまり、この ? の部分に、この型を持つλ項を入れれば証明が終わる。
l1 = λ x → λ y → x
とすれば良い。C-C C-L とすると何も表示されないので、証明が終わったことがわかる。
l1 = λ x → λ y → y
とすると、
B !=< A of type Set
when checking that the expression y has type A
と言われる。y は型Bを持つので、A が要求されているのと合っていない。
暗黙の変数 (implicit variable )
A B を postulate しないで、λ式に直接書くこともできる。この時に、{} で表される暗黙の変数を使ってみよう。
l1' : {A B : Set } → A → B → A
l1' = λ x → λ y → x
{A B : Set } は入力だが、λ式で明示しなくても良い。
l1' = λ { A B } → λ x → λ y → x
と明示しても良い。
Haskell と同じく、引数をパターンとして書くこともできる。
l1 x y = x
暗黙の変数があれば、
l1 {A} {B} x y = x
とすることができる。
矢印の Elimination
次に →を削除する E→ の推論の例を示そう。
l3 : A → ( A → B ) → B
これを証明するためには、入力が二つ必要である。(I→)
l3 x y = ?
結果はBを返す必要があるが、x も y も B ではない。しかし、y は A → B で B を返す関数である。なので、
l3 x y = y ?
とすることができる。y の入力は Aという型である必要がある。x がちょうど型Aなので、それを使う。
l3 x y = y x
λ式で書けば、
l3' = λ x → λ y → y x
A と B がSetだという仮定を暗黙の変数を使って入れてみよう。
Haskell との違い
f0 : {t : Set } -> t -> t
f0 t = ?
f1 : {t t1 : Set } -> t -> (t1 -> t) -> t
f1 = ?
f2 : {t t1 t2 : Set } { a : t2} -> (t2 -> t1) -> (t1 -> t) -> t
f2 = ?
f3 : {t : Set } -> t -> t -> t
f3 = ?
f4 : {t : Set } {a : t } -> ( t -> t ) -> t
f4 = ?
{a : t} などで、足りない入力を補える。
Product
Haksell では直積を表すには data を使ったが、Agda では record を使う。
record _∧_ A B : Set where
constructor _×_
field
proj1 : A
proj2 : B
_ は infix operator の引数を表す。型Aと型Bの直積を作るには、
p1 : A -> B -> A ∧ B
p1 a b = a × b
の様にする。直積の型を表す∧と、直積の値を表す × の二種類が必要になる。
この式は直積の導入(I∧)に相当する。
A B
---------------
A ∧ B
E∧ は、proj1 と proj2 を使う。
open _∧_
p2 : A ∧ B -> A
p2 axb = proj1 axb
axb は、一つの変数である。Agda では空白を入れないと演算子として認識されない。
reocrd を open しないで使いたければ、
p2' : A ∧ B -> A
p2' axb = _∧_.proj1 axb
とする。
porj1 は A ∧ B -> A という型を持つ関数だが、proj1 : A と書かれている。 A ∧ B はrecord 記述中では省略されていると考えても良い。
constructor を使わずに、直接 reocrd を作成することもできる。
p1' : A -> B -> A ∧ B
p1' a b = record { proj1 = a ; proj2 = b }
なので、constructor の定義は必須ではない。
Sum
この論理では普通の論理和は使わず、排他的論理和を使う。A ∨ B はAとBが同時に成り立つことはない。Haskell では data を使って Sum も表していた。Agad では reocrd と区別して data を使う。
data _∨_ A B : Set where
or1 : A → A ∨ B
or2 : B → A ∨ B
構文は record に似ているが、or1 と or2 は constructor である。なので、data を返す必要がある。or1 は A → A ∨ B
という型を持つ関数である。constructor を使って、∨I を使ってみよう。
o1 : B → A ∨ B
o1 x = or2 x
o2 : A → A ∨ B
o2 x = or1 x
これは、B → A ∨ B という論理式の証明になっている。データ型的には、or1 と or2 というtagの付いたunionを作っている。
SumのEliminationは少し複雑で、or1 と or2 の場合分けの証明になる。
o3 : A ∨ A → A
o3 (or1 x) = x
o3 (or2 x) = x
(or1 x) はパターンマッチで、x はλ x のxと同じ scope を持つ局所変数(引数)である。or1 と or2 が同時に起きることはない。
問題4.1
Excercise 4.1 以下の論理式の証明図に対応する lemma を Agda で作れ。
(1) A -> A (2) A -> (B -> A) (3) (A ∧ (A -> B)) -> B (4) B -> (B ∧ (A -> B)) (5) A -> B -> ( A ∨ B ) (6) B -> ( A ∨ (B -> A) ) -> A
等式
Agda ではどんなことが証明できるのだろうか?
1 + 1 = 2
ぐらいは証明したい。つまり、1 や 2 そして、+ と = を Agda で表すことを行う必要がある。
等式は、
x
----------------
x == x
で導入されるべきだろう。これは、== が constructor だということを示している。record ではなく、data を使う。
data _==_ {A : Set} : A → A → Set where
refl : {x : A} → x == x
== は二引数を持つので、A → A → Set という型を持つ。その constructor は refl ( reflection の略 )で、x を暗黙に受けとって x == x を返す。
e1' : ( x : A ) → x == x
e1' x = refl
問題は elimination だが、
x == y
----------------
y == x
は成立して欲しい。
sym' : x == y → y == x
sym' = ?
ということになる。これは x と y の型がないと怒られるので、
e2 : (x y : A ) → x == y → y == x
e2 = ?
としよう。 入力が三つなので、
sym' : x == y → y == x
sym' x y eq = ?
y == x を作って返せばよいのだが、
sym' x y eq = refl
ではうまくいかない? (どんなエラーが返るか、調べてみよ)
eq は x == y という型なのでパターンで受けることができる。
sym' x y refl = refl
これでもうまくいかない。
x != y of type A
when checking that the pattern refl has type x == y
確かに、x == y である必要がある。
sym' x x refl = refl
とすると、パターンに同じ変数があると怒られる。どうすれば良いのか?
e2 : (x y : A ) → x == y → y == x
e2 x .x refl = refl
と . を使うと入力にある同じ変数を取り扱うことができる。
(x y : A ) を { x y : A }として隠してやると、
e2' : {x y : A } → x == y → y == x
e2' refl = refl
と綺麗に書くことができる。あまり変数を明示しない方が証明が綺麗になることが多い。
問題4.2
Excercise 4.2 以下をAgdaで証明せよ
(1) { x y z : A } → x == y → y == z → x == z
(2) {A B : Set } { x : A } { y : A } { f : A → B } → x == y → f x == f y
(3) {A B : Set } { x : A } { y : A } { f : A → B } → f x == f y → x == y
自然数
自然数は zero から始まって、その次の1、そして、その次の2と、ずーっと続く、つまり、zero と「何かのその次」(successor)の二種類からなる。つまり、data でかける。
data Nat : Set where
zero : Nat
succ : Nat → Nat
ここで、2 は succ ( succ zero ) である。
足し算は、
_+_ : Nat → Nat → Nat
zero + x = ?
(succ x) + y = ?
と場合分けされる。
1 + 1 = 2 は以下のようになる。
nat1 : ( (succ zero ) + (succ zero ) ) == ( succ (succ zero ) )
nat1 = ?
これは入力はなく、等式を返せばよい。
nat1 : ( (succ zero ) + (succ zero ) ) == ( succ (succ zero ) )
nat1 = refl
で証明されたことになる。refl を書いて通れば、等式の証明として十分である。実際には refl は同じ項かどうかを Agda が調べることになる。同じでないものを refl で作ろうとすると Agda が文句をいう。
加算に関するいくつかの法則を証明してみよう。
lemma10 : (x : Nat) → ( zero + x ) == x
lemma10 x = refl
lemma11 : (x : Nat) → ( x + zero ) == x
lemma11 zero = refl
lemma11 (suc x) = cong suc (lemma11 x)
Nat を data の場合分けしている。
lemma11 (suc x) = cong suc (lemma11 x)
は、lemma11 の等式の両辺に S を足したものに相当することを示している。これは、数学的帰納法にもなっていて、zero の場合と、suc で n の場合から n + 1 の場合を証明していることになる。
lemma11 (suc x) = lemma11 (suc x)
は型は合っているが、証明にはならない。
Reasoning
3 + 2 + 1 = 5 + 1 = 6
みたいに等式を推論していく方法が Agda に用意されている。これは、
3 + 2 + 1 = 5 + 1
5 + 1 = 6
から、trans を使って、
3 + 2 + 1 = 6
を導けば良い。
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
ここでは == の代わりに既に ≡ が定義されているので、それを使う。
add-sym : (x y : Nat) -> x + y ≡ y + x add-sym zero zero = refl add-sym zero (suc y) = cong suc (add-sym zero y) add-sym (suc x) zero = cong suc (add-sym x zero) add-sym (suc x) (suc y) = ?ここで、
add-sym (suc x) (suc y) = begin
(suc x) + (suc y)
≡⟨ ? ⟩
(suc y) + (suc x)
∎
とできる。? に
a ≡ b
の形をした変形規則を入れていく。
≡⟨ refl ⟩は、同じ normal form を持っていることを示している。変形を丁寧にやりたい時に使う。
≡⟨⟩とも書ける。
≡⟨ cong suc (add-sym (suc x) y) ⟩で証明できるはずだが。
問題4.4
加算の反射率の証明を完成せよ。
add-sym : (x y : Nat) → ( x + y ) == ( y + x )
add-sym zero y = trans {!!} {!!}
add-sym (suc x) y = {!!}
System T
ゲーデルの System T を Agda 上に作成してみよう。