Proving sorting algorithms correct

September 8, 2014 - Tagged as: coq, en.

I’ve been working on proving some sorting algorithms correct in Coq. After 600 lines of Coq proofs, I managed to prove correctness of insertion sort, selection sort, and a weird sorting algorithm called pancake sort. This post is a literate Coq file which you can download and execute in a Coq IDE, step by step. To keep the post shorter and easier to read and make it more like an exercise, I hided most of the proofs in HTML version.

Goals of this post are:

• Provide some guidance for starters who are interested in proving algorithms correct.
• Demonstrate how to prove properties of functions with accumulators and functions that work on list indexes, instead of elements of the list.
• Demonstrate how to use “timeout” arguments to convince Coq that a function is really terminating on all inputs.

A note before starting: I deliberately ignored advanced proof automation tools and go with more primitive way of proving. This is for two reasons: 1) I don’t like magic, and since I don’t understand underlying mechanics of advanced proofs tactics like [crush], it’s magic to me 2) They’re sometimes so powerful, they get in your way to understand what’s really happening in the proof.

If you’re reading this post as an exercise and filling the proofs yourself, that should not be a problem for you. Otherwise you may find my proofs more verbose than what’s necessary.

Let’s start with standard stuff: imports. These are for some list helpers, list syntax, Peano definitions + functions etc. Just standard stuff. Only exception is the [Permutation] library, which I’ll soon explain why it’s necessary.

Require Import List.
Import ListNotations.
Open Scope list_scope.
Require Import Arith.
Require Import Omega.
Require Import Permutation.

Our goal is to define some sorting algorithms and then prove them correct, but for that we first need to define what we mean by for a sorting algorithm to be “correct”. For some functions definition of correctness may be tricky to give, but in the context of sorting I think it’s obvious:

• Result should be a permutation of it’s parameter.
• Result should be in sorted order.

Definition of a “permutation” is defined in the [Permutation] library we’ve just included, and it comes with lots of very useful lemmas. I suggest you to go to [Permutation] library’s documentation(you can go to the docs by clicking [Permutation] link in the imports part above) and just skim through the definition and lemmas, and convince yourself that the definition is really enough to show that two lists are really a permutation.

For being sorted, we need to define what does that mean.

Inductive sorted : list nat -> Prop :=
| Sorted_nil : sorted []
| Sorted_singleton : forall e, sorted [e]
| Sorted_cons : forall e h t, sorted (h :: t) -> e <= h -> sorted (e :: h :: t).
(* begin hide *)
Hint Constructors sorted.
(* end hide *)

Again, convince yourself that sorted l really encodes what we intuitively know about being sorted. Main property that should hold for any l that is sorted l is that for any consecutive elements a and b in the list, a <= b should hold, which our third constructor shows.

Using Permutation and sorted, we can define what does being correct for a sorting algorithm mean:

Inductive Sorting_correct (algo : list nat -> list nat) :=
| sorting_correct_intro :
    (forall l, sorted (algo l) /\ Permutation l (algo l)) -> Sorting_correct algo.

Note that in both definition of sorted and Sorting_correct, we used list of nats instead of any lists of ordered elements. This is really just to make definitions and proofs simpler. Generalization may be done as an exercise.

Now with those definitions, we can prove our first and easiest-to-prove algorithm.

Insertion sort

We define insertion sort as a right fold:

Fixpoint insert (i : nat) (l : list nat) :=
  match l with
  | []     => [i]
  | h :: t => if leb i h then i :: h :: t else h :: insert i t
  end.

Definition insertion_sort := fold_right insert [].
(* begin hide *)
Hint Unfold insertion_sort.
(* end hide *)

Now if we could show that insert h t on list h :: t returns a permutation, we could easily show that insertion sort returns a permutation, because all it does is to call insert on list elements, using fold_right.

