RevAcc.hs

-----------------------------------------------------------------------------
-- |
-- 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 QuasiQuotes         #-}
{-# 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 = smtFunction "revAcc"
       $ \acc xs -> [sCase| xs of
                       []     -> acc
                       a : as -> revAcc (a .: acc) as
                    |]

-- | Given 'revAcc', we can reverse a list by providing the empty list as the initial accumulator.
rev :: SymVal a => SList a -> SList a
rev = 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.
-- Functions proven terminating: revAcc, sbv.reverse
-- [Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool
correctness :: forall a. SymVal a => IO (Proof (Forall "xs" [a] -> SBool))
correctness = runTP $ do

  -- Helper lemma regarding 'revAcc'
  helper <- induct "revAccCorrect"
                   (\(Forall @"xs" (xs :: SList a)) (Forall @"acc" acc) -> revAcc acc xs .== reverse xs ++ acc) $
                   \ih (x, xs) acc -> [] |- revAcc acc (x .: xs)
                                         =: revAcc (x .: acc) xs
                                         ?? ih
                                         =: reverse xs ++ x .: acc
                                         =: (reverse xs ++ [x]) ++ acc
                                         =: reverse (x .: xs) ++ acc
                                         =: qed

  -- The main theorem simply follows from the helper:
  lemma "revCorrect"
        (\(Forall xs) -> rev xs .== reverse xs)
        [proofOf helper]