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

{-# 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 = runTP $ lemma "true" sTrue []

-- | @sFalse@ isn't provable.
--
-- We have:
--
-- >>> falseIsn'tProvable `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: sFalse
-- *** Failed to prove sFalse.
-- Falsifiable
falseIsn'tProvable :: IO ()
falseIsn'tProvable = runTP $ do
        _won'tGoThrough <- lemma "sFalse" sFalse []
        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 = runTP $ lemma "largerIntegerExists"
                                    (\(Forall x) (Exists y) -> x .< 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 p q = runTP $ do
    let qb = quantifiedBool

    lemma "forallConjunction"
           (      (qb (\(Forall x) -> p x) .&& qb (\(Forall x) -> q x))
            .<=> -------------------------------------------------------
                          qb (\(Forall x) -> p x .&& q 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 p q = runTP $ do
    let qb = quantifiedBool

    lemma "existsDisjunction"
           (      (qb (\(Exists x) -> p x) .|| qb (\(Exists x) -> q x))
            .<=> -------------------------------------------------------
                          qb (\(Exists x) -> p x .|| q 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 p q = runTP $ do
    let qb = quantifiedBool

    -- This won't prove!
    _won'tGoThrough <- lemma "forallConjunctionNot"
                             (      (qb (\(Forall x) -> p x) .|| qb (\(Forall x) -> q x))
                              .<=> -------------------------------------------------------
                                              qb (\(Forall x) -> p x .|| q x)
                             )
                             []

    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 p q = runTP $ do
    let qb = quantifiedBool

    _wont'GoThrough <- lemma "existsConjunctionNot"
                             (      (qb (\(Exists x) -> p x) .&& qb (\(Exists x) -> q x))
                              .<=> -------------------------------------------------------
                                              qb (\(Exists x) -> p x .&& q x)
                             )
                            []

    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 = calc "qcExample"
                 (\(Forall n) -> n + n .== 2 * n) $
                 \n -> [] |- n + n
                          ?? qc 1000
                          =: 2 * n
                          ?? qc 1000
                          ?? disp "val" (2 * n)
                          =: 2 * n + 1
                          =: 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 e = calc ("qcFermat " <> show e)
                  (\(Forall x) (Forall y) (Forall z) -> n .> 2 .=> x.^n + y.^n ./= z.^n) $
                  \x y z -> [n .> 2]
                         |- x .^ n + y .^ n ./= z .^ n
                         ?? qc 1000
                         =: sTrue
                         =: qed
  where n = literal 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 = runTP $ do

   let f :: SInteger -> SInteger
       f = uninterpret "f"

   badAxiom <- axiom "bad" (\(Forall n) -> f n .== 1 + f n)

   calc "noTerminationImpliesFalse"
        sFalse
        ([] |- f 0
            ?? badAxiom `at` Inst @"n" (0 :: SInteger)
            =: 1 + f 0
            =: 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 = [17,17,17] :: [Integer]
badRevLen :: IO ()
badRevLen = runTP $
   void $ lemma "badRevLen"
                (\(Forall @"xs" (xs :: SList Integer)) -> length (reverse xs) .== ite (length xs .== 3) 5 (length 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   = [12,15,20,24,33,42] :: [Integer]
--   imp  =                  42 :: Integer
--   spec =                   6 :: Integer
badLengthProof :: IO ()
badLengthProof = runTP $ do
   let badLength :: SList Integer -> SInteger
       badLength xs = ite (length xs .> 5 .&& 42 `elem` xs) 42 (length xs)

   void $ lemma "badLengthProof" (\(Forall @"xs" xs) -> observe "imp" (badLength xs) .== observe "spec" (length 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 = do
   -- Prove true, giving it a bad name
   _ <- lemma "evil" sTrue []

   -- Attempt to prove false, using evil:
   _ <- lemma "evil" sFalse []

   pure ()