len package:sbv

Coding list-length recursively. Again, we map directly to an SMTLib function.

Length of a list.

>>> sat $ \(l :: SList Word16) -> length l .== 2
Satisfiable. Model:
s0 = [0,0] :: [Word16]

>>> sat $ \(l :: SList Word16) -> length l .< 0
Unsatisfiable

>>> prove $ \(l1 :: SList Word16) (l2 :: SList Word16) -> length l1 + length l2 .== length (l1 ++ l2)
Q.E.D.

>>> sat $ \(s :: SString) -> length s .== 2
Satisfiable. Model:
s0 = "BA" :: String

>>> sat $ \(s :: SString) -> length s .< 0
Unsatisfiable

>>> prove $ \(s1 :: SString) s2 -> length s1 + length s2 .== length (s1 ++ s2)
Q.E.D.

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

>>> runTP $ lenAppend @Integer
Lemma: lenAppend                        Q.E.D.
[Proven] lenAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool

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

>>> runTP $ lenAppend2 @Integer
Lemma: lenAppend2                       Q.E.D.
[Proven] lenAppend2 :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool

length (x : xs) == 1 + length xs

>>> runTP $ lengthTail @Integer
Lemma: lengthTail                       Q.E.D.
[Proven] lengthTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool

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

>>> runTP $ length_drop @Integer
Lemma: length_drop                      Q.E.D.
[Proven] length_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool

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

>>> runTP $ length_take @Integer
Lemma: length_take                      Q.E.D.
[Proven] length_take :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool

Calculate the length of a list, using recursive functions. We have:

>>> lenExample
Satisfiable. Model:
s0 = [1,2,3] :: [Integer]
s1 =       3 :: Integer

Proof of correctness of an imperative list-length algorithm, using weakest preconditions. Illustrates the use of SBV's symbolic lists together with the WP algorithm.

The state of the length program, paramaterized over the element type a

Unique length used for firstified higher-order function names

Line length for TP proofs

The proof uses the metric |m-n|.

>>> runTP enumLen
Inductive 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

length (inits xs) == 1 + length xs

>>> runTP $ initsLength @Integer
Inductive 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

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 @Integer
Inductive 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

length (replicate k x) == max (0, k)

>>> runTP $ replicateLength @Integer
Inductive 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

length xs == length (reverse xs)

>>> runTP $ revLen @Integer
Inductive 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

length (tails xs) == 1 + length xs

>>> runTP $ tailsLength @Integer
Inductive 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

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:

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

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)

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

A program is the algorithm, together with its pre- and post-conditions.