-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.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.KnuckleDragger.StrongInduction where

import Prelude hiding (length, null, head, tail, reverse, (++))

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

#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): oddSequence
--   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] 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)
-> (SInteger -> SInteger)
-> (Proof -> SInteger -> (SBool, KDProofRaw SBool))
-> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
SMTConfig -> String -> a -> measure -> (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)) (forall a. Num a => a -> a
abs @SInteger) ((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 -> ChainsTo SBool -> ChainsTo 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)
==> KDProofRaw SBool
forall a. Contradiction a => a
contradiction
                                      , 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)
==> KDProofRaw SBool
forall a. Contradiction a => a
contradiction
                                      , 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
=: ChainsTo (KDProofRaw SBool)
KDProofRaw 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
oddSequence2 :: IO Proof
oddSequence2 :: IO Proof
oddSequence2 = SMTConfig -> KD Proof -> IO Proof
forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
z3{kdOptions = (kdOptions z3) {ribbonLength = 50}} (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) (abs @SInteger) $
                  \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 -> 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 -> Hinted SInteger
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
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 -> Proof -> Hinted SInteger
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
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 -> ChainsTo SInteger -> ChainsTo 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 -> [Proof] -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
s0
                                                                , Proof
s1
                                                                , 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
                                               ]

-- * List examples

-- | Interleave the elements of two lists. If one ends, we take the rest from the other.
interleave :: SymVal a => SList a -> SList a -> SList a
interleave :: forall a. SymVal a => SList a -> SList a -> SList a
interleave = String
-> (SList a -> SList a -> SList a) -> SList a -> SList a -> SList a
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"interleave" (\SList a
xs SList a
ys -> SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null  SList a
xs) SList a
ys (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
xs SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList a
ys (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
xs)))

-- | Prove that interleave preserves total length.
--
-- The induction here is on the total length of the lists, and hence
-- we use the generalized induction principle. We have:
--
-- >>> interleaveLen
-- Inductive lemma (strong): interleaveLen
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2                         Q.E.D.
--     Step: 1.2.3                         Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] interleaveLen
interleaveLen :: IO Proof
interleaveLen :: IO Proof
interleaveLen = 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

   String
-> (Forall "xs" [Integer] -> Forall "ys" [Integer] -> SBool)
-> (SList Integer -> SList Integer -> SInteger)
-> (Proof
    -> SList Integer -> SList Integer -> (SBool, KDProofRaw SBool))
-> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
String -> a -> measure -> (Proof -> steps) -> KD Proof
sInduct String
"interleaveLen"
           (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
ys SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (forall a. SymVal a => SList a -> SList a -> SList a
interleave @Integer SList Integer
xs SList Integer
ys))
           (\SList Integer
xs SList Integer
ys -> forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
ys) ((Proof
  -> SList Integer -> SList Integer -> (SBool, KDProofRaw SBool))
 -> KD Proof)
-> (Proof
    -> SList Integer -> SList Integer -> (SBool, KDProofRaw SBool))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
           \Proof
ih SList Integer
xs SList Integer
ys ->
              [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
ys SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (forall a. SymVal a => SList a -> SList a -> SList a
interleave @Integer SList Integer
xs SList Integer
ys)
                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> KDProofRaw SBool
-> (SInteger -> SList Integer -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
xs
                          KDProofRaw SBool
forall a. Trivial a => a
trivial
                          (\SInteger
a SList Integer
as -> 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
.: SList Integer
as) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
ys SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) SList Integer
ys)
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
as SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
ys SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList Integer
ys SList Integer
as)
                                 SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
as)
                                 KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                 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)

-- | Uninterleave the elements of two lists. We roughly split it into two, of alternating elements.
uninterleave :: SymVal a => SList a -> STuple [a] [a]
uninterleave :: forall a. SymVal a => SList a -> STuple [a] [a]
uninterleave SList a
lst = SList a -> STuple [a] [a] -> STuple [a] [a]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen SList a
lst ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a
forall a. SymVal a => SList a
nil, SList a
forall a. SymVal a => SList a
nil))

