index.holbert

[{"contents":[0,"Holbert: Reading, Writing and Proving in the Browser"],"tag":"Heading"},{"contents":"*Liam O'Connor*^contact:~l.oconnor~ at ~ed.ac.uk~\nORCID: @0000-0003-2765-4269|https://orcid.org/0000-0003-2765-4269@^ and *Rayhana Amjad*^contact:~rayhana.yasmin.h~ at ~gmail.com~\nORCID: @0000-0002-3086-1720|https://orcid.org/0000-0002-3086-1720@^\nUniversity of Edinburgh, Scotland\n\n/Human Aspects of Types and Reasoning Assistants (HATRA), 2022/","tag":"Paragraph"},{"contents":[3,"Abstract"],"tag":"Heading"},{"contents":"This paper presents Holbert a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.\n","tag":"Paragraph"},{"contents":[1,"Introduction"],"tag":"Heading"},{"contents":"Programming language theory is rife with valuable ideas that can be applied in the wider world of software, but it can also be challenging to teach; it requires a familiarity with mathematical proofs that students of computer science do not always possess. Teaching the ability to write proofs requires that students practice the skill with oversight to point out their errors and help them achieve correct proofs. The amount of feedback and interaction between teachers and students that this requires is not always practical, given large class sizes. To this end, Pierce^[1]:Benjamin C. Pierce. /Lambda: The Ultimate TA/. ICFP '09. @10.1145/1596550.1596552|https://doi.org/10.1145/1596550.1596552@^ advocates the use of proof assistants to more effectively communicate the foundations of programming language theory, as a proof assistant can similarly point out errors and verify the correctness of the proofs that a student writes. Early results from evaluation studies^[2]:Maria Knobelsdorf, Christiane Frede, Sebastian Böhne, Christoph Kreitz. /Theorem Provers as a Learning Tool in Theory of Computation/. ICER '17. @10.1145/3105726.3106184|https://doi.org/10.1145/3105726.3106184@^ show that students can profit strongly from the use of proof assistants in the classroom, compared to pen and paper proofs.","tag":"Paragraph"},{"contents":"Pierce^[1]:Benjamin C. Pierce. /Lambda: The Ultimate TA/. ICFP '09. @10.1145/1596550.1596552|https://doi.org/10.1145/1596550.1596552@^ uses the venerable proof assistant @Coq|https://coq.inria.fr/@ in their classroom, based on the accompanying textbook, Software Foundations^[3]:Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hrițcu, Vilhelm Sjöberg and Brent Yorgey. /Software Foundations/. @http://www.cis.upenn.edu/~bcpierce/sf@^. Greenberg and Osborn^[4]:Michael Greenberg, Joseph C. Osborn. /Teaching Discrete Mathematics to Early Undergraduates with Software Foundations/. CoqPL 2019. @https://cs.pomona.edu/~michael/papers/coqpl2019.pdf@^  also use this book as the basis for a tool-assisted discrete mathematics course.  Inspired by Pierce's example, Wadler et al.^[5]:Wadler, Philip, Wen Kokke, and Jeremy G. Siek. /Programming Language Foundations in Agda/. @https://plfa.inf.ed.ac.uk/22.08/@^ and Nipkow and Klein^[6]:Tobias Nipkow and Gerwin Klein. /Concrete Semantics/. Springer. @http://concrete-semantics.org/@^ have also written similar textbooks for their favourite proof assistants. Narboux^[7]:Julien Narboux, /Towards the use of a proof assistant to teach mathematics./ ICTMT '05. @https://hal.archives-ouvertes.fr/inria-00495952@^ also uses Coq, but to teach mathematics, not programming language theory. Buzzard^[8]:Kevin Buzzard, /The Xena Project/, @https://xenaproject.wordpress.com/@^ does something similar with Lean. \n","tag":"Paragraph"},{"contents":"All of these proof assistants, however, are not primarily designed for a pedagogical purpose. They can be difficult software to use, with installing and executing the software proving an initial obstacle, particularly with large groups of students. The interfaces of these proof assistants typically involve unfamiliar syntax, notation and interaction idioms, and do not give simple feedback when a student provides an incorrect proof^[4,:Michael Greenberg, Joseph C. Osborn. /Teaching Discrete Mathematics to Early Undergraduates with Software Foundations/. CoqPL 2019. @https://cs.pomona.edu/~michael/papers/coqpl2019.pdf@^ ^9,:Carl Eastlund, Dale Vaillancourt and Matthias Felleisen. /ACL2 for freshmen: First experiences/. ACL2 Workshop 2007. @Available at NEU|https://www2.ccs.neu.edu/racket/pubs/acl207-evf.pdf|@^ ^10]:Evmorfia Bartzia, Antoine Meyer and Julien Narboux. /Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis/. 2022. @hal-03648357|https://hal.archives-ouvertes.fr/hal-03648357@^. Using such a proof assistant in a course runs the risk of shifting the emphasis away from the primary theoretical content of the course, and towards learning how to use the proof assistant. The fact that many people work through the above-mentioned textbooks in order to learn how to use a new proof assistant, rather than to learn the associated theory, is evidence of this phenomenon. Furthermore, the text-based interface of these provers means that students must copy example proofs from the textbook into their editors to examine a proof in their proof assistant, necessitating constant mental context-switching that adds unnecessary cognitive overhead.","tag":"Paragraph"},{"contents":"Holbert is a new proof assistant that is designed to address these problems. It runs in the browser, so no installation is required. Rather than a text-based interface with complex syntax, Holbert presents rules, proofs and terms graphically, much as one would write them in a computer science paper. The interface is designed to fade into the background, and not require significant training to use. We provide several examples of its use in the next section.","tag":"Paragraph"},{"contents":"Crucially, Holbert is also an /online textbook platform/. With Holbert, students do not have to switch between using their proof assistant and reading an accompanying textbook, copying code into their editors. Instead, students can simply interact with proof exercises directly /in the textbook itself/. Online textbooks have the potential to be an exciting, interactive learning platform (and have already shown promising results in trials^[11]:Alex D. Edgcomb, Frank Vahid, Roman Lysecky, Andre Knoesen, Rajeevan Amirtharajah, Mary Lou Dorf. /Student performance improvement using interactive textbooks: A three-university cross-semester analysis/. 2015 ASEE Annual Conference & Exposition. @10.18260/p.24760|https://doi.org/10.18260/p.24760^), but for the teaching of mathematics or theoretical computer science, this potential has not yet been fully realised. With Holbert, we aim to reach this potential, and unlock new and exciting ways to teach our favourite mathematical topics.","tag":"Paragraph"},{"contents":[1,"A Tour of Holbert"],"tag":"Heading"},{"contents":"The foundation of Holbert is an /untyped/ variant of the original /higher order logic/ of Church^[12]:Alonzo Church. /A Formulation of the Simple Theory of Types/. The Journal of Symbolic Logic, 1940. @10.2307/2266170|https://doi.org/10.2307/2266170@^, which uses $lambda$-calculus to represent logical terms. Higher order logic is also the basis of proof assistants such as @Isabelle/HOL|https://isabelle.in.tum.de/@^[13]:Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel. /Isabelle////HOL: A Proof Assistant for Higher Order Logic/. Springer, 2002. @10.1007/3-540-45949-9|https://doi.org/10.1007/3-540-45949-9@^, but these proof assistants use typed formalisms to escape the paradoxes that are present in the untyped theory^1:Consider that the untyped $lambda$-term $(Y not)$, where $Y$ is a fixed-point combinator, $beta$-reduces to its own negation.^. The main reason for the elision of a type system is pedagogical. Holbert is intended as a vehicle for teaching programming language theory, including type theory, and requiring type theory knowledge /a priori/ to effectively use Holbert would be an irritating circularity. The lack of a type system also generally reduces the number of concepts required to learn Holbert, and enables our definitions to more closely resemble the untyped, informal definitions used in conventional computer science notation. Of course, this does mean that Holbert is technically unsound, but the theorems proven in Holbert are not intended for, say, verifying an operating system kernel^[14]:Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch. /seL4: Formal Verification of an OS Kernel./ SOSP '09. @10.1145/1629575.1629596|https://doi.org/10.1145/1629575.1629596@^—there is no requirement that Holbert theorems be trustworthy. To paraphrase the popular phrase, /\"Doctor, I can prove/ $bot$ /when I do this!\"/—then don't do that!","tag":"Paragraph"},{"contents":[2,"Defining Rules"],"tag":"Heading"},{"contents":"Logical statements, such as rules, theorems and axioms, are represented in Holbert using the format of natural deduction^[15]:Gerhard Gentzen. /Untersuchungen über das logische Schließen./ Mathematische Zeitschrift, 1935. @10.1007/BF01201353|https://doi.org/10.1007/BF01201353@^ inference rules, specifically /hereditary Harrop formulae/^[16]:Ronald Harrop, /On disjunctions and existential statements in intuitionistic systems of logic/. Mathematische Annalen, 1956. @10.1007/BF01360048|https://doi.org/10.1007/BF01360048@^. A hereditary Harrop formula is of the format $.rule:A*.H*|-C$, stating that for all substitutions of the metavariables $A*:A*$, the conclusion $C$ holds if the premises $H*$, which are themselves hereditary Harrop formulae, hold. Here $overlines*$ represent a sequence of zero or more. This structure allows for all of the usual natural deduction rules of intuitionistic propositional logic to be encoded in a natural way.","tag":"Paragraph"},{"contents":[[10,"_/\\_","LeftAssoc"],[5,"_\\/_","LeftAssoc"],[8,"_->_","RightAssoc"]],"tag":"SyntaxDecl"},{"contents":["Axiom",[["/\\ I",[["A","B"],[[[],[],{"contents":1,"tag":"LocalVar"}],[[],[],{"contents":0,"tag":"LocalVar"}]],{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["/\\ E1",[["A","B"],[[[],[],{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],null],["/\\ E2",[["A","B"],[[[],[],{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":0,"tag":"LocalVar"}],null],["-> I",[["A","B"],[[[],[[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}]],{"contents":[{"contents":[{"contents":["_->_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["-> E",[["A","B"],[[[],[],{"contents":[{"contents":[{"contents":["_->_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}],null],["\\/ I1",[["A","B"],[[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":[{"contents":[{"contents":["_\\/_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["\\/ I2",[["A","B"],[[[],[],{"contents":0,"tag":"LocalVar"}]],{"contents":[{"contents":[{"contents":["_\\/_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["\\/ E",[["A","B","C"],[[[],[],{"contents":[{"contents":[{"contents":["_\\/_",false],"tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[[[],[],{"contents":2,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}],[[],[[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}],null],["not I",[["P"],[[["X"],[[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}]],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["not E",[["P","X"],[[[],[],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}],null]],[]],"tag":"Rule"},{"contents":"By default, Holbert renders rules in the /hybrid/ format, where a vinculum is used for entailment on the top level, but the entailment sign (@entailment@) is used for hypothetical derivations. Holbert also supports /linear/ style, where rules are always rendered horizontally, and /vertical/ style, which is exactly Gentzen's original notation, using vincula for top-level entailments and a vertical layout with dots for hypothetical derivations.","tag":"Paragraph"},{"contents":"Any term in a rule definition, such as those above, can be edited in Holbert simply by clicking on it. Mix-fix operators such as $_/\\_$ have their precedence and associativity declared in *Notation* blocks (see above). This precedence and associativity only affects the editable text representation of the operator, and not its appearance in the rendered rule. If no *Notation* declaration is provided, infix operators can still be used, but their editable text representation will be in prefix format, so, for example, the conclusion of the rule $.thm:/\\ I$ would be written as ~_/\\_ A B~. ","tag":"Paragraph"},{"contents":["Theorem",[["/\\ comm",[["A","B"],[],{"contents":[{"contents":[{"contents":["_->_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[null,["A","B"],[],{"contents":[{"contents":[{"contents":["_->_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":"-> I","tag":"Defn"},[[null,[],[[[],[],{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":"/\\ I","tag":"Defn"},[[null,[],[],{"contents":0,"tag":"LocalVar"},[{"contents":"/\\ E2","tag":"Defn"},[[null,[],[],{"contents":[{"contents":[{"contents":["_/\\_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":0,"tag":"Local"},[]]]]]],[null,[],[],{"contents":1,"tag":"LocalVar"},null]]]]]]],8]]],[]],"tag":"Rule"},{"contents":"If an applicable rule is clicked, the rule is applied to the current goal as an introduction rule in the \"backwards reasoning\" commonly used in natural deduction. By default, only introduction rules are displayed, as all elimination rules would be applicable in this sense to all goals. While Holbert has special features for elimination rules, outlined in their own section later, elimination rules may also be applied as introduction rules by toggling a checkbox in the goal display, to show rules that do not fit the introduction rule format.","tag":"Paragraph"},{"contents":"When applying a rule $.rule:A*.H*|-C$ to a goal by backwards reasoning, we first replace all metavariables $A*:A*$ in the rule with fresh, global /unification variables/ (also called /schematic variables/). Then, we attempt to find a substitution to unification variables that unifies the goal with the conclusion $C$. If such a substitution can be found, new subgoals are added for each premise $H*$ and the substitution is applied to all unification variables occurring in the proof.","tag":"Paragraph"},{"contents":[2,"Higher-Order Unification"],"tag":"Heading"},{"contents":"Because our logic terms are $lambda$-terms, the first order unification algorithm of Robinson^[17]:J.A. Robinson. /A Machine-Oriented Logic Based on the Resolution Principle/. Journal of the ACM, 1965. @10.1145/321250.321253|https://doi.org/10.1145/321250.321253@^ is insufficient. Worse, the problem of unification modulo $alpha$$beta$$eta$-equivalence is, in general, undecidable. Huet^[18]:G.P. Huet /A unification algorithm for typed /$lambda$/-calculus/. Theoretical Computer Science, 1975. @10.1016/0304-3975(75)90011-0|https://doi.org/10.1016/0304-3975(75)90011-0@^ provides a semi-decision procedure, but this remains an unwieldy solution. Instead, and similarly to many other proof assistants, Holbert instead makes use of the /pattern unification/ technique of Miller^[19]:Dale Miller. /A Logic Programming Language With Lambda-Abstraction, Function Variables, and Simple Unification/. Journal of Logic and Computation, 1996. @10.1093/logcom/1.4.497|https://doi.org/10.1093/logcom/1.4.497@^, specifically derived from the implementation of Nipkow^[20]:Tobias Nipkow. /Functional unification of higher-order patterns/. LICS '93. @10.1109/LICS.1993.287599|https://doi.org/10.1109/LICS.1993.287599@ ^. This technique gives most general unifiers for terms that fall within the /pattern subset/, that is, terms where unification variables may only be applied to a list of distinct object variables. This restriction is not too onerous for the application of introduction rules, but some elimination and induction rules require some workarounds, described in later sections.","tag":"Paragraph"},{"contents":"Because unification variables are (proof-)global in scope, any substitution for a unification variable cannot directly mention the bound metavariables in scope for the goal. Thus, if we have a goal to prove, say, $.rule:A.A|- _/\\_ A A$ (for all $A:A$), and attempt to apply the rule $.thm:/\\ I$, instantiating the rule $.thm:/\\ I$ with naked unification variables would not work, because the conclusion $?1 /\\ ?2$ would not be unifiable with $A: _/\\_ A A$, as the assignments to the unification variables $?1$ and $?2$ cannot contain the bound metavariable $A: A$.  To address this problem, we instead /apply all bound variables in scope for the goal/ to the unification variables when we instantiate the rule. In our example, this means that we must now unify $A: _/\\_ A A$ with $A: _/\\_ (?1 A) (?2 A)$, which can easily be solved by assigning the identity function to both unification variables.","tag":"Paragraph"},{"contents":[2,"Higher-Order Abstract Syntax"],"tag":"Heading"},{"contents":"We can make use of Holbert's support for $lambda$-abstractions to write rules for quantifiers using $lambda$-abstraction to handle variable binding. To reduce notational clutter, $lambda$-abstractions in Holbert are written without the $lambda$, so the identity function would just be written as ~(x. x)~. ","tag":"Paragraph"},{"contents":["Axiom",[["all I",[["P"],[[["x"],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["all",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],null],["all E",[["P","x"],[[[],[],{"contents":[{"contents":["all",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}]],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["exists I",[["P","x"],[[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],null],["exists E",[["P","Q"],[[[],[],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],[["x"],[[[],[],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}],null]],[]],"tag":"Rule"},{"contents":"This technique of /higher order abstract syntax/ re-uses the existing binding mechanisms in Holbert to provide very natural looking rules for logical quantifiers. The same technique can also be used to represent variables and binding in programming language syntax, enabling programming languages to be formalised without the pedagogical overhead induced by term representations with name strings and substitutions, or de Bruijn^[21]:N.G. de Bruijn. /Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem/. Indagationes Mathematicae, 1972. @10.1016/1385-7258(72)90034-0|https://doi.org/10.1016/1385-7258(72)90034-0@^ indices.","tag":"Paragraph"},{"contents":[2,"Elimination Rules"],"tag":"Heading"},{"contents":"The elimination rule $.thm:all E$, presented in the previous section, is somewhat problematic as, after instantiation, its conclusion consists of a unification variable (from $P: P$) applied to another unification variable (from $x: x$), which is outside the pattern subset. In practice, if we were to apply $.thm:all E$ anyway, using backwards reasoning as with an introduction rule, to any goal $G$, our pattern unification would instantiate $P:P$ to a function that /ignores/ its argument and simply returns $G$, meaning that $x:x$ and the quantified variable $a: a$ are completely ignored. This is obviously not desirable. ","tag":"Paragraph"},{"contents":"But, applying elimination rules as introduction rules is, in any case, undesirable: While Gentzen's original presentation of natural deduction uses elimination rules in this way, this presents several usability problems, in addition to the aforementioned unification issue. Chiefly, as mentioned previously, the conclusion of any elimination rule can be unified with /any/ goal. Thus, /all/ elimination rules are applicable, in the sense of backwards reasoning, to a given goal, which presents an unwieldy list of candidate rules to the user. ","tag":"Paragraph"},{"contents":"In the process of constructing a proof, we think of applying elimination rules as /forward reasoning/, not backwards. Almost always, an elimination rule is thought to be applied to an assumption in the current context, /not/ to the current goal. Thus, Holbert features special features for applying elimination rules. Instead of clicking a rule to apply backwards to the current goal, the user clicks an /assumption/ on which to apply an elimination rule, and from there applicable elimination rules are displayed and may be applied to the goal. ","tag":"Paragraph"},{"contents":"Specifically, when applying an elimination rule $.rule:A*. P0, H* |- C$ to an assumption $S$ for a goal $G$, we once again replace metavariables $A*:A*$ in the rule with fresh, global unification variables (with all bound variables in scope for the goal applied). Then, rather than unify $C$ with our goal $G$, we first try to unify the first premise of the rule $P0$ with the assumption $S$, and only after this unification and substitution do we attempt to unify the conclusion of the rule with our goal. Note that, in the case of $.thm: all E$, this will avoid the non-pattern cases encountered previously. The first (and only) premise of the rule, $P: all (a. P a)$, only contains one unification variable after instantiation. Thus the first unification will, falling within the pattern subset, find the correct assignment to instantiate $P: P$, thus eliminating the non-pattern case previously encountered when unifying $C$ with $G$.","tag":"Paragraph"},{"contents":"When an elimination rule is applied in this way, the first subgoal from the applied rule is omitted in the resulting tree, as it is trivially discharged by the assumption. Instead, the numeric name of the assumption is superscripted to the name of the applied rule. As an example, here we prove one direction of the de Morgan identity for quantifiers:","tag":"Paragraph"},{"contents":["Theorem",[["not all exists",[["P"],[[[],[],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["x",{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}]],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":["all",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],"tag":"Ap"}],[[null,["P"],[[[],[],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["x",{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}]],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":["all",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":"not I","tag":"Defn"},[[null,["F"],[[[],[],{"contents":[{"contents":["all",false],"tag":"Const"},{"contents":["a",{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}]],{"contents":0,"tag":"LocalVar"},[{"contents":[{"contents":"exists E","tag":"Defn"},{"contents":0,"tag":"Local"}],"tag":"Elim"},[[null,["x"],[[[],[],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"},[{"contents":[{"contents":"not E","tag":"Defn"},{"contents":2,"tag":"Local"}],"tag":"Elim"},[[null,[],[],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":[{"contents":"all E","tag":"Defn"},{"contents":1,"tag":"Local"}],"tag":"Elim"},[]]]]]]]]]]]],7]]],[]],"tag":"Rule"},{"contents":"As a convenience feature, Holbert also includes support for inductive judgements. The user specifies only the introduction rules, and an induction principle and cases rule for inversion are synthesised automatically. To save space, we will simply define the natural numbers here, but these definitions may be significantly more complex. For example, Holbert can synthesise principles for simultaneous induction given mutually inductive introduction rules.","tag":"Paragraph"},{"contents":[2,"Induction"],"tag":"Heading"},{"contents":[[0,"_nat","NonAssoc"],[0,"_=_","NonAssoc"]],"tag":"SyntaxDecl"},{"contents":["Inductive",[["zero",[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],null],["suc",[["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],null]],[[{"contents":["_nat",1],"tag":"Cases"},[["§P","§0"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],[["n"],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":2,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}]],[{"contents":["_nat",1],"tag":"Induction"},[["§P0","§0"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],[["n"],[[[],[],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"Both of these derived rules can be applied as an elimination rule. The induction rule, however, exposes another scenario where our unification falls outside the pattern subset, and workarounds are required. Consider the case where we must prove some goal $k: G k$ for all $k: k$, with the assumption that $k: _nat k$. We instantiate the rule with fresh unification variables, replacing $P:P$ with ($k:(?0 k)$) and $x: x$ with ($k: (?1 k)$). Then we unify the first premise of our instantiated rule $k: _nat (?1 k)$ with the assumption $k: _nat k$, which resolves $?1$ to the identity function. We must now unify our goal $k: G k$ with the conclusion of our rule, which is now $k:__ (?0 k) k$. This falls outside the pattern subset, as $k: k$ occurs twice in the arguments to a unification variable. (Our unification algorithm once again picks the wrong solution here, choosing the first argument rather than the second.) ","tag":"Paragraph"},{"contents":"To avoid this problem, we adjust our strategy for applying elimination rules slightly. Instead of instantiating all variables in the rule at once, we instantiate variables in two phases. Firstly, we instantiate all those variables that occur in the first premise of the rule. These are instantiated with fresh unification variables that are applied to all bound metavariables in the scope of the goal, as before. Then we unify the first premise of the instantiated rule with our assumption. After applying the resulting substitution to the rule, we instantiate the remaining variables in the rule with fresh unification variables, but now they are only applied to those bound variables in the scope of the goal which do not already occur in the substituted rule. Then we unify the goal and the conclusion as before. This avoids the problematic term $k:__ (?0 k) k$ we saw earlier, because $k: k$ will only occur once in the second unification.","tag":"Paragraph"},{"contents":[2,"Prose-style Proofs"],"tag":"Heading"},{"contents":"While induction and proofs by cases can be presented as a natural deduction tree, this is not typically how such proofs are presented. The tree quickly becomes unwieldy and wide. Instead, Holbert allows proofs to be presented in /prose-style/, which tends to grow vertically rather than horizontally, and allows the user to write expository text for each case. As an example, we can prove that any non-zero natural number must be the successor of some other natural number.","tag":"Paragraph"},{"contents":["Theorem",[["pred",[["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["k",{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],[[{"style":"Prose","subtitle":"Show:"},["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["k",{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"},[{"contents":[{"contents":["_nat",1],"tag":"Cases"},{"contents":0,"tag":"Local"}],"tag":"Elim"},[[{"style":"Tree","subtitle":"We can see that 2 contradicts 1, so we can discharge our goal via /ex falso quodlibet/:"},[],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}]],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["k",{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"},[{"contents":[{"contents":"not E","tag":"Defn"},{"contents":1,"tag":"Local"}],"tag":"Elim"},[[null,[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"},[{"contents":2,"tag":"Local"},[]]]]]],[{"style":"Abbr","subtitle":"In this case, our assumption trivially gives a witness for our goal:"},["n'"],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["exists",false],"tag":"Const"},{"contents":["k",{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"},[{"contents":"exists I","tag":"Defn"},[[null,[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":2,"tag":"Local"},[]]]]]]]]],6]]],[]],"tag":"Rule"},{"contents":"In this case, only the top level application of the cases rule is presented in prose-style, with further subgoals still presented in tree-style. Holbert allows the reader to decide which style to use, and can switch between them seamlessly. As can be seen in the final subgoal of the above proof, some subgoals of a proof (or even entire proofs) can also be presented in /summary/ style, which displays only the rules used.","tag":"Paragraph"},{"contents":[2,"Constructors"],"tag":"Heading"},{"contents":"The symbols $@S$ and $@0$ above are what Holbert calls /constructors/. Constructors are input by prefixing their name with an ~@~ sign. Constructors are much the same as any other symbol, except that Holbert assumes that they are /injective/ and /disjoint/. If a goal has an assumption that asserts the equality of two different constructors, e.g. $x y z:@A x y = @B z$, then eliminating on this assumption will allow Holbert to make use of its in-built constructor disjointness theorem to prove the goal. Similarly, if an assumption asserts the equality of two applications of the same constructor, e.g. $x y a b: @C x y = @C a b$, Holbert can use its in-built injectivity theorem to generate assumptions $x a: x = a$ and $y b: y = b$. As an example, see the following proof that says that a natural number is never equal to its own successor:","tag":"Paragraph"},{"contents":["Theorem",[["notSucc",[["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"}],[[{"style":"Prose","subtitle":"Show:"},["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":[{"contents":["_nat",1],"tag":"Induction"},{"contents":0,"tag":"Local"}],"tag":"Elim"},[[{"style":"Tree","subtitle":"In the base case, we must use disjointness:"},[],[],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":"not I","tag":"Defn"},[[null,["X"],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":0,"tag":"LocalVar"},[{"contents":{"contents":1,"tag":"Local"},"tag":"Distinctness"},[]]]]]],[{"style":"Tree","subtitle":"In the inductive case, we use injectivity to get to our inductive hypothesis:"},["n'"],[[[],[],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":["not",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":"not I","tag":"Defn"},[[null,["X"],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":0,"tag":"LocalVar"},[{"contents":[{"tag":"Injectivity"},{"contents":3,"tag":"Local"}],"tag":"Elim"},[[null,[],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":0,"tag":"LocalVar"},[{"contents":[{"contents":"not E","tag":"Defn"},{"contents":1,"tag":"Local"}],"tag":"Elim"},[[null,[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":4,"tag":"Local"},[]]]]]]]]]]]]]]],8]]],[]],"tag":"Rule"},{"contents":[2,"Equality"],"tag":"Heading"},{"contents":"As can be seen in the derived cases rules, Holbert has a built-in notion of equality. It also supports rewriting a goal by such equalities. Of course, it is possible to encode such rewriting as an elimination rule, like:","tag":"Paragraph"},{"contents":["Axiom",[["subst",[["P","x","y"],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null]],[]],"tag":"Rule"},{"contents":"But, as our elimination rules are typically applied to an assumption, this would only be practically useful if the equality was one of the assumptions inside our goal context. Thus, we instead provide a bespoke rewriting function. Clicking a button in the goal view displays available equalities by which to rewrite. To determine if an equality is applicable, Holbert searches through the goal for a subterm that unifies with the left (or right, if the rewriting direction is reversed) hand side of the equality. To demonstrate this feature, we will first axiomatise some equations to define addition of natural numbers.","tag":"Paragraph"},{"contents":["Axiom",[["+B",[["n"],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["+I",[["m","n"],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"}],null]],[]],"tag":"Rule"},{"contents":"We can then inductively prove the right identity of addition, making use of rewriting in the inductive case:","tag":"Paragraph"},{"contents":["Theorem",[["+ 0",[["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[{"style":"Prose","subtitle":"Show:"},["n"],[[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":[{"contents":["_nat",1],"tag":"Induction"},{"contents":0,"tag":"Local"}],"tag":"Elim"},[[{"style":"Prose","subtitle":"For the base case, we can simply show:"},[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"},[{"contents":"+B","tag":"Defn"},[]]],[{"style":"Tree","subtitle":"This inductive case is shown by rewriting:"},["n'"],[[[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":["_nat",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":[{"contents":"+I","tag":"Defn"},false,"LHS"],"tag":"Rewrite"},[[null,[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":[{"contents":[{"contents":["_+_",false],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["0",true],"tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":[{"contents":1,"tag":"Local"},false,"LHS"],"tag":"Rewrite"},[[null,[],[],{"contents":[{"contents":[{"contents":["_=_",false],"tag":"Const"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":["S",true],"tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"tag":"Refl"},[]]]]]]]]]]]],14]]],[]],"tag":"Rule"},{"contents":"The arrow superscripts on the names of the rules applied indicate the direction of rewriting, and *refl* is the built-in axiom of reflexivity. ","tag":"Paragraph"},{"contents":"In proofs of equalities such as the above, it is common to present proofs as a sequence of equalities, in a /calculational/ or /equational/ style. Currently, this is not supported by Holbert, but work is underway to implement it, for both equalities and, more generally, for any preorder.","tag":"Paragraph"},{"contents":[1,"Related Work"],"tag":"Heading"},{"contents":"Holbert is not the only graphical proof assistant, nor the only proof assistant designed for education. @Logitext|http://logitext.mit.edu/main@ runs in the browser and is used to make an interactive tutorial for the sequent calculus^[22]:Edward Z. Yang. /Interactive Tutorial of the Sequent Calculus/. 2022. @http://logitext.mit.edu/logitext.fcgi/tutorial@^. Like Holbert, it features a graphical interface for constructing Gentzen trees. But, unlike Holbert, it is limited to the connectives and quantifiers of first-order logic, and does not allow students nor teachers to define their own rules or definitions. Jape^[23]:Richard Bornat, Bernard Sufrin. /Animating Formal Proof at the Surface: The Jape Proof Calculator/. The Computer Journal, 1999. @10.1093/comjnl/42.3.177|https://doi.org/10.1093/comjnl/42.3.177@^ is a now-defunct graphical prover written in Java that allows students to explore proofs using unification in a pre-encoded logic. @Edukera|https://edukera.com/@ and @dEAduction|https://github.com/dEAduction@ are both similar graphical proof interfaces, for Coq and Lean respectively. As Bartzia et al.^[10]:Evmorfia Bartzia, Antoine Meyer and Julien Narboux. /Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis/. 2022. @hal-03648357|https://hal.archives-ouvertes.fr/hal-03648357@^ note, all of these tools are not as general-purpose as Holbert, as they focus on /proof/ exercises and do not consider /formalisation/ exercises. They do not allow student users to create new rules or definitions^2:According to Bartzia et al., Edukera further restricts teachers to simply composing exercise sheets out of pre-defined exercises.^. This prevents the setting of exercises where a student must formalise in the proof assistant a theory described to them in writing, for example.","tag":"Paragraph"},{"contents":"@Alfa|https://cth.altocumulus.org/~hallgren/Alfa/index.html@, an earlier incarnation of @Agda|https://wiki.portal.chalmers.se/agda/pmwiki.php@, is a proof assistant based on Martin-Löf type theory with a structural editor and visualisation of proofs based on Gentzen trees. While Alfa is higher-order, graphical, and general purpose, it is no longer maintained, and unlike Holbert it is not suitable as a platform for a textbook.\n","tag":"Paragraph"},{"contents":"SASyLF^[24]:Jonathan Aldrich, Robert J. Simmons, Key Shin. /SASyLF: An Educational Proof Assistant for Language Theory/. FDPE '08. @10.1145/1411260.1411266|https://doi.org/10.1145/1411260.1411266@^ is an educational proof assistant intended for programming language theory. It is foundationally based on Twelf^[25]: Frank Pfenning, Carsten Schürmann. /System Description: Twelf — A Meta-Logical Framework for Deductive Systems/. CADE 1999. @10.1007/3-540-48660-7_14|https://doi.org/10.1007/3-540-48660-7_14@^, and therefore supports higher order abstract syntax as Holbert does. Unlike Holbert, it uses a more conventional textual interface, but with a syntax that tries to approximate conventional computer science notation. ","tag":"Paragraph"},{"contents":"ORC²A^[26]:Jianting Chen, Medha Gopalaswamy, Prabir Pradhan, Sooji Son, Peter-Michael Osera. /ORC²A: A Proof Assistant for Undergraduate Education/. SIGCSE '17. @10.1145/3017680.3022466|https://doi.org/10.1145/3017680.3022466@^ is a proof assistant that aims to make proof construction approachable to computer science students already skilled at programming, specifically applied to verification of computer programs. It features a text-based explicit proof language similar to Isabelle's Isar language.","tag":"Paragraph"},{"contents":"Unlike Holbert, none of the above-mentioned proof assistants are suitable for use as an interactive textbook platform. Lurch^[27]:Nathan C. Carter and Kenneth G. Monks. /Lurch: a word processor that can grade students' proofs/. OpenMath Workshop, 2013. @CICM-WS-WiP2013|http://ceur-ws.org/Vol-1010/paper-04.pdf@^, on the other hand, is primarily intended as a mathematical word processor, but includes some proof checking capabilities via its OpenMath backend. Unlike Holbert, this proof checking capability is more of a post-hoc sanity check (The authors describe it as a spell-checker for mathematics), and it does not assist the user in writing the proofs with an interactive interface, as Holbert does. ","tag":"Paragraph"},{"contents":[1,"Conclusions"],"tag":"Heading"},{"contents":"Holbert is still a work in progress, but it can already be used as an educational aid. It has been used in classes on logic at TU Dresden and Utrecht University, and Zabarauskas^[28]:Brendan Zabarauskas. /Martin-Löf Type Theory in Holbert./ 2022. @Gist|https://gist.github.com/brendanzab/1b4732179b15201bf33fed6dbca02458@^ has successfully formalised the type theory of Martin-Löf in Holbert and carried out some non-trivial proofs.","tag":"Paragraph"},{"contents":"In addition to the calculational proofs mentioned above, we also intend to add a feature to allow function definitions, which will bring Holbert roughly in line other HOL-based provers in terms of fundamental proof assistant features. There is also tremendous scope for domain-specific extensions to Holbert. Constructing category-theoretic proofs using commutative or string diagrams, doing geometry proofs visually, or annotating a computer program with Hoare logic assertions could be done as naturally as on paper. We are excited to explore these possibilities.","tag":"Paragraph"},{"contents":"Holbert is an open-source project, implemented in Haskell and compiled to JavaScript using @ghcjs|https://github.com/ghcjs/ghcjs@. We encourage contributions from anyone who is interested, and new features and capabilities are being added all the time. ","tag":"Paragraph"}]