tails package:sbv

tails of a list.

>>> tails ([] :: SList Integer)
[[]] :: [[SInteger]]

>>> tails [1,2,3,4::SInteger]
[[1,2,3,4],[2,3,4],[3,4],[4],[]] :: [[SInteger]]

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

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