# 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 := 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)
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 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.
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 blPermutation 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 sortis_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.