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.

Length of a string.

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

>>> sat $ \s -> length s .< 0
Unsatisfiable

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

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

We have:

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

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

We have:

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

length (x : xs) = 1 + length xs

We have:

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

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

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

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

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

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

Line length for KD proofs

See StrLen

String length

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

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]

length xs == length (reverse xs)

We have:

>>> revLen
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

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:

>>> interleaveLen
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

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