pancake sort, selection sort and insertion sort are proven correct

gistfile1.coq

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

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).
Hint Constructors sorted.

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

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 [].
Hint Unfold insertion_sort.

Lemma insert_perm : forall h t, Permutation (insert h t) (h :: t).
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.

Theorem Permutation_insertion_sort: forall l, Permutation l (insertion_sort l).
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.

Lemma insert_sorted_preserve : forall e l,
  sorted l -> sorted (insert e l).
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.

Theorem insertion_sort_sorted : forall l, sorted (insertion_sort l).
Proof.
  intros. induction l as [|h t]; simpl; auto.
Qed.

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

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.

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.
Proof.
  induction l as [|h t].
  + intros. simpl in H. omega.
  + intros. simpl in *. destruct (leb h m); apply IHt in H; omega.
Qed.

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).
Hint Constructors member.

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

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. 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.

Lemma find_min_idx_correct : forall n l,
  find_min_idx l = n ->
  (forall e, member e l -> nth n l 0 <= e).

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.

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.

Lemma replace_nth : forall l i e l',
  i < length l ->
  replace l i e = l' ->
  nth i l' 0 = e.
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.

Lemma replace_len : forall A l i (e : A),
  i < length l ->
  length l = length (replace l i e).
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.

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).
Hint Unfold selection_sort.

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.

Lemma replace_perm_head : forall n h t,
  n < length t ->
  Permutation (h :: t) (nth n t 0 :: replace t n h).
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.

Theorem Permutation_selection_sort : forall l, Permutation l (selection_sort l).
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.

Lemma member_replace : forall A l i (x y : A),
  member x (replace l i y) ->
  x = y \/ member x l.
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.

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).
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.

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

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).
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.

Theorem selection_sort_sorted : forall l, sorted (selection_sort l).
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.

Theorem selection_sort_correct : Sorting_correct selection_sort.
Proof.
  constructor. intros. split. apply selection_sort_sorted. apply Permutation_selection_sort.
Qed.

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).

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)).
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.

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.

Lemma Permutation_rev_at : forall A n (l : list A),
  Permutation l (rev_at n l).
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.

Lemma Permutation_flip_pancakes : forall l, Permutation l (flip_pancakes l).
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.

Theorem Permutation_pancake_sort : forall l, Permutation l (pancake_sort l).
Proof.
  intros. induction l as [|h t].
  + auto.
  + unfold pancake_sort. unfold map_rest. apply Permutation_map_rest.
    intros. apply Permutation_flip_pancakes.
Qed.

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')).
Proof.
  intros. apply member_preserved_by_perm with (l' := l) in H1.
  + auto.
  + apply Permutation_sym in H0. apply H0.
Qed.

Theorem flip_pancakes_len : forall l, length l = length (flip_pancakes l).
Proof.
  intros. apply Permutation_length. apply Permutation_flip_pancakes.
Qed.

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.

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.
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.

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.

Lemma flip_pancakes_min : forall l h' t',
  flip_pancakes l = h' :: t' ->
  (forall e', member e' t' -> h' <= e').
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.

Theorem pancake_sorted : forall l, sorted (pancake_sort l).
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.

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