KD: Rearrange list proofs

Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs

@@ -0,0 +1,142 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.AppendRev
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- Example use of the KnuckleDragger, on list append and reverses.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
+{-# LANGUAGE TypeApplications    #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.AppendRev where
+
+import Prelude hiding (sum, length, reverse, (++))
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+
+import Data.SBV.List ((.:), (++), reverse)
+import qualified Data.SBV.List as SL
+
+-- | @xs ++ [] == xs@
+--
+-- We have:
+--
+-- >>> appendNull
+-- Lemma: appendNull                       Q.E.D.
+appendNull :: IO Proven
+appendNull = lemma "appendNull"
+                (\(Forall @"xs" (xs :: SList Integer)) -> xs ++ SL.nil .== xs)
+                []
+
+-- | @(x : xs) ++ ys == x : (xs ++ ys)@
+--
+-- We have:
+-- >>> consApp
+-- Lemma: consApp                          Q.E.D.
+consApp :: IO Proven
+consApp = lemma "consApp"
+             (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))
+             []
+
+-- | Prove that list append is associative.
+--
+-- We have:
+-- >>> appendAssoc
+-- Axiom: List(a).induction                Admitted.
+-- Lemma: consApp                          Q.E.D.
+-- Lemma: appendAssoc                      Q.E.D.
+appendAssoc :: IO Proven
+appendAssoc = do
+
+   -- The classic proof by induction on xs
+   let p :: SymVal a => SList a -> SList a -> SList a -> SBool
+       p xs ys zs = xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs
+
+   -- Do the proof over integers. We use 'inductionPrinciple3', since our predicate has 3 arguments.
+   induct <- inductionPrinciple3 (p @Integer)
+
+   -- Get a hold on to the consApp lemma that we'll need
+   lconsApp <- consApp
+
+   lemma "appendAssoc"
+         (\(Forall @"xs" (xs :: SList Integer)) (Forall @"ys" ys) (Forall @"zs" zs) -> p xs ys zs)
+         [lconsApp , induct]
+
+-- | Prove that reversing a list twice leaves the list unchanged.
+--
+-- We have:
+--
+-- >>> reverseReverse
+-- Lemma: consApp                          Q.E.D.
+-- Axiom: List(a).induction                Admitted.
+-- Lemma: consApp                          Q.E.D.
+-- Lemma: appendAssoc                      Q.E.D.
+-- Lemma: appendNull                       Q.E.D.
+-- Chain: revApp_induction_pre
+--   Lemma: revApp_induction_pre.1         Q.E.D.
+--   Lemma: revApp_induction_pre.2         Q.E.D.
+-- Lemma: revApp_induction_pre             Q.E.D.
+-- Chain: revApp_induction_post
+--   Lemma: revApp_induction_post.1        Q.E.D.
+--   Lemma: revApp_induction_post.2        Q.E.D.
+-- Lemma: revApp_induction_post            Q.E.D.
+-- Axiom: List(a).induction                Admitted.
+-- Sorry: revApp                           Blindly believed.
+-- Axiom: List(a).induction                Admitted.
+-- Lemma: reverseReverse                   Q.E.D. [Modulo: revApp]
+reverseReverse :: IO Proven
+reverseReverse = do
+   -- We'll need the consApp and associativity-of-append proof, so get a hold on to them
+   lconsApp     <- consApp
+   lAppendAssoc <- appendAssoc
+   lAppendNull  <- appendNull
+
+   -- The usual inductive proof relies on @reverse (xs ++ ys) == reverse ys ++ reverse xs@, so first prove that:
+   revApp <- do
+        revApp_induction_pre <- chainLemma "revApp_induction_pre"
+           (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys)
+                 -> reverse ((x .: xs) ++ ys) .== (reverse (xs ++ ys)) ++ SL.singleton x)
+           (\(x :: SInteger) xs ys ->
+                [ reverse ((x .: xs) ++ ys)
+                , reverse (x .: (xs ++ ys))
+                , reverse (xs ++ ys) ++ SL.singleton x
+                ]
+           ) [lconsApp]
+
+        revApp_induction_post <- chainLemma "revApp_induction_post"
+           (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) (Forall @"ys" ys)
+                 -> (reverse ys ++ reverse xs) ++ SL.singleton x .== reverse ys ++ reverse (x .: xs))
+           (\(x :: SInteger) xs ys ->
+               [ (reverse ys ++ reverse xs) ++ SL.singleton x
+               , reverse ys ++ (reverse xs ++ SL.singleton x)
+               , reverse ys ++ reverse (x .: xs)
+               ]
+           ) [lAppendAssoc]
+
+        let q :: SymVal a => SList a -> SList a -> SBool
+            q xs ys = reverse (xs ++ ys) .== (reverse ys ++ reverse xs)
+
+        inductQ <- inductionPrinciple2 (q @Integer)
+
+        sorry "revApp" (\(Forall @"xs" (xs :: SList Integer)) (Forall @"ys" ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs)
+              [revApp_induction_pre, lAppendNull, inductQ, revApp_induction_post]
+
+   -- Result now follows from revApp and induction, and associativity of append.
+
+   let p :: SymVal a => SList a -> SBool
+       p xs = reverse (reverse xs) .== xs
+
+   induct <- inductionPrinciple (p @Integer)
+
+   lemma "reverseReverse"
+         (\(Forall @"xs" (xs :: SList Integer)) -> p xs)
+         [induct, revApp, lAppendAssoc]

Documentation/SBV/Examples/KnuckleDragger/ListLen.hs

@@ -0,0 +1,84 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.ListLen
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- Example use of the KnuckleDragger, about lenghts of lists
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeAbstractions    #-}
+{-# LANGUAGE TypeApplications    #-}
+
+{-# OPTIONS_GHC -Wall -Werror -Wno-unused-do-bind #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.ListLen where
+
+import Prelude hiding (sum, length, reverse, (++))
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+
+import qualified Data.SBV.List as SL
+
+-- $setup
+-- >>> -- For doctest purposes only:
+-- >>> :set -XScopedTypeVariables
+-- >>> import Control.Exception
+
+-- | Prove that the length of a list is one more than the length of its tail.
+--
+-- We have:
+--
+-- >>> listLengthProof
+-- Axiom: List(a).induction                Admitted.
+-- Lemma: length_correct                   Q.E.D.
+listLengthProof :: IO Proven
+listLengthProof = do
+   let length :: SList Integer -> SInteger
+       length = smtFunction "length" $ \xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs))
+
+       spec :: SList Integer -> SInteger
+       spec = SL.length
+
+       p :: SList Integer -> SBool
+       p xs = observe "imp" (length xs) .== observe "spec" (spec xs)
+
+   induct <- inductionPrinciple p
+
+   lemma "length_correct" (\(Forall @"xs" xs) -> p xs) [induct]
+
+-- | It is instructive to see what kind of counter-example we get if a lemma fails to prove.
+-- Below, we do a variant of the 'listLengthProof', but with a bad implementation, and see the
+-- counter-example. Our implementation returns an incorrect answer if the given list is longer
+-- than 5 elements and have 42 in it. We have:
+--
+-- >>> badProof `catch` (\(_ :: SomeException) -> pure ())
+-- Axiom: List(a).induction                Admitted.
+-- Lemma: bad
+-- *** Failed to prove bad.
+-- Falsifiable. Counter-example:
+--   xs   = [42,99,100,101,59,102] :: [Integer]
+--   imp  =                     42 :: Integer
+--   spec =                      6 :: Integer
+badProof :: IO ()
+badProof = do
+   let length :: SList Integer -> SInteger
+       length = smtFunction "length" $ \xs -> ite (SL.length xs .> 5 .&& 42 `SL.elem` xs) 42
+                                            $ ite (SL.null xs) 0 (1 + length (SL.tail xs))
+
+       spec :: SList Integer -> SInteger
+       spec = SL.length
+
+       p :: SList Integer -> SBool
+       p xs = observe "imp" (length xs) .== observe "spec" (spec xs)
+
+   induct <- inductionPrinciple p
+
+   lemma "bad" (\(Forall @"xs" xs) -> p xs) [induct]
+
+   pure ()

sbv.cabal

@@ -152,9 +152,10 @@ Library
                   , Documentation.SBV.Examples.Lists.Fibonacci
                   , Documentation.SBV.Examples.Lists.BoundedMutex
                   , Documentation.SBV.Examples.Lists.CountOutAndTransfer
+                  , Documentation.SBV.Examples.KnuckleDragger.AppendRev
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
-                  , Documentation.SBV.Examples.KnuckleDragger.Lists
+                  , Documentation.SBV.Examples.KnuckleDragger.ListLen
                   , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational
                   , Documentation.SBV.Examples.Misc.Definitions
                   , Documentation.SBV.Examples.Misc.Enumerate