sbv-13.0: Documentation/SBV/Examples/TP/Reverse.hs
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.TP.Reverse
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Can we define the reverse function using no auxiliary functions, i.e., only
-- in terms of cons, head, tail, and itself (recursively)? This example
-- shows such a definition and proves that it is correct.
--
-- See Zohar Manna's 1974 "Mathematical Theory of Computation" book, where this
-- definition and its proof is presented as Example 5.36.
-----------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.TP.Reverse where
import Prelude hiding (head, tail, null, reverse, length, init, last, (++))
import Data.SBV
import Data.SBV.List hiding (partition)
import Data.SBV.TP
import qualified Data.SBV.TP.List as TP
#ifdef DOCTEST
-- $setup
-- >>> :set -XTypeApplications
-- >>> import Data.SBV.TP
#endif
-- * Reversing with no auxiliaries
-- | This definition of reverse uses no helper functions, other than the usual
-- head, tail, cons, and uncons to reverse a given list. Note that efficiency
-- is not our concern here, we call 'rev' itself three times in the body.
rev :: SymVal a => SList a -> SList a
rev = smtFunction "rev" $ \xs -> ite (null xs .|| null (tail xs)) xs
(let (x, as) = uncons xs
(hras, tas) = uncons (rev as)
in hras .: rev (x .: rev tas))
-- * Correctness proof
-- | Correctness the function 'rev'. We have:
--
-- >>> runTP $ correctness @Integer
-- Lemma: revLen Q.E.D.
-- Lemma: revApp Q.E.D.
-- Lemma: revSnoc Q.E.D.
-- Lemma: revRev Q.E.D.
-- Inductive lemma (strong): revCorrect
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (2 way full case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 (2 way full case split)
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2.1 Q.E.D.
-- Step: 1.2.2.2 Q.E.D.
-- Step: 1.2.2.3 Q.E.D.
-- Step: 1.2.2.4 Q.E.D.
-- Step: 1.2.2.5 Q.E.D.
-- Step: 1.2.2.6 (simplify head) Q.E.D.
-- Step: 1.2.2.7 Q.E.D.
-- Step: 1.2.2.8 (simplify tail) Q.E.D.
-- Step: 1.2.2.9 Q.E.D.
-- Step: 1.2.2.10 Q.E.D.
-- Step: 1.2.2.11 Q.E.D.
-- Step: 1.2.2.12 (substitute) Q.E.D.
-- Step: 1.2.2.13 Q.E.D.
-- Step: 1.2.2.14 Q.E.D.
-- Step: 1.2.2.15 Q.E.D.
-- Result: Q.E.D.
-- [Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool
correctness :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
correctness = do
-- Quietly import a few helpers from "Data.SBV.TP.List"
revLen <- recall "revLen" $ TP.revLen @a
revApp <- recall "revApp" $ TP.revApp @a
revSnoc <- recall "revSnoc" $ TP.revSnoc @a
revRev <- recall "revRev" $ TP.revRev @a
sInductWith cvc5 "revCorrect"
(\(Forall xs) -> rev xs .== reverse xs)
(length, []) $
\ih xs -> [] |- rev xs
=: split xs trivial
(\a as -> split as trivial
(\_ _ -> head (rev as) .: rev (a .: rev (tail (rev as)))
?? ih `at` Inst @"xs" as
=: head (reverse as) .: rev (a .: rev (tail (rev as)))
?? ih `at` Inst @"xs" as
=: head (reverse as) .: rev (a .: rev (tail (reverse as)))
?? ih `at` Inst @"xs" (tail (rev as))
=: head (reverse as) .: rev (a .: rev (tail (reverse as)))
?? revSnoc `at` (Inst @"x" (last as), Inst @"xs" (init as))
=: let w = init as
b = last as
in head (b .: reverse w) .: rev (a .: rev (tail (reverse as)))
?? "simplify head"
=: b .: rev (a .: rev (tail (reverse as)))
?? revSnoc `at` (Inst @"x" (last xs), Inst @"xs" (init as))
=: b .: rev (a .: rev (tail (b .: reverse w)))
?? "simplify tail"
=: b .: rev (a .: rev (reverse w))
?? ih `at` Inst @"xs" (reverse w)
?? revLen `at` Inst @"xs" w
=: b .: rev (a .: reverse (reverse w))
?? revRev `at` Inst @"xs" w
=: b .: rev (a .: w)
?? ih
=: b .: reverse (a .: w)
?? "substitute"
=: last as .: reverse (a .: init as)
?? revApp `at` (Inst @"xs" (a .: init as), Inst @"ys" [last as])
=: reverse (a .: init as ++ [last as])
=: reverse (a .: as)
=: reverse xs
=: qed))
{- HLint ignore correctness "Use last" -}
{- HLint ignore correctness "Redundant reverse" -}