CaseSplit.hs

-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.CaseSplit
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Use TP to prove @2n^2 + n + 1@ is never divisible by @3@.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.CaseSplit where

import Data.SBV
import Data.SBV.TP

-- | Prove that @2n^2 + n + 1@ is not divisible by @3@.
--
-- We have:
--
-- >>> notDiv3
-- Lemma: notDiv3
--   Step: 1 (3 way case split)
--     Step: 1.1               Q.E.D.
--     Step: 1.2               Q.E.D.
--     Step: 1.3               Q.E.D.
--     Step: 1.Completeness    Q.E.D.
--   Result:                   Q.E.D.
-- [Proven] notDiv3 :: Ɐn ∷ Integer → Bool
notDiv3 :: IO (Proof (Forall "n" Integer -> SBool))
notDiv3 = runTP $ do

   let s n = 2 * n * n + n + 1

   -- Do a case-split for each possible outcome of @s n `sEMod` 3@. In each case
   -- we get the witness that is guaranteed to exist by the case condition, and rewrite
   -- @s n@ accordingly. Once this is done, z3 can figure out the rest by itself.
   calc "notDiv3"
        (\(Forall n) -> s n `sEMod` 3 ./= 0) $
        \n -> [] |- s n
                 =: cases [ n `sEMod` 3 .== 0 ==> s (0 + 3 * some "k" (\k -> n .== 0 + 3 * k)) =: qed
                          , n `sEMod` 3 .== 1 ==> s (1 + 3 * some "k" (\k -> n .== 1 + 3 * k)) =: qed
                          , n `sEMod` 3 .== 2 ==> s (2 + 3 * some "k" (\k -> n .== 2 + 3 * k)) =: qed
                          ]