Data.SBV.Examples.Uninterpreted.Function

Demonstrates function counter-examples

Documentation

f :: SWord8 -> SWord8 -> SWord16

An uninterpreted function

thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool

Asserts that f x z == f (y+2) z whenever x == y+2. Naturally correct.

thmBad :: SWord8 -> SWord8 -> SBool

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:

 ghci> prove thmBad
 Falsifiable. Counter-example:
   s0 = 0 :: SWord8
   s1 = 128 :: SWord8
   -- uninterpreted: f
        f 128 0 = 32768
        f _ _ = 0

Note how the counterexample function f returned by Yices violates commutativity; thus providing evidence that the asserted theorem is not valid.