Sorting

Insertion sort

Our work this week will be proving a sort correct. We'll write a function sort that takes a list of natural numbers and rearranges it to be in ascending order. We'll allow duplicates: that is, [0;0;1] is sorted but [0;1;0] is not.

The algorithm we'll implement is called insertion sort, which works in the following way:

to insert an element i into an already sorted list l, simply walk down the list until we find an item greater than or equal to i---then put i into the list; and
given an unsorted list, insert each element into the recursive result of sorting the list.

Exercise: 2 stars, standard (insert_sorted)

First, let's write a function that inserts a number into a list that is already sorted ascending. Before you start writing the code, decide what each of the following expressions should evaluate to.

insert_sorted 5 [] = ???

insert_sorted 5 [10] = ???

insert_sorted 5 [1;6;0]

Fixpoint insert_sorted (i:nat) (l: list nat) : list nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Exercise: 1 star, standard (sort)

Now write the sorting function: given an arbitrary list of nats, you should return a sorted list. Use insert_sorted. Be sure to test it out on a variety of inputs!

Fixpoint sort (l: list nat) : list nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Does our sorting function work? We can try a few examples:

Compute (sort [10;9;8;7;6;5;4;3;2;1]).

Compute (sort [3;1;4;1;5;9;2;6;5;3;5]).
(* ===> 1;1;2;3;3;4;5;5;5;6;9 *)

Compute (insert_sorted 7 [1; 3; 4; 8; 12; 14; 18]).
(* ===> 1; 3; 4; 7; 8; 12; 14; 18 *)

What makes a sort correct?

In the latter two thirds of the course, we'll spend a great deal of time thinking about what makes a program (or function, or other formal artifact) correct. We're starting to write programs complex enough that we can ask those questions now, before we have proof as a formal tool.

So... what makes a sort correct? A good way to answer that question is to think of things that aren't sorts. We can then try to identify what's wrong with them.

Here are five sample lists, l₀ through l₄. We'll look at a few non-sorting functions and see what they do wrong.

Definition l₀ : list nat := [].
Definition l₁ : list nat := [1; 2; 3].
Definition l₂ : list nat := [2; 1; 3].
Definition l₃ : list nat := [5].
Definition l₄ : list nat := [5; 5; 5; 1; 2; 1; 2].

The easiest way to not be a sort is to have the wrong type. Sorts should take lists to lists!

Definition ill_typed_sort (l : list nat) : nat :=
  match l with
  | [] ⇒ 0
  | h :: _ ⇒ h
  end.

Next, a sort should return a list that, is, well, sorted.

Definition id_list (l : list nat) : list nat := l.

The returned list shouldn't miss any elements from the input list, either!

Definition const_empty_list (l : list nat) : list nat := [].

Definition head_only (l : list nat) : list nat :=
  match l with
  | [] ⇒ []
  | h :: _ ⇒ [h]
  end.

Elements that weren't in the input list shouldn't appear!

Definition extra_zero (l : list nat) : list nat :=
0 :: sort l.

Exercise: 2 stars, standard (remove_all)

Complete the definition of remove_all. Running remove_all n l should return a list that is the same as l, but with no occurrences of n.

Fixpoint remove_all (n : nat) (l : list nat) : list nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Exercise: 2 stars, standard (unique)

Complete the definition of unique, where unique l should compute the unique elements of l in the same order, i.e., it should return a list (a) with no duplicate elements and (b) doesn't do any other reordering.

Different approaches to the implementation may lead to different output orderings, i.e., the unique [1;2;1] might return [1;2] or it might return [2;1] . Either is fine.

You might have to write something that feels a little bit inefficient to have Coq accept your program. Oh well!

Fixpoint unique (l : list nat) : list nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Definition unique_sort (l : list nat) : list nat := unique (sort l).

Identifying sortedness

Having built some intuition, let's make it concrete. A function is a sort when:

It takes a list and returns another list, sorted ascending.
The output list is a permutation of the input list, i.e., the elements of the output list are just a rearrangement of the input elements, with no additions or deletions.

Let's write functions to identify these conditions.

Exercise: 3 stars, standard (is_sorted)

Complete is_sorted, which should return true when l is sorted.

You might end up struggling with Coq's termination requirements. There are two tricks to help you get unstuck:

1. Use a nested match to figure out what you'll do recursion on.

2. You can pattern match a list and capture part of it by writing:

   match [1;2;3;4;5] with
   | ...
   | h₁::((h₂::t₂) as t₁) ⇒ ... (h₁=1; h₂=2; t₂ = [3;4;5]; t₁ = [2;3;4;5])

Fixpoint is_sorted (l : list nat) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Exercise: 4 stars, standard (is_permutation_of)

Write a function is_permutation_of : list nat → list nat → bool that returns true when the first list is a permutation of the second. (Though if l₁ is a permutation of l₂, then l₂ is a permuation of l₁---the property is symmetric.)

There are two straightforward ways to do this, but one is easier than the other. Here are the ideas:

1. For each element x in l₁, try to remove exactly one x from l₂. If you can't, they're not permutations (x is in l₁ but not l₂!). If you can, then check to make sure that the rest of l₁ is a permutation of l₂ with one x removed.

2. Write a function that generates every permutation of l₁. Write a function to test equality, and then see if l₂ is in the list of all permutations of l₁.

Both approaches will work here, and both will need you to invent and define helper functions. Approach (1) is easier to write (just two helper functions, rather than three or four). It also happens to be much more efficient... a list of 5 elements has 120 permutations!

After you've written your function, we'd like you to write some test cases.

Fixpoint is_permutation_of (l₁ : list nat) (l₂ : list nat) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Write at least ten test cases---at least five in each list---that exercise is_permutation_of.

Definition permutation_true_tests : list (list nat × list nat) := [(* FILL IN HERE *)
].

Definition permutation_false_tests : list (list nat × list nat) := [(* FILL IN HERE *)
].

This should compute to true.

Compute (allb (map (fun (p:(list nat × list nat)) ⇒ let (x,y) := p in is_permutation_of x y) permutation_true_tests))
&& (allb (map (fun (p:(list nat × list nat)) ⇒ let (x,y) := p in negb (is_permutation_of x y)) permutation_false_tests)).
☐

(* 2022-01-12 10:20 *)