SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/proof engine

Introduction to the proof engine

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

The kind of assertions to prove

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.

Implications

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

The state of the proof engine

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.

Three basic commands to manipulate the state of the proof engine

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

Enter

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

Remove

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 
 

Premise

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

Some simple proofs

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
 

Other boolean operators

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.

Equality

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.

Automation

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:

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.

Conjunction

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.

Disjunction

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.

Distributivity laws

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.

Summary

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.

Appendix

The class COMPARABLE

  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
 

The class BOOLEAN

  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
 

Emacs suffix

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

- The kind of assertions to prove

- Implications

- The proof engine

- The state of the proof engine

- Three basic commands to manipulate the state of the proof engine

- Enter

- Remove

- Premise

- Some simple proofs

- Other boolean operators

- Equality

- Automation

- Conjunction

- Disjunction

- Distributivity laws

- Summary

- Appendix

- The class COMPARABLE

- The class BOOLEAN

- Emacs suffix


ip-location