-----------------------------------------------------------------------------
-- |
-- 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
--   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] 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, KDProofRaw SBool))
-> KD Proof
forall a steps.
(SInductive 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, KDProofRaw SBool)) -> KD Proof)
-> (Proof -> SInteger -> (SBool, KDProofRaw 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] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
s SInteger
n
                             SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SBool
sFalse SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                      , SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SBool
sFalse SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                      , SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==>    Integer
2 Integer -> SInteger -> SBool
`sDivides` (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))
                                                    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
2)
                                                    SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted 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
2)
                                                    KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw 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
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                      ]

-- | 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: 1                               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.
--   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
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)

  s0 <- String -> SBool -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"oddSequence_0" (SInteger -> SInteger
s SInteger
0 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1) []
  s1 <- lemma "oddSequence_1" (s 1 .== 3) []

  sNp2 <- sInduct "oddSequence_sNp2"
                  (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 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
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SInteger
s SInteger
n
                                     SInteger -> SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2
                                     KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo 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) 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)
                                     SInteger -> [Helper] -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2)
                                        , Proof -> Helper
hprf (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))
                                        ]
                                     KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo 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
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) 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
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
2)
                                     SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                     KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
4SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
4 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
2)
                                     SInteger -> [Helper] -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? [SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2), Proof -> Helper
hprf (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
2))]
                                     KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
4SInteger -> 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
nSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
2) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                                     SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                     KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
4SInteger -> 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
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4 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
2SInteger -> 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
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed

  calc "oddSequence2" (\(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) $
                      \SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SInteger
s SInteger
n
                                      SInteger -> SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                      KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SInteger)] -> KDProofRaw SInteger
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> (SInteger
1 :: SInteger) SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed
                                               , SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> (SInteger
3 :: SInteger) SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed
                                               , SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==>    SInteger -> SInteger
s SInteger
n
                                                             SInteger -> [Helper] -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ SBool -> Helper
hyp (SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0)
                                                                , Proof -> Helper
hprf Proof
s0
                                                                , Proof -> Helper
hprf Proof
s1
                                                                , Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
sNp2 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
                                                                ]
                                                             KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo 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
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw 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'tProve1 `catch` (\(_ :: SomeException) -> pure ())
-- Inductive lemma (strong): lengthGood
--   Step: 1
-- *** Failed to prove lengthGood.1.
-- <BLANKLINE>
-- *** Solver reported: canceled
won'tProve1 :: IO ()
won'tProve1 :: IO ()
won'tProve1 = 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 -> SList Integer -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a steps.
(SInductive 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 -> SList Integer -> (SBool, KDProofRaw SInteger))
 -> KD Proof)
-> (Proof -> SList Integer -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                \Proof
ih SList Integer
xs -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SInteger
len SList Integer
xs
                             -- incorrectly instantiate the IH at xs!
                             SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted 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" SList Integer
xs
                             KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
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: 1
-- *** Failed to prove badLength.1.
-- Falsifiable. Counter-example:
--   xs = [] :: [Integer]
won'tProve2 :: IO ()
won'tProve2 :: IO ()
won'tProve2 = 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
"badLength" ((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
123
                                                  (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)))

   _ <- String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof -> SList Integer -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a steps.
(SInductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
sInduct String
"badLength"
                (\(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 -> SList Integer -> (SBool, KDProofRaw SInteger))
 -> KD Proof)
-> (Proof -> SList Integer -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                \Proof
ih SList Integer
xs -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SInteger
len SList Integer
xs
                             SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted 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" SList Integer
xs
                             KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed
   pure ()