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 → AA → 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 xA と 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 ∧ BE∧ は、proj1 と proj2 を使う。
open _∧_ p2 : A ∧ B -> A p2 axb = proj1 axbaxb は、一つの変数である。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
等式
agda1.agda 等式の例題 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 = {!!}
かけ算と足し算
かけ算と足し算の交換則を Agda 上に作成してみよう。