-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.PigeonHole
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proves the pigeon-hole principle. If a list of integers sum to more than the length
-- of the list itself, then some cell must contain a value larger than @1@.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP       #-}
{-# LANGUAGE DataKinds #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.PigeonHole where

import Prelude hiding (sum, length, elem, null, any)

import Data.SBV
import Data.SBV.List
import Data.SBV.TP

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV.TP
#endif

-- | Overflow: Some value is greater than 1.
overflow :: SList Integer -> SBool
overflow :: SList Integer -> SBool
overflow = (SBV Integer -> SBool) -> SList Integer -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any (SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
1)

-- | \(\sum xs > \lvert xs \rvert \Rightarrow \textrm{overflow}\, xs\)
--
-- >>> runTP pigeonHole
-- Inductive lemma: pigeonHole
--   Step: Base                            Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Result:                               Q.E.D.
--[Proven] pigeonHole :: Ɐxs ∷ [Integer] → Bool
pigeonHole :: TP (Proof (Forall "xs" [Integer] -> SBool))
pigeonHole :: TP (Proof (Forall "xs" [Integer] -> SBool))
pigeonHole = String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof (IHType (Forall "xs" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> SBool)
    -> IStepArgs (Forall "xs" [Integer] -> SBool) Bool)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall t.
(Proposition (Forall "xs" [Integer] -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [Integer] -> SBool)
-> (Proof (IHType (Forall "xs" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> SBool)
    -> IStepArgs (Forall "xs" [Integer] -> SBool) t)
-> TP (Proof (Forall "xs" [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
"pigeonHole"
                   (\(Forall SList Integer
xs) -> SList Integer -> SBV Integer
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
xs SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SList Integer -> SBV Integer
forall a. SymVal a => SList a -> SBV Integer
length SList Integer
xs SBool -> SBool -> SBool
.=> SList Integer -> SBool
overflow SList Integer
xs) ((Proof (IHType (Forall "xs" [Integer] -> SBool))
  -> IHArg (Forall "xs" [Integer] -> SBool)
  -> IStepArgs (Forall "xs" [Integer] -> SBool) Bool)
 -> TP (Proof (Forall "xs" [Integer] -> SBool)))
-> (Proof (IHType (Forall "xs" [Integer] -> SBool))
    -> IHArg (Forall "xs" [Integer] -> SBool)
    -> IStepArgs (Forall "xs" [Integer] -> SBool) Bool)
-> TP (Proof (Forall "xs" [Integer] -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \Proof (IHType (Forall "xs" [Integer] -> SBool))
ih (SBV Integer
x, SList Integer
xs) -> [SList Integer -> SBV Integer
forall a. (SymVal a, Num (SBV a)) => SList a -> SBV a
sum SList Integer
xs SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SList Integer -> SBV Integer
forall a. SymVal a => SList a -> SBV Integer
length SList Integer
xs]
                               [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList Integer -> SBool
overflow (SBV Integer
x SBV Integer -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                               SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV Integer
x SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV Integer
1 SBool -> SBool -> SBool
.|| SList Integer -> SBool
overflow SList Integer
xs)
                               SBool -> Proof SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "xs" [Integer] -> SBool))
ih
                               TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed