-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Majority
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving Boyer-Moore's majority algorithm correct. We follow the ACL2 proof
-- closely, which you can find at <https://github.com/acl2/acl2/blob/master/books/demos/majority-vote.lisp>.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Majority where

import Prelude hiding (null, length)

import Data.SBV
import Data.SBV.List

import Data.SBV.TP
import qualified Data.SBV.TP.List as TP

-- * Calculating majority

-- | Given a list, calculate the majority element using Boyer-Moore's algorithm.
-- Note that the algorithm returns the majority if it exists. If there is no
-- majority element, then the result is irrelevant.
majority :: SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority :: forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority = String
-> (SBV a -> SInteger -> SList a -> SBV a)
-> SBV a
-> SInteger
-> SList a
-> SBV a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"majority"
                    ((SBV a -> SInteger -> SList a -> SBV a)
 -> SBV a -> SInteger -> SList a -> SBV a)
-> (SBV a -> SInteger -> SList a -> SBV a)
-> SBV a
-> SInteger
-> SList a
-> SBV a
forall a b. (a -> b) -> a -> b
$ \SBV a
c SInteger
i SList a
lst ->  SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
lst) SBV a
c
                                       (let (SBV a
x, SList a
xs) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
lst
                                        in SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0)
                                                (SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
x SInteger
1 SList a
xs)
                                                (SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
c (SInteger
i SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
c SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x) SInteger
1 (-SInteger
1)) SList a
xs))

-- | We can now define mjrty, which simply feeds the majority function with an arbitrary element of the domain.
-- By the definition of 'majority' above, this arbitrary element will be returned if the given list is empty.
-- Otherwise, majority will be returned if it exists, and an element of the list otherwise.
mjrty :: SymVal a => SList a -> SBV a
mjrty :: forall a. SymVal a => SList a -> SBV a
mjrty = SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority (String -> (SBV a -> SBool) -> SBV a
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"arb" (SBool -> SBV a -> SBool
forall a b. a -> b -> a
const SBool
sTrue)) SInteger
0

-- | The function @how-many@ in the paper is already defined in SBV as 'TP.count'. Let's give it a name:
howMany :: SymVal a => SBV a -> SList a -> SInteger
howMany :: forall a. SymVal a => SBV a -> SList a -> SInteger
howMany = SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
TP.count

-- * Correctness

-- | The generalized majority theorem. This comment is taken more or less
-- directly from J's proof, cast in SBV terms:
--
-- This is the generalized theorem that explains how majority works on any @c@ and
-- @i@ instead of just on the initial @c@ and @i=0@.
--
-- The way to imagine @majority c i xs@ is that we started with
-- a bigger @xs'@ that contains @i@ occurrences of c followed by @xs@. That is,
-- @xs' = replicate i c ++ xs@.  We know that @majority c 0 xs'@ finds
-- the majority in @xs'@ if there is one.
--
-- So the generalized theorem supposes that @e@ occurs a majority of times in @xs'@.
-- We can say that in terms of @c@, @i@, and @xs@: the number of times @e@ occurs in @xs@
-- plus @i@ (if @e@ is @c@) is greater than half of the length of @xs@ plus @i@.
--
-- The conclusion states that @majority c i x@ is @e@. We have:
--
-- >>> correctness @Integer
-- Inductive lemma: majorityGeneral
--   Step: Base                            Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                         Q.E.D.
--     Step: 1.1.2                         Q.E.D.
--     Step: 1.2.1                         Q.E.D.
--     Step: 1.2.2 (2 way case split)
--       Step: 1.2.2.1.1                   Q.E.D.
--       Step: 1.2.2.1.2                   Q.E.D.
--       Step: 1.2.2.2.1                   Q.E.D.
--       Step: 1.2.2.2.2                   Q.E.D.
--       Step: 1.2.2.Completeness          Q.E.D.
--     Step: 1.Completeness                Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: majority                         Q.E.D.
-- Lemma: ifExistsFound                    Q.E.D.
-- Lemma: ifNoMajority                     Q.E.D.
-- Lemma: uniqueness
--   Step: 1                               Q.E.D.
--   Result:                               Q.E.D.
-- ([Proven] majority :: Ɐc ∷ Integer → Ɐxs ∷ [Integer] → Bool,[Proven] ifExistsFound :: Ɐc ∷ Integer → Ɐxs ∷ [Integer] → Bool,[Proven] ifNoMajority :: Ɐc ∷ Integer → Ɐxs ∷ [Integer] → Bool,[Proven] uniqueness :: Ɐm1 ∷ Integer → Ɐm2 ∷ Integer → Ɐxs ∷ [Integer] → Bool)
correctness :: forall a. SymVal a
            => IO ( Proof (Forall "c" a -> Forall "xs" [a] -> SBool)                    -- If majority exists, the calculated value is majority
                  , Proof (Forall "c" a -> Forall "xs" [a] -> SBool)                    -- If majority exists, it is found
                  , Proof (Forall "c" a -> Forall "xs" [a] -> SBool)                    -- If returned value isn't majority, then no majority exists
                  , Proof (Forall "m1" a -> Forall "m2" a  -> Forall "xs" [a] -> SBool) -- Uniqueness: If there are two majorities, they're the same
                  )
