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.
[Proven] sumReverse :: Ɐxs ∷ [Integer] → Bool