Maxixe ====== This document describes the Maxixe proof-checking language. It contains many examples of proofs written in Maxixe. These examples are written in [Falderal][] format so that, as well as illustrating the language for human readers, they can be automatically checked and thus serve as a test suite. However, because these examples are designed to show what is and what is not valid in Maxixe, these proofs are neither particularly realistic nor particularly interesting. For examples of proofs that are more interesting than these, please see the [Examples.md](Examples.md) document. Note that in these examples the `===> ok` or the `???>` line is not part of the proof (or even part of Maxixe's syntax); these lines are for Falderal's benefit. [Falderal]: http://catseye.tc/node/Falderal -> Tests for functionality "Check Maxixe proof" Basic Proof Structure --------------------- A Maxixe proof consists of 3 sections: `given`, in which rules of inference (including axioms and premises) are defined; `show`, which declares the goal of the proof; and `proof`, which lists the steps to derive the goal from the rules. This is probably the shortest possible valid proof that can be written in Maxixe (as well as the least interesting one). It proves exactly what is stated as a premise. given A = |- a show a proof C = a by A qed ===> ok ### Rules ### In Maxixe we often call rules of inference just 'rules' for short. A rule of inference consists of a name, an equals sign (`=`), a semicolon-separated list of zero or more hypotheses, a turnstile (`|-`), and a conclusion. A name must start with an upper-case letter and otherwise consists of alphanumeric characters and underscores. given foo = |- a show a proof C = a by A qed ???> Expected variable, but found atom No two rules may have the same name. given A = |- a A = |- b show a proof C = a by A qed ???> name has already been used for a rule of inference Each hypothesis is a term, and so is the conclusion. A term is given by a _constructor_, which starts with a lower-case letter or a decimal digit and otherwise consists of alphanumeric characters and underscores, followed by an optional comma-separated list of subterms enclosed in parentheses. A term with no subterms is called an _atom_. given A = atom_1 |- atom_2 B = |- term(subterm(a, b), c) show term(subterm(a, b), c) proof C = term(subterm(a, b), c) by B qed ===> ok A term may also be a _variable_, in which case it starts with an upper-case letter. Variables play a special role in the proof-checking process. TODO: describe pattern-matching here! given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule with S1 qed ===> ok The conclusion may not contain any variables which do not appear in the hypotheses. given Rule = P |- and(P, Q) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule with S1 qed ???> Q ### Goal ### The term given as the goal of a proof must not contain any variables. given A = |- a show A proof C = a by A qed ???> goal is not ground ### Steps ### Each step in a proof consists of a name, an equals sign, a term, and a justification. given A = |- a show a proof a by A qed ???> Expected variable, but found atom A step may not have the same name as a rule of inference. given A = |- a show a proof A = a by A qed ???> name has already been used for a rule of inference No two steps may have the same name. given A = |- a show a proof C = a by A C = a by A qed ???> name has already been used for a step Each step in a proof must name the rule being used in the justification (the `by` part) of the step. given A = |- a show a proof C = a qed ???> Expected 'by' The term given in a step of a proof must not contain any variables. given A = |- a show a proof C = Foo by A qed ???> If the rule named in the step of the proof has one or more hypotheses, the step must also give _arguments_ to use in _instantiating_ the rule. It must give exactly one argument for every hypothesis. given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule qed ???> Number of arguments provided (0) does not match number of hypotheses (1) given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule with S1, S1 qed ???> Number of arguments provided (2) does not match number of hypotheses (1) The rule named in the justification must be one of the defined rules of inference. given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Zanzibar_Land with S1 qed ???> Zanzibar_Land given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by S1 with S1 qed ???> S1 In most cases, the arguments given in the justification must be names of steps. that occur before the current step in the proof. given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule with Zanzibar_Land qed ???> Zanzibar_Land given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule with Premise qed ???> Premise Importantly, the steps given as arguments in a justification must occur *before* the current step of the proof. given Rule = P |- and(P, P) Premise = |- foo show and(foo, foo) proof S1 = foo by Premise S2 = and(foo, foo) by Rule with S2 qed ???> In step 'S2': Step name 'S2' in with is not the name of a preceding step Importantly, the term given in a step of a proof must follow from the rule and arguments given in the step's justification. given A = |- a show a proof C = foo by A qed ???> foo does not follow from A Importantly, the term in the last step in the proof must equal the term given in `show`. given A = |- a show foo proof C = a by A qed ???> proof does not reach goal Attributes and Substitution --------------------------- Here is the exception to the rule that an argument in a justification must be the name of a step. Hypotheses may be decorated with _attributes_ in curly braces. If a hypothesis is given the attribute `term`, the argument may be any ground term. given A = X{term} |- foo(X) show foo(zing(bar)) proof C = foo(zing(bar)) by A with zing(bar) qed ===> ok given A = X{term} |- foo(X) show foo(zing(bar)) proof C = foo(zing(bar)) by A with zing(Foo) qed ???> Not all variables replaced during rule instantiation If a hypothesis is given the attribute `atom`, the argument may be any atom. given A = X{atom} |- foo(X) show foo(bar) proof C = foo(bar) by A with bar qed ===> ok given A = X{atom} |- foo(X) show foo(zing(bar)) proof C = foo(zing(bar)) by A with zing(bar) qed ???> not an atom The conclusion may be optionally followed by a substitution, which is a comma-separated list of term-term pairs enclosed in square brackets. If a substitution is given, all the terms will be replaced by the other terms after conclusion has been derived. given A = P ; X{atom} |- P[f->X] Premise = |- foo(f) show foo(bar) proof S1 = foo(f) by Premise S2 = foo(bar) by A with S1, bar qed ===> ok given A = P ; X{atom} |- P[X->f] Premise = |- foo(bar) show foo(f) proof S1 = foo(bar) by Premise S2 = foo(f) by A with S1, bar qed ===> ok Subproofs --------- A proof may consist of nested subproofs, called _blocks_. Each block must be introduced by instantiating a specially-declared _block rule_. The structure of a block rule determines rules determine the structure of the block. A block rule (and thus a block) consists of one or more _cases_. Each case contains one or two non-block rules. The first rule must be used in the first step of the case, and the second rule, if given, must be used in the final step of the case. given A = |- a block Subproof case B = a |- b C = b |- c end end D = c |- d show d proof S1 = a by A block Subproof case S2 = b by B with S1 S3 = c by C with S2 end end S4 = d by D with S3 qed ===> ok If the second rule is not given, no restriction is placed on the final step of the case. given A = |- a block Subproof case B = a |- b end end C = b |- c D = c |- d show d proof S1 = a by A block Subproof case S2 = b by B with S1 S3 = c by C with S2 end end S4 = d by D with S3 qed ===> ok As an act of syntactic sugar, if a block contains only one case, the `case` ... `end` may be omitted, both in the proof, and in the rule definition. given A = |- a block Subproof B = a |- b end C = b |- c D = c |- d show d proof S1 = a by A block Subproof S2 = b by B with S1 S3 = c by C with S2 end S4 = d by D with S3 qed ===> ok Blocks may contain other blocks. given A = |- a block Subproof case B = a |- b C = b |- c end end D = c |- d show d proof S1 = a by A block Subproof case S2 = b by B with S1 block Subproof case S3 = b by B with S1 S4 = c by C with S3 end end S5 = c by C with S2 end end S6 = d by D with S5 qed ===> ok A step may refer to any preceding step in the same block, or in any outer block (i.e. any block that contains the current block.) given A = |- a block Subproof case B = a |- b C = b |- c end end D = c |- d show d proof S1 = a by A S2 = a by A block Subproof case S3 = b by B with S1 S4 = b by B with S2 S5 = c by C with S3 S6 = c by C with S4 end end S7 = d by D with S6 qed ===> ok However, a step may only refer to the _final_ step in any inner block (i.e. any block that is contained by the current block.) given A = |- a block Subproof case B = a |- b C = b |- c end end D = c |- d show c proof S1 = a by A block Subproof case S2 = b by B with S1 S3 = c by C with S2 end end S4 = c by C with S2 qed ???> S2 is a non-final step in an inner block The rule in the justification of the first step in a case must be the initial rule specified for the case in the block rule. given A = |- a block Subproof case B = a |- b C = b |- c end end D = c |- d show d proof S1 = a by A block Subproof case Sw = a by A S2 = b by B with S1 S3 = c by C with S2 end end S4 = d by D with S3 qed ???> initial step of case 1 of Subproof must use rule B The rule in the justification of the last step in a case must be the final rule specified for the case in the block rule. given A = |- a block Subproof case B = a |- b C = b |- c end end D = c |- d E = a |- c show d proof S1 = a by A block Subproof case S2 = b by B with S1 S3 = c by C with S2 S4 = c by E with S1 end end S5 = d by D with S4 qed ???> final step of case 1 of Subproof must use rule C A block in a proof must have the same number of cases as the block rule used. given A = |- a B = a |- b C = a |- c block Subproof case D = b |- d E = X |- X end case F = c |- d G = X |- X end end H = X |- X show d proof S1 = a by A S2 = b by B with S1 S3 = c by C with S1 block Subproof case S4 = d by D with S2 S5 = d by E with S4 end case S6 = d by F with S3 S7 = d by G with S6 end end S8 = d by H with S5 qed ===> ok given A = |- a B = a |- b C = a |- c block Subproof case D = b |- d E = X |- X end case F = c |- d G = X |- X end end H = X |- X show d proof S1 = a by A S2 = b by B with S1 S3 = c by C with S1 block Subproof case S4 = d by D with S2 S5 = d by E with S4 end end S8 = d by H with S5 qed ???> block must have same number of cases as block rule given A = |- a B = a |- b C = a |- c block Subproof case D = b |- d E = X |- X end end H = X |- X show d proof S1 = a by A S2 = b by B with S1 S3 = c by C with S1 block Subproof case S4 = d by D with S2 S5 = d by E with S4 end case S6 = d by D with S3 S7 = d by E with S6 end end S8 = d by H with S5 qed ???> block must have same number of cases as block rule When a block has multiple cases, the last step in each case must contain the same term. given A = |- a B = a |- b C = a |- c block Subproof case D = b |- d E = X |- X end case F = c |- d G = X |- X end end H = X |- X show d proof S1 = a by A S2 = b by B with S1 S3 = c by C with S1 block Subproof case S4 = d by D with S2 S5 = d by E with S4 end case S6 = d by F with S3 Sw = c by H with S3 S7 = c by G with Sw end end S8 = d by H with S5 qed ???> cases do not finish with same term ### Locals ### If a hypothesis has the `local` attribute, its argument must be an atom, and that atom may only occur in the block in which the hypothesis is invoked. To enforce this, because outer blocks may only access the final step of a case in a block anyway, we only need check that it does not occur in the final step of any case of the block. given A = |- a block Subproof case B = a ; Q{local atom} |- Q C = b |- c end end D = c |- d show d proof S1 = a by A block Subproof case S2 = b by B with S1, b S3 = c by C with S2 end end S4 = d by D with S3 qed ===> ok given A = |- a block Subproof case B = a ; Q{local atom} |- Q C = Any |- Any end end D = Any |- Any show b proof S1 = a by A block Subproof case S2 = b by B with S1, b S3 = b by C with S2 end end S4 = b by D with S3 qed ???> Local atom 'b' cannot be used in final step of case If a hypothesis has the `nonlocal` attribute, its argument must be a term, and that term may not contain any atoms which are local to the block in which the hypothesis is invoked. given A = |- a block Subproof case B = a ; Q{local atom} |- Q C = b ; Q{nonlocal term} |- c end end D = c |- d show d proof S1 = a by A block Subproof case S2 = b by B with S1, b S3 = c by C with S2, fun(c) end end S4 = d by D with S3 qed ===> ok given A = |- a block Subproof case B = a ; Q{local atom} |- Q C = b ; Q{nonlocal term} |- c end end D = c |- d show d proof S1 = a by A block Subproof case S2 = b by B with S1, b S3 = c by C with S2, fun(b) end end S4 = d by D with S3 qed ???> must not contain local atom 'b'