----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.TP.StrongInduction -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Examples of strong induction. ----------------------------------------------------------------------------- {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wall -Werror #-} module Documentation.SBV.Examples.TP.StrongInduction where import Prelude hiding (length, null, head, tail, reverse, (++), splitAt, sum) import Data.SBV import Data.SBV.List import Data.SBV.TP #ifdef DOCTEST -- $setup -- >>> :set -XScopedTypeVariables -- >>> import Control.Exception #endif -- * Numeric examples -- | Prove that the sequence @1@, @3@, @S_{k-2} + 2 S_{k-1}@ is always odd. -- -- We have: -- -- >>> oddSequence1 -- Inductive lemma (strong): oddSequence1 -- 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. -- [Proven] oddSequence1 :: Ɐn ∷ Integer → Bool oddSequence1 :: IO (Proof (Forall "n" Integer -> SBool)) oddSequence1 = runTP $ do let s :: SInteger -> SInteger s = smtFunction "seq" $ \n -> ite (n .<= 0) 1 $ ite (n .== 1) 3 $ s (n-2) + 2 * s (n-1) -- z3 can't handle this, but CVC5 is proves it just fine. -- Note also that we do a "proof-by-contradiction," by deriving that -- the negation of the goal leads to falsehood. sInductWith cvc5 "oddSequence1" (\(Forall n) -> n .>= 0 .=> sNot (2 `sDivides` s n)) (abs, []) $ \ih n -> [n .>= 0] |- 2 `sDivides` s n =: cases [ n .== 0 ==> contradiction , n .== 1 ==> contradiction , n .>= 2 ==> 2 `sDivides` (s (n-2) + 2 * s (n-1)) =: 2 `sDivides` s (n-2) ?? ih `at` Inst @"n" (n - 2) =: contradiction ] -- | Prove that the sequence @1@, @3@, @2 S_{k-1} - S_{k-2}@ generates sequence of odd numbers. -- -- We have: -- -- >>> oddSequence2 -- Lemma: oddSequence_0 Q.E.D. -- Lemma: oddSequence_1 Q.E.D. -- Inductive lemma (strong): oddSequence_sNp2 -- Step: Measure is non-negative Q.E.D. -- Step: 1 Q.E.D. -- Step: 2 Q.E.D. -- Step: 3 (simplify) Q.E.D. -- Step: 4 Q.E.D. -- Step: 5 (simplify) Q.E.D. -- Step: 6 Q.E.D. -- Result: Q.E.D. -- Lemma: oddSequence2 -- 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.Completeness Q.E.D. -- Result: Q.E.D. -- [Proven] oddSequence2 :: Ɐn ∷ Integer → Bool oddSequence2 :: IO (Proof (Forall "n" Integer -> SBool)) oddSequence2 = runTPWith (tpRibbon 50 z3) $ do let s :: SInteger -> SInteger s = smtFunction "seq" $ \n -> ite (n .<= 0) 1 $ ite (n .== 1) 3 $ 2 * s (n-1) - s (n-2) s0 <- lemma "oddSequence_0" (s 0 .== 1) [] s1 <- lemma "oddSequence_1" (s 1 .== 3) [] sNp2 <- sInduct "oddSequence_sNp2" (\(Forall n) -> n .>= 2 .=> s n .== 2 * n + 1) (abs, []) $ \ih n -> [n .>= 2] |- s n =: 2 * s (n-1) - s (n-2) ?? ih `at` Inst @"n" (n-1) =: 2 * (2 * (n-1) + 1) - s (n-2) ?? "simplify" =: 4*n - 4 + 2 - s (n-2) ?? ih `at` Inst @"n" (n-2) =: 4*n - 2 - (2 * (n-2) + 1) ?? "simplify" =: 4*n - 2 - 2*n + 4 - 1 =: 2*n + 1 =: qed calc "oddSequence2" (\(Forall n) -> n .>= 0 .=> s n .== 2 * n + 1) $ \n -> [n .>= 0] |- s n =: cases [ n .== 0 ==> trivial , n .== 1 ==> trivial , n .>= 2 ==> s n ?? s0 ?? s1 ?? sNp2 `at` Inst @"n" n =: 2 * n + 1 =: qed ] -- * Strong induction checks -- | For strong induction to work, We have to instantiate the proof at a "smaller" value. This -- example demonstrates what happens if we don't. We have: -- -- >>> won'tProve1 `catch` (\(_ :: SomeException) -> pure ()) -- Inductive lemma (strong): lengthGood -- Step: Measure is non-negative Q.E.D. -- Step: 1 -- *** Failed to prove lengthGood.1. -- -- *** Solver reported: canceled won'tProve1 :: IO () won'tProve1 = runTP $ do let len :: SList Integer -> SInteger len = smtFunction "len" $ \xs -> ite (null xs) 0 (1 + len (tail xs)) -- Run it for 5 seconds, as otherwise z3 will hang as it can't prove make the inductive step _ <- sInductWith z3{extraArgs = ["-t:5000"]} "lengthGood" (\(Forall xs) -> len xs .== length xs) (length, []) $ \ih xs -> [] |- len xs -- incorrectly instantiate the IH at xs! ?? ih `at` Inst @"xs" xs =: length xs =: qed pure () -- | Note that strong induction does not need an explicit base case, as the base-cases is folded into the -- inductive step. Here's an example demonstrating what happens when the failure is only at the base case. -- -- >>> won'tProve2 `catch` (\(_ :: SomeException) -> pure ()) -- Inductive lemma (strong): badLength -- Step: Measure is non-negative Q.E.D. -- Step: 1 -- *** Failed to prove badLength.1. -- Falsifiable. Counter-example: -- xs = [] :: [Integer] won'tProve2 :: IO () won'tProve2 = runTP $ do let len :: SList Integer -> SInteger len = smtFunction "badLength" $ \xs -> ite (null xs) 123 (ite (null xs) 0 (1 + len (tail xs))) _ <- sInduct "badLength" (\(Forall xs) -> len xs .== length xs) (length, []) $ \ih xs -> [] |- len xs ?? ih `at` Inst @"xs" xs =: length xs =: qed pure () -- | The measure for strong induction should always produce a non-negative measure. The measure, in general, is an integer, or -- a tuple of integers, for tuples upto size 5. The ordering is lexicographic. This allows us to do proofs over 5-different arguments -- where their total measure goes down. If the measure can be negative, then we flag that as a failure, as demonstrated here. We have: -- -- >>> won'tProve3 `catch` (\(_ :: SomeException) -> pure ()) -- Inductive lemma (strong): badMeasure -- Step: Measure is non-negative -- *** Failed to prove badMeasure.Measure is non-negative. -- Falsifiable. Counter-example: -- x = -1 :: Integer won'tProve3 :: IO () won'tProve3 = runTP $ do _ <- sInduct "badMeasure" (\(Forall @"x" (x :: SInteger)) -> x .== x) (id, []) $ \_ih x -> [] |- x =: x =: qed pure () -- | The measure must always go down using lexicographic ordering. If not, SBV will flag this as a failure. We have: -- -- >>> won'tProve4 `catch` (\(_ :: SomeException) -> pure ()) -- Inductive lemma (strong): badMeasure -- Step: Measure is non-negative 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 -- *** Failed to prove badMeasure.1.2.2. -- -- *** Solver reported: canceled won'tProve4 :: IO () won'tProve4 = runTP $ do let -- a bizarre (but valid!) way to sum two integers weirdSum :: SInteger -> SInteger -> SInteger weirdSum = smtFunction "weirdSum" (\x y -> ite (x .<= 0) y (weirdSum (x - 1) (y + 1))) _ <- sInductWith z3{extraArgs = ["-t:5000"]} "badMeasure" (\(Forall x) (Forall y) -> x .>= 0 .=> weirdSum x y .== x + y) -- This measure is not good, since it remains the same. Note that we do not get a -- failure, but the proof will never converge either; so we put a time bound (\x y -> abs x + abs y, []) $ \ih x y -> [x .>= 0] |- ite (x .<= 0) y (weirdSum (x - 1) (y + 1)) =: cases [ x .<= 0 ==> trivial , x .> 0 ==> weirdSum (x - 1) (y + 1) ?? ih `at` (Inst @"x" (x - 1), Inst @"y" (y + 1)) =: x - 1 + y + 1 =: x + y =: qed ] pure () -- * Summing via halving -- | We prove that summing a list can be done by halving the list, summing parts, and adding the results. The proof uses -- strong induction. We have: -- -- >>> sumHalves -- Inductive lemma: sumAppend -- Step: Base Q.E.D. -- Step: 1 Q.E.D. -- Step: 2 Q.E.D. -- Step: 3 Q.E.D. -- Result: Q.E.D. -- Inductive lemma (strong): sumHalves -- 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) Q.E.D. -- Result: Q.E.D. -- [Proven] sumHalves :: Ɐxs ∷ [Integer] → Bool sumHalves :: IO (Proof (Forall "xs" [Integer] -> SBool)) sumHalves = runTP $ do let halvingSum :: SList Integer -> SInteger halvingSum = smtFunction "halvingSum" $ \xs -> ite (null xs .|| null (tail xs)) (sum xs) (let (f, s) = splitAt (length xs `sDiv` 2) xs in halvingSum f + halvingSum s) helper <- induct "sumAppend" (\(Forall xs) (Forall ys) -> sum (xs ++ ys) .== sum xs + sum ys) $ \ih (x, xs) ys -> [] |- sum (x .: xs ++ ys) =: x + sum (xs ++ ys) ?? ih =: x + sum xs + sum ys =: sum (x .: xs) + sum ys =: qed -- Use strong induction to prove the theorem. CVC5 solves this with ease, but z3 struggles. sInductWith cvc5 "sumHalves" (\(Forall xs) -> halvingSum xs .== sum xs) (length, []) $ \ih xs -> [] |- halvingSum xs =: split xs qed (\a as -> split as qed (\b bs -> halvingSum (a .: b .: bs) =: let (f, s) = splitAt (length (a .: b .: bs) `sDiv` 2) (a .: b .: bs) in halvingSum f + halvingSum s ?? ih `at` Inst @"xs" f =: sum f + halvingSum s ?? ih `at` Inst @"xs" s =: sum f + sum s ?? helper `at` (Inst @"xs" f, Inst @"ys" s) =: sum (f ++ s) ?? "simplify" =: sum (a .: b .: bs) =: qed))