Require Import List. 
Require Import Arith.
Require Import Utf8.

(*
Il y a deux parties relativement ind\u00e9pendantes :
1. ce qui concerne equiv
2. ce qui concerne insert
*)

Definition listn := (list nat).

Fixpoint sorted (l0:listn) : Prop :=
    match l0 with
    | nil => True
    | (p::l1) =>
        match l1 with
        |  nil => True
        | (q::l2) => (p<=q) /\ sorted l1
        end
    end.

Fixpoint insert (n:nat) (l:listn) {struct l} : listn :=
    match l with
    | nil => n::nil
    | p::l' => if le_gt_dec n p then n::p::l' else p::(insert n l')
    end.

Theorem sorted_inv: forall (n: nat), forall (l: listn), sorted (n::l) -> sorted l.
simpl.
intros.
destruct l.
simpl. split.
destruct H.
apply H0.
Qed.

(* si on fait le destruct trop tot avant le simpl... *)
Theorem sorted_inv_bis: forall (n: nat), forall (l: listn), sorted (n::l) -> sorted l.
intros.
destruct l.
simpl. split.
simpl in H.
destruct H.
change (sorted (n0::l)) in H0.
apply H0.
Qed.

(*
La difficult\u00e9 vient de :
1. simpl sur un (sorted (a::b::l)) rend une expression compliqu\u00e9e => faire split
2. il faut faire une preuve par cas (destruct l) OU alors prouver un
lemme "le premier elt d'une liste tri\u00e9e est plus petit que tous les autres"
*)

Lemma insert_sorted: forall n: nat, forall l: listn, sorted l -> sorted (insert n l).
induction l ; intro ; simpl.
split.
destruct le_gt_dec.
split ; [apply l0 | apply H].
destruct l ; simpl.
split ; [apply lt_le_weak ; apply g | split ].
simpl insert in IHl ; destruct le_gt_dec ; split.
apply lt_le_weak ; apply g.
apply IHl ; apply H.
apply H ; apply IHl.
apply IHl ; apply H.
Qed.


(* une autre preuve de insert_sorted avec un lemme aux... *)

Lemma aux: forall l:listn, forall p q: nat, sorted (p::l) /\ p<=q -> sorted (p::(insert q l)).
induction l.
simpl. intros. destruct H ; split.
apply H0. split.
intros.
destruct H.
simpl.
destruct (le_gt_dec q a).
split. apply H0.
simpl. split. apply l0.
change (sorted (a::l)).
apply sorted_inv with (n:=p). apply H.
split.
apply H.
apply IHl. split. apply H.
apply lt_le_weak in g. apply g.
Qed.

Lemma insert_sorted_with_aux: forall l: listn, forall n: nat, sorted l -> sorted (insert n l).
intros l x H.
destruct l.
simpl. split.
simpl.
destruct le_gt_dec.
simpl.
split. apply l0. apply H.
apply lt_le_weak in g.
apply aux.
split.
apply H.
apply g.
Qed.



Fixpoint number_of (n:nat)(l:listn) {struct l} : nat :=
    match l with
    | nil => 0
    | p::l' => if eq_nat_dec n p then (number_of n l') + 1  else number_of n l'
    end.

Definition equiv (l l': listn) : Prop := forall n:nat, number_of n l = number_of n l'.

Lemma equiv_refl: forall l: listn, equiv l l.
intro.
unfold equiv.
intro.
reflexivity.
Qed.

Lemma equiv_sym: forall l l': listn, equiv l l' -> equiv l' l.
unfold equiv.
intros.
rewrite H.
reflexivity.
Qed.


Lemma equiv_trans: forall l0 l1 l2: listn, equiv l0 l1 -> equiv l1 l2 -> equiv l0 l2.
unfold equiv.
intros.
rewrite H.
apply H0.
Qed.

Lemma equiv_cons: forall n: nat, forall l l': listn, equiv l l' -> equiv (n::l) (n::l').
intros.
intro.
simpl.
destruct eq_nat_dec with (n:=n0) (m:=n) ; rewrite H ; reflexivity.
Qed.

Lemma equiv_perm: forall (a b: nat) (l l': listn), equiv l l' -> equiv (a::b::l) (b::a::l').
intros.
intro n.
simpl.
destruct eq_nat_dec ; destruct eq_nat_dec ;
rewrite H ; reflexivity.
Qed.


Lemma insert_equiv: forall n: nat, forall l: listn, equiv (n::l) (insert n l).
induction l.
simpl. apply equiv_refl.
simpl.
destruct le_gt_dec. apply equiv_refl.
apply equiv_trans with (l1:=(a::n::l)).
apply equiv_perm. apply equiv_refl.
apply equiv_cons ; apply IHl.
Qed.






(* Theorem isort: forall l: listn, exists l': listn,  sorted l' /\ equiv l l'. *)
Theorem isort: forall l: listn, {l': listn | sorted l' /\ equiv l l'}.
intro.
induction l.
exists nil. (*  ou exists (nil (A:=nat))  si necessaire... *)
split.
simpl.
split.
apply equiv_refl.
destruct IHl as [l' H]. (* pour nommer explicitement les deux H *)
destruct H.
exists (insert a l').
split.
apply insert_sorted.
apply H.
Check equiv_trans. apply equiv_trans with (l1:=(a::l')).
apply equiv_cons.
apply H0.
apply insert_equiv.
Qed.


Extraction insert.
Extraction isort.



Eval compute in (insert 2 nil).
Eval compute in (isort (2::1::nil)).