(* insertsort.v *)
(* Przykład zaczerpnięty z Coq'Art i troche przerobiony *)

Require Import List.
Require Import ZArith.
Open Scope N_scope.

Definition N_le_gt_dec n1 n2 := 
  Z_le_gt_dec (Z_of_N n1) (Z_of_N n2).


(**** Implementacja ****)

Fixpoint insert (z:N) (l : list N) {struct l} : list N :=
match l with
| nil => z :: nil
| a::l' => 
  match N_le_gt_dec z a with
  | left _ => z :: a :: l'
  | right _ => a :: (insert z l')
  end
end.

Fixpoint sort (l : list N) {struct l} : (list N) := 
match l with 
| nil => nil
| a::l' => insert a (sort l')
end.


(**** Testy ****)

Eval compute in (sort (5::2::7::9::0::nil)).


(**** Specyfikacja ****)

Inductive sorted : list N -> Prop :=
| sorted0 : sorted nil
| sorted1: forall z:N, sorted (z :: nil)
| sorted2: forall (z1 z2 : N) (l : list N),
    z1 <= z2 -> sorted (z2 :: l) -> sorted (z1 :: z2 :: l).

Program Definition sort' : forall l : list N, 
  {l' : list N | Permutation l l' /\ sorted l'} := sort.

Obligations.


(**** Dowód ****)

Hint Resolve sorted0 sorted1 sorted2 : sort.
Hint Resolve Nnat.Z_of_N_le_rev : sort.
(* Wstawienie elementu do posortowanej listy daje posortowaną listę. *)
Lemma insert_sorted : forall (l : list N) (x : N),
  sorted l -> sorted (insert x l).
Proof.
intros l x H; induction H as [| z | z1 z2]; simpl.

auto with sort.

destruct (N_le_gt_dec x z); auto with sort zarith.

simpl in IHsorted.
destruct (N_le_gt_dec x z2); 
destruct (N_le_gt_dec x z1); auto with sort zarith.

Qed.

Lemma sort_sorted : forall (l : list N), sorted (sort l).
Proof.
  induction l.
  auto with sort.
  simpl.
  apply insert_sorted.
  assumption.
Qed.

Hint Constructors Permutation.
Hint Resolve Permutation_refl Permutation_sym.


(* Lista powstała przez wstawienie do innej listy elementu na właściwe *)
(* miejsce jest permutacją listy powstałej z tej innej listy przez              *)
(* dołączenie wstawianego elementu na początek listy.                          *)
Lemma insert_Permutation : forall (l : list N) (x : N), 
  Permutation (x :: l) (insert x l).
Proof.
induction l as [| a l H]; simpl.
auto.
intros x.
destruct (N_le_gt_dec x a).
auto.

eauto.
Qed.

Lemma sort_Permutation : forall (l : list N), (Permutation l (sort l)).
Proof.
  induction l.
  auto.
  simpl.
  eauto using insert_Permutation.
Qed.

(* Finał: *)
Next Obligation.
Proof.
  split.
  apply sort_Permutation.
  apply sort_sorted.
Qed.

Check sort'.

Print sort'.

Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].

Recursive Extraction insert.
Extraction sort.
*)

(**** Koniec ****)