Sorting2
Permutations
Inductive Permutation {A : Type} : list A → list A → Prop :=
| perm_nil: Permutation [] []
| perm_skip (x:A) (l l':list A) (H : Permutation l l') : Permutation (x::l) (x::l')
| perm_swap (x y:A) (l:list A) : Permutation (y::x::l) (x::y::l)
| perm_trans (l1 l2 l3 : list A) (H12 : Permutation l1 l2) (H23 : Permutation l2 l3)
: Permutation l1 l3.
Example permutation_eg :
Permutation [true;true;false] [false;true;true].
Proof.
apply (perm_trans _ [true;false;true] _).
{ apply perm_skip.
apply perm_swap. }
{ apply perm_swap. }
Qed.
| perm_nil: Permutation [] []
| perm_skip (x:A) (l l':list A) (H : Permutation l l') : Permutation (x::l) (x::l')
| perm_swap (x y:A) (l:list A) : Permutation (y::x::l) (x::y::l)
| perm_trans (l1 l2 l3 : list A) (H12 : Permutation l1 l2) (H23 : Permutation l2 l3)
: Permutation l1 l3.
Example permutation_eg :
Permutation [true;true;false] [false;true;true].
Proof.
apply (perm_trans _ [true;false;true] _).
{ apply perm_skip.
apply perm_swap. }
{ apply perm_swap. }
Qed.
Theorem Permutation_length : ∀ A (l1 l2 : list A),
Permutation l1 l2 → length l1 = length l2.
Proof.
(* FILL IN HERE *) Admitted.
☐
Permutation l1 l2 → length l1 = length l2.
Proof.
(* FILL IN HERE *) Admitted.
☐
- Theorem: if l1 is a permutation of l2, then l1 and l2 have the same length.
- (perm_nil) We have l1 = [] and l2 = [], both of which have
length 0.
- (perm_skip) We have l1 = x::l1' and l2 = x::l2' and
Permutation l1' l2'; our IH shows that length l1' = length
l2'. We have length (x::l1') = length (x::l2') immediately by
the IH.
- (perm_swap) We have l1 = y::x::l and l2 = x::y::l. We have
length (y::x::l) = length (x::y::l) immediately.
- (perm_trans) We have l1 = l and l2 = l'' and a list l' such that Permutation l l' and Permutation l' l''; our IHs show that length l = length l' and length l' = length l''. We can find length l1 = l2 by transitivity of equality and our IHs. Qed.
(perm_nil) | |
Permutation [] [] |
Permutation l l' | (perm_skip) |
Permutation (x::l) (x::l') |
(perm_swap) | |
Permutation (y::x::l) (x::y::l) |
Permutation l l Permutation l' l'' | (perm_trans) |
Permutation l l'' |
l = [] l' = [] | (perm_nil') |
Permutation l l' |
Exercise: 1 star, standard (Permutation_sym)
Lemma Permutation_sym : ∀ A (l1 l2 : list A),
Permutation l1 l2 → Permutation l2 l1.
Proof.
(* FILL IN HERE *) Admitted.
☐
Permutation l1 l2 → Permutation l2 l1.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (All_perm)
To close, a useful utility lemma. Prove this by induction; but is it induction on al, or on bl, or on Permutation al bl, or on All f al? Some choices are much easier than others! If you're stuck, try a different one.
Theorem All_perm: ∀ {A} (f: A → Prop) al bl,
Permutation al bl →
All f al → All f bl.
Proof.
(* FILL IN HERE *) Admitted.
☐
Permutation al bl →
All f al → All f bl.
Proof.
(* FILL IN HERE *) Admitted.
☐
A computational interpretation
Fixpoint everywhere {A:Type} (a:A) (ls:list A) : list (list A) :=
match ls with
| [] ⇒ [[a]]
| h :: t ⇒ (a :: ls) :: (map (fun t' ⇒ h::t') (everywhere a t))
end.
Fixpoint permutations {A:Type} (ls:list A) : list (list A) :=
match ls with
| [] ⇒ [[]]
| h :: t ⇒ flat_map (everywhere h) (permutations t)
end.
match ls with
| [] ⇒ [[a]]
| h :: t ⇒ (a :: ls) :: (map (fun t' ⇒ h::t') (everywhere a t))
end.
Fixpoint permutations {A:Type} (ls:list A) : list (list A) :=
match ls with
| [] ⇒ [[]]
| h :: t ⇒ flat_map (everywhere h) (permutations t)
end.
Lemma everywhere_perm : ∀ A (l l' : list A) (x : A),
In l' (everywhere x l) →
Permutation (x :: l) l'.
Proof.
(* FILL IN HERE *) Admitted.
☐
In l' (everywhere x l) →
Permutation (x :: l) l'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem permutations_complete : ∀ A (l l' : list A),
In l' (permutations l) → Permutation l l'.
Proof.
(* FILL IN HERE *) Admitted.
☐
In l' (permutations l) → Permutation l l'.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 5 stars, advanced, optional (permutations_correct)
It's possible to prove the converse, that Permutation l l' implies In l' (permutations l). Feel free to give it a go, but it's very challenging! ☐
Fixpoint insert_sorted (i:nat) (l: list nat) :=
match l with
| nil ⇒ i::nil
| h::t ⇒ if leb i h then i::h::t else h :: insert_sorted i t
end.
Fixpoint sort (l: list nat) : list nat :=
match l with
| nil ⇒ nil
| h::t ⇒ insert_sorted h (sort t)
end.
match l with
| nil ⇒ i::nil
| h::t ⇒ if leb i h then i::h::t else h :: insert_sorted i t
end.
Fixpoint sort (l: list nat) : list nat :=
match l with
| nil ⇒ nil
| h::t ⇒ insert_sorted h (sort t)
end.
A sorting algorithm must rearrange the elements into a list that
is totally ordered.
What does it mean for a list to be sorted? We can define an
inductive proposition that seems to do the trick:
Inductive sorted: list nat → Prop :=
| sorted_nil : sorted []
| sorted_1 (x:nat) : sorted [x]
| sorted_cons (x y:nat) (l:list nat) (Hxy : x ≤ y) (H : sorted (y::l))
: sorted (x::y::l).
Example sorted_one_through_four :
sorted [1;2;3;4].
Proof.
(* WORKED IN CLASS *)
apply sorted_cons. { apply le_S. apply le_n. }
apply sorted_cons. { apply le_S. apply le_n. }
apply sorted_cons. { apply le_S. apply le_n. }
apply sorted_1.
Qed.
| sorted_nil : sorted []
| sorted_1 (x:nat) : sorted [x]
| sorted_cons (x y:nat) (l:list nat) (Hxy : x ≤ y) (H : sorted (y::l))
: sorted (x::y::l).
Example sorted_one_through_four :
sorted [1;2;3;4].
Proof.
(* WORKED IN CLASS *)
apply sorted_cons. { apply le_S. apply le_n. }
apply sorted_cons. { apply le_S. apply le_n. }
apply sorted_cons. { apply le_S. apply le_n. }
apply sorted_1.
Qed.
Is this really the right definition of what it means for a list to
be sorted? One might have thought that it should refer to list
indices, i.e., for valid indices i,j into the list, the ith item
is less than or equal to the jth item:
Fixpoint nth {X:Type} (n:nat) (l:list X) (default:X) : X :=
match n,l with
| _,[] ⇒ default
| 0,h::_ ⇒ h
| (S n'),_::t ⇒ nth n' t default
end.
Example nth_in_list : nth 3 [1;2;3;4;5] 0 = 4.
Proof. reflexivity. Qed.
Example nth_default : nth 7 [1;2;3;4;5] 0 = 0.
Proof. reflexivity. Qed.
Definition sorted' (al: list nat) :=
∀ i j, i < j < length al → nth i al 0 ≤ nth j al 0.
match n,l with
| _,[] ⇒ default
| 0,h::_ ⇒ h
| (S n'),_::t ⇒ nth n' t default
end.
Example nth_in_list : nth 3 [1;2;3;4;5] 0 = 4.
Proof. reflexivity. Qed.
Example nth_default : nth 7 [1;2;3;4;5] 0 = 0.
Proof. reflexivity. Qed.
Definition sorted' (al: list nat) :=
∀ i j, i < j < length al → nth i al 0 ≤ nth j al 0.
Note: the notation i < j < length al really means i < j ∧ j <
length al:
This is a reasonable definition too. It should be equivalent.
Later on, we'll prove that the two definitions really are
equivalent. For now, let's use the first one to define what it
means to be a correct sorting algorthm.
Definition is_a_sorting_algorithm (f: list nat → list nat) :=
∀ al, Permutation al (f al) ∧ sorted (f al).
∀ al, Permutation al (f al) ∧ sorted (f al).
That is: the result (f al) should not only be a sorted
sequence, but it should be some rearrangement (Permutation) of the
input sequence.
Proofs with Sortedness
Fixpoint is_sorted (l : list nat) : bool :=
match l with
| [] ⇒ true
| [_] ⇒ true
| x::(y::_) as l ⇒ leb x y && is_sorted l
end.
Lemma is_sorted_iff_sorted : ∀ l,
is_sorted l = true ↔ sorted l.
Proof.
(* WORKED IN CLASS *)
intros. split.
- intros H. induction l as [|n l' IHl'].
+ apply sorted_nil.
+ destruct l' as [|m l''].
× apply sorted_1.
× simpl is_sorted in H. apply andb_true_iff in H. apply sorted_cons.
{ destruct H as [H _]. apply leb_complete. apply H. }
{ destruct H as [_ H]. apply IHl'. apply H. }
- intros H. induction H as [|n|n m l' Hnm H IH].
+ reflexivity.
+ reflexivity.
+ simpl is_sorted.
apply leb_correct in Hnm.
rewrite Hnm.
simpl andb.
apply IH.
Qed.
match l with
| [] ⇒ true
| [_] ⇒ true
| x::(y::_) as l ⇒ leb x y && is_sorted l
end.
Lemma is_sorted_iff_sorted : ∀ l,
is_sorted l = true ↔ sorted l.
Proof.
(* WORKED IN CLASS *)
intros. split.
- intros H. induction l as [|n l' IHl'].
+ apply sorted_nil.
+ destruct l' as [|m l''].
× apply sorted_1.
× simpl is_sorted in H. apply andb_true_iff in H. apply sorted_cons.
{ destruct H as [H _]. apply leb_complete. apply H. }
{ destruct H as [_ H]. apply IHl'. apply H. }
- intros H. induction H as [|n|n m l' Hnm H IH].
+ reflexivity.
+ reflexivity.
+ simpl is_sorted.
apply leb_correct in Hnm.
rewrite Hnm.
simpl andb.
apply IH.
Qed.
In particular, what operations preserve sortedness? Which
functions will return a sorted list when given a sorted list?
We can formalize the notion of preservation as follows:
What operations on lists do we have? Let's start with simple ones,
like mapping (map). If we map the successor function S over a
sorted list, the list should still be sorted.
Lemma add1_preserves_sortedness :
preserves_sortedness (map S).
Proof.
intros al H. induction H.
- simpl map. apply sorted_nil.
- simpl map. apply sorted_1.
- simpl map. simpl in IHsorted.
apply sorted_cons.
apply n_le_m__Sn_le_Sm.
apply Hxy.
apply IHsorted.
Qed.
preserves_sortedness (map S).
Proof.
intros al H. induction H.
- simpl map. apply sorted_nil.
- simpl map. apply sorted_1.
- simpl map. simpl in IHsorted.
apply sorted_cons.
apply n_le_m__Sn_le_Sm.
apply Hxy.
apply IHsorted.
Qed.
We can do more than add one... we can add two!
Lemma add2_preserves_sortedness :
preserves_sortedness (map (plus 2)).
Proof.
intros al H. induction H.
- simpl map. apply sorted_nil.
- simpl map. apply sorted_1.
- simpl map. simpl plus in IHsorted. simpl map in IHsorted.
apply sorted_cons.
apply n_le_m__Sn_le_Sm.
apply n_le_m__Sn_le_Sm.
apply Hxy.
apply IHsorted.
Qed.
preserves_sortedness (map (plus 2)).
Proof.
intros al H. induction H.
- simpl map. apply sorted_nil.
- simpl map. apply sorted_1.
- simpl map. simpl plus in IHsorted. simpl map in IHsorted.
apply sorted_cons.
apply n_le_m__Sn_le_Sm.
apply n_le_m__Sn_le_Sm.
apply Hxy.
apply IHsorted.
Qed.
There are lots of functions that preserve sortedness. So many, in
fact, that we can characterize a set of them: the monotonic
functions are those that preserve ordering, i.e., if x ≤ y then
f x ≤ f y. Both S and (plus 2) are monotonic.
Every monotonic function preserves sortedness.
Lemma monotonic_preserves_sortedness : ∀ f,
monotonic f → preserves_sortedness (map f).
Proof.
intros f Hf.
intros al H. induction H.
- simpl map. apply sorted_nil.
- simpl map. apply sorted_1.
- simpl map. simpl map in IHsorted.
apply sorted_cons.
apply Hf. apply Hxy.
apply IHsorted.
Qed.
monotonic f → preserves_sortedness (map f).
Proof.
intros f Hf.
intros al H. induction H.
- simpl map. apply sorted_nil.
- simpl map. apply sorted_1.
- simpl map. simpl map in IHsorted.
apply sorted_cons.
apply Hf. apply Hxy.
apply IHsorted.
Qed.
Exercise: 3 stars, standard, optional (addn_preserves_sortedness)
Now prove that adding any number preserves sortedness.
Lemma addn_preserves_sortedness : ∀ n,
preserves_sortedness (map (plus n)).
Proof.
(* FILL IN HERE *) Admitted.
☐
preserves_sortedness (map (plus n)).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (sorted_smaller)
Lemma sorted_smaller : ∀ l x y,
x ≤ y →
sorted (y :: l) →
sorted (x :: l).
Proof. (* FILL IN HERE *) Admitted.
☐
x ≤ y →
sorted (y :: l) →
sorted (x :: l).
Proof. (* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard, optional (sorted_filter_cons)
Our proof goes in two stages. First, we show that if something is good at the front of a sorted list, it's also good at the front of a filtered sorted list.
Lemma sorted_filter_cons : ∀ l p x,
sorted (x :: l) →
sorted (x :: filter p l).
Proof.
(* FILL IN HERE *) Admitted.
☐
sorted (x :: l) →
sorted (x :: filter p l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard (filter_preserves_sortedness)
Using the (optional) lemma above, we can prove the more general property: (filter p) preserves sortedness for all predicates p.
Lemma filter_preserves_sortedness : ∀ p,
preserves_sortedness (filter p).
Proof.
(* FILL IN HERE *) Admitted.
☐
preserves_sortedness (filter p).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (bad_function_breaks_sortedness)
Definition bad_function : nat → nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Now prove that your function doesn't preserve sortedness.
Lemma bad_function_breaks_sortedness :
¬ preserves_sortedness (map bad_function).
Proof.
(* FILL IN HERE *) Admitted.
☐
¬ preserves_sortedness (map bad_function).
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof of Correctness
Exercise: 3 stars, standard (insert_sorted_perm)
Prove the following auxiliary lemma, insert_sorted_perm, which will be useful for proving sort_perm below. Your proof will be by induction, but you'll need some of the permutation facts from the above.
Lemma insert_sorted_perm: ∀ x l, Permutation (x::l) (insert_sorted x l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard (insert_sorted_sorted)
This one is a bit tricky. However, there is just a single induction right at the beginning, and you do not need to use insert_sorted_perm or sort_perm. The leb_spec lemma from day 16 may come in handy, or you can (destruct leb ...) and use leb_iff and leb_n_m__leb_m_n.
Lemma insert_sorted_sorted:
∀ a l, sorted l → sorted (insert_sorted a l).
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ a l, sorted l → sorted (insert_sorted a l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem insertion_sort_correct:
is_a_sorting_algorithm sort.
Proof.
split. apply sort_perm. apply sort_sorted.
Qed.
is_a_sorting_algorithm sort.
Proof.
split. apply sort_perm. apply sort_sorted.
Qed.
Exercise: 2 stars, standard, optional (sort_stable)
It's a nice exercise to prove the idempotence and stability lemmas from the informal work in Coq.
Lemma sort_already_sorted : ∀ l,
sorted l → sort l = l.
Proof.
(* FILL IN HERE *) Admitted.
Corollary sort_idempotent : ∀ l,
sort (sort l) = sort l.
Proof.
(* FILL IN HERE *) Admitted.
☐
sorted l → sort l = l.
Proof.
(* FILL IN HERE *) Admitted.
Corollary sort_idempotent : ∀ l,
sort (sort l) = sort l.
Proof.
(* FILL IN HERE *) Admitted.
☐
Making Sure the Specification is Right
Exercise: 4 stars, standard, optional (sorted_sorted')
Hint: Instead of doing induction on the list al, do induction
on the sortedness of al. This proof is a bit tricky, so
you may have to think about how to approach it, and try out
one or two different ideas.
(* FILL IN HERE *) Admitted.
☐
☐
Here, you can't do induction on the sorted'-ness of the list,
because sorted' is not an inductive predicate.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *) Admitted.
☐
Proving Correctness from the Alternate Spec
- insert_sorted_perm, sort_perm
- All_perm, Permutation_length
- Permutation_sym, Permutation_trans
- a new lemma All_nth, stated below.
Exercise: 3 stars, standard, optional (All_nth)
Lemma All_nth:
∀ {A: Type} (P: A → Prop) d (al: list A),
All P al ↔ (∀ i, i < length al → P (nth i al d)).
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ {A: Type} (P: A → Prop) d (al: list A),
All P al ↔ (∀ i, i < length al → P (nth i al d)).
Proof.
(* FILL IN HERE *) Admitted.
☐
(* Prove that inserting into a sorted list yields a sorted list, for
the index-based notion of sorted.
You'll find leb_spec handy again. If you find that your context
gets cluttered, you can run clear H to get rid of the hypothesis
H; you can run clear - H to get rid of everything _but_ H. Be
careful---you can't undo these tactics! *)
Lemma insert_sorted_sorted':
∀ a l, sorted' l → sorted' (insert_sorted a l).
(* FILL IN HERE *) Admitted.
☐
the index-based notion of sorted.
You'll find leb_spec handy again. If you find that your context
gets cluttered, you can run clear H to get rid of the hypothesis
H; you can run clear - H to get rid of everything _but_ H. Be
careful---you can't undo these tactics! *)
Lemma insert_sorted_sorted':
∀ a l, sorted' l → sorted' (insert_sorted a l).
(* FILL IN HERE *) Admitted.
☐
The Moral of This Story
(* 2022-01-12 10:20 *)