Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.KnuckleDragger.Lists

Contents

Appending null
Moving cons over append
Associativity of append
Reverse and append
Reversing twice is identity
Lengths of lists
Any, all, and filtering
Map, append, and reverse
Reverse and length
Foldr-map fusion
Foldr-foldr fusion
Foldr over append
Foldl over append
Foldr-foldl correspondence
Foldr-foldl duality, generalized
Another foldl-foldr correspondence
Bookkeeping law
Filter-append
Map and filter don't commute
Partition
Take and drop
Summing via halving
Zip

Description

A variety of KnuckleDragger proofs on list processing functions. Note that these proofs only hold for finite lists. SMT-solvers do not model infinite lists, and hence all claims are for finite (but arbitrary-length) lists.

Synopsis

data A
type SA = SBV A
data B
type SB = SBV B
data C
type SC = SBV C
appendNull :: IO Proof
consApp :: IO Proof
appendAssoc :: IO Proof
revCons :: IO Proof
revApp :: IO Proof
reverseReverse :: IO Proof
lengthTail :: IO Proof
badLengthProof :: IO ()
lenAppend :: IO Proof
lenAppend2 :: IO Proof
allAny :: IO Proof
filterEx :: IO Proof
filterEx2 :: IO ()
mapEquiv :: IO Proof
mapAppend :: (SA -> SB) -> IO Proof
mapReverse :: IO Proof
revLen :: IO Proof
badRevLen :: IO ()
foldrMapFusion :: IO Proof
foldrFusion :: IO Proof
foldrOverAppend :: IO Proof
foldlOverAppend :: (SB -> SA -> SB) -> IO Proof
foldrFoldlDuality :: IO Proof
foldrFoldlDualityGeneralized :: IO Proof
foldrFoldl :: IO Proof
bookKeeping :: IO Proof
filterAppend :: (SA -> SBool) -> IO Proof
filterConcat :: IO Proof
mapFilter :: IO ()
partition1 :: IO Proof
partition2 :: IO Proof
take_take :: IO Proof
drop_drop :: IO Proof
take_drop :: IO Proof
take_cons :: IO Proof
take_map :: IO Proof
drop_cons :: SymVal elt => Proxy elt -> IO Proof
drop_map :: IO Proof
length_take :: IO Proof
length_drop :: IO Proof
take_all :: IO Proof
drop_all :: IO Proof
take_append :: IO Proof
drop_append :: IO Proof
sumHalves :: IO Proof
map_fst_zip :: IO Proof
map_snd_zip :: IO Proof
map_fst_zip_take :: IO Proof
map_snd_zip_take :: IO Proof

Documentation

data A Source #

Data declaration for an uninterpreted type, usually indicating source.

Instances

Instances details

Data A Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> A -> c A # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c A # toConstr :: A -> Constr # dataTypeOf :: A -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c A) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c A) # gmapT :: (forall b. Data b => b -> b) -> A -> A # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> A -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> A -> r # gmapQ :: (forall d. Data d => d -> u) -> A -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> A -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> A -> m A # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> A -> m A # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> A -> m A #
Read A Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods readsPrec :: Int -> ReadS A # readList :: ReadS [A] # readPrec :: ReadPrec A # readListPrec :: ReadPrec [A] #
Show A Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods showsPrec :: Int -> A -> ShowS # show :: A -> String # showList :: [A] -> ShowS #
SymVal A Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV A) Source # literal :: A -> SBV A Source # fromCV :: CV -> A Source # isConcretely :: SBV A -> (A -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV A) Source # free_ :: MonadSymbolic m => m (SBV A) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV A] Source # symbolic :: MonadSymbolic m => String -> m (SBV A) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV A] Source # unliteral :: SBV A -> Maybe A Source # isConcrete :: SBV A -> Bool Source # isSymbolic :: SBV A -> Bool Source #
HasKind A Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods kindOf :: A -> Kind Source # hasSign :: A -> Bool Source # intSizeOf :: A -> Int Source # isBoolean :: A -> Bool Source # isBounded :: A -> Bool Source # isReal :: A -> Bool Source # isFloat :: A -> Bool Source # isDouble :: A -> Bool Source # isRational :: A -> Bool Source # isFP :: A -> Bool Source # isUnbounded :: A -> Bool Source # isUserSort :: A -> Bool Source # isChar :: A -> Bool Source # isString :: A -> Bool Source # isList :: A -> Bool Source # isSet :: A -> Bool Source # isTuple :: A -> Bool Source # isMaybe :: A -> Bool Source # isEither :: A -> Bool Source # isArray :: A -> Bool Source # showType :: A -> String Source #
SatModel A Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods parseCVs :: [CV] -> Maybe (A, [CV]) Source # cvtModel :: (A -> Maybe b) -> Maybe (A, [CV]) -> Maybe (b, [CV]) Source #

