-----------------------------------------------------------------------------
-- |
-- 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 QuasiQuotes         #-}
{-# 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 4 = True
--   p 3 = False
--   p _ = True
-- <BLANKLINE>
--   q :: Integer -> Bool
--   q 4 = False
--   q 3 = True
--   q _ = True
--
-- Note how @p@ and @q@ differ in their treatment of the inputs 3 and 4, but agree everywhere else. So, for each
-- input, at least one of @p@ or @q@ is @True@, making the disjunction @True@ for all inputs. But the predicates
-- @p@ and @q@ are not universally true themselves, constituting a counter-example.
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 3 = False
--   p _ = True
-- <BLANKLINE>
--   q :: Integer -> Bool
--   q 3 = True
--   q _ = False
--
-- In this case, both @p@ and @q@ have a satisfying input (for @p@ everything but 3, for @q@, only 3), but
-- there is no single value that satisfies both, thus giving us our 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

-- * Termination checking

-- | When a recursive function is defined via 'smtFunction', SBV automatically checks that it terminates
-- by guessing and verifying a termination measure. Here we define a simple recursive @sumToN@ and prove
-- a property about it. Note the @Functions proven terminating@ line in the output, confirming that SBV
-- verified the termination of @sumToN@ before proceeding with the proof.
--
-- >>> terminationDemo
-- Lemma: sumToN_at_5    Q.E.D.
-- Functions proven terminating: sumToN
-- [Proven] sumToN_at_5 :: Ɐn ∷ Integer → Bool
terminationDemo :: IO (Proof (Forall "n" Integer -> SBool))
terminationDemo = runTP $ do
    let sumToN :: SInteger -> SInteger
        sumToN = smtFunction "sumToN" $ \x -> [sCase| x of
                                                 _ | x .<= 0 -> 0
                                                 _           -> x + sumToN (x - 1)
                                              |]

    lemma "sumToN_at_5"
          (\(Forall n) -> n .== 5 .=> sumToN n .== 15)
          []

-- | If SBV cannot determine a termination measure, it will report an error. Here, we define
-- a function that recurses without decreasing any argument, and SBV rightfully rejects it:
--
-- >>> badTermination `catch` (\(e :: SomeException) -> mapM_ putStrLn . filter (\l -> take 3 l == "***") . lines $ show e)
-- *** Data.SBV: Cannot determine a termination measure.
-- ***
-- ***   Function: bad :: SBV Integer -> SBV Integer
-- ***
-- ***   Measures tried:
-- ***     abs arg1
-- ***     smax 0 arg1
-- ***     abs arg1 + smax 0 arg1
-- ***     (abs arg1, smax 0 arg1)
-- ***     (smax 0 arg1, abs arg1)
-- ***
-- *** Please use 'smtFunctionWithMeasure' to provide an explicit measure.
badTermination :: IO ()
badTermination = do
    let bad :: SInteger -> SInteger
        bad = smtFunction "bad" $ \x -> [sCase| x of
                                           _ | x .== 0 -> 0
                                           _           -> bad x
                                        |]
    r <- prove $ \x -> bad x .== bad x
    print r

-- | If the user provides an explicit but incorrect termination measure via 'smtFunctionWithMeasure',
-- SBV will detect this and report an error. Here, we use @const 0@ as a measure, which clearly
-- does not decrease at recursive calls:
--
-- >>> badMeasure `catch` (\(e :: SomeException) -> mapM_ putStrLn . filter (\l -> take 3 l == "***") . lines $ show e)
-- *** Data.SBV: Termination measure does not strictly decrease at a recursive call site.
-- ***
-- ***   Function: badM :: SBV Integer -> SBV Integer
-- ***
-- ***   Falsifiable. Counter-example:
-- ***     arg    = 1 :: Integer
-- ***     before = 0 :: Integer
-- ***     then   = 0 :: Integer
-- ***
-- *** The measure must strictly decrease at every recursive call.
badMeasure :: IO ()
badMeasure = do
    let badM :: SInteger -> SInteger
        badM = smtFunctionWithMeasure "badM" (const (0 :: SInteger), [])
             $ \x -> [sCase| x of
                        _ | x .<= 0 -> 0
                        _           -> x + badM (x - 1)
                     |]
    r <- prove $ \x -> badM x .== badM x
    print r

-- | A termination measure is only a valid argument for termination if it takes values in a
-- /well-founded/ order: one with no infinite descending chains. Being non-negative and strictly
-- decreasing then forces the recursion to stop. The integers (bounded below by @0@) are well-founded,
-- but the reals are /not/: the chain @1, 1\/2, 1\/4, ...@ descends forever without ever reaching a
-- minimum. So a real-valued measure proves nothing.
--
-- Consider this Zeno-style non-terminating recursion: for any @x > 0@, the argument @x \/ 2@ is
-- again positive, so it never reaches the base case. Yet the measure @0 `smax` x@ is non-negative
-- and strictly decreases at the recursive call (@x \/ 2 < x@). Accepting it would mean certifying a
-- non-terminating function as terminating, which can be used to derive falsehoods.
--
-- @
-- zeno :: SReal -> SReal
-- zeno = smtFunctionWithMeasure \"zeno\" (\\x -> 0 \`smax\` x, [])
--      $ \\x -> ite (x .<= 0) 0 (zeno (x \/ 2))
-- @
--
-- SBV rules this out /at compile time/: the 'Data.SBV.Zero' class gates which types may be used as
-- measures, and there is deliberately no instance for algebraic reals. So the definition above does
-- not type-check, reporting:
--
-- @
--     • A termination measure may not have a real-valued result.
--
--       The reals are not well-ordered: an infinite descending chain such as
--       1, 1\/2, 1\/4, ... has no least element, so a non-negative and strictly
--       decreasing real measure does not imply termination.
--
--       Use an integer-valued measure instead (e.g. a count of remaining steps).
-- @

-- * Axioms and consistency

-- | SBV checks that recursive functions defined via 'smtFunction' terminate, verifying a termination measure, which
-- can be auto-guessed or specified by the user. However, axioms are taken on faith: they are not checked for consistency.
-- If an axiom introduces a non-terminating or contradictory definition, the logic becomes inconsistent, i.e.,
-- we can prove arbitrary results.
--
-- Here is a simple example where we assert an axiom equivalent to a non-terminating definition @f n == 1 + f n@.
-- Using this, we can deduce @False@:
--
-- >>> axiomsAreDangerous
-- Axiom: bad
-- Lemma: axiomsCanBeInconsistent
--   Step: 1 (bad @ (n |-> 0 :: SInteger))    Q.E.D.
--   Result:                                  Q.E.D.
-- [Proven] axiomsCanBeInconsistent :: Bool
axiomsAreDangerous :: IO (Proof SBool)
axiomsAreDangerous = runTP $ do

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

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

   calc "axiomsCanBeInconsistent"
        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,19,25,32,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, SBV caches proof results keyed by symbolic fingerprint. Use 'recall' to invoke a proof action that
-- benefits from the cache: if the proposition has already been proved, the cached result is returned immediately.
-- Note that 'lemma', 'calc', and 'induct' always prove from scratch and then store the result in the cache;
-- only 'recall' performs a cache lookup.
--
-- Lemma names do not need to be unique. If you prove the same proposition under different names, 'recall' will
-- show the aliases. If you prove different propositions under the same name, each is proved independently.
-- To demonstrate, note that reusing the name @"evil"@ does not cause any confusion: the second call to
-- 'lemma' proves from scratch and correctly fails:
--
-- >>> runTP duplicateNames `catch` (\(_ :: SomeException) -> pure ())
-- Lemma: evil         Q.E.D.
-- Lemma: evil
-- *** Failed to prove evil.
-- Falsifiable
--
-- (Incidentally, if you really want to be evil, you can just use 'axiom' and assert false, but that's another story.)
duplicateNames :: TP ()
duplicateNames = do
   -- Prove true
   _ <- lemma "evil" sTrue []

   -- Attempt to prove false, reusing the same name. Will be caught!
   _ <- lemma "evil" sFalse []

   pure ()