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