Functional Programming in Coq : TD3 =================================== **M2 LMFI** Remainder : ```coq Require Import Bool Arith List. Import ListNotations. ``` ## Classical exercises on lists Program the following functions, without using the corresponding functions from the Coq standard library : - `length` - concatenate (`app` in Coq, infixe notation `++`) - `rev` (for reverse, a.k.a mirror) - `map : forall {A B}, (A->B)-> list A -> list B` - `filter : forall {A}, (A->bool) -> list A -> list A` - at least one `fold` function, either `fold_right` or `fold_left` - `seq : nat -> nat -> list nat`, such that `seq a n = [a; a+1; ... a+n-1]` Why is it hard to program function like `head`, `last` or `nth` ? How can we do ? ## Some executable predicates on lists - `forallb : forall {A}, (A->bool) -> list A -> bool`. - `increasing` which tests whether a list of numbers is strictly increasing. - `delta` which tests whether two successive numbers of the list are always apart by at least `k`. ## Mergesort - Write a `split` function which dispatch the elements of a list into two lists of half the size (or almost). It is not important whether an element ends in the first or second list. In particular, concatenating the two final lists will not necessary produce back the initial one, just a permutation of it. - Write a `merge` function which merges two sorted lists into a new sorted list containing all elements of the initial ones. This can be done with structural recursion thanks to a inner `fix` (see `ack` in the session 3 of the course). - Write a `mergesort` function based on the former functions. ## Powerset Write a `powerset` function which takes a list `l` and returns the list of all subsets of `l`. For instance `powerset [1;2] = [[];[1];[2];[1;2]]`. The order of subsets in the produced list is not relevant.