More reasoning with Prooftoys
Contents
In the descriptions of rules of inference, capital letters A, B, and C are variables with boolean (true/false) values. The letters x and y are used for variables of any type. You can supply any term you choose for capital letters X and Y without the need to follow the usual rules for substitution.
Some basic facts
x = x
A == A
The value of any expression is equal to itself. This is often a good
way to start a proof that A
is equal to something else. Keep
replacing one side (usually the right) with something else that is
equal to it.
x = y == y = x
(symmetry of equality)
x = y & y = z => x = z
(transitivity of equality)
f = g == forall {x. f x = g x}
(extensionality)When working with equality in Prooftoys it is important to remember
that equivalence (==
) is the same concept as equality
applied to true/false values.
There are also numerous facts about quantifiers that work as rewrite rules using an extended form of matching, described TBD.
Tautologies
Tautology | Use |
---|---|
A => A |
starting various kinds of proofs |
(A => B) & (B => A) == (A == B) |
proving an equivalence |
Proving A and B
If statements A and B are both proved, how can I prove the statement
A & B
?
Removing irrelevant assumptions
If a conditional fact has an assumption with a variable that only appears (free) in that assumption and nowhere else in the statement of the fact, that assumption can be safely be removed. We can suggest the working of the inference like this:
a_1 & a_2 & ... => C
To: a_2 & ... => C
The one limitation is that there must be some value for the variable that can make the irrelevant assumption true. So to use this rule in a proof, there must be a proof that such a value exists. Prooftoys currently supports a couple of common cases. These are useful cases, and Prooftoys can work out the existence fact on its own. The cases are:
<var> = <term>
; and
R <var>
In both cases, the variable var
does not appear in the
fact outside this one assumption.
For every assumption of these kinds, the existence of a value satisfying it is provable, so we can remove the assumption from the proof step.
Definitions
Adding a new axiom
[[discuss]]