MultisetInsertion Sort Verified With Multisets
- {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
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 →
∃ l1 l2,
l = l1 ++ x :: l2
∧ contents (l1 ++ l2) x = n.
Proof.
(* FILL IN HERE *) Admitted.
☐
S n = contents l x →
∃ l1 l2,
l = l1 ++ x :: l2
∧ contents (l1 ++ l2) x = n.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma contents_insert_other : ∀ l1 l2 x y,
y ≠ x → contents (l1 ++ x :: l2) y = contents (l1 ++ l2) y.
Proof.
(* FILL IN HERE *) Admitted.
☐
y ≠ x → contents (l1 ++ x :: l2) y = contents (l1 ++ l2) y.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma contents_perm: ∀ al bl,
contents al = contents bl → Permutation al bl.
Proof.
intros al bl H0.
assert (H: ∀ x, contents al x = contents bl x).
{ rewrite H0. auto. }
clear H0.
generalize dependent bl.
(* FILL IN HERE *) Admitted.
☐
contents al = contents bl → Permutation al bl.
Proof.
intros al bl H0.
assert (H: ∀ x, contents al x = contents bl x).
{ rewrite H0. auto. }
clear H0.
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.
☐
(* 2024-11-04 20:41 *)