(** Computer Aided Formal Reasoning (G54CFR)
    Thorsten Altenkirch

    L14 (insertion sort)

    The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Section inssort.

Set Implicit Arguments.

Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.


(* 

  insertion sort

  Our next example is sorting: we want to sort a given lists according 
  to an given order. E.g. the list

  4 :: 2 :: 3 :: 1 :: nil

  should be sorted into

  1 :: 2 :: 3 :: 4 :: nil

  We will implement and verify "insertion sort". To keep things simple 
  we will sort lists of natural numbers wrt to the <= order. First we
  implement a boolean function which comapres two numbers:
*)

Fixpoint leqb (m n : nat) {struct m} : bool :=
  match m with
  | 0 => true
  | S m => match n with 
           | 0 => false
           | S n => leqb m n
           end
  end.

Eval compute in leqb 3 4.
Eval compute in leqb 4 3.

(*
   The main function of insertion sorty is the function insert 
   which inserts a new element into an already sorted list:
*)

Fixpoint insert (n:nat)(ms : list nat) {struct ms} : list nat :=
  match ms with
  | nil => n::nil
  | m::ms' => if leqb n m
              then n::ms
              else m::(insert n ms')
  end.

Eval compute in insert 3 (1::2::4::nil).

(* Now sort builds a sorted list from any list by inserting each 
   element into the empty list.
*)

Fixpoint sort (ms : list nat) : list nat :=
  match ms with
  | nil => nil
  | m::ms' => insert m (sort ms')
  end.

Eval compute in sort (4::2::3::1::nil).

(* However, how do we know that sort will work for all lists?
   We are going to verify sort. First we have to define what 
   we mean by sorted. *)

Definition leqb_hd (n:nat)(ms : list nat) : bool :=
  match ms with
  | nil => true
  | m::ms' => leqb n m
  end.

Fixpoint sorted (ms:list nat) : bool :=
  match ms with
  | nil => true
  | m::ms' => leqb_hd m ms' && sorted ms'
  end.

Eval compute in sorted (4::2::3::1::nil).
Eval compute in sorted (sort (4::2::3::1::nil)).

(* to understand the proof, we continue with insert_lem below. When 
   trying to prove insert_lem it turns out we need the following 
   two auxilliary lemmas.
*)

Lemma leqb_total : forall m n:nat, leqb m n=false -> leqb n m = true.
induction m.
  intros.
  inversion H.
  intro n.
  case n.
  intros.
  reflexivity.
  intros.
  simpl. 
  apply IHm.
  simpl in H.
  assumption.
Qed.

Lemma insert_hd_lem : forall (a m:nat)(ms:list nat), 
  leqb_hd a ms=true -> leqb a m=true -> leqb_hd a (insert m ms) =true.
  intros a m ms.
  case ms.
    intros.
    simpl.
    assumption.
    (* cons *)
    intros n l.
    simpl.
    intros.
    case (leqb m n).
    simpl.
    assumption.
    simpl.
    assumption.
Qed.

(* insert_lem expresses that if we insert an element into a sorted 
   list, we obtain a sorted list.
*)

Lemma insert_lem : forall (m:nat)(ms:list nat), 
  sorted ms=true -> sorted (insert m ms)=true.
(* we proceed by induction over ms: *)
induction ms.
  (* case : ms = nil *)
  intros.
  simpl.
  reflexivity.
  (* case: m:ms *)
  intros.
  simpl.
  case_eq (leqb m a).
    (* leqb m a = true *)
    intros.
    change ((leqb m a) && (sorted (a::ms)) = true).
    rewrite H0.
    rewrite H.
    reflexivity.
    (* leqb m a = false *)
    intros.
    simpl.
    simpl in H.
    apply andb_true_intro.
    cut (leqb_hd a ms=true /\ sorted ms = true).
    split.
    apply insert_hd_lem.
    elim H1.
    intros.
    assumption.
    apply leqb_total.
    assumption.
    apply IHms.
    elim H1.
    intros.
    assumption.
    apply andb_prop.
    assumption.
Qed.
    
(* using the previous lemma it is easy to prove our main theorem. *)
Theorem sort_ok : forall ms:list nat,sorted (sort ms)=true.
induction ms.
  (* case ms=nil: *)
  reflexivity.
  (* case a::ms *)
  simpl.
  apply insert_lem.
  assumption.
Qed.

(* Is this enough? No, we copuld have implemented a function with the 
   property sort_ok by always returning the empty list. Another 
   important property of a sorting function is that it returns a 
   permutation of the input. We define what a permutation is. Again to 
   simplify or discussion we only do this for list nat. 
*)

(* 

   Permutations

   A list is a permutation of another list if every element appears 
   the same number of times. Hence we define the function count:
*)

Fixpoint count (n:nat)(ms:list nat) {struct ms} : nat :=
  match ms with
  | nil => 0
  | m::ms' => let cn := count n ms' 
              in if beq_nat n m then S cn else cn
  end.

Eval compute in count 1 (2::1::1::nil).
Eval compute in count 2 (2::1::1::nil).

Definition Perm (ns ms:list nat) := forall n:nat,count n ns=count n ms.

(* we establish some basic property of Perm, which will be useful 
   later: *)

Lemma refl_perm : forall ns:list nat,Perm ns ns.
unfold Perm.
intros.
reflexivity.
Qed.

Lemma trans_perm : forall ls ms ns:list nat,Perm ls ms -> Perm ms ns -> Perm ls ns.
unfold Perm.
intros.
  transitivity (count n ms).
  apply H.
  apply H0.
Qed.

Lemma cons_perm : forall (n:nat)(ms ns:list nat),Perm ms ns -> Perm (n::ms) (n::ns).
unfold Perm.
intros.
  simpl.
  rewrite H.
  case (beq_nat n0 n).
    reflexivity.
    reflexivity.
Qed.


(* Let's show that rev produces a permutation. *)

Fixpoint snoc (A:Set)(l : list A)(a : A) {struct l} : list A
  := match l with
     | nil => cons a nil
     | cons b m => cons b (snoc m a)
     end.

Fixpoint rev (A:Set)(l : list A) {struct l} : list A :=
  match l with
  | nil => nil
  | cons a m => snoc (rev m) a 
  end.

Lemma snoc_perm : forall (ns:list nat)(n:nat),Perm (n::ns) (snoc ns n).
induction ns.
  intros.
  apply refl_perm.
  (* cons *)
  unfold Perm.
  intros.
  simpl.
  unfold Perm in IHns.
  rewrite <- IHns.
  simpl.
  case (beq_nat n0 n).
    case (beq_nat n0 a).
      reflexivity.
      reflexivity.
      reflexivity.
Qed.

Lemma rev_perm : forall (ns:list nat),Perm ns (rev ns).
induction ns.
  apply refl_perm.
  simpl.
  eapply trans_perm.
  apply cons_perm.
  apply IHns.
  apply snoc_perm.
Qed.
  
(* perm for sort *)

Lemma insert_perm : forall (ns:list nat)(n:nat), Perm (n::ns) (insert n ns).
induction ns.
  intros.
  apply refl_perm.
  intros.
  simpl.
  case (leqb n a).
    apply refl_perm.
    eapply trans_perm.
    instantiate (1 := a::n::ns).
    unfold Perm.
    intros.
    simpl.
    case (beq_nat n0 n).
      case (beq_nat n0 a).
      reflexivity.
      reflexivity.
      case (beq_nat n0 a).
      reflexivity.
      reflexivity.
    apply cons_perm.
    apply IHns.
Qed.

Theorem sort_perm : forall ms:list nat,Perm ms (sort ms).
induction ms.
  apply refl_perm.
  eapply trans_perm.
    apply cons_perm.
    apply IHms.
    simpl.
    apply insert_perm.
Qed.