(** ***** Exercise: 1 star. *)
Lemma insert_perm : forall h t, Permutation (insert h t) (h :: t).
(* begin hide *)
Proof.
  intros. induction t as [|h' t']; auto.
  simpl. destruct (leb h h'); auto.
  apply perm_trans with (h' :: h :: t'); auto. apply perm_swap.
Qed.
(* end hide *)

(** *****
  Exercise: 2 stars.
  Use [insert_perm] and transitivity, symmetry and reflexivity of [Permutation]. *)
Theorem Permutation_insertion_sort: forall l, Permutation l (insertion_sort l).
(* begin hide *)
Proof.
  intros. induction l as [|h t]; auto.
  assert (Permutation (h :: t) (h :: insertion_sort t)); auto.
  simpl. rewrite H. rewrite insert_perm. reflexivity.
Qed.
(* end hide *)

To show that it returns sorted, we use a similar approach. We first show that if sorted l, then sorted (insert e l). Empty and singleton lists are sorted by definition. Using these facts, we can easily prove that insertion sort really return sorted.

(** *****
  Exercise: 2 star.
  You need to use some lemmas about [leb] that are already included. Use [SearchAbout leb]. *)
Lemma insert_sorted_preserve : forall e l,
  sorted l -> sorted (insert e l).
(* begin hide *)
Proof.
  intros e l h. induction h; simpl; auto with *.
  + remember (leb e e0) as bh. symmetry in Heqbh. destruct bh.
    - apply leb_complete in Heqbh. auto.
    - apply leb_complete_conv in Heqbh. auto with *.
  + simpl. remember (leb e e0) as bh. symmetry in Heqbh. destruct bh.
     - apply leb_complete in Heqbh. auto.
     - remember (leb e h) as bh'. symmetry in Heqbh'. destruct bh'.
       * apply leb_complete in Heqbh'. apply leb_complete_conv in Heqbh. auto with *.
       * apply leb_complete_conv in Heqbh. constructor; auto.
         simpl in IHh. rewrite Heqbh' in IHh. apply IHh.
Qed.
Hint Resolve insert_sorted_preserve.
(* end hide *)

(** ***** Exercise: 2 star. Use [insert_sorted_preserve]. *)
Theorem insertion_sort_sorted : forall l, sorted (insertion_sort l).
(* begin hide *)
Proof.
  intros. induction l as [|h t]; simpl; auto.
Qed.
(* end hide *)

With permutation and sorted properties proved, we can show that our insertion sort implementation is correct:

Theorem insertion_sort_correct : Sorting_correct insertion_sort.
Proof.
  constructor. split. apply insertion_sort_sorted. apply Permutation_insertion_sort.
Qed.

Selection sort

Next, we move to selection sort. This one is significantly harder and most stuff we define in this section will be used in the next section.

Before implementing the algorithm, we need some auxiliary functions. find_min_idx is both used in selection sort and pancake sort. As you can imagine from the name, it returns index of one of the smallest elements in a list.

Note that it’s very very hard to reason about this definition. The reason is that we’re using index of a list, instead of head/tail of it. Simple induction-based proofs that we do before simply don’t work on this definition.

Fixpoint find_min_idx_aux (l : list nat) (min min_idx cur_idx : nat) : nat :=
  match l with
  | []     => min_idx
  | h :: t => if leb h min then find_min_idx_aux t h cur_idx (S cur_idx)
                           else find_min_idx_aux t min min_idx (S cur_idx)
  end.

Definition find_min_idx (l : list nat) : nat :=
  match l with
  | []     => 0
  | h :: t => find_min_idx_aux t h 0 1
  end.

An invariant of find_min_idx:

(** ***** Exercise: 1 star. *)
Lemma find_min_idx_len_inv : forall l m mi ci r,
  find_min_idx_aux l m mi ci = r ->
  mi < ci ->
  r < ci + length l.
(* begin hide *)
Proof.
  induction l as [|h t].
  + intros. simpl in H. omega.
  + intros. simpl in *. destruct (leb h m); apply IHt in H; omega.
Qed.
(* end hide *)

Make sure you understand what it’s saying. We need this lemma to eliminate some impossible cases in proofs.

We also need a “membership” predicate. This is used to express the idea of “for all elements in the list …”, which is expressed in Coq like forall e, member e l -> ....

Inductive member {A} : A -> list A -> Prop :=
| Member_head : forall e l, member e (e :: l)
| Member_tail : forall e h t, member e t -> member e (h :: t).
(* begin hide *)
Hint Constructors member.
(* end hide *)

Again, convince yourself that this really expresses that idea. Here’s a property of member:

(** ***** Exercise: 1 star. *)
Lemma member_preserved_by_perm : forall A (l : list A) l' e,
  Permutation l l' ->
  member e l ->
  member e l'.
(* begin hide *)
Proof.
  intros A l l' e H. induction H; auto.
  + intro. inversion H0; auto.
  + intro. inversion H; auto. inversion H2; auto.
Qed.
(* end hide *)

Now using member, we can express correctness of find_min_idx and prove it. Note that this is a very hard exercise. I couldn’t solve it for a week, and even after that period I couldn’t solve it without help from Coq IRC channel. Feel free to cheat by looking the source of this post.

(* begin hide *)
Lemma find_min_idx_aux_ret_ge_mi :
  forall l m mi ci r,
    find_min_idx_aux l m mi ci = r ->
    mi <= ci ->
    mi <= r.
Proof.
  induction l as [|h t].
  + intros. simpl in H. omega.
  + intros. simpl in H. destruct (leb h m); apply IHt in H; omega.
Qed.

Lemma find_min_idx_aux_correct_same :
  forall l m mi ci,
    mi < ci ->
    find_min_idx_aux l m mi ci = mi ->
    forall e,
      member e l ->
      m <= e.
Proof.
  intro. remember (length l) as len. generalize dependent l. induction len as [|len'].
  + intros. destruct l. inversion H1. inversion Heqlen.
  + intros.
    (* l should be in form h :: t with length t = len' *)
    destruct l as [|h t]; inversion Heqlen; clear Heqlen.

    simpl in H0. destruct (leb h m) eqn: eq.
    - pose proof (find_min_idx_aux_ret_ge_mi t h ci (S ci) mi H0).
      assert (ci <= S ci) by omega. apply H2 in H4. omega.
    - inversion_clear H1.
      * apply leb_complete_conv in eq. omega.
      * apply IHlen' with (l := t) (mi := mi) (ci := S ci); auto.
Qed.

Lemma find_min_idx_aux_cases :
  forall l r m mi ci,
    find_min_idx_aux l m mi ci = r ->
    r = mi \/ ci <= r.
Proof.
  induction l as [|h t].
  + intros. simpl in H. omega.
  + intros. simpl in H. destruct (leb h m) eqn: eq.
    - apply IHt in H. inversion H; right; omega.
    - apply IHt in H. inversion H; auto. right. omega.
Qed.

Lemma find_min_idx_aux_correct_succ_le_min :
  forall l n m mi ci,
    find_min_idx_aux l m mi ci = n + ci ->
    mi < ci ->
    nth n l 0 <= m.
Proof.
  induction l as [|h t].
  + intros. destruct n; simpl; omega.
  + intros. simpl in H. destruct (leb h m) eqn: eq.
    - destruct n as [|n'].
      * apply leb_complete in eq. auto.
      * simpl. apply leb_complete in eq.
        subst.  pose proof (IHt n' h ci (S ci)).
        assert (S n' + ci = n' + S ci) by omega.
        rewrite H2 in H. apply H1 in H; omega.
    - destruct n as [|n'].
      * apply find_min_idx_aux_cases in H. inversion H; omega.
      * simpl. apply IHt with (mi := mi) (ci := S ci); omega.
Qed.

Lemma find_min_idx_aux_correct_succ :
  forall l n m mi ci,
    find_min_idx_aux l m mi ci = n + ci ->
    mi < ci ->
    forall e,
      member e l ->
      nth n l 0 <= e.
Proof.
  induction l as [|h t].
  + intros. inversion H1.
  + intros. simpl in H. destruct (leb h m) eqn: eq.
    - inversion_clear H1.
      * simpl. destruct n as [|n']. reflexivity.
        apply find_min_idx_aux_correct_succ_le_min with (mi := ci) (ci := S ci); omega.
      * simpl. destruct n as [|n'].
        { apply find_min_idx_aux_correct_same with (l := t) (mi := ci) (ci := S ci);
          try omega; auto. }
        { apply IHt with (m := h) (mi := ci) (ci := S ci); try omega; auto. }
    - inversion_clear H1.
      * simpl. destruct n as [|n']. reflexivity.
        assert (S n' + ci = n' + S ci) by omega. rewrite H1 in H; clear H1.
        pose proof (find_min_idx_aux_correct_succ_le_min t n' m mi (S ci) H).
        assert (mi < S ci) by omega. apply H1 in H2; clear H1.
        SearchAbout leb. apply leb_complete_conv in eq. omega.
      * simpl. destruct n as [|n'].
        { simpl in H. pose proof (find_min_idx_aux_cases t ci m mi (S ci) H).
          inversion H1; omega. }
        { apply IHt with (m := m) (mi := mi) (ci := S ci); try omega; auto. }
Qed.
(* end hide *)
(** ***** Exercise: 5 stars. [find_min_idx] really returns index of smallest element. *)
Lemma find_min_idx_correct : forall n l,
  find_min_idx l = n ->
  (forall e, member e l -> nth n l 0 <= e).
(* begin hide *)
Proof.
  destruct l as [|h t].
  + intros. inversion H0.
  + intros. destruct n as [|n'].
    - simpl in H. simpl. inversion H0.
      * reflexivity.
      * apply find_min_idx_aux_correct_same with (l := t) (mi := 0) (ci := 1); auto.
    - simpl in H. simpl. inversion_clear H0.
      * apply find_min_idx_aux_correct_succ_le_min with (mi := 0) (ci := 1); omega.
      * apply find_min_idx_aux_correct_succ with (m := h) (mi := 0) (ci := 1); try omega; auto.
Qed.
(* end hide *)

Now, in selection sort, we run several operations on argument. One of them is find_min_idx which we already defined. Another one of them is replace operation, which replaces nth element in a list with given element. Here’s a definition and some properties:

Fixpoint replace {A} (l : list A) (idx : nat) (e : A) : list A :=
  match l with
  | [] => []
  | h :: t =>
      match idx with
      | 0 => e :: t
      | S idx' => h :: replace t idx' e
      end
  end.

(** ***** Exercise: 1 star. First part of correctness proof of [replace]. *)
Lemma replace_nth : forall l i e l',
  i < length l ->
  replace l i e = l' ->
  nth i l' 0 = e.
(* begin hide *)
Proof.
  induction l as [|h t]; intros.
  + inversion H.
  + simpl in *. destruct i as [|i']; subst; auto.
    - apply lt_S_n in H. simpl. apply IHt; auto.
Qed.
(* end hide *)

(** ***** Exercise: 1 star.
    Second part of correctness proof of [replace]. [replace] preserves length of the list. *)
Lemma replace_len : forall A l i (e : A),
  i < length l ->
  length l = length (replace l i e).
(* begin hide *)
Proof.
  induction l as [|h t]; intros.
  + inversion H.
  + simpl in *. destruct i as [|i']; subst; auto.
    - simpl. f_equal. apply IHt with (i := i') (e := e); auto; omega.
Qed.
(* end hide *)

Using replace, we can define selection_sort. Note that our naive implementation doesn’t convince Coq that it terminates on all input. An easy workaround is to add a step parameter. Observing that selection sort algorithm terminates in length l steps, where l is the input, we can define this:

Fixpoint selection_sort_aux (l : list nat) (step : nat) : list nat :=
  match step with
  | 0       => l
  | S step' =>
      match l with
      | []     => []
      | h :: t =>
          match find_min_idx_aux t h 0 1 with
          | 0     => h :: selection_sort_aux t step'
          | S min => nth min t 0 :: selection_sort_aux (replace t min h) step'
          end
      end
  end.

Definition selection_sort (l : list nat) : list nat := selection_sort_aux l (length l).
(* begin hide *)
Hint Unfold selection_sort.
(* end hide *)

We have all we need to prove permutation property. It’s still not easy though. I’m putting an extra lemma here as a tip.

(* begin hide *)
Lemma perm_cons_inside : forall A (a : A) b c d e,
  Permutation (a :: b) (c :: d) ->
  Permutation (a :: e :: b) (c :: e :: d).
Proof.
  intros.
  assert (Permutation (e :: a :: b) (a :: e :: b)) by constructor.
  rewrite <- H0.
  assert (Permutation (c :: e :: d) (e :: c :: d)) by constructor.
  rewrite H1. auto.
Qed.
(* end hide *)
(** ***** Exercise: 2 stars. *)
Lemma replace_perm_head : forall n h t,
  n < length t ->
  Permutation (h :: t) (nth n t 0 :: replace t n h).
(* begin hide *)
Proof.
  induction n as [|n'].
  + intros. destruct t; simpl in *. omega. constructor.
  + intros. destruct t as [|th tt]. inversion H.
    assert (n' < length tt). { simpl in H. omega. } clear H. simpl.
    pose proof IHn' h tt H0.
    apply perm_cons_inside. assumption.
Qed.
(* end hide *)

(** ***** Exercise: 3 stars. Use [replace_perm_head]. *)
Theorem Permutation_selection_sort : forall l, Permutation l (selection_sort l).
(* begin hide *)
Proof.
  intro. remember (length l) as len. generalize dependent l.
  induction len as [|len']; intros; destruct l; auto; inversion Heqlen; clear Heqlen.
  unfold selection_sort in *. simpl. destruct (find_min_idx_aux l n 0 1) as [|n'] eqn: ret; auto.

  (* selection sort on (replace l n' n) should return a permutation *)
  pose proof IHlen' (replace l n' n).
  (* .. but to show that, we first need to show that (replace l n' n) has same length with l.
     to be able to use [replace_len], we need to show [n' < length l] *)
  apply find_min_idx_len_inv in ret. simpl in *. rewrite <- H0 in ret.
  assert (n' < length l) by omega; clear ret.
  (* now we know [n' < length l], we can show [length (replace l n' n) = length l]. *)
  pose proof replace_len nat l n' n H1. assert (len' = length (replace l n' n)) by omega.
  (* show that recursive call returns a permutation *)
  apply H in H3.

  assert (Permutation (nth n' l 0 :: selection_sort_aux (replace l n' n) (length l))
                      (nth n' l 0 :: replace l n' n)).
  { apply perm_skip. rewrite H2. rewrite <- H3. reflexivity. }

  rewrite H4. apply replace_perm_head. auto. auto.
Qed.
(* end hide *)

Proving sorted property is again, not easy. I’m putting some lemmas as pointers. Lemmas are very easy to prove, leaving only the master theorem as a challange.

(** ***** Exercise: 1 star. *)
Lemma member_replace : forall A l i (x y : A),
  member x (replace l i y) ->
  x = y \/ member x l.
(* begin hide *)
Proof.
  intros A l. induction l as [|h t].
  + intros. inversion H.
  + intros. destruct i as [|i']; simpl in *; inversion H; auto.
    subst. pose proof IHt i' x y H2. inversion H0; auto.
Qed.
(* end hide *)

(** ***** Exercise: 2 stars. Use [member_replace] and [find_min_idx_correct]. *)
Lemma swap_min_replace : forall h t min_idx,
  find_min_idx (h :: t) = S min_idx ->
  (forall e, member e (replace t min_idx h) -> nth min_idx t 0 <= e).
(* begin hide *)
Proof.
  intros.
  pose proof H0. apply member_replace in H0.
  pose proof H. apply find_min_idx_correct with (e := e) in H2; auto.
  inversion H0; subst; auto.
Qed.
(* end hide *)

(** ***** Exercise: 1 star. *)
Lemma sorted_min_tail : forall h t,
  sorted t ->
  (forall e, member e t -> h <= e) ->
  sorted (h :: t).
(* begin hide *)
Proof.
  intros. destruct t as [|ht tt]; auto.
Qed.
(* end hide *)

(** ***** Exercise: 2 stars. Use [member_preserved_by_perm]. *)
Lemma min_preserved_by_perm : forall m l l',
  Permutation l l' ->
  (forall e, member e l -> m <= e) ->
  (forall e, member e l' -> m <= e).
(* begin hide *)
Proof.
  intros m l l' H. induction H; intros; auto.
  + apply H0. apply member_preserved_by_perm with (l' := x :: l) in H1.
    - apply H1.
    - constructor. apply Permutation_sym in H. apply H.
  + apply member_preserved_by_perm with (l' := y :: x :: l) in H0. auto. constructor.
Qed.
(* end hide *)


(** ***** Exercise: 4 stars. Selection sort returns sorted. *)
Theorem selection_sort_sorted : forall l, sorted (selection_sort l).
(* begin hide *)
Proof.
  intro. remember (length l) as len. generalize dependent l.
  induction len as [|len']; intros; destruct l; inversion Heqlen; clear Heqlen; auto.
  unfold selection_sort. simpl. remember (find_min_idx_aux l n 0 1) as min_idx.
  destruct min_idx as [|min_idx'].
  + symmetry in Heqmin_idx.
    assert (0 < 1) by omega. pose proof find_min_idx_aux_correct_same l n 0 1 H Heqmin_idx.
    apply sorted_min_tail. apply IHlen'. apply H0.
    apply min_preserved_by_perm with (l := l). apply Permutation_selection_sort. apply H1.

  + symmetry in Heqmin_idx. pose proof swap_min_replace.
    unfold find_min_idx in H. pose proof H n l min_idx' Heqmin_idx. clear H.

    assert (length l = length (replace l min_idx' n)).
    { apply replace_len. apply find_min_idx_len_inv in Heqmin_idx; omega. }

    assert (sorted (selection_sort_aux (replace l min_idx' n) (length l))).
    { unfold selection_sort in IHlen'.
      rewrite H. apply IHlen'. rewrite H0. apply replace_len.
      apply find_min_idx_len_inv in Heqmin_idx; omega.
    }

    assert (Permutation (replace l min_idx' n)
                        (selection_sort_aux (replace l min_idx' n) (length l))).
    { rewrite H. apply Permutation_selection_sort. }

    apply sorted_min_tail. auto. intros.

    pose proof min_preserved_by_perm
                (nth min_idx' l 0)
                (replace l min_idx' n)
                (selection_sort_aux (replace l min_idx' n) (length l)) H3 H1. auto.
Qed.
(* end hide *)

(** ***** Exercise: 1 star. Show that selection sort is correct. *)
Theorem selection_sort_correct : Sorting_correct selection_sort.
(* begin hide *)
Proof.
  constructor. intros. split. apply selection_sort_sorted. apply Permutation_selection_sort.
Qed.
(* end hide *)

Pancake sort

This is getting harder and harder. We’ll define pancake sort in terms of rev_at which reverses a list at given index and map_rest which is like map, but applies the function to the rest of the list.

Fixpoint rev_at {A} idx (l : list A) : list A :=
  match idx with
  | 0      => rev l
  | S idx' =>
      match l with
      | []     => []
      | h :: t => h :: rev_at idx' t
      end
  end.

Fixpoint map_rest_aux {A} (l : list A) (f : list A -> list A) (timeout : nat) : list A :=
  match timeout with
  | 0 => l
  | S timeout' =>
      match f l with
      | [] => []
      | h :: t => h :: map_rest_aux t f timeout'
      end
  end.

Definition map_rest {A} (l : list A) (f : list A -> list A) : list A :=
  map_rest_aux l f (length l).

Two things to note: 1) rev_at returns the original list if idx is larger than length l - 1. 2) map_rest only works as expected if f preserves length of it’s argument in it’s return value.

There’s a very useful property that we need to show before showing that pancake sort returns a permutation: if f l returns a permutation, than map_rest l f returns a permutation:

(** ***** Exercise: 2 stars. *)
Lemma Permutation_map_rest :
  forall A (f : list A -> list A),
  (forall (l : list A), Permutation l (f l)) ->
  (forall (l : list A), Permutation l (map_rest l f)).
(* begin hide *)
Proof.
  intros. remember (length l) as n. symmetry in Heqn. generalize dependent l. induction n as [|n'].
  + intros. destruct l. constructor. inversion Heqn.
  + intros. destruct l.
    - inversion Heqn.
    - inversion Heqn; clear Heqn.
      unfold map_rest. simpl. destruct (f (a :: l)) as [|h t] eqn: Heqret.
      * pose proof H (a :: l). rewrite Heqret in H0. apply H0.
      * pose proof H (a :: l). rewrite Heqret in H0.
        apply Permutation_trans with (l   := a :: l)
                                     (l'  := h :: t)
                                     (l'' := h :: map_rest_aux t f (length l)); auto.
        apply perm_skip. unfold map_rest in IHn'.
        apply Permutation_length in H0. inversion H0. rewrite H3.
        apply IHn' with (l := t).
        rewrite <- H3. apply H1.
Qed.
(* end hide *)

Using this definition we can define pancake sort:

Definition flip_pancakes (l : list nat) : list nat :=
  let min_idx := find_min_idx l in
  rev_at 0 (rev_at min_idx l).

Definition pancake_sort (l : list nat) : list nat := map_rest l flip_pancakes.

Showing permutation property is actually very easy. All we need is two simple lemmas:

(** ***** Exercise: 2 stars. Use already included standard permutation lemmas. *)
Lemma Permutation_rev_at : forall A n (l : list A),
  Permutation l (rev_at n l).
(* begin hide *)
Proof.
  intros. generalize dependent n. induction l.
  + destruct n; constructor.
  + destruct n as [|n'].
    - simpl. rewrite Permutation_cons_append. apply Permutation_app_tail. apply Permutation_rev.
    - simpl. apply Permutation_cons. apply IHl.
Qed.
(* end hide *)

(** ***** Exercise: 2 stars. Use transitivity of permutation and [Permutation_rev_at]. *)
Lemma Permutation_flip_pancakes : forall l, Permutation l (flip_pancakes l).
(* begin hide *)
Proof.
  intro. unfold flip_pancakes.
  apply perm_trans with
    (l   := l)
    (l'  := rev_at (find_min_idx l) l)
    (l'' := rev_at 0 (rev_at (find_min_idx l) l)); apply Permutation_rev_at.
Qed.
(* end hide *)

(** ***** Exercise: 1 star. Use [Permutation_flip_pancakes]. *)
Theorem Permutation_pancake_sort : forall l, Permutation l (pancake_sort l).
(* begin hide *)
Proof.
  intros. induction l as [|h t].
  + auto.
  + unfold pancake_sort. unfold map_rest. apply Permutation_map_rest.
    intros. apply Permutation_flip_pancakes.
Qed.
(* end hide *)

Now the hard part. I needed a lot of lemmas for showing sorted property. I’m listing lemmas I used in no particular order.

(** ***** Exercise: 2 stars.
    Smallest element is still smallest in a permutation.
    I found this a bit tricky. You may need to use another lemma we defined. *)
Lemma min_permutation : forall e l,
  (forall e', member e' l -> e <= e') ->
  (forall l', Permutation l l' ->
    (forall e', member e' l' -> e <= e')).
(* begin hide *)
Proof.
  (* tricky part is to see what lemma do you need *)
  intros. apply member_preserved_by_perm with (l' := l) in H1.
  + auto.
  + apply Permutation_sym in H0. apply H0.
Qed.
(* end hide *)

(** ***** Exercise: 1 star. [flip_pancakes] preserves the length. *)
Theorem flip_pancakes_len : forall l, length l = length (flip_pancakes l).
(* begin hide *)
Proof.
  intros. apply Permutation_length. apply Permutation_flip_pancakes.
Qed.
(* end hide *)

(* begin hide *)
Lemma rev_at_1 : forall A n (l : list A),
  rev_at n l = firstn n l ++ rev (skipn n l).
Proof.
  intros. generalize dependent n. induction l as [|h t].
  + intros. destruct n; auto.
  + intros. destruct n as [|n'].
    - reflexivity.
    - simpl. f_equal. apply IHt.
Qed.

Lemma skipn_head : forall n l h t,
  skipn n l = h :: t -> nth n l 0 = h.
Proof.
  intros n l. generalize dependent n. induction l.
  + intros. destruct n; inversion H.
  + intros. destruct n as [|n'].
    - simpl in *. inversion H. reflexivity.
    - simpl in *. apply IHl with (t := t). apply H.
Qed.

Lemma skipn_list : forall A n (l : list A),
  n < length l ->
  exists h t, skipn n l = h :: t.
Proof.
  intros. generalize dependent n. induction l.
  + intros. destruct n; inversion H.
  + intros. destruct n.
    - eexists. eexists. simpl. auto.
    - assert (n < length l). { inversion H; omega. }
      pose proof IHl n H0. inversion H1. inversion H2. exists x. exists x0. auto.
Qed.
(* end hide *)

(** ***** Exercise: 4 stars.
    We can use [rev_at] to move smallest element to the end of the list,
    and then to the beginning of the list. Very tricky. Feel free to cheat. *)
Lemma rev_at_n : forall n l h t,
  n < length l ->
  rev_at 0 (rev_at n l) = h :: t ->
  h = nth n l 0.
(* begin hide *)
Proof.
  intros. rewrite rev_at_1 in H0. simpl in H0. rewrite rev_at_1 in H0.
  rewrite rev_app_distr in H0. rewrite rev_involutive in H0.
  (* [skipn n l] should be in form [a :: b]. *)
  pose proof skipn_list nat n l H. inversion_clear H1. inversion_clear H2. rewrite H1 in H0.
  assert (x = h). { simpl in H0. inversion H0. reflexivity. }
  subst. pose proof skipn_head n l h x0 H1. auto.
Qed.
(* end hide *)

(* begin hide *)
Lemma find_min_idx_len : forall n l,
  find_min_idx l = n ->
  l = [] \/ n < length l.
Proof.
  intros. induction l as [|h t].
  + auto.
  + right. simpl in *. pose proof find_min_idx_len_inv t h 0 1 n H. auto.
Qed.
(* end hide *)

(** ***** Exercise: 3 stars. [flip_pancakes] moves smallest element to the head of the list. *)
Lemma flip_pancakes_min : forall l h' t',
  flip_pancakes l = h' :: t' ->
  (forall e', member e' t' -> h' <= e').
(* begin hide *)
Proof.
  intros.
  pose proof (Permutation_flip_pancakes l). rewrite H in H1.
  unfold flip_pancakes in H. apply rev_at_n in H.
  + remember (find_min_idx l) as min.
    symmetry in Heqmin. pose proof (find_min_idx_correct min l Heqmin).
    pose proof (min_preserved_by_perm (nth min l 0) l (h' :: t') H1 H2). rewrite <- H in H3. auto.
  + destruct l. apply Permutation_nil in H1. inversion H1.
    pose proof find_min_idx_len (find_min_idx (n :: l)) (n :: l).
    assert (find_min_idx (n :: l) = find_min_idx (n :: l)) by reflexivity.
    apply H2 in H3. inversion H3.
    - inversion H4.
    - omega.
Qed.
(* end hide *)

(** ***** Exercise: 4 stars.
    You need a lot of lemmas we defined before, and it's a very long proof.
    Still not as hard as [find_min_idx_correct]. *)
Theorem pancake_sorted : forall l, sorted (pancake_sort l).
(* begin hide *)
Proof.
  intro. remember (length l) as len. generalize dependent l. induction len.
  + intros. destruct l. constructor. inversion Heqlen.
  + intros. destruct l as [|h t].
    - inversion Heqlen.
    - unfold pancake_sort in *. unfold map_rest in *. simpl.
      destruct (flip_pancakes (h :: t)) eqn: ret.
      * pose proof (flip_pancakes_len (h :: t)). rewrite ret in H. inversion H.
      * (* clean up the goal a bit, we want `sorted (n :: pancake_sort l)` *)
        assert (length l = length t) as leq.
        { pose proof (flip_pancakes_len (h :: t)). rewrite ret in H. inversion H. reflexivity. }
        rewrite <- leq. clear leq.

        (* fold pancake_sort *)
        assert (map_rest_aux l flip_pancakes (length l) = pancake_sort l); auto.
        rewrite H. clear H.

        (* we can use inductive hypothesis to show pancake_sort l returns sorted *)
        assert (sorted (pancake_sort l)).
        { pose proof (flip_pancakes_len (h :: t)).
          rewrite ret in H. inversion H. inversion Heqlen. rewrite H1 in H2.
          pose proof (IHlen l H2). apply H0. }

        (* since n :: l = flip_pancakes (h :: t), n is smaller or equal than any element in l.
           we also know that pancake_sort returns a permutation.
           using that we can prove our goal. *)

        pose proof (flip_pancakes_min (h :: t) n l ret) as Nsmallest.

        destruct (pancake_sort l) as [|sh st] eqn: ret'.
        { constructor. }
        { (* n should be smallest in sorted version too *)
          pose proof (Permutation_pancake_sort l). rewrite ret' in H0.
          apply min_permutation with (e := n) (e' := sh) in H0.
          + constructor. assumption. omega.
          + apply Nsmallest.
          + constructor.
        }
Qed.
(* end hide *)

And finally, our master theorem:

Theorem pancake_sort_correct : Sorting_correct pancake_sort.
Proof.
  constructor. intro. split. apply pancake_sorted. apply Permutation_pancake_sort.
Qed.

Notes and lessons learned

Implementation of algorithms are not what you’d expect to have in an imperative language. Rather than mutable arrays with O(1) access, I used classic functional style, using persistent linked lists. While that doesn’t affect runtime asymptotic complexities of sorting algorithms I used, it causes a lot of redundant allocations and worse iteration performance. Even the OCaml/Haskell extractions are not usable.

Still, proving on those purely functional definitions were very hard. The reason is that once you move away from basic “induction of subterm” style proofs, proving gets very hard very fast. Specifically, I found working on indexes and accumulators very hard.

As a next step, I’m hoping to define an imperative language in Coq, like IMP of Software Foundations but with mutable arrays, and prove same algorithms defined in that language correct.

---