Tactics.hs

import Data.SBV

p :: Bool -> Predicate
p bug = do
    a <- sInteger "a"
    b <- sInteger "b"

    -- We'll do our proof with a two-level case split. First on 'a', then on 'b'
    -- The conditions are rather arbitrary for illustrative examples here. But they
    -- are arbitrary SBool's, so you can code anything you want.

    -- Note that the conditions need not be mutually exclusive, nor cover the whole space
    -- SBV will prove all the cases, and then will generate a coverage claim to make
    -- sure everything is covered

    -- Sub-case split on B.
    let mkBLessThan i = ("b < " ++ show i, b .< literal i, [])

    -- Case-split on A. Note that we want the sub-case split on B to execute in parallel,
    -- so we put the 'ParallelCase' tactic in the list
    let mkALessThan i = ("a < " ++ show i, a .< literal i, [ CaseSplit True (map mkBLessThan [5, 10])
                                                           , ParallelCase
                                                           ])

    -- Tell SBV to case split to 4 cases:
    --       a < 10
    --       a < 100
    --       a < 200
    --       Coverage (when none of the above is true)
    -- Note that the conditions are neither mutually exclusive nor fully covering
    -- SBV will do the right thing. (Of course, you can make the conditions
    -- mutually exclusive, there's nothing wrong with that.)
    --
    -- The first argument to CaseSplit (boolean) controls verbosity
    tactic $ CaseSplit True (map mkALessThan [10, 100, 200])

    -- We can also execute top-level cases in parallel. But "two-levels of parallel"
    -- gets confusing. Uncomment the following line to execute the top-split in parallel too
    -- SBV will do the right thing!
    -- tactic ParallelCase

    -- Let's prove a .> b ==> abs (a - b) .== a - b
    -- But! insert a bug when a is 75, if we're so instructed
    let bogus | bug  = a ./= 75
              | True = true

    return $ bogus &&& (a .> b ==> abs (a - b) .== a - b)

-- Note that tactics work for both sat and prove calls.. Some variations below
main :: IO ()
main = do line "Proof will fail"
          print =<< prove (p True)
          line "Proof will pass"
          print =<< prove (p False)
          line "Sat will pass, but never with 75!"
          print =<< sat   (p True)
          line "Sat will pass"
          print =<< sat   (p False)
  where line w = putStrLn $ "= " ++ w ++ " " ++ replicate 30 '='

{-
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /Users/LeventErkok/.ghci
[1 of 1] Compiling Main             ( f.hs, interpreted )
Ok, modules loaded: Main.
= Proof will fail ==============================
>> Case 1: a < 10   [Starting]
>>>> Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Proved]
<< Case 1: a < 10   [Proved]
>> Case 2: a < 100  [Starting]
>>>> Cases 2.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 2.[1-3]: Parallel case split: 2 cases and coverage: [Failed (Case 2.2: b < 10)]
<< Case 2: a < 100  [Failed]
Falsifiable. Counter-example:
  a = 75 :: Integer
  b =  0 :: Integer
= Proof will pass ==============================
>> Case 1: a < 10   [Starting]
>>>> Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Proved]
<< Case 1: a < 10   [Proved]
>> Case 2: a < 100  [Starting]
>>>> Cases 2.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 2.[1-3]: Parallel case split: 2 cases and coverage: [Proved]
<< Case 2: a < 100  [Proved]
>> Case 3: a < 200  [Starting]
>>>> Cases 3.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 3.[1-3]: Parallel case split: 2 cases and coverage: [Proved]
<< Case 3: a < 200  [Proved]
>> Coverage X [Starting]
<< Coverage X [Proved]
Q.E.D.
= Sat will pass, but never with 75! ==============================
>> Case 1: a < 10   [Starting]
>>>> Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Satisfiable (Case 1.2: b < 10)]
<< Case 1: a < 10   [Satisfiable]
Satisfiable. Model:
  a =  0 :: Integer
  b = -1 :: Integer
= Sat will pass ==============================
>> Case 1: a < 10   [Starting]
>>>> Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Starting]
<<<< Cases 1.[1-3]: Parallel case split: 2 cases and coverage: [Satisfiable (Case 1.2: b < 10)]
<< Case 1: a < 10   [Satisfiable]
Satisfiable. Model:
  a =  0 :: Integer
  b = -1 :: Integer
Leaving GHCi.
-}