The Eiffel Compiler / Interpreter (tecomp)

The last blog entry gave an introduction to Modern Eiffel's proof engine. The basic rules have been explained, the boolean operations "=>", "and" and "or" have been introduced with their corresponding axioms and some proofs have been given for expressions using these operations. The class BOOLEAN up to now looks like

immutable class BOOLEAN inherit COMPARABLE redefine is_equal end feature implication alias "=>" (o:BOOLEAN): BOOLEAN ... is_equal (o:BOOLENA): BOOLEAN ... conjuncted alias "and" (o:BOOLEAN): BOOLEAN ... disjuncted alias "or" (o:BOOLEAN): BOOLEAN ... all(a,b,c: BOOLEAN) check reflexivity: a => a modus_ponens: a => (a=>b) => b transitivity: (a=>b) => (b=>c) => (a=>c) reorder: (a=>b=>c) => (b=>a=>c) end ... -- some more proved assertions end

In this blog entry the boolean operation "not" and its axioms will be introduced into the class BOOLEAN which open up the world of proofs by contradiction.

The concept of negation is strongly related to the concept of contradiction. If we say that some statement "a" is wrong (expressed as "not a") we can prove it in the following manner. We assume that "a" is valid and derive from this assumption something which is inacceptable, i.e. something which is definitely false e.g. a contradiction. Since the assumption of "a" leads us to something unacceptable we can safely conclude that "a" must be false. I.e. our proof is a refutation of "a".

This basic idea is expressed in the axioms of negation.

negated alias "not": BOOLEAN external "built_in" ensure all(a:BOOLEAN) check intro: (a => False) => not a elim: a => not a => False indirect: (not a => False) => a end end

Recall that postconditions of built-in functions are accepted by the proof engine without proof, i.e. they are treated as axioms.

The boolean constant "False" represents something which cannot be true.

The first axiom "intro" states the following: In order to prove that something (i.e. "a") is false it is sufficient to show that the assumption of "a" leads to "False".

The corresponding "elim" axiom states the opposite direction. If something (i.e. "a") is valid then the assumption that "a" is wrong leads to "False".

The axiom "elim" is written in this form because it is convenient in the following chapters. But in order to see the symmetry between "intro" and "elim" we can write "elim" in the form "not a => (a => False)". It is easy to prove that the second form is valid as well (just use some trivial "enter" and "premise" commands).

Note that the axioms "intro" and "elim" together postulate the fact that "not a" and "a=>False" are equivalent. Many textbooks about logic do not introduce "not" as an independent operation. They define "not a" by being equivalent to "a=>False".

In the "elim" axiom "False" occurs on the right hand side of an implication. This means that we can derive "False" if we have some contradictory assumptions (the premises of "False" are "a" and "not a").

The axiom "indirect" opens up the possibility to proof an assertion "a" indirectly. Instead to prove "a" directly we can assume "not a" and derive "False" from it.

The law of double negation states that "a" and "not not a" are equivalent. We can proof this law using the axioms of negation.

all(a:BOOLEAN) check fwd: a => not not a proof enter premise(not a => False) -- using "intro" enter -- a, not a : False premise(a, not a) end bwd: not not a => a proof enter premise(not a => False) -- using "indirect" enter -- not not a, not a: False premise(not a, not not a) end equiv: a = not not a end

The proofs are not difficult. But it is worthwhile to go through some of them step by step. In order to prove "a => not not a" we issue "enter" which leads to the state

a : not not a

with the current goal "not not a". I.e. we want to prove that "not a" is wrong. In order to do this we use the axiom "intro" and assume that "not a" leads to "False". After the next "enter" we reach

a, not a: False

i.e. we have to prove "False" using the assumptions. From the axiom "elim" we know that we can prove "False" if we have some contradiction. In the assumptions we have already the contradiction "a" and "not a". Therefore the command "premise(a, not a)" leads to the state

a, not a: a, not a

Both goals are discharged automatically by the proof engine using implicitely two removes.

The proof of "not not a => a" has the same structure. It uses the axiom "indirect" instead of the axiom "intro".

After having a proof for "a => not not a" and "not not a => a" the proof engine can derive a proof of "a = not not a" automatically.

Proofs by contradiction usually have a certain pattern. The current goal is transformed into an implication with "False" on the right hand side by using either the "intro" or the "indirect" axiom. Then the assumption on the left hand side of the implication is shifted onto the assumption stack. Then the current goal "False" is proved by some contradiction using the axiom "elim".

The command "contradiction" is introduced to give a shorthand for this pattern and enhance the readability of proofs by contradiction.

