Introduction to the proof engine

In the previous blog entry the outline of Modern Eiffel has been described. In this blog entry I’m going to talk about proofs of assertions involving boolean expressions with the help of Modern Eiffel’s proof engine.

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” dischargesthe 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 be proved 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.

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:

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

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 for the
following commands

  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 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
About these ads
  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

Follow

Get every new post delivered to your Inbox.

Join 33 other followers

%d bloggers like this: