-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.McCarthy91
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving McCarthy's 91 function correct.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.McCarthy91 where

import Data.SBV
import Data.SBV.TP

-- * Definitions

-- | Nested recursive definition of McCarthy's function.
mcCarthy91 :: SInteger -> SInteger
mcCarthy91 :: SInteger -> SInteger
mcCarthy91 = String -> (SInteger -> SInteger) -> SInteger -> SInteger
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"mcCarthy91" ((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
100)
                                                  (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
10)
                                                  (SInteger -> SInteger
mcCarthy91 (SInteger -> SInteger
mcCarthy91 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
11)))
-- | Specification for McCarthy's function.
spec91 :: SInteger -> SInteger
spec91 :: SInteger -> SInteger
spec91 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
100) (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
10) SInteger
91

-- * Correctness

-- | We prove the equivalence of the nested recursive definition against the spec with a case analysis
-- and strong induction. We have:
--
-- >>> correctness
-- Lemma: case1                            Q.E.D.
-- Lemma: case2                            Q.E.D.
-- Inductive lemma (strong): case3
--   Step: Measure is non-negative         Q.E.D.
--   Step: 1 (unfold)                      Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: mcCarthy91
--   Step: 1 (3 way case split)
--     Step: 1.1                           Q.E.D.
--     Step: 1.2                           Q.E.D.
--     Step: 1.3                           Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- [Proven] mcCarthy91 :: Ɐn ∷ Integer → Bool
correctness :: IO (Proof (Forall "n" Integer -> SBool))
correctness :: IO (Proof (Forall "n" Integer -> SBool))
correctness = 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

   -- Case 1. When @n > 100@
   Proof (Forall "n" Integer -> SBool)
case1 <- String
-> (Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"case1" (\(Forall @"n" SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
100 SBool -> SBool -> SBool
.=> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec91 SInteger
n) []

   -- Case 2. When @90 <= n <= 100@
   Proof (Forall "n" Integer -> SBool)
case2 <- String
-> (Forall "n" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "n" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"case2" (\(Forall @"n" SInteger
n) -> SInteger
90 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
100 SBool -> SBool -> SBool
.=> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec91 SInteger
n) []

   -- Case 3. When @n < 90@. The crucial point here is the measure, which makes sure 101 < 100 < 99 < ...
   Proof (Forall "n" Integer -> SBool)
case3 <- 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
"case3"
                    (\(Forall SInteger
n) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
90 SBool -> SBool -> SBool
.=> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec91 SInteger
n)
                    (\SInteger
n -> SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
101 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
n)) ((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
90] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger -> SInteger
mcCarthy91 SInteger
n
                                       SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold"
                                       TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
mcCarthy91 (SInteger -> SInteger
mcCarthy91 (SInteger
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
11))
                                       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
n SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
11)
                                       TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
mcCarthy91 SInteger
91
                                       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

   -- Putting it all together
   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
"mcCarthy91"
        (\(Forall SInteger
n) -> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger
spec91 SInteger
n) (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 -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- [(SBool, TPProofRaw SInteger)] -> TPProofRaw SInteger
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
100               SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> Proof (Forall "n" Integer -> SBool) -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
case1 TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
spec91 SInteger
n 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
                          , SInteger
90 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
n SBool -> SBool -> SBool
.&& SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
100 SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> Proof (Forall "n" Integer -> SBool) -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
case2 TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
spec91 SInteger
n 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
                          , SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
90                SBool -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger -> SInteger
mcCarthy91 SInteger
n SInteger -> Proof (Forall "n" Integer -> SBool) -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "n" Integer -> SBool)
case3 TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SInteger
spec91 SInteger
n 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
                          ]