-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Coins
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving the classic coin change theorem: For any amount @n >= 8@, you can make
-- exact change using only 3-cent and 5-cent coins.
--
-- This example is inspired by: <https://github.com/imandra-ai/imandrax-examples/blob/main/src/coins.iml>
-----------------------------------------------------------------------------

{-# LANGUAGE CPP               #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuasiQuotes       #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeApplications  #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Coins where

import Data.SBV
import Data.SBV.Maybe hiding (maybe)
import qualified Data.SBV.Maybe as SM
import Data.SBV.TP

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV.TP
#endif

-- * Types

-- | A pocket contains a count of 3-cent and 5-cent coins.
data Pocket = Pocket { Pocket -> Integer
num3s :: Integer
                     , Pocket -> Integer
num5s :: Integer
                     }

-- | Create a symbolic version of Pocket.
mkSymbolic [''Pocket]

-- * Making change

-- | Make change for a given amount. Returns 'Nothing' if the amount is less than 8.
-- Base cases:
--
--   *  8 = 3 + 5
--   *  9 = 3 + 3 + 3
--   * 10 = 5 + 5
--
-- For @n > 10@, we use change for @n-3@ and add one more 3-cent coin.
mkChange :: SInteger -> SMaybe Pocket
mkChange :: SBV Integer -> SMaybe Pocket
mkChange = String
-> (SBV Integer -> SMaybe Pocket) -> SBV Integer -> SMaybe Pocket
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"mkChange" ((SBV Integer -> SMaybe Pocket) -> SBV Integer -> SMaybe Pocket)
-> (SBV Integer -> SMaybe Pocket) -> SBV Integer -> SMaybe Pocket
forall a b. (a -> b) -> a -> b
$ \SBV Integer
n ->
    SBool -> SMaybe Pocket -> SMaybe Pocket -> SMaybe Pocket
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<   SBV Integer
8)  SMaybe Pocket
forall a. SymVal a => SBV (Maybe a)
sNothing
  (SMaybe Pocket -> SMaybe Pocket) -> SMaybe Pocket -> SMaybe Pocket
forall a b. (a -> b) -> a -> b
$ SBool -> SMaybe Pocket -> SMaybe Pocket -> SMaybe Pocket
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==  SBV Integer
8) (SBV Pocket -> SMaybe Pocket
forall a. SymVal a => SBV a -> SBV (Maybe a)
sJust (SBV Integer -> SBV Integer -> SBV Pocket
sPocket SBV Integer
1 SBV Integer
1))
  (SMaybe Pocket -> SMaybe Pocket) -> SMaybe Pocket -> SMaybe Pocket
forall a b. (a -> b) -> a -> b
$ SBool -> SMaybe Pocket -> SMaybe Pocket -> SMaybe Pocket
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==  SBV Integer
9) (SBV Pocket -> SMaybe Pocket
forall a. SymVal a => SBV a -> SBV (Maybe a)
sJust (SBV Integer -> SBV Integer -> SBV Pocket
sPocket SBV Integer
3 SBV Integer
0))
  (SMaybe Pocket -> SMaybe Pocket) -> SMaybe Pocket -> SMaybe Pocket
forall a b. (a -> b) -> a -> b
$ SBool -> SMaybe Pocket -> SMaybe Pocket -> SMaybe Pocket
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
10) (SBV Pocket -> SMaybe Pocket
forall a. SymVal a => SBV a -> SBV (Maybe a)
sJust (SBV Integer -> SBV Integer -> SBV Pocket
sPocket SBV Integer
0 SBV Integer
2))
    -- n > 10: use change for (n-3) and add a 3-cent coin
    [sCase|Pocket fromJust (mkChange (n - 3)) of
       Pocket n3 n5 -> sJust (sPocket (n3 + 1) n5)
    |]

-- | Evaluate the value of a pocket (total cents).
evalPocket :: SMaybe Pocket -> SInteger
evalPocket :: SMaybe Pocket -> SBV Integer
evalPocket = SBV Integer
-> (SBV Pocket -> SBV Integer) -> SMaybe Pocket -> SBV Integer
forall a b.
(SymVal a, SymVal b) =>
SBV b -> (SBV a -> SBV b) -> SMaybe a -> SBV b
SM.maybe SBV Integer
0 ((SBV Pocket -> SBV Integer) -> SMaybe Pocket -> SBV Integer)
-> (SBV Pocket -> SBV Integer) -> SMaybe Pocket -> SBV Integer
forall a b. (a -> b) -> a -> b
$ \SBV Pocket
p -> [sCase|Pocket p of
                                  Pocket n3 n5 -> 3 * n3 + 5 * n5
                                |]

-- * Correctness

-- | Prove that for any @n >= 8@, @mkChange@ produces a pocket that evaluates to @n@.
--
-- We have:
--
-- >>> runTP correctness
-- Inductive lemma (strong): mkChangeCorrect
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (5 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.3                           Q.E.D.
--     Step: 1.4                           Q.E.D.
--     Step: 1.5.1                         Q.E.D.
--     Step: 1.5.2                         Q.E.D.
--     Step: 1.5.3                         Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] mkChangeCorrect :: Ɐn ∷ Integer → Bool
correctness :: TP (Proof (Forall "n" Integer -> SBool))
correctness :: TP (Proof (Forall "n" Integer -> SBool))
correctness = do
    String
-> (Forall "n" Integer -> SBool)
-> (MeasureArgs (Forall "n" Integer -> SBool) Integer, [ProofObj])
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> (MeasureArgs a m, [ProofObj])
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "n" Integer -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> (MeasureArgs (Forall "n" Integer -> SBool) m, [ProofObj])
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
sInduct String
"mkChangeCorrect"
            (\(Forall SBV Integer
n) -> SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
8 SBool -> SBool -> SBool
.=> SMaybe Pocket -> SBV Integer
evalPocket (SBV Integer -> SMaybe Pocket
mkChange SBV Integer
n) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
n)
            (MeasureArgs (Forall "n" Integer -> SBool) Integer
SBV Integer -> SBV Integer
forall a. a -> a
id, []) ((Proof (Forall "n" Integer -> SBool)
  -> StepArgs (Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof (Forall "n" Integer -> SBool)
ih SBV Integer
n -> [SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
8]
                  [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SMaybe Pocket -> SBV Integer
evalPocket (SBV Integer -> SMaybe Pocket
mkChange SBV Integer
n) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
n
                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
8  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                           , SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
9  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                           , SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
10 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                           , SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV Integer
8   SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial   -- Vacuously true: contradicts n >= 8
                           , SBV Integer
n SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
10  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SMaybe Pocket -> SBV Integer
evalPocket (SBV Integer -> SMaybe Pocket
mkChange SBV Integer
n) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
n
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [sCase|Pocket fromJust (mkChange (n - 3)) of
                                            Pocket n3 n5 -> evalPocket (sJust (sPocket (n3 + 1) n5)) .== n
                                         |]
                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ih 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" (SBV Integer
n SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
3)
                                       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
                           ]