sbv-14.1: Documentation/SBV/Examples/TP/SortHelpers.hs
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.TP.SortHelpers
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Various definitions and lemmas that are useful for sorting related proofs.
-----------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.TP.SortHelpers where
import Prelude hiding (null, length, tail, elem, head, (++), take, drop)
import Data.SBV
import Data.SBV.List
import Data.SBV.TP
import Documentation.SBV.Examples.TP.Lists
#ifdef DOCTEST
-- $setup
-- >>> :set -XTypeApplications
-- >>> import Data.SBV.TP
#endif
-- | A predicate testing whether a given list is non-decreasing.
nonDecreasing :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SBool
nonDecreasing = smtFunction "nonDecreasing"
$ \l -> [sCase| l of
[] -> sTrue
[_] -> sTrue
x : rest@(y : _) -> x .<= y .&& nonDecreasing rest
|]
-- | Are two lists permutations of each other?
isPermutation :: SymVal a => SList a -> SList a -> SBool
isPermutation xs ys = quantifiedBool (\(Forall @"x" x) -> count x xs .== count x ys)
-- | The tail of a non-decreasing list is non-decreasing. We have:
--
-- >>> runTP $ nonDecrTail @Integer
-- Lemma: nonDecrTail Q.E.D.
-- Functions proven terminating: nonDecreasing
-- [Proven] nonDecrTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
nonDecrTail :: forall a. (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrTail = lemma "nonDecrTail"
(\(Forall x) (Forall xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs)
[]
-- | If we insert an element that is less than the head of a nonDecreasing list, it remains nondecreasing. We have:
--
-- >>> runTP $ nonDecrIns @Integer
-- Lemma: nonDecrInsert Q.E.D.
-- Functions proven terminating: nonDecreasing
-- [Proven] nonDecrInsert :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
nonDecrIns :: forall a. (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrIns = lemma "nonDecrInsert"
(\(Forall x) (Forall xs) -> nonDecreasing xs .&& sNot (null xs) .&& x .<= head xs .=> nonDecreasing (x .: xs))
[]
-- | Sublist relationship
sublist :: SymVal a => SList a -> SList a -> SBool
sublist xs ys = quantifiedBool (\(Forall @"e" e) -> count e xs .> 0 .=> count e ys .> 0)
-- | 'sublist' correctness. We have:
--
-- >>> runTP $ sublistCorrect @Integer
-- Inductive lemma: countNonNeg
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1.1 Q.E.D.
-- Step: 1.1.2 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Inductive lemma: countElem
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1.1 Q.E.D.
-- Step: 1.1.2 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Inductive lemma: elemCount
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Lemma: sublistCorrect
-- Step: 1 Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: count
-- [Proven] sublistCorrect :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐx ∷ Integer → Bool
sublistCorrect :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
sublistCorrect = do
cElem <- countElem @a
eCount <- elemCount @a
calc "sublistCorrect"
(\(Forall xs) (Forall ys) (Forall x) -> xs `sublist` ys .&& x `elem` xs .=> x `elem` ys) $
\xs ys x -> [xs `sublist` ys, x `elem` xs]
|- x `elem` ys
?? cElem `at` (Inst @"xs" xs, Inst @"e" x)
?? eCount `at` (Inst @"xs" ys, Inst @"e" x)
=: sTrue
=: qed
-- | If one list is a sublist of another, then its head is an elem. We have:
--
-- >>> runTP $ sublistElem @Integer
-- Inductive lemma: countNonNeg
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1.1 Q.E.D.
-- Step: 1.1.2 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Inductive lemma: countElem
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1.1 Q.E.D.
-- Step: 1.1.2 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Inductive lemma: elemCount
-- Step: Base Q.E.D.
-- Step: 1 (2 way case split)
-- Step: 1.1 Q.E.D.
-- Step: 1.2.1 Q.E.D.
-- Step: 1.2.2 Q.E.D.
-- Step: 1.Completeness Q.E.D.
-- Result: Q.E.D.
-- Lemma: sublistCorrect
-- Step: 1 Q.E.D.
-- Result: Q.E.D.
-- Lemma: sublistElem
-- Step: 1 Q.E.D.
-- Result: Q.E.D.
-- Functions proven terminating: count
-- [Proven] sublistElem :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
sublistElem :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistElem = do
slc <- sublistCorrect @a
calc "sublistElem"
(\(Forall x) (Forall xs) (Forall ys) -> (x .: xs) `sublist` ys .=> x `elem` ys) $
\x xs ys -> [(x .: xs) `sublist` ys]
|- x `elem` ys
?? slc `at` (Inst @"xs" (x .: xs), Inst @"ys" ys, Inst @"x" x)
=: sTrue
=: qed
-- | If one list is a sublist of another so is its tail. We have:
--
-- >>> runTP $ sublistTail @Integer
-- Lemma: sublistTail Q.E.D.
-- Functions proven terminating: count
-- [Proven] sublistTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
sublistTail :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistTail =
lemma "sublistTail"
(\(Forall x) (Forall xs) (Forall ys) -> (x .: xs) `sublist` ys .=> xs `sublist` ys)
[]
-- | Permutation implies sublist. We have:
--
-- >>> runTP $ sublistIfPerm @Integer
-- Lemma: sublistIfPerm Q.E.D.
-- Functions proven terminating: count
-- [Proven] sublistIfPerm :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
sublistIfPerm :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistIfPerm = lemma "sublistIfPerm"
(\(Forall xs) (Forall ys) -> isPermutation xs ys .=> xs `sublist` ys)
[]