Mercurial > hg > Papers > 2015 > atton-osc

comparison slide.html @ 13:37a7b8c31a0c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
12:dfa919e8fb20 13:37a7b8c31a0c
41 <h1 id="section">このセミナーの目的</h1> 41 <h1 id="section">このセミナーの目的</h1>
42 </header> 42 </header>
43 <!-- === begin markdown block === 43 <!-- === begin markdown block ===
44 44
45 generated by markdown 1.1.1 on Ruby 2.1.2 (2014-05-08) [x86_64-darwin13.0] 45 generated by markdown 1.1.1 on Ruby 2.1.2 (2014-05-08) [x86_64-darwin13.0]
46 on 2014-05-24 10:41:10 +0900 with Markdown engine kramdown (1.3.3) 46 on 2014-05-24 10:56:09 +0900 with Markdown engine kramdown (1.3.3)
47 using options {} 47 using options {}
48 --> 48 -->
49 49
50 <!-- _S9SLIDE_ --> 50 <!-- _S9SLIDE_ -->
51 51
509 <header> 509 <header>
510 <h1 id="section-12">交換法則を証明していく</h1> 510 <h1 id="section-12">交換法則を証明していく</h1>
511 </header> 511 </header>
512 <!-- _S9SLIDE_ --> 512 <!-- _S9SLIDE_ -->
513 513
514 <pre><code> sum-sym : (x y : Int) -&gt; x + y ≡ y + x 514 <pre><code> add-sym : (x y : Int) -&gt; x + y ≡ y + x
515 sum-sym O O = refl 515 add-sym O O = refl
516 sum-sym O (S y) = cong S (sum-sym O y) 516 add-sym O (S y) = cong S (add-sym O y)
517 sum-sym (S x) O = cong S (sum-sym x O) 517 add-sym (S x) O = cong S (add-sym x O)
518 sum-sym (S x) (S y) = ? 518 add-sym (S x) (S y) = ?
519 </code></pre> 519 </code></pre>
520 520
521 521
522 522
523 </section> 523 </section>
529 <h1 id="o-o-">O, O の場合</h1> 529 <h1 id="o-o-">O, O の場合</h1>
530 </header> 530 </header>
531 <!-- _S9SLIDE_ --> 531 <!-- _S9SLIDE_ -->
532 532
533 <ul> 533 <ul>
534 <li>sum-sym O O = refl</li> 534 <li>add-sym O O = refl</li>
535 <li>両方ともO の時、証明したい命題は O + O ≡ O + O</li> 535 <li>両方ともO の時、証明したい命題は O + O ≡ O + O</li>
536 <li>_ + _ の定義の x + O = x より</li> 536 <li>_ + _ の定義の x + O = x より</li>
537 <li>O ≡ O を構成したい</li> 537 <li>O ≡ O を構成したい</li>
538 <li>refl によって構成する</li> 538 <li>refl によって構成する</li>
539 <li>refl O と考えてもらえると良い</li> 539 <li>refl O と考えてもらえると良い</li>
550 <h1 id="o--s-">片方が O, 片方に S が付いている場合</h1> 550 <h1 id="o--s-">片方が O, 片方に S が付いている場合</h1>
551 </header> 551 </header>
552 <!-- _S9SLIDE_ --> 552 <!-- _S9SLIDE_ -->
553 553
554 <ul> 554 <ul>
555 <li>sum-sym O (S y) = cong S (sum-sym O y)</li> 555 <li>add-sym O (S y) = cong S (add-sym O y)</li>
556 <li>式的には O + (S y) ≡ (S y) + O</li> 556 <li>式的には O + (S y) ≡ (S y) + O</li>
557 <li>_ + _ の定義 x + (S y) = S (x + y) より</li> 557 <li>_ + _ の定義 x + (S y) = S (x + y) より</li>
558 <li>O + (S y) ≡ S (O + y)</li> 558 <li>O + (S y) ≡ S (O + y)</li>
559 <li>O と y を交換して O + (S y) ≡ S (y + O)</li> 559 <li>O と y を交換して O + (S y) ≡ S (y + O)</li>
560 <li>つまり y と O を交換して S をかけると良い</li> 560 <li>つまり y と O を交換して S をかけると良い</li>
561 <li>交換して S をかける -&gt; cong S (sum-sym O y)</li> 561 <li>交換して S をかける -&gt; cong S (add-sym O y)</li>
562 </ul> 562 </ul>
563 563
564 564
565 565
566 </section> 566 </section>
572 <h1 id="trans-">trans による等式変形</h1> 572 <h1 id="trans-">trans による等式変形</h1>
573 </header> 573 </header>
574 <!-- _S9SLIDE_ --> 574 <!-- _S9SLIDE_ -->
575 575
576 <ul> 576 <ul>
577 <li>sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない</li> 577 <li>add-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない</li>
578 <li> 578 <li>
579 <p>等しさを保ったまま式を変形していくことが必要になります</p> 579 <p>等しさを保ったまま式を変形していくことが必要になります</p>
580 </li> 580 </li>
581 <li>sum-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c) 581 <li>add-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c)
582 <ul> 582 <ul>
583 <li>trans (refl) ?</li> 583 <li>trans (refl) ?</li>
584 <li>trans (trans refl (cong S (sum-sym (S x) y)) ?</li> 584 <li>trans (trans refl (cong S (add-sym (S x) y)) ?</li>
585 </ul> 585 </ul>
586 </li> 586 </li>
587 </ul> 587 </ul>
588 588
589 589
622 <h1 id="reasoning--1">≡-reasoning による最初の定義</h1> 622 <h1 id="reasoning--1">≡-reasoning による最初の定義</h1>
623 </header> 623 </header>
624 <!-- _S9SLIDE_ --> 624 <!-- _S9SLIDE_ -->
625 625
626 626
627 <pre><code> sum-sym (S x) (S y) = begin 627 <pre><code> add-sym (S x) (S y) = begin
628 (S x) + (S y) 628 (S x) + (S y)
629 ≡⟨ ? ⟩ 629 ≡⟨ ? ⟩
630 (S y) + (S x) 630 (S y) + (S x)
631 ∎ 631 ∎
632 </code></pre> 632 </code></pre>
649 <li>の定義である x + (S y) = S (x + y) により変形</li> 649 <li>の定義である x + (S y) = S (x + y) により変形</li>
650 </ul> 650 </ul>
651 </li> 651 </li>
652 </ul> 652 </ul>
653 653
654 <pre><code> sum-sym (S x) (S y) = begin 654 <pre><code> add-sym (S x) (S y) = begin
655 (S x) + (S y) 655 (S x) + (S y)
656 ≡⟨ refl ⟩ 656 ≡⟨ refl ⟩
657 S (S x + y) 657 S (S x + y)
658 ≡⟨ ? ⟩ 658 ≡⟨ ? ⟩
659 (S y) + (S x) 659 (S y) + (S x)
666 </div></div> 666 </div></div>
667 667
668 <div class="slide" id="29"><div> 668 <div class="slide" id="29"><div>
669 <section> 669 <section>
670 <header> 670 <header>
671 <h1 id="cong--sum-sym-">cong と sum-sym を使って交換</h1> 671 <h1 id="cong--add-sym-">cong と add-sym を使って交換</h1>
672 </header> 672 </header>
673 <!-- _S9SLIDE_ --> 673 <!-- _S9SLIDE_ -->
674 674
675 <ul> 675 <ul>
676 <li>S が1つ取れたのでsum-symで交換できる</li> 676 <li>S が1つ取れたのでadd-symで交換できる</li>
677 <li>sum-sym で交換した後に cong で S がかかる</li> 677 <li>add-sym で交換した後に cong で S がかかる</li>
678 </ul> 678 </ul>
679 679
680 <pre><code> S ((S x) + y) 680 <pre><code> S ((S x) + y)
681 ≡⟨ cong S (sum-sym (S x) y) ⟩ 681 ≡⟨ cong S (add-sym (S x) y) ⟩
682 S ((y + (S x))) 682 S ((y + (S x)))
683 </code></pre> 683 </code></pre>
684 684
685 685
686 686
768 <header> 768 <header>
769 <h1 id="x--y--y--x">加法の交換法則 : (x + y) = (y + x)</h1> 769 <h1 id="x--y--y--x">加法の交換法則 : (x + y) = (y + x)</h1>
770 </header> 770 </header>
771 <!-- _S9SLIDE_ --> 771 <!-- _S9SLIDE_ -->
772 772
773 <pre><code> sum-sym (S x) (S y) = begin 773 <pre><code> add-sym (S x) (S y) = begin
774 (S x) + (S y) 774 (S x) + (S y)
775 ≡⟨ refl ⟩ 775 ≡⟨ refl ⟩
776 S ((S x) + y) 776 S ((S x) + y)
777 ≡⟨ cong S (sum-sym (S x) y) ⟩ 777 ≡⟨ cong S (add-sym (S x) y) ⟩
778 S (y + (S x)) 778 S (y + (S x))
779 ≡⟨ (sym (left-increment y (S x))) ⟩ 779 ≡⟨ (sym (left-increment y (S x))) ⟩
780 (S y) + (S x) 780 (S y) + (S x)
781 ∎ 781 ∎
782 </code></pre> 782 </code></pre>