-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.StrongInduction
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Examples of strong induction on integers.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP              #-}
{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.StrongInduction where

import Prelude hiding (length, null, tail)

import Data.SBV
import Data.SBV.List
import Data.SBV.Tools.KnuckleDragger

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> :set -XScopedTypeVariables
-- >>> import Control.Exception
#endif

-- | Prove that the sequence @1@, @3@, @S_{k-2} + 2 S_{k-1}@ is always odd.
--
-- We have:
--
-- >>> oddSequence1
-- Inductive lemma (strong): oddSequence
--   Base: oddSequence.Base                Q.E.D.
--   Asms: 1                               Q.E.D.
--   Step 1: Case split one way:
--     Case [1 of 1]: n[1]                 Q.E.D.
--     Completeness:                       Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: oddSequence.Step                Q.E.D.
-- [Proven] oddSequence
oddSequence1 :: IO Proof
oddSequence1 :: IO Proof
oddSequence1 = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
  let s :: SInteger -> SInteger
      s :: SInteger -> SInteger
s = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"seq" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
1
                                  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1) SInteger
3
                                  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
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.
  SMTConfig
-> String
-> (Forall "n" Integer -> SBool)
-> (Proof -> SInteger -> (SBool, [ProofStep SBool]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
sInductWith SMTConfig
cvc5 String
"oddSequence"
          (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
s SInteger
n)) ((Proof -> SInteger -> (SBool, [ProofStep SBool])) -> KD Proof)
-> (Proof -> SInteger -> (SBool, [ProofStep SBool])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [String -> [SBool] -> Helper
cases String
"n" [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
2],  SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
2 Integer -> SInteger -> SBool
`sDivides` (SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
s SInteger
n)
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                             SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sFalse
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

-- | Prove that the sequence @1@, @3@, @2 S_{k-1} - S_{k-2}@ generates sequence of odd numbers.
--
-- We have:
--
-- >>> oddSequence2
-- Inductive lemma (strong): oddSequence
--   Base: oddSequence.Base                Q.E.D.
--   Asms: 1                               Q.E.D.
--   Step 1: Case split one way:
--     Case [1 of 1]: n[1]                 Q.E.D.
--     Completeness:                       Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: 3                               Q.E.D.
--   Step: 4                               Q.E.D.
--   Step: 5                               Q.E.D.
--   Step: 6                               Q.E.D.
--   Step: 7                               Q.E.D.
--   Step: oddSequence.Step                Q.E.D.
-- [Proven] oddSequence
oddSequence2 :: IO Proof
oddSequence2 :: IO Proof
oddSequence2 = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
  let s :: SInteger -> SInteger
      s :: SInteger -> SInteger
s = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"seq" ((SInteger -> SInteger) -> SInteger -> SInteger)
-> (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
n -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
1
                                  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1) SInteger
3
                                  (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
2)

  String
-> (Forall "n" Integer -> SBool)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
sInduct String
"oddSequence"
          (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger
s SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) ((Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof)
-> (Proof -> SInteger -> (SBool, [ProofStep SInteger])) -> KD Proof
forall a b. (a -> b) -> a -> b
$
          \Proof
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                             SInteger -> [Helper] -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [String -> [SBool] -> Helper
cases String
"n" [SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
2],  SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)]
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let focus :: a -> a
focus a
v = SBool -> a -> a -> a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) a
1 (SBool -> a -> a -> a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1) a
3 a
v)
                             in SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
s SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger -> SInteger
s (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1))
                             SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger -> SInteger
s (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))
                             SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> Inst "n" Integer -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SInteger
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                             ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1))
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1))
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
4 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
forall {a}. (Mergeable a, Num a) => a -> a
focus (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

-- | 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'tProve `catch` (\(_ :: SomeException) -> pure ())
-- Inductive lemma (strong): lengthGood
--   Base: lengthGood.Base                 Q.E.D.
--   Step: 1
-- *** Failed to prove lengthGood.1.
-- <BLANKLINE>
-- *** Solver reported: canceled
won'tProve :: IO ()
won'tProve :: IO ()
won'tProve = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
   let len :: SList Integer -> SInteger
       len :: SList Integer -> SInteger
len = String -> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"len" ((SList Integer -> SInteger) -> SList Integer -> SInteger)
-> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ \SList Integer
xs -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs) SInteger
0 (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
len (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
tail SList Integer
xs))

   -- Run it for 5 seconds, as otherwise z3 will hang as it can't prove make the inductive step
   _ <- SMTConfig
-> String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof
    -> SInteger -> SList Integer -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
sInductWith SMTConfig
z3{extraArgs = ["-t:5000"]} String
"lengthGood"
                (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SInteger
len SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs) ((Proof
  -> SInteger -> SList Integer -> (SBool, [ProofStep SInteger]))
 -> KD Proof)
-> (Proof
    -> SInteger -> SList Integer -> (SBool, [ProofStep SInteger]))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                \Proof
ih SInteger
x SList Integer
xs -> [] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList Integer -> SInteger
len (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                               -- incorrectly instantiate the IH at x .: xs
                               SInteger -> Proof -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                               ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                               SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed
   pure ()