Portability | portable |
---|---|

Stability | experimental |

Maintainer | erkokl@gmail.com |

Demonstrates function counter-examples

# Documentation

thmGood :: SWord8 -> SWord8 -> SWord8 -> SBoolSource

Asserts that `f x z == f (y+2) z`

whenever `x == y+2`

. Naturally correct:

`>>>`

Q.E.D.`prove thmGood`

thmBad :: SWord8 -> SWord8 -> SBoolSource

Asserts that `f`

is commutative; which is not necessarily true!
Indeed, the SMT solver (Yices in this case) returns a counter-example
function that is not commutative. We have:

`>>>`

Falsifiable. Counter-example: x = 0 :: SWord8 y = 128 :: SWord8 -- uninterpreted: f f 128 0 = 32768 f _ _ = 0`prove $ forAll ["x", "y"] thmBad`

Note how the counterexample function `f`

returned by Yices violates commutativity;
thus providing evidence that the asserted theorem is not valid.