# Introduction

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

assumptions

-- "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

us

zero + a = succ(zero+a.pred)

From our assumption we know that “zero+a.pred=a.pred. We can use this fact to

derive

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

techniques.

# The basic concepts

## Used examples

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

techniques.

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.

## Match expressions

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

operators

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

are equal.

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

transparent.

## 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

the creators.

These rules can be summarized by the following assertions (here for the

example UNARY_NATURAL).

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

defined rules.

– It enters all preconditions “p1”, “p2”, … and the assertion “ass” onto the

goal stack.

– 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

proof).

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.

## Recursive definitions

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

recursive branch.

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

“Current.plus(o)”.

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

stack).

## Induction principles

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

all(c:COLOR) f(c)

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

principle

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

all numbers.

# 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

## Addition

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”.

### Commutativity

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

all(x:X) e

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.

### Associativity

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

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

proof.

It is not recommended to try nested proofs by induction. It is possible to

perform nested proofs but one gets lost easily.

# Summary

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.

# Appendix

## 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