The Eiffel Compiler / Interpreter (tecomp)

In this blog entry I'm going to talk about proofs of assertions involving boolean expressions.

We are going to proof basic properties of boolean expressions like

reflexivity_of_implication: all(a:BOOLEAN) a => a commutativity_of_and: all(a,b:BOOLEAN) (a and b) = (b and a) transitivity_of_implication: all(a,b,c:BOOLEAN) (a=>b) and (b=>a) => (a=>c) contrapositive: all(a,b:BOOLEAN) (a=>b) = (not b => not a) de_morgan1: all(a,b:BOOLEAN) not (a and b) = (not a or not b) ...

In Modern Eiffel (like in ISE Eiffel) all asssertions can have an optional tag of the form "tag_name:". This optional tag is just a comment and has no semantic meaning.

The above described assertions do not have any free variables, all variable are bound within a quanitified expression. These kind of assertions are not bound to any context, i.e. they must be universally valid.

Note that the operators "not" "=" "and" "or" "=>" have precedences. "not" has the highest precedence and "=>" has the lowest precedence. The binary operators "and" and "or" are left associcative and the binary operator "=>" is right associative.

A quantifier like "all(a:BOOLEAN)" is just another form of an implication. I.e.

all(a:BOOLEAN) a => a

can be read as

```
"a has type BOOLEAN" => a => a
```

Each assertion can have a proof e.g.

all(a:BOOLEAN) a => a proof enter(2) remove end

A proof consists of a series of proof commands within a "proof ... end" block. The proof commands and the corresponding rules will be explained in the next chapters.

Many assertions can be grouped within a "check ... end" block. This can help to reduce the amount of quantifiers and enhance readability. E.g. the above assertions can be written as

all(a,b,c: BOOLEAN) check reflexivity: a => a commutativity: (a and b) = (b and a) transitivity: (a=>b) and (b=>c) => (a=>c) contrapositive: (a=>b) = (not a => not b) de_morgan1: not (a and b) = (not a or not b) end

Each of the assertions within the "check ... end" block can have its own proof. Note that grouping assertions within a "check ... end" block is just a shorthand. Modern Eiffel treats the above block as the five individual assertions stated at the beginning of the chapter.

The operators "and", "or" and "not" are well known. Intuition about these boolean operators is usually well developed. The implication operator is less known. But in order to successfully master proof techniques, implication is the most important boolean operation. Why? In order to prove an assertion we have to demonstrate that it follows from some basic facts and rules. The fact that b follows from a is expressed as the boolean implication "a=>b".

If the assertion "a=>b" is valid (i.e. it is either a basic fact/axiom or it has already been proved) and we want to prove "b", it is sufficient to prove "a". We also say that "a" is stronger than "b".

The implication "a=>b" states nothing about the validity of "a" and "b". Both can be false and the implication is still valid. The only combination which is ruled out by "a=>b" is that "a" is true and "b" is false. This cannot be the case, because the truth of "a" must imply the truth of "b".

Implications can be cascaded like "a=>b=>c". Because the implication operator is right associative this has to be read as "a=>(b=>c)".

Let us analyze the meaning of "a=>b=>c". This implication says that "a" implies the implication "b=>c". I.e. "b=>c" is valid under the assumption of "a". This in turn means the "c" is valid under the assumption of "b" under the assumption of "a". If we have already proved "a" and "b" and "a=>b=>c" is valid, we can safely conclude "c".

The last paragraph has demostrated that "a=>b=>c" is equivalent to "a and b => c". We can prove this equivalence with the help of the proof engine (see following chapters). The first form is usually preferable because it allows us to use the proof engine efficiently. Therefore instead of writing

(a=>b) and (b=>c) => (a=c)

we express this transitivity law as

(a=>b) => (b=>c) => (a=c)

It takes some time to get used to this form. But playing around with the proof engine will convince you that the second form is superior to the first form.

The proof engine has an internal state. It consists of an assumption and a goal stack. An arbitrary state of the proof engine can look like

a1, a2 [a3 [a4 : g1, g2] g3] g4

