Reasoning with inductive 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

– 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
Advertisements
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: