*How if I answer no?*"

-- Shakespeare, Hamlet

Act V, Scene II, Line 167

In The Little Prover we find the following Axioms of If:

(dethm if-true (x y)

(equal (if 't x y) x))

(dethm if-false (x y)

(equal (if 'nil x y) y)

(dethm if-same (x y)

(equal (if x y y) y)

(dethm if-nest-A (x y z)

(if x

(equal (if x y z) y)

't))

(dethm if-nest-E (x y z)

(if x

't

(equal (if x y z) z)))

The way I learn best is by

Looking at if-true we see that if we have a true

*premise*that we always take the

*answer*part of the if.

(if

*premise*

*answer*

*else*)

This is not a shock to anyone, but is very useful.

Moving on we see if-false states that if we have a false

*premise*that we always take the

*else*part of the if. Again nothing shocking but very useful.

Next we see if-same which states that if the

*answer*and

*else*are the same then the

*premise*does not matter. This makes complete logical sense, but I'll admit I never really thought of it before.

Now let us look at if-nest-A which states that if the condition is true in the

*premise*then it must be true in the

*answer*part. This is very awesome, we can now eliminate code by simply looking for redundant ifs. We see this in the following:

given

**x**is true

(if

**x**

(if

**x**:yep :nope)

:nope)))))

We see that we have the(if

*what-ever*in the outside which matches the (if

*what-ever*in the

*answer*part thus we can eliminate it pulling it up (in the code above the :yep), since if the

*premise*is true on the outside it is true on the inside. This axiom is very useful in refactoring code and I figured it out for myself a long time ago and find myself using it all the time, it is nice to know that it has a solid theoretical basis.

Last we see the anti of if-nest-A, if-nest-E. if-nest-E states that if the condition is false in the

*premise*then it must be false in the

*else*part. We see this in the following:

given

**x**is false

(if

**x**

:nope

(if

**x**:nope :yep))

We see that we have the (if

*what-ever*in the outside which matches the (if

*what-ever*in the

*else*part thus we can eliminate it pulling it up (in the code above the :yep), since if the

*premise*is false on the outside it is false on the inside. Again, this is very useful in eliminating code.

These axioms are very powerful and I would argue are more useful than tests. If this interests you I would recommend reading The Little Prover or working your way through the flying tour of ACL2.