qsort-like verifying

Require Import Arith omega.Omega Lists.List.
Import ListNotations.

Fixpoint ble_nat (n m : nat) : bool :=
 match n with
 | 0    => true
 | S n' =>
    match m with
    | 0    => false
    | S m' => ble_nat n' m'
    end
 end.

Theorem fold_ble_nat_S : forall n m,
 ble_nat (S n) m = match m with | 0 => false| S m' => ble_nat n m' end.
Proof. reflexivity. Qed.

Theorem le_ble_nat_true : forall n m,
 n <= m <-> ble_nat n m = true.
Proof.
 intros. split; generalize dependent m; induction n; intros.
    inversion H; auto.
    destruct m. 
       inversion H.
       simpl. apply IHn. omega.
    apply le_0_n.
    destruct m; inversion H.
       apply le_n_S. auto.
Qed.

Theorem not_le_ble_nat_false : forall n m,
 ~ (n <= m) <-> ble_nat n m = false.
Proof.
 unfold not. intros. split; generalize dependent m; induction n; intros.
    omega.
    destruct m; auto.
       simpl. apply IHn. omega.
    inversion H.
    destruct m.
       inversion H0.
       inversion H. apply IHn in H2; omega.
Qed.

Tactic Notation "ble_omega" :=
 intros; repeat (rewrite <- le_ble_nat_true in *); 
  repeat (rewrite <- not_le_ble_nat_false in *); omega. 

Ltac destruct_ble_nat :=
 repeat (rewrite <- fold_ble_nat_S);
 repeat match goal with
        | |- context [ble_nat ?n ?m] => let d := fresh "d" in destruct (ble_nat n m) eqn : d
        end;
 simpl; try ble_omega; auto.

Definition max (n m : nat) := 
 if ble_nat n m then m else n. 

Theorem max_max : forall n m,
 max n (max n m) = max n m.
Proof. unfold max. intros. destruct_ble_nat. Qed.

Theorem ble_nat_max : forall n m,
 ble_nat n (max n m) = true.
Proof. unfold max. intros. destruct (ble_nat n m) eqn : d; ble_omega. Qed.

Fixpoint maximum (l : list nat) :=
 match l with
 | []      => 0
 | x :: l' => max x (maximum l')
 end.

(*----------------------------------------------------------------------------------------------*)

Fixpoint qsort' (l : list nat) (min_n max_n : nat) :=
 match l with
 | nil     => nil
 | x :: l' =>
    if andb (ble_nat min_n x) (ble_nat (S x) max_n)
    then qsort' l' min_n x ++ [x] ++ qsort' l' x max_n
    else qsort' l' min_n max_n
 end.

Definition qsort (l : list nat) :=
 qsort' l 0 (S (maximum l)).

Theorem qsort'_refl : forall l x,
 qsort' l x x = [].
Proof. intros. induction l; simpl; destruct_ble_nat. Qed.

(*----------------------------------------------------------------------------------------------*)

Inductive forall_list (P : nat -> Prop) : list nat -> Prop :=
 | forall_list_nil  : forall_list P []
 | forall_list_step : forall l v, forall_list P l -> P v -> forall_list P (v :: l).

Definition le_all (n : nat) : list nat -> Prop :=
 forall_list (le n).

Inductive sorted : list nat -> Prop :=
 | sorted_nil  : sorted []
 | sorted_step : forall l v, sorted l -> le_all v l -> sorted (v :: l).

Definition all_le (n : nat) : list nat -> Prop :=
 forall_list (fun m => le m n).

Hint Constructors forall_list.
Hint Unfold le_all.
Hint Constructors sorted.
Hint Unfold all_le.

Hint Extern 1 => simpl.
Hint Extern 2 => ble_omega.

Theorem forall_list_impl : forall l (P Q : nat -> Prop),
 forall_list P l -> (forall n, P n -> Q n) -> forall_list Q l.
Proof. induction 1; auto. Qed.

Theorem forall_list_app : forall l1 l2 P,
 forall_list P l1 ->
 forall_list P l2 ->
 forall_list P (l1 ++ l2).
Proof. induction 1; auto. Qed.

Hint Resolve forall_list_impl.
Hint Resolve forall_list_app.

Theorem sorted_app : forall l2 l1,
 sorted l1 ->
 sorted l2 ->
 forall_list (fun n => le_all n l2) l1 ->
 sorted (l1 ++ l2).
Proof. induction 1; auto. intuition. inversion H2. auto. Qed.

Theorem le_all_step : forall l v n,
 le_all v l ->
 n <= v ->
 le_all n (v :: l).
Proof. eauto. Qed.

Hint Resolve le_all_step.

Tactic Notation "qsort_intro" :=
 intro l; induction l as [| v l']; intros; simpl; auto;
  destruct_ble_nat; unfold le_all in *; unfold all_le in *.

Theorem le_all_qsort' : forall l n m,
 le_all n (qsort' l n m).
Proof. qsort_intro. eauto. Qed.

Theorem all_le_qsort' : forall l n m,
 all_le m (qsort' l n m).
Proof. qsort_intro. Hint Extern 2 => instantiate. apply forall_list_app; eauto. Qed.

Theorem sorted_after_qsort' : forall l n m,
 sorted (qsort' l n m).
Proof. 
 generalize le_all_qsort', all_le_qsort'. intros ? ?. qsort_intro. apply sorted_app; eauto.
Qed.