SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/inductive

Reasoning with inductive data types

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

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.

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:

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
 

Emacs suffix

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- Introduction

- The basic concepts

- Used examples

- Match expressions

- Equality and identity

- The command "rewrite"

- Proof rules for equality

- Attributes with preconditions

- Recursive definitions

- Induction principles

- The type UNARY_NATURAL

- Addition

- Zero is neutral

- Commutativity

- Associativity

- Multiplication

- Summary

- Appendix

- The role of "zero" in multiplication

- Multiplication distributes over addition

- Multiplication is commutative

- Emacs suffix


ip-location