Documentation.SBV.Examples.KnuckleDragger.RevLen

Proof that reversing a list does not change its length.

Documentation

data Elt

Use an uninterpreted type for the elements

Instances

Data Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.RevLen

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.RevLen

Methods

readsPrec :: Int -> ReadS Elt

readList :: ReadS [Elt]

readPrec :: ReadPrec Elt

readListPrec :: ReadPrec [Elt]

Show Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.RevLen

Methods

showsPrec :: Int -> Elt -> ShowS

show :: Elt -> String

showList :: [Elt] -> ShowS

SymVal Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.RevLen

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.RevLen

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.RevLen

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.

revLen :: IO Proof

length xs == length (reverse xs)

We have:

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

badRevLen :: IO ()

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)

We have:

>>> badRevLen `catch` (\(_ :: SomeException) -> pure ())
Lemma: badRevLen
*** Failed to prove badRevLen.
Falsifiable. Counter-example:
  xs = [Elt_1,Elt_2,Elt_1] :: [Elt]