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.

Multisets

A multiset maps a value to its multiplicity.

Definition value := nat.
Definition multiset := value → nat.
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 x ⇒ if x =? v then 1 else 0.
The union of two multisets is their pointwise sum.

Definition union (a b : multiset) : multiset :=
  fun x ⇒ a 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 :: bl ⇒ union (singleton a) (contents bl)
  end.
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].
Proof.
  extensionality x.
  repeat (destruct x; try reflexivity).
  (* Why does this work? Try it step by step, without repeat. *)
Qed.

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

Definition is_a_sorting_algorithm' (f: list nat → list 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.
Proof.
  (* 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 bl ↔ Permutation al bl.
Proof.
  (* 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 sort ↔ is_a_sorting_algorithm' sort.
Proof.
  (* FILL IN HERE *) Admitted.
☐
That means we can verify sorting algorithms using either permutations or multisets, whichever we find more convenient.