KD: Case-split example

Documentation/SBV/Examples/KnuckleDragger/CaseSplit.hs

@@ -0,0 +1,91 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.CaseSplit
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- Use KnuckleDragger to prove @2n^2 + n + 1@ is never divisible by @3@.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE CPP              #-}
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE TypeAbstractions #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.CaseSplit where
+
+import Prelude hiding (sum, length)
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+
+-- | The default settings for z3 have trouble running this proof out-of-the-box.
+-- We have to pass auto_config=false to z3!
+z3NoAutoConfig :: KDConfig
+z3NoAutoConfig = z3KD{kdExtraSolverArgs = ["auto_config=false"]}
+
+-- | Prove that @2n^2 + n + 1@ is not divisible by @3@.
+--
+-- We have:
+--
+-- >>> notDiv3
+-- Chain: case_n_mod_3_eq_0
+--   Lemma: case_n_mod_3_eq_0.1            Q.E.D.
+--   Lemma: case_n_mod_3_eq_0.2            Q.E.D.
+-- Lemma: case_n_mod_3_eq_0                Q.E.D.
+-- Chain: case_n_mod_3_eq_1
+--   Lemma: case_n_mod_3_eq_1.1            Q.E.D.
+--   Lemma: case_n_mod_3_eq_1.2            Q.E.D.
+-- Lemma: case_n_mod_3_eq_1                Q.E.D.
+-- Chain: case_n_mod_3_eq_2
+--   Lemma: case_n_mod_3_eq_2.1            Q.E.D.
+--   Lemma: case_n_mod_3_eq_2.2            Q.E.D.
+-- Lemma: case_n_mod_3_eq_2                Q.E.D.
+-- Lemma: notDiv3                          Q.E.D.
+notDiv3 :: IO Proof
+notDiv3 = runKDWith z3NoAutoConfig $ do
+
+   let s n = 2 * n * n + n + 1
+       p n = s n `sEMod` 3 ./= 0
+
+   -- Do the proof in 3 phases; one each for the possible value of n `mod` 3 being 0, 1, and 2
+   -- Note that we use the euclidian definition of division/modulus.
+
+   -- Case 0: n = 0 (mod 3)
+   case0 <- chainLemma "case_n_mod_3_eq_0"
+                       (\(Forall @"n" n) -> (n `sEMod` 3 .== 0) .=> p n)
+                       (\n -> let k = n `sEDiv` 3
+                              in [ n `sEMod` 3 .== 0
+                                 , n .== 3 * k
+                                 , s n .== s (3 * k)
+                                 ])
+                       []
+
+   -- Case 1: n = 1 (mod 3)
+   case1 <- chainLemma "case_n_mod_3_eq_1"
+                       (\(Forall @"n" n) -> (n `sEMod` 3 .== 1) .=> p n)
+                       (\n -> let k = n `sEDiv` 3
+                              in [ n `sEMod` 3 .== 1
+                                 , n .== 3 * k + 1
+                                 , s n .== s (3 * k + 1)
+                                 ])
+                       []
+
+   -- Case 2: n = 2 (mod 3)
+   case2 <- chainLemma "case_n_mod_3_eq_2"
+                       (\(Forall @"n" n) -> (n `sEMod` 3 .== 2) .=> p n)
+                       (\n -> let k = n `sEDiv` 3
+                              in [ n `sEMod` 3 .== 2
+                                 , n .== 3 * k + 2
+                                 , s n .== s (3 * k + 2)
+                                 ])
+                       []
+
+   -- Note that z3 is smart enough to figure out the above cases are complete, so
+   -- no extra completeness helper is needed.
+   lemma "notDiv3"
+         (\(Forall @"n" n) -> p n)
+         [case0, case1, case2]

sbv.cabal

@@ -155,6 +155,7 @@ Library
                   , Documentation.SBV.Examples.Lists.BoundedMutex
                   , Documentation.SBV.Examples.Lists.CountOutAndTransfer
                   , Documentation.SBV.Examples.KnuckleDragger.AppendRev
+                  , Documentation.SBV.Examples.KnuckleDragger.CaseSplit
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen