Documentation.SBV.Examples.KnuckleDragger.ListLen

Example use of the KnuckleDragger, about lenghts of lists

Documentation

data Elt

Use an uninterpreted type for the elements

Instances

Data Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.ListLen

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Elt -> c Elt

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Elt

toConstr :: Elt -> Constr

dataTypeOf :: Elt -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Elt)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Elt)

gmapT :: (forall b. Data b => b -> b) -> Elt -> Elt

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elt -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elt -> r

gmapQ :: (forall d. Data d => d -> u) -> Elt -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Elt -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elt -> m Elt

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elt -> m Elt

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elt -> m Elt

Read Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.ListLen

Methods

readsPrec :: Int -> ReadS Elt

readList :: ReadS [Elt]

readPrec :: ReadPrec Elt

readListPrec :: ReadPrec [Elt]

Show Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.ListLen

Methods

showsPrec :: Int -> Elt -> ShowS

show :: Elt -> String

showList :: [Elt] -> ShowS

SymVal Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.ListLen

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Elt)

literal :: Elt -> SBV Elt

fromCV :: CV -> Elt

isConcretely :: SBV Elt -> (Elt -> Bool) -> Bool

free :: MonadSymbolic m => String -> m (SBV Elt)

free_ :: MonadSymbolic m => m (SBV Elt)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Elt]

symbolic :: MonadSymbolic m => String -> m (SBV Elt)

symbolics :: MonadSymbolic m => [String] -> m [SBV Elt]

unliteral :: SBV Elt -> Maybe Elt

isConcrete :: SBV Elt -> Bool

isSymbolic :: SBV Elt -> Bool

HasKind Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.ListLen

Methods

kindOf :: Elt -> Kind

hasSign :: Elt -> Bool

intSizeOf :: Elt -> Int

isBoolean :: Elt -> Bool

isBounded :: Elt -> Bool

isReal :: Elt -> Bool

isFloat :: Elt -> Bool

isDouble :: Elt -> Bool

isRational :: Elt -> Bool

isFP :: Elt -> Bool

isUnbounded :: Elt -> Bool

isUserSort :: Elt -> Bool

isChar :: Elt -> Bool

isString :: Elt -> Bool

isList :: Elt -> Bool

isSet :: Elt -> Bool

isTuple :: Elt -> Bool

isMaybe :: Elt -> Bool

isEither :: Elt -> Bool

isArray :: Elt -> Bool

showType :: Elt -> String

SatModel Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.ListLen

Methods

parseCVs :: [CV] -> Maybe (Elt, [CV])

cvtModel :: (Elt -> Maybe b) -> Maybe (Elt, [CV]) -> Maybe (b, [CV])

type SElt = SBV Elt

Symbolic version of the type Elt.

listLengthProof :: IO Proof

Prove that the length of a list is one more than the length of its tail.

We have:

>>> listLengthProof
Lemma: length_correct                   Q.E.D.
[Proven] length_correct

badProof :: IO ()

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 listLengthProof, 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. We have:

>>> badProof `catch` (\(_ :: SomeException) -> pure ())
Lemma: bad
*** Failed to prove bad.
Falsifiable. Counter-example:
  xs   = [8,25,26,27,28,42] :: [Integer]
  imp  =                 42 :: Integer
  spec =                  6 :: Integer

lenAppend :: IO Proof

length (xs ++ ys) == length xs + length ys

We have:

>>> lenAppend
Lemma: lenAppend                        Q.E.D.
[Proven] lenAppend

lenAppend2 :: IO Proof

length xs == length ys -> length (xs ++ ys) == 2 * length xs

We have:

>>> lenAppend2
Lemma: lenAppend2                       Q.E.D.
[Proven] lenAppend2