# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400830958 -32400
# Node ID b82e226f56ffc5857636cb107c4099ca089aef48
# Parent  75610214a40480209eccc889b80743fe9581b212
Update slides to add-assoc + mult-sym

diff -r 75610214a404 -r b82e226f56ff slide.md
--- a/slide.md	Fri May 23 14:13:40 2014 +0900
+++ b/slide.md	Fri May 23 16:42:38 2014 +0900
@@ -67,9 +67,9 @@
 
 # 自然数に対する演算の定義
 * x と y の加算 : x にかかっている S の分だけ S を b に適用する
-* x と y の加算 : x にかかっている S の分だけ y を 0 に加算する
+* x と y の乗算 : x にかかっている S の分だけ y を 0 に加算する
 
-* Agda tips : 不明な項を ? と書くこともできます
+* Agda tips : 不明な項を ? と書くこともできます。 goal と呼びます
 * その状態で C-c C-l するとその項の型が分かります
 
 
@@ -127,15 +127,12 @@
 * 加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン
 
 * 乗法の交換法則 : (x * y) = (y * x)
-* 乗法の結合法則 : (x * y) * z = x * (y * z)
-
-* 分配法則       : x * (y + z) = (x * y) + (x * z)
 
 # '等しい' ということ
 * '等しい'という型 _ ≡ _ を定義する
   * refl  : x ≡ x
   * sym   : x ≡ y -> y ≡ x
-  * cong  : (f : A → B) -> x ≡ y → f x ≡ f y
+  * 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 : 記号は \ の後に文字列を入れると出てきます。 '≡' は "\ =="
@@ -148,6 +145,7 @@
 * 関数なら normal form が同じなら同じ
   * lambda-term : (A : Set)  -> (\(x : A) -> x) ≡ (\(y : A) -> y)
   * lambda-term A = refl
+* 関数による変形は形が違う等しいものとして扱います
 
 
 # 交換法則を型として定義する
@@ -239,6 +237,7 @@
 ```
 
 * Agda tips : goal の上で C-c C-c で引数のパターン分け
+  * 例えば y にのみ適用してみる
 * Agda tips : goal の上で C-c C-a で証明を探してくれる
 
 
@@ -310,12 +309,4 @@
 が必要になる
 
 
-# 乗法の結合法則 : (a * b) * c = a * (b * c)
-TODO: まだ。書いとく(うしろで良いかな)
-
-
-# 分配法則  : x * (y + z) = (x * y) + (x * z)
-TODO: まだ。書いとく(うしろで良いかな)
-
-
 <!-- vim: set filetype=markdown.slide: -->