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 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.
-> Tests for functionality "Check Maxixe proof"
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
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
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
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
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
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
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'