correctness :: forall a.
SymVal a =>
IO
  (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
   Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
   Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
   Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
correctness = TP
  (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
   Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
   Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
   Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
-> IO
     (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
forall a. TP a -> IO a
runTP (TP
   (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
    Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
    Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
    Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
 -> IO
      (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
       Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
       Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
       Proof
         (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)))
-> TP
     (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
-> IO
     (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$ do

  -- Helper definition
  let isMajority :: SBV a -> SList a -> SBool
      isMajority :: SBV a -> SList a -> SBool
isMajority SBV a
e SList a
xs = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
xs SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
TP.count SBV a
e SList a
xs

  -- First prove the generalized majority theorem
  Proof
  (Forall "xs" [a]
   -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
majorityGeneral <-
     String
-> (Forall "xs" [a]
    -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
    -> IHArg
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
         a)
-> TP
     (Proof
        (Forall "xs" [a]
         -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
forall t.
(Proposition
   (Forall "xs" [a]
    -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a]
    -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
    -> IHArg
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
         t)
-> TP
     (Proof
        (Forall "xs" [a]
         -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> 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
"majorityGeneral"
            (\(Forall @"xs" SList a
xs) (Forall @"i" SInteger
i) (Forall @"e" (SBV a
e :: SBV a)) (Forall @"c" SBV a
c)
                  -> SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0 SBool -> SBool -> SBool
.&& (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
i) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
c) SInteger
i SInteger
0 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
TP.count SBV a
e SList a
xs SBool -> SBool -> SBool
.=> SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
c SInteger
i SList a
xs SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
e) ((Proof
    (IHType
       (Forall "xs" [a]
        -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
  -> IHArg
       (Forall "xs" [a]
        -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
  -> IStepArgs
       (Forall "xs" [a]
        -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
       a)
 -> TP
      (Proof
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
    -> IHArg
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a]
          -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
         a)
-> TP
     (Proof
        (Forall "xs" [a]
         -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof
  (IHType
     (Forall "xs" [a]
      -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
ih (SBV a
x, SList a
xs) SInteger
i SBV a
e SBV a
c ->
                   [SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0, (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
i) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
c) SInteger
i SInteger
0 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV a -> SList a -> SInteger
forall a. SymVal a => SBV a -> SList a -> SInteger
TP.count SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)]
                [SBool] -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
c SInteger
i (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw (SBV a))] -> TPProofRaw (SBV a)
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
x SInteger
1 SList a
xs
                                    SBV a -> Proof Bool -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a]
      -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
Proof (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
ih Proof (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> IArgs
     (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" SInteger
1, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SBV a
e, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV a
x)
                                    TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
e
                                    SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV a)
TPProofRaw (SBV a)
forall a. TPProofRaw a
qed
                         , SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
0 SBool -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
c (SInteger
i SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
c SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x) SInteger
1 (-SInteger
1)) SList a
xs
                                    SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw (SBV a))] -> TPProofRaw (SBV a)
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV a
c SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x SBool -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
c (SInteger
i SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SList a
xs
                                                        SBV a -> Proof Bool -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a]
      -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
Proof (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
ih Proof (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> IArgs
     (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SBV a
e, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV a
c)
                                                        TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
e
                                                        SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV a)
TPProofRaw (SBV a)
forall a. TPProofRaw a
qed
                                             , SBV a
c SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV a
x SBool -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBV a -> SInteger -> SList a -> SBV a
forall a. SymVal a => SBV a -> SInteger -> SList a -> SBV a
majority SBV a
c (SInteger
i SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1) SList a
xs
                                                        SBV a -> Proof Bool -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a]
      -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool))
Proof (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
ih Proof (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> IArgs
     (Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"i" (SInteger
iSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SBV a
e, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV a
c)
                                                        TPProofRaw (SBV a)
-> ChainsTo (TPProofRaw (SBV a)) -> ChainsTo (TPProofRaw (SBV a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
e
                                                        SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV a)
TPProofRaw (SBV a)
forall a. TPProofRaw a
qed
                                             ]
                         ]

  -- We can now prove the main theorem, by instantiating the general version.
  Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
correct <- String
-> (Forall "c" a -> Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "c" a -> Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"majority"
                   (\(Forall SBV a
c) (Forall SList a
xs) -> SBV a -> SList a -> SBool
isMajority SBV a
c SList a
xs SBool -> SBool -> SBool
.=> SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
mjrty SList a
xs SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
c)
                   [Proof
  (Forall "xs" [a]
   -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof
  (Forall "xs" [a]
   -> Forall "i" Integer -> Forall "e" a -> Forall "c" a -> SBool)
majorityGeneral]

  -- Corollary: If there is a majority element, then what we return is a majority element:
  Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
ifExistsFound <- String
-> (Forall "c" a -> Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "c" a -> Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"ifExistsFound"
                        (\(Forall SBV a
c) (Forall SList a
xs) -> SBV a -> SList a -> SBool
isMajority SBV a
c SList a
xs SBool -> SBool -> SBool
.=> SBV a -> SList a -> SBool
isMajority (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
mjrty SList a
xs) SList a
xs)
                        [Proof (Forall "c" a -> Forall "xs" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
correct]

  -- Contrapositive to the above: If the returned value is not majority, then there is no majority:
  Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
ifNoMajority <- String
-> (Forall "c" a -> Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "c" a -> Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"ifNoMajority"
                        (\(Forall SBV a
c) (Forall SList a
xs) -> SBool -> SBool
sNot (SBV a -> SList a -> SBool
isMajority (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
mjrty SList a
xs) SList a
xs) SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SBV a -> SList a -> SBool
isMajority SBV a
c SList a
xs))
                        [Proof (Forall "c" a -> Forall "xs" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
ifExistsFound]

  -- Let's also prove majority is unique, while we're at it, even though it is not essential for our main argument.
  Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)
unique <- String
-> (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)
-> StepArgs
     (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool) a
-> TP
     (Proof
        (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
forall t.
(Proposition
   (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)
-> StepArgs
     (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool) t
-> TP
     (Proof
        (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"uniqueness"
                 (\(Forall SBV a
m1) (Forall SBV a
m2) (Forall SList a
xs) -> SBV a -> SList a -> SBool
isMajority SBV a
m1 SList a
xs SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
isMajority SBV a
m2 SList a
xs SBool -> SBool -> SBool
.=> SBV a
m1 SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
m2) (StepArgs
   (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool) a
 -> TP
      (Proof
         (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)))
-> StepArgs
     (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool) a
-> TP
     (Proof
        (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV a
m1 SBV a
m2 SList a
xs -> [SBV a -> SList a -> SBool
isMajority SBV a
m1 SList a
xs, SBV a -> SList a -> SBool
isMajority SBV a
m2 SList a
xs]
                           [SBool] -> TPProofRaw (SBV a) -> (SBool, TPProofRaw (SBV a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a
m1
                           SBV a -> Proof Bool -> Hinted (SBV a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
correct Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "c" a -> Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV a
m1, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs)
                           TPProofRaw (SBV a) -> Proof Bool -> Hinted (TPProofRaw (SBV a))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
correct Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "c" a -> Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" SBV a
m2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs)
                           Hinted (TPProofRaw (SBV a))
-> ChainsTo (Hinted (TPProofRaw (SBV a)))
-> ChainsTo (Hinted (TPProofRaw (SBV a)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
m2
                           SBV a -> ChainsTo (SBV a) -> ChainsTo (SBV a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SBV a)
TPProofRaw (SBV a)
forall a. TPProofRaw a
qed

  (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
 Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
 Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
 Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
-> TP
     (Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "c" a -> Forall "xs" [a] -> SBool),
      Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
correct, Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
ifExistsFound, Proof (Forall "c" a -> Forall "xs" [a] -> SBool)
ifNoMajority, Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)
unique)