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 で使う

VSCode でのAgda の使い方


Emacs を使う場合

  brew tap caskroom/cask
  brew cask install emacs

などになるので、~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。

  agda.el を install

GUI 側で使わないと文字化けすることがあるようです。ews.el とか。

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 を切り替えて読みます。


neovim で使う

普通の vim では動かないです。

neovim でのAgda の使い方


プログラムを書く

Haskell と似たような、それでいて少し違う。そういうもので記述していきます。

agda1.agda というファイルを開けます。

    module agda1 where

と先頭に書きます。ファイル名と同じでないとだめです。

注意

    :  の前後は空白を開ける
    全角スペースが入らないように気を付ける。

  indent で、前の行と繋げる
    空白を空けないと一つのワードになる
    -> の前後にも空白が必要
    -> の優先順位   a -> b -> c は a -> ( b -> c )
    () と {} は特別扱いされる

C-C C-L で構文チェック。親切なエラーメッセージに従って直そう。

     ex. Parse Error

以下では、この例題を使う。

agda1.agda


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


等式

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 上に作成してみよう。

multily on Agda


Agda での否定の使い方と Directed Acyclic Graph

Directed Acyclic Graph

問題4.5

三つの vertex を持つグラフ。

Excercise 4.5


コード例

hello.agda

Shinji KONO / Wed May 8 17:24:23 2024