-- | Generalized form of uninterleave with the auxilary lists made explicit.C
uninterleaveGen :: SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen :: forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen = String
-> (SList a -> STuple [a] [a] -> STuple [a] [a])
-> SList a
-> STuple [a] [a]
-> STuple [a] [a]
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"uninterleave" (\SList a
xs STuple [a] [a]
alts -> let (SList a
es, SList a
os) = STuple [a] [a] -> (SList a, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple STuple [a] [a]
alts
                                                          in SBool -> STuple [a] [a] -> STuple [a] [a] -> STuple [a] [a]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                                 ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse SList a
es, SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse SList a
os))
                                                                 (SList a -> STuple [a] [a] -> STuple [a] [a]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
xs) ((SList a, SList a) -> STuple [a] [a]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a
os, SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
xs SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es))))

-- | The functions 'uninterleave' and 'interleave' are inverses so long as the inputs are of the same length. (The equality
-- would even hold if the first argument has one extra element, but we keep things simple here.)
--
-- We have:
--
-- >>> interleaveRoundTrip
-- Lemma: revCons                          Q.E.D.
-- Inductive lemma (strong): roundTripGen
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (4 way full case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.3                           Q.E.D.
--     Step: 1.4.1                         Q.E.D.
--     Step: 1.4.2                         Q.E.D.
--     Step: 1.4.3                         Q.E.D.
--     Step: 1.4.4                         Q.E.D.
--     Step: 1.4.5                         Q.E.D.
--     Step: 1.4.6                         Q.E.D.
--     Step: 1.4.7                         Q.E.D.
--     Step: 1.4.8                         Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: interleaveRoundTrip
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] interleaveRoundTrip
interleaveRoundTrip :: IO Proof
interleaveRoundTrip :: IO Proof
interleaveRoundTrip = SMTConfig -> KD Proof -> IO Proof
forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
cvc5 (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

   revHelper <- String
-> (Forall "a" Integer
    -> Forall "as" [Integer] -> Forall "bs" [Integer] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"revCons" (\(Forall @"a" SInteger
a) (Forall @"as" SList Integer
as) (Forall @"bs" SList Integer
bs)
                                        -> forall a. SymVal a => SList a -> SList a
reverse @Integer (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
bs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
as SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs)) []

   -- Generalize the theorem first to take the helper lists explicitly
   roundTripGen <- sInduct
         "roundTripGen"
         (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) (Forall @"alts" STuple [Integer] [Integer]
alts) ->
               forall a. SymVal a => SList a -> SInteger
length @Integer 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
ys
                  SBool -> SBool -> SBool
.=> let (SList Integer
es, SList Integer
os) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple STuple [Integer] [Integer]
alts
                      in SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList Integer
xs SList Integer
ys) STuple [Integer] [Integer]
alts STuple [Integer] [Integer] -> STuple [Integer] [Integer] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
es SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
xs, SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
os SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys))
         (\SList Integer
xs SList Integer
ys (STuple [Integer] [Integer]
_alts :: STuple [Integer] [Integer]) -> forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
ys) $
         \Proof
ih SList Integer
xs SList Integer
ys STuple [Integer] [Integer]
alts -> [forall a. SymVal a => SList a -> SInteger
length @Integer 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
ys]
                        [SBool]
-> KDProofRaw (STuple [Integer] [Integer])
-> (SBool, KDProofRaw (STuple [Integer] [Integer]))
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- let (SList Integer
es, SList Integer
os) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple STuple [Integer] [Integer]
alts
                        in SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList Integer
xs SList Integer
ys) STuple [Integer] [Integer]
alts
                        STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList Integer, SList Integer)
-> KDProofRaw (STuple [Integer] [Integer])
-> ((SInteger, SList Integer)
    -> KDProofRaw (STuple [Integer] [Integer]))
-> ((SInteger, SList Integer)
    -> KDProofRaw (STuple [Integer] [Integer]))
