Reasoning in Agda
Menu MenuAgda での式の変形
Agda では等式の推論規則、反射律、推移律、合同律などの変形を行う方法があり、便利に使うことができます。Reasoning 自体も Agda で記述されているので、それを再現しながら実際に使ってみましょう。list-nad.agda 自分で _==_ という等号を用意してみましょう。これは、_≡_ 同じであり、実際、変換することも可能です。あくまでも練習のために用意したものです。
data _==_ {A : Set } : List A -> List A -> Set where
reflection : {x : List A} -> x == x
cong1 : {A : Set } { B : Set } ->
( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
cong1 f reflection = reflection
eq-cons : {A : Set } {x y : List A} ( a : A ) -> x == y -> ( a :: x ) == ( a :: y )
eq-cons a z = cong1 ( \x -> ( a :: x) ) z
trans-list : {A : Set } {x y z : List A} -> x == y -> y == z -> x == z
trans-list reflection reflection = reflection
名前が衝突しないように変えてあります。Agda では module で名前を隠したり変更したりすることができますが、同時に使おうとした時に名前が重なっていると厄介です。これは、Agda の monomorphism だとも言えますが、その代わり、記号が決まれば型が決まるのは単純でわかりやすいはずです。
cong1 や eq-cons は、すべてここで証明しています。つまり、data _==_ がもともと持っている性質です。これは、x == x という公理から、すべて導かれると思っても良いです。
これらは証明の short cut として使うことができます。実際、List の [] の単位元としての性質や、結合律を以下のように証明できます。
list-id-l : { A : Set } -> { x : List A} -> [] ++ x == x
list-id-l = reflection
list-id-r : { A : Set } -> ( x : List A ) -> x ++ [] == x
list-id-r [] = reflection
list-id-r (x :: xs) = eq-cons x ( list-id-r xs )
list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
list-assoc [] ys zs = reflection
list-assoc (x :: xs) ys zs = eq-cons x ( list-assoc xs ys zs )
命題の型が証明するべき式で、値の関数が推論の組み合わせに対応するのが、Curry-Howard 対応でした。
残念ながら、 eq-cons x ( list-assoc xs ys zs ) が ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) ) の証明であることはひと目ではわかりません。
Reasoning を使うことにより、以下のように式の変形を追うことができます。(ここでは自分で定義した ==⟨ ⟩ とか使ってますが、普通は、 Relation.Binary.PropositionalEquality の ≈-Reasoning を利用します。この時は使い方がわからなかった)
++-assoc : (L : Set ) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
++-assoc A [] ys zs = let open ==-Reasoning A in
begin -- to prove ([] ++ ys) ++ zs == [] ++ (ys ++ zs)
( [] ++ ys ) ++ zs
==⟨ reflection ⟩
ys ++ zs
==⟨ reflection ⟩
[] ++ ( ys ++ zs )
∎
++-assoc A (x :: xs) ys zs = let open ==-Reasoning A in
begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
((x :: xs) ++ ys) ++ zs
==⟨ reflection ⟩
(x :: (xs ++ ys)) ++ zs
==⟨ reflection ⟩
x :: ((xs ++ ys) ++ zs)
==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
x :: (xs ++ (ys ++ zs))
==⟨ reflection ⟩
(x :: xs) ++ (ys ++ zs)
∎
==⟨ reflection ⟩ は、 ==⟨⟩ と書くこともできます。begin で始めて、∎ で終わる。同じ推論要素が含まれてるので、結局は同じことをやっているのですが、関数適応の各段階で型を目で見れるのはうれしいことです。
indent は正確でなければなりません。begin や ==⟨ reflection ⟩ 、 ∎ は、すべて Agda の演算子だからです。
==⟨ ?? ⟩ の ?? に書くことができるのは、
a == b
という形をした型を生成する関数です。== に関する推論規則は必ず、この形をしています。その他の推論は、cong 合同規則を使って行います。つまり、
式の任意の部分に勝手に代入できますわけではありません
そういうことをしたいのならば、そういう推論規則を証明して使う必要があります。
reflection は x == x を返すので、基本的に変形前と後では式は同じはずです。でも、見かけは異なります。Agda は normalization を行なってから比較を行うので、同じ normal form を持つ式は「まったく同じもの」です。例えば、関数適用などは変形に入りません。しかし、人は、それを明示しないとわからないものです。
後で、Reasoning の、もう少し便利な(複雑な)使い方について話す機会もあるでしょう。
以下では、Reasoning の Agda での実装について触れますが、ここは必須でないので飛ばしても構いません。
Reasoning の実装
Reasoning は以下のように実装されています。これは Agda のプログラムです。
module ==-Reasoning (A : Set ) where
infixr 2 _∎
infixr 2 _==⟨_⟩_ _==⟨⟩_
infix 1 begin_
data _IsRelatedTo_ (x y : List A) :
Set where
relTo : (x≈y : x == y ) → x IsRelatedTo y
begin_ : {x : List A } {y : List A} →
x IsRelatedTo y → x == y
begin relTo x≈y = x≈y
_==⟨_⟩_ : (x : List A ) {y z : List A} →
x == y → y IsRelatedTo z → x IsRelatedTo z
_ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
_==⟨⟩_ : (x : List A ) {y : List A}
→ x IsRelatedTo y → x IsRelatedTo y
_ ==⟨⟩ x≈y = x≈y
_∎ : (x : List A ) → x IsRelatedTo x
_∎ _ = relTo reflection
最初に演算子の優先順位が記述されています。_==⟨_⟩_ は三項演算子であり、カッコを含んでいます。
data _IsRelatedTo_ (x y : List A) は、x == y を格納するデータ型です。relTo は related to であり Constructor です。ここでは、等式 _==_ の data 型を受け取って、_IsRelatedTo_ に変換しています。
x≈y は空白が入ってないので単なる変数です。Agda では、x ≈ y と x≈y が異なります。
Reasoning の動作
この構文は後ろから読んでいきます。証明は x == x から推論規則を適用して変形していくからです。
_∎ : (x : List A ) → x IsRelatedTo x
_∎ _ = relTo reflection
は最後の証明すべき等式の右辺、つまり List の型 (x :: xs) ++ (ys ++ zs) を受け取る。reflection は _==_ の constructor で、 X == X を作成します。それを relTo で _IsRelaedTo_ にさらに変換します。
((x :: xs) ++ (ys ++ zs) ) isRelatedTo ((x :: xs) ++ (ys ++ zs) )
いうのが _∎ _ の戻り値の型です。X は、まだ決まってない型です。受け取った引数は _ で無視されています。_∎ が演算子であり、その後の単独の _ が無視された引数です。重要なのは型なので値はどうでも良いというわけです。
その一つ上、
==⟨ reflection ⟩
は、何もしません。この前後は「まったく同じもの」です。 ここでは、
x :: (xs ++ (ys ++ zs))
は、(x :: xs) ++ ys = x :: (xs ++ ys) という関数適用によって変形されて、
(x :: xs) ++ (ys ++ zs)
これになっています。二つは同じものなので、どちらからどちらへでも変形できます。 ==⟨⟩ でがんがん変形して、できなかったら、何かを呼び出すことを考えます。 実際、
_ ==⟨⟩ x≈y = x≈y
なので何もしていません。結果、(Agda の中では同じだが、人の頭の中では)
x :: (xs ++ (ys ++ zs)) IsRelateTo (x :: (xs ++ (ys ++ zs)))
となりました。 問題は、
x :: ((xs ++ ys) ++ zs)
==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
x :: (xs ++ (ys ++ zs))
この部分です。ここでは、cong1 (_::_ x) (++-assoc A xs ys zs) を使って式を変形しています。cong1 は、
cong1 : {A : Set } { B : Set } ->
( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
cong1 f reflection = reflection
なので、f を受け取って、
f x == f y
を生成します。ここでの f は (_::_ x) です。つまり「先頭に x を付け加える関数」です。C-c C-n で (_::_ a ) [] を試してみましょう。
逆順にたどっているので、f x == f y に相当するのが、
x :: (xs ++ (ys ++ zs)) isRelatedTo ((x :: xs) ++ (ys ++ zs) )
です。確かに、右辺は x が先頭に付いています。
++-assoc A xs ys zs は、証明すべき式と同じですが、ここでは、
(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
という型を返すはずです。これが x == y です。つまり、cong1 は、
x :: ((xs ++ ys) ++ zs) == x :: (xs ++ (ys ++ zs)) ... (1)
--------- x ------------ -------- y ------------
を返します。これが、以下の (二つ目の) x≈y という変数に入って _==⟨_⟩_ が呼び出されます。
_==⟨_⟩_ : (x : List A ) {y z : List A} →
x == y → y IsRelatedTo z → x IsRelatedTo z
_ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
最初の引数は、これまでの推論だが _ で無視されています。重要なのは値ではなくて型だからです。最後の引数は relTo y≈z というパターンで分解されます。relTo の引数は _==_ というパターンなので、結局、y≈z に
x :: (xs ++ (ys ++ zs)) == ((x :: xs) ++ (ys ++ zs) ) ... (2)
----------y ----------- --------- z ------------
が入ることになります。この二つの式を trans-list という関数、
trans-list : {A : Set } {x y z : List A} -> x == y -> y == z -> x == z
trans-list reflection reflection = reflection
で変形すると、trans-list は、
x :: ((xs ++ ys) ++ zs) == ((x :: xs) ++ (ys ++ zs) ) ... (3)
--------- x ------------ --------- z ------------
を返します。これを relTo で、
(x :: ((xs ++ ys) ++ zs)) isRelatedTo (((x :: xs) ++ (ys ++ zs) )) ... (4)
を構築しています。
_==_ のままでもできそうですが、_==_ では必ず x == x でなければなりません。一方で、_isRelatedTo_ は定義では左右が異なっても大丈夫です。最終的には同じになるにしても。今は、終わりから辿っているので、_isRelatedTo_ の両辺は必ず == になっています。
あとは reflection で変形するだけです。最後に、
begin_ : {x : List A } {y : List A} →
x IsRelatedTo y → x == y
begin relTo x≈y = x≈y
で、x == y に戻しています。この段階で正しく両辺は(_==_ の意味で)等しいはずです。最終的に _==_ の左右は異なる normal form を持つことになります。
集合レベルに対応するためには適切な変更が必要になりますが、ここでは A の型だけが問題で、それは module の引数で渡してしまえば良いわけです。
つまり、Reasoning は特定の型の要素を持つ List に対して行われて、これを混ぜることはできません。同じ module を入れ子で呼び出すことは Agda では面倒です。そういう場合は、一つ Lemma (補助命題) をはさむことで解決します。
ここでは、わざと自分で Reasoning を作成しましたが、 Relation.Binary.PropositionalEquality に既に ≡-Reasoning が用意されています。この場合は、≡ に対して定義されている refl や cong を使います。