-----------------------------------------------------------------------------
-- |
-- 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        #-}
{-# LANGUAGE TypeAbstractions #-}

{-# 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 :: IO (Proof (Forall "n" Integer -> SBool))
notDiv3 = TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "n" Integer -> SBool))
 -> IO (Proof (Forall "n" Integer -> SBool)))
-> TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$ do

   let s :: a -> a
s a
n = a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
n a -> a -> a
forall a. Num a => a -> a -> a
* a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
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.
   String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"notDiv3"
        (\(Forall SBV Integer
n) -> SBV Integer -> SBV Integer
forall {a}. Num a => a -> a
s SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Integer
0) (StepArgs (Forall "n" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
        \SBV Integer
n -> [] [SBool]
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Integer -> SBV Integer
forall {a}. Num a => a -> a
s SBV Integer
n
                 SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw (SBV Integer))] -> TPProofRaw (SBV Integer)
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
0 SBool
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Integer -> SBV Integer
forall {a}. Num a => a -> a
s (SBV Integer
0 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
3 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* String -> (SBV Integer -> SBool) -> SBV Integer
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Integer
k -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
0 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
3 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
k)) SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed
                          , SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
1 SBool
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Integer -> SBV Integer
forall {a}. Num a => a -> a
s (SBV Integer
1 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
3 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* String -> (SBV Integer -> SBool) -> SBV Integer
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Integer
k -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
1 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
3 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
k)) SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed
                          , SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
`sEMod` SBV Integer
3 SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
2 SBool
-> TPProofRaw (SBV Integer) -> (SBool, TPProofRaw (SBV Integer))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV Integer -> SBV Integer
forall {a}. Num a => a -> a
s (SBV Integer
2 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
3 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* String -> (SBV Integer -> SBool) -> SBV Integer
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" (\SBV Integer
k -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
2 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
3 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
* SBV Integer
k)) SBV Integer -> ChainsTo (SBV Integer) -> ChainsTo (SBV Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Integer)
TPProofRaw (SBV Integer)
forall a. TPProofRaw a
qed
                          ]