-> ((SInteger, SList Integer)
    -> (SInteger, SList Integer)
    -> KDProofRaw (STuple [Integer] [Integer]))
-> KDProofRaw (STuple [Integer] [Integer])
forall a b r.
(SymVal a, SymVal b) =>
(SList a, SList b)
-> KDProofRaw r
-> ((SBV b, SList b) -> KDProofRaw r)
-> ((SBV a, SList a) -> KDProofRaw r)
-> ((SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r)
-> KDProofRaw r
split2 (SList Integer
xs, SList Integer
ys)
                                  KDProofRaw (STuple [Integer] [Integer])
forall a. Trivial a => a
trivial
                                  (SInteger, SList Integer)
-> KDProofRaw (STuple [Integer] [Integer])
forall a. Trivial a => a
trivial
                                  (SInteger, SList Integer)
-> KDProofRaw (STuple [Integer] [Integer])
forall a. Trivial a => a
trivial
                                  (\(SInteger
a, SList Integer
as) (SInteger
b, SList Integer
bs) -> SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs)) STuple [Integer] [Integer]
alts
                                                    STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs) SList Integer
as) STuple [Integer] [Integer]
alts
                                                    STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (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 -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList Integer
as SList Integer
bs) STuple [Integer] [Integer]
alts
                                                    STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList Integer
as SList Integer
bs) ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es, SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
os))
                                                    STuple [Integer] [Integer]
-> Proof -> Hinted (STuple [Integer] [Integer])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer],
    Inst "alts" ([Integer], [Integer]))
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
bs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"alts" ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es, SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
os)))
                                                    KDProofRaw (STuple [Integer] [Integer])
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es) SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
as, SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
os) SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
bs)
                                                    STuple [Integer] [Integer]
-> Proof -> Hinted (STuple [Integer] [Integer])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
revHelper Proof
-> (Inst "a" Integer, Inst "as" [Integer], Inst "bs" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"as" SList Integer
es, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Integer
as)
                                                    KDProofRaw (STuple [Integer] [Integer])
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
es SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as), SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
os) SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
bs)
                                                    STuple [Integer] [Integer]
-> Proof -> Hinted (STuple [Integer] [Integer])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
revHelper Proof
-> (Inst "a" Integer, Inst "as" [Integer], Inst "bs" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"a" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"as" SList Integer
os, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"bs" SList Integer
bs)
                                                    KDProofRaw (STuple [Integer] [Integer])
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
es SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as), SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
os SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList 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))
                                                    STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
es SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
xs, SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
os SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                                                    STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (STuple [Integer] [Integer])
KDProofRaw (STuple [Integer] [Integer])
forall a. KDProofRaw a
qed)

   -- Round-trip theorem:
   calc "interleaveRoundTrip"
           (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length 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
ys SBool -> SBool -> SBool
.=> SList Integer -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a]
uninterleave (forall a. SymVal a => SList a -> SList a -> SList a
interleave @Integer SList Integer
xs SList Integer
ys) STuple [Integer] [Integer] -> STuple [Integer] [Integer] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer
xs, SList Integer
ys)) $
           \SList Integer
xs SList Integer
ys -> [SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length 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
ys]
                  [SBool]
-> KDProofRaw (STuple [Integer] [Integer])
-> (SBool, KDProofRaw (STuple [Integer] [Integer]))
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a]
uninterleave (forall a. SymVal a => SList a -> SList a -> SList a
interleave @Integer SList Integer
xs SList Integer
ys)
                  STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> STuple [Integer] [Integer] -> STuple [Integer] [Integer]
forall a. SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
uninterleaveGen (SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
interleave SList Integer
xs SList Integer
ys) ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer
forall a. SymVal a => SList a
nil, SList Integer
forall a. SymVal a => SList a
nil))
                  STuple [Integer] [Integer]