where a1, a2, a3 and a4 are assumptions and g1, g2, g3 and g4 are goals still to be proved. The left bracket "[" can occur only within the assumptions and right bracket "]" can occur only within the goals. The right and left brackets must match. The colon ":" separates the assumptions from the goals. The goal right to the ":" is the current goal to be proved. All proof commands apply to the current goal.

In the above state goals g1 and g2 have to be proved under the assumptions a1, a2, a3 and a4 and the goal g3 has to be proved under the assumptions a1, a2 and a3 and the goal g4 under the assumptions a1 and a2.

A proof is partially done if there is no more goal to the right of the colon ":". E.g. the state

a1, a2 [a3 [a4 : ] g3] g4

indicates that the inner proof is done. The inner proof will be discharged immediately to reach

a1, a2 [a3 : g3] g4

leaving the goals g3 and g4 still to be proved. A proof is completely done if there are no more goals to be proved.

Initially at the start of a proof the proof engine enters the state

: g

where g is the assertion to be proved. I.e. there are no assumptions and just one goal.

The proof engine has only a view basic commands to manipulate its state.

The first command is "enter" which enters a subproof. The enter command is valid only if the current goal is an implication. It transforms the state in the following way:

-- state before: ... : a=>b ... enter -- state after: ... [ a : b ] ...

This rule of the enter command reflects the fact that an implication "a=>b" is valid if "b" can be proved under the assumption of "a".

In case that the current goal is a cascaded implication like "a=>b=>c=>d" the enter command can have an optional argument to indicate how many assumptions are shifted onto the assumption stack.

-- state before: ... : a=>b=>c=>d ... enter -- state after: ... [ a : b=>c=>d ] ... -- state before: ... : a=>b=>c=>d ... enter(2) -- state after: ... [ a, b : c=>d ] ... -- state before: ... : a=>b=>c=>d ... enter(3) -- state after: ... [ a, b, c : d ] ...

The next command is "remove". It removes the current goal. This command is allowed only if the current goal is "True" or it matches an assumption or an already proved assertion. E.g.

-- state before: a1, a2 [a3 [a4 : a1] g3] g4 remove -- state after: a1, a2 [a3 : g3] g4

The third command is "premise(p1,p2,...)". It has one or more arguments called the premises. The command "premise(p1,p2,...)" can be issued, if the assertion "p1=>p2=>...=>g" where "g" is the current goal matches any assumption or an already proved assertion. E.g.

-- state before: ... a=>b=>c ... : c ... premise(a,b) -- state after: ... a=>b=>c ... : a, b ...

Any current goal can be substituted by a set of goals which together are stronger than the current goal. Under the assumption of "a=>b=>c" the validity of "a" and "b" implies the validity of "c". Therefore "c" can be substituted by the goals "a" and "b".

These three commands "enter", "remove" and "premise" are already sufficient to make some simple proofs. We can prove reflexivity of implication.

reflexivity: all(a:BOOLEAN) a=>a proof -- : all(a:BOOLEAN) a=>a enter(2) -- a:BOOLEAN, a : a remove end

The command "enter(2)" shifts two assumptions onto the assumption stack. The first assumption is that "a" is of type BOOLEAN and the second is that "a" is true. The command "remove" discharges the current goal "a" because it matches an assumption. After "remove" there are no more goals to be proved and the proof is completed.

In order to prove the modus ponens law we need one application of the command "premise".

modus_ponens: all(a,b:BOOLEAN) a => (a=>b) => b proof enter(4) -- a:BOOLEAN, b:BOOLEAN, a, a=>b : b premise(a) -- a:BOOLEAN, b:BOOLEAN, a, a=>b : a remove end

The first command enters 4 assumptions onto the assumption stack. The command "premise(a)" substitutes the current goal "b" by "a" because "a=>b" is a valid assumption (i.e. "a" is stronger than "b"). In the last step "a" can be removed from the goal stack, because it is a valid assumption.

Transitivity of implication can be proved in the same manner as the modus ponens law.

transitivity: all(a,b,c:BOOLEAN) (a=>b) => (b=>c) => (a=>c) proof enter(6) -- ... a=>b, b=>c, a : c premise(b) premise(a) remove end

Note that we have just used the basic rules of the proof engine to prove some trivial facts like reflexivity, modus ponens and transitivity. I.e. these facts are not necessary as axioms. The rules of the commands "enter", "premise" and "remove" are sufficient. These rules play the role of axioms.