type SA = SBV A Source #

Symbolic version of the type A.

data B Source #

Data declaration for an uninterpreted type, usually indicating target.

Instances

Instances details

Data B Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> B -> c B # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c B # toConstr :: B -> Constr # dataTypeOf :: B -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c B) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c B) # gmapT :: (forall b. Data b => b -> b) -> B -> B # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> B -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> B -> r # gmapQ :: (forall d. Data d => d -> u) -> B -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> B -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> B -> m B # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> B -> m B # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> B -> m B #
Read B Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods readsPrec :: Int -> ReadS B # readList :: ReadS [B] # readPrec :: ReadPrec B # readListPrec :: ReadPrec [B] #
Show B Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods showsPrec :: Int -> B -> ShowS # show :: B -> String # showList :: [B] -> ShowS #
SymVal B Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV B) Source # literal :: B -> SBV B Source # fromCV :: CV -> B Source # isConcretely :: SBV B -> (B -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV B) Source # free_ :: MonadSymbolic m => m (SBV B) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV B] Source # symbolic :: MonadSymbolic m => String -> m (SBV B) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV B] Source # unliteral :: SBV B -> Maybe B Source # isConcrete :: SBV B -> Bool Source # isSymbolic :: SBV B -> Bool Source #
HasKind B Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods kindOf :: B -> Kind Source # hasSign :: B -> Bool Source # intSizeOf :: B -> Int Source # isBoolean :: B -> Bool Source # isBounded :: B -> Bool Source # isReal :: B -> Bool Source # isFloat :: B -> Bool Source # isDouble :: B -> Bool Source # isRational :: B -> Bool Source # isFP :: B -> Bool Source # isUnbounded :: B -> Bool Source # isUserSort :: B -> Bool Source # isChar :: B -> Bool Source # isString :: B -> Bool Source # isList :: B -> Bool Source # isSet :: B -> Bool Source # isTuple :: B -> Bool Source # isMaybe :: B -> Bool Source # isEither :: B -> Bool Source # isArray :: B -> Bool Source # showType :: B -> String Source #
SatModel B Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods parseCVs :: [CV] -> Maybe (B, [CV]) Source # cvtModel :: (B -> Maybe b) -> Maybe (B, [CV]) -> Maybe (b, [CV]) Source #

type SB = SBV B Source #

Symbolic version of the type B.

data C Source #

Data declaration for an uninterpreted type, usually indicating an intermediate value.

Instances

Instances details

Data C Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> C -> c C # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c C # toConstr :: C -> Constr # dataTypeOf :: C -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c C) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c C) # gmapT :: (forall b. Data b => b -> b) -> C -> C # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> C -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> C -> r # gmapQ :: (forall d. Data d => d -> u) -> C -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> C -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> C -> m C # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> C -> m C # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> C -> m C #
Read C Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods readsPrec :: Int -> ReadS C # readList :: ReadS [C] # readPrec :: ReadPrec C # readListPrec :: ReadPrec [C] #
Show C Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods showsPrec :: Int -> C -> ShowS # show :: C -> String # showList :: [C] -> ShowS #
SymVal C Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV C) Source # literal :: C -> SBV C Source # fromCV :: CV -> C Source # isConcretely :: SBV C -> (C -> Bool) -> Bool Source # free :: MonadSymbolic m => String -> m (SBV C) Source # free_ :: MonadSymbolic m => m (SBV C) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV C] Source # symbolic :: MonadSymbolic m => String -> m (SBV C) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV C] Source # unliteral :: SBV C -> Maybe C Source # isConcrete :: SBV C -> Bool Source # isSymbolic :: SBV C -> Bool Source #
HasKind C Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods kindOf :: C -> Kind Source # hasSign :: C -> Bool Source # intSizeOf :: C -> Int Source # isBoolean :: C -> Bool Source # isBounded :: C -> Bool Source # isReal :: C -> Bool Source # isFloat :: C -> Bool Source # isDouble :: C -> Bool Source # isRational :: C -> Bool Source # isFP :: C -> Bool Source # isUnbounded :: C -> Bool Source # isUserSort :: C -> Bool Source # isChar :: C -> Bool Source # isString :: C -> Bool Source # isList :: C -> Bool Source # isSet :: C -> Bool Source # isTuple :: C -> Bool Source # isMaybe :: C -> Bool Source # isEither :: C -> Bool Source # isArray :: C -> Bool Source # showType :: C -> String Source #
SatModel C Source #
Instance details Defined in Documentation.SBV.Examples.KnuckleDragger.Lists Methods parseCVs :: [CV] -> Maybe (C, [CV]) Source # cvtModel :: (C -> Maybe b) -> Maybe (C, [CV]) -> Maybe (b, [CV]) Source #

