sbv-13.6: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.Coins

Description

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

Synopsis

Types

data Pocket Source #

A pocket contains a count of 3-cent and 5-cent coins.

Constructors

Pocket 

Fields

Instances

Instances details
Arbitrary Pocket Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

arbitrary :: Gen Pocket #

shrink :: Pocket -> [Pocket] #

SymVal Pocket Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Pocket) Source #

mkSymValInit :: State -> SBV Pocket -> IO () Source #

literal :: Pocket -> SBV Pocket Source #

fromCV :: CV -> Pocket Source #

isConcretely :: SBV Pocket -> (Pocket -> Bool) -> Bool Source #

minMaxBound :: Maybe (Pocket, Pocket) Source #

free :: MonadSymbolic m => String -> m (SBV Pocket) Source #

free_ :: MonadSymbolic m => m (SBV Pocket) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Pocket] Source #

symbolic :: MonadSymbolic m => String -> m (SBV Pocket) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV Pocket] Source #

unliteral :: SBV Pocket -> Maybe Pocket Source #

unlitCV :: SBV Pocket -> Maybe (Kind, CVal) Source #

isConcrete :: SBV Pocket -> Bool Source #

isSymbolic :: SBV Pocket -> Bool Source #

HasKind Pocket Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

kindOf :: Pocket -> Kind Source #

hasSign :: Pocket -> Bool Source #

intSizeOf :: Pocket -> Int Source #

isBoolean :: Pocket -> Bool Source #

isBounded :: Pocket -> Bool Source #

isReal :: Pocket -> Bool Source #

isFloat :: Pocket -> Bool Source #

isDouble :: Pocket -> Bool Source #

isRational :: Pocket -> Bool Source #

isFP :: Pocket -> Bool Source #

isUnbounded :: Pocket -> Bool Source #

isADT :: Pocket -> Bool Source #

isChar :: Pocket -> Bool Source #

isString :: Pocket -> Bool Source #

isList :: Pocket -> Bool Source #

isSet :: Pocket -> Bool Source #

isTuple :: Pocket -> Bool Source #

isArray :: Pocket -> Bool Source #

isRoundingMode :: Pocket -> Bool Source #

isUninterpreted :: Pocket -> Bool Source #

showType :: Pocket -> String Source #

HasInductionSchema (Forall ta Pocket -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

inductionSchema :: (Forall ta Pocket -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Pocket -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

inductionSchema :: (Forall ta Pocket -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

inductionSchema :: (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

inductionSchema :: (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

inductionSchema :: (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Coins

Methods

inductionSchema :: (Forall ta Pocket -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Pocket :: String -> [CV] -> Pocket Source #

Conversion from SMT values to Pocket values.

_undefiner_Pocket :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SPocket = SBV Pocket Source #

Symbolic version of the type Pocket.

sPocket :: SBV Integer -> SBV Integer -> SBV Pocket Source #

Symbolic version of the constructor Pocket.

isPocket :: SBV Pocket -> SBool Source #

Field recognizer predicate.

getPocket_1 :: SBV Pocket -> SBV Integer Source #

Field accessor function.

snum3s :: SBV Pocket -> SBV Integer Source #

Field accessor function.

getPocket_2 :: SBV Pocket -> SBV Integer Source #

Field accessor function.

snum5s :: SBV Pocket -> SBV Integer Source #

Field accessor function.

sCasePocket :: Mergeable result => SBV Pocket -> (SBV Integer -> SBV Integer -> result) -> result Source #

Case analyzer for the type Pocket.

Making change

mkChange :: SInteger -> SMaybe Pocket Source #

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.

evalPocket :: SMaybe Pocket -> SInteger Source #

Evaluate the value of a pocket (total cents).

Correctness

correctness :: TP (Proof (Forall "n" Integer -> SBool)) Source #

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