We call "reflexivity", "modus ponens" and "transitivity" trivial, because our intuition tells us that they must be true. Clearly if "a implies b" and "b implies c" then certainly "a implies c". But what about the assertion

all(a,b,c:BOOLEAN) (a=>b=>c) => (a=>b) => (a=>c)

What does our intuition tell us about the truth of this assertion? Don't excercise your brain too much. Just try to prove it with the proof engine.

all(a,b,c:BOOLEAN) (a=>b=>c) => (a=>b) => (a=>c) proof enter(6) -- ... a=>b=>c, a=>b, a : c premise(a,b) -- ... a=>b=>c, a=>b, a : a, b remove premise(a) remove end

The basic rules of the proof engine "enter", "premise" and "remove" are not sufficient to proof all valid assertions of the propositional calculus. We need some additional axioms. Modern Eiffel allows axioms (i.e. unproved assertions) only in the postconditions of built-in functions.

The outline of the class BOOLEAN looks like

immutable class BOOLEAN inherit COMPARABLE redefine is_equal end feature implication alias "=>" (o:BOOLEAN): BOOLEAN external "built_in" end is_equal(o:BOOLEAN): BOOLEAN ... conjuncted alias "and" (o:BOOLEAN): BOOLEAN ... disjuncted alias "or" (o:BOOLEAN): BOOLEAN ... negated alias "not" : BOOLEAN ... ... end

The built-in function "=>" does not need axioms. The axioms of "=>" are implicitly given by the rules for the basic commands "enter", "premise" and "remove" of the proof engine.

The other built-in functions and their related axioms are discussed in the following.

The binary operator "=" is defined by the function "is_equal". This function is inherited from the class COMPARABLE and it is redefined within the class BOOLEAN.

is_equal(o:BOOLEAN): BOOLEAN external "built_in" ensure all(a,b:BOOLEAN) check intro: (a=>b) => (b=>a) => a=b elim1: a=b => (a=>b) elim2: a=b => (b=>a) end end

The function "is_equal" does not need the alias "=", because the operator "=" is bound by the language rule to the function "is_equal".

The first axiom says that "a=b" can be derived from "a=>b" and "b=>a". The second and third axiom say that the implications "a=>b" and "b=>a" follow from the equality "a=b". This is inline with our intuitive understanding of boolean equivalence.

Since the function "is_equal" is inherited from the class COMPARABLE, its contracts (i.e. pre- and postconditions) are inherited as well. The postcondition of "is_equal" within the class COMPARABLE (see last post describing the outline of Modern Eiffel) states

all(x,y,z: like Current) check reflexivity: x=x symmetry: x=y => y=x transitivity: x=y => y=z => x=z end

The class BOOLEAN has chosen to redefine the function "is_equal". Therefore it has to prove that the inherited contracts are respected.

The proof of reflexivity is straightforward

x=x proof premise(x=>x, x=>x) remove remove end

The axiom "intro" of "is_equal" tells us the premises for "x=x". We can discharge the premises by "remove" because "x=>x" has already been proved for any variable x of type BOOLEAN.

The symmetry requires some more "premise" and "remove" commands and the use of the "elim" axioms of "is_equal". It still should quite be easy for the reader to follow.

x=y => y=x proof enter premise(y=>x, x=>y) -- x=y : y=>x, x=>y premise(x=y) remove premise(x=y) remove end

This proof is already a little bit boring. There is nothing really creative in this proof. It is just the mechanical application of the basic rules and some of the axioms. Some of you might ask: "Isn't it possible that the machine does this mechanical work for us?". An answer is given in the next chapter.

In order to take off from us this kind of mechanical work Modern Eiffel's proof engine has some built in automation. The proof engine offers the command "resolve". This command does the following repeatedly:

- Try to remove the current goal immediately.
- Try to issue "premise" as long as the premises are not more complicated than the current goal.
- Try to enter.

This procedure needs some backtracking, because in some state of the iteration more than one "premise" command might be possible, but not all lead to a valid proof.

