From 6820113f1c57c12b6fe1d32ef1e0ec0235f5274e Mon Sep 17 00:00:00 2001 From: Carlo Angiuli Date: Fri, 8 Jun 2018 14:24:10 -0400 Subject: [PATCH] Update documentation; write tutorial. (#687) * Un-break the custom CSS. * Fix Pygments lexer for RedPRL. * Write tutorial, part one. * Write tutorial, part two. --- doc/src/conf.py | 2 +- doc/src/redprl.py | 19 +- doc/src/refine.rst | 2 + doc/src/static/red.css | 6 +- doc/src/tutorial.rst | 384 +++++++++++++++++------------------------ 5 files changed, 178 insertions(+), 235 deletions(-) diff --git a/doc/src/conf.py b/doc/src/conf.py index d448b2236..716ba8986 100644 --- a/doc/src/conf.py +++ b/doc/src/conf.py @@ -73,7 +73,7 @@ exclude_patterns = ['build', 'Thumbs.db', '.DS_Store'] # The name of the Pygments (syntax highlighting) style to use. -pygments_style = 'sphinx' +pygments_style = 'colorful' # If true, `todo` and `todoList` produce output, else they produce nothing. todo_include_todos = True diff --git a/doc/src/redprl.py b/doc/src/redprl.py index 8969da78e..f3ccdb700 100644 --- a/doc/src/redprl.py +++ b/doc/src/redprl.py @@ -30,6 +30,9 @@ class RedPRLLexer(RegexLexer): 'line', 'pushout', 'coeq', 'eq', 'fcom', 'V', 'universe', 'hcom', 'coe', 'subtype', 'universe'] + def joiner(arr): + return '|'.join(map(lambda str: '\\b' + str + '\\b', arr)) + # earlier rules take precedence tokens = { 'root': [ @@ -38,18 +41,20 @@ class RedPRLLexer(RegexLexer): (r'//.*?$', Comment.Singleline), (r'/\*', Comment.Multiline, 'comment'), - ('/[\w/]+|\\b'.join(types), Name.Builtin), - ('|\\b'.join(exprs), Name.Builtin), + (joiner(map(lambda str: str + '/[\w/]+', types)), Name.Builtin), + (joiner(exprs), Name.Builtin), + (joiner(types), Name.Builtin), (r'\$|\*|!|@|=(?!>)|\+|->|~>|<~', Name.Builtin), - ('|\\b'.join(tacs), Keyword), + (joiner(tacs), Keyword), (r';|`|=>|<=', Keyword), - ('|\\b'.join(cmds), Keyword.Declaration), + (joiner(cmds), Keyword.Declaration), - ('|\\b'.join(misc), Name.Builtin), + (joiner(misc), Name.Builtin), (r'\#[a-zA-Z0-9\'/-]*', Name.Variable), + (r'\%[a-zA-Z0-9\'/-]*', Name.Variable), (r'\(|\)|\[|\]|\.|:|,|\{|\}|_', Punctuation), (r'\b\d+', Number), @@ -58,12 +63,16 @@ class RedPRLLexer(RegexLexer): (r'^\|', Generic.Traceback), (r'>>', Name.Keyword), (r'<-', Name.Keyword), + (r'/=', Name.Keyword), + (r'<', Name.Keyword), (r'ext', Name.Keyword), (r'where', Name.Keyword), + (r'\|', Punctuation), (r'[A-Z][a-zA-Z0-9\'/-]*', Name.Function), (r'[a-z][a-zA-Z0-9\'/-]*', Name.Variable), (r'\?[a-zA-Z0-9\'/-]*', Name.Exception), + (r'-+$', Punctuation), ], 'comment': [ diff --git a/doc/src/refine.rst b/doc/src/refine.rst index 70ae59f3d..298b2edb3 100644 --- a/doc/src/refine.rst +++ b/doc/src/refine.rst @@ -10,6 +10,8 @@ Booleans H >> bool = bool in (U #l #k) +.. _bool/eq/tt: + :index:`bool/eq/tt` ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ :: diff --git a/doc/src/static/red.css b/doc/src/static/red.css index b812b0c1f..41ebcacb0 100644 --- a/doc/src/static/red.css +++ b/doc/src/static/red.css @@ -79,13 +79,13 @@ code { } div[class^='highlight'] pre { - font-size: 14px; + font-size: 14px !important; line-height: 1.5 !important; padding: 12px 20px; } div[class^='highlight'] { - border: none; + border: none !important; background: initial; } @@ -94,7 +94,7 @@ div[class^='highlight'] { font-weight: 700; } -pre .gt { +.highlight .gt { background-color: #f7bcbb; color: #f7bcbb; padding: 3px 0; diff --git a/doc/src/tutorial.rst b/doc/src/tutorial.rst index 9d98a8c22..7ceb98cdf 100644 --- a/doc/src/tutorial.rst +++ b/doc/src/tutorial.rst @@ -8,8 +8,15 @@ in the ``examples/`` subdirectory. .. _POPL 2018 tutorial: https://existentialtype.wordpress.com/2018/01/15/popl-2018-tutorial/ -.. todo:: - Write the tutorial. +|RedPRL| is a program logic for a functional programming language extended with +constructs for higher-dimensional reasoning. A proof in |RedPRL| is a tactic +script that constructs a program (or *extract*) and demonstrates that it +inhabits the specified type. + +Getting started +--------------- + +Let's start by defining the function that negates a boolean: :: @@ -20,25 +27,67 @@ in the ``examples/`` subdirectory. if b then `ff else `tt }. +The ``lam b =>`` tactic introduces a variable ``b : bool`` in the context, +``if then else`` performs a case split, and each branch is resolved by a boolean +literal (```ff`` and ```tt``). We can inspect the proof state at any point using +a *hole*. Replace ```ff`` with ``?the-tt-case``, and run |RedPRL| again: + +:: + + ?the-tt-case. + Goal #0. + b : bool + --------- + bool + +That is, the current subgoal has type ``bool``, and ``b : bool`` is in scope. +Replace ``?the-tt-case`` with ```ff`` once again, and follow this theorem by: + +:: + print Not. - // (not(not(b)) == b) because it holds for every closed boolean. +The ``print`` command displays the theorem statement and its extract. In this +case, we can prove ``Not`` with the extract directly: + +:: + + theorem NotDirect : + (-> bool bool) + by { + `(lam [b] (if [_] bool b ff tt)) + }. + +In general, we might not have a particular extract in mind, or establishing the +type of that extract may require non-trivial reasoning, so we typically choose +(or are forced) to use interactive tactics rather than specifying extracts. + +|RedPRL| has a notion of exact, extensional equality of programs, written ``=``. +For example, applying ``Not`` twice is equal to the identity function. +(Function application is written ``$``.) + +:: + theorem NotNot : (-> [b : bool] (= bool ($ Not ($ Not b)) b)) by { - lam b => - // The next four lines can be replaced by auto. - unfold Not; - if b - then (reduce at left; refine bool/eq/tt) - else (reduce at left; refine bool/eq/ff) + lam b => auto }. - print NotNot. +This instance of ``auto`` cases on ``b``, and in each case simplifies the +left-hand side and supplies a reflexive equality. (For example, the subgoal +``(= bool tt tt)`` is handled by the :ref:`refinement rule ` +``refine bool/eq/tt``.) + +Families of types respect equality of indices. For example, suppose we have a +boolean-indexed family of types ``family``. By virtue of the equation we just +proved, an element of the type ``($ family b)`` is also an element of the type +``($ family ($ Not ($ Not b)))``: + +:: - // Type families respect equality proofs. theorem RespectEquality : (-> [family : (-> [b : bool] (U 0))] @@ -47,109 +96,110 @@ in the ``examples/`` subdirectory. ($ family ($ Not ($ Not b)))) by { lam family b pf => - rewrite ($ NotNot b); - [ with b' => `($ family b') + rewrite ($ NotNot b); // equation to rewrite along + [ with b' => `($ family b') // what to rewrite (i.e., b') , use pf ]; auto }. +Here, ``(U 0)`` is a universe (the "type of small types"). The ``rewrite`` +tactic rewrites the argument to ``family`` along the equality +``(= bool ($ Not ($ Not b)) b)`` given by ``($ NotNot b)``, taking +``pf : ($ family b)`` to a proof of ``($ family ($ Not ($ Not b))))``. - // print does not mention the equality proof! - // (No need to ``transport'' at runtime.) - print RespectEquality. +Surprisingly, the extract is just a constant function: ``(lam [x0 x1 x2] x2)``! +The reason is that at runtime, for any particular ``b``, the types +``($ family b)`` and ``($ family ($ Not ($ Not b))))`` will be exactly the same, +so there's no need for a coercion. - // In fact, all proofs of (not(not(b)) == b) are equal. - theorem EqualityIrrelevant : - (= - (-> [b : bool] (= bool ($ Not ($ Not b)) b)) - NotNot - (lam [b] ax)) - by { - auto - }. +Cubical reasoning +----------------- - print EqualityIrrelevant. +|RedPRL| also includes a notion of *path* similar to the *identity type* of +homotopy type theory. Like equations, paths are respected by the constructs of +type theory. However, while respect for equations is silent, respect for paths +affects the runtime behavior of programs. - // Paths (cf equalities), like those arising from - // equivalences via univalence, do induce computation. - theorem FunToPair : +In |RedPRL|, paths are mediated by *dimension variables* abstractly representing +how the path varies over an interval. Nested paths of paths are indexed by +multiple dimension variables, and therefore trace out squares, cubes, +hypercubes, etc., hence the name *cubical type theory*. A reflexive path depends +degenerately on a dimension variable: + +:: + + theorem Refl : (-> - [ty : (U 0 kan)] - (-> bool ty) - (* ty ty)) + [ty : (U 0)] + [a : ty] + (path [_] ty a a)) by { - lam ty fun => - {`($ fun tt), `($ fun ff)} + lam ty a => + abs _ => `a }. - // {{{ Univalence +The ``abs _ =>`` tactic is analogous to ``lam a =>`` but introduces dimension +variables rather than ordinary variables. + +Paths form a groupoid: they can be composed and reversed; composition is +associative (up to a path) and has ``Refl`` as unit (up to a path); etc. These +operations all follow from a single operation, *homogeneous Kan composition* +(``hcom``), which produces the fourth side of a square given the other three, or +the sixth side of a cube given the other five, etc. The details of this +operation are beyond the scope of this tutorial, but the following illustration +demonstrates how to compose paths ``p`` and ``q`` using ``hcom``: + +.. highlight:: none + +:: + + --- x p + | --------- + y | | + a | | q + | | + a.........c - define HasAllPathsTo (#C,#c) = (-> [c' : #C] (path [_] #C c' #c)). - define IsContr (#C) = (* [c : #C] (HasAllPathsTo #C c)). - define Fiber (#A,#B,#f,#b) = (* [a : #A] (path [_] #B ($ #f a) #b)). - define IsEquiv (#A,#B,#f) = (-> [b : #B] (IsContr (Fiber #A #B #f b))). - define Equiv (#A,#B) = (* [f : (-> #A #B)] (IsEquiv #A #B f)). +That is, if ``p`` goes from ``a`` to ``b``, and ``q`` goes from ``b`` to ``c``, +then we can form a square with ``p`` on top, ``q`` on the right, and the +constantly-``a`` path on the left; the bottom must therefore be a path from +``a`` to ``c``. The concrete notation is given below (where ``(@ p x)`` applies +the path ``p`` to the dimension variable ``x`` as argument). - theorem WeakConnection(#l:lvl) : +.. highlight:: redprl + +:: + + theorem PathConcat : (-> - [ty : (U #l hcom)] - [a b : ty] + [ty : (U 0 kan)] + [a b c : ty] [p : (path [_] ty a b)] - (path [i] (path [_] ty (@ p i) b) p (abs [_] b))) + [q : (path [_] ty b c)] + (path [_] ty a c)) by { - (lam ty a b p => - abs i j => - `(hcom 1~>0 ty b - [i=0 [k] (hcom 0~>j ty (@ p k) [k=0 [w] (@ p w)] [k=1 [_] b])] - [i=1 [k] (hcom 0~>1 ty (@ p k) [k=0 [w] (@ p w)] [k=1 [_] b])] - [j=0 [k] (hcom 0~>i ty (@ p k) [k=0 [w] (@ p w)] [k=1 [_] b])] - [j=1 [k] (hcom 0~>1 ty (@ p k) [k=0 [w] (@ p w)] [k=1 [_] b])])) - }. - - tactic GetEndpoints(#p, #t:[exp,exp].tac) = { - query pty <- #p; - match pty { - [ty l r | #jdg{(path [_] %ty %l %r)} => - claim p/0 : (@ #p 0) = %l in %ty by {auto}; - claim p/1 : (@ #p 1) = %r in %ty by {auto}; - (#t p/0 p/1) - ] - } + lam ty a b c p q => + abs x => + `(hcom 0~>1 ty (@ p x) [x=0 [_] a] [x=1 [y] (@ q y)]) }. +Another source of paths is Voevodsky's *univalence principle*, stating that any +equivalence (isomorphism-up-to-paths) between types gives rise to a path between +those types. We apply this principle to the isomorphism between ``(-> bool ty)`` +and ``(* ty ty)`` sending a function to the pair (``{ , }``) of its output on +``tt`` and ``ff``. - print WeakConnection. +:: - theorem FunToPairIsEquiv : + theorem FunToPair : (-> [ty : (U 0 kan)] - (IsEquiv (-> bool ty) (* ty ty) ($ FunToPair ty))) + (-> bool ty) + (* ty ty)) by { - lam ty pair => - { { lam b => if b then `(!proj1 pair) else `(!proj2 pair) - , abs _ => `pair } - , unfold Fiber; - lam {fun,p} => - (GetEndpoints p [p/0 p/1] #tac{ - (abs x => - {lam b => if b then `(!proj1 (@ p x)) else `(!proj2 (@ p x)), - abs y => - `(@ ($ (WeakConnection #lvl{0}) (* ty ty) ($ FunToPair ty fun) pair p) x y) - }); - [ unfold FunToPair in p/0; reduce in p/0 at right; - inversion; with q3 q2 q1 q0 => - reduce at right in q2; - reduce at right in q3; - auto; with b => - elim b; reduce at right; symmetry; assumption - , unfold FunToPair in p/1; reduce in p/1 at right; - inversion; with q3 q2 q1 q0 => elim pair; - reduce at right in q0; reduce at right in q1; - auto; assumption - ] - }) - } + lam ty fun => + {`($ fun tt), `($ fun ff)} }. theorem PathFunToPair : @@ -158,15 +208,15 @@ in the ``examples/`` subdirectory. (path [_] (U 0 kan) (-> bool ty) (* ty ty))) by { lam ty => abs x => - `(V x (-> bool ty) (* ty ty) - (tuple [proj1 ($ FunToPair ty)] [proj2 ($ FunToPairIsEquiv ty)])) + // see tutorial.prl for omitted proofs }. - // }}} +Respect for paths follows from an explicit *coercion* operation (``coe``). We +can coerce along the path ``($ PathFunToPair ty)`` from left to right +(``0~>1``), taking an element of ``(bool -> ty)`` to ``(ty * ty)``. - print PathFunToPair. +:: - // We can coerce elements of (bool -> ty) to (ty * ty). theorem RespectPaths : (-> [ty : (U 0 kan)] @@ -177,9 +227,15 @@ in the ``examples/`` subdirectory. `(coe 0~>1 [x] (@ ($ PathFunToPair ty) x) fun) }. - print RespectPaths. +Unlike ``rewrite``, uses of ``coe`` are reflected in the extract, because they +affect computation. Indeed, an element of ``(bool -> ty)`` is not literally an +element of ``(ty * ty)``, and there is more than one isomorphism between these +types! A major benefit of cubical type theory over homotopy type theory is that +coercions actually *compute*: if we apply ``RespectPaths`` to the identity +function, we get exactly the pair ``{`tt,`ff}``. + +:: - // When coercing, the choice of PathFunToPair matters! theorem ComputeCoercion : (= (* bool bool) @@ -189,102 +245,14 @@ in the ``examples/`` subdirectory. auto }. +**Experts:** though paths in |RedPRL| are defined by dimension variables rather +than the ``refl`` and ``J`` operators of homotopy type theory, ``J`` is +definable using coercion and homogeneous Kan composition (but will not compute +to ``d`` on ``refl``). - // --------------------------------------------------------- - // Part Two - // --------------------------------------------------------- - - // A constant path does not depend on its dimension. - theorem Refl : - (-> - [ty : (U 0)] - [a : ty] - (path [_] ty a a)) - by { - lam ty a => - abs _ => `a - }. - - // The path structure of each type is defined in terms of - // its constituent types. - theorem FunPath : - (-> - [a b : (U 0)] - [f g : (-> a b)] - (path [_] (-> a b) f g) - [arg : a] - (path [_] b ($ f arg) ($ g arg))) - by { - lam a b f g p => - lam arg => abs x => - `($ (@ p x) arg) - }. - - - print FunPath. - - theorem PathInv : - (-> - [ty : (U 0 kan)] - [a b : ty] - [p : (path [_] ty a b)] - (path [_] ty b a)) - by { - // a -- x - // ------- | - // | | y - // p | | a - // | | - // b .... a - - lam ty a b p => - abs x => - `(hcom 0~>1 ty a [x=0 [y] (@ p y)] [x=1 [_] a]) - }. - - theorem PathConcat : - (-> - [ty : (U 0 kan)] - [a b c : ty] - [p : (path [_] ty a b)] - [q : (path [_] ty b c)] - (path [_] ty a c)) - by { - // p -- x - // ------- | - // | | y - // a | | q - // | | - // a .... c - - lam ty a b c p q => - abs x => - `(hcom 0~>1 ty (@ p x) [x=0 [_] a] [x=1 [y] (@ q y)]) - }. - - theorem InvRefl : - (-> - [ty : (U 0 kan)] - [a : ty] - (path - [_] (path [_] ty a a) - ($ PathInv ty a a (abs [_] a)) - (abs [_] a))) - by { - // See diagram! - lam ty a => - abs x y => - `(hcom 0~>1 ty a - [x=0 [z] (hcom 0~>z ty a [y=0 [_] a] [y=1 [_] a])] - [x=1 [_] a] - [y=0 [_] a] - [y=1 [_] a]) - }. +:: - // Although the path type is not defined by refl and J - // (as in HoTT), we can still define J using hcom + coe. - // The #l is an example of a parametrized definition. - theorem J(#l:lvl) : + theorem J(#l:lvl) : // parametrized over any universe level #l (-> [ty : (U #l kan)] [a : ty] @@ -301,39 +269,3 @@ in the ``examples/`` subdirectory. (abs [j] (hcom 0~>j ty a [i=0 [_] a] [i=1 [j] (@ p j)]))) d) }. - theorem JInv : - (-> - [ty : (U 0 kan)] - [a b : ty] - [p : (path [_] ty a b)] - (path [_] ty b a)) - by { - lam ty a b p => - exact - ($ (J #lvl{0}) - ty - a - (lam [b _] (path [_] ty b a)) - (abs [_] a) - b - p) - ; auto - //; unfold J; reduce at left right; ? - }. - - print JInv. - - // Computing winding numbers in the circle. - - // Bonus material: - - theorem Shannon : - (-> - [ty : (-> bool (U 0))] - [elt : (-> [b : bool] ($ ty b))] - [b : bool] - (= ($ ty b) ($ elt b) (if [b] ($ ty b) b ($ elt tt) ($ elt ff)))) - by { - lam ty elt b => - elim b; auto - }.