-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Basics
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Some basic TP usage.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Basics where

import Prelude hiding(reverse, length, elem)

import Data.SBV
import Data.SBV.List
import Data.SBV.TP

import Control.Monad (void)

#ifdef DOCTEST
-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> :set -XTypeApplications
-- >>> import Data.SBV
-- >>> import Data.SBV.TP
-- >>> import Control.Exception
#endif

-- * Truth and falsity

-- | @sTrue@ is provable.
--
-- We have:
--
-- >>> trueIsProvable
-- Lemma: true                             Q.E.D.
-- [Proven] true :: Bool
trueIsProvable :: IO (Proof SBool)
trueIsProvable :: IO (Proof SBool)
trueIsProvable = TP (Proof SBool) -> IO (Proof SBool)
forall a. TP a -> IO a
runTP (TP (Proof SBool) -> IO (Proof SBool))
-> TP (Proof SBool) -> IO (Proof SBool)
forall a b. (a -> b) -> a -> b
$ String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"true" SBool
sTrue []

-- | @sFalse@ isn't provable.
--
-- We have:
--
-- >>> falseIsn'tProvable `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: sFalse
-- *** Failed to prove sFalse.
-- Falsifiable
falseIsn'tProvable :: IO ()
falseIsn'tProvable :: IO ()
falseIsn'tProvable = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Proof SBool
_won'tGoThrough <- String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"sFalse" SBool
sFalse []
        () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- * Quantification

