sbv-14.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 QuasiQuotes #-}
{-# 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 Documentation.SBV.Examples.TP.Lists 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, and cons to reverse a given list. Note that efficiency
-- is not our concern here, we call 'rev' itself three times in the body.
rev :: forall a. SymVal a => SList a -> SList a
rev = smtFunctionWithMeasure "rev"
( length @a
, [measureLemma (revPreservesLen @a)]
)
$ \xs -> [sCase| xs of
[] -> xs
x : as -> case rev as of
[] -> [x]
hras : tas -> hras .: rev (x .: rev tas)
|]
-- | Reversing preserves length. Needed as a measure helper for 'rev'.
--
-- >>> runTP $ revPreservesLen @Integer
-- Inductive lemma (strong): revPreservesLen
-- Step: Measure is non-negative Q.E.D.
-- Step: 1 (3 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3.1 Q.E.D.
-- Step: 1.3.2 Q.E.D.
-- Step: 1.3.3 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: rev
-- [Proven] revPreservesLen :: Ɐxs ∷ [Integer] → Bool
revPreservesLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
revPreservesLen = sInductWith cvc5 "revPreservesLen"
(\(Forall xs) -> length (rev @a xs) .== length xs)
(length, []) $
\ih xs -> [] |- length (rev @a xs) .== length xs
=: [pCase| xs of
[] -> trivial
[_] -> trivial
whole@(a : as) -> length (head (rev as) .: rev (a .: rev (tail (rev as)))) .== length whole
-- Simplify: length (h .: e) = 1 + length e
=: (1 + length (rev (a .: rev (tail (rev as))))) .== (1 + length as)
-- Now apply the IH instances in order: each precondition depends on previous conclusions
?? ih `at` Inst @"xs" as
?? ih `at` Inst @"xs" (tail (rev as))
?? ih `at` Inst @"xs" (a .: rev (tail (rev as)))
=: sTrue
=: qed
|]
-- * 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 (3 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2 Q.E.D.
-- Step: 1.3.1 Q.E.D.
-- Step: 1.3.2 Q.E.D.
-- Step: 1.3.3 Q.E.D.
-- Step: 1.3.4 Q.E.D.
-- Step: 1.3.5 Q.E.D.
-- Step: 1.3.6 (simplify head) Q.E.D.
-- Step: 1.3.7 Q.E.D.
-- Step: 1.3.8 (simplify tail) Q.E.D.
-- Step: 1.3.9 Q.E.D.
-- Step: 1.3.10 Q.E.D.
-- Step: 1.3.11 Q.E.D.
-- Step: 1.3.12 (substitute) Q.E.D.
-- Step: 1.3.13 Q.E.D.
-- Step: 1.3.14 Q.E.D.
-- Step: 1.3.15 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: rev, sbv.reverse
-- [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 $ TP.revLen @a
revApp <- recall $ TP.revApp @a
revSnoc <- recall $ TP.revSnoc @a
revRev <- recall $ TP.revRev @a
sInductWith cvc5 "revCorrect"
(\(Forall xs) -> rev xs .== reverse xs)
(length, []) $
\ih xs -> [] |- rev xs
=: [pCase| xs of
[] -> trivial
[_] -> trivial
a : as -> 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" -}