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

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

Proof.

(* FILL IN HERE *) Admitted.

Lemma bag_eqv_trans: ∀ b

Proof.

(* FILL IN HERE *) Admitted.

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

Proof.

(* FILL IN HERE *) Admitted.

☐

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

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

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.

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

(* 2023-03-25 11:22 *)