Now it is necessary to explain what "not more complicated" means. Modern Eiffel's measure for "complicated" is the depth of the expression. Every expression (therefore assertions as well) can be viewed as a tree.

a=>b a=>b=>c => => / \ / \ a b a => / \ b c

The expression "a=>b=>c" is one level deeper i.e. more complicated than "a=>b". The condition that new goals must not be more complicated guarantees that the above procedure associated with the command "resolve" will terminate. The number of expressions which can be built and are not more complicated than the goal is limited.

Let us see how "resolve" performs on the proof of the assertion "x=y => y=x".

It tries to remove the goal immediately. This fails because we neither have an assumption or another already proved assertion which matches this expression. Then it tries to find premises for these assertion in the assumptions and in the set of the already proved assertions. This approach fails as well. The command "enter" succeeds, because the current goal is an implication. This leads us to the state

x=y : y=x

Now the next iteration starts. The only possible command here is "premise(y=>x,x=>y)" by using the "intro" axiom of "is_equal". Since the premises are not more complicated than the current goal, the proof engine issues this command which leads to the state

x=y : y=>x, x=>y

At this point of the iteration the command "premise(x=y)" succeeds by using the "elim2" axiom of "is_equal.

x=y : x=y, x=>y

The current goal can be discharged immediately by issuing a "remove".

x=y : x=>y

The remaining steps are just a repetition of the above steps by using the axiom "elim1" instead of "elim2".

The transitivity law of "is_equal"

x=y => y=z => x=z

still remains to be proved. The reader is encouraged to follow the above procedure and mimick the steps done by the command "resolve". By doing this it becomes clear that the proof engine can proof this assertion automatically.

If an assertion does not have an explicit proof, the proof engine tries to prove it by using the command "resolve". Therefore assertions which can be proved automatically by the proof engine do not need a proof. It is sufficient to state the assertions. I.e. for reflexivity, symmetry and transitivity of "is_equal" it is sufficient to write

all(x,y,z: like Current) check x=x x=y => y=x x=y => y=z => x=>z end

Even this is not necessary in the case of "is_equal" of the class BOOLEAN. The assertions are already stated in the parent class COMPARABLE. Since BOOLEAN redefines "is_equal" these assertion loose their axiom status and the proof engine expects a proof. Since no explicit proof is provided it tries "resolve" and succeeds.

Therefore it is sufficient to provide as a definition of "is_equal"

is_equal(o:BOOLEAN): BOOLEAN external "built_in" ensure all(a,b:BOOLEAN) check intro: (a=>b) => (b=>a) => a=b elim1: a=b => (a=>b) elim2: a=b => (b=>a) end end

and the inherited contracts for reflexivity, symmetry and transitivity are proved by the proof engine automatically.

The boolean operator "and" is defined in the class BOOLEAN as

conjuncted alias "and" (o:BOOLEAN): BOOLEAN external "built_in" ensure all(a,b:BOOLEAN) check intro: a => b => a and b elim1: a and b => a elim2: a and b => b end end

The postconditions are treated by proof engine as axioms, because the function "and" is a builtin function. These axioms coincide well with our intuition about the "and" operation.

In order to prove that "a and b" is true it is sufficient to prove that "a" and "b" are true. I.e. the validity of "a" and "b" implies the validity of "a and b".

On the other hand from the truth of "a and b" the truth of "a" and "b" can be safely concluded.

These axioms are sufficient to prove the commutativity of "and".

all(a,b:BOOLEAN) check comm1: a and b => b and a proof enter premise(b,a) -- using "intro" -- a and b : b, a premise(a and b) -- using "elim2" remove premise(a and b) -- using "elim1" remove end comm2: (a and b) = (b and a) end

The assertion "comm1" needs an explicit proof because the command "premise(a and b)" makes the goal more complicated and therefore cannot be issued by the proof engine automatically. However the assertion "comm2" does not need an explicit proof, because it can be proved automatically by using the above described procedure for the command "resolve".

The reader is strongly encouraged to prove "comm2" by hand mimicking the steps of the command "resolve" in order to get a good intuition on how the command "resolve" works.

In the chapter "Implications" it has been stated that "a=>b=>c" and "a and b => c" are equivalent without giving a formal proof. Now we have enough machinery to give the proof.

