Inductive types are very powerful because they allow to write recursively
defined functions which are guaranteed to terminate and to reason about them
by induction. Recursively defined functions an proofs by induction are closely
related. As an introductory example we use the class
case class UNARY_NATURAL create zero succ(pred: UNARY_NATURAL) feature plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then Current case succ(p) then succ(Current+p) end end
and assume that we want to prove the assertion
all(a) zero + a = a
We can proof this assertion informally with the following argument.
The assertion is obviously true if “a” has been created with the creator
“zero”. The definition of “plus” says in the first case clause that
“anything+zero” yields “anything” and this anything might be “zero” as well.
Now let us consider the case that “a” has been created with “succ” and that
the assertion is valid for the predecessor of “a”, i.e. we have the
-- "a" has been created by the creator "succ" zero + a.pred = a.pred -- induction hypothesis
Now we prove the assertion “zero+a=a” under these premises. If “a” has been
created with “succ” the second case clause of the definition of “plus” tells
zero + a = succ(zero+a.pred)
From our assumption we know that “zero+a.pred=a.pred. We can use this fact to
zero + a = succ(a.pred)
The expression “succ(a.pred)” must be equivalent to “a” and this gives us
zero + a = a
which is identical to our assertion to be proved.
This “inductive” reasoning is possible because and UNARY_NATURAL is an
inductive type. If we do not yet have an object of UNARY_NATURAL the only way
to construct one is to use the “zero” creator. If we already have a
UNARY_NATURAL (say “n”) we can use the creator “succ” to create
“succ(n)”. Then if “zero” satisfies a certain property and every number “n”
carries over this property to its successor “succ(n)” then we conclude that
the property is valid for all number constructed in this manner.
Modern Eiffel’s proof engine supports inductive proofs like the one informally
described. The following chapter prepares the basic machinery which enable us
to do inductive proofs efficiently using the proof engine. It explains how we
state that some object has been constructed in a certain manner, what equality
means for inductive types and which rewrites are allowed, how we satisfy
preconditions to access an attribute and how we do proofs by induction.
The class UNARY_NATURAL is not efficient to do arithmetics. Nobody should do
actual calculations in a program using this class. However it is an excellent
vehicle to model natural numbers and demonstrate the basic reasoning
The basic concepts
The basic reasoning techniques which rely on inductive data types are best
explained with simple examples. In addition to the type UNARY_NATURAL we use
the types COLOR, OPTIONAL[G] and EMPTY to explain the basic rules and the
case class COLOR create red green blue end case class OPTIONAL[G] create none value(value:G) end case class EMPTY end
The class OPTIONAL is a generic class which takes one type parameter. This
generic class can construct e.g. the type OPTIONAL[CHARACTER]. Objects of type
OPTIONAL[CHARACTER] have no value if they have been created with “none” or
have a value of type CHARACTER if they have been created with “value(‘a’)”.
Note that feature names in Modern Eiffel need not be unique. The class
OPTIONAL has two features, a creator named “value” and an attribute named
“value”. These two features have different signatures. The creator takes one
argument and the attribute returns a value. In Modern Eiffel the feature name
together with the signature must uniquely address a feature.
The class EMPTY has no creator. Therefore it is not possible to create objects
of this type.
An object of inductive type is immutable, i.e. its value is fixed at creation
time and cannot be changed. We need a way to express the fact that an object
attached to a variable has been created with a certain creator. E.g. for a
UNARY_NATURAL “a” we want to make statements like “a has been created with the
zero creator” or “a has been created with the succ creator”. This is expressed
in Modern Eiffel as a match expression.
a as zero -- a has been created with "zero" a as succ(_) -- a has been created with "succ" a as succ(succ(_)) -- a has been created by double application of "succ"
We use the anonymous variable “_” to express that we are not interested in the
value of the argument. “a as succ(_)” expresses the fact that “a” has been
constructed with the creator “succ” with some argument.
Match expressions are boolean expressions. We can combine them with boolean
not (a as zero) not (a as succ(_) a as zero and b as succ(_)
The opterator “as” has the same precedence as the relational operators “=”,
“<=”, … I.e. it has higher precedence than “and”, “or”, … and lower
precedence than “not”.
Equality and identity
For immutable type objects equality is a rather strong property. If two
immutable type objects “o1″ and “o2″ are equal, i.e. “o1=o2″ or
“o1.is_equal(o2)” then they are indistiguishable. There is no construct in
Modern Eiffel to distinguish two instances of an immutable type object if they
This means that immutable type objects are treated like numbers. E.g. the
number “5″ is always the number “5″ and has the same properties (e.g. “5″ is a
prime number) regardless where it is stored.
We say that immutable type objects do not have identity.
Mutable type objects have an identity. We can build a mutable type which
models a car. Two instances of CAR are different objects even if they are
equal. E.g. you can have a car which is equal to your neighbour’s car. Both
cars are from the same car company, are the same model, have the same color,
have the same extras. But they are different cars. They are mutable, because
their state can change, e.g. their velocity. Changes of the state of one does
not change the state of the other. As opposed to this there is no way to
change the number “5″. It is possible to assign to a variable a different
number, but the number cannot change.
We need two different operators to express these different concepts. The
equality operator “=” expresses equality and the identity operator “~”
expresses identity. Of course identity implies equality. An object is always
equal to itself.
Here we discuss objects of inductive types. An inductive type is an immutable
type and for immutable types there is no difference between equality and
identity. The identity of an immutable type object is its value. I.e. equality
implies identity (which is not true for mutable objects).
Whenever we have two expression “e1″ and “e2″ of immutable type we can
substitute one for the other. This property is called referentially
transparency. Expressions returning immutable type objects are referentially
The command “rewrite”
In order to exploit the property that two equal objects of immutable type are
indistinguishable we introduce the command “rewrite(e1,e2)”. E.g.
-- state before: x=y, ... : 2+x=2*y rewrite(x,y) -- state after: x=y, ... : 2+y=2*y
If the proof engine encounters the command “rewrite(e1,e2)” it checks whether
the type of “e1″ and “e2″ is an immutable type and if the equality “e1=e2″ is
either on the assumption stack or it it matches an already proved
assertion. If yes, it substitutes within the current goal all expressions of
the form “e1″ by the expression “e2″.
If the type of “e1″ and “e2″ is mutable, then it searches for a match of
“e1~e2″ instead of “e1=e2″.
The rewrite command can have more than two arguments. The command
“rewrite(e1,e2,e3,…)” is semantically equivalent to the sequence of commands
“rewrite(e1,e2); rewrite(e2,e3); …”.
In many cases the rewrite command does not encounter a match for “e1=e2″ but a
match for “a=>(e1=e2)” (or a cascaded implication like
“a=>b=>…=>(e1=e2)”). In this case the proof engine loads all premises “a”,
… onto the goal stack and issues for each of them a “remove” and then does
the rewriting of the current goal.
Proof rules for equality
Equalities are expressed by the equality operator “=” and inequalities are
expressed by the inequality operator “/=”. The expression “a/=b” is a
shorthand for “not (a=b)”.
Two objects of inductive type are equal if and only if
- they have been created with the same creator
- using the same arguments
Furthermore inductive types are constructive.
There must be at least one basic creator to create “first” objects of this
type. A basic creator either doesn’t have arguments (like “zero” in the type
UNARY_NATURAL) or has arguments of objects which are not based on objects of
the same inductive type.
Then there might be recursive creators (like “succ”) which involve other
objects of the same type. These creators create an object which is different
from all objects involved in its construction.
I.e. it is not possible to have any cycles in the process of object creation.
The attributes of the objects are identical to the corresponding arguments of
These rules can be summarized by the following assertions (here for the
different_creator: succ(x) /= zero injection: x /= succ(x) equal_intro: x=y => succ(x)=succ(y) equal_elim: succ(x)=succ(y) => x=y reconstruction: x = succ(x.pred) retrieval: x = succ(x).pred
The proof engine uses these assertions as axioms. I.e. the command “remove”
can discharge goals which match the above equalities or inequalities and the
command “premise” can exploit the above implications.
The general case where “c”, “c1″, “c2″, … are different creators looks like
different_creator: c1(...) /= c2(...) injection: a /= c1(a,...) equal_intro: a1~b1 => a2~b2 => c(a1,a2,...)=c(b1,b2,...) equal_elim: c(a1,a2,...)=c(b1,b2,...) => a1~b1 reconstruction a = c(a.attr1, a.attr2, ...) retrieval a ~ c(a,b,...).attr1
In the general case some of the arguments of the creators might be mutable
type objects. For these types the corresponding identities are
guaranteed. Remember that for immutable type objects there is no difference
between equality and identity.
Attributes with preconditions
An attribute of an object of inductive type is available only if the object
has been constructed with a creator which introduced the attribute.
The attribute “value” of an object of type OPTIONAL[CHARACTER] can be accessed
only if the object has been created with the creator “value”. If the object
has been created with “none”, then the attribute “value” does not exist,
i.e. cannot be accessed.
A similar condition applies to an object of type UNARY_NATURAL. The attribute
“pred” (the predecessor) can be accessed only if the number has been created
with the creator “succ”. For a number created with “zero” the attribute “pred”
is not accessible.
I.e. the access of an attribute has a precondition.
a,b: UNARY_NATURAL o: OPTIONAL[UNARY_NATURAL] -- expression precondition(s) o.value o as value(_) a.pred a as succ(_) a.pred=b a as succ(_) o.value=a.pred o as value(_), a as succ(_)
The above expressions can be combined to form boolean expressions. All binary
boolean operators are short circuited. Therefore the following rules apply:
-- expression precondition(s) o=none and a=b.pred o=none => b as succ(_) o.value=a and a=b.pred o as value(_), o.value=a => b as succ(_) o.value=a => a=b.pred o as value(_), o.value=a => b as succ(_) o=none or a=b.pred o/=none => b as succ(_)
In the general case we get the preconditions:
-- assumptions: -- expression e has preconditions e_p1, e_p2, ... -- e1 has preconditions e1_p1, e1_p2, ... -- e2 has preconditions e1_p1, e1_p2, ... -- function f has preconditions f_p1, f_p2, ... -- expression precondition(s) f(e) e_p1, e_p2,..., f_p1(e), f_p2(e),... e1 => e2 e1_p1, e1_p2,..., e1=>e2_p1, e1=>e2_p2,... e1 and e2 e1_p1, e1_p2,..., e1=>e2_p1, e1=>e2_p2,... e1 or e2 e1_p1, e1_p2,..., not e1 => e2_p1, not e1 => e2_p2,...
An assertion to be proved is an expression which might have preconditions
according to the above defined rules. If the proof engine enters a proof of an
assertion “ass” with preconditions it does the following.
- It calculates all preconditions “p1″, “p2″, … according to the above
- It enters all preconditions “p1″, “p2″, … and the assertion “ass” onto the
- It issues for each precondition the command “resolve”.
- If it cannot proof all preconditions by “resolve” the proof fails and the
assertion is not accepted as valid.
- After resolving all preconditions it starts with the provided proof commands
(or with an implicit “resolve” in case that the assertion has no explicit
This rule requires that all preconditions of an assertion must be provable
with “resolve”. The programmer has to make sure that this is possible by
providing enough assertions as lemmas.
The function “plus” within the class UNARY_NATURAL is defined recursively as
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then Current case succ(p) then succ(Current+p) end
Keep in mind that Modern Eiffel is object oriented, i.e. if “a” and “b” are
variables of type UNARY_NATURAL, then the two expressions
a.plus(b) a + b
are equivalent because the operator “+” has been defined to be an alias for
the feature named “plus”. The special entity “Current” describes the current
object (like “this”, “self”, … in other object oriented languages). The
inspect expression inspects how “o” has been created. There has to be a case
clause for each possible creator.
The first case clause applies if “o” has been created with the “zero”
creator. The second case clause applies if “o” has been created with the
“succ” creator. Since “succ” requires one argument, the fresh variable “p” is
introduced to describe the predecessor of the newly created object.
Due to the nature of inductive types the compiler can check that the case
clauses are exhaustive. Furthermore the compiler can check that the recursion
does indeed terminate. It does this check in verifying that each recursive
call has at least one “decreasing” argument. In this case the second argument
is decreasing because it is called with the predecessor of “o” in the
The following two case clauses are equivalent:
case succ(p) then succ(Current+p) -- is equivalent to case succ(_) then succ(Current+o.pred)
The first form is usually preferable. Remember that the expression
“succ(Current+o.pred)” has according to the above described rule the
precondition “o as succ(_)”. Since the case clause is only entered if the
precondition is valid, the whole inspect expression is valid.
The definition of the function “plus” is an equality. We can give an
equivalent definition which makes this fact more transparent.
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL ensure Result = inspect o case zero then Current case succ(p) then succ(Current+p) end end
The local variable “Result” represents the expression “Current+o” or
In the first case “Result” is equal to “Current” and in the second case it is
equal to “succ(Current+o.pred)”. I.e. we can rewrite the definition as
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL ensure o as zero => (Result = Current) o as succ(_) => (Result = succ(Current+o.pred)) end
If we abstract this definition even more we get
all(a,b:UNARY_NATURAL) check a+zero = a b as succ(_) => a+b = succ(a+b.pred) end
The last form describes how the proof engine views this function
definition. Therefore the proof engine allows the command “rewrite(a+zero,a)”
for any variable “a”. Furthermore command “rewrite(a+b, succ(a+b.pred))” is
allowed by the proof engine if it can discharge “b as succ(_)” immediately by
“remove” (this is possible if “b as succ(_)” is already on the assumption
The proof engine creates for each inductive type and induction principle.
Let us look at the example COLOR. An object of type COLOR can be constructed
only with one of the three constructors “red”, “green” or “blue”. If we want
to proof an assertion of the form
it is sufficient to prove “f(c)” for each possible construction of “c”. For
the type COLOR the proof engine derives the induction principle
all(e:BOOLEAN) e[c:=red] => e[c:=green] => e[c:=blue] => all(c:COLOR) e
where e[x:=exp] is the expression obtained by substituting within “e” all free
occurrences of the variable “x” by the expression “exp”.
With this principle we can start a proof like
all(c:COLOR) f(c) proof induction(f(red), f(green), f(blue)) ... end
The command “induction” like the command “premise” replaces the curent goal
by its premises according to the derived induction principle.
For the type OPTIONAL[G] the following induction principle is generated
all(e:BOOLEAN) e[o:=none] => (all(o:OPTIONAL[G]) o as value(_) => e) => all(o:OPTIONAL[G]) e
This allows us to start a proof as
all(o:OPTINAL[CHARACTER]) f(o) proof induction( f(none), all(o:OPTIONAL[G]) o as value(_) => f(o) ) ... end
The principle should be clear. If we want to prove a universally quantified
assertion of the form “all(x:T) f(x)” we have to proof one premise for each
creator. If the creator is argumentless then the variable is substituted by
the creator. If the creator has arguments then a universally quantified
premise is generated with an implication. The implication has as its premise
that the value has been constructed with the specific creator.
What induction principle is generated for the type EMPTY? The type EMPTY has
no creators, i.e. there are no premises. This corresponds to the fact that we
cannot create an object of type EMPTY because we have no creator. No creator
means no premise. Therefore the induction principle looks like
all(e:BOOLEAN) all(u:EMPTY) e
which basically says that “e” is valid for all objects of type EMPTY. But
since there are no objects of type EMPTY, this principle cannot be used to
actually prove anything (unless we achieve the impossible and create an object
of type EMPTY!).
The generated induction principle gets interesting if the inductive type is
recursive. For the type UNARY_NATURAL the proof engine generates the induction
all(e:BOOLEAN) e[n:=zero] => (all(n:UNARY_NATURAL) n as succ(_) => e[n:=n.pred] -- induction hypothesis => e ) => all(n:UNARY_NATURAL) e
with a possible proof template
all(n:UNARY_NATURAL) f(n) proof induction( f(zero), all(n) n as succ(_) => f(n.pred) => f(n) ) ... end
As opposed to the induction principles for COLOR, OPTIONAL, etc. this
induction principle has an induction hypothesis which gives us more context
when shifted onto the assumption stack.
The induction principle states:
If a statement is true for the number “zero” and every number carries the
truth of the statement over to its successor, then the statement is true for
The type UNARY_NATURAL
In this chapter we focus on the type UNARY_NATURAL. It is defined like
case class UNARY_NATURAL create zero succ(pred:UNARY_NATURAL) feature -- functions ... -- properties ... end
The function “plus” is defined as
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then Current case succ(p) then succ(Current+p) end
Zero is neutral
We first prove that zero is a right neutral element of addition.
all(a:UNARY_NATURAL) check a + zero = a proof rewrite(a+zero,a); remove end end
The rewrite command is justified by the non recursive branch of the inspect
expression. If the second operand in the addition is “zero” then the result is
the first operand.
The proof “zero is left neutral” requires a proof by induction.
all(a:UNARY_NATURAL) zero + a = a proof induction( zero+zero=zero, all(a) a as succ(_) => zero+a.pred=a.pred => zero+a=a ) rewrite(zero+zero,zero); remove enter(3) rewrite( zero+a, succ(zero+a.pred), -- definition of "plus" succ(a.pred) ) -- induction hypothesis remove -- reconstruction end
The initial step requires us to proof that “zero+a=a” is valid if we
substitute “a” by zero. A simple rewrite based on the nonrecursive branch of
the definition of “plus” let us remove the goal.
The induction step requires us to prove that “zero+a=a” is valid under the
assumption that “a” has been created with “succ” and the statement is already
valid for the predecessor of “a”.
Since “a” has been created with “succ” we can rewrite “zero+a” by
“succ(zero+a.pred)” (based on the recursive branch of the definition of
“plus”). Then we can rewrite this to “succ(a.pred)” based on the induction
hypothesis. Based on the rules of equality we can discharge the remaining
goal “succ(a.pred)=a” immediately by “remove”.
Addition must be commutative. We can prove commutativity by induction. But the
proof needs another assertion to work smoothly. First we have to prove the
fact that “a+b=succ(a.pred+b)”. This equality is needed for rewriting within
the proof of commutativity.
all(a,b:UNARY_NATURAL) check lemma: a as succ(_) => a+b = succ(a.pred+b) proof generalize(b) induction( a as succ(_) => a+zero = succ(a.pred+zero), all(b) b as succ(_) => a as succ(_) => a+b.pred = succ(a.pred+b.pred) => a+b = succ(a.pred+b) ) rewrite(a.pred+zero,a.pred); rewrite(a+zero,a); remove enter(4) rewrite( a+b, succ(a+b.pred), -- definition "plus" succ(succ(a.pred+b.pred)), -- induction hypothesis succ(a.pred+b) ) -- definition "plus" end commutativiy: a+b = b+a proof generalize(a) induction( zero+b = b+zero, all(a) a as succ(_) => a.pred+b = b+a.pred => a+b = b+a ) rewrite(zero+b,b); rewrite(b+zero,b); remove enter(3) rewrite( b+a, succ(b+a.pred), -- definition "plus" succ(a.pred+b), -- induction hypothesis a+b ) -- lemma remove end end
The rewritings should be easy to follow. But I have used the not yet
introduced command “generalize” which needs some explanation. Remember that we
had already assertions of the form
all(x:X; y:Y; ...) check ass1 proof ... end ass2 proof ... end ... end
where the “check … end” block had been used to group a number of assertions
which needed the same variables. In Modern Eiffel this is just a shorthand for
all(x:X; y:Y; ...) ass1 proof enter(n) ... end all(x:X; y:Y; ...) ass2 proof enter(n) ... end ...
I.e. the assertions “ass1″, “ass2″ are treated as individual assertions each
with its own quantifier. Remember also that an assertion of the form
is the implicit implication
"x has type X" => e
where the typing judgement can be shifted onto the assumption stack. If we
prove an assertion within the “check … end” block, all typing judgements of
the surrounding quantifier have already been shifted onto the assumption
stack. This means that the variables are now free variables.
However a proof by induction needs an assertion of the form “all(x:X) e”. The
command “generalize(x)” regeneralizes the assertion with respect to the
variable “x”, i.e. it puts an allquantor before the expression within the
current goal. This generalization replaces the current goal with a stronger
(or equivalent) goal.
The command “generalize(a,b,…)” is equivalent to “…; generalize(b);
generalize(a)”. Therefore it gives us the possibility to reorder the
variables within the allquantor.
The proof engine accepts the command “generalize” only for variables which
already occur as free variables in the current goal.
In the following a proof of the associativity of “plus” is given.
all(a,b:UNARY_NATURAL) check lemma_1: b as succ(_) => (a+b) as succ(_) proof enter rewrite(a+b, succ(a+b.pred)) -- definition of "plus" remove -- match expression end lemma_2: b as succ(_) => a+b.pred = (a+b).pred proof enter premise(succ(a+b.pred) = succ((a+b).pred)) -- eq elim rewrite(succ(a+b.pred), a+b) -- definition of "+" rewrite(succ(a+b).pred, a+b) -- argument retrieval remove end associativity: a+b+c = a+(b+c) proof generalize(c) induction( a+b+zero = a+(b+zero) all(c) c as succ(_) => a+b+c.pred = a+(b+c.pred) => a+b+c = a+(b+c) ) resolve enter(3) rewrite( a+b+c, succ(a+b+c.pred), -- definition of "plus" succ(a+(b+c.pred)), -- induction hypothesis succ(a+(b+c).pred), -- lemma_2 a+(b+c) ) -- definition of "plus" remove end
Some comments to understand the proofs:
- The right hand side of lemma_2 “a+b.pred = (a+b).pred” accesses the
predecessor attribute of “b” and “a+b”. Therefore it has the preconditions
“b as succ(_)” and (a+b) as succ(_). The first one is already on the left
hand side of the implication. The second one follows as well from the left
hand side. The lemma_1 gives a trivial proof. Later we will see that the
proof engine is powerful enough to derive lemma_1 automatically. But we
state the lemma and prove it explicitly here.
- In the proof of associativity we have used the command “resolve” to
discharge the initial step of the induction automatically. This is possible
because “resolve” tries all possible rewritings as long as the rewritten
goal is not more complicated than the current goal. The command “resolve” is
even more powerful. But this is not yet needed here, because we keep on
stating many steps explicitly.
Multiplication is defined recursively as well.
times alias "*" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then zero case succ(p) then Current*p + Current end
For multiplication we expect the following properties:
all(a,b,c,d: UNARY_NATURAL) check zero_1: a*zero = zero zero_2: zero*a = zero lemma: a+b+(c+d) = a+c + (b+c) distributivity: (a+b)*c = a*c + b*c end all(a,b,c: UNARY_NATURAL) check lemma_1: a + b + c = a + c + b lemma_2: b as succ(_) => b.pred*a+a = b*a commutativity: a*b = b*a -- hint use definition of "*" and "+" before -- using the induction hypothesis end
The proof of these properties is left as an excercise to the reader. It is not
difficult to perform these proofs.
Sometimes it is difficult to find the needed lemmas to proof an expected
law. If one starts e.g. to prove distributivity without the mentioned lemmas
an induction proof soon gets stuck because one cannot make some necessary
rewriting. The best thing to do is to state the lemma which allows the
rewriting and see if it is possible to complete the proof. Then of course the
lemma has to be proved as well which might need other lemmas to support the
It is not recommended to try nested proofs by induction. It is possible to
perform nested proofs but one gets lost easily.
We introduced the basic reasoning techniques for inductive types.
Inductive types have special axioms for equality. The commands “remove” and
“premise” are powerful enough to exploit this properties. Furthermore term
rewriting can be done based on equality.
Inductive types have attributes which might have preconditions. The proof
engine verifies that all preconditions are valid.
For each inductive type an induction principle is generated by the proof
engine. The additional commands “generalize” and “induction” have been
introduced to perform proofs by induction.
The role of “zero” in multiplication
all(a:UNARY_NATURAL) check zero_1: a*zero = zero proof rewrite(a*zero,zero); remove end zero_2: zero*a = zero proof generalize(a) induction( zero*zero=zero, all(a) a as succ(_) => zero*a.pred=zero => zero*a=zero ) resolve enter(2) rewrite( zero*a, zero*a.pred + zero, zero*a.pred, zero ) remove end end
Multiplication distributes over addition
all(a,b,c,d: UNARY_NATURAL) check lemma: a+b+(c+d) = a+c + (b+c) proof rewrite( a+b+(c+d), a+b+c+d, a+(b+c)+d, a+(c+b)+d, a+c+b+d, a+c + (b+d) ) remove end distributivity: (a+b)*c = a*c + b*c proof generalize(c) induction( (a+b)*zero = a*zero + b*zero, all(c) c as succ(_) => (a+b)*c.pred = a*c.pred + b*c.pred => (a+b)*c = a*c + b*c ) resolve enter(3) rewrite( (a+b)*c, (a+b)*c.pred + (a+b), a*c.pred+b*c.pred + (a+b), a*c.pred+a + (b*c.pred+b), a*c + b*c ) remove end end
Multiplication is commutative
all(a,b,c: UNARY_NATURAL) check lemma_1: a + b + c = a + c + b proof rewrite( a+b+c, a+(b+c), a+(c+b), a+c+b ) end lemma_2: b as succ(_) => b.pred*a+a = b*a proof generalize(a) induction( b as succ(_) => b.pred*zero+zero = b*zero, all(a) a as succ(_) => (b as succ(_) => b.pred*a.pred+a.pred = b*a.pred) => b as succ(_) => b.pred*a+a = b*a ) resolve enter(4) rewrite( b.pred*a + a, b.pred*a.pred + b.pred + a, succ(b.pred*a.pred + b.pred + a.pred), -- def "+" succ(b.pred*a.pred + a.pred + b.pred), -- lemma_1 succ(b*a.pred + b.pred), -- induction hypothesis b*a.pred+b, -- def "+" b*a ) -- def "*" end commutativity: a*b = b*a proof generalize(b) induction( a*zero = zero*a all(b) b as succ(_) => a*b.pred = b.pred*a => a*b = b*a ) resolve enter(3) rewrite( a*b, a*b.pred+a, b.pred*a+a, b*a ) remove end end