McCarthy91.hs

-----------------------------------------------------------------------------
-- |
-- 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 QuasiQuotes      #-}
{-# 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. We use 'smtFunctionWithContract' because
-- the nested recursion @mcCarthy91 (mcCarthy91 (n + 11))@ requires knowing what the inner call returns
-- in order to verify that the outer call's measure decreases. The contract states that for inputs @≤ 100@,
-- the result is @91@. Note that the contract itself is verified as part of the measure check: SBV proves
-- both measure decrease and the contract simultaneously via well-founded induction.
mcCarthy91 :: SInteger -> SInteger
mcCarthy91 = smtFunctionWithContract "mcCarthy91"
               ( \n -> 0 `smax` (101 - n)
               , \n r -> n .<= 100 .=> r .== 91
               , []
               )
           $ \n -> [sCase| n of
                      _ | 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.
-- Functions proven terminating: mcCarthy91
-- [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
                          ]