Require Export DMFP.Day05_lists. (* ################################################################# *) (** * 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 [nat]s, 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, [l0] through [l4]. We'll look at a few non-sorting functions and see what they do wrong. *) Definition l0 : list nat := []. Definition l1 : list nat := [1; 2; 3]. Definition l2 : list nat := [2; 1; 3]. Definition l3 : list nat := [5]. Definition l4 : 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 | ... | h1::((h2::t2) as t1) => ... (h1=1; h2=2; t2 = [3;4;5]; t1 = [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 [l1] is a permutation of [l2], then [l2] is a permuation of [l1]---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 [l1], try to remove exactly one [x] from [l2]. If you can't, they're not permutations ([x] is in [l1] but not [l2]!). If you can, then check to make sure that the rest of [l1] is a permutation of [l2] with one [x] removed. 2. Write a function that generates every permutation of [l1]. Write a function to test equality, and then see if [l2] is in the list of all permutations of [l1]. 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 (l1 : list nat) (l2 : 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 => is_permutation_of (fst p) (snd p)) permutation_true_tests)) && (allb (map (fun p => negb (is_permutation_of (fst p) (snd p))) permutation_false_tests)). (** [] *) (* 2021-09-13 09:44 *)