-> Proof -> Hinted (STuple [Integer] [Integer])
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
roundTripGen Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer],
    Inst "alts" ([Integer], [Integer]))
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"alts" ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer
forall a. SymVal a => SList a
nil :: SList Integer, SList Integer
forall a. SymVal a => SList a
nil :: SList Integer)))
                  KDProofRaw (STuple [Integer] [Integer])
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
-> ChainsTo (KDProofRaw (STuple [Integer] [Integer]))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
forall a. SymVal a => SList a
nil SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
xs, SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
reverse SList Integer
forall a. SymVal a => SList a
nil SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                  STuple [Integer] [Integer]
-> ChainsTo (STuple [Integer] [Integer])
-> ChainsTo (STuple [Integer] [Integer])
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (STuple [Integer] [Integer])
KDProofRaw (STuple [Integer] [Integer])
forall a. KDProofRaw 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 = 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)
-> (SList Integer -> SInteger)
-> (Proof -> SList Integer -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
SMTConfig -> String -> a -> measure -> (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)
                (forall a. SymVal a => SList a -> SInteger
length @Integer) ((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: 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 = 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)
-> (SList Integer -> SInteger)
-> (Proof -> SList Integer -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
String -> a -> measure -> (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)
                (forall a. SymVal a => SList a -> SInteger
length @Integer) ((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 ()

-- | 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 = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
   _ <- String
-> (Forall "x" Integer -> SBool)
-> (SInteger -> SInteger)
-> (Proof -> SInteger -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
String -> a -> measure -> (Proof -> steps) -> KD Proof
sInduct String
"badMeasure"
                (\(Forall @"x" (SInteger
x :: SInteger)) -> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                (forall a. a -> a
id @SInteger) ((Proof -> SInteger -> (SBool, KDProofRaw SInteger)) -> KD Proof)
-> (Proof -> SInteger -> (SBool, KDProofRaw SInteger)) -> KD Proof
forall a b. (a -> b) -> a -> b
$
                \Proof
_h (SInteger
x :: SInteger) -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw 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
KDProofRaw SInteger
forall a. KDProofRaw a
qed

   pure ()

-- | The measure must always go down using lexicographic ordering. If not, SBV will flag this as a failure. We have:
--
-- >>> won'tProve4 `catch` (\(_ :: SomeException) -> pure ())
-- Inductive lemma (strong): badMeasure
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2
-- *** Failed to prove badMeasure.1.2.2.
-- <BLANKLINE>
-- *** Solver reported: canceled
won'tProve4 :: IO ()
won'tProve4 :: IO ()
won'tProve4 = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

   let -- a bizarre (but valid!) way to sum two integers
       weirdSum :: SInteger -> SInteger -> SInteger
weirdSum = String
-> (SInteger -> SInteger -> SInteger)
-> SInteger
-> SInteger
-> SInteger
forall a. (SMTDefinable 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)))

   _ <- SMTConfig
-> String
-> (Forall "x" Integer -> Forall "y" Integer -> SBool)
-> (SInteger -> SInteger -> SInteger)
-> (Proof -> SInteger -> SInteger -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
SMTConfig -> String -> a -> measure -> (Proof -> steps) -> KD Proof
sInductWith SMTConfig
z3{extraArgs = ["-t:5000"]} String
"badMeasure"
                (\(Forall @"x" (SInteger
x :: SInteger)) (Forall @"y" (SInteger
y :: SInteger)) -> 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
+ forall a. Num a => a -> a
abs @SInteger SInteger
y) ((Proof -> SInteger -> SInteger -> (SBool, KDProofRaw SInteger))
 -> KD Proof)
-> (Proof -> SInteger -> SInteger -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
                \Proof
ih (SInteger
x :: SInteger) (SInteger
y :: SInteger) ->
                    [SInteger
x 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)
|- 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, KDProofRaw SInteger)] -> KDProofRaw SInteger
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
x 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)
==> KDProofRaw SInteger
forall a. Trivial a => a
trivial
                                       , SInteger
x 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 -> 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 -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "x" Integer, Inst "y" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`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))
                                                  KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw 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
KDProofRaw SInteger
forall a. KDProofRaw a
qed
                                       ]

   pure ()