| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.TP.List
Description
A variety of TP 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
- appendNull :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
- consApp :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- appendAssoc :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "zs" [a] -> SBool))
- initsLength :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
- tailsLength :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
- tailsAppend :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- revLen :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
- revApp :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- revCons :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
- revSnoc :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
- revRev :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
- enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
- revNM :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
- lengthTail :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
- lenAppend :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- lenAppend2 :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- replicateLength :: SymVal a => TP (Proof (Forall "k" Integer -> Forall "x" a -> SBool))
- allAny :: TP (Proof (Forall "xs" [Bool] -> SBool))
- mapEquiv :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))
- mapAppend :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- mapReverse :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))
- mapCompose :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> (SBV b -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))
- foldrMapFusion :: (SymVal a, SymVal b, SymVal c) => SBV c -> (SBV a -> SBV b) -> (SBV b -> SBV c -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))
- foldrFusion :: (SymVal a, SymVal b, SymVal c) => SBV c -> SBV b -> (SBV c -> SBV b) -> (SBV a -> SBV c -> SBV c) -> (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))
- foldrOverAppend :: SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- foldlOverAppend :: (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" b -> SBool))
- foldrFoldlDuality :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "e" b -> SBool))
- foldrFoldlDualityGeneralized :: SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> SBool))
- foldrFoldl :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b -> TP (Proof (Forall "xs" [a] -> SBool))
- bookKeeping :: SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xss" [[a]] -> SBool))
- filterAppend :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- filterConcat :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xss" [[a]] -> SBool))
- takeDropWhile :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))
- destutter :: SymVal a => SList a -> SList a
- destutterIdempotent :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
- appendDiff :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))
- diffAppend :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))
- diffDiff :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))
- partition1 :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))
- partition2 :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))
- take_take :: SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))
- drop_drop :: SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))
- take_drop :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- take_cons :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))
- take_map :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- drop_cons :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))
- drop_map :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- length_take :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- length_drop :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- take_all :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- drop_all :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
- take_append :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- drop_append :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- map_fst_zip :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
- map_snd_zip :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
- map_fst_zip_take :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
- map_snd_zip_take :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
- count :: SymVal a => SBV a -> SList a -> SInteger
- countAppend :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))
- takeDropCount :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool))
- countNonNeg :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
- countElem :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
- elemCount :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
- disjoint :: (Eq a, SymVal a) => SList a -> SList a -> SBool
- disjointDiff :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> SBool))
- interleave :: SymVal a => SList a -> SList a -> SList a
- uninterleave :: SymVal a => SList a -> STuple [a] [a]
- interleaveLen :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
- interleaveRoundTrip :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
Append
appendNull :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) Source #
xs ++ [] == xs
>>>runTP $ appendNull @IntegerLemma: appendNull Q.E.D. [Proven] appendNull :: Ɐxs ∷ [Integer] → Bool
consApp :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
(x : xs) ++ ys == x : (xs ++ ys)
>>>runTP $ consApp @IntegerLemma: consApp Q.E.D. [Proven] consApp :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
appendAssoc :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "zs" [a] -> SBool)) Source #
(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
>>>runTP $ appendAssoc @IntegerLemma: appendAssoc Q.E.D. [Proven] appendAssoc :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐzs ∷ [Integer] → Bool
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!)
initsLength :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) Source #
length (inits xs) == 1 + length xs
>>>runTP $ initsLength @IntegerInductive lemma (strong): initsLength Step: Measure is non-negative Q.E.D. Step: 1 Q.E.D. Result: Q.E.D. [Proven] initsLength :: Ɐxs ∷ [Integer] → Bool
tailsLength :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) Source #
length (tails xs) == 1 + length xs
>>>runTP $ tailsLength @IntegerInductive lemma: tailsLength Step: Base Q.E.D. 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] tailsLength :: Ɐxs ∷ [Integer] → Bool
tailsAppend :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
tails (xs ++ ys) == map (++ ys) (tails xs) ++ tail (tails ys)
This property comes from Richard Bird's "Pearls of functional Algorithm Design" book, chapter 2.
Note that it is not exactly as stated there, as the definition of tail Bird uses is different
than the standard Haskell function tails: Bird's version does not return the empty list as the
tail. So, we slightly modify it to fit the standard definition. (NB. z3 is finicky on this
problem, while cvc5 works much better.)
>>>runTPWith cvc5 $ tailsAppend @IntegerInductive lemma: base case Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Result: Q.E.D. Lemma: helper Step: 1 Q.E.D. Step: 2 Q.E.D. Result: Q.E.D. Inductive lemma: tailsAppend Step: Base Q.E.D. 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] tailsAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
Reverse
revLen :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) Source #
length xs == length (reverse xs)
>>>runTP $ revLen @IntegerInductive lemma: revLen Step: Base Q.E.D. 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] revLen :: Ɐxs ∷ [Integer] → Bool
revApp :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
reverse (xs ++ ys) .== reverse ys ++ reverse xs
>>>runTP $ revApp @IntegerInductive lemma: revApp Step: 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. Result: Q.E.D. [Proven] revApp :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
revCons :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) Source #
reverse (x:xs) == reverse xs ++ [x]
>>>runTP $ revCons @IntegerLemma: revCons Q.E.D. [Proven] revCons :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
revSnoc :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) Source #
reverse (xs ++ [x]) == x : reverse xs
>>>runTP $ revSnoc @IntegerInductive lemma: revApp Step: 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. Result: Q.E.D. Lemma: revSnoc Q.E.D. [Proven] revSnoc :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
revRev :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) Source #
reverse (reverse xs) == xs
>>>runTP $ revRev @IntegerInductive lemma: revApp Step: 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. Result: Q.E.D. Inductive lemma: revRev Step: Base Q.E.D. 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] revRev :: Ɐxs ∷ [Integer] → Bool
enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)) Source #
\(\text{length } [n \dots m] = \max(0,\; m - n + 1)\)
The proof uses the metric |m-n|.
>>>runTP enumLenInductive lemma (strong): enumLen Step: Measure is non-negative Q.E.D. Step: 1 (2 way case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.2.3 Q.E.D. Step: 1.2.4 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] enumLen :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
revNM :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool)) Source #
reverse [n .. m] == [m, m-1 .. n]
The proof uses the metric |m-n|.
>>>runTP $ revNMInductive lemma (strong): helper Step: Measure is non-negative Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Result: Q.E.D. Inductive lemma (strong): revNM Step: Measure is non-negative Q.E.D. Step: 1 (2 way case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.2.3 Q.E.D. Step: 1.2.4 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] revNM :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
Length
lengthTail :: SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) Source #
length (x : xs) == 1 + length xs
>>>runTP $ lengthTail @IntegerLemma: lengthTail Q.E.D. [Proven] lengthTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
lenAppend :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
length (xs ++ ys) == length xs + length ys
>>>runTP $ lenAppend @IntegerLemma: lenAppend Q.E.D. [Proven] lenAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
lenAppend2 :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
length xs == length ys -> length (xs ++ ys) == 2 * length xs
>>>runTP $ lenAppend2 @IntegerLemma: lenAppend2 Q.E.D. [Proven] lenAppend2 :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
Replicate
replicateLength :: SymVal a => TP (Proof (Forall "k" Integer -> Forall "x" a -> SBool)) Source #
length (replicate k x) == max (0, k)
>>>runTP $ replicateLength @IntegerInductive lemma: replicateLength Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.2.3 Q.E.D. Step: 1.2.4 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] replicateLength :: Ɐk ∷ Integer → Ɐx ∷ Integer → Bool
All and any
allAny :: TP (Proof (Forall "xs" [Bool] -> SBool)) Source #
not (all id xs) == any not xs
A list of booleans is not all true, if any of them is false.
>>>runTP allAnyInductive lemma: allAny Step: Base Q.E.D. 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] allAny :: Ɐxs ∷ [Bool] → Bool
Map
mapEquiv :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
f == g ==> map f xs == map g xs
>>>runTP $ mapEquiv @Integer @Integer (uninterpret "f") (uninterpret "g")Inductive lemma: mapEquiv Step: Base Q.E.D. 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] mapEquiv :: Ɐxs ∷ [Integer] → Bool
mapAppend :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
map f (xs ++ ys) == map f xs ++ map f ys
>>>runTP $ mapAppend @Integer @Integer (uninterpret "f")Inductive lemma: mapAppend Step: 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. Result: Q.E.D. [Proven] mapAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
mapReverse :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
map f . reverse == reverse . map f
>>>runTP $ mapReverse @Integer @String (uninterpret "f")Inductive lemma: mapAppend Step: 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. Result: Q.E.D. Inductive lemma: mapReverse Step: 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. Result: Q.E.D. [Proven] mapReverse :: Ɐxs ∷ [Integer] → Bool
mapCompose :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> (SBV b -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
map f . map g == map (f . g)
>>>runTP $ mapCompose @Integer @Bool @String (uninterpret "f") (uninterpret "g")Inductive lemma: mapCompose Step: 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. Result: Q.E.D. [Proven] mapCompose :: Ɐxs ∷ [Integer] → Bool
Foldr and foldl
foldrMapFusion :: (SymVal a, SymVal b, SymVal c) => SBV c -> (SBV a -> SBV b) -> (SBV b -> SBV c -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
foldr f a . map g == foldr (f . g) a
>>>runTP $ foldrMapFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "c")Inductive lemma: foldrMapFusion Step: Base Q.E.D. 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] foldrMapFusion :: Ɐxs ∷ [[Char]] → Bool
foldrFusion :: (SymVal a, SymVal b, SymVal c) => SBV c -> SBV b -> (SBV c -> SBV b) -> (SBV a -> SBV c -> SBV c) -> (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
f . foldr g a == foldr h b provided, f a = b and for all x and y, f (g x y) == h x (f y).
>>>runTP $ foldrFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "f") (uninterpret "g") (uninterpret "h")Inductive lemma: foldrFusion Step: Base Q.E.D. 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] foldrFusion :: Ɐxs ∷ [[Char]] → Bool
foldrOverAppend :: SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs
>>>runTP $ foldrOverAppend @Integer (uninterpret "a") (uninterpret "f")Inductive lemma: foldrOverAppend Step: Base Q.E.D. 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] foldrOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
foldlOverAppend :: (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" b -> SBool)) Source #
foldl f e (xs ++ ys) == foldl f (foldl f e xs) ys
>>>runTP $ foldlOverAppend @Integer @Bool (uninterpret "f")Inductive lemma: foldlOverAppend Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Result: Q.E.D. [Proven] foldlOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Bool → Bool
foldrFoldlDuality :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "e" b -> SBool)) Source #
foldr f e xs == foldl (flip f) e (reverse xs)
>>>runTP $ foldrFoldlDuality @Integer @String (uninterpret "f")Inductive lemma: foldlOverAppend Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Result: Q.E.D. Inductive lemma: foldrFoldlDuality Step: 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. Result: Q.E.D. [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Ɐe ∷ [Char] → Bool
foldrFoldlDualityGeneralized :: SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
Given:
x @ (y @ z) = (x @ y) @ z (associativity of @) and e @ x = x (left unit) and x @ e = x (right unit)
Proves:
foldr (@) e xs == foldl (@) e xs
>>>runTP $ foldrFoldlDualityGeneralized @Integer (uninterpret "e") (uninterpret "|@|")Inductive lemma: helper Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. Inductive lemma: foldrFoldlDuality Step: 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. Result: Q.E.D. [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Bool
foldrFoldl :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b -> TP (Proof (Forall "xs" [a] -> SBool)) 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:
>>>runTP $ foldrFoldl @Integer @String (uninterpret "<+>") (uninterpret "<*>") (uninterpret "e")Inductive lemma: foldl over <*>/<+> Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. Inductive lemma: foldrFoldl Step: 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. Result: Q.E.D. [Proven] foldrFoldl :: Ɐxs ∷ [Integer] → Bool
bookKeeping :: SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xss" [[a]] -> SBool)) 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)
>>>runTP $ bookKeeping @Integer (uninterpret "a") (uninterpret "f")Inductive lemma: foldBase Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. Inductive lemma: foldrOverAppend Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: Q.E.D. Inductive lemma: bookKeeping Step: 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. Result: Q.E.D. [Proven] bookKeeping :: Ɐxss ∷ [[Integer]] → Bool
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
filterAppend :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
filter p (xs ++ ys) == filter p xs ++ filter p ys
>>>runTP $ filterAppend @Integer (uninterpret "p")Inductive lemma: filterAppend Step: 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. Result: Q.E.D. [Proven] filterAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
filterConcat :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xss" [[a]] -> SBool)) Source #
filter p (concat xss) == concatMap (filter p xss)
>>>runTP $ filterConcat @Integer (uninterpret "f")Inductive lemma: filterAppend Step: 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. Result: Q.E.D. Inductive lemma: filterConcat Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Result: Q.E.D. [Proven] filterConcat :: Ɐxss ∷ [[Integer]] → Bool
takeDropWhile :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
takeWhile f xs ++ dropWhile f xs == xs
>>>runTP $ takeDropWhile @Integer (uninterpret "f")Inductive lemma: takeDropWhile Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1.1 Q.E.D. Step: 1.1.2 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] takeDropWhile :: Ɐxs ∷ [Integer] → Bool
Stutter removal
destutterIdempotent :: SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) Source #
destutter (destutter xs) == destutter xs
>>>runTP $ destutterIdempotent @IntegerInductive lemma: helper1 Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. Inductive lemma: helper2 Step: Base Q.E.D. Step: 1 Q.E.D. Result: Q.E.D. Inductive lemma (strong): helper3 Step: Measure is non-negative Q.E.D. Step: 1 (2 way full case split) Step: 1.1 Q.E.D. Step: 1.2 (2 way full case split) Step: 1.2.1 Q.E.D. Step: 1.2.2.1 Q.E.D. Step: 1.2.2.2 (2 way case split) Step: 1.2.2.2.1.1 Q.E.D. Step: 1.2.2.2.1.2 Q.E.D. Step: 1.2.2.2.2.1 Q.E.D. Step: 1.2.2.2.2.2 Q.E.D. Step: 1.2.2.2.Completeness Q.E.D. Result: Q.E.D. Lemma: destutterIdempotent Q.E.D. [Proven] destutterIdempotent :: Ɐxs ∷ [Integer] → Bool
Difference
appendDiff :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool)) Source #
(as ++ bs) \ cs == (as \ cs) ++ (bs \ cs)
>>>runTP $ appendDiff @IntegerInductive lemma: appendDiff Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Result: Q.E.D. [Proven] appendDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool
diffAppend :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool)) Source #
as \ (bs ++ cs) == (as \ bs) \ cs
>>>runTP $ diffAppend @IntegerInductive lemma: diffAppend Step: Base Q.E.D. 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] diffAppend :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool
diffDiff :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool)) Source #
(as \ bs) \ cs == (as \ cs) \ bs
>>>runTP $ diffDiff @IntegerInductive lemma: diffDiff Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1.1 Q.E.D. Step: 1.1.2 Q.E.D. Step: 1.1.3 (2 way case split) Step: 1.1.3.1 Q.E.D. Step: 1.1.3.2.1 Q.E.D. Step: 1.1.3.2.2 (a ∉ cs) Q.E.D. Step: 1.1.3.Completeness Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 (2 way case split) Step: 1.2.2.1.1 Q.E.D. Step: 1.2.2.1.2 Q.E.D. Step: 1.2.2.1.3 (a ∈ cs) Q.E.D. Step: 1.2.2.2.1 Q.E.D. Step: 1.2.2.2.2 Q.E.D. Step: 1.2.2.2.3 (a ∉ bs) Q.E.D. Step: 1.2.2.2.4 (a ∉ cs) Q.E.D. Step: 1.2.2.Completeness Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] diffDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool
Partition
partition1 :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
fst (partition f xs) == filter f xs
>>>runTP $ partition1 @Integer (uninterpret "f")Inductive lemma: partition1 Step: Base Q.E.D. 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] partition1 :: Ɐxs ∷ [Integer] → Bool
partition2 :: SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool)) Source #
snd (partition f xs) == filter (not . f) xs
>>>runTP $ partition2 @Integer (uninterpret "f")Inductive lemma: partition2 Step: Base Q.E.D. 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] partition2 :: Ɐxs ∷ [Integer] → Bool
Take and drop
take_take :: SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
take n (take m xs) == take (n smin m) xs>>>runTP $ take_take @IntegerLemma: take_take Q.E.D. [Proven] take_take :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
drop_drop :: SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
n >= 0 && m >= 0 ==> drop n (drop m xs) == drop (n + m) xs
>>>runTP $ drop_drop @IntegerLemma: drop_drop Q.E.D. [Proven] drop_drop :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
take_drop :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
take n xs ++ drop n xs == xs
>>>runTP $ take_drop @IntegerLemma: take_drop Q.E.D. [Proven] take_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
take_cons :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool)) Source #
n .> 0 ==> take n (x .: xs) == x .: take (n - 1) xs
>>>runTP $ take_cons @IntegerLemma: take_cons Q.E.D. [Proven] take_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
take_map :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
take n (map f xs) == map f (take n xs)
>>>runTP $ take_map @Integer @Integer (uninterpret "f")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 Step: 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. Result: Q.E.D. Lemma: take_map Step: 1 Q.E.D. Result: Q.E.D. [Proven] take_map :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
drop_cons :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool)) Source #
n .> 0 ==> drop n (x .: xs) == drop (n - 1) xs
>>>runTP $ drop_cons @IntegerLemma: drop_cons Q.E.D. [Proven] drop_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
drop_map :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
drop n (map f xs) == map f (drop n xs)
>>>runTP $ drop_map @Integer @String (uninterpret "f")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 Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Step: 3 Q.E.D. Step: 4 Q.E.D. Result: 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 :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
length_take :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
n >= 0 ==> length (take n xs) == length xs `min` n
>>>runTP $ length_take @IntegerLemma: length_take Q.E.D. [Proven] length_take :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
length_drop :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
n >= 0 ==> length (drop n xs) == (length xs - n) `max` 0
>>>runTP $ length_drop @IntegerLemma: length_drop Q.E.D. [Proven] length_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
take_all :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
length xs <= n ==> take n xs == xs
>>>runTP $ take_all @IntegerLemma: take_all Q.E.D. [Proven] take_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
drop_all :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) Source #
length xs <= n ==> drop n xs == nil
>>>runTP $ drop_all @IntegerLemma: drop_all Q.E.D. [Proven] drop_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
take_append :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
take n (xs ++ ys) == (take n xs ++ take (n - length xs) ys)
>>>runTP $ take_append @IntegerLemma: take_append Q.E.D. [Proven] take_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
drop_append :: SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)) 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.
>>>runTP $ drop_append @IntegerLemma: drop_append Q.E.D. [Proven] drop_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
Zip
map_fst_zip :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool)) Source #
length xs == length ys ==> map fst (zip xs ys) = xs
>>>runTP $ map_fst_zip @Integer @IntegerInductive lemma: map_fst_zip Step: Base Q.E.D. 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] map_fst_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
map_snd_zip :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool)) Source #
length xs == length ys ==> map snd (zip xs ys) = xs
>>>runTP $ map_snd_zip @Integer @IntegerInductive lemma: map_snd_zip Step: Base Q.E.D. 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] map_snd_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
map_fst_zip_take :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool)) Source #
map fst (zip xs ys) == take (min (length xs) (length ys)) xs
>>>runTP $ map_fst_zip_take @Integer @IntegerLemma: take_cons Q.E.D. Inductive lemma: map_fst_zip_take Step: 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. Result: Q.E.D. [Proven] map_fst_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
map_snd_zip_take :: (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool)) Source #
map snd (zip xs ys) == take (min (length xs) (length ys)) xs
>>>runTP $ map_snd_zip_take @Integer @IntegerLemma: take_cons Q.E.D. Inductive lemma: map_snd_zip_take Step: 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. Result: Q.E.D. [Proven] map_snd_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
Counting elements
count :: SymVal a => SBV a -> SList a -> SInteger Source #
Count the number of occurrences of an element in a list
countAppend :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)) Source #
count e (xs ++ ys) == count e xs + count e ys
>>>runTP $ countAppend @IntegerInductive lemma: countAppend Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 (unfold count) Q.E.D. Step: 3 Q.E.D. Step: 4 (simplify) Q.E.D. Result: Q.E.D. [Proven] countAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Integer → Bool
takeDropCount :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool)) Source #
count e (take n xs) + count e (drop n xs) == count e xs
>>>runTP $ takeDropCount @IntegerInductive lemma: countAppend Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 (unfold count) Q.E.D. Step: 3 Q.E.D. Step: 4 (simplify) Q.E.D. Result: Q.E.D. Lemma: take_drop Q.E.D. Lemma: takeDropCount Step: 1 Q.E.D. Step: 2 Q.E.D. Result: Q.E.D. [Proven] takeDropCount :: Ɐxs ∷ [Integer] → Ɐn ∷ Integer → Ɐe ∷ Integer → Bool
countNonNeg :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool)) Source #
count e xs >= 0
>>>runTP $ countNonNeg @IntegerInductive lemma: countNonNeg Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1.1 Q.E.D. Step: 1.1.2 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] countNonNeg :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool
countElem :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool)) Source #
e `elem` xs ==> count e xs .> 0
>>>runTP $ countElem @IntegerInductive lemma: countNonNeg Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1.1 Q.E.D. Step: 1.1.2 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. Inductive lemma: countElem Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1.1 Q.E.D. Step: 1.1.2 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] countElem :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool
elemCount :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool)) Source #
count e xs .> 0 .=> e `elem` xs
>>>runTP $ elemCount @IntegerInductive lemma: elemCount Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. [Proven] elemCount :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool
Disjointness
disjointDiff :: (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> SBool)) Source #
disjoint as bs .=> as \ bs == as
>>>runTP $ disjointDiff @IntegerInductive lemma: disjointDiff Step: Base Q.E.D. Step: 1 Q.E.D. Step: 2 Q.E.D. Result: Q.E.D. [Proven] disjointDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Bool
Interleaving
interleave :: SymVal a => SList a -> SList a -> SList a Source #
Interleave the elements of two lists. If one ends, we take the rest from the other.
uninterleave :: SymVal a => SList a -> STuple [a] [a] Source #
Uninterleave the elements of two lists. We roughly split it into two, of alternating elements.
interleaveLen :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
Prove that interleave preserves total length.
The induction here is on the total length of the lists, and hence we use the generalized induction principle. We have:
>>>runTP $ interleaveLen @IntegerInductive lemma (strong): interleaveLen Step: Measure is non-negative Q.E.D. Step: 1 (2 way full case split) Step: 1.1 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 Q.E.D. Step: 1.2.3 Q.E.D. Result: Q.E.D. [Proven] interleaveLen :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
interleaveRoundTrip :: SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #
The functions uninterleave and interleave are inverses so long as the inputs are of the same length. (The equality
would even hold if the first argument has one extra element, but we keep things simple here.)
We have:
>>>runTP $ interleaveRoundTrip @IntegerLemma: revCons Q.E.D. Inductive lemma (strong): roundTripGen Step: Measure is non-negative Q.E.D. Step: 1 (4 way full case split) Step: 1.1 Q.E.D. Step: 1.2 Q.E.D. Step: 1.3 Q.E.D. Step: 1.4.1 Q.E.D. Step: 1.4.2 Q.E.D. Step: 1.4.3 Q.E.D. Step: 1.4.4 Q.E.D. Step: 1.4.5 Q.E.D. Step: 1.4.6 Q.E.D. Step: 1.4.7 Q.E.D. Step: 1.4.8 Q.E.D. Result: Q.E.D. Lemma: interleaveRoundTrip Step: 1 Q.E.D. Step: 2 Q.E.D. Result: Q.E.D. [Proven] interleaveRoundTrip :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool