Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.TP.SumReverse

Description

Proves sum (reverse xs) == sum xs.

Synopsis

revSum :: (SymVal a, Num (SBV a)) => IO (Proof (Forall "xs" [a] -> SBool))

Documentation

revSum :: (SymVal a, Num (SBV a)) => IO (Proof (Forall "xs" [a] -> SBool)) Source #

sum (reverse xs) = sum xs

>>> revSum @Integer
Inductive lemma: sumAppend
  Step: Base                   Q.E.D.
  Step: 1                      Q.E.D.
  Step: 2                      Q.E.D.
  Step: 3                      Q.E.D.
  Step: 4 (associativity)      Q.E.D.
  Step: 5                      Q.E.D.
  Result:                      Q.E.D.
Inductive lemma: sumReverse
  Step: Base                   Q.E.D.
  Step: 1                      Q.E.D.
  Step: 2                      Q.E.D.
  Step: 3                      Q.E.D.
  Step: 4 (commutativity)      Q.E.D.
  Step: 5                      Q.E.D.
  Result:                      Q.E.D.
Functions proven terminating: sbv.foldr, sbv.reverse
[Proven] sumReverse :: Ɐxs ∷ [Integer] → Bool