-----------------------------------------------------------------------------
-- |
-- 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 #-}

{-# 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 = smtFunction "mcCarthy91" $ \n -> ite (n .> 100)
                                                  (n - 10)
                                                  (mcCarthy91 (mcCarthy91 (n + 11)))
-- | Specification for McCarthy's function.
spec91 :: SInteger -> SInteger
spec91 n = ite (n .> 100) (n - 10) 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 = runTP $ do

   -- Case 1. When @n > 100@
   case1 <- lemma "case1" (\(Forall @"n" n) -> n .>= 100 .=> mcCarthy91 n .== spec91 n) []

   -- Case 2. When @90 <= n <= 100@
   case2 <- lemma "case2" (\(Forall @"n" n) -> 90 .<= n .&& n .<= 100 .=> mcCarthy91 n .== spec91 n) []

   -- Case 3. When @n < 90@. The crucial point here is the measure, which makes sure 101 < 100 < 99 < ...
   case3 <- sInduct "case3"
                    (\(Forall n) -> n .< 90 .=> mcCarthy91 n .== spec91 n)
                    (\n -> abs (101 - n), []) $
                    \ih n -> [n .< 90] |- mcCarthy91 n
                                       ?? "unfold"
                                       =: mcCarthy91 (mcCarthy91 (n + 11))
                                       ?? ih `at` Inst @"n" (n + 11)
                                       =: mcCarthy91 91
                                       =: qed

   -- Putting it all together
   calc "mcCarthy91"
        (\(Forall n) -> mcCarthy91 n .== spec91 n) $
        \n -> [] |- cases [ n .> 100               ==> mcCarthy91 n ?? case1 =: spec91 n =: qed
                          , 90 .<= n .&& n .<= 100 ==> mcCarthy91 n ?? case2 =: spec91 n =: qed
                          , n .< 90                ==> mcCarthy91 n ?? case3 =: spec91 n =: qed
                          ]