all(a,b,c:BOOLEAN) check curry: (a and b => c) => (a=>b=>c) proof enter(3) -- a and b => c, a, b : c premise(a and b) resolve end uncurry: (a=>b=>c) => (a and b => c) proof enter(2) -- a=>b=>c, a and b : c premise(a,b) premise(a and b); remove -- semicolon separates premise(a and b); remove -- commands on the same line end equiv: (a and b => c) = (a=>b=>c) end

The command "resolve" shortens the proof of "curry" and removes some of the mechanical steps. The assertion "equiv" does not need any explicit proof, because the implicit "resolve" does all the work. Just the proof of "uncurry" has to be entered fully, because it needs two times the command "premise(a and b)" which makes the current goal more complicated.

The boolean operator "or" is defined in the class BOOLEAN as

disjuncted alias "or" (o:BOOLEAN): BOOLEAN external "built_in" ensure all(a,b,c:BOOLEAN) check intro1: a => a or b intro2: b => a or b elim: (a or b) => (a=>c) => (b=>c) => c end end

The two introduction axioms state: In order to prove "a or b" it is sufficient two prove one of them.

The elimination axiom might be more difficult to understand at first glance. But it is quite logical. Let's assume that we want to prove some assertion "c". Furthermore it is possible to prove that "a=>c" and "b=>c". I.e. the truth of "a" implies the truth of "c" and the truth of "b" implies the truth of "c". If we can prove additionally that "a" or "b" is true, then we can conclude that "c" must be true as well.

The elimination axiom can be used to make proofs by case split. If we know from the assumptions or from already proved assertions that one of two assertions is true, we can prove our current goal by proving that the goal follows from each of the two alternatives.

In order to make proofs with case splits more readable we introduce the convenience command "case_split(a,b)". It is just a shorthand.

case_split(a,b) -- is a shorthand for (assuming that "c" is the current goal) premise(a or b, a=>c, b=>c) remove

I.e. in order to issue the command "case_split(a,b)" it is necessary that "a or b" is trivially true (i.e. can be removed immediately). With the comand "case_split" we can prove the commutativity of "or".

all(a,b:BOOLEAN) check comm1: a or b => b or a proof enter case_split(a,b) -- a or b : a=>(b or a), b=>(b or a) end comm2: (a or b) = (b or a) end

The proof of "comm1" leaves two goals on the goal stack. These goals are trivial to prove by "resolve". It is not necessary to write the command "resolve(2)" explicitly. If the manual proof stops with some open goals, the proof engine tries to proof the open goals by issuing a "resolve" command for each goal still to be proved.

The technique to use a case split is very important to master, because many proofs use this technique. The next chapter derives some distributivity laws of boolean algebra. These proofs can be used to get more practice with case splits.

From boolean algebra we know the distributivity laws

all(a,b,c:BOOLEAN) check (a and (b or c)) = ((a and b) or (a and c)) (a or (b and c)) = ((a or b) and (a or c)) end

Both laws are equivalences. This requires that we prove the forward and backward direction. Let us prove the forward direction of the distributivity law of "and".

all(a,b,c: BOOLEAN) check and_dist_fwd: a and (b or c) => (a and b) or (a and c) proof premise(a => (b or c) => (a and b) or (a and c)) enter(2) -- a, b or c : (a and b) or (a and c) case_split(b,c) -- a, b or c : b => (a and b) or (a and c), -- c => (a and b) or (a and c) enter; premise(a and b); resolve enter; premise(a and c); resolve end ... end

The first step is to "curry" the implication of the form "x and y => z" into the form "x=>y=>z". Then we shift two assumptions onto the assumption stack. Whenever we have an assumption of the form "a or b" we can try to issue "case_split(a,b)".

After the command "case_split(a,b)" we can shift "b" onto the assumption stack and prove "a and b" trivially. The second goal can be proved by shifting "c" onto the assumption stack and proving "a and c" trivially.

It is a good exercise to prove the backward direction of "and" and the forward and backward direction of "or" explicitly. The complete set of proofs is given in the appendix.

In this blog entry I have demonstrated how Modern Eiffel's proof engine can be used to proof some basic laws of propositional calculus.

