# Rhombus/HOL ```racket #lang rhombus/hol package: [rhombus-hol-prover](https://pkgs.racket-lang.org/package/rhombus-hol-prover) ``` Rhombus/HOL is a theorem prover embedded in Rhombus: an LCF-style higher-order-logic kernel with an ACL2-style automatic prover on top. A module written in `rhombus/hol` is an ordinary Rhombus module that may also contain logical declarations, and those declarations have two readings at once. A datatype is a derived logical datatype ​_and_​ a set of Rhombus classes; a function definition is a derived set of equations ​_and_​ a Rhombus function; a theorem is a claim that is proved while the module compiles. ```racket #lang rhombus/hol datatype List.of(?a) | Nil() | Cons(head :: ?a, tail :: List.of(?a)) function app(xs :: List.of(?a), ys :: List.of(?a)) :: List.of(?a): match xs | Nil(): ys | Cons(x, rest): Cons(x, app(rest, ys)) theorem app_nil_r: forall (xs :: List.of(?a)): app(xs, Nil()) === xs ``` That module exports a working app function, and it does not compile unless app\_nil\_r is proved. 1 Two Readings of One Declaration 1.1 When things happen 1.2 A complete module 1.3 What is not intercepted 2 Declarations 2.1 datatype 2.1.1 Mutually recursive datatypes 2.2 function 2.2.1 Mutually recursive functions 2.3 definition 2.3.1 Local and anonymous function 2.4 inductive 2.5 HOL notation 2.6 Function overloading 2.7 Executable automata 2.7.1 Generic regular expressions 2.8 theorem and proof 2.9 Importing a theory 2.9.1 Ordering 2.9.2 Forms that cannot be read 3 Types, Expressions and Propositions 3.1 Types 3.2 Expressions 3.2.1 Numerals 3.2.2 Local definitions 3.2.3 Matching 3.2.4 Clauses on the declaration 3.3 Propositions 3.3.1 Named logical constants 3.3.2 Quantifier and choice binders, and `Set` values 3.3.3 Precedence 4 Termination 4.1 Lexicographic structural descent 4.2 Measures 4.3 The subterm relation 4.4 A family of functions 4.5 What is not supported 5 The Prover 5.1 Simplification 5.2 Destructor elimination 5.3 Fertilization 5.4 Generalization 5.5 Elimination of irrelevance 5.6 Induction 5.7 When a proof fails 5.8 Justification 6 What Is Assumed 6.1 The kernel 6.2 Alignment with HOL Light’s `fusion.ml` 6.3 The axioms 6.4 What is postulated beyond that 6.5 Theories 6.6 Where this leaks 6.7 Limitations of this version 7 License and Third-Party Notices ## 1. Two Readings of One Declaration Every logical declaration in a `rhombus/hol` module is read twice, from the same source text. * **Logically**, as a declaration in a _theory_: a datatype contributes injectivity, distinctness, exhaustiveness and induction axioms; a function contributes one equation per clause; a theorem contributes a proved statement. * **Executably**, as ordinary Rhombus: a datatype becomes a class per constructor, and a function becomes a Rhombus function with its type annotations erased. Both readings originate in the same declaration expansion. The HOL enforestation pass produces a theory-independent Core tree; the executable emitter uses the same source declaration. Built-ins therefore use Rhombus’s own spellings wherever a construct exists on both sides — `#true`, !, &&, ||, == and if — while logic-only constructs use spellings such as ===, and and forall. User-defined notation follows the pure, total subset of Rhombus operator case syntax and binds a spelling only in the HOL expression space. Its ordered cases use the same closed patterns, type checker, and decision tree as HOL functions; each fixity must be exhaustive. An ordinary operator remains independent and may additionally use Rhombus-only dynamic bindings, failure, repetition, and unsafe execution. Function overloading is resolved during elaboration, not by the logic. overload adds a typed clause to a callable name; direct calls and calls in notation implementation expressions use the same resolver. A successful call lowers directly to the selected constant. The resulting kernel term contains no overload node, and generated executable code performs no runtime type test. ### 1.1. When things happen Proofs run ​_while the module is compiled_​, not when it is run. A theorem that cannot be proved is a compile error, and so is a definition that cannot be shown to terminate. Nothing about the logic happens at run time; by then the module is just Rhombus code. One consequence is worth stating plainly: a failed proof is reported the way a syntax error is, at the line of the declaration, with the goals that were left over. ```racket theorem rev_is_identity: forall (xs :: List.of(?a)): rev(xs) === xs ``` `theorem: rev_is_identity: could not prove.` `Remaining goal,` `after` `induction on xs (case Cons)` `simplification` `induction on y (case Cons)` `simplification` `assuming rev(y) === y` `assuming app(z, Cons(x, Nil)) === Cons(x, z)` `y === x and x === y` ### 1.2. A complete module ```racket #lang rhombus/hol export: List Nil Cons app rev datatype List.of(?a) | Nil() | Cons(head :: ?a, tail :: List.of(?a)) function app(xs :: List.of(?a), ys :: List.of(?a)) :: List.of(?a): match xs | Nil(): ys | Cons(x, rest): Cons(x, app(rest, ys)) function rev(xs :: List.of(?a)) :: List.of(?a): match xs | Nil(): Nil() | Cons(x, rest): app(rev(rest), Cons(x, Nil())) theorem app_nil_r: forall (xs :: List.of(?a)): app(xs, Nil()) === xs theorem app_assoc: forall (xs :: List.of(?a), ys :: List.of(?a), zs :: List.of(?a)): app(app(xs, ys), zs) === app(xs, app(ys, zs)) theorem rev_app_distr: forall (xs :: List.of(?a), ys :: List.of(?a)): rev(app(xs, ys)) === app(rev(ys), rev(xs)) ``` An ordinary Rhombus module can import that one and use it: ```racket #lang rhombus import: "list_proofs.rhm" open rev(Cons(1, Cons(2, Cons(3, Nil())))) ``` ### 1.3. What is not intercepted `rhombus/hol` is still a general-purpose language. Only the declaration forms in Declarations are given a logical reading; everything else — including ordinary fun, def and class — means exactly what it means in `rhombus`. import means what it means in `rhombus` too, and additionally adopts the theory of whatever it names that has one; see Importing a theory. In particular fun is never intercepted. A logical definition is written with function, and the separate keyword is what makes it possible to report a body outside the definable grammar as an error instead of silently treating the definition as an ordinary one. ```racket // a logical definition: equations, derivation, a termination check function double(n :: Nat) :: Nat: match n | zero(): zero() | succ(k): succ(succ(double(k))) // an ordinary Rhombus function: no logical meaning, no restrictions fun describe(n :: Int) :: String: "the number " +& n ``` ## 2. Declarations These are the forms that `rhombus/hol` gives a logical reading. Anything else in a module body is ordinary Rhombus. The declarations that change the current theory, including overload, are bound macros. A user-written declaration macro can expand to them; generated declarations contribute executable bindings and logical state in the same expansion order as directly written declarations. They must ultimately expand in a module body, not inside a block or a fun body. notation is also a bound macro. Each notation definition is visible while the following logical declaration is enforested. ### 2.1. datatype `datatype Id` `| ctor` `| ...` `datatype Id.of(?tyvar, ...)` `| ctor` `| ...` `ctor = CtorId` `| CtorId()` `| CtorId(field :: Type, ...)` Declares an _algebraic datatype_. A type variable is written ?a. A parameterized declaration binds `Id.of`; the bare `Id` remains a constructor namespace and cannot be used as a type without its arguments. Nullary datatypes continue to use their bare identifier. The declaration head may end in `:`; this is the block form of the same declaration. A nullary constructor declaration may likewise omit its empty parentheses. Thus `datatype Nat: | zero` and `datatype Nat | zero()` declare the same datatype shape. The omission applies to the constructor declaration; expressions and patterns in this manual use the explicit call form `zero()`. ```racket datatype List.of(?a) | Nil() | Cons(head :: ?a, tail :: List.of(?a)) ``` Logically this ​_derives_​ the usual characterisation of the type — constructors are injective, distinct constructors build distinct values, every value is built by some constructor, and the induction principle holds — as theorems with no hypotheses. A non-recursive type is built as a sum of products over its field types; a recursive one is carved out of the labelled trees over `num` with the kernel’s type-definition principle. Neither adds an axiom. Field selectors and constructor discriminators are declared too, so List above brings Cons\_head, Cons\_tail, is\_Nil and is\_Cons into the theory. All of their equations enter the rewriter, which is what makes match-defined functions compute during a proof. A recursive datatype also gets its subterm relation; see Termination. Except for the exact reserved declaration `datatype Nat | zero() | succ(pred :: Nat)`, executable datatypes emit one Rhombus class per constructor, related by an interface so that a value can be matched against any of them. The classes are ordinary: they compare structurally with == and print readably. The reserved `Nat` is the intentional runtime-representation exception. Its executable values are host nonnegative integers: `zero()` produces `0`, `succ(n)` produces `n + 1`, `zero()` patterns test for zero, and `succ(p)` patterns accept positive integers and bind the predecessor. Its logical datatype, constructor equations, and derived theorems are unchanged, and no other datatype is represented this way. A declaration is rejected unless every recursive occurrence of the type is _strictly positive_ — informally, the type being declared may not appear to the left of an arrow in a field. An ill-founded declaration has no set of labelled trees to be carved out of, so it now fails to be constructed rather than being assumed into existence. #### 2.1.1. Mutually recursive datatypes `datatype.together:` `datatype Id` `| ctor` `| ...` `datatype Id` `| ctor` `| ...` A `datatype.together:` block declares a family of datatypes at once, so a constructor field may be at any member of the family. Every member declares the same type parameters, constructor names are distinct across the family, and every member must be inhabited by values the family’s own constructors build. ```racket datatype.together: datatype Expr | lit(value :: Nat) | app(args :: Args) datatype Args | anil() | acons(head :: Expr, tail :: Args) ``` The family is read as one ordinary recursive datatype — the union of every member’s constructors — with each member carved out of it as the least set its own constructors build, which is inductive’s construction. So a family adds no representation and no new principle, and each member derives exactly what a lone declaration derives, stated about its own constructors. The family’s joint induction, whose hypotheses may be about any member, is kept by name as `Member1_..._union_induct` for a proof’s `~use:`. A single datatype declaration is the one-member case of the same form. ### 2.2. function `function Id(arg :: Type, ...) :: Type:` `body` `proof:` `~measure: expr` Declares a total, terminating function. The body must be in the grammar of Expressions; anything else is an error naming the offending expression. ```racket function app(xs :: List.of(?a), ys :: List.of(?a)) :: List.of(?a): match xs | Nil(): ys | Cons(x, rest): Cons(x, app(rest, ys)) ``` Logically each winning clause becomes one equation, universally closed over the clause’s variables, and each equation enters the rewriter. Before any of that the definition must pass three checks: the clauses must cover every case, every clause must win for at least one argument shape after earlier clauses take priority, and the recursion must be shown to terminate \(Termination). Clauses may overlap; matching is ordered and the earliest matching clause wins in both the logical and executable readings. The compiler prepares that checked clause matrix once. A function defines a non-recursive matrix directly or derives its recursive equations from the selected well-founded order. If this version cannot construct that proof, it refuses the declaration. Executably it emits a Rhombus fun with the type annotations erased. The erasure is why the annotations may mention type variables that have no run-time meaning. An optional adjacent proof block supplies a termination argument through `~measure: expression` for a definition that does not descend structurally. It is checked only when no structural descent can be found, so a measure on a definition that already descends is not examined. #### 2.2.1. Mutually recursive functions `function.together:` `function Id(arg :: Type, ...) :: Type` `| (pattern, ...): body` `| ...` `function Id(arg :: Type, ...) :: Type` `| (pattern, ...): body` `| ...` A `function.together:` block declares a family of functions at once, so a member’s body may call any member of the family. Each member declares every parameter type and its result type — the members are elaborated against each other, not inferred from their bodies — and all members use the same type variables. A member is always called with all of its arguments. A member may still carry its own adjacent proof block. ```racket function.together: function a_size(a :: Args) :: Nat | (anil()): zero() | (acons(e, r)): plus(e_size(e), a_size(r)) function e_size(e :: Expr) :: Nat | (lit(n)): succ(zero()) | (app(a)): succ(a_size(a)) ``` The family is read as one ordinary function over a tagged argument: a domain datatype with one constructor per member, and a result datatype when the members’ result types differ. That function is derived by the same well-founded machinery a lone recursive function uses, and each member is then the plain definition that tags its arguments and reads the result back. Each member’s own clausal equations are derived from it and enter the rewriter, so proofs see the members and never the encoding. Executably the members are ordinary Rhombus functions calling each other. Because a call leaves the member that made it, the descent order spans the family: either every member supplies `~measure:` into one datatype, or the family descends structurally on one argument column per member, read through a datatype family’s union type when the recursion crosses between mutually recursive datatypes (Termination). A member’s proof block is the ordinary one: it sits next to that member inside the block and carries exactly one `~measure:`. Since the members’ measures are read as one measure over the tag, they land in the same type, and a measure may not call a member of its own family — it justifies the family’s definition, so it cannot use it. ### 2.3. definition `definition Id :: Type:` `expr` Declares one non-recursive constant with an explicit type. The right-hand side is checked as a HOL term of that type and installed through HOL’s basic definition principle. Its resulting equation enters the rewriter, so later theorems unfold uses of the definition normally. ```racket definition choose_zero :: Nat: select (n :: Nat): n === zero() ``` Definitions are logical only: they emit no Rhombus binding and may use noncomputable HOL terms such as select. Use function for a definition that must run: it has an executable reading, supports pattern clauses and recursion, and therefore accepts only the executable expression subset. #### 2.3.1. Local and anonymous function `function (arg :: Type, ...) :: Type:` `body` `function Id(arg :: Type, ...) :: Type:` `body` `tail` Anywhere inside a function or theorem body, `function` means a HOL lambda abstraction rather than a recursive constant definition. Parenthesized parameters with no name (`function (x :: Nat) :: Nat: ...`) produce an anonymous first-class function value, usable as an ordinary argument, result, or applied directly: ```racket function make_succ() :: Nat -> Nat: function (x :: Nat) :: Nat: succ(x) ``` A named local `function Id(...): body` desugars to `let` binding `Id` to that lambda value, then the rest of the enclosing body: `function f(x): e; tail` means `let f = (function (x): e) in tail`. No new semantic mechanism is introduced — named local functions are ordinary non-recursive let sugar, so they follow let’s own sequential scoping (Expressions): a local function sees every earlier binding in the same body, including earlier local functions, but not itself and not any local function declared after it. Nesting to any depth, and lexical capture of an enclosing parameter or let, both follow from this: a local function’s free variables are resolved the same way any other nested lambda’s would be. Because a local function is a plain lambda, it has no recursive binding of its own name and no proof block. Three shapes are therefore rejected rather than silently accepted: * A local function’s body referring to its own name (local self-recursion). * A local function’s body referring to a local function declared later in the same enclosing body (a forward reference). * A local or anonymous function’s body calling the enclosing function that is currently being defined — the top-level recursive-definition machinery is not extended to reach through a nested lambda. A parameter or result type may be omitted from a local or anonymous function; it is then inferred from how the value is used, exactly like any other omitted binder type (Propositions). A local function may also use the case-clause form `function | (pattern, ...): body | ...` in place of an explicit parameter list, with each case’s own patterns supplying the parameters — the same form available for a top-level function’s declaration-level clauses. ### 2.4. inductive `inductive Id(Type, ...)` `| Id: proposition` `| ...` `inductive.together:` `inductive Id(Type, ...)` `| Id: proposition` `| ...` `inductive Id(Type, ...)` `| Id: proposition` `| ...` Declares the least predicates closed under the given rules. Each head lists one predicate’s argument types; each rule is a closed proposition about the predicates being declared, so it quantifies over its own variables. ```racket inductive spine(Tree) | spine_leaf: spine(leaf()) | spine_node: forall (r :: Tree): spine(r) ==> spine(node(leaf(), r)) ``` The declaration makes one basic definition per predicate — each is a component of the intersection of every predicate family the rules are closed under, which ordinary higher-order quantification already expresses — and then ​_derives_​ three families of theorems from them: one introduction theorem per rule, under the rule’s own name; `Id_induct` per predicate, saying that any family closed under the rules contains it; and `Id_cases` per predicate, the inversion theorem, saying that membership came from some rule concluding with that predicate. Nothing is postulated. Predicates declared in one `inductive.together:` block are mutually recursive: they share every rule, so a rule may conclude with any of them and reach the others through its premises. ```racket inductive.together: inductive even_depth(Tree) | even_leaf: even_depth(leaf()) | even_step: forall (t :: Tree): odd_depth(t) ==> even_depth(node(t, t)) inductive odd_depth(Tree) | odd_step: forall (t :: Tree): even_depth(t) ==> odd_depth(node(t, t)) ``` Those theorems are retained by name like a theorem and are requested with `~use:`; they do not enter the rewriter, so the automation never unfolds the fixed point by itself. A rule is rejected unless it concludes with one of the declared predicates applied to its arguments, and unless every recursive occurrence in a premise is an application of a declared predicate in a position the rules are monotone in. An occurrence under not, one to the left of a nested `==>`, one passed to another function, and one inside a rule’s own arguments are each refused: without monotonicity there need be no least predicates closed under the rules, and the introduction theorems would not be derivable. Like definition, an inductive predicate is logical only and emits no Rhombus binding. ### 2.5. HOL notation `notation operator-name :: ResultType:` `operator-option` `...` `| (left-pattern operator-name right-pattern) :: ResultType:` `HOLBody` `| ...` notation adds an operator spelling to the HOL expression space. Its canonical parenthesized prefix, infix, and postfix heads follow Rhombus operator case layout; legacy unparenthesized heads, immediate `|` cases, and named groups of cases are also accepted. Prefix may be combined with infix or postfix, but infix and postfix cannot be combined. Each operand is one pattern from the closed HOL pattern grammar: variables, \_, static type annotations, supported literals and collection forms, and declared datatype constructors. A compound operand pattern that occupies more than one shrubbery term must be parenthesized inside the operator head, just as for operator. Cases of each fixity are tried in source order. Unlike a general Rhombus operator, however, the matrix must be exhaustive, every row must be reachable, and each operand column has one HOL type. Thus notation cannot use dynamic patterns to dispatch between unrelated runtime types. At each use, arbitrary operand expressions are evaluated once, from left to right, before the selected fixity’s cases match their values. A shared or case-local :: annotation is a static HOL result type, not a Rhombus predicate check or converter: ```racket notation <&> :: Boolean: ~order: hol_conjunction ~associativity: ~none | (#false <&> _): #false | (#true <&> right): right theorem conjunction_example: false <&> true ``` The implementation of every case is a HOL body, including sequential let, match, and local function forms. Notation normalizes to an immediately applied anonymous Core function and the same ordered pattern matrix feeds logical elaboration and executable lowering. Actual operand types and pattern constraints are available while overloaded calls in a body are resolved. The notation itself has no ordinary Rhombus binding or repetition binding and adds no logical constant. :~, `~unsafe`, `~name`, `~who`, partial no-match behavior, effects, and multiple values are deliberately unsupported. Outside a logical declaration, use the body’s ordinary Rhombus operations directly or declare a separate ordinary operator; the two expression spaces remain explicit. The precedence options are the ones accepted by Rhombus operator, including `~order`, `~stronger_than`, `~weaker_than`, `~same_as`, `~same_on_left_as`, `~same_on_right_as`, and `~associativity`. A named order supplies its associativity; an explicit associativity is checked against that order. Without a shared named block, only the first case of each fixity may declare options. Shared and case-local options cannot repeat the same kind, and `~associativity` applies only to an infix fixity. The available HOL orders, strongest to weakest, are hol\_application, hol\_power, hol\_prefix\_arithmetic, hol\_multiplication, hol\_addition, hol\_append, hol\_set\_intersection, hol\_set\_union, hol\_relation, hol\_equality, hol\_negation, hol\_conjunction, hol\_disjunction, hol\_implication, and hol\_equivalence. See Propositions for the built-in operators at each order. Multiple fixities of one operator can share options: ```racket notation <~>: ~order: hol_conjunction | (<~> value): neg(value) | (left <~> right): conj(left, right) ``` Different spellings use separate, symmetric declarations: ```racket notation (left <+> right): ~order: hol_addition custom_add(left, right) notation (a <++> b): ~order: hol_addition custom_add(a, b) ``` Notation definitions take effect before the following declaration is enforested. Export the HOL-space binding explicitly: ```racket export: only_space hol_expr: <&> ``` Importing that module with open makes the notation available to following function and theorem declarations. ### 2.6. Function overloading overload adds an overload clause to a callable function name. No separate registration form or operator-specific overload form is needed. Direct calls and calls in notation implementation expressions use the same resolver. `overload add(Nat, Nat) = nat_add` `overload add(Integer, Integer) = int_add` `notation (left <+> right):` `~order: hol_addition` `add(left, right)` Here `x <+> y` binds `left` and `right` before checking `add(left, right)`. The ordinary elaborator sees the call, checks whether `add` has overload clauses, and selects a clause from the argument types and, when available, the expected result type. A successful call becomes a direct call to the selected implementation constant. Kernel terms contain no overload node, and generated executable code performs no runtime type test. The notation-facing overloaded names are `add`, `subtract`, `negate`, `multiply`, `power`, `less`, `less_equal`, `greater`, `greater_equal`, `append`, `member`, `union`, and `intersection`. The standard library also makes common operations available through `map`, `empty`, `size`, `reverse`, `flatten`, `height`, `contains`, `delete`, `to_list`, `compare`, `minimum`, and `maximum`. Importing a theory imports its overload registry together with its constants and theorems. The standard method set is: * `Nat`: arithmetic, power, four order comparisons, three-way comparison, minimum, and maximum. * `Integer` and `Rational`: arithmetic, unary negation, four order comparisons, three-way comparison, minimum, and maximum. * `Option.of(?a)`: map and empty. * `List.of(?a)`: append, map, empty, size, reverse, flatten, and contains. * `NonemptyList.of(?a)`: append, map, and conversion to a list. * `BinaryTree.of(?a)` and `RoseTree.of(?a)`: map, size, flatten, height, and contains. * `FiniteSet.of(?a)`: empty, size, contains, delete, and conversion to a list. * `FiniteMap.of(?k, ?v)`: value map, empty, size, key containment, deletion, and conversion to a list. * `String`: append, map, empty, size, and reverse. * `?a -> Boolean` sets: membership, union, intersection, and subtraction. * `?a -> ?a -> Boolean` relations: union, intersection, and subtraction. Each clause declares the complete argument tuple. Every argument and the expected result type participate in first-order unification. Clauses for one function name must have one arity and must not overlap; an overlap is rejected when the clause is registered instead of creating an order-dependent winner. No applicable clause is a compile error listing the available candidates. The accepted forms are: `overload function_name(ArgumentType, ...) = constant` `overload function_name(ArgumentType, ...) :: ResultType = constant` `overload function_name(name :: ArgumentType, ...) = constant(name, ...)` The result annotation is optional when the implementation constant determines it. The first overload clause establishes a callable function name; no separate declaration is required: `overload map(?a -> ?b, List.of(?a)) = list_map` `overload empty() = nil` `function mapped_empty(f :: Nat -> Nat) :: List.of(Nat):` `map(f, empty())` The outer expected `List.of(Nat)` result selects `map`’s clause; its selected argument signature then supplies the expected type that selects `empty`. A bare implementation constant receives arguments in signature order. When its parameter order differs, name the signature arguments and write a call template: `notation (element in collection):` `~order: hol_relation` `member(element, collection)` `overload member(` `element :: ?a,` `collection :: ?a -> Boolean` `) = set_member(collection, element)` `overload greater(` `left :: Integer,` `right :: Integer` `) = int_lt(right, left)` Thus `x in s` lowers to `set_member(s, x)`, while `x > y` lowers to `int_lt(y, x)`. A template must use every overload argument exactly once. Zero-argument overloaded functions may use the expected result type for contextual selection, so nested calls such as `map(f, empty())` resolve statically. ### 2.7. Executable automata The standard automata library has one representation for each kind of automaton, and every automaton operation is declared with function so that it has both a logical meaning and ordinary run-time code. `DFA.of(?q, ?a)`, constructed by `dfa`, stores one initial state, a transition function, and a final-state predicate. `dfa_run` follows the transition function over a `List.of(?a)`, and `dfa_accepts` tests the resulting state. The nondeterministic representations make their finite search space explicit: * `NFA.of(?q, ?a)`, constructed by `nfa`, stores an equality decider (`?q -> ?q -> Boolean`), a `FiniteSet.of(?q)` state universe, an initial `FiniteSet.of(?q)`, a transition predicate \(`?q -> ?a -> ?q -> Boolean`), and a final-state predicate. * `EpsilonNFA.of(?q, ?a)`, constructed by `epsilon_nfa`, stores the same data and an epsilon-transition predicate \(`?q -> ?q -> Boolean`). The NFA operations are `nfa_run`, `nfa_accepts`, and `nfa_determinize`. The epsilon-NFA operations are `epsilon_nfa_closure`, `epsilon_nfa_run`, `epsilon_nfa_accepts`, `epsilon_nfa_eliminate`, and `epsilon_nfa_determinize`. Run and epsilon-closure operations return `FiniteSet.of(?q)`. Epsilon elimination returns `NFA.of(?q, ?a)`. Determinization returns `DFA.of(FiniteSet.of(?q), ?a)`, whose states are finite sets of source states. Every destination search enumerates only the stored universe and uses the stored equality decider for finite-set operations. Epsilon closure is bounded structurally by consuming the universe list as fuel, so it terminates even when epsilon transitions contain cycles. The universe is therefore part of the automaton representation rather than optional metadata. `nfa_determinize_accepts_iff` states that `nfa_accepts` agrees with acceptance by the DFA returned from `nfa_determinize` for every word, and `nfa_determinize_language` gives the corresponding extensional language equality. These theorems are unconditional: NFA acceptance and the subset construction use the same finite-set runner. Likewise, `epsilon_nfa_determinize_accepts_iff` and `epsilon_nfa_determinize_language` are unconditional preservation theorems for `epsilon_nfa_accepts` and the DFA returned by `epsilon_nfa_determinize`. The epsilon-NFA source and the produced DFA share the same bounded closure and subset-construction computation. Finite-universe epsilon elimination additionally has a representation obligation. `epsilon_nfa_well_formed(m)` requires the stored equality decider to agree with logical equality, the initial states to belong to the explicit universe, and the universe to be closed under epsilon and symbol transitions. Under that explicit hypothesis, `epsilon_nfa_eliminate_accepts_iff` proves word-acceptance preservation and `epsilon_nfa_eliminate_language` proves language preservation. No well-formedness premise is required by either determinization theorem, because those theorems compare the executable runners directly. #### 2.7.1. Generic regular expressions Importing `rhombus/hol/stdlib` with open exposes the generic regular-expression library. `Regexp.of(?a)` is an AST over an arbitrary symbol type `?a` with exactly six constructors: * `regexp_none()` accepts no words and `regexp_epsilon()` accepts only the empty word. * `regexp_atom(predicate)` accepts a one-symbol word when its executable `?a -> Boolean` predicate accepts that symbol, so compiled matching remains ordinary run-time code. * `regexp_alternate(left, right)`, `regexp_sequence(left, right)`, and `regexp_star(body)` denote union, concatenation, and Kleene closure. `regexp_literal(decide_equal, value)` is a convenience function that constructs an atom from an executable equality decider; it is not a seventh AST constructor. The inductively defined relation `regexp_accepts(r, word)` gives the language semantics independently of every automaton representation and runner. Its rules give epsilon the empty word, atoms their accepted singleton words, alternation either branch, sequencing the concatenation of two accepted words, and star zero or more accepted body words. The standard library defines `Codepoint` as a nominal wrapper `codepoint(Nat)` and `String` as `text(List.of(Codepoint))`. The public `codepoint_to_nat` operation unwraps it, and curried `codepoint_equal` provides executable equality. The wrapper deliberately accepts every `Nat`; it carries no Unicode scalar-value invariant. Thus `Codepoint` is not interchangeable with `Nat`, and `String` is not interchangeable with `List.of(Codepoint)`, without treating either nominal boundary as validation. `regexp_compile(pattern :: String) :: Option.of(Regexp.of(Codepoint))` parses the standard-library `String` codepoint list into an executable regular-expression AST. Its grammar is: `pattern` `::= ε | alternation` `alternation` `::= concatenation ("|" concatenation)*` `concatenation ::= repetition+` `repetition` `::= atom ("*")?` `atom` `::= literal | "." | "\" codepoint | "(" alternation ")"` `literal` `::= any Unicode codepoint other than |, *, (, ), ., or \` Here `ε` denotes empty input in the start rule, not a pattern codepoint. The compiler unwraps each `Codepoint` with `codepoint_to_nat` to recognize the operators by their ASCII values: `|` is 124, `*` is 42, `(` is 40, `)` is 41, `.` is 46, and backslash is 92. Alternation has the lowest precedence, implicit concatenation the next, and postfix `*` the highest; parentheses group an alternation. Each unescaped literal denotes an atom using executable `codepoint_equal`. `.` denotes an atom whose predicate accepts every codepoint. A backslash makes exactly the next codepoint a literal, including any operator codepoint. The empty entire pattern compiles to `some(regexp_epsilon())`. Every other successful parse consumes the complete input and returns `some(result)`, where `result` is the resulting `Regexp.of(Codepoint)`. Dangling escapes, unmatched parentheses, leading or trailing `|`, empty alternatives or groups, leading or repeated `*`, and any leftover malformed input are rejected with `none()`. Compilation follows the conventional Thompson pipeline `Regexp -> EpsilonNFA -> NFA -> DFA`. `regexp_to_epsilon_nfa` performs Thompson construction, `regexp_to_nfa` eliminates epsilon transitions, and `regexp_to_dfa` determinizes the resulting NFA. `regexp_matches(r, word)` executes the DFA and tests the whole word; it is not a substring search. The principal compiler theorems are `regexp_to_epsilon_nfa_well_formed` and `regexp_to_epsilon_nfa_accepts_iff` for the Thompson result; `regexp_to_nfa_accepts_iff` and `regexp_to_nfa_language` for epsilon elimination; and `regexp_to_dfa_accepts_iff` and `regexp_to_dfa_language` for determinization. The direct semantic correspondences are `regexp_to_nfa_semantics_iff` and `regexp_to_dfa_semantics_iff`. The executable matcher is related to each stage by `regexp_matches_epsilon_nfa_iff`, `regexp_matches_nfa_iff`, and `regexp_matches_dfa_iff`, while `regexp_matches_iff` is the end-to-end correctness theorem `regexp_matches(r, word) <=> regexp_accepts(r, word)`. `regexp_find(r, input)` returns an `Option.of(RegexpMatch)`. `regexp_match(start, end)` constructs a result, and `regexp_match_start` and `regexp_match_end` select its `Nat` offsets. Search is leftmost-longest: it chooses the earliest start having a match, then the greatest accepted end at that start. Ranges are half-open `[start, end)`, measured in input-list elements; `start === end` is a valid zero-width match. `regexp_replace_first(r, replacement, input)` replaces only that leftmost-longest range. `regexp_replace_all(r, replacement, input)` repeats the same search over the unconsumed original input; replacement symbols are never searched. A nonempty match consumes its range. After a zero-width match before EOF, replace-all emits the replacement, copies exactly one original symbol at the match position unchanged, and resumes after that symbol. At a zero-width match at EOF, it emits the replacement once and stops. The four String adapters are `string_regexp_matches`, `string_regexp_find`, `string_regexp_replace_first`, and `string_regexp_replace_all`. They accept `Regexp.of(Codepoint)` and convert strings with `string_to_codepoints` and `string_from_codepoints`. Consequently String search offsets count codepoints, not encoded bytes, and replacement follows exactly the generic list behavior above. ### 2.8. theorem and proof `theorem Id:` `proposition` `proof:` `proof_option` `...` `proof_option = ~induct: [Id, ...]` `| ~split: [proposition, ...]` `| ~choose: [term, ...]` `| ~use: [Id, ...]` `| ~skip: [Id, ...]` `| ~disable: [Id, ...]` `| ~limit: nonnegative_integer` `| ~extensionality: [Id, ...]` `| ~sorry` States a proposition and proves it while the module compiles. The proposition grammar is in Propositions. The proof clause is optional and defaults to the same waterfall automation as an empty option configuration. When present, it must follow its theorem immediately and contain one or more option groups. ```racket theorem app_nil_r: forall (xs :: List.of(?a)): app(xs, Nil()) === xs theorem app_assoc: forall (xs :: List.of(?a), ys :: List.of(?a), zs :: List.of(?a)): app(app(xs, ys), zs) === app(xs, app(ys, zs)) proof: ~induct: [xs] ``` Every theorem is retained by name but is not added to the global rule database. Use a theorem explicitly in a proof with the `~use` option. Adding an unrelated theorem therefore cannot change later automation. Every proof-option keyword may appear at most once. Every bracketed option list must be nonempty, retains its written order, and cannot be continued by repeating the keyword. The `~induct` list gives strict nested induction hints. The first name is consumed when an unresolved branch reaches induction; the remaining names are propagated in order to every generated subgoal. A branch where its next named variable cannot be inducted on is an explicit proof failure. Once all listed names are consumed, the ordinary induction heuristic resumes. `~split` performs its Boolean case splits in list order. `~choose` supplies existential candidates in list order, before the case splits. `~use` names theorems to enable for this proof only, which is useful when a lemma is too aggressive to leave in the rewriter permanently. `~disable` names rules to disable for this proof only. `~skip` names waterfall stages — `simplify`, `eliminate`, `fertilize`, `generalize`, `irrelevance`, `induct` — to skip for this proof only; see The Prover. `~limit` sets this proof’s nonnegative search-step ceiling. None of these options change what the prover is allowed to conclude, only what it tries. `~sorry` is the exception: it skips the proof and admits the proposition as a kernel axiom, which is how an unfinished proof lets later declarations go on. The axiom stays on record in the theory’s axiom list, so a theory built with `~sorry` is visibly not a conservative extension. The other options may stay beside it; they are ignored. The `~extensionality` list names fresh variables for sequential function-extensionality steps. All names are consumed in order before `~choose`, `~split`, or the ordinary waterfall runs. Each step reduces an equality of functions (including `Set` values, which are functions to Boolean) to pointwise equality using the kernel’s derived `EXT` rule, with no new axiom. A non-function equality at any requested step is a compile-time error, not a silent no-op: ```racket theorem funs_equal: double === add_self proof: ~extensionality: [x] ``` ### 2.9. Importing a theory There is no separate form for importing a theory. An ordinary Rhombus import of a `rhombus/hol` module brings both halves: its functions, because that is what an import does, and its theory, so its datatypes, definitions and theorems are available to the prover. ```racket import: "list_proofs.rhm" open ``` A module is recognised as a theory by having one — every `rhombus/hol` module publishes its theory in a hol\_theory submodule — so this is checked, not guessed from the shape of the path. An import of anything else passes through untouched, and one import form may name both: ```racket import: "plain_helper.rhm" open "list_proofs.rhm" open ``` Adoption is transitive: the imported theory already contains whatever it imported in turn, so a dependency does not have to be named again. #### 2.9.1. Ordering Two rules follow from keeping the chain of theories linear. An import of a theory must come before the module’s own logical declarations, and when there is more than one they must be given in dependency order. Adopting a theory that is not an extension of the one already in scope is an error, because a module holding two unrelated theories could not use their theorems together. #### 2.9.2. Forms that cannot be read To find the module path in an import clause, the longest prefix of the clause that parses as one is taken. That covers `"path.rhm"`, lib`("collection/path.rhm")` and collection/path, with any modifiers after them. It does not cover a clause whose path is inside a block, as in import: meta: `"path.rhm"`. Rather than drop such a theory silently, an import that names a theory in a form this version cannot read is an error, and says so. ## 3. Types, Expressions and Propositions ### 3.1. Types `Type = Id` `a declared datatype with no parameters` `| Id.of(Type, ...)` `a declared type constructor, applied` `| ?a` `a type variable` `| Type -> Type` `a function type (right associative)` `| (Type)` `explicit grouping` `| Boolean` `the type of propositions` Type variables are written ?a, ?b and so on. A function is implicitly polymorphic in every type variable it mentions; there is no `forall` at the type level to write. Parameterized datatype declarations bind a constructor namespace: for example, `datatype List.of(?a)` binds `List.of`, and an instance is written `List.of(Nat)`. The bare name `List` is not a type, because its argument is missing. Function arrows associate to the right, so `A -> B -> C` means `A -> (B -> C)`; write `(A -> B) -> C` when the domain is itself a function. Boolean is spelled as Rhombus spells it. A function’s annotations are erased on the way to the executable half, but the conditions of its if forms are not, so the two halves have to agree on what a Boolean is. ### 3.2. Expressions This is the grammar of a function body. HOL expressions use a dedicated, extensible enforestation space; function bodies admit only the pure, total forms below. `body = expr` `the value of the body` `| let Id = expr` `a local definition, then the rest` `body` `| let pattern = expr` `an irrefutable-pattern local definition` `body` `| function Id(arg :: Type, ...) :: Type:` `a named local function,` `body` `then the rest` `body` `| match expr | clause | ...` `refining a parameter or pattern variable` `expr = Id` `a parameter, pattern variable or local` `| Id(expr, ...)` `a constructor, function or named primitive` `| NonnegativeInteger` `a self-typed Nat literal` `| +NonnegativeInteger | -NonnegativeInteger` `a self-typed Integer literal` `| #true | #false | true | false` `| !expr` `| expr && expr` `| expr || expr` `| expr == expr` `| -expr` `overloadable negate for a nonliteral operand` `| expr ** expr` `| expr * expr` `| expr + expr | expr - expr` `| expr ++ expr` `| expr in expr` `| expr union expr` `| expr intersect expr` `| expr < expr | expr <= expr | expr > expr | expr >= expr` `| if expr | expr | expr` `| cond-expr` `| expr notation-op expr` `| expr :: Type` `an expected-type ascription` `| function (arg :: Type, ...) :: Type: body` `an anonymous function` `| function | (pattern, ...): body | ...` `a case-clause function` `| block: body` `an ordinary expression built from a body` `| (expr)` `cond-expr = cond` `| expr: expr` `| ...` `| ~else: expr` `clause = CtorId(Id, ...): body` `| CtorId: body` `row = (pattern, ...): body` `on the declaration, one per argument` `| pattern: body` `at one argument, parentheses optional` let and match are forms of a ​_body_​, not of an expression: a let is a statement followed by the rest of the body, and there is no let inside the operand of a &&. That is not a notational choice — it is what the elaborator accepts. cond tests its guards from top to bottom and returns the body of the first true guard. A final `~else` clause is mandatory and must be last: ```racket function pick(b :: Boolean, x :: Nat, y :: Nat) :: Nat: cond | b: x | ~else: y ``` Both the executable and logical readings lower this form to right-nested if expressions. Guards and clause results are expressions, not full bodies, so a clause cannot contain a local let or match. The built-in operators mean in the logic what they mean in Rhombus: `#true` and `#false` are the truth values, ! is negation, && and || are conjunction and disjunction, and == is equality at any type. Arithmetic, append, membership, and set operators lower to ordinary named calls: `add`, `subtract`, `negate`, `multiply`, `power`, `less`, `less_equal`, `greater`, `greater_equal`, `append`, `member`, `union`, and `intersection`. The elaborator resolves each named call directly or through the overload clauses imported with the current theory. There is no runtime type switch and no implicit numeric coercion: the complete argument tuple and, when available, the expected result type must select one non-overlapping clause. notation adds a spelling to the HOL expression space. Operator-style cases accept the closed HOL pattern grammar and are tried in source order within each fixity. Arbitrary operands are evaluated once before dispatch; the resulting matrix must be exhaustive, every row reachable, and each operand column statically homogeneous. Shared or case-local result annotations are HOL type constraints, not dynamic checks or converters. && and || short-circuit when the module runs, while the logical `and` and `or` are strict. Nothing can tell the difference, because every function in this grammar is total. Anything outside the grammar is a compile error that names the offending expression. A string literal is admitted as an expression and pattern. It desugars to `text` applied to a `List.of(Codepoint)`, with each source Unicode scalar represented as `codepoint(n)`, where `n` is the corresponding surface numeral. The declarations providing `Nat`, `Codepoint`, `List.of(?a)`, and `text` determine the logical and executable meanings; see "Matching" below. #### 3.2.1. Numerals At the surface, a bare nonnegative decimal `n` is a `Nat` literal. The forms `+n` and `-n` are `Integer` literals; `+0` and `-0` both denote integer zero. Prefix `+` exists only on a bare decimal literal. Unary `-` applied to a nonliteral expression remains the ordinary overloadable `negate` operator. The normalized frontend retains only `CoreNatLit(value :: NonnegInt, at)` as a numeric literal node. Surface normalization directly encodes `+n` as `CoreCall(CoreGlobalRef(int_nonnegative), [CoreNatLit(n)])`; `-n` uses the same ordinary call shape with `int_negative` and magnitude `n - 1`. Thus `CoreNatLit(n)` becomes the Nat-only checked form `CheckedNumeral(n :: NonnegInt, at)`, while an integer literal follows the same checked constant-resolution and type-checking path as other object-language applications. Its resulting `Integer` type is unified with the expected type. Both `+0` and `-0` normalize through `int_nonnegative(0)`. For the exact reserved declaration `datatype Nat | zero() | succ(pred :: Nat)`, a `CheckedNumeral` has two compact readings: logical elaboration calls `mk_nat_lit` to produce the kernel term `NatLit(n)`, while executable emission produces the host `Nat`/`NonnegInt` integer `n`. The backends therefore handle only Nat numerals. Integer literals reach them as ordinary checked `int_nonnegative` or `int_negative` constructor applications around the Nat literal, so neither backend branches on a signed numeral and `Integer` does not acquire a host-integer representation. For this reserved `Nat` only, executable `zero()` is `0`, and executable `succ(n)` is `n + 1`. A runtime `zero()` pattern tests for zero. A runtime `succ(p)` pattern accepts a positive integer and binds `p` to its predecessor. Functions can therefore retain the ordinary constructor expression and pattern interface without allocating Peano constructor chains. Other datatype declarations still emit one Rhombus class per constructor. These host operations implement only the executable reading; they neither prove a HOL equation nor authorize a kernel result. Logically, the reserved `Nat`, `zero`, and `succ` retain their ordinary datatype meaning, constructor equations, distinctness, injectivity, cases, and induction theorems. The kernel represents a logical numeral with its native `NatLit(n)` term, whose payload is a host nonnegative integer and whose size is independent of its value. `NatLit` is not a new logical constant or axiom. The kernel alone may reveal one logical constructor step: `NatLit(0)` `= zero()` `NatLit(n + 1) = succ(NatLit(n))` Consequently, logical functions that match `zero()` and `succ(k)` retain their ordinary Peano equations. Closed kernel equality and arithmetic use checked conversions instead of first constructing a successor chain. Every conversion returns a theorem checked by the kernel; no theorem is accepted merely because host arithmetic produced the same numeric result. A bare surface `Nat` literal pattern has the same split. Its logical reading is an atomic `NatLit` discrimination, while its executable reading compares the host nonnegative integer with `n`; neither expands to `succ(...succ(zero())...)`. Signed integer literals are not patterns. An expected type checks, but cannot select or convert, a literal’s fixed type. Thus `10 :: Integer`, `+10 :: Nat`, and passing `10` to an `Integer` parameter are errors. There are no implicit numeric coercions. `Rational` has no literal form or fraction syntax; a whole rational is written explicitly as `rational_from_integer(+n)` or with the appropriate constructor/API. #### 3.2.2. Local definitions A let is ​_substituted_​ in the logical reading: the equation is about the value, and it mentions the initializer only where the body reads the variable. ```racket function unread(n :: Nat) :: Nat: match n | zero(): zero() | succ(k): let ignored = unread(k) succ(zero()) ``` states `unread(succ(k)) === succ(zero)`, with no unread on the right. The compiled program still evaluates the initializer, though, so termination is checked against ​_both_​ readings: the call above has to descend even though the equation does not mention it, and one that does not is refused. See What Is Assumed for why the two readings are kept apart. #### 3.2.3. Matching A body may be a match on one of the parameters, and each clause body may itself be a match on a ​_different_​ parameter. The nesting is flattened into a pattern matrix, which is what lets a definition descend on more than one argument. ```racket function ack(m :: Nat, n :: Nat) :: Nat: match m | zero(): succ(n) | succ(p): match n | zero(): ack(p, succ(zero())) | succ(q): ack(p, ack(succ(p), q)) ``` The matrix must cover the product of the matched columns. It may overlap: clauses are ​_ordered_​, and where several match the earliest wins — the same reading the match this compiles to gives the same text. What is refused is a clause no argument shape can reach, since that is a mistake however the clauses are arranged. `_` stands for a position the clause does not name. It may appear inside a pattern (`Cons(x, _)`) or as a whole clause head (`| _: ...`), which is how a catch-all after a specific case is written. A pattern position may also be a bracket list pattern (`[]`, `[x]`, `[x, y, & rest]`), which desugars to nested `cons`/`nil` constructor patterns over whatever datatype provides them — the pattern counterpart of a bracket list literal expression. A nonnegative numeral is an atomic native `Nat` discrimination. It is compatible with ordinary `zero()` and `succ(k)` patterns, but never desugars to a successor chain. A pair pattern (`Pair(x, y)`) matches the language’s one product type. A `#true` or `#false` pattern matches `Boolean`. The kernel’s `bool` is a primitive type rather than a declaration, so the facts the pattern compiler needs — two nullary constructors, their distinctness, cases and induction — are derived from `BOOL_CASES_AX` and installed with the base theory; no axiom is added. Totality is then checked as for any other datatype, so `| #true: ...` alone is a missing case, not a fallthrough. A `String` literal pattern is the ordinary constructor pattern `text(cons(codepoint, ... nil()))`. Each codepoint uses the atomic native numeral-pattern rule, so empty, ASCII, and non-ASCII literals have the same shape complexity per source scalar and obey the normal ordered reachability and exhaustiveness rules. #### 3.2.4. Clauses on the declaration The same matrix may be written on the declaration itself, one row of patterns per clause covering every argument, which is how Rhombus’s own multi-case fun is written: ```racket function app(xs :: List.of(?a), ys :: List.of(?a)) :: List.of(?a) | (Nil(), ys): ys | (Cons(x, rest), ys): Cons(x, app(rest, ys)) ``` A row must have one pattern per argument; at one argument the parentheses may be dropped, exactly as a one-argument match clause drops them. The patterns are the same patterns, so nesting, `_` and the ordering above all read the same way here, and a row may constrain every column at once — which a nested match cannot say in a single clause: ```racket function eq2(m :: Nat, n :: Nat) :: Nat | (zero(), zero()): zero() | (succ(a), succ(b)): succ(eq2(a, b)) | (_, _): zero() ``` This is sugar in the strict sense: a row refines the same pattern vector the nested form refines, so nothing downstream — the decision tree, coverage, termination, the `WFREC` derivation — can tell which form was written. The executable half becomes a multi-case fun over the same patterns, so the first matching clause wins on both sides. A definition’s equations are stated at the shapes each clause actually ​_wins_​ at, not at its pattern as written — `| zero(): a | _: b` gives `f(zero) === a` and `f(succ(k)) === b`, never the inconsistent pair `f(zero) === a` and `forall n: f(n) === b`. A pattern may nest to any depth: `Cons(x, Cons(y, rest))` is a pattern, written directly in a clause head, or built the same way one level at a time via a nested match on an already-bound variable — `match xs | Cons(x, rest): match rest | Nil(): ...` refines the tail `Cons(x, rest)` already bound. A match on anything else — a computed value, a let binding, or an argument an enclosing match already refined, which there denotes the value its pattern matched — is an ordinary match expression. ### 3.3. Propositions This is the grammar of a theorem statement. It is enforested in the same dedicated HOL expression space as function expressions, with a different admissibility policy. `prop = expr` `| not prop` `| prop and prop` `| prop or prop` `| prop ==> prop` `| prop <=> prop` `| prop === prop` `| forall (Id :: Type, ...): prop` `| exists (Id :: Type, ...): prop` `| exists1 (Id :: Type): prop` `exactly one binder` `| select (Id :: Type): prop` `exactly one binder` `| Set{}` `the canonical empty set` `| Set{expr, ...}` `an extensional set literal` `| Set{Id :: Type | prop}` `a set comprehension` `| if prop | prop | prop` `| cond-prop` `| prop notation-op prop` `| (prop)` `cond-prop = cond` `| prop: prop` `| ...` `| ~else: prop` A proposition is never emitted as Rhombus, so it uses the logical spellings: `and`, `or`, `not`, `===` for equality, `==>` for implication and `<=>` for equivalence. (Equality and equivalence are the same relation; the two spellings differ only in precedence, so that an equivalence between equations reads without parentheses.) The same cond form is available in a proposition, with proposition guards and results and the same mandatory final `~else`. #### 3.3.1. Named logical constants Of the base theory’s constants, only `true` and `false` are names. Equality, the connectives, unique existence, and choice are reached only through their syntax (`===`, `and`, `exists1 (x :: T): p`, and so on): `p and q` has no second spelling `conj(p, q)`. The base theory’s remaining constants, such as well-foundedness, cannot be named at all. The logic’s own vocabulary (`eq`, `imp`, `conj`, `disj`, `neg`, `forall`, `exists`, `exists1`, `select`, `cond`, `wf`) is reserved, so declaring one of those names is an error; the constants the implementation builds for itself have names containing `’`, which no identifier can spell. `true`, `false`, equality, and the connectives other than implication have both logical and executable readings, so they may appear in a function body. Implication, exists1, and select are logic-only: use them in theorem statements, not in a function. #### 3.3.2. Quantifier and choice binders, and `Set` values exists1 and select also have dedicated binder forms, parallel to forall and exists, taking exactly one binder (unlike forall/exists, which take one or more): ```racket theorem unique_zero: exists1 (x :: Nat): x === zero() theorem pick_zero: (select (x :: Nat): x === zero()) === zero() ``` Each desugars to the named kernel constant applied to an anonymous function: `exists1 (x :: T): p` is `exists1(function (x :: T): p)`, and likewise for select. Supplying more than one binder is a compile-time error, since `exists1`/`select` generalize no further than a single witness. A binder’s type may be omitted and inferred from how the bound variable is used in the body, exactly like a forall/exists binder. A `Set` value is an ordinary predicate (`?a -> Boolean`), not a distinct builtin set type: `Set{}` is the predicate that rejects every element, `Set{e, ...}` is the extensional disjunction-of-equalities predicate over its listed elements, and `Set{x :: T | prop}` (binder type optional, same inference rule) is the predicate `function (x :: T) :: Boolean: prop`. All three are applied directly as a function to test membership. Two sets built from different literal descriptions are proved equal the same way two functions are: see `~extensionality` in Declarations. Because they assert existence or uniqueness without computing a witness, exists, exists1, and select have no executable reading: they may appear in a theorem statement but not in a function body. A `Set` comprehension’s own body, and forall, are ordinary predicates and follow the same executability rule as any other expression they are built from. #### 3.3.3. Precedence Strongest first. `**`, `++`, and `==>` are right-associative. Arithmetic multiplication, addition, set intersection, set union, conjunction, and disjunction associate to the left. Relations and equality are non-associative, so chains such as `a < b < c` and `a === b === c` are syntax errors. **order** **proposition** **expression** `hol_application` named application named application `hol_power` `**` `**` `hol_prefix_arithmetic` `-x` `-x` `hol_multiplication` `*` `*` `hol_addition` `+ -` `+ -` `hol_append` `++` `++` `hol_set_intersection` `intersect` `intersect` `hol_set_union` `union` `union` `hol_relation` `< <= > >= in` `< <= > >= in` `hol_equality` `===` `==` `hol_negation` `not` `!` `hol_conjunction` `and` `&&` `hol_disjunction` `or` `||` `hol_implication` `==>` (right) `hol_equivalence` `<=>` A quantifier extends as far to the right as it can, so ```racket forall (xs :: List.of(?a)): app(xs, Nil()) === xs and rev(xs) === rev(xs) ``` quantifies over the whole conjunction. These levels govern frontend notation-aware rendering. The kernel printer is canonical and prints selected implementation constants as applications such as `nat_add(x, y)`; the frontend surface printer reconstructs notation only when it is given explicit overload and notation tables. ## 4. Termination A recursive definition is admitted only once it has been shown to terminate. This is not a style rule. The clausal equations of a non-terminating definition are inconsistent — `f(x) = f(x) + 1` proves `0 = 1` — so the check is what makes a definition a conservative extension rather than an axiom. Two methods are tried, in this order. ### 4.1. Lexicographic structural descent The first method is syntactic and generates nothing to prove. It looks for an order of argument positions such that every recursive call leaves some prefix of them unchanged and shrinks the next one to a proper constructor subterm of its pattern. Descending on a single argument is the one-element case: ```racket function app(xs :: List.of(?a), ys :: List.of(?a)) :: List.of(?a): match xs | Nil(): ys | Cons(x, rest): Cons(x, app(rest, ys)) ``` rest is a field of the pattern Cons`(`x, rest`)`, so column xs descends at the only recursive call, and the order is just xs. Ackermann’s function needs two: ```racket function ack(m :: Nat, n :: Nat) :: Nat: match m | zero(): succ(n) | succ(p): match n | zero(): ack(p, succ(zero())) | succ(q): ack(p, ack(succ(p), q)) ``` No single argument decreases at every call — the inner call holds m and shrinks n — but the order m, n settles all three calls. The search is greedy, and that is not an approximation: a column that is admissible at one step stays admissible, and taking it can only discharge call sites, so if any order works the greedy one does. The recorded order contains only the columns needed to settle the calls. Separately, the prover records every position that descends at every call as an induction hint; those extra positions improve induction without widening the well-founded order. "Proper constructor subterm" may be reached through any number of recursive fields of the same datatype. A nested pattern variable is therefore a proper subterm exactly when the datatype’s generated `T_lt` relation connects it to the original pattern. Fields of other types do not count. ### 4.2. Measures When no structural order exists, an adjacent proof block may supply one with `~measure: expression`. ```racket function down(n :: Nat) :: Nat: if nul(n) | zero() | succ(down(pred_of(n))) proof: ~measure: n ``` The recursion here is on a computed argument, not on a field of a pattern, so the syntactic check cannot see it. The measure says that n gets smaller anyway. Each recursive call raises one obligation: the measure of the arguments is below the measure of the patterns, under the branch conditions that reach the call. The obligation above is `forall (x :: Nat): not nul(x) ==> Nat_lt(pred_of(x), x)` and it goes through the same prover as a theorem, with everything declared so far available. Note the guard: a call inside the false branch of an if only has to decrease when that branch is taken, which is most of what a measure is for. If an obligation cannot be discharged, the definition is a compile error carrying the obligation and the goals that were left over. A measure is examined only when no structural order was found. Adding a `~measure:` option to a definition that already descends structurally is therefore harmless but also unchecked — the structural argument is complete on its own. ### 4.3. The subterm relation A measure has to decrease in ​_something_​, and that something has to be well-founded. Every recursive datatype declaration generates its _subterm relation_, named by appending `_lt` to the type’s name: ```racket datatype Nat | zero() | succ(pred :: Nat) ``` brings Nat\_lt into the theory, defined by `Nat_lt(x, zero) <=> false` `Nat_lt(x, succ(y)) <=> x === y or Nat_lt(x, y)` which is exactly `<`. For a branching type both children count: `Tree_lt(x, Node(l, v, r))` `<=> x === l or (Tree_lt(x, l) or (x === r or Tree_lt(x, r)))` Two things make this the right order to measure into. It is ​_derived, not postulated_​, and in a stronger sense than "installed through a definitional seam": the relation is `TC(Nat_child)`, the transitive closure of a direct-child predicate written with the datatype’s own discriminators and selectors. Neither the closure nor the child predicate recurses, so neither needs a recursion theorem, and the equations above are ​_proved_​ from the closure’s induction principle rather than asserted. And it is ​_well-founded by the datatype’s own induction principle_​: a descending chain would be an infinitely deep term, and induction says there are none. That is why a measure must land in a declared datatype. A measure into Boolean, or into any type with no subterm relation, is rejected. The relation’s equations are in the rewriter under its own name, so a proof can suppress them with `~disable`: `[`Nat\_lt`]` without touching the datatype’s other rules. ### 4.4. A family of functions A `function.together:` family is checked as the one tagged function its members are read as, so it uses this same machinery: one order spans the family, because a recursive call leaves the member that made it. Either every member supplies a `~measure:` landing in one declared datatype, or the family descends structurally — one argument column per member, at a common recursive datatype. A `datatype.together:` family’s union type is such a datatype, and it is what relates values of different members, so a recursion that crosses between mutually recursive datatypes descends in it. A branch condition that calls the function being defined is not among an obligation’s assumptions: the function has no equations yet, so the call has to descend whichever way that branch went. ### 4.5. What is not supported * **Nested recursion.** A recursive call among the arguments of another recursive call has no obligation this version can state, because the obligation would mention the function being defined. * **Recursion under a binder.** A local or anonymous function inside a recursive definition’s body is an ordinary non-recursive lambda (Local and anonymous function): it has no binding of its own name, and a call from inside it back to the enclosing definition currently being checked is a recursive call reached through that lambda’s binder. The checker walks into every `Abs` node of the elaborated term, so this is caught and reported the same way any other unstated recursive call is, not silently accepted. ## 5. The Prover Proofs are found by a _waterfall_, in the ACL2 sense: a fixed pipeline of stages, each of which either makes progress on a goal or passes it down. A stage that makes progress sends its subgoals back to the top. A goal that falls off the bottom is left open, and the record of what was tried becomes the error message. `simplification -> destructor elimination -> fertilization ->` `generalization -> elimination of irrelevance -> induction` There is no search and no backtracking. The prover is a function of the goal and the rule database, which is what makes a failure reproducible and a successful proof stable when an unrelated theorem is added elsewhere. ### 5.1. Simplification The goal is rewritten to a normal form with every enabled rule: the equations of every declared function, the injectivity, distinctness, discriminator and selector equations of every datatype, the product projections \(`fst(Pair(x, y)) === x` and its dual), proof-local theorems selected by `~use`: `[`theorem`]`, and the goal’s own assumptions. A rule is indexed by its left-hand side, so an equation’s two orientations are two different rules. A datatype derives each distinctness fact in one orientation — `not (zero === succ(x))` — and that says nothing about the phrase `succ(zero) === zero`, so the database is given the symmetric form of each as well. Neither can loop: both rewrite an equation to `false`. The rewritten goal is then beta-normalized. A rewrite rule is indexed by the head constant of its left-hand side, and a beta redex — a function expression applied to an argument — has no head constant, so no rule can ever match one. Anonymous and local functions, an expression-position let, exists1, select and a Set comprehension all elaborate to exactly that shape, and unfolding an ordinary function whose argument is one creates further redexes, so the two passes alternate until neither applies. Beta conversion is applied to the goal the waterfall holds, not inside the rewriter, which is what keeps it away from the equations of a recursive definition: there a redex is the folded recursive call, and reducing it would expose the `WFREC` encoding instead. The assumptions are simplified too, not merely used as rules. An assumption is only a rule for the conclusion, which says nothing when the assumption is `not nul(zero)`: as a rule it rewrites a phrase that does not occur. Reduced it is `false`, and the goal is closed whatever its conclusion. Guarded recursion produces exactly that shape, so measure obligations depend on it. A rule whose two sides are permutations of each other — commutativity, say — is applied in one direction only, ordered by a term ordering, so it cannot oscillate. ### 5.2. Destructor elimination A goal that talks about a value through its selectors is rewritten to talk about its constructor instead: knowing `is_Cons(xs)`, the goal is restated with `xs` replaced by `Cons(Cons_head(xs), Cons_tail(xs))`. This is what lets simplification proceed on a variable whose shape is known but not written. ### 5.3. Fertilization An assumption of the shape `x === t` or `t === x`, with `x` a variable that does not occur in `t`, lets every occurrence of `x` in the conclusion be rewritten to `t`. Its usual source is an induction hypothesis freshly exposed by the previous case split, of exactly that shape. The hypothesis a fertilization step used is dropped from the resulting subgoal’s own assumption list, so a given equation is used at most once along one branch. Two equations can otherwise be cyclic — `x === f(y)` and `y === g(x)` each pass the occurs check alone, but eliminating `x` can reintroduce `y`, whose own equation reintroduces `x` — and without this, the two would toggle the goal back and forth forever instead of ever reaching the bottom of the pipeline. ### 5.4. Generalization A subterm that appears on both sides of the goal and is not a constructor application is replaced by a fresh variable. This throws information away, and it is what makes induction hypotheses strong enough to be useful. Only saturated application spines are candidates, and function-typed terms never are: generalizing a partial application produces a goal that is not just weaker but false. ### 5.5. Elimination of irrelevance A hypothesis that shares no variable, even transitively through other kept hypotheses, with anything the conclusion needs is dropped before induction is attempted. Such a hypothesis cannot help prove the conclusion, and keeping it around can only confuse the heuristics that come after — most often the choice of induction variable. Dropping it needs no proof step: a theorem proved from fewer assumptions is already usable wherever more are available, so the subgoal’s proof, unchanged, is the parent goal’s proof too. ### 5.6. Induction A variable of a declared datatype is chosen and the goal is split into one case per constructor, with an induction hypothesis for each recursive field. The heuristic chooses a variable from the argument positions the functions in the goal actually recurse on — the same information the termination checker produced, so the prover inducts the way the definitions recurse. A nonempty `~induct`: `[`first, next, ...`]` list overrides that choice with strict, ordered nested hints. Each induction consumes one name on every unresolved branch and propagates the remaining names to all generated subgoals; a branch where its next hint cannot apply fails explicitly. The heuristic resumes after the list is exhausted. Nested induction is bounded at depth six. That constant is not a tuning budget; it is what makes the driver a function rather than a search. Induction introduces fresh variables of the same type, so without a bound the prover would induct forever. ### 5.7. When a proof fails The residue is the goals left open, each with the trail of stages that produced it: `theorem: rev_is_identity: could not prove.` `Remaining goal,` `after` `induction on xs (case Cons)` `simplification` `induction on y (case Cons)` `simplification` `assuming rev(y) === y` `assuming app(z, Cons(x, Nil)) === Cons(x, z)` `y === x and x === y` The trail is usually enough to say what happened. Here it says the conjecture is false rather than unproved: the prover got down to `y === x and x === y` for arbitrary distinct `x` and `y`, which no lemma will close. When a goal is instead a true statement the prover could not reach — an instance of associativity, say — the fix is to prove that statement as its own theorem and select it explicitly with `~use`: `[`associativity`]`. The things to reach for, in order: prove the missing theorem and select it with `~use`; give `~induct`: `[`variable`]` when the prover picked the wrong variable (or list several variables for strict nested induction); give `~use`: `[`lemma`]` when an existing theorem is needed here; give `~disable`: `[`rule`]` — ACL2’s `:in-theory (disable ...)` — to turn off a named rewrite rule for this proof when an enabled rule is firing where it should not; give `~split`: `[`proposition`]` — ACL2’s `:cases` — when the goal turns on a Boolean term (typically an application of an uninterpreted or externally-supplied predicate) that no other stage can resolve, to split on it up front and let each branch reach its own conclusion with that term’s truth value as a hypothesis; give `~skip`: `[`stage`]` — ACL2’s `:do-not` — to turn off one of `simplify`, `eliminate`, `fertilize`, `generalize`, `irrelevance` or `induct` for this proof only, on the rare occasion a stage’s heuristic is actively getting in the way. Each proof-option keyword occurs at most once, and every list is nonempty and retains source order. None of these can turn a false conjecture true or a wrong proof into a right one: a bad choice of any of them just changes what the residue looks like. ### 5.8. Justification No stage can produce a theorem. Each hands back its subgoals together with a function that builds a theorem for the goal out of theorems for the subgoals, and those functions are composed only when every leaf is closed. The only theorems that exist are the ones the kernel made, so a bug in a stage can make the prover fail to find a proof, or find an unnecessary one, but cannot make it report a proof that does not exist. Logical `Goal` values contain only assumptions and a conclusion. Stages attach a typed trace event to each subgoal they produce; search extends an explicit trace path with that event on the way into the subgoal, and snapshots the path into a `Residue` only where a goal is left open. Terms and symbols are converted to display strings only when the residue message is rendered. There is no proof tree built first and executed second. A `Step`’s justification function is composed directly into the search that produced it, the moment every one of its subgoals has come back with a real theorem; if any subgoal is left stuck instead, the justification is never called, and the residues of every subgoal that never resolved are returned in its place. The theorem the waterfall returns is therefore built by that composition as search proceeds, not read back afterward off some separate executed structure. ## 6. What Is Assumed A proof assistant is only worth what its trusted base is worth. This section says what that base is, and where it leaks. ### 6.1. The kernel Theorems are values of an opaque type. There is no public constructor, no reflection into one, and no serialised form, so the only way to obtain a theorem is to have the kernel make it. Everything above the kernel — derived rules, conversions, the rewriter, the whole waterfall — can only assemble calls to it. A bug up there costs a proof, not soundness. The kernel provides ten primitive inference rules, following HOL Light: `REFL`, `TRANS`, `MK_COMB`, `ABS`, `BETA`, `ASSUME`, `EQ_MP`, `DEDUCT_ANTISYM_RULE`, `INST` and `INST_TYPE`. Terms are locally nameless, so alpha-equivalence is structural equality and there is no alpha-conversion to get wrong. ### 6.2. Alignment with HOL Light’s `fusion.ml` The kernel’s public surface is deliberately close to HOL Light’s, close enough that reading `fusion.ml` is a reasonable way to predict what this kernel does before reading it. Three differences, and why each one is there: * **`BETA` takes an arbitrary redex**, not only the trivial `(fun x: t(x))(x) === t(x)`. HOL Light’s primitive `BETA` is deliberately the trivial case only; general beta conversion is a derived rule built on top of it. Terms here are locally nameless, so substitution cannot capture, and admitting the general case as primitive costs nothing in soundness — it is exactly as easy to state and check as the trivial case. Taking the general case as primitive removes one derived-rule layer \(`BETA_CONV` composed with a substitution argument) that would otherwise exist purely to work around named bound variables, which this representation does not have. * **`Thm` carries a `Stamp`**, not a bare theory reference. HOL Light’s kernel has a single global, mutably-extended theory, so a theorem needs no lineage tag to know what it can be combined with. This kernel’s theories are immutable values (see the section on theories below, needed because `raco make` compiles many modules in one process and a single mutable global would make one module’s declarations leak into another’s), so a rule combining two theorems has to check they come from one line of extension. The ten rules’ ​_content_​ is unchanged; the stamp check is bookkeeping the mutable-theory design does not need. * **Two extra polymorphic definitional principles** beyond the eight HOL Light exposes as primitive-adjacent (`new_constant`, `new_axiom`, `new_basic_definition`): `new_type` and `new_basic_type_definition` are named the same as HOL Light’s and do the same thing (the latter is the one genuinely conservative type-formation principle, carving a new type out of a nonempty predicate on an existing one). Nothing here is additional trust; it is the same principle under the same name. Everything else — the argument order, the error conditions each rule checks, and the set of ten primitive rules itself \(`REFL`/`TRANS`/`MK_COMB`/`ABS`/`BETA`/`ASSUME`/`EQ_MP`/ `DEDUCT_ANTISYM_RULE`/`INST`/`INST_TYPE`) — matches `fusion.ml` rule for rule. Type unification (used only by the elaborator, never by a proof step), pretty printing, and the compile-time trace log used by the independent Idris differential checker are not part of this comparison: none of the three exists in `fusion.ml` either, and none of the three is one of the ten rules or a definitional principle — printing lives beside the kernel only because `check_term`’s error messages need it; moving it would create a circular import. Type unification was already moved out to the elaborator (`rhombus-hol-prover/rhombus/hol/backend/proof/elaborate.rhm`) before this section was written. ### 6.3. The axioms Four: * **ETA** — `(fun x: f(x)) === f` * **SELECT** — the choice operator returns a witness when one exists * **BOOL\_CASES** — `(t <=> true) or (t <=> false)` * _axiom of infinity_ — there is an injection from the type `ind` into itself that is not onto The first three follow HOL4. BOOL\_CASES is derivable from choice and eta, but taking it directly saves a long stretch of derived-rule scripting and costs nothing in confidence — it is a standard consistent basis. Infinity is there because ​_recursive_​ datatypes are derived rather than postulated, and the construction needs an infinite type to index the trees it carves them out of. It is stated once, in the base theory, and shared: a module declaring ten recursive datatypes assumes it exactly as often as a module declaring none. Non-recursive datatypes do not touch it — they are built from `unit`, `prod` and `sum` over their field types — but they are in the same theory, so it is present either way. That trade is the point. The alternative, and what this system did before, was to assume no infinity and instead postulate every recursive datatype’s characterisation: injectivity, distinctness, exhaustiveness and induction, per declaration. One shared axiom replaced an unbounded number of per-declaration ones. Every logical connective is ​_defined_​ on top of the kernel’s equality, not postulated. So are the conditional rules `if true | a | b === a` and its dual, and the thirteen propositional simplification rules. A datatype’s subterm relation `T_lt` is derived twice over, and both halves matter because so much rests on them. That `T_lt` is ​_well founded_​ is proved from the datatype’s own induction principle \(`prove_wf_t_lt`); it is what every derived recursive function recurses in. That `T_lt` ​_is_​ the subterm relation — its constructor equations, one per constructor — is proved as well: the relation is defined as `TC T_child`, the transitive closure of a direct-child predicate spelled with the datatype’s own discriminators and selectors, so neither the closure nor the child predicate is a recursive definition and neither needs a recursion theorem. The equations then follow from the closure’s induction principle \(`rhombus/hol/backend/proof/definition/function/transitive_closure`). ### 6.4. What is postulated beyond that Nothing. Both kinds of datatype, the subterm relation each brings, and every function are proved; a definition this version cannot derive is refused rather than assumed. You do not have to count, though, because the compiler does. Every declaration that takes a derived path checks that the theory it produced has the same number of axioms as the theory it started from, and refuses the declaration otherwise. So "derived" is an invariant rather than a claim: a path that quietly began postulating — which is a way this has actually broken before — fails at the declaration that did it, naming it. **Datatypes.** A datatype declaration is ​_derived_​, whether recursive or not. A non-recursive one — any number of constructors, fields and type parameters — is built as a sum of products of `unit` over its field types. A ​_self-recursive_​ one is carved out of the labelled trees over `num` (`rhombus/hol/backend/proof/definition/datatype/tree`, `rhombus/hol/backend/proof/definition/datatype/recursion`): its representation is the least set of trees closed under its constructors, cut out by `new_basic_type_definition`, and its injectivity, distinctness, exhaustiveness, induction, discriminators, selectors and destructor elimination all come out as theorems with no hypotheses. Run the axiom schema on the same declaration and every statement agrees — the same theory, reached by proof. What a self-recursive declaration still costs is one thing: the axiom of infinity, which the base theory carries once however many datatypes a module declares, because the trees are indexed by paths over `num`. So a module declaring two recursive datatypes assumes four things — the base logic’s three and infinity — and declaring a third would not move that number. There is no third case and no fallback: a field either is the type itself or it is not, so the axiom schema is no longer on the declaration path at all. It survives only as the baseline the derivations are differentially tested against. The _strict positivity_ check still guards the declaration, but it no longer guards a consistency claim about axioms nobody proved — an ill-founded declaration now fails to be carved rather than being assumed. **Function definitions.** A function that does not call itself is ​_defined_​, whatever its patterns look like: its decision tree is written as a closed term with the datatype’s discriminators for the tests and its selectors for the variables, new\_basic\_definition takes that, and the clausal equations — one per leaf, so that ordered clauses resolve the way they were written — are proved by unfolding it. A function that does recurse is ​_derived_​: its clausal equations are proved from a well-founded recursion theorem (itself derived, not postulated) applied to a step function compiled from the same decision tree. The order it recurses in is built from the descent the termination check found — one column’s subterm relation, the lexicographic product of several columns’ when no single one shrinks everywhere (Ackermann’s), or the measure’s result type’s pulled back along the measure. Several arguments are derived over their tuple; patterns may nest to any depth; the types the order compares in may be any instance of a datatype declared here, `List.of(Nat)` as much as `List.of(?a)`. **An ordinary function never adds an axiom.** If the recursion has no order this version can build, the declaration is ​_refused_​, naming which of the possible reasons applies, and the theory is left as it was. This is checked and not merely intended: each derived declaration compares the axioms of the theory it produced against the theory it was given, checks that the second extends the first, and checks that every equation it registered is hypothesis-free and belongs to that theory. None of these derivations change the statements consumed downstream, so the rule database, the waterfall, and match compilation are unaffected by how those statements were proved. **Numerals.** A compact `NatLit(n)` is an Isabelle-verified kernel term form for the ordinary Peano value `n`; it is neither an object-language constant nor an axiom. The native Nat extension conservatively installs the reserved `Nat`, `zero`, and `succ` objects and returns their zero/successor distinctness, successor injectivity, and induction theorems. Native numeral conversions are trusted only through their proved Isabelle implementation and checked theorem output. One conversion exposes `NatLit(0) = zero()` or `NatLit(n+1) = succ(NatLit(n))`; equality and arithmetic conversions produce Boolean equations. The Rhombus façade validates term shape, theory provenance, and stamps before exposing a `Thm`. Host arithmetic therefore never enters the prover as an unproved result: a wrong conversion cannot manufacture a theorem. Surface `+n` and `-n` integer literals do not add an integer term form to the kernel, an integer Core literal node, or a signed checked-numeral form. During surface normalization they become ordinary object-language constructor applications of `int_nonnegative` or `int_negative` around a Nat-only `CoreNatLit`. Only that Nat numeral becomes a checked `NatLit`. `Rational` has no literal form and uses explicit construction. ### 6.5. Theories A theorem carries a stamp identifying the theory it was proved in, and a theory records its ancestors. A rule that combines theorems checks that one theory extends the other. This is not bookkeeping. Without it, two modules could extend a shared theory in incompatible ways — one declaring `zero` at one type, the other at another — and a theorem from each could be combined into a proof of anything. Theorems from sibling theories are refused. Across modules, a `rhombus/hol` module publishes its finished theory in a hol\_theory submodule, and an import of that module adopts it: the same theory, the same theorem objects. Nothing is re-parsed and nothing is re-asserted, so there is no trust boundary at a module edge. A design that instead published a ​_description_​ of the theory and re-admitted each theorem on the word of the exporting module’s compile would introduce exactly such a boundary, forgeable by hand-writing the description. **A `~sorry` theorem is an axiom.** The `~sorry` proof option admits its theorem through `new_axiom` instead of proving it. Nothing hides it: the axiom is in the theory’s axiom list, and a theory that must be conservative, such as the standard library, is tested to have added none. ### 6.6. Where this leaks Three honest caveats. **The kernel is reachable.** Its module lives at `rhombus/hol/kernel.rhm`, an ordinary file with no module-system enforcement behind it. A module that imports it directly can call `new_axiom` and manufacture any theorem it likes. "It compiled, so it was proved" therefore holds for modules that do not do that, which is not the same as holding unconditionally. Sealing this properly needs the kernel module to be protected at the module-system level; that is not done. **The extraction toolchain is trusted.** Primitive inferences and theory extensions are definitions in Isabelle, with machine-checked soundness, well-formedness, model existence, and consistency results. Those definitions are exported to `kernel/generated.rhm`; the handwritten façade cannot construct Thm or Theory values and only converts public values, failures, extension deltas, and trace events. The Isabelle kernel, code generator, Rhombus compiler, and runtime therefore remain part of the trusted computing base. **Type variables in specialised theorems.** A datatype’s theorems are proved at its own type and instantiated at each use through the same `INST_TYPE` as everything else. That is standard, but it means the positivity checker has to be right about parameterised types, not merely about ground ones. ### 6.7. Limitations of this version Beyond the termination restrictions in Termination: * Logical declarations must appear directly in a `rhombus/hol` module body — not inside block and not inside a macro expansion. * Patterns may nest to any depth, clauses are ordered (earliest match wins, as in the match they compile to), and `_` names a position a clause does not use — inside a pattern or as a whole clause head. A clause that no argument shape can reach is still refused, and so is a matrix that leaves a constructor uncovered: ordering is a way to write a fallback, not a way to skip totality. A definition’s equations are stated only at the shapes each clause wins at. This keeps an ordered catch-all from also asserting an equation at a shape handled by an earlier clause, preserving the executable definition’s earliest-match meaning. * An import of a theory must precede the module’s own declarations, and several must be given in dependency order. Two theories neither of which extends the other cannot be used together. An import whose module path this version cannot read is refused rather than quietly treated as ordinary. * Adopting a theory re-runs the exporting module’s proofs, once per importing compilation. * The function body grammar has named applications, if, cond, local let, matching, Booleans, self-typed `Nat` and `Integer` literals, HOL notation, `block:`, an expected-type ascription, and anonymous or named-local function (an ordinary, non-recursive lambda; Local and anonymous function). `Rational` values require explicit construction. Overloaded function calls are resolved before kernel terms or executable code are produced; neither layer contains a runtime overload mechanism. The grammar has no effects, implicit numeric coercions, general runtime-only Rhombus expressions, or — inside a local or anonymous function — any recursive binding: self-recursion, forward reference to a later local function, and a call back into the currently-being-defined enclosing function are all rejected (Termination). * Proof search is bounded, but a rule that does not make progress is still admitted. mk\_rule’s conditions catch a variable left-hand side, an unconstrained variable or type variable on the right, and a trivial equation; nothing checks that a rule shrinks anything. Such a rule no longer hangs `raco make`, because rewriting runs against a shared step budget and detects a position that rewrites back to a term it has already been — but it fails the compile with a resource error rather than telling you which rule was at fault. See The Prover. ## 7. License and Third-Party Notices `LICENSE` contains the 0BSD terms for original Rhombus/HOL material. `REUSE.toml` is the authoritative per-file copyright and SPDX license map. `THIRD_PARTY_NOTICES` records exact source-derived scopes separately from design references and generated assets. `LICENSES/` contains canonical SPDX terms; `THIRD_PARTY_LICENSES/` retains audited upstream notices and exact revisions. Package-local copies keep independently distributable archives self-contained. The public site links the repository-level documents from its front page.