type SC = SBV C Source #

Symbolic version of the type C.

Appending null

appendNull :: IO Proof Source #

xs ++ [] == xs

We have:

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

Moving cons over append

consApp :: IO Proof Source #

(x : xs) ++ ys == x : (xs ++ ys)

We have:

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

Associativity of append

appendAssoc :: IO Proof Source #

(xs ++ ys) ++ zs == xs ++ (ys ++ zs)

We have:

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

Surprisingly, z3 can prove this without any induction. (Since SBV's append translates directly to the concatenation of sequences in SMTLib, it must trigger an internal heuristic in z3 that proves it right out-of-the-box!)

Reverse and append

revCons :: IO Proof Source #

reverse (x:xs) == reverse xs ++ [x]

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

revApp :: IO Proof Source #

reverse (xs ++ ys) .== reverse ys ++ reverse xs

We have:

>>> revApp
Inductive lemma: revApp
  Base: revApp.Base                     Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: revApp.Step                     Q.E.D.
[Proven] revApp

Reversing twice is identity

reverseReverse :: IO Proof Source #

reverse (reverse xs) == xs

We have:

>>> reverseReverse
Inductive lemma: revApp
  Base: revApp.Base                     Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: revApp.Step                     Q.E.D.
Inductive lemma: reverseReverse
  Base: reverseReverse.Base             Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: reverseReverse.Step             Q.E.D.
[Proven] reverseReverse

Lengths of lists

lengthTail :: IO Proof Source #

length (x : xs) = 1 + length xs

We have:

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

badLengthProof :: IO () Source #

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

>>> badLengthProof `catch` (\(_ :: SomeException) -> pure ())
Lemma: badLengthProof
*** Failed to prove badLengthProof.
Falsifiable. Counter-example:
  xs   = [15,11,13,16,27,42] :: [Integer]
  imp  =                  42 :: Integer
  spec =                   6 :: Integer

lenAppend :: IO Proof Source #

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

We have:

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

lenAppend2 :: IO Proof Source #

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

We have:

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

Any, all, and filtering

allAny :: IO Proof Source #

not (all id xs) == any not xs

A list of booleans is not all true, if any of them is false. We have:

>>> allAny
Inductive lemma: allAny
  Base: allAny.Base                     Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: allAny.Step                     Q.E.D.
[Proven] allAny

filterEx :: IO Proof Source #

If an integer list doesn't have 2 as an element, then filtering for > 2 or .>= 2 yields the same result. We have:

>>> filterEx
Inductive lemma: filterEx
  Base: filterEx.Base                   Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: filterEx.Step                   Q.E.D.
[Proven] filterEx

filterEx2 :: IO () Source #

The filterEx example above, except we get a counter-example if 2 can be in the list. Note that we don't need the induction tactic here.

>>> filterEx2 `catch` (\(_ :: SomeException) -> pure ())
Lemma: filterEx2
*** Failed to prove filterEx2.
Falsifiable. Counter-example:
  xs = [2] :: [Integer]

Map, append, and reverse

mapEquiv :: IO Proof Source #

f = g => map f xs = map g xs

>>> mapEquiv
Inductive lemma: mapEquiv
  Base: mapEquiv.Base                   Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: mapEquiv.Step                   Q.E.D.
[Proven] mapEquiv

mapAppend :: (SA -> SB) -> IO Proof Source #

map f (xs ++ ys) == map f xs ++ map f ys

>>> mapAppend (uninterpret "f")
Inductive lemma: mapAppend
  Base: mapAppend.Base                  Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: mapAppend.Step                  Q.E.D.
[Proven] mapAppend

mapReverse :: IO Proof Source #

map f . reverse == reverse . map f

>>> mapReverse
Inductive lemma: mapAppend
  Base: mapAppend.Base                  Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: mapAppend.Step                  Q.E.D.
Inductive lemma: mapReverse
  Base: mapReverse.Base                 Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: mapReverse.Step                 Q.E.D.
[Proven] mapReverse

Reverse and length

revLen :: IO Proof Source #

length xs == length (reverse xs)

We have:

>>> revLen
Inductive lemma: revLen
  Base: revLen.Base                     Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: revLen.Step                     Q.E.D.
[Proven] revLen

badRevLen :: IO () Source #

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 = [A_1,A_2,A_1] :: [A]

Foldr-map fusion

foldrMapFusion :: IO Proof Source #

foldr f a . map g = foldr (f . g) a

We have:

>>> foldrMapFusion
Inductive lemma: foldrMapFusion
  Base: foldrMapFusion.Base             Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: foldrMapFusion.Step             Q.E.D.
[Proven] foldrMapFusion

Foldr-foldr fusion

foldrFusion :: IO Proof Source #

  Given f a = b and f (g x y) = h x (f y), for all x and y
  We have: f . foldr g a = foldr h b

>>> foldrFusion
Inductive lemma: foldrFusion
  Base: foldrFusion.Base                Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: foldrFusion.Step                Q.E.D.
[Proven] foldrFusion

Foldr over append

foldrOverAppend :: IO Proof Source #

foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs

We have:

>>> foldrOverAppend
Inductive lemma: foldrOverAppend
  Base: foldrOverAppend.Base            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: foldrOverAppend.Step            Q.E.D.
[Proven] foldrOverAppend

Foldl over append

foldlOverAppend :: (SB -> SA -> SB) -> IO Proof Source #

foldl f a (xs ++ ys) == foldl f (foldl f a xs) ys

We have:

>>> foldlOverAppend (uninterpret "f")
Inductive lemma: foldlOverAppend
  Base: foldlOverAppend.Base            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: foldlOverAppend.Step            Q.E.D.
[Proven] foldlOverAppend

Foldr-foldl correspondence

foldrFoldlDuality :: IO Proof Source #

foldr f e xs == foldl (flip f) e (reverse xs)

We have:

>>> foldrFoldlDuality
Inductive lemma: foldlOverAppend
  Base: foldlOverAppend.Base            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: foldlOverAppend.Step            Q.E.D.
Inductive lemma: foldrFoldlDuality
  Base: foldrFoldlDuality.Base          Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: foldrFoldlDuality.Step          Q.E.D.
[Proven] foldrFoldlDuality

Foldr-foldl duality, generalized

foldrFoldlDualityGeneralized :: IO Proof Source #

Given:

    x @ (y @ z) = (x @ y) @ z     (associativity of @)
and e @ x = x                     (left unit)
and x @ e = x                     (right unit)

Prove:

    foldr (@) e xs = foldl (@) e xs

We have:

>>> foldrFoldlDualityGeneralized
Inductive lemma: helper
  Base: helper.Base                     Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: helper.Step                     Q.E.D.
Inductive lemma: foldrFoldlDuality
  Base: foldrFoldlDuality.Base          Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Asms: 5                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: foldrFoldlDuality.Step          Q.E.D.
[Proven] foldrFoldlDuality

Another foldl-foldr correspondence

foldrFoldl :: IO Proof Source #

Given:

       (x <+> y) <*> z = x <+> (y <*> z)
  and  x <+> e = e <*> x

Proves:

   foldr (<+>) e xs = foldl (<*>) e xs

In Bird's Introduction to Functional Programming book (2nd edition) this is called the second duality theorem. We have:

>>> foldrFoldl
Inductive lemma: foldl over <*>/<+>
  Base: foldl over <*>/<+>.Base         Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: foldl over <*>/<+>.Step         Q.E.D.
Inductive lemma: foldrFoldl
  Base: foldrFoldl.Base                 Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: foldrFoldl.Step                 Q.E.D.
[Proven] foldrFoldl

Bookkeeping law

bookKeeping :: IO Proof Source #

Provided f is associative and a is its both left and right-unit:

foldr f a . concat == foldr f a . map (foldr f a)

We have:

>>> bookKeeping
Inductive lemma: foldBase
  Base: foldBase.Base                   Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: foldBase.Step                   Q.E.D.
Inductive lemma: foldrOverAppend
  Base: foldrOverAppend.Base            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: foldrOverAppend.Step            Q.E.D.
Inductive lemma: bookKeeping
  Base: bookKeeping.Base                Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: bookKeeping.Step                Q.E.D.
[Proven] bookKeeping

NB. As of early 2025, we cannot express the above theorem in SBV directly, since it involves nested lambdas. (On the right hand side map has an argument that is represented as a foldr, which itself has a lambda.) As SMTLib moves to a higher-order logic, we intend to make such expressions readily expressable. In the mean time, we use an equivalent (albeit roundabout) version, where we define map-foldr combo as a recursive function ourselves.

NB. This theorem does not hold if f does not have a left-unit! Consider the input [[], [x]]. Left hand side reduces to x, while the right hand side reduces to: f a x. And unless f is commutative or a is not also a left-unit, then one can find a counter-example. (Aside: if both left and right units exist for a binary operator, then they are necessarily the same element, since l = f l r = r. So, an equivalent statement could simply say f has both left and right units.) A concrete counter-example is:

  data T = A | B | C

  f :: T -> T -> T
  f C A = A
  f C B = A
  f x _ = x

You can verify f is associative. Also note that C is the right-unit for f, but it isn't the left-unit. In fact, f has no-left unit by the above argument. In this case, the bookkeeping law produces B for the left-hand-side, and A for the right-hand-side for the input [[], [B]].

Filter-append

filterAppend :: (SA -> SBool) -> IO Proof Source #

filter p (xs ++ ys) == filter p xs ++ filter p ys

We have:

>>> filterAppend (uninterpret "p")
Inductive lemma: filterAppend
  Base: filterAppend.Base               Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: filterAppend.Step               Q.E.D.
[Proven] filterAppend

filterConcat :: IO Proof Source #

filter p (concat xss) == concatMap (filter p xss)

Similar to the book-keeping law, we cannot express this in SBV directly, since it involves a nested lambda. concatMap (filter p) maps a higher-order function filter p, which itself has a nested lambda. So, we use our own merged definition. Hopefully we'll relax this as SMTLib gains more higher order features.

We have:

>>> filterConcat
Inductive lemma: filterAppend
  Base: filterAppend.Base               Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: filterAppend.Step               Q.E.D.
Inductive lemma: filterConcat
  Base: filterConcat.Base               Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: filterConcat.Step               Q.E.D.
[Proven] filterConcat

Map and filter don't commute

mapFilter :: IO () Source #

In general, mapping and filtering operations do not commute. We'll see the kind of counter-example we get from SBV if we attempt to prove:

>>> mapFilter `catch` (\(_ :: SomeException) -> pure ())
Lemma: badMapFilter
*** Failed to prove badMapFilter.
Falsifiable. Counter-example:
  xs  = [A_3] :: [A]
  lhs = [A_0] :: [A]
  rhs =    [] :: [A]

  f :: A -> A
  f _ = A_0

  p :: A -> Bool
  p A_3 = True
  p _   = False

As expected, the function f maps everything to A_0, and the predicate p only lets A_3 through. As shown in the counter-example, for the input [A_3], left-hand-side filters nothing and the result is the singleton A_0. But the map on the right-hand side maps everything to [A_0] and the filter gets rid of the elements, resulting in an empty list.

Partition

partition1 :: IO Proof Source #

fst (partition f xs) == filter f xs

>>> partition1
Inductive lemma: partition1
  Base: partition1.Base                 Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: partition1.Step                 Q.E.D.
[Proven] partition1

partition2 :: IO Proof Source #

snd (partition f xs) == filter (not . f) xs

>>> partition2
Inductive lemma: partition2
  Base: partition2.Base                 Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: partition2.Step                 Q.E.D.
[Proven] partition2

Take and drop

take_take :: IO Proof Source #

take n (take m xs) = take (n smin m) xs

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

drop_drop :: IO Proof Source #

n >= 0 && m >= 0 => drop n (drop m xs) = drop (n + m) xs

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

take_drop :: IO Proof Source #

take n xs ++ drop n xs == xs

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

take_cons :: IO Proof Source #

n .> 0 => take n (x .: xs) = x .: take (n - 1) xs

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

take_map :: IO Proof Source #

take n (map f xs) == map f (take n xs)

>>> take_map
Lemma: take_cons                        Q.E.D.
Lemma: map1                             Q.E.D.
Lemma: take_map.n <= 0                  Q.E.D.
Inductive lemma: take_map.n > 0
  Base: take_map.n > 0.Base             Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Asms: 5                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: take_map.n > 0.Step             Q.E.D.
Lemma: take_map                         Q.E.D.
[Proven] take_map

drop_cons :: SymVal elt => Proxy elt -> IO Proof Source #

n .> 0 => drop n (x .: xs) = drop (n - 1) xs

>>> drop_cons (Proxy @A)
Lemma: drop_cons                        Q.E.D.
[Proven] drop_cons

drop_map :: IO Proof Source #

drop n (map f xs) == map f (drop n xs)

>>> drop_map
Lemma: drop_cons                        Q.E.D.
Lemma: drop_cons                        Q.E.D.
Lemma: drop_map.n <= 0                  Q.E.D.
Inductive lemma: drop_map.n > 0
  Base: drop_map.n > 0.Base             Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: drop_map.n > 0.Step             Q.E.D.
Lemma: drop_map
  Step  : 1                             Q.E.D.
  Step  : 2                             Q.E.D.
  Step  : 3                             Q.E.D.
  Step  : 4                             Q.E.D.
  Result:                               Q.E.D.
[Proven] drop_map

length_take :: IO Proof Source #

n >= 0 ==> length (take n xs) = length xs `min` n

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

length_drop :: IO Proof Source #

n >= 0 ==> length (drop n xs) = (length xs - n) `max` 0

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

take_all :: IO Proof Source #

length xs <= n ==> take n xs == xs

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

drop_all :: IO Proof Source #

length xs <= n ==> drop n xs == nil

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

take_append :: IO Proof Source #

take n (xs ++ ys) = (take n xs ++ take (n - length xs) ys)

>>> take_append
Lemma: take_append
  Step  : 1                             Q.E.D.
  Result:                               Q.E.D.
[Proven] take_append

drop_append :: IO Proof Source #

drop n (xs ++ ys) = drop n xs ++ drop (n - length xs) ys

NB. As of Feb 2025, z3 struggles to prove this, but cvc5 gets it out-of-the-box.

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

Summing via halving

sumHalves :: IO Proof Source #

We prove that summing a list can be done by halving the list, summing parts, and adding the results. The proof uses strong induction. We have:

>>> sumHalves
Inductive lemma: sumAppend
  Base: sumAppend.Base                  Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: sumAppend.Step                  Q.E.D.
Inductive lemma (strong): sumHalves
  Base: sumHalves.Base                  Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: sumHalves.Step                  Q.E.D.
[Proven] sumHalves

Zip

map_fst_zip :: IO Proof Source #

length xs = length ys ⟹ map fst (zip xs ys) = xs

>>> map_fst_zip
Inductive lemma: map_fst_zip
  Base: map_fst_zip.Base                Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: map_fst_zip.Step                Q.E.D.
[Proven] map_fst_zip

map_snd_zip :: IO Proof Source #

length xs = length ys ⟹ map snd (zip xs ys) = xs

>>> map_snd_zip
Inductive lemma: map_snd_zip
  Base: map_snd_zip.Base                Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: map_snd_zip.Step                Q.E.D.
[Proven] map_snd_zip

map_fst_zip_take :: IO Proof Source #

map fst (zip xs ys) = take (min (length xs) (length ys)) xs

>>> map_fst_zip_take
Lemma: take_cons                        Q.E.D.
Inductive lemma: map_fst_zip_take
  Base: map_fst_zip_take.Base           Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: map_fst_zip_take.Step           Q.E.D.
[Proven] map_fst_zip_take

map_snd_zip_take :: IO Proof Source #

map snd (zip xs ys) = take (min (length xs) (length ys)) xs

>>> map_snd_zip_take
Lemma: take_cons                        Q.E.D.
Inductive lemma: map_snd_zip_take
  Base: map_snd_zip_take.Base           Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: map_snd_zip_take.Step           Q.E.D.
[Proven] map_snd_zip_take