while package:sbv

A while loop: While name invariant measure condition body. The string name is merely for diagnostic purposes. If the measure is Nothing, then only partial correctness of this loop will be proven.

Symbolic equivalent of dropWhile >>> dropWhile ((x :: SInteger) -> x sMod 2 .== 0) (literal [1..10]) [1,2,3,4,5,6,7,8,9,10] :: [SInteger] >>> dropWhile ((x :: SInteger) -> x sMod 2 ./= 0) (literal [1..10]) [2,3,4,5,6,7,8,9,10] :: [SInteger]

Symbolic equivalent of takeWhile

>>> takeWhile (\(x :: SInteger) -> x `sMod` 2 .== 0) (literal [1..10])
[] :: [SInteger]

>>> takeWhile (\(x :: SInteger) -> x `sMod` 2 ./= 0) (literal [1..10])
[1] :: [SInteger]

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