-- shorthand for -- state before: ... : not x ... contradiction(y) premise(x=>False) enter premise(y,not y) -- state after: ... x: y, not y ... -- state before: ... : x ... contradiction(y) premise(not x=>False) enter premise(y,not y) -- state after: ... not x: y, not y ...

We can redo the proofs of double negation using the command "contradiction".

all(a:BOOLEAN) check a => not not a proof enter; contradiction(a) end not not a => a proof enter; contradiction(not a) end a = not not a end

The proofs are more concise and communicate better the proof idea.

Since "contradiction" uses only the basic commands "premise" and "enter" it is like "case_split" (see previous blog entry) a convenience command.

We can use the command "contradicton" to prove that (a and not a) is not valid.

all(a:BOOLEAN) check contradiction: not (a and not a) proof contradiction(a) premise(a and not a); remove premise(a and not a); remove end end

If we start reasoning we should not make false assumptions, because with false assumptions everything breaks down. The corresponding laws of logic tells us that "from a false assumptions follows everything" (or in latin "ex falso quodlibet") and that "from a contradiction follows everything" (in latin "ex contradictio quodlibet").

We can prove these two laws with the proof engine by issuing some simple commands.

all(a,b:BOOLEAN) check ex_falso: False => a proof enter; premise(not a => False); enter; remove end ex_contradictio: a => not a => b proof enter(2); premise(False); premise(a,not a); remove(2) end end

Note how the second proof uses the already proved assertion "ex_falso" with the command "premise(False)". We could have proved the assertion "ex_contradictio" directly like

a => not a => b proof enter(2) premise(not b => False) enter premise(a, not a) remove(2) end

This proof is just one command longer than the above given proof. Therefore we have not gained a lot in the first proof by using "ex_falso". But you should keep in mind that the proof engine allows us to modularize our proofs. We can first proof simpler assertions and combine them to proof more complex assertions.

Let's assume that "a=>b" is a valid assumption, i.e. "a" is stronger than "b". If we know additionally that "b" is not true, we conclude that "a" cannot be true either. Why? If "a" were true, then "b" must be true as well which contradicts the fact that "b" is false.

This line or reasoning is used to prove the four possible contrapositive laws of implication.

all(a,b:BOOLEAN) check contra1: (a=>b) => not b => not a proof enter(2); contradiction(b) -- a=>b, not b, a : b, not b end contra2: (not a => not b) => b => a proof enter(2); contradiction(b) -- not a => not b, b, not a : b, not b end contra3: (a => not b) => b => not a proof enter(2); contradiction(b) -- a => not b, b, a : b, not b end contra4: (not a => b) => not b => a proof enter(2); contradiction(b) -- not a => b, not b, not a : b, not b premise(not a) end end

There are two "De Morgan" laws in logic. One for the operator "or" and one for the operator "and".

all(a,b:BOOLEAN) check de_morgan_or: not (a or b) = not a and not b de_morgan_and: not (a and b) = not a or not b end

Our intuition tells us, that these laws are valid.

The expression "a or b" can only be false if both "a" and "b" are false. Otherwise "a or b" would be true.

The expression "a and b" is false, if "a" or "b" is false. If both are true, "a and b" is true and therefore cannot be false. In the following we use the proof engine to verify the assertions.

The reader is encouraged to try to proof De Morgan's laws before reading further.

The first trials to proof De Morgan's laws usually end up with some complicated looking proofs. In the following some basic techniques are explained to keep the proofs simple and readable.

Before trying to proof De Morgan's laws let us analyze the structure of the laws. The laws are boolean equivalences. Therefore it is necessary to prove the forward and the backward direction. It is convenient to state the forward and backward direction as separate assertions, because the proof engine can proof an equivalence automatically using an implicit "resolve" if the forward and backward direction is given. Therefore we state

fwd: not (a or b) => not a and not b bwd: not a and not b => not (a or b)

The forward direction has an expression of the form "x and y" on the right hand side of an implication. The usual command sequence "enter; premise(x,y)" enter a state where we have the goals "not a" and "not b" as two separate goals still to be proved. Both must follow from the assumption "not (a or b)". Why not state them as separate assertions?

lemma1: not (a or b) => not a lemma2: not (a or b) => not b

If we analyze the structure we see that both lemmas fit the pattern "not x => not y". In the previous chapter "contrapositive" we have already proved "(y=>x) => (not x => not y)" (parentheses around the last implication are not necessary, but have been inserted to see the structure better). I.e. we can apply the command "premise(a => a or b)" to the first lemma which leaves us with a trivial goal on the goal stack.

