# HG changeset patch # User Yasutaka Higa # Date 1400822020 -32400 # Node ID 75610214a40480209eccc889b80743fe9581b212 # Parent c55157da5bf37e23c441a87d0aed6355ed64b240 Update to sum-assoc diff -r c55157da5bf3 -r 75610214a404 slide.md --- a/slide.md Thu May 22 20:30:05 2014 +0900 +++ b/slide.md Fri May 23 14:13:40 2014 +0900 @@ -48,33 +48,49 @@ # Agda における自然数の定義 * data 型を使います - * data Int : Set where - * Zero : Int - * Succ : Int -> Int -* Zero は Int, Succ は Int を受けとって Int を返す、と読めます + +``` + data Int : Set where + O : Int + S : Int -> Int +``` +* O は Int, S は Int を受けとって Int を返す、と読めます * Set は組込みで存在する型です。「成り立つ」といった感じです。 # 自然数の例 -* 0 = Zero -* 1 = Succ Zero -* 2 = Succ (Succ Zero) -* 5 = Succ (Succ (Succ (Succ (Succ Zero)))) +* 0 = O +* 1 = S O +* 2 = S (S O) +* 5 = S (S (S (S (S O)))) # 自然数に対する演算の定義 -* a と b の加算 : a にかかっている Succ の分だけ Succ を b にかける -* a と b の加算 : a にかかっている Succ の分だけ b を 0 に加算する +* x と y の加算 : x にかかっている S の分だけ S を b に適用する +* x と y の加算 : x にかかっている S の分だけ y を 0 に加算する * Agda tips : 不明な項を ? と書くこともできます * その状態で C-c C-l するとその項の型が分かります +# Agda における自然数に対する演算の定義 +``` + infixl 30 _+_ + _+_ : Int -> Int -> Int + x + O = x + x + (S y) = S (x + y) +``` + +* Agda tips : C-c C-n すると式を評価することができます +* (S O) + (S (S O)) などしてみましょう + + # Agda における関数定義のSyntax * Agda において、関数は * 関数名 : 型 * 関数名 <スペース区切りで引数> = 関数の定義や値 * のように定義します +* 中置関数は _ で挟みます # Agda における引数を持つ関数の型の表記法 @@ -86,32 +102,35 @@ * 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます -# Agda における自然数に対する演算の定義 -TODO: 書いておく - -* Agda tips : C-c C-n すると式を評価することができます -* add (Succ Zero) (Succ (Succ Zero)) などしてみましょう - - # パターンマッチ * Agda においてはデータ型は引数で分解することができます * ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます * double : Int -> Int * double O = O - * double (S n) = S (S (double n)) + * double (S x) = S (S (double x)) * 関数名 (引数のパターン) = 定義 +# もういちど : 自然数に対する演算の定義 +``` + infixl 30 _+_ + _+_ : Int -> Int -> Int + x + O = x + x + (S y) = S (x + y) +``` +* 中置、関数、パターンマッチが使われています +* infixl は左結合を意味します。数値は結合強度です + + # これから証明していきたいこと -* 加法の交換法則 : (a + b) = (b + a) -* 加法の結合法則 : (a + b) + c = a + (b + c) +* 加法の交換法則 : (x + y) = (y + x) +* 加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン + +* 乗法の交換法則 : (x * y) = (y * x) +* 乗法の結合法則 : (x * y) * z = x * (y * z) * 分配法則 : x * (y + z) = (x * y) + (x * z) -* 乗法の交換法則 : (a * b) = (b * a) -* 乗法の結合法則 : (a * b) * c = a * (b * c) - - # '等しい' ということ * '等しい'という型 _ ≡ _ を定義する * refl : x ≡ x @@ -119,6 +138,7 @@ * cong : (f : A → B) -> x ≡ y → f x ≡ f y * trans : x ≡ y -> y ≡ z -> y ≡ z * defined : Relation.Binary.PropositionalEquality in Standard Library +* Agda tips : 記号は \ の後に文字列を入れると出てきます。 '≡' は "\ ==" # '同じもの'とは @@ -132,32 +152,128 @@ # 交換法則を型として定義する * ≡を用いて - * (n : Int) -> (m : Int) -> n + m ≡ m + n + * (x : Int) -> (y : Int) -> x + y ≡ y + x * 引数は (名前 : 型) として名前付けできます -# 等式変形 -TODO: trans による等式変形 +# 交換法則を証明していく +``` +sum-sym : (x y : Int) -> x + y ≡ y + x +sum-sym O O = refl +sum-sym O (S y) = cong S (sum-sym O y) +sum-sym (S x) O = cong S (sum-sym x O) +sum-sym (S x) (S y) = ? +``` + +# trans による等式変形 +* sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない +* 等しさを保ったまま式を変形していくことが必要になります + +* sum-sym (S x) (S y) = trans (a ≡ b) (b ≡ c) + * trans (refl) ? + * trans (trans refl (cong S (left-add-one x y)) ? # ≡-reasoning による等式変形 -TODO: reasoning による等式変形 +* trans が何段もネストしていくと分かりづらい +* ≡-reasoning という等式変形の拡張構文が Standard Library にあります + +``` + begin + 変換前の式 + ≡⟨ 変換する関数 ⟩ + 変換後の式 + ∎ +``` + + +# ≡-reasoning による最初の定義 + +``` +sum-sym (S x) (S y) = begin + (S x) + (S y) + ≡⟨ ? ⟩ + (S y) + (S x) + ∎ +``` + + +# 交換法則の証明 : + の定義による変形 +* 上から + の定義により変形 + +``` +sum-sym (S x) (S y) = begin + (S x) + (S y) + ≡⟨ refl ⟩ + S (S x + y) + ≡⟨ ? ⟩ + (S y) + (S x) + ∎ +``` + + +# cong と sum-sym を使って交換 +* S が1つ取れたのでsum-symで交換できる +* sum-sym で交換した後に cong で S がかかる + +``` + S ((S x) + y) + ≡⟨ cong S (sum-sym (S x) y) ⟩ + S ((y + (S x))) +``` -# 加法の交換法則 : (a + b) = (b + a) -TODO: 書いとく +# 交換法則の証明 : 加法の時に左側からSを移動させることができない + +* 加法の定義は + * x + (S y) = S (x + y) +* left-operand から S を取る方法が無い + * S (y + S x) ≡ S y + S x +* にあてはまるものを入れてくれ、と出てきている + -# 加法の結合法則 : (a + b) + c = a + (b + c) -TODO: 書いとく +# left-operand からSを操作する証明を定義 +``` + left-increment : (x y : Int) -> (S x) + y ≡ S (x + y) + left-increment x y = ? +``` + +* Agda tips : goal の上で C-c C-c で引数のパターン分け +* Agda tips : goal の上で C-c C-a で証明を探してくれる + + +# left-operand からSを移動させる +* left-increment は (S x) + y ≡ S (x + y) なので逆にしないと使えない -# 分配法則 : x * (y + z) = (x * y) + (x * z) -TODO: 書いとく(うしろで良いかな) +``` + ... + S ((S x) + y) + ≡⟨ sym (left-increment x (S y)) ⟩ + (S y) + (S x) + ∎ +``` + -# 乗法の交換法則 : (a * b) = (b * a) -TODO: 書いとく(うしろで良いかな) +# 加法の交換法則 : (x + y) = (y + x) +``` +sum-sym (S x) (S y) = begin + (S x) + (S y) + ≡⟨ refl ⟩ + S ((S x) + y) + ≡⟨ cong S (sum-sym (S x) y) ⟩ + S (y + (S x)) + ≡⟨ (sym (left-increment y (S x))) ⟩ + (S y) + (S x) + ∎ +``` -# 乗法の結合法則 : (a * b) * c = a * (b * c) -TODO: 書いとく(うしろで良いかな) + +# 加法の結合法則 : (x + y) + z = x + (y + z) +* 次に結合法則を証明します +* 手順は同じです + * ≡ で証明したい式を定義 + * 定義に証明を書く + * 必要ならば等式を変形していく # Agda による証明方法のまとめ @@ -168,4 +284,38 @@ * C-c C-l により型のチェックが成功すれば証明終了 +# 乗法の定義 +``` +infixl 40 _*_ +_*_ : Int -> Int -> Int +n * O = O +n * (S O) = n +n * (S m) = n + (n * m) +``` + +* _+_ よりも結合強度を上げる必要がある + + +# 乗法の交換法則 : (a * b) = (b * a) +``` +mult-sym : (n m : Int) -> n * m ≡ m * n +``` + +途中で + +``` +(n m : Int) -> (S n) * m ≡ m + (n * m) +``` + +が必要になる + + +# 乗法の結合法則 : (a * b) * c = a * (b * c) +TODO: まだ。書いとく(うしろで良いかな) + + +# 分配法則 : x * (y + z) = (x * y) + (x * z) +TODO: まだ。書いとく(うしろで良いかな) + +