MultisetInsertion Sort Verified With Multisets

We previously used permutations to specify sorting. We could also use multisets, which are like sets but allow multiplicity of elements.
For example:
  • {1, 2} is a set, and is the same as set {2, 1}.
  • [1; 1; 2] is a list, and is different than list [2; 1; 1].
  • {1, 1, 2} is a multiset and the same as multiset {2, 1, 1}.
In this chapter we'll explore using multisets to specify sortedness.


A multiset maps a value to its multiplicity.

Definition value := nat.

Definition multiset := valuenat.
The empty multiset has multiplicity 0 for every value.

Definition empty : multiset :=
  fun x ⇒ 0.
Multiset singleton v contains only v, and exactly once.

Definition singleton (v: value) : multiset :=
  fun xif x =? v then 1 else 0.
The union of two multisets is their pointwise sum.

Definition union (a b : multiset) : multiset :=
  fun xa x + b x.

Specification of Sorting

The contents of a list are the elements it contains, without any notion of order. Function contents extracts the contents of a list as a multiset.

Fixpoint contents (al: list value) : multiset :=
  match al with
  | [] ⇒ empty
  | a :: blunion (singleton a) (contents bl)

Example sort_pi_same_contents:
  contents (sort [3;1;4;1;5;9;2;6;5;3;5]) = contents [3;1;4;1;5;9;2;6;5;3;5].
  extensionality x.
  repeat (destruct x; try reflexivity).
  (* Why does this work? Try it step by step, without repeat. *)

A sorting algorithm must preserve contents and totally order the list.

Definition is_a_sorting_algorithm' (f: list natlist nat) := al,
    contents al = contents (f al) ∧ sorted (f al).
That definition is similar to is_a_sorting_algorithm from Sort, except that we're now using contents instead of Permutation.

Verification of Insertion Sort

The exercises will take you through a verification of insertion sort, culminating in:

Exercise: 1 star, standard (insertion_sort_correct)

Finish the proof of correctness!

Theorem insertion_sort_correct :
  is_a_sorting_algorithm' sort.
  (* FILL IN HERE *) Admitted.

Equivalence of Permutation and Multiset Specifications

Exercise: 1 star, standard (same_contents_iff_perm)

Theorem same_contents_iff_perm: al bl,
    contents al = contents blPermutation al bl.
  (* FILL IN HERE *) Admitted.
Therefore the two specifications are equivalent.

Exercise: 2 stars, standard (sort_specifications_equivalent)

Theorem sort_specifications_equivalent: sort,
    is_a_sorting_algorithm sortis_a_sorting_algorithm' sort.
  (* FILL IN HERE *) Admitted.
That means we can verify sorting algorithms using either permutations or multisets, whichever we find more convenient.