diff --git a/.gitignore b/.gitignore index de81573..f105203 100644 --- a/.gitignore +++ b/.gitignore @@ -305,3 +305,4 @@ TSWLatexianTemp* *.agdai MAlonzo/** +*.html diff --git a/agda/Agda.css b/agda/Agda.css new file mode 100644 index 0000000..dee5578 --- /dev/null +++ b/agda/Agda.css @@ -0,0 +1,467 @@ +/*! normalize.css v2.1.3 | MIT License | git.io/normalize */ + +/* ========================================================================== + HTML5 display definitions + ========================================================================== */ + +/** + * Correct `block` display not defined in IE 8/9. + */ + + article, + aside, + details, + figcaption, + figure, + footer, + header, + hgroup, + main, + nav, + section, + summary { + display: block; + } + + /** + * Correct `inline-block` display not defined in IE 8/9. + */ + + audio, + canvas, + video { + display: inline-block; + } + + /** + * Prevent modern browsers from displaying `audio` without controls. + * Remove excess height in iOS 5 devices. + */ + + audio:not([controls]) { + display: none; + height: 0; + } + + /** + * Address `[hidden]` styling not present in IE 8/9. + * Hide the `template` element in IE, Safari, and Firefox < 22. + */ + + [hidden], + template { + display: none; + } + + /* ========================================================================== + Base + ========================================================================== */ + + /** + * 1. Set default font family to sans-serif. + * 2. Prevent iOS text size adjust after orientation change, without disabling + * user zoom. + */ + + html { + font-family: sans-serif; /* 1 */ + -ms-text-size-adjust: 100%; /* 2 */ + -webkit-text-size-adjust: 100%; /* 2 */ + } + + /** + * Remove default margin. + */ + + body { + margin: 0; + } + + /* ========================================================================== + Links + ========================================================================== */ + + /** + * Remove the gray background color from active links in IE 10. + */ + + a { + background: transparent; + } + + /** + * Address `outline` inconsistency between Chrome and other browsers. + */ + + a:focus { + outline: thin dotted; + } + + /** + * Improve readability when focused and also mouse hovered in all browsers. + */ + + a:active, + a:hover { + outline: 0; + } + + /* ========================================================================== + Typography + ========================================================================== */ + + /** + * Address variable `h1` font-size and margin within `section` and `article` + * contexts in Firefox 4+, Safari 5, and Chrome. + */ + + h1 { + font-size: 2em; + margin: 0.67em 0; + } + + /** + * Address styling not present in IE 8/9, Safari 5, and Chrome. + */ + + abbr[title] { + border-bottom: 1px dotted; + } + + /** + * Address style set to `bolder` in Firefox 4+, Safari 5, and Chrome. + */ + + b, + strong { + font-weight: bold; + } + + /** + * Address styling not present in Safari 5 and Chrome. + */ + + dfn { + font-style: italic; + } + + /** + * Address differences between Firefox and other browsers. + */ + + hr { + -moz-box-sizing: content-box; + box-sizing: content-box; + height: 0; + } + + /** + * Address styling not present in IE 8/9. + */ + + mark { + background: #ff0; + color: #000; + } + + /** + * Correct font family set oddly in Safari 5 and Chrome. + */ + + code, + kbd, + pre, + samp { + font-family: monospace, serif; + font-size: 1em; + } + + /** + * Improve readability of pre-formatted text in all browsers. + */ + + pre { + white-space: pre; + overflow-x: scroll; + } + + /** + * Set consistent quote types. + */ + + q { + quotes: "\201C" "\201D" "\2018" "\2019"; + } + + /** + * Address inconsistent and variable font size in all browsers. + */ + + small { + font-size: 80%; + } + + /** + * Prevent `sub` and `sup` affecting `line-height` in all browsers. + */ + + sub, + sup { + font-size: 75%; + line-height: 0; + position: relative; + vertical-align: baseline; + } + + sup { + top: -0.5em; + } + + sub { + bottom: -0.25em; + } + + /* ========================================================================== + Embedded content + ========================================================================== */ + + /** + * Remove border when inside `a` element in IE 8/9. + */ + + img { + border: 0; + } + + /** + * Correct overflow displayed oddly in IE 9. + */ + + svg:not(:root) { + overflow: hidden; + } + + /* ========================================================================== + Figures + ========================================================================== */ + + /** + * Address margin not present in IE 8/9 and Safari 5. + */ + + figure { + margin: 0; + } + + /* ========================================================================== + Forms + ========================================================================== */ + + /** + * Define consistent border, margin, and padding. + */ + + fieldset { + border: 1px solid #c0c0c0; + margin: 0 2px; + padding: 0.35em 0.625em 0.75em; + } + + /** + * 1. Correct `color` not being inherited in IE 8/9. + * 2. Remove padding so people aren't caught out if they zero out fieldsets. + */ + + legend { + border: 0; /* 1 */ + padding: 0; /* 2 */ + } + + /** + * 1. Correct font family not being inherited in all browsers. + * 2. Correct font size not being inherited in all browsers. + * 3. Address margins set differently in Firefox 4+, Safari 5, and Chrome. + */ + + button, + input, + select, + textarea { + font-family: inherit; /* 1 */ + font-size: 100%; /* 2 */ + margin: 0; /* 3 */ + } + + /** + * Address Firefox 4+ setting `line-height` on `input` using `!important` in + * the UA stylesheet. + */ + + button, + input { + line-height: normal; + } + + /** + * Address inconsistent `text-transform` inheritance for `button` and `select`. + * All other form control elements do not inherit `text-transform` values. + * Correct `button` style inheritance in Chrome, Safari 5+, and IE 8+. + * Correct `select` style inheritance in Firefox 4+ and Opera. + */ + + button, + select { + text-transform: none; + } + + /** + * 1. Avoid the WebKit bug in Android 4.0.* where (2) destroys native `audio` + * and `video` controls. + * 2. Correct inability to style clickable `input` types in iOS. + * 3. Improve usability and consistency of cursor style between image-type + * `input` and others. + */ + + button, + html input[type="button"], /* 1 */ + input[type="reset"], + input[type="submit"] { + -webkit-appearance: button; /* 2 */ + cursor: pointer; /* 3 */ + } + + /** + * Re-set default cursor for disabled elements. + */ + + button[disabled], + html input[disabled] { + cursor: default; + } + + /** + * 1. Address box sizing set to `content-box` in IE 8/9/10. + * 2. Remove excess padding in IE 8/9/10. + */ + + input[type="checkbox"], + input[type="radio"] { + box-sizing: border-box; /* 1 */ + padding: 0; /* 2 */ + } + + /** + * 1. Address `appearance` set to `searchfield` in Safari 5 and Chrome. + * 2. Address `box-sizing` set to `border-box` in Safari 5 and Chrome + * (include `-moz` to future-proof). + */ + + input[type="search"] { + -webkit-appearance: textfield; /* 1 */ + -moz-box-sizing: content-box; + -webkit-box-sizing: content-box; /* 2 */ + box-sizing: content-box; + } + + /** + * Remove inner padding and search cancel button in Safari 5 and Chrome + * on OS X. + */ + + input[type="search"]::-webkit-search-cancel-button, + input[type="search"]::-webkit-search-decoration { + -webkit-appearance: none; + } + + /** + * Remove inner padding and border in Firefox 4+. + */ + + button::-moz-focus-inner, + input::-moz-focus-inner { + border: 0; + padding: 0; + } + + /** + * 1. Remove default vertical scrollbar in IE 8/9. + * 2. Improve readability and alignment in all browsers. + */ + + textarea { + overflow: auto; /* 1 */ + vertical-align: top; /* 2 */ + } + + /* ========================================================================== + Tables + ========================================================================== */ + + /** + * Remove most spacing between table cells. + */ + + table { + border-collapse: collapse; + border-spacing: 0; + } + + .go-top { + position: fixed; + bottom: 2em; + right: 2em; + text-decoration: none; + background-color: #E0E0E0; + font-size: 12px; + padding: 1em; + display: inline; + } + + /* Github css */ + + html,body{ margin: auto; + padding-right: 1em; + padding-left: 1em; + color:black;}*:not('#mkdbuttons'){margin:0;padding:0}body{font:13.34px helvetica,arial,freesans,clean,sans-serif;-webkit-font-smoothing:subpixel-antialiased;line-height:1.4;padding:3px;background:#fff;border-radius:3px;-moz-border-radius:3px;-webkit-border-radius:3px}p{margin:1em 0}a{color:#4183c4;text-decoration:none}body{background-color:#fff;padding:30px;margin:15px;font-size:14px;line-height:1.6}body>*:first-child{margin-top:0!important}body>*:last-child{margin-bottom:0!important}@media screen{body{box-shadow:0 0 0 1px #cacaca,0 0 0 4px #eee}}h1,h2,h3,h4,h5,h6{margin:20px 0 10px;padding:0;font-weight:bold;-webkit-font-smoothing:subpixel-antialiased;cursor:text}h1{font-size:28px;color:#000}h2{font-size:24px;border-bottom:1px solid #ccc;color:#000}h3{font-size:18px;color:#333}h4{font-size:16px;color:#333}h5{font-size:14px;color:#333}h6{color:#777;font-size:14px}p,blockquote,table,pre{margin:15px 0}ul{padding-left:30px}ol{padding-left:30px}ol li ul:first-of-type{margin-top:0}hr{background:transparent url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAYAAAAECAYAAACtBE5DAAAAGXRFWHRTb2Z0d2FyZQBBZG9iZSBJbWFnZVJlYWR5ccllPAAAAyJpVFh0WE1MOmNvbS5hZG9iZS54bXAAAAAAADw/eHBhY2tldCBiZWdpbj0i77u/IiBpZD0iVzVNME1wQ2VoaUh6cmVTek5UY3prYzlkIj8+IDx4OnhtcG1ldGEgeG1sbnM6eD0iYWRvYmU6bnM6bWV0YS8iIHg6eG1wdGs9IkFkb2JlIFhNUCBDb3JlIDUuMC1jMDYwIDYxLjEzNDc3NywgMjAxMC8wMi8xMi0xNzozMjowMCAgICAgICAgIj4gPHJkZjpSREYgeG1sbnM6cmRmPSJodHRwOi8vd3d3LnczLm9yZy8xOTk5LzAyLzIyLXJkZi1zeW50YXgtbnMjIj4gPHJkZjpEZXNjcmlwdGlvbiByZGY6YWJvdXQ9IiIgeG1sbnM6eG1wPSJodHRwOi8vbnMuYWRvYmUuY29tL3hhcC8xLjAvIiB4bWxuczp4bXBNTT0iaHR0cDovL25zLmFkb2JlLmNvbS94YXAvMS4wL21tLyIgeG1sbnM6c3RSZWY9Imh0dHA6Ly9ucy5hZG9iZS5jb20veGFwLzEuMC9zVHlwZS9SZXNvdXJjZVJlZiMiIHhtcDpDcmVhdG9yVG9vbD0iQWRvYmUgUGhvdG9zaG9wIENTNSBNYWNpbnRvc2giIHhtcE1NOkluc3RhbmNlSUQ9InhtcC5paWQ6OENDRjNBN0E2NTZBMTFFMEI3QjRBODM4NzJDMjlGNDgiIHhtcE1NOkRvY3VtZW50SUQ9InhtcC5kaWQ6OENDRjNBN0I2NTZBMTFFMEI3QjRBODM4NzJDMjlGNDgiPiA8eG1wTU06RGVyaXZlZEZyb20gc3RSZWY6aW5zdGFuY2VJRD0ieG1wLmlpZDo4Q0NGM0E3ODY1NkExMUUwQjdCNEE4Mzg3MkMyOUY0OCIgc3RSZWY6ZG9jdW1lbnRJRD0ieG1wLmRpZDo4Q0NGM0E3OTY1NkExMUUwQjdCNEE4Mzg3MkMyOUY0OCIvPiA8L3JkZjpEZXNjcmlwdGlvbj4gPC9yZGY6UkRGPiA8L3g6eG1wbWV0YT4gPD94cGFja2V0IGVuZD0iciI/PqqezsUAAAAfSURBVHjaYmRABcYwBiM2QSA4y4hNEKYDQxAEAAIMAHNGAzhkPOlYAAAAAElFTkSuQmCC) repeat-x 0 0;border:0 none;color:#ccc;height:4px;padding:0}body>h2:first-child{margin-top:0;padding-top:0}body>h1:first-child{margin-top:0;padding-top:0}body>h1:first-child+h2{margin-top:0;padding-top:0}body>h3:first-child,body>h4:first-child,body>h5:first-child,body>h6:first-child{margin-top:0;padding-top:0}a:first-child h1,a:first-child h2,a:first-child h3,a:first-child h4,a:first-child h5,a:first-child h6{margin-top:0;padding-top:0}h1+p,h2+p,h3+p,h4+p,h5+p,h6+p,ul li>:first-child,ol li>:first-child{margin-top:0}dl{padding:0}dl dt{font-size:14px;font-weight:bold;font-style:italic;padding:0;margin:15px 0 5px}dl dt:first-child{padding:0}dl dt>:first-child{margin-top:0}dl dt>:last-child{margin-bottom:0}dl dd{margin:0 0 15px;padding:0 15px}dl dd>:first-child{margin-top:0}dl dd>:last-child{margin-bottom:0}blockquote{border-left:4px solid #DDD;padding:0 15px;color:#777}blockquote>:first-child{margin-top:0}blockquote>:last-child{margin-bottom:0}table{border-collapse:collapse;border-spacing:0;font-size:100%;font:inherit}table th{font-weight:bold;border:1px solid #ccc;padding:6px 13px}table td{border:1px solid #ccc;padding:6px 13px}table tr{border-top:1px solid #ccc;background-color:#fff}table tr:nth-child(2n){background-color:#f8f8f8}img{max-width:100%}code,tt{margin:0 2px;padding:0 5px;white-space:nowrap;border:1px solid #eaeaea;background-color:#f8f8f8;border-radius:3px;font-family:Consolas,'Liberation Mono',Courier,monospace;font-size:12px;color:#333}pre>code{margin:0;padding:0;white-space:pre;border:0;background:transparent}.highlight pre{background-color:#f8f8f8;border:1px solid #ccc;font-size:13px;line-height:19px;overflow:auto;padding:6px 10px;border-radius:3px}pre{background-color:#f8f8f8;border:1px solid #ccc;font-size:13px;line-height:19px;overflow:auto;padding:6px 10px;border-radius:3px}pre code,pre tt{background-color:transparent;border:0}.poetry pre{font-family:Georgia,Garamond,serif!important;font-style:italic;font-size:110%!important;line-height:1.6em;display:block;margin-left:1em}.poetry pre code{font-family:Georgia,Garamond,serif!important;word-break:break-all;word-break:break-word;-webkit-hyphens:auto;-moz-hyphens:auto;hyphens:auto;white-space:pre-wrap}sup,sub,a.footnote{font-size:1.4ex;height:0;line-height:1;vertical-align:super;position:relative}sub{vertical-align:sub;top:-1px}@media print{body{background:#fff}img,pre,blockquote,table,figure{page-break-inside:avoid}body{background:#fff;border:0}code{background-color:#fff;color:#333!important;padding:0 .2em;border:1px solid #dedede}pre{background:#fff}pre code{background-color:white!important;overflow:visible}}@media screen{body.inverted{color:#eee!important;border-color:#555;box-shadow:none}.inverted body,.inverted hr .inverted p,.inverted td,.inverted li,.inverted h1,.inverted h2,.inverted h3,.inverted h4,.inverted h5,.inverted h6,.inverted th,.inverted .math,.inverted caption,.inverted dd,.inverted dt,.inverted blockquote{color:#eee!important;border-color:#555;box-shadow:none}.inverted td,.inverted th{background:#333}.inverted h2{border-color:#555}.inverted hr{border-color:#777;border-width:1px!important}::selection{background:rgba(157,193,200,0.5)}h1::selection{background-color:rgba(45,156,208,0.3)}h2::selection{background-color:rgba(90,182,224,0.3)}h3::selection,h4::selection,h5::selection,h6::selection,li::selection,ol::selection{background-color:rgba(133,201,232,0.3)}code::selection{background-color:rgba(0,0,0,0.7);color:#eee}code span::selection{background-color:rgba(0,0,0,0.7)!important;color:#eee!important}a::selection{background-color:rgba(255,230,102,0.2)}.inverted a::selection{background-color:rgba(255,230,102,0.6)}td::selection,th::selection,caption::selection{background-color:rgba(180,237,95,0.5)}.inverted{background:#0b2531;background:#252a2a}.inverted body{background:#252a2a}.inverted a{color:#acd1d5}}.highlight .c{color:#998;font-style:italic}.highlight .err{color:#a61717;background-color:#e3d2d2}.highlight .k,.highlight .o{font-weight:bold}.highlight .cm{color:#998;font-style:italic}.highlight .cp{color:#999;font-weight:bold}.highlight .c1{color:#998;font-style:italic}.highlight .cs{color:#999;font-weight:bold;font-style:italic}.highlight .gd{color:#000;background-color:#fdd}.highlight .gd .x{color:#000;background-color:#faa}.highlight .ge{font-style:italic}.highlight .gr{color:#a00}.highlight .gh{color:#999}.highlight .gi{color:#000;background-color:#dfd}.highlight .gi .x{color:#000;background-color:#afa}.highlight .go{color:#888}.highlight .gp{color:#555}.highlight .gs{font-weight:bold}.highlight .gu{color:#800080;font-weight:bold}.highlight .gt{color:#a00}.highlight .kc,.highlight .kd,.highlight .kn,.highlight .kp,.highlight .kr{font-weight:bold}.highlight .kt{color:#458;font-weight:bold}.highlight .m{color:#099}.highlight .s{color:#d14}.highlight .na{color:#008080}.highlight .nb{color:#0086b3}.highlight .nc{color:#458;font-weight:bold}.highlight .no{color:#008080}.highlight .ni{color:#800080}.highlight .ne,.highlight .nf{color:#900;font-weight:bold}.highlight .nn{color:#555}.highlight .nt{color:#000080}.highlight .nv{color:#008080}.highlight .ow{font-weight:bold}.highlight .w{color:#bbb}.highlight .mf,.highlight .mh,.highlight .mi,.highlight .mo{color:#099}.highlight .sb,.highlight .sc,.highlight .sd,.highlight .s2,.highlight .se,.highlight .sh,.highlight .si,.highlight .sx{color:#d14}.highlight .sr{color:#009926}.highlight .s1{color:#d14}.highlight .ss{color:#990073}.highlight .bp{color:#999}.highlight .vc,.highlight .vg,.highlight .vi{color:#008080}.highlight .il{color:#099}.highlight .gc{color:#999;background-color:#eaf2f5}.type-csharp .highlight .k,.type-csharp .highlight .kt{color:#00F}.type-csharp .highlight .nf{color:#000;font-weight:normal}.type-csharp .highlight .nc{color:#2b91af}.type-csharp .highlight .nn{color:#000}.type-csharp .highlight .s,.type-csharp .highlight .sc{color:#a31515} + +/* Aspects. */ +.Agda .Comment { color: #B22222 } +.Agda .Background { color: #000000 } +.Agda .Markup { color: #000000 } +.Agda .Keyword { color: #CD6600 } +.Agda .String { color: #B22222 } +.Agda .Number { color: #A020F0 } +.Agda .Symbol { color: #404040 } +.Agda .PrimitiveType { color: #0000CD } +.Agda .Pragma { color: black } +.Agda .Operator {} +.Agda .Hole { background: #B4EEB4 } + +/* NameKinds. */ +.Agda .Bound { color: black } +.Agda .Generalizable { color: black } +.Agda .InductiveConstructor { color: #008B00 } +.Agda .CoinductiveConstructor { color: #8B7500 } +.Agda .Datatype { color: #0000CD } +.Agda .Field { color: #EE1289 } +.Agda .Function { color: #0000CD } +.Agda .Module { color: #A020F0 } +.Agda .Postulate { color: #0000CD } +.Agda .Primitive { color: #0000CD } +.Agda .Record { color: #0000CD } + +/* OtherAspects. */ +.Agda .DottedPattern {} +.Agda .UnsolvedMeta { color: black; background: yellow } +.Agda .UnsolvedConstraint { color: black; background: yellow } +.Agda .TerminationProblem { color: black; background: #FFA07A } +.Agda .IncompletePattern { color: black; background: #F5DEB3 } +.Agda .Error { color: red; text-decoration: underline } +.Agda .TypeChecks { color: black; background: #ADD8E6 } +.Agda .Deadcode { color: black; background: #808080 } +.Agda .ShadowingInTelescope { color: black; background: #808080 } + +/* Standard attributes. */ +.Agda a { text-decoration: none } +.Agda a[href]:hover { background-color: #B4EEB4 } +.Agda [href].hover-highlight { background-color: #B4EEB4; } diff --git a/agda/Makefile b/agda/Makefile new file mode 100644 index 0000000..afb9995 --- /dev/null +++ b/agda/Makefile @@ -0,0 +1,25 @@ +.PHONY: all clean + +all: agda + make pandoc + +open: + firefox ./public/algebra.html + +agda: Everything.agda + agda --html --html-dir=public algebra.lagda.md --html-highlight=auto -i. + rm -f public/Agda.css + cp Agda.css public/Agda.css + +pandoc: public/*.md + @$(foreach file,$^, \ + pandoc $(file) -s --to=html+TEX_MATH_DOLLARS --mathjax -c Agda.css -o $(file:.md=.html) ; \ + ) + +clean: + rm -f Everything.agda + rm -rf public/* + find . -name '*.agdai' -exec rm \{\} \; + +Everything.agda: + git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda \ No newline at end of file diff --git a/agda/algebra.lagda.md b/agda/algebra.lagda.md new file mode 100644 index 0000000..63afea7 --- /dev/null +++ b/agda/algebra.lagda.md @@ -0,0 +1,486 @@ +```agda +open import equality +module algebra where +``` + +# Algebra of programming + +## Preliminaries (Types, Lemmas, Functions) + +```agda + id : ∀ {A : Set} → A → A + id a = a + + _! : ∀ {A B : Set} → (b : B) → A → B + (b !) _ = b +``` + +We will need functional extensionality + +```agda + postulate + extensionality : ∀ {A B : Set} (f g : A → B) → (∀ (x : A) → f x ≡ g x) → f ≡ g + + ext-rev : ∀ {A B : Set} {f g : A → B} → f ≡ g → (∀ (x : A) → f x ≡ g x) + ext-rev {A} {B} {f} {g} refl x = refl +``` + +Function composition and some facts about it + +```agda + infixr 9 _∘_ + _∘_ : ∀ {A B C : Set} (g : B → C) (f : A → B) → A → C + (g ∘ f) x = g (f x) + {-# INLINE _∘_ #-} + + identityʳ : ∀ {A B : Set} {f : A → B} → f ∘ id ≡ f + identityʳ {f} = refl + + identityˡ : ∀ {A B : Set} {f : A → B} → id ∘ f ≡ f + identityˡ {f} = refl + + _⟩∘⟨_ : ∀ {A B C : Set} {g i : B → C} {f h : A → B} → g ≡ i → f ≡ h → g ∘ f ≡ i ∘ h + refl ⟩∘⟨ refl = refl + + introˡ : ∀ {A B : Set} {f : A → B} {h : B → B} → h ≡ id → f ≡ h ∘ f + introˡ {f} {h} eq = trans (sym identityˡ) (sym eq ⟩∘⟨ refl) + + introʳ : ∀ {A B : Set} {f : A → B} {h : A → A} → h ≡ id → f ≡ f ∘ h + introʳ {f} {h} eq = trans (sym identityʳ) (refl ⟩∘⟨ sym eq) +``` + +## Unit and void type + +```agda + data ⊤ : Set where + unit : ⊤ + + data ⊥ : Set where + + ¡ : ∀ {B : Set} → ⊥ → B + ¡ () + + ¡-unique : ∀ {B : Set} → (f : ⊥ → B) → f ≡ ¡ + ¡-unique f = extensionality f ¡ (λ ()) +``` + +## Products + +```agda + infixr 8 _×_ + infixr 7 _×₁_ + record _×_ (A B : Set) : Set where + constructor _,_ + field + outl : A + outr : B + open _×_ + + ×-cong : ∀ {A B : Set} {x y : A} {u v : B} → x ≡ y → u ≡ v → (x , u) ≡ (y , v) + ×-cong refl refl = refl + + ⟨_,_⟩ : {A B C : Set} → (A → B) → (A → C) → A → B × C + ⟨ f , g ⟩ x = (f x) , (g x) + project₁ : ∀ {A B C : Set} (f : A → B) (g : A → C) → outl ∘ ⟨ f , g ⟩ ≡ f + project₁ _ _ = refl + project₂ : ∀ {A B C : Set} (f : A → B) (g : A → C) → outr ∘ ⟨ f , g ⟩ ≡ g + project₂ _ _ = refl + + ⟨⟩-cong : {A B C : Set} → (f g : A → B) → (h i : A → C) → f ≡ g → h ≡ i → ⟨ f , h ⟩ ≡ ⟨ g , i ⟩ + ⟨⟩-cong f g h i refl refl = refl + + ⟨⟩-unique : ∀ {A B C : Set} (f : A → B) (g : A → C) (h : A → B × C) → outl ∘ h ≡ f → outr ∘ h ≡ g → h ≡ ⟨ f , g ⟩ + ⟨⟩-unique f g h refl refl = refl + + _×₁_ : ∀ {A B C D : Set} (f : A → C) (g : B → D) → A × B → C × D + _×₁_ f g (x , y) = f x , g y +``` + +Composition as function on products + +```agda + comp : ∀ {A B C : Set} → ((A → B) × (B → C)) → A → C + comp (f , g) x = g (f x) +``` + +curry, uncurry, eval + +```agda + curry : ∀ {A B C : Set} → (A × B → C) → (A → B → C) + curry f a b = f (a , b) + + uncurry : ∀ {A B C : Set} → (A → B → C) → (A × B → C) + uncurry f (a , b) = f a b + + ev : ∀ {A B : Set} → (A → B) × A → B + ev (f , a) = f a +``` + +**HOMEWORK 1** + +```agda + curry-uncurry : ∀ {A B C : Set} → curry ∘ uncurry {A} {B} {C} ≡ id + curry-uncurry = extensionality (curry ∘ uncurry) id λ _ → refl + + uncurry-curry : ∀ {A B C : Set} → uncurry ∘ curry {A} {B} {C} ≡ id + uncurry-curry = extensionality (uncurry ∘ curry) id λ _ → refl +``` + +## Naturals + +```agda + data ℕ : Set where + zero : ℕ + succ : ℕ → ℕ + {-# BUILTIN NATURAL ℕ #-} + + data 𝔹 : Set where + true : 𝔹 + false : 𝔹 + {-# BUILTIN BOOL 𝔹 #-} + + succ-inj : ∀ {x y : ℕ} → succ x ≡ succ y → x ≡ y + succ-inj refl = refl + + -- todo rewrite foldn to use ugly cartesian product... + foldn : ∀ {C : Set} → (C × (C → C)) → ℕ → C + foldn (c , h) zero = c + foldn (c , h) (succ n) = h (foldn (c , h) n) + + foldn-id : foldn (zero , succ) ≡ id {ℕ} + foldn-id = extensionality (foldn (zero , succ)) id helper + where + helper : (x : ℕ) → foldn (zero , succ) x ≡ id x + helper zero = refl + helper (succ n) rewrite helper n = refl + + foldn-fusion : ∀ {C C' : Set} (c : C) (h : C → C) (k : C → C') (c' : C') (h' : C' → C') → k c ≡ c' → k ∘ h ≡ h' ∘ k → k ∘ foldn (c , h) ≡ foldn (c' , h') + foldn-fusion {C} {C'} c h k c' h' refl eq = extensionality (k ∘ foldn (c , h)) (foldn (k c , h')) helper + where + helper : (x : ℕ) → (k ∘ foldn (c , h)) x ≡ foldn (k c , h') x + helper zero = refl + helper (succ x) = begin + (k ∘ h) (foldn (c , h) x) ≡⟨ ext-rev eq (foldn (c , h) x) ⟩ + (h' ∘ k) (foldn (c , h) x) ≡⟨ cong h' (helper x) ⟩ + h' (foldn (k c , h') x) ∎ +``` + +### proving with the fusion law + +```agda + add : ℕ → ℕ → ℕ + add zero n = n + add (succ m) n = succ (add m n) + + plus : ℕ → ℕ → ℕ + plus n = foldn (n , succ) + plus' : ℕ → ℕ → ℕ + plus' = foldn (id , (comp ∘ ⟨ id , succ ! ⟩)) + plus-test1 : plus 13 19 ≡ 32 + plus-test1 = refl + + + : ℕ × ℕ → ℕ + + = uncurry (foldn (id , (comp ∘ ⟨ id , succ ! ⟩))) + +-test1 : + (3 , 5) ≡ 8 + +-test1 = refl + +-test2 : + (0 , 100) ≡ 100 + +-test2 = refl + +-test3 : + (100 , 0) ≡ 100 + +-test3 = refl + + +0 : ∀ (n : ℕ) → + (n , 0) ≡ n + +0 zero = refl + +0 (succ n) rewrite +0 n = refl + + -- TODO define with fusion la + plus-succˡ : ∀ {m n : ℕ} → succ (plus m n) ≡ plus (succ m) n + plus-succˡ {m} {zero} = refl + plus-succˡ {m} {succ n} rewrite plus-succˡ {m} {n} = refl + plus-comm : ∀ {m n : ℕ} → plus m n ≡ plus n m + plus-comm {zero} {n} = ext-rev foldn-id n + plus-comm {succ m} {n} rewrite plus-comm {n} {m} = sym (plus-succˡ {m} {n}) + + plus-comm' : ∀ {m n : ℕ} → (plus m) ∘ (plus n) ≡ (plus n) ∘ (plus m) + plus-comm' {m} {n} = begin + (plus m) ∘ (foldn (n , succ)) ≡⟨ commute₁ ⟩ + foldn ((plus m n) , succ) ≡⟨ extensionality (foldn ((plus m n) , succ)) (foldn ((plus n m) , succ)) helper ⟩ + foldn ((plus n m) , succ) ≡⟨ sym commute₂ ⟩ + (plus n) ∘ (foldn (m , succ)) ∎ + where + helper : (x : ℕ) → foldn ((plus m n) , succ) x ≡ foldn ((plus n m) , succ) x + helper x rewrite plus-comm {m} {n} = refl + commute₁ = foldn-fusion n succ (plus m) (plus m n) succ refl refl + commute₂ = foldn-fusion m succ (plus n) (plus n m) succ refl refl +``` + +**HOMEWORK 2** + +```agda + mul : ℕ → ℕ → ℕ + mul zero n = zero + mul (succ m) n = plus n (mul m n) + mul-test1 : mul 0 3 ≡ 0 + mul-test1 = refl + mul-test2 : mul 3 15 ≡ 45 + mul-test2 = refl + + mult : (m : ℕ) → ℕ → ℕ + mult m = foldn (zero , (plus m)) + + times : (ℕ × ℕ) → ℕ + times = uncurry times' + where + times' : ℕ → ℕ → ℕ + times' = foldn ((zero !) , (comp ∘ ⟨ curry ⟨ outr , ev ⟩ , + ! ⟩)) + times-test1 : times (1 , 1) ≡ 1 + times-test1 = refl + times-test2 : times (123 , 15) ≡ 1845 + times-test2 = refl + times-test3 : times (5 , 0) ≡ 0 + times-test3 = refl +``` + +**HOMEWORK 3** + +```agda + fac2 : ℕ → ℕ + fac2 zero = 1 + fac2 (succ n) = times (n , fac2 n) + + fac : ℕ → ℕ + fac = outr ∘ fac' + where + fac' : ℕ → (ℕ × ℕ) + fac' = foldn ((zero , succ zero) , ⟨ succ ∘ outl , times ∘ (succ ×₁ id) ⟩) + fac-test1 : fac 5 ≡ 120 + fac-test1 = refl + fac-test2 : fac 0 ≡ 1 + fac-test2 = refl +``` + +Proofs from the script + +```agda + distrib : ∀ (m n x : ℕ) → mult m (plus n x) ≡ plus (mult m n) (mult m x) + distrib m n x = begin + mult m (plus n x) ≡⟨ refl ⟩ + mult m (foldn (n , succ) x) ≡⟨ ext-rev commute₁ x ⟩ + foldn ((mult m n) , (plus m)) x ≡⟨ sym (ext-rev commute₂ x) ⟩ + plus (mult m n) (foldn (zero , (plus m)) x) ≡⟨ refl ⟩ + plus (mult m n) (mult m x) ∎ + where + commute₁ : (mult m) ∘ (foldn (n , succ)) ≡ foldn ((mult m n) , (plus m)) + commute₁ = foldn-fusion n succ (mult m) (mult m n) (plus m) kc kh + where + kc : mult m n ≡ mult m n + kc = refl + kh : mult m ∘ succ ≡ plus m ∘ mult m + kh = refl + commute₂ : (plus (mult m n)) ∘ (foldn (zero , (plus m))) ≡ foldn ((mult m n) , (plus m)) + commute₂ = foldn-fusion zero (plus m) (plus (mult m n)) (mult m n) (plus m) kc (kh m n) + where + kc : plus (mult m n) zero ≡ mult m n + kc = refl + kh : ∀ (m n : ℕ) → (plus (mult m n)) ∘ (plus m) ≡ (plus m) ∘ (plus (mult m n)) + kh zero zero = refl + kh (succ m) zero = plus-comm' + kh m (succ n) = plus-comm' + + induction : ∀ (p : ℕ → 𝔹) → p zero ≡ true → (∀ (n : ℕ) → p (succ n) ≡ p n) → p ≡ true ! + induction p IS IH = begin + p ≡⟨ introʳ foldn-id ⟩ + p ∘ foldn (zero , succ) ≡⟨ commute₁ ⟩ + foldn (true , id) ≡⟨ sym commute₂ ⟩ + (true !) ∘ foldn (zero , succ) ≡⟨ identityʳ ⟩ + true ! ∎ + where + commute₁ = foldn-fusion zero succ p true id IS (extensionality (p ∘ succ) p IH) + commute₂ = foldn-fusion zero succ (true !) true id refl refl +``` + +## Lists + +```agda + data 𝕃 (A : Set) : Set where + nil : 𝕃 A + cons : (A × 𝕃 A) → 𝕃 A + + foldr : ∀ {A C : Set} → (C × (A × C → C)) → 𝕃 A → C + foldr (c , h) nil = c + foldr (c , h) (cons (x , xs)) = h (x , foldr (c , h) xs) + + foldr-id : ∀ {A : Set} → foldr (nil , cons) ≡ id {𝕃 A} + foldr-id {A} = extensionality (foldr (nil , cons)) id helper + where + helper : ∀ (x : 𝕃 A) → foldr (nil , cons) x ≡ id x + helper nil = refl + helper (cons (x , xs)) rewrite helper xs = refl + + foldr-fusion : ∀ {A B B' : Set} (c : B) (h : A × B → B) (k : B → B') (c' : B') (h' : A × B' → B') + → k c ≡ c' + → k ∘ h ≡ h' ∘ (id ×₁ k) + → k ∘ foldr (c , h) ≡ foldr (c' , h') + foldr-fusion {A} c h k c' h' kc kh = extensionality (k ∘ foldr (c , h)) (foldr (c' , h')) helper + where + helper : ∀ (x : 𝕃 A) → k (foldr (c , h) x) ≡ foldr (c' , h') x + helper nil = kc + helper (cons (x , xs)) rewrite ext-rev kh (x , foldr (c , h) xs) | helper xs = refl + + length : ∀ {A : Set} → 𝕃 A → ℕ + length {A} = foldr (zero , h) + where + h : A × ℕ → ℕ + h = succ ∘ outr + + isempty? : ∀ {A : Set} → 𝕃 A → 𝔹 + isempty? = foldr (true , (false !)) + + cat : ∀ {A : Set} → 𝕃 A × 𝕃 A → 𝕃 A + cat = uncurry (foldr (id , curry (cons ∘ ⟨ outl ∘ outl , ev ∘ (outr ×₁ id) ⟩))) + + sum : 𝕃 ℕ → ℕ + sum = foldr (0 , +) +``` + +**HOMEWORK 4** + +```agda + take : ∀ {A : Set} → ℕ → 𝕃 A → 𝕃 A + take zero = nil ! + take (succ n) = foldr (nil , (cons ∘ (id ×₁ take n))) +``` + +**HOMEWORK 5** + +We show that the `list` function is functorial: + +```agda + list : ∀ {A B : Set} → (A → B) → 𝕃 A → 𝕃 B + list f = foldr (nil , (cons ∘ (f ×₁ id))) + + list-id : ∀ {A : Set} → list id ≡ id {𝕃 A} + list-id = foldr-id + + list-homomorphism : ∀ {A B C : Set} (f : A → B) (g : B → C) → (list g) ∘ (list f) ≡ list (g ∘ f) + list-homomorphism {A} {B} {C} f g = foldr-fusion nil (cons ∘ (f ×₁ id)) (list g) nil (cons ∘ ((g ∘ f) ×₁ id)) refl refl +``` + +**HOMEWORK 6** + +Ackermann function: + +```agda + ack : ℕ × ℕ → ℕ + ack = uncurry (foldn (succ , h)) + where + -- https://arxiv.org/pdf/1602.05010.pdf + -- first look + h' : (ℕ → ℕ) → ℕ → ℕ + h' f = foldn (f 1 , f) + -- pointfree + h : (ℕ → ℕ) → ℕ → ℕ + h = curry (ev ∘ ((foldn ∘ ⟨ ev ∘ ⟨ id , 1 ! ⟩ , id ⟩) ×₁ id)) + + -- pointwise definition for comparison + ack' : ℕ → ℕ → ℕ + ack' 0 = succ + ack' (succ n) zero = ack' n 1 + ack' (succ n) (succ m) = ack' n (ack' (succ n) m) + + ack-test1 : ack (3 , 3) ≡ ack' 3 3 + ack-test1 = refl + ack-test2 : ack (0 , 3) ≡ ack' 0 3 + ack-test2 = refl + ack-test3 : ack (3 , 2) ≡ ack' 3 2 + ack-test3 = refl + ack-test4 : ack (2 , 2) ≡ ack' 2 2 + ack-test4 = refl +``` + +**HOMEWORK 7** + +Trees: + +```agda + data 𝕋 (A : Set) : Set where + leaf : A → 𝕋 A + bin : 𝕋 A × 𝕋 A → 𝕋 A + + foldt : ∀ {A C : Set} → ((A → C) × ((C × C) → C)) → 𝕋 A → C + foldt (c , h) (leaf a) = c a + foldt (c , h) (bin (s , t)) = h (foldt (c , h) s , foldt (c , h) t) + + front : ∀ {A : Set} → 𝕋 A → 𝕃 A + front = foldt ((cons ∘ ⟨ id , nil ! ⟩) , cat) + + foldt-id : ∀ {A : Set} → foldt (leaf , bin) ≡ id {𝕋 A} + foldt-id {A} = extensionality (foldt (leaf , bin)) id helper + where + helper : ∀ (x : 𝕋 A) → foldt (leaf , bin) x ≡ id x + helper (leaf x) = refl + helper (bin (x , y)) rewrite helper x | helper y = refl + + foldt-fusion : ∀ {A C C' : Set} (c : A → C) (h : C × C → C) (k : C → C') (c' : A → C') (h' : C' × C' → C') → k ∘ c ≡ c' → k ∘ h ≡ h' ∘ (k ×₁ k) → k ∘ foldt (c , h) ≡ foldt (c' , h') + foldt-fusion {A} {C} {C'} c h k c' h' kc kh = extensionality (k ∘ foldt (c , h)) (foldt (c' , h')) helper + where + helper : ∀ (x : 𝕋 A) → k (foldt (c , h) x) ≡ foldt (c' , h') x + helper (leaf x) = ext-rev kc x + helper (bin (s , t)) rewrite ext-rev kh (foldt (c , h) s , foldt (c , h) t) | helper s | helper t = refl + +``` + +**HOMEWORK 8** + +```agda + sumt : 𝕋 ℕ → ℕ + sumt = foldt (id , +) + + front-sum : sumt ≡ sum ∘ front + front-sum = sym (foldt-fusion (cons ∘ ⟨ id , nil ! ⟩) cat sum id + (extensionality _ _ triangle) square) + where + triangle : ∀ x → (sum ∘ (cons ∘ ⟨ id , nil ! ⟩)) x ≡ id x + triangle x rewrite +0 x = refl + square : sum ∘ cat ≡ + ∘ (sum ×₁ sum) + square = extensionality _ _ helper + where + helper : (x : 𝕃 ℕ × 𝕃 ℕ) → (sum ∘ cat) x ≡ (+ ∘ (sum ×₁ sum)) x + helper = {! !} +``` + +**HOMEWORK 9** + +```agda + data 𝕋' (A : Set) : Set where + leaf' : A → 𝕋' A + bin' : A × 𝕋' A × 𝕋' A → 𝕋' A + + foldb : ∀ {A C : Set} → ((A → C) × (A × C × C → C)) → 𝕋' A → C + foldb (c , h) (leaf' x) = c x + foldb (c , h) (bin' (x , (s , t))) = h (x , (foldb (c , h) s , foldb (c , h) t)) + + foldb-id : ∀ {A : Set} → foldb (leaf' , bin') ≡ id {𝕋' A} + foldb-id {A} = extensionality (foldb (leaf' , bin')) id helper + where + helper : ∀ (x : 𝕋' A) → foldb (leaf' , bin') x ≡ id x + helper (leaf' x) = refl + helper (bin' (x , (t , s))) rewrite helper t | helper s = refl + + foldb-fusion : ∀ {A C C' : Set} (c : A → C) (h : A × C × C → C) (k : C → C') (c' : A → C') (h' : A × C' × C' → C') → k ∘ c ≡ c' → k ∘ h ≡ h' ∘ (id ×₁ k ×₁ k) → k ∘ foldb (c , h) ≡ foldb (c' , h') + foldb-fusion {A} {C} {C'} c h k c' h' kc kh = extensionality _ _ helper + where + helper : ∀ (x : 𝕋' A) → (k ∘ foldb (c , h)) x ≡ foldb (c' , h') x + helper (leaf' x) = ext-rev kc x + helper (bin' (x , (s , t))) rewrite ext-rev kh (x , (foldb (c , h) s , foldb (c , h) t)) | helper s | helper t = refl + + size : ∀ {A : Set} → 𝕋' A → ℕ + size = foldb ((1 !) , (succ ∘ + ∘ outr)) + + flatten : ∀ {A : Set} → 𝕋' A → 𝕃 A + flatten = foldb ((cons ∘ ⟨ id , nil ! ⟩) , (cons ∘ (id ×₁ cat))) + + flatten-size : ∀ {A : Set} → length ∘ flatten ≡ size {A} + flatten-size {A} = foldb-fusion (cons ∘ ⟨ id , nil ! ⟩) (cons ∘ (id ×₁ cat)) length (1 !) (succ ∘ + ∘ outr) refl square + where + square : length ∘ (cons ∘ ((id ×₁ cat))) ≡ (succ ∘ + ∘ outr) ∘ (id ×₁ length ×₁ length) + square = {! !} +``` \ No newline at end of file diff --git a/agda/equality.agda b/agda/equality.agda new file mode 100644 index 0000000..d6b82c3 --- /dev/null +++ b/agda/equality.agda @@ -0,0 +1,35 @@ +module equality where + -- in this module we define propositional equality and some helper syntax. + + infix 4 _≡_ + data _≡_ {A : Set} (a : A) : A → Set where + instance refl : a ≡ a + {-# BUILTIN EQUALITY _≡_ #-} + + -- ≡ is a equivalence relation + sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x + sym refl = refl + + trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z + trans refl refl = refl + + cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y + cong f refl = refl + + -- Equational reasoning + infix 3 _∎ + infixr 2 _≡⟨⟩_ step-≡ + infix 1 begin_ + begin_ : ∀ {A : Set} {x y : A} → x ≡ y → x ≡ y + begin x = x + + _≡⟨⟩_ : ∀ {A : Set} (x y : A) → x ≡ y → x ≡ y + _ ≡⟨⟩ _ = λ x → x + + _∎ : ∀ {A : Set} (x : A) → x ≡ x + _ ∎ = refl + + step-≡ : ∀ {A : Set} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z + step-≡ _ y≡z x≡y = trans x≡y y≡z + + syntax step-≡ x eq1 eq2 = x ≡⟨ eq2 ⟩ eq1 \ No newline at end of file