Agda の入門の要約
Menu Menutop : Agda による圏論入門 ここで使われている例題は、
Category exercise in Agda に置いてあります。
Agda の install の方法
Homebrew を使うのが良いそうです。Emacs を先に入れます。
brew tap caskroom/cask brew cask install emacsその後、
brew install agdaGHCが入ってないなら、
brew install ghcinstall 先がどこかは、
/usr/local/Cellar/agda/2.5.2/lib/agda
などになるので、~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。
init.el GUI 側で使わないと文字化けすることがあるようです。
Terminal.app からなら、
East Asian Ambiguous Width問題と絵文字の横幅問題の修正ロケール を使うと直るようです。
いないと思うけど、xterm on X11 から使う人は、
X11 用 14dot 日本語Unicode font に、それようの eaw-xterm.el があります。
Emacs から使うので、Emacs も勉強しよう。
Emacs の使い方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 を切り替えて読みます。
cabal を使う方法
まず、 lHaskell を入れてください。 gchi が入っていれば、cabal を使って Agda を入れるのがのが簡単です。
cabal install agda
install 先がどこかは、
~/.cabal/config
の中の prefix を見るとわかります。~/.cabal/bin あたりにはいっているので、これを path に入れよう。~/.zshenv で、
path=($HOME/.cabal/bin $path)
などとすると良いでしょう。(zsh 使ってない? なんて、もったいない!!) path を通せば、
agda
で起動しますが、Emacs から使うのが普通だそうです。
起動方法
emacs から agda1.agda というファイルを開けます。
module agda1 where
と先頭に書きます。ファイル名と同じでないとだめです。
プログラムを書く
Haskell と似たような、それでいて少し違う。そういうもので記述していきます。注意
: の前後は空白を開ける
全角スペースが入らないように気を付ける。
indent には意味があります。
-> の前後にも空白が必要
C-C C-L で構文チェック。親切なエラーメッセージに従って直そう。
ex. Parse Error
Agda 入門
Agda 入門 Interactive Theorem Proving for Agda Users
これが良いようですが、λ計算全体の講義なので、結構大きいし、Agda のことは相対的に少ない感じです。
Dependently Typed Programming in Ag こちらは比較的短いのですが Emacs の操作とか ? の扱いが載ってません。ここの例題は、これから持ってきています。
Goal
Agda の特徴のこれから埋めていく部分です。{! !}
? でも良い。
Nat の例題
Agda1.agda Agda は indent に厳しいので注意が必要です。もちろん tab はだめ。空白を開けるところと開けないところをチェック。=> や -> の前後には空白を開ける。空白を開けないところは開けない。
module Agda1 where
infixl 60 _*_
infixl 40 _+_
infixr 20 _or_
-- infix ø 5 if_then_else_
data Bool : Set where
true : Bool
false : Bool
not : Bool -> Bool
not true = false
not false = true
まず、C-C C-C で、色が変わることをチェックします。エラーメッセージが出たら、構文を調べましょう。
型と値
型は、
hoge : Set
という形で宣言します。これは型です。 Set という型が基本。Set は最初から定義されています。
Set という型を持つ hoge という変数という意味。
data 型
data Bool : Set where
true : Bool
false : Bool
data 文で、新しい型を定義します。ここでは、Bool という型は、Set の一部で、
true
false
の二つの値があります。それ以外は Bool 型ではありません。
関数の定義
not : Bool -> Bool
not true = false
not false = true
Haskell と同じように pattern matching で記述します。型宣言を必ず書く必要があります。
上のファイルを読み込んで、
C-C C-N
として、mini buffer 上で、
not true
や
not false
が、正しい値を返すかどうか調べよう。
Nat
data Nat : Set where
zero : Nat
suc : Nat -> Nat
_+_ : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)
_*_ : Nat -> Nat -> Nat
zero * m = zero
suc n * m = m + (n * m)
これは自然数の演算を定義しています。1 は suc zero 、2 は suc suc zero 。
data Nat は、型を定義しているだけで、1 とか 2 は定義してません。ただ、zero が Nat ということと、x が Nat なら、suc x も Nat だということを示しているだけ。
suc zero
を C-C C-N で評価してみよう。
suc suc zero
はエラーになります。suc は引数を一つしか取らないので。
suc (suc zero)
は通るはずです。
(suc (suc (suc zero))) * (suc (suc zero))
や
(suc (suc (suc zero))) + (suc (suc zero))
を C-C C-N で評価してみよう。
zero + (suc zero)
Haskell と違って、+ を普通の関数のように、
+ zero (suc zero)
と呼び出すことはできません。
Lambda 式
lambda.agda
module lambda where
postulate A : Set
postulate B : Set
postulate f : A -> B
postulate a : A
postulate は仮定みたいなもの。a は集合Aの要素、f は集合Aから集合Bへの関数だと言っています。
b : B
b = f a
型と値の両方を定義しなければなりません。b は集合Bの要素。あるいは B という型を持つ変数。b = f a は b の値を定義しています。ここでは、関数 f の値です。f 自体は定義していません。
g : A -> A
g = \x -> x
g は、引数をそのまま返す関数です。恒等関数ともいいます。
h : A -> A
h a = a
このように書いても良いです。
postulate P : ( A -> A ) -> Set
関数を引数に取って何かを返します。
k : P g -> P h
k x = x
そういう型を持つ関数。g と h は、前に定義しました。
A2 : Set
A2 = A -> A
A3 : Set
A3 = A2 -> A2
a2 : A2
a2 = \x -> x
いろいろな恒等関数の例です。
命題論理
proposition.agda
module proposition where
postulate A : Set
postulate B : Set
集合であるA,Bを命題変数として使います。
Lemma1 : Set
Lemma1 = A -> ( A -> B ) -> B
これが証明すべき命題論理式になります。実際には式に対応する型です。
lemma1 : Lemma1
として、この型を持つ lambda 式を使えば証明したことになります。
以下のどれもが証明となり得ます。
-- lemma1 a a-b = a-b a
-- lemma1 = \a a-b -> a-b a
-- lemma1 = \a b -> b a
-- lemma1 a b = b a
product
∧ は以下の定義を使います。
record _∧_ (A B : Set) : Set where
field
and1 : A
and2 : B
record は、A と B を持つ直積で、and1 と and2 を指定した record が Constructor となる。C の struct に相当します。
lemma4 = \b -> \a -> record { and1 = b ; and2 = a }
and1 と and2 を accesor として使うことができます。
lemma5 = \b -> _^_.and2 b
これらが、∧ に関する証明(に対応するλ式)を提供します。
disjunction
disjunction は排他的和とも呼ばれる。Or のことである。C の union に相当します。
data _∨_ (A B : Set) : Set where
or1 : A -> A ∨ B
or2 : B -> A ∨ B
record 文と違い、or1 と or2 が Constructor です。
Lemma6 : Set
Lemma6 = B -> ( A ∨ B )
lemma6 : Lemma6
lemma6 = \b -> or2 b
これは、∨ の導入になっていますが、
lemma7: ( A ∨ A ) -> A
lemma7 = ?
は、どのように証明すれば良いでしょうか?
問題4.1
以下の論理式の証明図に対応する lemma を Agda で作ってください。
(1) A -> A (2) A -> (B -> ->A) (3) (A ∧ (A -> B)) -> B (4) B -> (B ∧ (A -> B))(A ∧ B ) -> A は、\a -> _∧_.and1 a で証明できるが、
(3) (A ∧ (A -> B)) -> Bは、かなり難しいかも知れません。
_∧_.and1 a と _∧_.and2 b をいじって、直接構成してもなんとかできるはずですが、
lemma31 (A ∧ (A -> B)) -> (A -> B) lemma32 (A ∧ (A -> B)) -> A lemma33 A -> ( A -> B ) -> Bの三つに分解すると簡単になります。(3-1) は (A ∧ B) -> B と同じ。この三つの lemma を組み合わせて証明を作ると良いです。