-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.RevAcc
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proves that the accummulating version of reverse is equivalent to the
-- standard definition.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.RevAcc where

import Prelude hiding (head, tail, null, reverse, (++))

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

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

-- * Reversing with an accummulator.

-- | Accummulating reverse.
revAcc :: SymVal a => SList a -> SList a -> SList a
revAcc :: forall a. SymVal a => SList a -> SList a -> SList a
revAcc = String
-> (SList a -> SList a -> SList a) -> SList a -> SList a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"revAcc" ((SList a -> SList a -> SList a) -> SList a -> SList a -> SList a)
-> (SList a -> SList a -> SList a) -> SList a -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ \SList a
acc SList a
xs -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs) SList a
acc (SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
revAcc (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
xs SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
acc) (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
xs))

-- | Given 'revAcc', we can reverse a list by providing the empty list as the initial accumulator.
rev :: SymVal a => SList a -> SList a
rev :: forall a. SymVal a => SList a -> SList a
rev = SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
revAcc []

-- * Correctness proof

-- | Correctness the function 'rev'. We have:
--
-- >>> correctness @Integer
-- Inductive lemma: revAccCorrect
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: revCorrect                       Q.E.D.
-- [Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool
correctness :: forall a. SymVal a => IO (Proof (Forall "xs" [a] -> SBool))
correctness :: forall a. SymVal a => IO (Proof (Forall "xs" [a] -> SBool))
correctness = 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 lemma regarding 'revAcc'
  Proof (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
helper <- String
-> (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "acc" [a] -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> Forall "acc" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "acc" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> Forall "acc" [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
"revAccCorrect"
                   (\(Forall @"xs" (SBV [a]
xs :: SList a)) (Forall @"acc" SBV [a]
acc) -> SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
revAcc SBV [a]
acc SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
xs SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
++ SBV [a]
acc) ((Proof (IHType (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
  -> IHArg (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
  -> IStepArgs (Forall "xs" [a] -> Forall "acc" [a] -> SBool) [a])
 -> TP (Proof (Forall "xs" [a] -> Forall "acc" [a] -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "acc" [a] -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \Proof (IHType (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
ih (SBV a
x, SBV [a]
xs) SBV [a]
acc -> [] [SBool] -> TPProofRaw (SBV [a]) -> (SBool, TPProofRaw (SBV [a]))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
revAcc SBV [a]
acc (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs)
                                         SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
revAcc (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
acc) SBV [a]
xs
                                         SBV [a] -> Proof (Forall "acc" [a] -> SBool) -> Hinted (SBV [a])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "xs" [a] -> Forall "acc" [a] -> SBool))
Proof (Forall "acc" [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] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
xs SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
++ SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
acc
                                         SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
xs SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SBV [a])
SBV a
x]) SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
++ SBV [a]
acc
                                         SBV [a] -> ChainsTo (SBV [a]) -> ChainsTo (SBV [a])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse (SBV a
x SBV a -> SBV [a] -> SBV [a]
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
xs) SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
++ SBV [a]
acc
                                         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

  -- The main theorem simply follows from the helper:
  String
-> (Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"revCorrect"
        (\(Forall SBV [a]
xs) -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
rev SBV [a]
xs SBV [a] -> SBV [a] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a
reverse SBV [a]
xs)
        [Proof (Forall "xs" [a] -> Forall "acc" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> Forall "acc" [a] -> SBool)
helper]