# MultisetInsertion Sort Verified With Multisets

*set*is like a list in which element order is irrelevant, and in which no duplicate elements are permitted. That is, an element can either be

*in*the set or not in the set, but it can't be in the set multiple times. A

*multiset*relaxes that restriction: an element can be in the multiset multiple times. The number of times the element occurs in the multiset is the element's

*multiplicity*.

- {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}.

# Multisets

The empty multiset has multiplicity 0 for every value.

Multiset singleton v contains only v, and exactly once.

The union of two multisets is their

*pointwise*sum.#### Exercise: 1 star, standard (union_assoc)

Lemma union_assoc: ∀ a b c : multiset,

union a (union b c) = union (union a b) c.

Proof.

intros.

extensionality x.

(* FILL IN HERE *) Admitted.

☐

union a (union b c) = union (union a b) c.

Proof.

intros.

extensionality x.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard (union_swap)

Lemma union_swap : ∀ a b c : multiset,

union a (union b c) = union b (union a c).

Proof.

(* FILL IN HERE *) Admitted.

☐

union a (union b c) = union b (union a c).

Proof.

(* FILL IN HERE *) Admitted.

☐

# Specification of Sorting

*with the same multiset of values*, and this list must be totally ordered. Let's formalize that idea.

*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.

match al with

| [] ⇒ empty

| a :: bl ⇒ union (singleton a) (contents bl)

end.

The insertion-sort program sort from Sort preserves
the contents of a list. Here's an example of that:

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.

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).

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.
The following series of exercises will take you through a
verification of insertion sort using multisets.
Prove that insertion sort's insert function produces the same
contents as merely prepending the inserted element to the front of
the list.
Proceed by induction. You do not need extensionality if you
make use of the above lemmas about union.

# Verification of Insertion Sort

#### Exercise: 3 stars, standard (insert_contents)

Lemma insert_contents: ∀ x l,

contents (insert x l) = contents (x :: l).

Proof.

(* FILL IN HERE *) Admitted.

☐

contents (insert x l) = contents (x :: l).

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard (sort_contents)

Theorem insertion_sort_correct :

is_a_sorting_algorithm' sort.

Proof.

(* FILL IN HERE *) Admitted.

☐

is_a_sorting_algorithm' sort.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 1 star, standard (permutations_vs_multiset)

Compare your proofs of insert_perm, sort_perm with your proofs of insert_contents, sort_contents. Which proofs are simpler?- easier with permutations
- easier with multisets
- about the same

- permutations
- multisets

(* Do not modify the following line: *)

Definition manual_grade_for_permutations_vs_multiset : option (nat×string) := None.

☐

Definition manual_grade_for_permutations_vs_multiset : option (nat×string) := None.

☐

# Equivalence of Permutation and Multiset Specifications

Permutation al bl ↔ contents al = contents bl

## The Forward Direction

#### Exercise: 3 stars, standard (perm_contents)

Lemma perm_contents: ∀ al bl : list nat,

Permutation al bl → contents al = contents bl.

Proof.

(* FILL IN HERE *) Admitted.

☐

Permutation al bl → contents al = contents bl.

Proof.

(* FILL IN HERE *) Admitted.

☐

## The Backward Direction (Advanced)

#### Exercise: 2 stars, advanced (contents_nil_inv)

Lemma contents_nil_inv : ∀ l, (∀ x, 0 = contents l x) → l = nil.

Proof.

(* FILL IN HERE *) Admitted.

☐

Proof.

(* FILL IN HERE *) Admitted.

☐

Lemma contents_cons_inv : ∀ l x n,

S n = contents l x →

∃ l

l = l

∧ contents (l

Proof.

(* FILL IN HERE *) Admitted.

☐

S n = contents l x →

∃ l

_{1}l_{2},l = l

_{1}++ x :: l_{2}∧ contents (l

_{1}++ l_{2}) x = n.Proof.

(* FILL IN HERE *) Admitted.

☐

Lemma contents_insert_other : ∀ l

y ≠ x → contents (l

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}l_{2}x y,y ≠ x → contents (l

_{1}++ x :: l_{2}) y = contents (l_{1}++ l_{2}) y.Proof.

(* FILL IN HERE *) Admitted.

☐

Lemma contents_perm: ∀ al bl,

contents al = contents bl → Permutation al bl.

Proof.

intros al bl H

assert (H: ∀ x, contents al x = contents bl x).

{ rewrite H

clear H

generalize dependent bl.

(* FILL IN HERE *) Admitted.

☐

contents al = contents bl → Permutation al bl.

Proof.

intros al bl H

_{0}.assert (H: ∀ x, contents al x = contents bl x).

{ rewrite H

_{0}. auto. }clear H

_{0}.generalize dependent bl.

(* FILL IN HERE *) Admitted.

☐

## The Main Theorem

#### 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.

☐

contents al = contents bl ↔ Permutation al bl.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### 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.

☐

is_a_sorting_algorithm sort ↔ is_a_sorting_algorithm' sort.

Proof.

(* FILL IN HERE *) Admitted.

☐

(* 2021-05-26 10:00 *)