-----------------------------------------------------------------------------
-- |
-- 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 :: IO (Proof (Forall "n" Integer -> SBool))
oddSequence1 = TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "n" Integer -> SBool))
 -> IO (Proof (Forall "n" Integer -> SBool)))
-> TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
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, Typeable 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)
-> MeasureArgs (Forall "n" Integer -> SBool) Integer
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "n" Integer -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "n" Integer -> SBool)
-> MeasureArgs (Forall "n" Integer -> SBool) m
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
sInductWith SMTConfig
cvc5 String
"oddSequence1"
          (\(Forall 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))
          MeasureArgs (Forall "n" Integer -> SBool) Integer
SInteger -> SInteger
forall a. Num a => a -> a
abs ((Proof (Forall "n" Integer -> SBool)
  -> StepArgs (Forall "n" Integer -> SBool) Bool)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) Bool)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof (Forall "n" Integer -> SBool)
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- Integer
2 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
s SInteger
n
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Contradiction a => a
contradiction
                                      , SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Contradiction a => a
contradiction
                                      , SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw 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 Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ih Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`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)
                                                 TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (TPProofRaw SBool)
TPProofRaw SBool
forall a. Contradiction a => a
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 :: IO (Proof (Forall "n" Integer -> SBool))
oddSequence2 = SMTConfig
-> TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
forall a. SMTConfig -> TP a -> IO a
runTPWith (Int -> SMTConfig -> SMTConfig
tpRibbon Int
50 SMTConfig
z3) (TP (Proof (Forall "n" Integer -> SBool))
 -> IO (Proof (Forall "n" Integer -> SBool)))
-> TP (Proof (Forall "n" Integer -> SBool))
-> IO (Proof (Forall "n" Integer -> SBool))
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, Typeable 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)

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

  Proof (Forall "n" Integer -> SBool)
sNp2 <- String
-> (Forall "n" Integer -> SBool)
-> MeasureArgs (Forall "n" Integer -> SBool) Integer
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "n" Integer -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> MeasureArgs (Forall "n" Integer -> SBool) m
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) t)
-> TP (Proof (Forall "n" Integer -> SBool))
sInduct String
"oddSequence_sNp2"
                  (\(Forall 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)
                  MeasureArgs (Forall "n" Integer -> SBool) Integer
SInteger -> SInteger
forall a. Num a => a -> a
abs ((Proof (Forall "n" Integer -> SBool)
  -> StepArgs (Forall "n" Integer -> SBool) Integer)
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> (Proof (Forall "n" Integer -> SBool)
    -> StepArgs (Forall "n" Integer -> SBool) Integer)
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \Proof (Forall "n" Integer -> SBool)
ih SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
s SInteger
n
                                     SInteger -> ChainsTo SInteger -> ChainsTo 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 -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ih Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`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)
                                     TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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"
                                     TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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 -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