The basic rules, commands and axioms are releatively simple. This is on purpose. If you construct a mechanical verifier for proofs there remains always the question "Is the proof engine correct?". Or better stated: "Can I trust proofs which pass the proof engine?".

The trusted base of the proof engine is just the rules of the basic commands and the axioms. Note that convenience commands like "case_split" and "resolve" just issue basic commands. As long as the basic commands are implemented correctly in the proof engine it is not possible to construct invalid proofs with the proof engine.

The careful reader might have noted that we have not yet talked about negation (i.e. the boolean operation "not"). This will be done in the next blog entry which will introduce this operation and proofs by contradiction.

deferred class COMPARABLE feature is_equal(o: like Current): BOOLEAN external "built_in" ensure all(x,y,z: like Current) check reflexive: x=x symmetric: x=y => y=x transitive: x=y => y=z => x=z end end end

immutable class BOOLEAN inherit COMPARABLE redefine is_equal end feature -- boolean operations implication alias "=>" (o:BOOLEAN): BOOLEAN external "built_in" end is_equal(o: BOOLEAN): BOOLEAN external "built_in" ensure all(a,b:BOOLEAN) check intro: (a=>b) => (b=>a) => a=b elim1: a=b => (a=>b) elim2: a=b => (b=>a) end end conjuncted alias "and" (o:BOOLEAN): BOOLEAN external "built_in" ensure all(a,b:BOOLEAN) check intro: a => b => a and b elim1: a and b => a elim2: a and b => b end end disjuncted alias "or" (o:BOOLEAN): BOOLEAN external "built_in" ensure all(a,b,c:BOOLEAN) check intro1: a => a or b intro2: b => a or b elim: (a or b) => (a=>c) => (b=>c) => c end end feature -- implication laws all(a,b,c: BOOLEAN) check reflexive: a => a modus_ponens: a => (a=>b) => b transitive: (a=>b) => (b=>c) => (a=>c) end feature -- commutativity of "and" all(a,b:BOOLEAN) check comm1: a and b => b and a proof enter; premise(b,a) premise(a and b); remove premise(a and b); remove end comm2: (a and b) = (b and a) end feature -- currying all(a,b,c: BOOLEAN) check curry: (a and b => c) => (a=>b=>c) proof enter(3); premise(a and b) end uncurry: (a=>b=>c) => (a and b => c) proof enter(2); premise(a,b) premise(a and b); remove premise(a and b); remove end equiv: (a and b) = (a=>b=>c) end feature -- commutativity of "or" all(a,b:BOOLEAN) check comm1: a or b => b or a proof enter; case_split(a,b) end comm2: (a or b) = (b or a) end feature -- distributivity of "and" all(a,b,c: BOOLEAN) check and_dist_fwd: a and (b or c) => (a and b) or (a and c) proof premise(a=>(b or c) => (a and b) or (a and c)) enter(2) -- a, b or c : (a and b) or (a and c) case_split(b,c) enter; premise(a and b); resolve enter; premise(a and c); resolve end and_dist_bwd: (a and b) or (a and c) => a and (b or c) proof enter premise(a, b or c) -- (a and b) or (a and c) : a, b or c -- goal a case_split(a and b, a and c) enter; premise(a and b); remove enter; premise(a and c); remove -- goal b or c case_split(a and b, a and c) enter; premise(b); premise(a and b); remove enter; premise(c); premise(a and c); remove end and_dist: ((a and b) or (a and c)) = (a and (b or c)) end feature -- distributivity of "or" all(a,b,c) check or_dist_fwd: a or (b and c) => (a or b) and (a or c) proof enter; premise(a or b, a or c) -- goal: a or b case_split(a, (b and c)) enter; resolve enter; premise(b), premise(b and c); remove -- goal: a or c case_split(a, (b and c)) enter; resolve enter; premise(c); premise(b and c); remove end or_dist_bwd: (a or b) and (a or c) => a or (b and c) proof premise((a or b) => (a or c) => a or (b and c)) enter(2) case_split(a,b) resolve enter; case_split(a,c) -- a or b, a or c, b : a => a or (b and c), c => a or (b and c) end or_dist: (a or (b and c)) = ((a or b) and (a or c)) end end

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