Adjacent deduplication with full multiplicities

The output is a list of key/count pairs with positive counts and strictly increasing keys. Expanding those runs recovers the sorted input exactly. This specifies the whole finite set and all multiplicities, rather than a one-way membership condition. These proofs are original.

Main definitions

• expand: expand key/count pairs into their repeated keys.
• RunEncoding: positive, strictly ordered runs reconstructing the input.

Main results

• RunEncoding.keys_nodup: each key occurs once.
• RunEncoding.mem_iff: the keys enumerate exactly the input set.
• RunEncoding.multiplicity: each count is the full input multiplicity.

def Cslib.Algorithms.WordRAM.Deduplicate.expand (rs : List (ℕ × ℕ)) : List ℕ

Expand a list of key/count pairs into repeated keys.

structure Cslib.Algorithms.WordRAM.Deduplicate.RunEncoding (xs : List ℕ) (rs : List (ℕ × ℕ)) : Prop

Runs with positive counts and strictly increasing keys reconstruct exactly xs.

• positive (p : ℕ × ℕ) : p ∈ rs → 0 < p.2

  Each emitted run is nonempty.

• ordered : List.Pairwise (fun (p q : ℕ × ℕ) => p.1 < q.1) rs

  A key never reappears after a different key.

• reconstruct : expand rs = xs

  All input positions are accounted for, with their exact order and multiplicity.

theorem Cslib.Algorithms.WordRAM.Deduplicate.expand_append (rs ss : List (ℕ × ℕ)) : expand (rs ++ ss) = expand rs ++ expand ss

Expansion distributes over concatenation.

theorem Cslib.Algorithms.WordRAM.Deduplicate.expand_singleton (k c : ℕ) : expand [(k, c)] = List.replicate c k

Expansion of one run.

theorem Cslib.Algorithms.WordRAM.Deduplicate.mem_expand {rs : List (ℕ × ℕ)} {k : ℕ} : k ∈ expand rs ↔ ∃ (p : ℕ × ℕ), p ∈ rs ∧ p.1 = k ∧ 0 < p.2

Every key in an expansion occurs in some nonempty run.

theorem Cslib.Algorithms.WordRAM.Deduplicate.length_le_expand {rs : List (ℕ × ℕ)} (hp : ∀ (p : ℕ × ℕ), p ∈ rs → 0 < p.2) : rs.length ≤ (expand rs).length

Positive runs contain at least one element each.

theorem Cslib.Algorithms.WordRAM.Deduplicate.RunEncoding.keys_nodup {xs : List ℕ} {rs : List (ℕ × ℕ)} (h : RunEncoding xs rs) : (List.map Prod.fst rs).Nodup

The key array contains no repeated key.

theorem Cslib.Algorithms.WordRAM.Deduplicate.RunEncoding.mem_iff {xs : List ℕ} {rs : List (ℕ × ℕ)} (h : RunEncoding xs rs) (k : ℕ) : k ∈ List.map Prod.fst rs ↔ k ∈ xs

The key array enumerates precisely the input set.

theorem Cslib.Algorithms.WordRAM.Deduplicate.RunEncoding.multiplicity {xs : List ℕ} {rs : List (ℕ × ℕ)} (h : RunEncoding xs rs) {p : ℕ × ℕ} (hp : p ∈ rs) : List.count p.1 xs = p.2

Each emitted count equals the full multiplicity in the input list.

theorem Cslib.Algorithms.WordRAM.Deduplicate.first_run (k : ℕ) (xs : List ℕ) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) (k :: xs)) : ∃ (c : ℕ), ∃ (rest : List ℕ), 0 < c ∧ k :: xs = List.replicate c k ++ rest ∧ ∀ (v : ℕ), v ∈ rest → k < v

A nonempty sorted list starts with a positive run of its head, followed only by larger keys. This is a mathematical decomposition used to verify the adjacent scan, not an oracle operation of the program.