-- | Basic quantification example: For every integer, there's a larger integer.
--
-- We have:
-- >>> largerIntegerExists
-- Lemma: largerIntegerExists              Q.E.D.
-- [Proven] largerIntegerExists :: Ɐx ∷ Integer → ∃y ∷ Integer → Bool
largerIntegerExists :: IO (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
largerIntegerExists :: IO (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
largerIntegerExists = TP (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
-> IO (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
 -> IO (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool)))
-> TP (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
-> IO (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "x" Integer -> Exists "y" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Integer -> Exists "y" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"largerIntegerExists"
                                    (\(Forall SInteger
x) (Exists SInteger
y) -> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
y)
                                    []

-- * Basic connectives

-- | Pushing a universal through conjunction. We have:
--
-- >>> forallConjunction @Integer (uninterpret "p") (uninterpret "q")
-- Lemma: forallConjunction                Q.E.D.
-- [Proven] forallConjunction :: Bool
forallConjunction :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO (Proof SBool)
forallConjunction :: forall a.
SymVal a =>
(SBV a -> SBool) -> (SBV a -> SBool) -> IO (Proof SBool)
forallConjunction SBV a -> SBool
p SBV a -> SBool
q = TP (Proof SBool) -> IO (Proof SBool)
forall a. TP a -> IO a
runTP (TP (Proof SBool) -> IO (Proof SBool))
-> TP (Proof SBool) -> IO (Proof SBool)
forall a b. (a -> b) -> a -> b
$ do
    let qb :: (Forall Any a -> SBool) -> SBool
qb = (Forall Any a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"forallConjunction"
           (      ((Forall Any a -> SBool) -> SBool
qb (\(Forall SBV a
x) -> SBV a -> SBool
p SBV a
x) SBool -> SBool -> SBool
.&& (Forall Any a -> SBool) -> SBool
qb (\(Forall SBV a
x) -> SBV a -> SBool
q SBV a
x))
            SBool -> SBool -> SBool
.<=> -------------------------------------------------------
                          (Forall Any a -> SBool) -> SBool
qb (\(Forall SBV a
x) -> SBV a -> SBool
p SBV a
x SBool -> SBool -> SBool
.&& SBV a -> SBool
q SBV a
x)
           )
           []

-- | Pushing an existential through disjunction. We have:
--
-- >>> existsDisjunction @Integer (uninterpret "p") (uninterpret "q")
-- Lemma: existsDisjunction                Q.E.D.
-- [Proven] existsDisjunction :: Bool
existsDisjunction :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO (Proof SBool)
existsDisjunction :: forall a.
SymVal a =>
(SBV a -> SBool) -> (SBV a -> SBool) -> IO (Proof SBool)
existsDisjunction SBV a -> SBool
p SBV a -> SBool
q = TP (Proof SBool) -> IO (Proof SBool)
forall a. TP a -> IO a
runTP (TP (Proof SBool) -> IO (Proof SBool))
-> TP (Proof SBool) -> IO (Proof SBool)
forall a b. (a -> b) -> a -> b
$ do
    let qb :: (Exists Any a -> SBool) -> SBool
qb = (Exists Any a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"existsDisjunction"
           (      ((Exists Any a -> SBool) -> SBool
qb (\(Exists SBV a
x) -> SBV a -> SBool
p SBV a
x) SBool -> SBool -> SBool
.|| (Exists Any a -> SBool) -> SBool
qb (\(Exists SBV a
x) -> SBV a -> SBool
q SBV a
x))
            SBool -> SBool -> SBool
.<=> -------------------------------------------------------
                          (Exists Any a -> SBool) -> SBool
qb (\(Exists SBV a
x) -> SBV a -> SBool
p SBV a
x SBool -> SBool -> SBool
.|| SBV a -> SBool
q SBV a
x)
           )
           []

-- | We cannot push a universal through a disjunction. We have:
--
-- >>> forallDisjunctionNot @Integer (uninterpret "p") (uninterpret "q") `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: forallConjunctionNot
-- *** Failed to prove forallConjunctionNot.
-- Falsifiable. Counter-example:
--   p :: Integer -> Bool
--   p 2 = True
--   p 1 = False
--   p _ = True
-- <BLANKLINE>
--   q :: Integer -> Bool
--   q 2 = False
--   q 1 = True
--   q _ = True
--
-- Note how @p@ assigns two selected values to @True@ and everything else to @False@, while @q@ does the exact opposite.
-- So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds
-- a model with two distinct values, as one would have sufficed. But it is still a valud model.)
forallDisjunctionNot :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO ()
forallDisjunctionNot :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO ()
forallDisjunctionNot SBV a -> SBool
p SBV a -> SBool
q = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let qb :: (Forall Any a -> SBool) -> SBool
qb = (Forall Any a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    -- This won't prove!
    Proof SBool
_won'tGoThrough <- String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"forallConjunctionNot"
                             (      ((Forall Any a -> SBool) -> SBool
qb (\(Forall SBV a
x) -> SBV a -> SBool
p SBV a
x) SBool -> SBool -> SBool
.|| (Forall Any a -> SBool) -> SBool
qb (\(Forall SBV a
x) -> SBV a -> SBool
q SBV a
x))
                              SBool -> SBool -> SBool
.<=> -------------------------------------------------------
                                              (Forall Any a -> SBool) -> SBool
qb (\(Forall SBV a
x) -> SBV a -> SBool
p SBV a
x SBool -> SBool -> SBool
.|| SBV a -> SBool
q SBV a
x)
                             )
                             []

    () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | We cannot push an existential through conjunction. We have:
--
-- >>> existsConjunctionNot @Integer (uninterpret "p") (uninterpret "q") `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: existsConjunctionNot
-- *** Failed to prove existsConjunctionNot.
-- Falsifiable. Counter-example:
--   p :: Integer -> Bool
--   p 1 = False
--   p _ = True
-- <BLANKLINE>
--   q :: Integer -> Bool
--   q 1 = True
--   q _ = False
--
-- In this case, we again have a predicate That disagree at every point, providing a counter-example.
existsConjunctionNot :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO ()
existsConjunctionNot :: forall a. SymVal a => (SBV a -> SBool) -> (SBV a -> SBool) -> IO ()
existsConjunctionNot SBV a -> SBool
p SBV a -> SBool
q = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let qb :: (Exists Any a -> SBool) -> SBool
qb = (Exists Any a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

    Proof SBool
_wont'GoThrough <- String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"existsConjunctionNot"
                             (      ((Exists Any a -> SBool) -> SBool
qb (\(Exists SBV a
x) -> SBV a -> SBool
p SBV a
x) SBool -> SBool -> SBool
.&& (Exists Any a -> SBool) -> SBool
qb (\(Exists SBV a
x) -> SBV a -> SBool
q SBV a
x))
                              SBool -> SBool -> SBool
.<=> -------------------------------------------------------
                                              (Exists Any a -> SBool) -> SBool
qb (\(Exists SBV a
x) -> SBV a -> SBool
p SBV a
x SBool -> SBool -> SBool
.&& SBV a -> SBool
q SBV a
x)
                             )
                            []

    () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- * QuickCheck

-- | Using quick-check as a step. This can come in handy if a proof step isn't converging,
-- or if you want to quickly see if there are any obvious counterexamples. This example prints:
--
-- @
-- Lemma: qcExample
--   Step: 1 (passed 1000 tests)           Q.E.D. [Modulo: quickCheck]
--   Step: 2 (Failed during quickTest)
-- 
-- *** QuickCheck failed for qcExample.2
-- *** Failed! Assertion failed (after 1 test):
--   n   = 175 :: Word8
--   lhs =  94 :: Word8
--   rhs =  95 :: Word8
--   val =  94 :: Word8
--
-- *** Exception: Failed
-- @
--
-- Of course, the counterexample you get might differ depending on the quickcheck outcome.
qcExample :: TP (Proof (Forall "n" Word8 -> SBool))
qcExample :: TP (Proof (Forall "n" Word8 -> SBool))
qcExample = String
-> (Forall "n" Word8 -> SBool)
-> StepArgs (Forall "n" Word8 -> SBool) Word8
-> TP (Proof (Forall "n" Word8 -> SBool))
forall t.
(Proposition (Forall "n" Word8 -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Word8 -> SBool)
-> StepArgs (Forall "n" Word8 -> SBool) t
-> TP (Proof (Forall "n" Word8 -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"qcExample"
                 (\(Forall SBV Word8
n) -> SBV Word8
n SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
+ SBV Word8
n SBV Word8 -> SBV Word8 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Word8
2 SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
* SBV Word8
n) (StepArgs (Forall "n" Word8 -> SBool) Word8
 -> TP (Proof (Forall "n" Word8 -> SBool)))
-> StepArgs (Forall "n" Word8 -> SBool) Word8
-> TP (Proof (Forall "n" Word8 -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Word8
n -> [] [SBool]
-> TPProofRaw (SBV Word8) -> (SBool, TPProofRaw (SBV Word8))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV Word8
n SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
+ SBV Word8
n
                          SBV Word8 -> Helper -> Hinted (SBV Word8)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Int -> Helper
qc Int
1000
                          TPProofRaw (SBV Word8)
-> ChainsTo (TPProofRaw (SBV Word8))
-> ChainsTo (TPProofRaw (SBV Word8))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Word8
2 SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
* SBV Word8
n
                          SBV Word8 -> Helper -> Hinted (SBV Word8)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Int -> Helper
qc Int
1000
                          TPProofRaw (SBV Word8) -> Helper -> Hinted (TPProofRaw (SBV Word8))
forall a b. HintsTo a b => a -> b -> Hinted a
?? String -> SBV Word8 -> Helper
forall a. String -> SBV a -> Helper
disp String
"val" (SBV Word8
2 SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
* SBV Word8
n)
                          Hinted (TPProofRaw (SBV Word8))
-> ChainsTo (Hinted (TPProofRaw (SBV Word8)))
-> ChainsTo (Hinted (TPProofRaw (SBV Word8)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV Word8
2 SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
* SBV Word8
n SBV Word8 -> SBV Word8 -> SBV Word8
forall a. Num a => a -> a -> a
+ SBV Word8
1
                          SBV Word8 -> ChainsTo (SBV Word8) -> ChainsTo (SBV Word8)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV Word8)
TPProofRaw (SBV Word8)
forall a. TPProofRaw a
qed

-- | We can't really prove Fermat's last theorem. But we can quick-check instances of it.
--
-- >>> runTP (qcFermat 3)
-- Lemma: qcFermat 3
--   Step: 1 (qc: Running 1000 tests)      QC OK
--   Result:                               Q.E.D. [Modulo: quickCheck]
-- [Modulo: quickCheck] qcFermat 3 :: Ɐx ∷ Integer → Ɐy ∷ Integer → Ɐz ∷ Integer → Bool
qcFermat :: Integer -> TP (Proof (Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> SBool))
qcFermat :: Integer
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
qcFermat Integer
e = String
-> (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall t.
(Proposition
   (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     t
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc (String
"qcFermat " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
e)
                  (\(Forall SInteger
x) (Forall SInteger
y) (Forall SInteger
z) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
2 SBool -> SBool -> SBool
.=> SInteger
xSInteger -> SInteger -> SInteger
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
ySInteger -> SInteger -> SInteger
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
zSInteger -> SInteger -> SInteger
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^SInteger
n) (StepArgs
   (Forall "x" Integer
    -> Forall "y" Integer -> Forall "z" Integer -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "x" Integer
          -> Forall "y" Integer -> Forall "z" Integer -> SBool)))
-> StepArgs
     (Forall "x" Integer
      -> Forall "y" Integer -> Forall "z" Integer -> SBool)
     Bool
-> TP
     (Proof
        (Forall "x" Integer
         -> Forall "y" Integer -> Forall "z" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \SInteger
x SInteger
y SInteger
z -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
2]
                         [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SInteger
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^ SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
y SInteger -> SInteger -> SInteger
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^ SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
z SInteger -> SInteger -> SInteger
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^ SInteger
n
                         SBool -> Helper -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Int -> Helper
qc Int
1000
                         TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                         SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
  where n :: SInteger
n = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
e

-- * No termination checks

-- | It's important to realize that TP proofs in SBV neither check nor guarantee that the
-- functions we use are terminating. This is beyond the scope (and current capabilities) of what SBV can handle.
-- That is, the proof is up-to-termination, i.e., any proof implicitly assumes all functions defined (or axiomatized)
-- terminate for all possible inputs. If non-termination is possible, then the logic becomes inconsistent, i.e.,
-- we can prove arbitrary results.
--
-- Here is a simple example where we tell SBV that there is a function @f@ with non terminating behavior. Using this,
-- we can deduce @False@:
--
-- >>> noTerminationChecks
-- Axiom: bad
-- Lemma: noTerminationImpliesFalse
--   Step: 1 (bad @ (n |-> 0 :: SInteger)) Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] noTerminationImpliesFalse :: Bool
noTerminationChecks :: IO (Proof SBool)
noTerminationChecks :: IO (Proof SBool)
noTerminationChecks = TP (Proof SBool) -> IO (Proof SBool)
forall a. TP a -> IO a
runTP (TP (Proof SBool) -> IO (Proof SBool))
-> TP (Proof SBool) -> IO (Proof SBool)
forall a b. (a -> b) -> a -> b
$ do

   let f :: SInteger -> SInteger
       f :: SInteger -> SInteger
f = String -> SInteger -> SInteger
forall a. SMTDefinable a => String -> a
uninterpret String
"f"

   Proof (Forall "n" Integer -> SBool)
badAxiom <- String
-> (Forall "n" Integer -> SBool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"bad" (\(Forall SInteger
n) -> SInteger -> SInteger
f SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
f SInteger
n)

   String -> SBool -> StepArgs SBool Integer -> TP (Proof SBool)
forall t.
(Proposition SBool, SymVal t, EqSymbolic (SBV t)) =>
String -> SBool -> StepArgs SBool t -> TP (Proof SBool)
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"noTerminationImpliesFalse"
        SBool
sFalse
        ([] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
f SInteger
0
            SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
badAxiom Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
0 :: SInteger)
            TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
f SInteger
0
            SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed)

-- * Trying to prove non-theorems

-- | An example where we attempt to prove a non-theorem. Notice the counter-example
-- generated for:
--
-- @length xs == ite (length xs .== 3) 5 (length xs)@
--
-- >>> badRevLen `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: badRevLen
-- *** Failed to prove badRevLen.
-- Falsifiable. Counter-example:
--   xs = [14,11,14] :: [Integer]
badRevLen :: IO ()
badRevLen :: IO ()
badRevLen = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$
   TP (Proof (Forall "xs" [Integer] -> SBool)) -> TP ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TP (Proof (Forall "xs" [Integer] -> SBool)) -> TP ())
-> TP (Proof (Forall "xs" [Integer] -> SBool)) -> TP ()
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "xs" [Integer] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"badRevLen"
                (\(Forall @"xs" (SList Integer
xs :: SList Integer)) -> SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
3) SInteger
5 (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs))
                []

-- | It is instructive to see what kind of counter-example we get if a lemma fails to prove.
-- Below, we do a variant of the 'lengthTail, but with a bad implementation over integers,
-- and see the counter-example. Our implementation returns an incorrect answer if the given list is longer
-- than 5 elements and have 42 in it:
--
-- >>> badLengthProof `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: badLengthProof
-- *** Failed to prove badLengthProof.
-- Falsifiable. Counter-example:
--   xs   = [15,11,13,16,27,42] :: [Integer]
--   imp  =                  42 :: Integer
--   spec =                   6 :: Integer
badLengthProof :: IO ()
badLengthProof :: IO ()
badLengthProof = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
   let badLength :: SList Integer -> SInteger
       badLength :: SList Integer -> SInteger
badLength SList Integer
xs = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
5 SBool -> SBool -> SBool
.&& SInteger
42 SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs) SInteger
42 (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs)

   TP (Proof (Forall "xs" [Integer] -> SBool)) -> TP ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TP (Proof (Forall "xs" [Integer] -> SBool)) -> TP ())
-> TP (Proof (Forall "xs" [Integer] -> SBool)) -> TP ()
forall a b. (a -> b) -> a -> b
$ String
-> (Forall "xs" [Integer] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"badLengthProof" (\(Forall @"xs" SList Integer
xs) -> String -> SInteger -> SInteger
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"imp" (SList Integer -> SInteger
badLength SList Integer
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== String -> SInteger -> SInteger
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"spec" (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs)) []

-- * Caching

-- | It is not unusual that TP proofs rely on other proofs. Typically, all the helpers are used together and proven in
-- one go. It is, however, useful to be able to write these proofs as top-level entries, and reuse them multiple times
-- in several proofs. (See "Documentation/SBV/Examples/TP/PowerMod.hs" for an example.) To avoid re-proving such
-- lemmas, you can turn on proof caching. The idea behind caching is simple: If we see a lemma with the same name being
-- proven again, then we simply reuse the last result. The catch here is that lemmas are identified by their names: Hence,
-- for caching to be sound, you need to make sure all names used in your proof are unique. Otherwise you can
-- conclude wrong results!
--
-- A good trick is to pay the price and run your entire proof without caching (which is the default) once, and if it is
-- all good, turn on caching to save time in regressions. (And rerun without caching after code changes.)
--
-- To demonstrate why caching can be unsound, simply consider a proof where we first prove true, and then prove false
-- but we /trick/ TP by reusing the name. If you run this, you'll see:
--
-- >>> runTP badCaching `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: evil                             Q.E.D.
-- Lemma: evil
-- *** Failed to prove evil.
-- Falsifiable
--
-- This is good, the proof failed since it's just not true. (Except for the confusing naming printed in the trace
-- due to our own choice.)
--
-- Let's see what happens if we turn caching on:
--
-- >>> runTPWith (tpCache z3) badCaching
-- Lemma: evil                             Q.E.D.
-- Cached: evil                            Q.E.D.
--
-- In this case we were able to ostensibly prove False, i.e., this result is unsound. But at least SBV warned us
-- that we used a cached proof (@evil@), reminding us that using unique names is a proof of obligation for the user
-- if caching is turned on. Clearly, we failed to uniquely name our proofs in this case.
--
-- Note that a bad proof obtained this way is unsound in the way that it is misleading: That is, it will lead you
-- to believe you proved something while you actually proved something else. (More technically, you cannot take the evil
-- lemma and use it to prove arbitrary things, since it's still just the proof of truth.) In this sense it is just
-- useless as opposed to soundness, but it is alarming as one can be led astray.
--
-- (Incidentally, if you really want to be evil, you can just use 'axiom' and assert false, but that's another story.)
badCaching :: TP ()
badCaching :: TP ()
badCaching = do
   -- Prove true, giving it a bad name
   Proof SBool
_ <- String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"evil" SBool
sTrue []

   -- Attempt to prove false, using evil:
   Proof SBool
_ <- String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"evil" SBool
sFalse []

   () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()