(*|
===================================================
Week 3: Techniques for Defining Recursive Functions
===================================================

Author
  Nate Foster, with some materials from CS6115
License
  No redistribution allowed

.. coq:: none
|*)

Require Import String List Arith Lia.
Import ListNotations.
Open Scope string_scope.

(*|
.. contents::

And now for something completely different... We've seen how we can define some recursive functions in Coq, provided that it passes the termination checker. But what if we have a more complicated function? As an example, let's look at implementing merge sort for lists of natural numbers, using the standard ordering.
|*)

Definition nat_lte := Compare_dec.le_gt_dec.

(*|
First, we need to define a function to merge two (already sorted lists). Normally, we'd write this as follows:
|*)

Fail Fixpoint merge (xs ys:list nat) {struct xs} : list nat :=
  match xs, ys with
   | [], ys => ys
   | xs, [] => xs
   | x::xs', y::ys' => if nat_lte x y then
                         x :: (merge xs' ys)
                       else
                         y :: (merge xs ys')
   end. (* .unfold .fails .no-goals *)

(*|
Unfortunately, Coq will reject this because it's the case that xs is always getting smaller, nor the case that ys is always getting smaller.  Of course, one of them is always getting smaller, so eventually, this will terminate. But in this case, we can hack around the problem by simply re-organizing the function as follows.
|*)

Fixpoint merge (xs:list nat) : list nat -> list nat :=
  match xs with
  | nil => fun ys => ys
  | x::xs' =>
      (fix inner_merge (ys:list nat) : list nat :=
         match ys with
         | nil => x::xs'
         | y::ys' =>
             if nat_lte x y then
               x :: (merge xs' ys)
             else
               y :: (inner_merge ys')
         end)
  end.

(*|
We can write some examples to test that `merge` works as expected.

.. coq:: unfold
|*)

Compute merge [1;3;5] [2;4;6].
Eval compute in merge [3] [1;4].

(*|
Now let's write a pair of helper functions, one that takes a list of list of naturals and merges consecutive elements, and another that transforms a list into a list of singleton lists.
|*)

Fixpoint merge_pairs (xs:list (list nat)) : list (list nat) :=
  match xs with
  | h1::h2::t => (merge h1 h2) :: (merge_pairs t)
  | xs' => xs'
  end.

Definition make_lists (xs:list nat) : list (list nat) :=
  List.map (fun x => x::nil) xs.

(*|
Here are some examples to illustrate what these helper functions do.

.. coq:: unfold
|*)

Compute (make_lists [5; 1; 4; 2; 3]).
Compute (merge_pairs [[1;3];[2;4;9];[0];[2;3]]).
Compute (merge_pairs [[1;3];[2;4;9];[0]]).
Compute (merge_pairs
           (merge_pairs
              (merge_pairs
                 (make_lists [5; 1; 4; 2; 3])))).

(*|
Next we will prove an important lemma that relate the length of the list computed by `merge_pairs` to the length of its argument. Note that we prove a conjunction to get a strong enough induction hypothesis. (As a fun exercise, try to prove just the first conjunct by induction and see where you get stuck.)
|*)

Lemma merge_pairs_length' : forall xs,
  (forall h1 h2,
      length (merge_pairs (h1::h2::xs)) < length (h1::h2::xs)) /\
  (forall h,
      length (merge_pairs (h::xs)) <= length (h::xs)).
Proof.
  induction xs as [|x xs [H1 H2]].
  - simpl. split; lia.
  - split.
    + specialize (H2 x). simpl in *. lia.
    + intros x'. specialize (H1 x' x). lia.
Qed.

(*|
Next, we can prove a corollary that captures the case we will need to define merge sort.
|*)

Lemma merge_pairs_length : forall h1 h2 xs,
    length (merge_pairs (h1::h2::xs)) < length (h1::h2::xs).
Proof.
  intros.
  specialize (merge_pairs_length' xs).
  intros [H _].
  apply H.
Qed.

(*|
Recursive Functions with Explicit Termination Measures
======================================================

Now we are ready to define our merge sort. We'll do it by iterating `merge_pairs` until we have a singleton list. Since this iteration function is not structurally recursive, but rather, defined using a measure, we first need to import a couple of libraries.

.. coq:: in
|*)

Require Import Program.
Require Import Program.Wf.
Require Import Recdef.

(*|
The details of how the constructs in modules work is not important for now. The main thing to know is that the `Function` construct is siilar to `Fixpoint` but we must give a `{measure ...}` clause to tell Coq what is going down. In this case, the length of the argument list is always going down when we do a recursive call.
|*)

Function merge_iter (xs: list (list nat)) { measure length xs }
  : list nat :=
  match xs with
  | nil => nil
  | x::nil => x
  | x1::x2::xs' => merge_iter (merge_pairs (x1::x2::xs'))
  end.
Proof.
  intros. apply merge_pairs_length.
Defined.

(*|
Note that we had to use `merge_pairs_length` before Coq was willing to accept our recursive definition. It is also interesting to examine the objects that are generated by this definition.

.. coq:: unfold
|*)

Print merge_iter.
Print merge_iter_terminate.

(*|
With these pieces in hand, we can finally define our `merge_sort` function.
|*)

Definition merge_sort (xs:list nat) :=
  merge_iter (make_lists xs).

(*|
Let's test that is is working as expected:

.. coq:: unfold
|*)

Compute (merge_sort [7;8;3;5;1;2;6;4]).
Compute (merge_sort [3;2;7;8]).

(*|
Recursive Functions with Fuel (And, Type Classes!)
==================================================

Another approach to dealing with tricky general recursive functions is to approximate them using "fuel." To illustrate this approach, we'll introduce Coq's type classes, which are similar to Haskell's, and develop some constructs for pretty-printing various data types.

A type class defines an interface for some type.  In this case, we say that types `A` that implement the `Show` interface have a method named `show` that will convert them to a `string.`
|*)

Class Show (A:Type) := {
  show : A -> string
}.

(*|
Here is an instance for booleans.
|*)

Instance boolShow : Show bool := {
    show := fun (b:bool) => if b then "true" else "false"
  }.

Compute show true. (* .unfold *)
Compute show false. (* .unfold *)

(*|
Note that we cannot yet use this for natural numbers:
|*)

Compute (_: Show nat). (* .unfold *)
Eval compute in show 3. (* .unfold *)

(*|
To define a `Show` instance for natural numbers, let's first define a helper that shows a single digit.
|*)

Definition digit2string(d:nat) : string :=
  match d with
  | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3"
  | 4 => "4" | 5 => "5" | 6 => "6" | 7 => "7"
  | 8 => "8" | _ => "9"
  end.

(*|
Alas, it can be difficult to convince Coq that the iterated version of this helper function terminates.  So, we can simply give it fuel.
|*)

Fixpoint digits'(fuel n:nat) (accum : string) : string :=
  match fuel with
  | 0 => accum
  | S fuel' =>
      match n with
      | 0 => accum
      | _ => let d := digit2string(n mod 10) in
             digits' fuel' (n / 10) (d ++ accum)
      end
  end.

(*|
Fortunately, it's sufficient to use `n` as the fuel for itself, since we know we won't need to divide `n` by `10` more than `n` times.  We could of course use the `log` of `n` (base `10`) instead, but there's no benefit to being this precise, so we'll just use `n`.
|*)

Definition digits (n:nat) : string :=
  match digits' n n "" with
  | "" => "0"
  | ds => ds
  end.

(*|
Here is another version written using `Function` and with an explicit termination measure.
|*)

Function digits'' (n:nat) (accum:string) { measure (fun x => x) n }
  : string :=
  match n with
  | 0 => accum
  | _ => let d := digit2string(n mod 10) in
         digits'' (n / 10) (d ++ accum)
  end.
Proof.
  intros.
  apply Nat.div_lt; lia.
Qed.

(*|
Now we can define the `Show` instance for `nat`.
|*)

Instance natShow : Show nat := {
  show := digits
}.

Compute show 42. (* .unfold *)
Compute show (10+2). (* .unfold *)

(*|
Importantly, because we used a type class, we can still `show` booleans.
|*)

Compute show true. (* .unfold *)

(*|
We can also define parameterized `Show` instances, which allow us to show data structures.
|*)

Instance pairShow (A B:Type) (showA : Show A) (showB : Show B)
  : Show (A*B) := {
    show := (fun p => "(" ++
                        (show (fst p)) ++ "," ++
                        (show (snd p)) ++
                        ")")
  }.

Compute show (3,4). (* .unfold *)
Compute show (true,42). (* .unfold *)

Print pairShow. (* .unfold *)

Definition show_list {A:Type} {showA:Show A} (xs:list A) : string :=
  ("[" ++ ((fix loop (xs:list A) : string :=
              match xs with
              | nil => "]"
              | h::nil => show h ++ "]"
              | h::t => show h ++ "," ++ loop t
              end) xs)).

Instance listShow (A:Type) (showA:Show A)
  : Show (list A) := {
    show := @show_list A showA
  }.

(*|
.. coq:: unfold
|*)

Compute show (1::2::3::nil).
Compute show (true::false::nil).
Compute show ((1,true)::(42,false)::nil).
Compute show ((1::2::3::nil)::(4::5::nil)::(6::nil)::nil).

(*|
Type classes are a powerful abstraction tool that fit very well with some proof developments. If you decide to use them, one tip is to make type classes as small and simple as possible. For example, you probably want to separate out the operations you want to use from the properties that the implementation is expected to satisfy.
|*)