ih Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`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)
                                     TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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"
                                     TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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
TPProofRaw SInteger
forall a. TPProofRaw a
qed

  String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall t.
(Proposition (Forall "n" Integer -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "n" Integer -> SBool)
-> StepArgs (Forall "n" Integer -> SBool) t
-> TP (Proof (Forall "n" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"oddSequence2" (\(Forall 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) (StepArgs (Forall "n" Integer -> SBool) Integer
 -> TP (Proof (Forall "n" Integer -> SBool)))
-> StepArgs (Forall "n" Integer -> SBool) Integer
-> TP (Proof (Forall "n" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                      \SInteger
n -> [SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
s SInteger
n
                                      SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                               , SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                               , SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
2 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger
s SInteger
n
                                                          SInteger -> Proof SBool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
s0
                                                          TPProofRaw SInteger -> Proof SBool -> Hinted (TPProofRaw SInteger)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
s1
                                                          Hinted (TPProofRaw SInteger)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SInteger))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
sNp2 Proof (Forall "n" Integer -> SBool)
-> IArgs (Forall "n" Integer -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" SInteger
n
                                                          Hinted (Hinted (TPProofRaw SInteger))
-> ChainsTo (Hinted (Hinted (TPProofRaw SInteger)))
-> ChainsTo (Hinted (Hinted (TPProofRaw 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
TPProofRaw SInteger
forall a. TPProofRaw a
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.
-- <BLANKLINE>
-- *** Solver reported: canceled
won'tProve1 :: IO ()
won'tProve1 :: IO ()
won'tProve1 = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> 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, Typeable 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
   Proof (Forall "xs" [Integer] -> SBool)
_ <- SMTConfig
-> String
-> (Forall "xs" [Integer] -> SBool)
-> MeasureArgs (Forall "xs" [Integer] -> SBool) Integer
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "xs" [Integer] -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [Integer] -> SBool)
-> MeasureArgs (Forall "xs" [Integer] -> SBool) m
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) t)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
sInductWith SMTConfig
z3{extraArgs = ["-t:5000"]} String
"lengthGood"
                (\(Forall 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)
                MeasureArgs (Forall "xs" [Integer] -> SBool) Integer
SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length ((Proof (Forall "xs" [Integer] -> SBool)
  -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
 -> TP (Proof (Forall "xs" [Integer] -> SBool)))
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$
                \Proof (Forall "xs" [Integer] -> SBool)
ih SList Integer
xs -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
len SList Integer
xs
                             -- incorrectly instantiate the IH at xs!
                             SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [Integer] -> SBool)
ih Proof (Forall "xs" [Integer] -> SBool)
-> IArgs (Forall "xs" [Integer] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs
                             TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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
TPProofRaw SInteger
forall a. TPProofRaw a
qed
   () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
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 :: IO ()
won'tProve2 = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> 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, Typeable 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)))

   Proof (Forall "xs" [Integer] -> SBool)
_ <- String
-> (Forall "xs" [Integer] -> SBool)
-> MeasureArgs (Forall "xs" [Integer] -> SBool) Integer
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "xs" [Integer] -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [Integer] -> SBool)
-> MeasureArgs (Forall "xs" [Integer] -> SBool) m
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) t)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
sInduct String
"badLength"
                (\(Forall 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)
                MeasureArgs (Forall "xs" [Integer] -> SBool) Integer
SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length ((Proof (Forall "xs" [Integer] -> SBool)
  -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
 -> TP (Proof (Forall "xs" [Integer] -> SBool)))
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$
                \Proof (Forall "xs" [Integer] -> SBool)
ih SList Integer
xs -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
len SList Integer
xs
                             SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [Integer] -> SBool)
ih Proof (Forall "xs" [Integer] -> SBool)
-> IArgs (Forall "xs" [Integer] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs
                             TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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
TPProofRaw SInteger
forall a. TPProofRaw a
qed
   () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
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 :: IO ()
won'tProve3 = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
   Proof (Forall "x" Integer -> SBool)
_ <- String
-> (Forall "x" Integer -> SBool)
-> MeasureArgs (Forall "x" Integer -> SBool) Integer
-> (Proof (Forall "x" Integer -> SBool)
    -> StepArgs (Forall "x" Integer -> SBool) Integer)
-> TP (Proof (Forall "x" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "x" Integer -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "x" Integer -> SBool)
-> MeasureArgs (Forall "x" Integer -> SBool) m
-> (Proof (Forall "x" Integer -> SBool)
    -> StepArgs (Forall "x" Integer -> SBool) t)
-> TP (Proof (Forall "x" Integer -> SBool))
sInduct String
"badMeasure"
                (\(Forall @"x" (SInteger
x :: SInteger)) -> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                MeasureArgs (Forall "x" Integer -> SBool) Integer
SInteger -> SInteger
forall a. a -> a
id ((Proof (Forall "x" Integer -> SBool)
  -> StepArgs (Forall "x" Integer -> SBool) Integer)
 -> TP (Proof (Forall "x" Integer -> SBool)))
-> (Proof (Forall "x" Integer -> SBool)
    -> StepArgs (Forall "x" Integer -> SBool) Integer)
-> TP (Proof (Forall "x" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                \Proof (Forall "x" Integer -> SBool)
_ih SInteger
x -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x
                             SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed


   () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
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.
-- <BLANKLINE>
-- *** Solver reported: canceled
won'tProve4 :: IO ()
won'tProve4 :: IO ()
won'tProve4 = TP () -> IO ()
forall a. TP a -> IO a
runTP (TP () -> IO ()) -> TP () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

   let -- a bizarre (but valid!) way to sum two integers
       weirdSum :: SInteger -> SInteger -> SInteger
       weirdSum :: SInteger -> SInteger -> SInteger
weirdSum = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"weirdSum" (\SInteger
x SInteger
y -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
y (SInteger -> SInteger -> SInteger
weirdSum (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)))

   Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
_ <- SMTConfig
-> String
-> (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> MeasureArgs
     (Forall "x" Integer -> Forall "y" Integer -> SBool) Integer
-> (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
    -> StepArgs
         (Forall "x" Integer -> Forall "y" Integer -> SBool) Integer)
-> TP (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "x" Integer -> Forall "y" Integer -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> MeasureArgs
     (Forall "x" Integer -> Forall "y" Integer -> SBool) m
-> (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
    -> StepArgs (Forall "x" Integer -> Forall "y" Integer -> SBool) t)
-> TP (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool))
sInductWith SMTConfig
z3{extraArgs = ["-t:5000"]} String
"badMeasure"
                (\(Forall SInteger
x) (Forall SInteger
y) -> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
weirdSum SInteger
x SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
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
                (\SInteger
x SInteger
y -> SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SInteger
forall a. Num a => a -> a
abs SInteger
y) ((Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
  -> StepArgs
       (Forall "x" Integer -> Forall "y" Integer -> SBool) Integer)
 -> TP (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)))
-> (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
    -> StepArgs
         (Forall "x" Integer -> Forall "y" Integer -> SBool) Integer)
-> TP (Proof (Forall "x" Integer -> Forall "y" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
                \Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
ih SInteger
x SInteger
y -> [SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SInteger
y (SInteger -> SInteger -> SInteger
weirdSum (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
y 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
=: [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                              , SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
0 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger -> SInteger
weirdSum (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) (SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                                                         SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
ih Proof (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> IArgs (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" (SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"y" (SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1))
                                                         TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
y 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
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
y
                                                         SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed
                                              ]

   () -> TP ()
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
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 :: IO (Proof (Forall "xs" [Integer] -> SBool))
sumHalves = TP (Proof (Forall "xs" [Integer] -> SBool))
-> IO (Proof (Forall "xs" [Integer] -> SBool))
forall a. TP a -> IO a
runTP (TP (Proof (Forall "xs" [Integer] -> SBool))
 -> IO (Proof (Forall "xs" [Integer] -> SBool)))
-> TP (Proof (Forall "xs" [Integer] -> SBool))
-> IO (Proof (Forall "xs" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$ do

    let halvingSum :: SList Integer -> SInteger
        halvingSum :: SList Integer -> SInteger
halvingSum = String -> (SList Integer -> SInteger) -> SList Integer -> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"halvingSum" ((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 SBool -> SBool -> SBool
.|| SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
tail SList Integer
xs))
                                                           (SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
xs)
                                                           (let (SList Integer
f, SList Integer
s) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
2) SList Integer
xs
                                                            in SList Integer -> SInteger
halvingSum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
halvingSum SList Integer
s)

    Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
helper <- String
-> (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
-> (Proof
      (IHType (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
    -> IStepArgs
         (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool) Integer)
-> TP
     (Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
forall t.
(Proposition
   (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
-> (Proof
      (IHType (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
    -> IStepArgs
         (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool) t)
-> TP
     (Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sumAppend"
                     (\(Forall SList Integer
xs) (Forall SList Integer
ys) -> SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
ys) ((Proof
    (IHType (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
  -> IHArg (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
  -> IStepArgs
       (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool) Integer)
 -> TP
      (Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)))
-> (Proof
      (IHType (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
    -> IStepArgs
         (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool) Integer)
-> TP
     (Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$
                     \Proof
  (IHType (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
ih (SInteger
x, SList Integer
xs) SList Integer
ys -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                                          SInteger
-> Proof (Forall "ys" [Integer] -> SBool) -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool))
Proof (Forall "ys" [Integer] -> SBool)
ih
                                          TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
ys
                                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
ys
                                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed

    -- Use strong induction to prove the theorem. CVC5 solves this with ease, but z3 struggles.
    SMTConfig
-> String
-> (Forall "xs" [Integer] -> SBool)
-> MeasureArgs (Forall "xs" [Integer] -> SBool) Integer
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "xs" [Integer] -> SBool), Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [Integer] -> SBool)
-> MeasureArgs (Forall "xs" [Integer] -> SBool) m
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) t)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
sInductWith SMTConfig
cvc5 String
"sumHalves"
      (\(Forall SList Integer
xs) -> SList Integer -> SInteger
halvingSum SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
xs)
      MeasureArgs (Forall "xs" [Integer] -> SBool) Integer
SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length ((Proof (Forall "xs" [Integer] -> SBool)
  -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
 -> TP (Proof (Forall "xs" [Integer] -> SBool)))
-> (Proof (Forall "xs" [Integer] -> SBool)
    -> StepArgs (Forall "xs" [Integer] -> SBool) Integer)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$
      \Proof (Forall "xs" [Integer] -> SBool)
ih SList Integer
xs -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SInteger
halvingSum SList Integer
xs
                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> TPProofRaw SInteger
-> (SInteger -> SList Integer -> TPProofRaw SInteger)
-> TPProofRaw SInteger
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SList Integer
xs TPProofRaw SInteger
forall a. TPProofRaw a
qed
                            (\SInteger
a SList Integer
as -> SList Integer
-> TPProofRaw SInteger
-> (SInteger -> SList Integer -> TPProofRaw SInteger)
-> TPProofRaw SInteger
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SList Integer
as TPProofRaw SInteger
forall a. TPProofRaw a
qed
                                            (\SInteger
b SList Integer
bs -> SList Integer -> SInteger
halvingSum (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs)
                                                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
f, SList Integer
s) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs) SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
`sDiv` SInteger
2) (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs)
                                                   in SList Integer -> SInteger
halvingSum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
halvingSum SList Integer
s
                                                   SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [Integer] -> SBool)
ih Proof (Forall "xs" [Integer] -> SBool)
-> IArgs (Forall "xs" [Integer] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
f
                                                   TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
halvingSum SList Integer
s
                                                   SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [Integer] -> SBool)
ih Proof (Forall "xs" [Integer] -> SBool)
-> IArgs (Forall "xs" [Integer] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
s
                                                   TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
f SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
s
                                                   SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
helper Proof (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
-> IArgs (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
f, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
s)
                                                   TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SList Integer
f SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
s)
                                                   SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                                   TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SInteger
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs)
                                                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
TPProofRaw SInteger
forall a. TPProofRaw a
qed))