Mercurial > hg > Papers > 2015 > atton-osc
changeset 13:37a7b8c31a0c
Replace sum-sym to add-sym
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 May 2014 10:56:24 +0900 |
| parents | dfa919e8fb20 |
| children | 43c56be5f779 |
| files | slide.html slide.md |
| diffstat | 2 files changed, 39 insertions(+), 39 deletions(-) [+] |
line wrap: on
line diff
--- a/slide.html Sat May 24 10:41:20 2014 +0900 +++ b/slide.html Sat May 24 10:56:24 2014 +0900 @@ -43,7 +43,7 @@ <!-- === begin markdown block === generated by markdown 1.1.1 on Ruby 2.1.2 (2014-05-08) [x86_64-darwin13.0] - on 2014-05-24 10:41:10 +0900 with Markdown engine kramdown (1.3.3) + on 2014-05-24 10:56:09 +0900 with Markdown engine kramdown (1.3.3) using options {} --> @@ -511,11 +511,11 @@ </header> <!-- _S9SLIDE_ --> -<pre><code> 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) = ? +<pre><code> add-sym : (x y : Int) -> x + y ≡ y + x + add-sym O O = refl + add-sym O (S y) = cong S (add-sym O y) + add-sym (S x) O = cong S (add-sym x O) + add-sym (S x) (S y) = ? </code></pre> @@ -531,7 +531,7 @@ <!-- _S9SLIDE_ --> <ul> - <li>sum-sym O O = refl</li> + <li>add-sym O O = refl</li> <li>両方ともO の時、証明したい命題は O + O ≡ O + O</li> <li>_ + _ の定義の x + O = x より</li> <li>O ≡ O を構成したい</li> @@ -552,13 +552,13 @@ <!-- _S9SLIDE_ --> <ul> - <li>sum-sym O (S y) = cong S (sum-sym O y)</li> + <li>add-sym O (S y) = cong S (add-sym O y)</li> <li>式的には O + (S y) ≡ (S y) + O</li> <li>_ + _ の定義 x + (S y) = S (x + y) より</li> <li>O + (S y) ≡ S (O + y)</li> <li>O と y を交換して O + (S y) ≡ S (y + O)</li> <li>つまり y と O を交換して S をかけると良い</li> - <li>交換して S をかける -> cong S (sum-sym O y)</li> + <li>交換して S をかける -> cong S (add-sym O y)</li> </ul> @@ -574,14 +574,14 @@ <!-- _S9SLIDE_ --> <ul> - <li>sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない</li> + <li>add-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない</li> <li> <p>等しさを保ったまま式を変形していくことが必要になります</p> </li> - <li>sum-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c) + <li>add-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c) <ul> <li>trans (refl) ?</li> - <li>trans (trans refl (cong S (sum-sym (S x) y)) ?</li> + <li>trans (trans refl (cong S (add-sym (S x) y)) ?</li> </ul> </li> </ul> @@ -624,7 +624,7 @@ <!-- _S9SLIDE_ --> -<pre><code> sum-sym (S x) (S y) = begin +<pre><code> add-sym (S x) (S y) = begin (S x) + (S y) ≡⟨ ? ⟩ (S y) + (S x) @@ -651,7 +651,7 @@ </li> </ul> -<pre><code> sum-sym (S x) (S y) = begin +<pre><code> add-sym (S x) (S y) = begin (S x) + (S y) ≡⟨ refl ⟩ S (S x + y) @@ -668,17 +668,17 @@ <div class="slide" id="29"><div> <section> <header> - <h1 id="cong--sum-sym-">cong と sum-sym を使って交換</h1> + <h1 id="cong--add-sym-">cong と add-sym を使って交換</h1> </header> <!-- _S9SLIDE_ --> <ul> - <li>S が1つ取れたのでsum-symで交換できる</li> - <li>sum-sym で交換した後に cong で S がかかる</li> + <li>S が1つ取れたのでadd-symで交換できる</li> + <li>add-sym で交換した後に cong で S がかかる</li> </ul> <pre><code> S ((S x) + y) - ≡⟨ cong S (sum-sym (S x) y) ⟩ + ≡⟨ cong S (add-sym (S x) y) ⟩ S ((y + (S x))) </code></pre> @@ -770,11 +770,11 @@ </header> <!-- _S9SLIDE_ --> -<pre><code> sum-sym (S x) (S y) = begin +<pre><code> add-sym (S x) (S y) = begin (S x) + (S y) ≡⟨ refl ⟩ S ((S x) + y) - ≡⟨ cong S (sum-sym (S x) y) ⟩ + ≡⟨ cong S (add-sym (S x) y) ⟩ S (y + (S x)) ≡⟨ (sym (left-increment y (S x))) ⟩ (S y) + (S x)
--- a/slide.md Sat May 24 10:41:20 2014 +0900 +++ b/slide.md Sat May 24 10:56:24 2014 +0900 @@ -188,16 +188,16 @@ # 交換法則を証明していく ``` - 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) = ? + add-sym : (x y : Int) -> x + y ≡ y + x + add-sym O O = refl + add-sym O (S y) = cong S (add-sym O y) + add-sym (S x) O = cong S (add-sym x O) + add-sym (S x) (S y) = ? ``` # O, O の場合 -* sum-sym O O = refl +* add-sym O O = refl * 両方ともO の時、証明したい命題は O + O ≡ O + O * _ + _ の定義の x + O = x より * O ≡ O を構成したい @@ -206,22 +206,22 @@ # 片方が O, 片方に S が付いている場合 -* sum-sym O (S y) = cong S (sum-sym O y) +* add-sym O (S y) = cong S (add-sym O y) * 式的には O + (S y) ≡ (S y) + O * _ + _ の定義 x + (S y) = S (x + y) より * O + (S y) ≡ S (O + y) * O と y を交換して O + (S y) ≡ S (y + O) * つまり y と O を交換して S をかけると良い -* 交換して S をかける -> cong S (sum-sym O y) +* 交換して S をかける -> cong S (add-sym O y) # trans による等式変形 -* sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない +* add-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない * 等しさを保ったまま式を変形していくことが必要になります -* sum-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c) +* add-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c) * trans (refl) ? - * trans (trans refl (cong S (sum-sym (S x) y)) ? + * trans (trans refl (cong S (add-sym (S x) y)) ? # ≡-reasoning による等式変形 @@ -241,7 +241,7 @@ # ≡-reasoning による最初の定義 ``` - sum-sym (S x) (S y) = begin + add-sym (S x) (S y) = begin (S x) + (S y) ≡⟨ ? ⟩ (S y) + (S x) @@ -253,7 +253,7 @@ * + の定義である x + (S y) = S (x + y) により変形 ``` - sum-sym (S x) (S y) = begin + add-sym (S x) (S y) = begin (S x) + (S y) ≡⟨ refl ⟩ S (S x + y) @@ -263,13 +263,13 @@ ``` -# cong と sum-sym を使って交換 -* S が1つ取れたのでsum-symで交換できる -* sum-sym で交換した後に cong で S がかかる +# cong と add-sym を使って交換 +* S が1つ取れたのでadd-symで交換できる +* add-sym で交換した後に cong で S がかかる ``` S ((S x) + y) - ≡⟨ cong S (sum-sym (S x) y) ⟩ + ≡⟨ cong S (add-sym (S x) y) ⟩ S ((y + (S x))) ``` @@ -309,11 +309,11 @@ # 加法の交換法則 : (x + y) = (y + x) ``` - sum-sym (S x) (S y) = begin + add-sym (S x) (S y) = begin (S x) + (S y) ≡⟨ refl ⟩ S ((S x) + y) - ≡⟨ cong S (sum-sym (S x) y) ⟩ + ≡⟨ cong S (add-sym (S x) y) ⟩ S (y + (S x)) ≡⟨ (sym (left-increment y (S x))) ⟩ (S y) + (S x)