sbv-12.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.Majority

Description

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.

Synopsis

Calculating majority

majority :: SymVal a => SBV a -> SInteger -> SList a -> SBV a Source #

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.

mjrty :: SymVal a => SList a -> SBV a Source #

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.

howMany :: SymVal a => SBV a -> SList a -> SInteger Source #

The function how-many in the paper is already defined in SBV as count. Let's give it a name:

Correctness

correctness :: 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)) Source #

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)