Require Import List.
Require Import Arith.

Definition sorted (l:list nat) :=
  forall l1 l2 x1 x2, l = l1 ++ x1::x2::l2 -> x1 <= x2.

Lemma s1 : sorted nil.
Proof.
 intros l1 l2 x1 x2 H; destruct l1; discriminate H.
Qed.

Lemma s2 : forall a, sorted (a::nil).
Proof.
 intros a l1 l2 x1 x2 H; destruct l1 as [ | n l1']; try discriminate H.
 destruct l1' as [ | l1'']; simpl in H; try discriminate H.
Qed.

Lemma s3 : forall a b l, a <= b -> sorted (b::l) -> sorted (a::b::l).
Proof.
intros a b l ab s l1 l2 x1 x2 H.
destruct l1 as [ | m l1'].
injection H; intros; subst a b l; auto.
injection H; clear H; intros H Ha; subst a.
unfold sorted in s; apply s with (1:=H); auto.
Qed.

Lemma s_le : forall a b l, sorted (a::b::l) -> a <= b.
Proof.
intros a b l H; apply (H nil l a b); auto.
Qed.

Lemma s_s_tail : forall a b l, sorted (a::b::l) -> sorted (b::l).
Proof.
intros a b l s l1 l2 x1 x2 q; apply (s (a::l1) l2 x1 x2); rewrite q; auto.
Qed.

Check leb_correct.
Check leb_complete.
Check leb_complete_conv.
Check leb_correct_conv.

Fixpoint insert (n:nat)(l:list nat) {struct l} : list nat :=
  match l with
    nil => n::nil
  | a::tl => if leb a n then a::insert n tl else n::a::tl
  end.

Fixpoint sort (l:list nat) : list nat :=
  match l with
    nil => nil
  | a::tl => insert a (sort tl)
  end.

Lemma insert_sorted : forall n l, sorted l -> sorted (insert n l).
Proof.
intros n l;
  assert ((sorted l -> sorted (insert n l)) /\ 
          forall a, sorted (a::l) -> sorted (insert n (a::l))).
elim l.
split; simpl; [intros _; apply s2 | intros a _].
generalize (leb_complete a n)(leb_complete_conv n a); case (leb a n).
intros an _; apply s3; auto; apply s2.
intros _ na; apply s3; try apply lt_le_weak; auto; apply s2.
clear l; intros m l [IH1 IH2]; split.
intros sml; apply IH2; auto.
intros p spml; simpl.
generalize (leb_complete p n)(leb_complete_conv n p); case (leb p n).
intros pn _; generalize (IH2 m); simpl.
case (leb m n); intros IH2'; apply s3; auto.
apply s_le with (1:= spml); trivial.
apply IH2'; apply s_s_tail with (1:=spml).
apply IH2'; apply s_s_tail with (1:=spml).
intros _ np; apply s3; auto.
apply lt_le_weak; auto.
elim H; auto.
Qed.

Lemma sort_sorted : forall l, sorted (sort l).
Proof.
intros l; elim l;
  [ simpl; apply s1 | simpl; intros a l' IHl'; apply insert_sorted; auto].
Qed.

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

Lemma nat_eq_bool_complete :
  forall n m, nat_eq_bool n m = true -> n = m.
Proof.
intros n; elim n; [intros m; case m |clear n; intros n IHn m; case m];
 try (simpl; auto; intros; discriminate).
Qed.

Lemma nat_eq_bool_complete_conv :
  forall n m, nat_eq_bool n m = false -> n <> m.
Proof.
intros n; elim n; [intros m; case m |clear n; intros n IHn m; case m];
 try (simpl; auto; intros; discriminate).
Qed.

Fixpoint count (n:nat)(l:list nat) {struct l} : nat :=
  match l with
    nil => 0
  | a::tl => if  nat_eq_bool n a then 1 + count n tl else count n tl
  end.

Definition permutation (l1 l2: list nat) : Prop :=
  forall n, count n l1 = count n l2.

Lemma permutation_trans :
  forall l1 l2 l3, permutation l1 l2 -> permutation l2 l3 -> permutation l1 l3.
Proof.
unfold permutation; intros l1 l2 l3 p12 p23 n; transitivity (count n l2); auto.
Qed.

Lemma permutation_refl :
  forall l, permutation l l.
Proof.
unfold permutation; auto.
Qed.

Lemma permutation_sym :
  forall l1 l2, permutation l1 l2 -> permutation l2 l1.
Proof.
unfold permutation; intros l1 l2 p12 n;auto.
Qed.

Lemma permutation_cons :
  forall a l1 l2, permutation l1 l2 -> permutation (a::l1) (a::l2).
Proof.
unfold permutation; intros a l1 l2 p12 n; simpl.
case (nat_eq_bool n a); auto.
Qed.

Lemma permutation_cons2 :
  forall a b l, permutation (a::b::l) (b::a::l).
Proof.
unfold permutation; intros a b l n; simpl.
case (nat_eq_bool n b); case (nat_eq_bool n a); auto.
Qed.

Lemma insert_permutation :
  forall n l, permutation (insert n l) (n::l).
Proof.
intros n l; elim l.
simpl; apply permutation_refl.
intros a l' IHl'; simpl; case (leb a n).
apply permutation_trans with (a::n::l').
apply permutation_cons; auto.
apply permutation_cons2.
apply permutation_refl.
Qed.

Lemma sort_permutation :
  forall l, permutation (sort l) l.
Proof.
intros l; elim l; simpl; [apply permutation_refl | intros a l' IHl'].
apply permutation_trans with (a::sort l').
apply insert_permutation.
apply permutation_cons; auto.
Qed.