(* based on an example in the Coq'Art book *)

Require Import List.
Require Import Arith.
Import ListNotations.

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

Example insert1 : insert 5 [2;3;6] = [2;3;5;6].
Proof. reflexivity. Qed.

Fixpoint sort l := 
  match l with 
      [ ] => [ ] 
    | h :: t => insert h (sort t)
  end.

Example sort1 : sort [5;6;3;2] = [2;3;5;6].
Proof. reflexivity. Qed.

(* The specification *)

Inductive sorted : list nat -> Prop :=
  sort_mt : sorted [ ]
| sort_one : forall x, sorted [x]
| sort_more : forall x y l,
                x <= y
                -> sorted (y :: l)
                -> sorted (x :: y :: l).

Hint Constructors sorted: sortedbase.

(* From List module (eq_dec is an implicit parameter)

Fixpoint count_occ (l : list A) (x : A) : nat :=
  match l with
    | [] => 0
    | y :: tl =>
      let n := count_occ tl x in
        if eq_dec y x then S n else n
  end.
*) 

Definition count := count_occ Nat.eq_dec.
		   
Example count1 : count [3;2;4;5;2;2] 2 = 3.
Proof. reflexivity. Qed.

Definition permut (l1 l2 : list nat) := 
   forall x:nat, count l1 x  = count l2 x.

(* We will show:

Theorem sort_correctness :
  forall l, sorted (sort l) /\ permut l (sort l).

   Obvious helpful lemmas:

Theorem insert_correct :
  forall l x,
    sorted l -> sorted (insert x l).
    
Theorem insert_permut :
  forall l x,
    permut (x::l) (insert x l). 
*)

(* Proof of correctness *)

Lemma permut_refl : forall l, permut l l.
Proof.
  unfold permut. auto.
Qed.

Lemma permut_swap :
  forall x y l l',
    permut l l'
    -> permut (x :: y :: l) (y :: x :: l').
Proof.
  intros x y l l' H z. simpl.
  case (Nat.eq_dec x z);
    case (Nat.eq_dec y z);
     simpl; auto.
Qed.

Lemma permut_trans:
  forall l l' l'',
    permut l l'
    -> permut l' l''
    -> permut l l''.
Proof.
  unfold permut.
  intros l l' l'' H1 H2 x.
  rewrite H1. apply H2.
Qed.

Lemma permut_cons:
  forall x l l',
    permut l l' -> permut (x :: l) (x :: l').
Proof.
  intros x l l' H z. simpl.
  case (Nat.eq_dec x z); auto.
Qed.

Hint Resolve permut_refl permut_swap permut_cons: sortedbase.

Theorem insert_correct :
  forall l x,
    sorted l -> sorted (insert x l).

Proof with (auto with sortedbase arith).
  intros l x H. elim H; simpl...
  intro z. case (le_lt_dec x z)...
  intros z1 z2. case (le_lt_dec x z2); simpl; intros;
  case (le_lt_dec x z1); simpl...
Qed.

Theorem insert_permut :
  forall l x,
    permut (x::l) (insert x l). 

Proof with (auto with sortedbase).
  induction l as [| a l' IH]; simpl...
  intro x. case (le_lt_dec x a)...
  intro. apply (permut_trans _ (a :: x :: l') _)...
Qed.

Theorem sort_sorts : forall l, sorted (sort l).

Proof.
  induction l.
  - auto with sortedbase.
  - simpl. apply insert_correct; auto.
Qed.

Theorem sort_permutes : forall l, permut l (sort l).
Proof.
 induction l; simpl.
 - unfold permut. auto.
 - apply (permut_trans _ (a :: (sort l)) _).
   auto with sortedbase. apply insert_permut.
Qed.

Theorem sort_correctness :
  forall l, sorted (sort l) /\ permut l (sort l).
Proof.
  split. apply sort_sorts. apply sort_permutes.
Qed.