Since the command "premise(a => a or b)" transforms the current goal "not (a or b) => not a" into a simpler one, the proof engine will issue this command automatically. I.e. no explicit proof is necessary for "lemma1". The same reasoning applies to "lemma2".

Having "lemma1" and "lemma2" let the proof engine prove "fwd" automatically as well. The commands "enter; premise(not a, not b); remove(2)" will be issued by the implicit resolve command.

Now let us look at the backward direction

bwd: not a and not b => not (a or b)

This assertion has the structure "x and y => z". From the previous blog entry we have already proved that this follows from "x=>y=>z". We can state the backward direction in the curried form as another lemma and prove it.

lemma3: not a => not b => not (a or b) proof enter(2); premise(a or b => False); enter -- not a, not b, a or b : False case_split(a,b) enter; premise(a, not a); remove(2) enter; premise(b, not b); remove(2) end

This is the only necessary explicit proof. The following code is sufficient to proof De Morgan's law for "or".

de_morgan_or: all(a,b:BOOLEAN) check lemma1: not (a or b) => not a lemma2: not (a or b) => not b fwd: not (a or b) => not a and not b lemma3: not a => not b => not (a or b) proof enter(2); premise(a or b => False); enter -- not a, not b, a or b : False case_split(a,b) enter; premise(a, not a); remove(2) enter; premise(b, not b); remove(2) end bwd: not a and not b => not (a or b) law: not (a or b) = (not a and not b) end

I have to admit that all my first proofs of this law have been much more complicated. This happened because I did not analyze the structure of the assertions and I did not use the previously proved assertions. It takes some time improve this skill, but it pays off as you see above.

The possibilities of the (implicit) command "resolve" are not very powerful. There are other theorem provers with much more sophisticated search strategies to find a proof for a theorem. However even the limited automation features of "resolve" might sometimes surprise.

If you write the proofs in a way which uses fully the capabilities of "resolve" the reader of your proofs might not be able to follow your line of reasoning. Therefore it might be useful to write more explicit proof commands instead of letting the proof engine derive them. It is a matter of taste how much proof commands you write. But it is a good guideline to code the proof explicitely until the remaining steps are really trivial.

Therefore I would prefer to make the first step to proof "lemma1" and "lemma2" explicit.

de_morgan_or: all(a,b:BOOLEAN) check lemma1: not (a or b) => not a proof premise(a => a or b) end lemma2: not (a or b) => not b proof premise(b => a or b) end ... -- other assertions as before end

The following code snippet gives a proof for the second of De Morgan's laws. It uses just one lemma to keep the proofs compact. The proofs make some steps explicit which could be done by the proof engine automatically. The reader is encouraged to find out the commands which could have been derived automatically.

de_morgan_and: all(a,b:BOOLEAN) check lemma: not not a and not not b => a and b proof premise(not not a => not not b => a and b) enter(2) premise(a,b) -- not not a, not not b: a, b premise(not not a); remove premise(not not b); remove end fwd: not (a and b) => not a or not b proof premise(not (not a or not b) => a and b) enter premise(not not a and not not b) premise(not (not a or not b)) remove end bwd: not a or not b => not (a and b) proof premise(a and b => not (not a or not b)) premise(a => b => not (not a or not b)) enter(2) -- a, b : not (not a or not b) premise(not not a and not not b) end law: not (a and b) = (not a or not b) end

For completeness we add a proof of the "excluded middle".

all(a:BOOLEAN) check a or not a proof contradiction(not a) -- not (a or not a) : not a, not not a premise(not (a or not a)); remove premise(not (a or not a)); remove end end

This and the previous blog entry have been dedicated to the propositional calculus. It has been shown how the proof engine can be used to proof all basic laws of logic.

This is possible with a few axioms introduced in the basic operations for conjunction, disjunction, equality and negation and just a handful of proof commands with their corresponding rules.

-- basic commands remove -- remove the current goal premise(p1,p2,...) -- substitute the current goal by the set p1, p2, ... enter -- shift an assumption onto the assumption stack -- convenience commands case_split(a,b) -- use a case split where "a or b" must be valid contradiction(a) -- show that the negation of the current goal leads -- to the contradiction "a and not a" -- automation resolve -- issue the commands "remove", "enter", "premise" -- repeatedly as long the goal does not get more -- complicated (depth of the expression tree)

But propositional calculus is not sufficient for computer programs. Computer programs shall do some useful calculations and execute some useful actions. In the following blog entries more calculations will be introduced hand in hand with the appropriate verification techniques.

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