# BagPermInsertion Sort With Bags

*bags*(also called

*multisets*), which we introduced in Lists. A

*set*of values is like a list with no repeats where the order does not matter. A

*multiset*is like a list, possibly with repeats, where the order does not matter. Whereas the principal query on a set is whether a given element appears in it, the principal query on a bag is

*how many*times a given element appears in it.

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: ∀ b

_{1}b

_{2}, bag_eqv b

_{1}b

_{2}→ bag_eqv b

_{2}b

_{1}.

Proof.

(* FILL IN HERE *) Admitted.

Lemma bag_eqv_trans: ∀ b

_{1}b

_{2}b

_{3}, bag_eqv b

_{1}b

_{2}→ bag_eqv b

_{2}b

_{3}→ bag_eqv b

_{1}b

_{3}.

Proof.

(* FILL IN HERE *) Admitted.

The following little lemma is handy in a couple of places.

Lemma bag_eqv_cons : ∀ x b

_{1}b

_{2}, bag_eqv b

_{1}b

_{2}→ bag_eqv (x::b

_{1}) (x::b

_{2}).

Proof.

(* FILL IN HERE *) Admitted.

☐

# Correctness

*with the same multiset of values*, and this list must be totally ordered.

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 →

∃ l

l = l

∧ count x (l

Proof.

(* FILL IN HERE *) Admitted.

☐

S n = count x l →

∃ l

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

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

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

(* FILL IN HERE *) Admitted.

☐

Lemma count_insert_other : ∀ l

y ≠ x → count y (l

Proof.

(* FILL IN HERE *) Admitted.

☐

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

_{1}++ x :: l_{2}) = count y (l_{1}++ l_{2}).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.

(* 2020-08-07 17:08 *)