-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.SumReverse
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proves @sum (reverse xs) == sum xs@.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE OverloadedLists     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.SumReverse where

import Prelude hiding ((++), foldr, sum, reverse)

import Data.SBV
import Data.SBV.TP
import Data.SBV.List


#ifdef DOCTEST
-- $setup
-- >>> :set -XFlexibleContexts
-- >>> :set -XTypeApplications
#endif

-- | @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
revSum :: forall a. (SymVal a, Num (SBV a)) => IO (Proof (Forall "xs" [a] -> SBool))
revSum :: forall a.
(SymVal a, Num (SBV a)) =>
IO (Proof (Forall "xs" [a] -> SBool))
revSum = TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "xs" [a] -> SBool))
 -> IO (Proof (Forall "xs" [a] -> SBool)))
-> TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$ do

  -- helper: sum distributes over append.
  Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sumAppend <- String
-> (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) a)
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sumAppend"
                      (\(Forall SList a
xs) (Forall SList a
ys) -> SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList a
xs SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys) SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
xs SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
ys) ((Proof (IHType (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  -> IHArg (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
  -> IStepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) a)
 -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) a)
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
                      \Proof (IHType (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
ih (SBV a
x, SList a
xs) SList a
ys -> [] [SBool] -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum ((SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys)
                                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList a
xs SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys))
                                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList a
xs SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys)
                                           SBV a -> Proof (Forall "ys" [a] -> SBool) -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
Proof (Forall "ys" [a] -> SBool)
ih
                                           TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ (SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
xs SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
ys)
                                           SBV a -> String -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"associativity"
                                           TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV a
x SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
xs) SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
ys
                                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
ys
                                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV a)
TPProofRaw (SBV a)
forall a. TPProofRaw a
qed

  -- Now prove the original theorem by induction
  String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) a)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sumReverse"
         (\(Forall SList a
xs) -> SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse SList a
xs) SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
xs) ((Proof (IHType (Forall "xs" [a] -> SBool))
  -> IHArg (Forall "xs" [a] -> SBool)
  -> IStepArgs (Forall "xs" [a] -> SBool) a)
 -> TP (Proof (Forall "xs" [a] -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) a)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
         \Proof (IHType (Forall "xs" [a] -> SBool))
ih (SBV a
x, SList a
xs) -> [] [SBool] -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse SList a
xs SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
x])
                           SBV a -> Proof Bool -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sumAppend Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse SList a
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" [Item (SList a)
SBV a
x])
                           TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse SList a
xs) SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum [Item (SList a)
SBV a
x]
                           SBV a -> Proof SBool -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "xs" [a] -> SBool))
ih
                           TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
xs SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SBV a
x
                           SBV a -> String -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"commutativity"
                           TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList a
xs
                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBV a
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV a)
TPProofRaw (SBV a)
forall a. TPProofRaw a
qed