Papers/2015/atton-osc: slide.html annotate

annotate slide.html @ 14:43c56be5f779 default tip

Fix typo

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Sat, 24 May 2014 11:30:42 +0900
parents	37a7b8c31a0c
children

rev	line source
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	1 <!DOCTYPE HTML>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	2
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	3 <html lang="Japanese">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	4 <head>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	5 <title>Agda 入門</title>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	6 <meta charset="UTF-8">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	7 <meta name="viewport" content="width=1274, user-scalable=no">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	8 <meta name="generator" content="Slide Show (S9)">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	9 <meta name="author" content="Yasutaka Higa">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	10 <link rel="stylesheet" href="themes/ribbon/styles/style.css">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	11 <style>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	12 #Cover H2 {
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	13 color:#FFF;
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	14 text-align:center;
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	15 font-size:70px;
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	16 }
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	17 </style>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	18 </head>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	19 <body class="list">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	20 <header class="caption">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	21 <h1>Agda 入門</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	22 <p>Yasutaka Higa</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	23 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	24 <div class="slide bg" id="Cover"><div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	25 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	26 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	27 <h2>Agda 入門</h2>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	28 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	29
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	30 <img src="pictures/" alt="">
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	31 <!-- © John Carey, http://fiftyfootshadows.net/ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	32 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	33 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	34
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	35 <!-- todo: add slide.classes to div -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	36 <!-- todo: create slide id from header? like a slug in blogs? -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	37
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	38 <div class="slide" id="2"><div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	39 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	40 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	41 <h1 id="section">このセミナーの目的</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	42 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	43 <!-- === begin markdown block ===
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	44
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	45 generated by markdown 1.1.1 on Ruby 2.1.2 (2014-05-08) [x86_64-darwin13.0]
14 43c56be5f779 Fix typo Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 13 diff changeset	46 on 2014-05-24 11:29:40 +0900 with Markdown engine kramdown (1.3.3)
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	47 using options {}
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	48 -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	49
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	50 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	51
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	52 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	53 <li>証明支援系の言語である Agda の入門を目的としています</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	54 <li>具体的には
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	55 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	56 <li>Agda による証明の方法を知る</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	57 <li>実際に自然数に対する演算の証明を追う</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	58 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	59 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	60 <li>ことをしていきます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	61 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	62
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	63
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	64
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	65 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	66 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	67
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	68 <div class="slide" id="3"><div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	69 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	70 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	71 <h1 id="agda-">Agda とはどういう言語なのか</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	72 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	73 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	74
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	75 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	76 <li>証明支援系と呼ばれる分野の言語です
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	77 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	78 <li>他には Coq などがあります</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	79 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	80 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	81 <li>Haskell で実装されています</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	82 <li>型が非常に強力で表現力が高いです
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	83 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	84 <li>命題や仕様を表す論理式を型として定義することができます</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	85 <li>例えば 1 + 1 = 2 とか</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	86 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	87 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	88 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	89
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	90
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	91
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	92 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	93 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	94
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	95 <div class="slide" id="4"><div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	96 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	97 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	98 <h1 id="curry-howard-isomorphism">型と証明との対応 : Curry-Howard Isomorphism</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	99 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	100 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	101
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	102 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	103 <li>Agda における証明は
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	104 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	105 <li>証明したい命題 == 関数の型</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	106 <li>命題の証明 == 関数の定義</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	107 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	108 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	109 <li>として定義します</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	110 <li>関数と命題の対応を Curry-Howard Isomorphism と言います</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	111 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	112
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	113
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	114
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	115 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	116 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	117
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	118 <div class="slide" id="5"><div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	119 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	120 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	121 <h1 id="section-1">命題と定義, 仕様と実装</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	122 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	123 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	124
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	125 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	126 <li>どうしてプログラムで証明できるかというと</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	127 <li>(命題と定義) は (仕様と実装) のように対応します
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	128 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	129 <li>int chars_to_int(char * chars)</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	130 <li>つまり char * から int は作れる、という命題に対応している</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	131 <li>実装は { itoa(chars) }</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	132 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	133 </li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	134 <li>char * から int は作れる、という仕様(型, 命題)は</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	135 <li>atoi という実装(定義)により証明された</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	136 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	137
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	138
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	139
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	140 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	141 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	142
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	143 <div class="slide" id="6"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	144 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	145 <header>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	146 <h1 id="agda--1">Agda をはじめよう</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	147 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	148 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	149
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	150 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	151 <li>emacs に agda-mode があります</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	152 <li>module filename where</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	153 <li>を先頭に書く必要があります</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	154 <li>証明を定義していく</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	155 <li>C-c C-l で型チェック(証明チェック)ができます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	156 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	157
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	158
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	159
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	160 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	161 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	162
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	163 <div class="slide" id="7"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	164 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	165 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	166 <h1 id="peano-arithmetic">自然数の定義 : Peano Arithmetic</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	167 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	168 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	169
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	170 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	171 <li>自然数 0 が存在する</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	172 <li>任意の自然数 x にはその後続数 S (x) が存在する</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	173 <li>0 より前の自然数は存在しない</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	174 <li>異なる自然数は異なる後続数を持つ
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	175 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	176 <li>x != y のとき S(x) != S(y) となる</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	177 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	178 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	179 <li>0 が性質を満たし、a も性質を満たせばその後続数も性質を満たすとき、すべての自然数はその性質を満たす</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	180 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	181
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	182
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	183
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	184 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	185 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	186
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	187 <div class="slide" id="8"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	188 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	189 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	190 <h1 id="agda--2">Agda における自然数の定義</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	191 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	192 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	193
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	194 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	195 <li>data 型を使います</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	196 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	197
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	198 <pre><code> data Int : Set where
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	199 O : Int
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	200 S : Int -> Int
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	201 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	202 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	203 <li>Int は O か、 Int に S がかかったもののみで構成される</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	204 <li>Set は組込みで存在する型で、”成り立つ”と考えてもらうと良いです。</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	205 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	206
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	207
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	208
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	209 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	210 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	211
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	212 <div class="slide" id="9"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	213 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	214 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	215 <h1 id="section-2">自然数の例</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	216 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	217 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	218
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	219 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	220 <li>0 = O</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	221 <li>1 = S O</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	222 <li>2 = S (S O)</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	223 <li>5 = S (S (S (S (S O))))</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	224 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	225
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	226
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	227
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	228 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	229 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	230
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	231 <div class="slide" id="10"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	232 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	233 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	234 <h1 id="section-3">自然数に対する演算の定義</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	235 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	236 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	237
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	238 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	239 <li>x と y の加算 : x にかかっている S の分だけ S を y に適用する</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	240 <li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	241 <p>x と y の乗算 : x にかかっている S の分だけ y を 0 に加算する</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	242 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	243 <li>Agda tips : 不明な項を ? と書くこともできます。 goal と呼びます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	244 <li>その状態で C-c C-l するとその項の型が分かります</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	245 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	246
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	247
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	248
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	249 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	250 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	251
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	252 <div class="slide" id="11"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	253 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	254 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	255 <h1 id="agda--3">Agda における自然数に対する演算の定義</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	256 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	257 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	258
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	259 <pre><code> infixl 30 _+_
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	260 _+_ : Int -> Int -> Int
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	261 x + O = x
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	262 x + (S y) = S (x + y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	263 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	264
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	265 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	266 <li>Agda tips : C-c C-n すると式を評価することができます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	267 <li>(S O) + (S (S O)) などしてみましょう</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	268 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	269
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	270
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	271
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	272 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	273 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	274
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	275 <div class="slide" id="12"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	276 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	277 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	278 <h1 id="agda-syntax">Agda における関数定義のSyntax</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	279 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	280 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	281
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	282 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	283 <li>Agda において、関数は
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	284 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	285 <li>_ + _ : Int -> Int -> Int</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	286 <li>関数名 : 型</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	287 <li>関数名引数はスペース区切り = 関数の定義や値</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	288 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	289 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	290 <li>のように定義します</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	291 <li>中置関数は、引数があるべきところに _ を書くことでできます</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	292 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	293
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	294
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	295
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	296 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	297 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	298
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	299 <div class="slide" id="13"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	300 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	301 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	302 <h1 id="agda--4">Agda で複数の引数がある関数の型</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	303 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	304 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	305
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	306 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	307 <li>_ + _ : Int -> Int -> Int</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	308 <li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	309 <p>func : A -> (A -> B) -> B</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	310 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	311 <li>引数の型 -> 返り値の型</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	312 <li>-> の結合は右結合です。なので括弧を付けると以下のようになります
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	313 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	314 <li>A -> ((A -> B) -> B)</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	315 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	316 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	317 <li>右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	318 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	319
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	320
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	321
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	322 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	323 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	324
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	325 <div class="slide" id="14"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	326 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	327 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	328 <h1 id="section-4">パターンマッチ</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	329 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	330 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	331
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	332 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	333 <li>Agda においてはデータ型は引数で分解することができます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	334 <li>ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	335 <li>Int は O か Int に S が付いたもの、でした
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	336 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	337 <li>x + O = x</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	338 <li>x + (S y) = S (x + y)</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	339 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	340 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	341 <li>関数名 (引数のパターン) = 定義</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	342 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	343
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	344
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	345
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	346 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	347 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	348
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	349 <div class="slide" id="15"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	350 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	351 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	352 <h1 id="section-5">もういちど : 自然数に対する演算の定義</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	353 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	354 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	355
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	356 <pre><code> infixl 30 _+_
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	357 _+_ : Int -> Int -> Int
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	358 x + O = x
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	359 x + (S y) = S (x + y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	360 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	361 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	362 <li>中置、関数、パターンマッチが使われています</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	363 <li>infixl は左結合を意味します。数値は結合強度です</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	364 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	365
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	366
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	367
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	368 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	369 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	370
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	371 <div class="slide" id="16"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	372 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	373 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	374 <h1 id="section-6">これから証明していきたいこと</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	375 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	376 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	377
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	378 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	379 <li>加法の交換法則 : (x + y) = (y + x)</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	380 <li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	381 <p>加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	382 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	383 <li>乗法の交換法則 : (x * y) = (y * x)</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	384 <li>乗法の結合法則 : (x * y) * z = x * (y * z)</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	385 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	386
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	387
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	388
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	389 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	390 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	391
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	392 <div class="slide" id="17"><div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	393 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	394 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	395 <h1 id="section-7">‘等しい’ ということ</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	396 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	397 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	398
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	399 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	400 <li>‘等しい’という型 _ ≡ _ を data で定義します。</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	401 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	402
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	403 <pre><code> data _≡_ {A : Set} : A -> A -> Set where
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	404 refl : {x : A} -> x == x
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	405 </code></pre>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	406
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	407 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	408 <li>defined : Relation.Binary.PropositionalEquality in Standard Library</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	409 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	410
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	411
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	412
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	413 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	414 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	415
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	416 <div class="slide" id="18"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	417 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	418 <header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	419 <h1 id="section-8">等しさを保ったままできること</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	420 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	421 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	422
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	423 <p>等しさを保ったまま変換する関数を作ると良い</p>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	424
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	425 <ul>
12 dfa919e8fb20 Fix definition sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 11 diff changeset	426 <li>sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	427 <li>cong : {A B : Set} {x y : A} -> (f : A -> B) -> x ≡ y -> f x ≡ f y</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	428 <li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	429 <p>trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z</p>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	430 </li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	431 <li>Agda tips : 記号は \ の後に文字列を入れると出てきます。 ‘≡’ は “\ ==”</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	432 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	433
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	434
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	435
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	436 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	437 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	438
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	439 <div class="slide" id="19"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	440 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	441 <header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	442 <h1 id="section-9">‘同じもの’とは</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	443 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	444 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	445
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	446 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	447 <li>項なら同じ項
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	448 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	449 <li>term : (A : Set) -> (a : Set) -> a ≡ a</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	450 <li>term A a = refl</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	451 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	452 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	453 <li>関数なら normal form が同じなら同じ
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	454 <ul>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	455 <li>lambda-term : (A : Set) -> (\ (x : A) -> x) ≡ (\ (y : A) -> y)</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	456 <li>lambda-term A = refl</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	457 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	458 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	459 <li>関数による式変形は等しいものとして扱います</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	460 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	461
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	462
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	463
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	464 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	465 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	466
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	467 <div class="slide" id="20"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	468 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	469 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	470 <h1 id="section-10">単純な証明 : 1 + 1 = 2</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	471 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	472 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	473
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	474 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	475 <li>型として (S O) + (S O) ≡ (S (S O)) を定義</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	476 <li>証明を書く</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	477 <li>‘同じもの’ の refl でおしまい</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	478 <li>自明に同じものになるのなら refl で証明ができます</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	479 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	480
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	481
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	482
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	483 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	484 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	485
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	486 <div class="slide" id="21"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	487 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	488 <header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	489 <h1 id="section-11">交換法則を型として定義する</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	490 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	491 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	492
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	493 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	494 <li>≡を用いて
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	495 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	496 <li>(x : Int) -> (y : Int) -> x + y ≡ y + x</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	497 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	498 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	499 <li>引数は (名前 : 型) として名前付けできます</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	500 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	501
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	502
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	503
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	504 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	505 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	506
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	507 <div class="slide" id="22"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	508 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	509 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	510 <h1 id="section-12">交換法則を証明していく</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	511 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	512 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	513
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	514 <pre><code> add-sym : (x y : Int) -> x + y ≡ y + x
37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	515 add-sym O O = refl
37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	516 add-sym O (S y) = cong S (add-sym O y)
37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	517 add-sym (S x) O = cong S (add-sym x O)
37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	518 add-sym (S x) (S y) = ?
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	519 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	520
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	521
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	522
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	523 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	524 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	525
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	526 <div class="slide" id="23"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	527 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	528 <header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	529 <h1 id="o-o-">O, O の場合</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	530 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	531 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	532
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	533 <ul>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	534 <li>add-sym O O = refl</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	535 <li>両方ともO の時、証明したい命題は O + O ≡ O + O</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	536 <li>_ + _ の定義の x + O = x より</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	537 <li>O ≡ O を構成したい</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	538 <li>refl によって構成する</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	539 <li>refl O と考えてもらえると良い</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	540 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	541
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	542
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	543
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	544 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	545 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	546
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	547 <div class="slide" id="24"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	548 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	549 <header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	550 <h1 id="o--s-">片方が O, 片方に S が付いている場合</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	551 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	552 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	553
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	554 <ul>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	555 <li>add-sym O (S y) = cong S (add-sym O y)</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	556 <li>式的には O + (S y) ≡ (S y) + O</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	557 <li>_ + _ の定義 x + (S y) = S (x + y) より</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	558 <li>O + (S y) ≡ S (O + y)</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	559 <li>O と y を交換して O + (S y) ≡ S (y + O)</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	560 <li>つまり y と O を交換して S をかけると良い</li>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	561 <li>交換して S をかける -> cong S (add-sym O y)</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	562 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	563
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	564
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	565
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	566 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	567 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	568
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	569 <div class="slide" id="25"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	570 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	571 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	572 <h1 id="trans-">trans による等式変形</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	573 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	574 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	575
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	576 <ul>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	577 <li>add-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	578 <li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	579 <p>等しさを保ったまま式を変形していくことが必要になります</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	580 </li>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	581 <li>add-sym (S x) (S y) = trans (f : a ≡ b) (g : b ≡ c)
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	582 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	583 <li>trans (refl) ?</li>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	584 <li>trans (trans refl (cong S (add-sym (S x) y)) ?</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	585 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	586 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	587 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	588
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	589
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	590
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	591 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	592 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	593
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	594 <div class="slide" id="26"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	595 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	596 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	597 <h1 id="reasoning-">≡-reasoning による等式変形</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	598 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	599 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	600
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	601 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	602 <li>trans が何段もネストしていくと分かりづらい</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	603 <li>≡-reasoning という等式変形の構文が Standard Library にあります</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	604 <li>Agda では見掛け上構文のような関数をAgdaでは定義できます</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	605 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	606
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	607 <pre><code> begin
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	608 変換前の式
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	609 ≡⟨ 変換する関数 ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	610 変換後の式
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	611 ∎
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	612 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	613
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	614
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	615
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	616 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	617 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	618
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	619 <div class="slide" id="27"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	620 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	621 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	622 <h1 id="reasoning--1">≡-reasoning による最初の定義</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	623 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	624 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	625
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	626
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	627 <pre><code> add-sym (S x) (S y) = begin
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	628 (S x) + (S y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	629 ≡⟨ ? ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	630 (S y) + (S x)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	631 ∎
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	632 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	633
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	634
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	635
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	636 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	637 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	638
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	639 <div class="slide" id="28"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	640 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	641 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	642 <h1 id="section-13">交換法則の証明 : + の定義による変形</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	643 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	644 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	645
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	646 <ul>
14 43c56be5f779 Fix typo Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 13 diff changeset	647 <li>_ + _ の定義である x + (S y) = S (x + y) により変形</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	648 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	649
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	650 <pre><code> add-sym (S x) (S y) = begin
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	651 (S x) + (S y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	652 ≡⟨ refl ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	653 S (S x + y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	654 ≡⟨ ? ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	655 (S y) + (S x)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	656 ∎
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	657 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	658
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	659
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	660
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	661 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	662 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	663
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	664 <div class="slide" id="29"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	665 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	666 <header>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	667 <h1 id="cong--add-sym-">cong と add-sym を使って交換</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	668 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	669 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	670
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	671 <ul>
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	672 <li>S が1つ取れたのでadd-symで交換できる</li>
37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	673 <li>add-sym で交換した後に cong で S がかかる</li>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	674 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	675
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	676 <pre><code> S ((S x) + y)
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	677 ≡⟨ cong S (add-sym (S x) y) ⟩
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	678 S ((y + (S x)))
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	679 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	680
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	681
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	682
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	683 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	684 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	685
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	686 <div class="slide" id="30"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	687 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	688 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	689 <h1 id="s">加法の時に左側からSを移動させられない</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	690 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	691 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	692
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	693
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	694 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	695 <li>加法の定義は
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	696 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	697 <li>x + (S y) = S (x + y)</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	698 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	699 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	700 <li>left-operand にかかっている S を移動させる方法が無い</li>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	701 <li>たしかに ? のについて
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	702 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	703 <li>S (y + S x) ≡ S y + S x</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	704 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	705 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	706 <li>にあてはまるものを入れてくれ、と出てきている</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	707 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	708
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	709
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	710
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	711 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	712 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	713
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	714 <div class="slide" id="31"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	715 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	716 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	717 <h1 id="left-operand-s">left-operand からSを操作する証明を定義</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	718 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	719 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	720
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	721 <pre><code> left-increment : (x y : Int) -> (S x) + y ≡ S (x + y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	722 left-increment x y = ?
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	723 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	724
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	725 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	726 <li>Agda tips : goal の上で C-c C-c で引数のパターン分け
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	727 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	728 <li>例えば y にのみ適用してみる</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	729 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	730 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	731 <li>Agda tips : goal の上で C-c C-a で証明を探してくれる</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	732 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	733
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	734
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	735
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	736 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	737 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	738
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	739 <div class="slide" id="32"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	740 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	741 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	742 <h1 id="left-operand-s-1">left-operand からSを移動させる</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	743 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	744 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	745
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	746 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	747 <li>left-increment は (S x) + y ≡ S (x + y) なので逆にして使う</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	748 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	749
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	750 <pre><code> ...
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	751 S ((S x) + y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	752 ≡⟨ sym (left-increment x (S y)) ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	753 (S y) + (S x)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	754 ∎
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	755 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	756
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	757
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	758
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	759 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	760 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	761
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	762 <div class="slide" id="33"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	763 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	764 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	765 <h1 id="x--y--y--x">加法の交換法則 : (x + y) = (y + x)</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	766 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	767 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	768
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	769 <pre><code> add-sym (S x) (S y) = begin
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	770 (S x) + (S y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	771 ≡⟨ refl ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	772 S ((S x) + y)
13 37a7b8c31a0c Replace sum-sym to add-sym Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	773 ≡⟨ cong S (add-sym (S x) y) ⟩
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	774 S (y + (S x))
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	775 ≡⟨ (sym (left-increment y (S x))) ⟩
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	776 (S y) + (S x)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	777 ∎
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	778 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	779
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	780
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	781
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	782 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	783 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	784
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	785 <div class="slide" id="34"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	786 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	787 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	788 <h1 id="x--y--z--x--y--z">加法の結合法則 : (x + y) + z = x + (y + z)</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	789 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	790 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	791
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	792 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	793 <li>次に結合法則を証明します</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	794 <li>手順は同じです
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	795 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	796 <li>≡ で証明したい式を定義</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	797 <li>定義に証明を書く</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	798 <li>必要ならば等式を変形していく</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	799 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	800 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	801 <li>ちなみに x + y + z は infixl なので ((x + y) + z) となります</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	802 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	803
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	804
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	805
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	806 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	807 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	808
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	809 <div class="slide" id="35"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	810 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	811 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	812 <h1 id="agda--5">Agda による証明方法のまとめ</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	813 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	814 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	815
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	816 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	817 <li>関数の型を命題、関数の定義を証明とする</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	818 <li>等しさを証明するには等しいという型を定義する</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	819 <li>等しさを保ったまま式を変形していくことにより等価性を証明できる
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	820 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	821 <li>trans, reasoning</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	822 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	823 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	824 <li>C-c C-l により型のチェックが成功すれば証明終了</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	825 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	826
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	827
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	828
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	829 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	830 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	831
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	832 <div class="slide" id="36"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	833 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	834 <header>
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	835 <h1 id="section-14">乗法の定義</h1>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	836 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	837 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	838
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	839 <pre><code> infixl 40 _*_
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	840 _*_ : Int -> Int -> Int
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	841 n * O = O
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	842 n * (S O) = n
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	843 n * (S m) = n + (n * m)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	844 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	845
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	846 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	847 <li><em>+</em> よりも結合強度を上げるといわゆる自然数の演算</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	848 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	849
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	850
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	851
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	852 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	853 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	854
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	855 <div class="slide" id="37"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	856 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	857 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	858 <h1 id="x--y--y--x-1">乗法の交換法則 : (x * y) = (y * x)</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	859 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	860 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	861
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	862 <pre><code> mult-sym : (x y : Int) -> x * y ≡ y * x
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	863 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	864
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	865 <p>途中で</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	866
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	867 <pre><code> (x y : Int) -> (S x) * y ≡ y + (x * y)
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	868 </code></pre>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	869
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	870 <p>が必要になることが分かる</p>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	871
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	872
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	873
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	874 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	875 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	876
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	877 <div class="slide" id="38"><div>
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	878 <section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	879 <header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	880 <h1 id="agda">Agdaにおいて何ができるのか</h1>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	881 </header>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	882 <!-- _S9SLIDE_ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	883
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	884 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	885 <li>証明の正しさを対話的に教えてくれる
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	886 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	887 <li>それに必要な証明が結果的に分かることもある</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	888 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	889 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	890 <li>今回は Int に対する演算だった
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	891 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	892 <li>lambda-term に落とせれば Agda で証明していける</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	893 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	894 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	895 <li>他にも命題論理の証明などがある</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	896 <li>プログラミング言語そのものに対するアプローチ
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	897 <ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	898 <li>lambda-term の等価性によってリファクタリングなど</li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	899 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	900 </li>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	901 </ul>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	902
11 9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	903
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	904
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	905 </section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	906 </div></div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	907
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	908 <div class="slide" id="39"><div>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	909 <section>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	910 <header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	911 <h1 id="section-15">良くあるエラー</h1>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	912 </header>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	913 <!-- _S9SLIDE_ -->
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	914
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	915 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	916 <li>parse error
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	917 <ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	918 <li>スペースある無しで意味が変わります</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	919 <li>A: Set <- NG</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	920 <li>A : Set <- OK</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	921 <li>A: という term がありえるから</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	922 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	923 </li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	924 <li>型が合わない -> 赤で警告されます</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	925 <li>情報が足りない -> 黄色で警告されます</li>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	926 </ul>
9876354c1c19 Update to OSC Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	927
9 170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	928 <!-- vim: set filetype=markdown.slide: -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	929 <!-- === end markdown block === -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	930
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	931 </section>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	932 </div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	933
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	934
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	935 <!--
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	936 To hide progress bar from entire presentation
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	937 just remove “progress” element.
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	938 -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	939 <div class="progress"><div></div></div>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	940 <script src="scripts/script.js"></script>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	941 <!-- Copyright © 2010–2011 Vadim Makeev, http://pepelsbey.net/ -->
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	942 </body>
170a67c4198c Generate slides Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	943 </html>

Mercurial > hg > Papers > 2015 > atton-osc

annotate slide.html @ 14:43c56be5f779 default tip