oldindex.holbert

[{"tag":"Heading","contents":[0,"Holbert Demo"]},{"tag":"Paragraph","contents":"Welcome to this demo of the Holbert prototype. Holbert is the combination of an online notebook and higher-order logic theorem prover. It allows for preparation of interactive documents which include proof exercises in natural deduction style. "},{"tag":"Heading","contents":[1,"Design Philosophy"]},{"tag":"Paragraph","contents":"I designed Holbert to be an educational tool. Ultimately, I plan to convert the notes from the Programming Languages course I taught for many years into this tool. Previous attempts to integrate theorem provers with PL foundations education have been quite successful (see /Software Foundations/, /Concrete Semantics/), but I feel that the complexity of tools such as Coq and Isabelle mean that their respective courses become less about PL foundations in general and more about how to operate the theorem prover effectively. People using these PL foundations books to learn how to use their proof assistants rather than to learn PL foundations is evidence of this. "},{"tag":"Paragraph","contents":"In addition, conventional proof assistants are large pieces of software that can be complicated to install. By making Holbert run in the browser, students don't have to install anything, and can even use a tablet or other device to access work."},{"tag":"Paragraph","contents":"Holbert is both a document preparation system and a proof assistant. This way, proof problems and sets of rules and exercises can be embedded right within educational notes. In future, I want to extend this system to support examinations and assessments as well."},{"tag":"Paragraph","contents":"Holbert is based on /natural deduction/ and /higher order logic/. Because it doesn't have a type system, this means the logic it encodes is *unsound*. So it should not be used to verify production software or anywhere where the theorems it proves should be trusted. Normally, I would be very opposed to removing type systems from anything, however removing the type system from higher order logic simplifies its pedagogy, particularly when teaching a course about type systems. If I used a typed theorem prover, in order to teach about types, I would first have to teach about types, which is an annoying circularity.\n"},{"tag":"Heading","contents":[1,"Propositional Logic"]},{"tag":"Paragraph","contents":"To give an example of Holbert in action, lets define basic propositional logic. All terms are given in untyped lambda calculus. Terms applied to constants with underscores in them are rendered as infix operators. For example, ~if_then_else_fi A B C~ is rendered as $A B C:if_then_else_fi A B C$. Many common operators and symbols have their ASCII approximations replaced with unicode, and trailing numbers are rendered as subscripts.\n"},{"tag":"Rule","contents":["Axiom",[["/\\ I",[["phi","psi"],[[[],[],{"tag":"LocalVar","contents":1}],[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],null],["/\\ E1",[["phi","psi"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":1}],null],["/\\ E2",[["phi","psi"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":0}],null]],[]]},{"tag":"Paragraph","contents":"The implication rules give an example of a hypothetical derivation (i.e. a rule with a rule as a premise):\n"},{"tag":"Rule","contents":["Axiom",[["-> I",[["phi","psi"],[[[],[[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],null],["-> E",[["phi","psi"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}],null]],[]]},{"tag":"Paragraph","contents":"The \"Display Options\" in the bottom section of the sidebar provides a few options for rendering these rules. By default, we use the \"Hybrid\" mode which uses linear notation for premises and vertical notation for the main inference vinculum. Vertical notation is closer to Gentzen's original notation for natural deduction.\n"},{"tag":"Paragraph","contents":"The rules are editable. Click any part of the rule to edit it. To add premises, first click on the conclusion to which you want to add a premise. Similarly for meta-binders.\n\n/Note/: Altering rules will delete any part of a proof that makes use of the rule, to ensure that theorems remain in a consistent state. Be careful of this!"},{"tag":"Paragraph","contents":"To add new rules (or indeed any other element), click on a plus sign icon on the right hand side of the main content panel, then click \"Axiom\"."},{"tag":"Heading","contents":[2,"Proofs"]},{"tag":"Paragraph","contents":"Proofs are constructed \"backwards\", in the bottom-up fashion working from the conclusion. Clicking on a goal tag on the proof tree for a Theorem gives a list of all applicable introduction rules. Click on any such fact to apply it to the current goal. To apply an elimination rule on an assumption, click on the assumption and choose from the list of available elimination rules."},{"tag":"Paragraph","contents":"First, we shall prove a combined elimination rule for conjunction, which is a bit easier to work with:"},{"tag":"Rule","contents":["Theorem",[["/\\ E",[["phi","psi","P"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}],[[],[[[],[],{"tag":"LocalVar","contents":2}],[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}]],{"tag":"LocalVar","contents":0}],[[null,["phi","psi","P"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}],[[],[[[],[],{"tag":"LocalVar","contents":2}],[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}]],{"tag":"LocalVar","contents":0},[{"tag":"Local","contents":1},[[null,[],[],{"tag":"LocalVar","contents":2},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E1"},{"tag":"Local","contents":0}]},[]]],[null,[],[],{"tag":"LocalVar","contents":1},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E2"},{"tag":"Local","contents":0}]},[]]]]]],4]]],[]]},{"tag":"Paragraph","contents":"Our next example, associativity of conjunction, is complete already, whereas commutativity has not been started:\n"},{"tag":"Rule","contents":["Theorem",[["/\\ assoc",[["A","B","C"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}]}],[[null,["A","B","C"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"/\\ I"},[[null,[],[],{"tag":"LocalVar","contents":2},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E"},{"tag":"Local","contents":0}]},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}],[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"LocalVar","contents":2},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E1"},{"tag":"Local","contents":1}]},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},[{"tag":"Defn","contents":"/\\ I"},[[null,[],[],{"tag":"LocalVar","contents":1},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E"},{"tag":"Local","contents":0}]},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}],[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"LocalVar","contents":1},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E2"},{"tag":"Local","contents":1}]},[]]]]]],[null,[],[],{"tag":"LocalVar","contents":0},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"/\\ E2"},{"tag":"Local","contents":0}]},[]]]]]]]]]]]],18]]],[]]},{"tag":"Rule","contents":["Theorem",[["/\\ comm",[["A","B"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]}],[[null,["A","B"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_/\\_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]},null],2]]],[]]},{"tag":"Heading","contents":[2,"Disjunction and Negation"]},{"tag":"Paragraph","contents":"We haven't yet specified all the remaining bits of propositional logic, so let's quickly do that now:"},{"tag":"Rule","contents":["Axiom",[["\\/ I1",[["phi","psi"],[[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_\\/_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],null],["\\/ I2",[["phi","psi"],[[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_\\/_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],null],["\\/ E",[["phi","psi","P"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_\\/_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}],[[],[[[],[],{"tag":"LocalVar","contents":2}]],{"tag":"LocalVar","contents":0}],[[],[[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}]],{"tag":"LocalVar","contents":0}],null]],[]]},{"tag":"Paragraph","contents":"We will specify negation $phi: not phi$ as merely equivalent to $phi: _->_ phi bot$, with the same introduction and elimination rules as implication (except that the conclusion of $not$ elimination is generalised to avoid needless applications of $bot$ elimination):\n"},{"tag":"Rule","contents":["Axiom",[["not I",[["phi"],[[[],[[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"Const","contents":"bot"}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}],null],["not E",[["phi","P"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":1}]}],[[],[],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}],null]],[]]},{"tag":"Paragraph","contents":"Lastly, the rules to define the constants for true $top$ and false $bot$, where true has only an introduction rule and false has only an elimination rule."},{"tag":"Rule","contents":["Axiom",[["top I",[[],[],{"tag":"Const","contents":"top"}],null],["bot E",[["P"],[[[],[],{"tag":"Const","contents":"bot"}]],{"tag":"LocalVar","contents":0}],null]],[]]},{"tag":"Heading","contents":[3,"Constructivity"]},{"tag":"Paragraph","contents":"The logic we have formalised here is constructive. We can prove only double negation introduction:\n"},{"tag":"Rule","contents":["Theorem",[["not not I",[["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}]}],[[null,["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"not I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Const","contents":"bot"},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"not E"},{"tag":"Local","contents":1}]},[[null,[],[],{"tag":"LocalVar","contents":0},[{"tag":"Local","contents":0},[]]]]]]]]]]]],5]]],[]]},{"tag":"Paragraph","contents":"To experiment with the above proof, you can press the trash can next to any rule application to reconstruct the proof from that point.\n"},{"tag":"Paragraph","contents":"Because we are in a constructive setting, our rules are not enough to express double negation elimination, one formulation of excluded middle:"},{"tag":"Rule","contents":["Theorem",[["not not E",[["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}],[[null,["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]},null],5]]],[]]},{"tag":"Heading","contents":[1,"Higher-Order Logic"]},{"tag":"Paragraph","contents":"As Holbert terms are $lambda$ terms, we can use $lambda$-abstractions to encode variable binding structure, and avoid ugliness such as substitution. These $lambda$ abstractions are defined without much ceremony in Holbert, where $P: x. P x$ (written as ~x. P x~) is a $lambda$ term with a parameter $x$ and a result $P: P x$.\n"},{"tag":"Rule","contents":["Axiom",[["all I",[["P"],[[["x"],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}],null],["all E",[["P","x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}],null]],[]]},{"tag":"Paragraph","contents":"The existential quantifier is the dual of the universal, and the rules are using a similar format, but with an auxiliary conclusion variable (similar to $\\/$ elimination):\n"},{"tag":"Rule","contents":["Axiom",[["exists I",[["P","x"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}],null],["exists E",[["P","R"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":1}]],{"tag":"LocalVar","contents":0}],null]],[]]},{"tag":"Paragraph","contents":"As we are still in a constructive logic, we can prove only one direction of the classical equivalence between $P: exists (x. not (P x))$ and $P: not (all (x. P x))$.\n"},{"tag":"Rule","contents":["Theorem",[["deMorgan1",[["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]}],[[null,["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Defn","contents":"not I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]],{"tag":"Const","contents":"bot"},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"exists E"},{"tag":"Local","contents":0}]},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Const","contents":"bot"},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"not E"},{"tag":"Local","contents":2}]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"all E"},{"tag":"Local","contents":1}]},[]]]]]]]]]]]]]]],9]]],[]]},{"tag":"Paragraph","contents":"In the other direction, we do get almost to a complete proof, and at first glance it looks as though we could unify the metavariable with $x: x$ to complete the proof:\n"},{"tag":"Rule","contents":["Theorem",[["deMorgan2",[["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]}],[[null,["P"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Defn","contents":"exists I"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":0},{"tag":"Ap","contents":[{"tag":"MetaVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]},[{"tag":"Defn","contents":"not I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":0},{"tag":"Ap","contents":[{"tag":"MetaVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Const","contents":"bot"},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"not E"},{"tag":"Local","contents":0}]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"all"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]},[{"tag":"Defn","contents":"all I"},[[null,["x"],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]},null]]]]]]]]]]]]]]]],9]]],[]]},{"tag":"Paragraph","contents":"The reason this doesn't work becomes clearer if we show metavariable telescopes (the option in the sidebar). The variable $x: x$ does not occur in the telescope, and thus this metavariable cannot be unified with $x : x$.\n"},{"tag":"Heading","contents":[1,"Equality"]},{"tag":"Paragraph","contents":"Holbert has a built-in notion of equality. The constant $_=_$ is assumed to be a reflexive, symmetric relation that is a congruence in all contexts. We can define specific equalities just by writing new axioms, for example logical equivalence:"},{"tag":"Rule","contents":["Axiom",[["iff",[["phi","psi"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],null]],[]]},{"tag":"Paragraph","contents":"We can now prove the equivalence of negation and implication to false. Because this proof consists of two distinct lemmas for each direction, it's convenient to use /prose style/ proofs in this case. The proof presentation mode changes how a proof appears in the document. By default, proofs are in /tree mode/, but clicking the button next to the \"/Proof/\" heading switches to prose style. In prose style, each goal is laid out vertically, and a small (editable) paragraph of text is associated with each case. Each subgoal can itself be in either tree style or prose style. The tree icon can be clicked to convert back into tree style."},{"tag":"Rule","contents":["Theorem",[["not -equiv",[["phi"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]}],[[{"subtitle":"Show:","proseStyle":true},["phi"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},[{"tag":"Defn","contents":"iff"},[[{"subtitle":"Show our first direction:","proseStyle":false},[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"Const","contents":"bot"},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"not E"},{"tag":"Local","contents":0}]},[[null,[],[],{"tag":"LocalVar","contents":0},[{"tag":"Local","contents":1},[]]]]]]]]]]]],[{"subtitle":"Showing the other direction:","proseStyle":false},[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"-> I"},[[null,[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]},[{"tag":"Defn","contents":"not I"},[[null,[],[[[],[],{"tag":"LocalVar","contents":0}]],{"tag":"Const","contents":"bot"},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"-> E"},{"tag":"Local","contents":0}]},[[null,[],[],{"tag":"LocalVar","contents":0},[{"tag":"Local","contents":1},[]]]]]]]]]]]]]]],13]]],[]]},{"tag":"Heading","contents":[2,"Rewriting"]},{"tag":"Paragraph","contents":"If we have an equality $A B:_=_ A B$ and we have a goal $A: P A$ (for any context $P$) then we can /rewrite/ the goal into $A: P B$ using Holbert's built-in goal rewriting feature. Pressing the small equals sign on the sidebar next to the goal when a goal is selected shows available rewrite rules. "},{"tag":"Paragraph","contents":"As an example, we can prove that $A: not (not A)$ follows from $A: _->_ (_->_ A bot) bot$ by rewriting by our equality above:"},{"tag":"Rule","contents":["Theorem",[["not not -example1",[["A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},{"tag":"Const","contents":"bot"}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}],[[null,["A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},{"tag":"Const","contents":"bot"}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"not -equiv"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Const","contents":"bot"}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"not -equiv"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},{"tag":"Const","contents":"bot"}]},[{"tag":"Local","contents":0},[]]]]]]]]],7]]],[]]},{"tag":"Paragraph","contents":"Note that the second (i.e. higher in the tree) rewriting did so /inside/ the context of $_->$ $bot$. This illustrates the convenience of rewriting. The proof in the other direction can be accomplished by rewriting in reverse, exploiting symmetry of equality:"},{"tag":"Rule","contents":["Theorem",[["not not -example2",[["A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},{"tag":"Const","contents":"bot"}]}],[[null,["A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},{"tag":"Const","contents":"bot"}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"not -equiv"},true]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"bot"}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"not -equiv"},true]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Local","contents":0},[]]]]]]]]],10]]],[]]},{"tag":"Heading","contents":[1,"Induction"]},{"tag":"Paragraph","contents":"Inductive judgements can be defined by using the \"Inductive\" rule block. These blocks are much like the \"Axioms\" rule blocks we've already seen, but they require all rules defined to be /introduction/ rules. From these blocks, two kinds of elimination rules are /automatically generated/. For each judgement introduces, the cases rule allows us to perform rule inversion, and the induction rule allows for induction. As an example, let us first define the natural numbers:"},{"tag":"Rule","contents":["Inductive",[["zero",[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Const","contents":"0"}]}],null],["suc",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],null]],[[{"tag":"Cases","contents":["_nat",1]},[["§P","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]}]],{"tag":"LocalVar","contents":1}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":2}]],{"tag":"LocalVar","contents":1}]],[{"tag":"Induction","contents":["_nat",1]},[["§P0","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"Const","contents":"0"}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]]]]},{"tag":"Paragraph","contents":"The expandable \"Derived Rules\" section contains all the generated axioms for each of the defined judgements. As a simple example of rule inversion, let's prove that any non-zero natural number must be the successor of some other natural number:"},{"tag":"Rule","contents":["Theorem",[["pred",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["k",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}]}],[[{"subtitle":"Show:","proseStyle":true},["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"not"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["k",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Elim","contents":[{"tag":"Cases","contents":["_nat",1]},{"tag":"Local","contents":0}]},[[{"subtitle":"We know that $n: n = 0$ is false, so we can discharge our goal ex falso.","proseStyle":false},[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["k",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Elim","contents":[{"tag":"Defn","contents":"not E"},{"tag":"Local","contents":1}]},[[{"subtitle":"Show:","proseStyle":true},[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]},[{"tag":"Local","contents":2},[]]]]]],[{"subtitle":"We may show:","proseStyle":false},["k"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"exists"},{"tag":"Lam","contents":["k",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Defn","contents":"exists I"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Local","contents":2},[]]]]]]]]],6]]],[]]},{"tag":"Paragraph","contents":"To demonstrate induction, let's define an alternative version of natural numbers with different inductive structure:"},{"tag":"Rule","contents":["Inductive",[["zero'",[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Const","contents":"0"}]}],null],["one'",[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Const","contents":"0"}]}]}],null],["suc-suc'",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}],null]],[[{"tag":"Cases","contents":["_nat'",1]},[["§P","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}],[[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]}]],{"tag":"LocalVar","contents":1}],[[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"LocalVar","contents":1}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":2}]],{"tag":"LocalVar","contents":1}]],[{"tag":"Induction","contents":["_nat'",1]},[["§P0","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"Const","contents":"0"}]}],[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Const","contents":"0"}]}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]]]]},{"tag":"Paragraph","contents":"Let us show that our strange natural numbers are perfectly natural, by induction:"},{"tag":"Rule","contents":["Theorem",[["nat' -> nat",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[{"subtitle":"Show:","proseStyle":true},["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Elim","contents":[{"tag":"Induction","contents":["_nat'",1]},{"tag":"Local","contents":0}]},[[{"subtitle":"/Base case/. We must show","proseStyle":true},[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Const","contents":"0"}]},[{"tag":"Defn","contents":"zero"},[]]],[{"subtitle":"/Base case/. We must show","proseStyle":false},[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Const","contents":"0"}]},[{"tag":"Defn","contents":"zero"},[]]]]]],[{"subtitle":"/Inductive case/. We must show","proseStyle":false},["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Local","contents":1},[]]]]]]]]]]]],5]]],[]]},{"tag":"Paragraph","contents":"Showing the other direction first requires us to prove a lemma:"},{"tag":"Rule","contents":["Theorem",[["nat' -suc",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[[{"subtitle":"Show:","proseStyle":true},["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Elim","contents":[{"tag":"Induction","contents":["_nat'",1]},{"tag":"Local","contents":0}]},[[{"subtitle":"/Base case/. We show","proseStyle":true},[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"one'"},[]]],[{"subtitle":"/Base case/. We show","proseStyle":false},[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Const","contents":"0"}]}]}]},[{"tag":"Defn","contents":"suc-suc'"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Const","contents":"0"}]},[{"tag":"Defn","contents":"zero'"},[]]]]]],[{"subtitle":"/Inductive case/. We show","proseStyle":false},["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Defn","contents":"suc-suc'"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Local","contents":1},[]]]]]]]]],4]]],[]]},{"tag":"Paragraph","contents":"With our lemma we can now prove our goal:"},{"tag":"Rule","contents":["Theorem",[["nat -> nat'",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}],[[{"subtitle":"Show:","proseStyle":true},["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]},[{"tag":"Elim","contents":[{"tag":"Induction","contents":["_nat",1]},{"tag":"Local","contents":0}]},[[{"subtitle":"/Base case/. We show:","proseStyle":true},[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Const","contents":"0"}]},[{"tag":"Defn","contents":"zero'"},[]]],[{"subtitle":"/Inductive case/. We show (with our lemma):","proseStyle":false},["k"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"nat' -suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat'"},{"tag":"LocalVar","contents":0}]},[{"tag":"Local","contents":1},[]]]]]]]]],3]]],[]]},{"tag":"Heading","contents":[2,"Simultaneous Induction"]},{"tag":"Paragraph","contents":"Simultaneous induction is a little awkward, but possible in Holbert. To demonstrate, let's define two mutually inductive predicates for odd and even numbers:"},{"tag":"Rule","contents":["Inductive",[["zero-even",[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"Const","contents":"0"}]}],null],["suc-even",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],null],["suc-odd",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],null]],[[{"tag":"Cases","contents":["_even",1]},[["§P","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}],[[],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"0"}]}]],{"tag":"LocalVar","contents":1}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":2}]],{"tag":"LocalVar","contents":1}]],[{"tag":"Cases","contents":["_odd",1]},[["§P","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":2}]],{"tag":"LocalVar","contents":1}]],[{"tag":"Induction","contents":["_even",1]},[["§P0","§P1","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"Const","contents":"0"}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]],[{"tag":"Induction","contents":["_odd",1]},[["§P0","§P1","§0"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"Const","contents":"0"}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}],[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]]]]},{"tag":"Paragraph","contents":"We can prove that all even (or odd) numbers are natural numbers by simultaneous induction, however because we can only prove one of these theorems at a time, Holbert's unification will not fill in the other inductive hypothesis for us. So, we have to manually instantiate the metavariable when applying the induction rule, and proving both theorems requires a repetition of most of the proof:"},{"tag":"Rule","contents":["Theorem",[["even- nat",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[null,["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Elim","contents":[{"tag":"Induction","contents":["_even",1]},{"tag":"Local","contents":0}]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Const","contents":"0"}]},[{"tag":"Defn","contents":"zero"},[]]],[null,["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Local","contents":1},[]]]]]],[null,["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Local","contents":1},[]]]]]]]]],5]]],[]]},{"tag":"Rule","contents":["Theorem",[["odd- nat",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[null,["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Elim","contents":[{"tag":"Induction","contents":["_odd",1]},{"tag":"Local","contents":0}]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Const","contents":"0"}]},[{"tag":"Defn","contents":"zero"},[]]],[null,["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_odd"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Local","contents":1},[]]]]]],[null,["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_even"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"Ap","contents":[{"tag":"Const","contents":"S"},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"suc"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_nat"},{"tag":"LocalVar","contents":0}]},[{"tag":"Local","contents":1},[]]]]]]]]],5]]],[]]},{"tag":"Paragraph","contents":"While this is mildly inconvenient, we don't see this as something that urgently needs addressing for now."}]