BagPermInsertion Sort With Bags
From Coq Require Import Strings.String. (* for manual grading *)
From Coq Require Import Setoid Morphisms.
From VFA Require Import Perm.
From VFA Require Import Sort.
To keep this chapter more self-contained,
we restate the critical definitions from Lists.
Definition bag := list nat.
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil ⇒ 0
| h :: t ⇒
(if h =? v then 1 else 0) + count v t
end.
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil ⇒ 0
| h :: t ⇒
(if h =? v then 1 else 0) + count v t
end.
We will say two bags are equivalent if they have the same number
of copies of every possible element.
(* It is easy to prove bag_eqv is an equivalence relation. *)
Lemma bag_eqv_refl : ∀ b, bag_eqv b b.
Proof.
(* FILL IN HERE *) Admitted.
Lemma bag_eqv_sym: ∀ b1 b2, bag_eqv b1 b2 → bag_eqv b2 b1.
Proof.
(* FILL IN HERE *) Admitted.
Lemma bag_eqv_trans: ∀ b1 b2 b3, bag_eqv b1 b2 → bag_eqv b2 b3 → bag_eqv b1 b3.
Proof.
(* FILL IN HERE *) Admitted.
The following little lemma is handy in a couple of places.
Lemma bag_eqv_cons : ∀ x b1 b2, bag_eqv b1 b2 → bag_eqv (x::b1) (x::b2).
Proof.
(* FILL IN HERE *) Admitted.
☐
Correctness
Definition is_a_sorting_algorithm' (f: list nat → list nat) :=
∀ al, bag_eqv al (f al) ∧ sorted (f al).
Exercise: 3 stars, standard (insert_bag)
First, prove the auxiliary lemma insert_bag, which will be useful for proving sort_bag below. Your proof will be by induction.Theorem insertion_sort_correct:
is_a_sorting_algorithm' sort.
Proof.
split. apply sort_bag. apply sort_sorted.
Qed.
Exercise: 1 star, standard (permutations_vs_multiset)
Compare your proofs of insert_perm, sort_perm with your proofs of insert_bag, sort_bag. Which proofs are simpler?- easier with permutations,
- easier with multisets
- about the same.
- permutations or
- 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.
☐
Permutations and Multisets
Exercise: 3 stars, standard (perm_bag)
The forward direction is straighforward, by induction on the evidence for Permutation:
Lemma perm_bag:
∀ al bl : list nat,
Permutation al bl → bag_eqv al bl.
(* FILL IN HERE *) Admitted.
☐
∀ al bl : list nat,
Permutation al bl → bag_eqv al bl.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, advanced (bag_nil_inv)
Lemma bag_cons_inv : ∀ l x n,
S n = count x l →
∃ l1 l2,
l = l1 ++ x :: l2
∧ count x (l1 ++ l2) = n.
Proof.
(* FILL IN HERE *) Admitted.
☐
S n = count x l →
∃ l1 l2,
l = l1 ++ x :: l2
∧ count x (l1 ++ l2) = n.
Proof.
(* FILL IN HERE *) Admitted.
☐
Lemma count_insert_other : ∀ l1 l2 x y,
y ≠ x → count y (l1 ++ x :: l2) = count y (l1 ++ l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
y ≠ x → count y (l1 ++ x :: l2) = count y (l1 ++ l2).
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem bag_eqv_iff_perm:
∀ al bl, bag_eqv al bl ↔ Permutation al bl.
Proof.
intros. split. apply bag_perm. apply perm_bag.
Qed.
∀ al bl, bag_eqv al bl ↔ Permutation al bl.
Proof.
intros. split. apply bag_perm. apply perm_bag.
Qed.
Therefore, it doesn't matter whether you prove your sorting
algorithm using the Permutations method or the multiset method.
Corollary sort_specifications_equivalent:
∀ sort, is_a_sorting_algorithm sort ↔ is_a_sorting_algorithm' sort.
Proof.
unfold is_a_sorting_algorithm, is_a_sorting_algorithm'.
split; intros;
destruct (H al); split; auto;
apply bag_eqv_iff_perm; auto.
Qed.
(* 2021-05-04 07:54 *)