Tutorial: Boyer-Moore Majority Vote

In this tutorial, we verify the Boyer-Moore majority voting algorithm (MJRTY) — a celebrated algorithm that finds the majority element of a sequence using only constant extra space. The proof demonstrates how to use lemmas strategically to guide ImandraX.

The algorithm

The majority vote algorithm maintains a candidate and a counter. It scans the list once, incrementing the counter for matching elements and decrementing for mismatches:

let rec majority_aux c i xs =
  match xs with
  | [] -> c
  | x :: xs ->
    if i = 0 then majority_aux (Some x) 1 xs
    else majority_aux c (i + (if (Some x) = c then 1 else -1)) xs
[@@adm xs]
 
let majority xs =
  majority_aux None 0 xs

The [@@adm xs] annotation proves termination: xs gets shorter on each recursive call.

Helper definitions

We need to count occurrences and define what a "majority" means:

let rec num_occurs c xs =
  match xs with
  | [] -> 0
  | x :: xs ->
    (if x = c then 1 else 0) + num_occurs c xs
 
let is_majority c xs =
  2 * num_occurs c xs > List.length xs

An element is a "majority" if it appears more than half the time.

The key lemma

The core insight is captured in this lemma about majority_aux:

lemma majority_key e c i xs =
  i >= 0
  && (i + List.length xs)
      < 2 * ((if c = (Some e) then i else 0) + num_occurs e xs)
  ==>
  majority_aux c i xs = Some e
[@@by auto]

This says: if the "effective count" of element e (the counter contribution plus remaining occurrences) exceeds half the remaining elements, then majority_aux will find e.

The proof requires induction on xs (the list being scanned), which auto handles automatically.

The main theorem

lemma majority_is_correct c xs =
  is_majority c xs
  ==>
  majority xs = Some c
[@@by [%use majority_key c (Some c) 0 xs] @> auto]

This is the main correctness result: if a majority element exists, the algorithm finds it.

Note the proof strategy:

• [%use majority_key c (Some c) 0 xs] instantiates the key lemma with the initial state (c = Some c, i = 0)
• @> auto handles the remaining simplification

Without the [%use ...] hint, auto alone would struggle — it wouldn't know how to instantiate the universal quantifiers in majority_key. This is a common pattern: you provide the right lemma instance, then let automation finish the job.

A beautiful corollary

There can be at most one majority element:

lemma majority_unique c d xs =
  is_majority c xs && is_majority d xs
  ==>
  c = d
[@@by [%use majority_is_correct c xs]
   @> [%use majority_is_correct d xs]
   @> auto]

The proof is elegant: if both c and d are majorities, then majority xs = Some c and majority xs = Some d. Since majority returns a single value, c = d.

The tactic:

1. [%use majority_is_correct c xs] — adds majority xs = Some c to the hypotheses
2. [%use majority_is_correct d xs] — adds majority xs = Some d to the hypotheses
3. auto — derives c = d from the two equalities

The complete specification

Together, these theorems give a complete specification of the algorithm:

1. Correctness: If a majority exists, majority finds it (majority_is_correct)
2. Uniqueness: At most one majority can exist (majority_unique)

Note what the specification does not say: if no majority element exists, majority is free to return any element. This is by design — the algorithm only guarantees correct behavior when a majority exists.

What you've learned

• Strategic lemma usage with [%use ...] to guide automation
• Algorithm verification — specifying and proving correctness of non-trivial algorithms
• Corollary proofs — deriving consequences from established results
• Specification design — knowing what to prove (and what not to prove)
• The [@@adm] annotation for termination on structurally decreasing arguments

Next steps

The Interactive Proofs tutorial shows how to use the VS Code goal state viewer to develop complex proofs step by step.