content: -----------------------------------------------------------------------------
  -- |
  -- 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 = runTP $ do
  
    -- helper: sum distributes over append.
    sumAppend <- induct "sumAppend"
                        (\(Forall xs) (Forall ys) -> sum (xs ++ ys) .== sum xs + sum ys) $
                        \ih (x, xs) ys -> [] |- sum ((x .: xs) ++ ys)
                                             =: sum (x .: (xs ++ ys))
                                             =: x + sum (xs ++ ys)
                                             ?? ih
                                             =: x + (sum xs + sum ys)
                                             ?? "associativity"
                                             =: (x + sum xs) + sum ys
                                             =: sum (x .: xs) + sum ys
                                             =: qed
  
    -- Now prove the original theorem by induction
    induct "sumReverse"
           (\(Forall xs) -> sum (reverse xs) .== sum xs) $
           \ih (x, xs) -> [] |- sum (reverse (x .: xs))
                             =: sum (reverse xs ++ [x])
                             ?? sumAppend `at` (Inst @"xs" (reverse xs), Inst @"ys" [x])
                             =: sum (reverse xs) + sum [x]
                             ?? ih
                             =: sum xs + x
                             ?? "commutativity"
                             =: x + sum xs
                             =: sum (x .: xs)
                             =: qed
  