Require Arith.

(* 1. Quelques preliminaires, utiles pour la suite, mais ce n'est
  pas grave si vous ne comprenez pas les preuves. *)

(* au_plus est une function qui retourne le booleen true si m<=n, false sinon.
  Il s'agit d'un programme, au contraire de la relation le, qui est un predicat
  (de type nat -> nat -> Prop). *)
Fixpoint au_plus [m,n:nat] : bool :=
  Cases m of
      O => true
    | (S m') =>
      Cases n of
          O => false
	| (S n') => (au_plus m' n')
      end
  end.

Lemma choix_bool : (b:bool) b=true \/ b=false.
Proof.
  Induction b. Left . Reflexivity.
  Right . Reflexivity.
Qed.

Lemma au_plus_le_1 : (n,m:nat) (au_plus m n)=true -> (le m n).
Proof.
  Induction n. Induction m. Intro. Apply le_n.
  Simpl. Intros. Discriminate H0.
  Induction m. Intro. Apply le_O_n.
  Simpl. Intros. Apply le_n_S. Apply H. Assumption.
Qed.

Lemma au_plus_le_2 : (n,m:nat) (le m n) -> (au_plus m n)=true.
Proof.
  Induction n. Induction m. Trivial.
  Intros. Elim (le_Sn_O n0 H0).
  Induction m. Trivial.
  Intros. Simpl. Apply H. Apply le_S_n. Assumption.
Qed.

Lemma au_plus_le_3 : (n,m:nat) (au_plus m n)=false -> ~(le m n).
Proof.
  Unfold not. Intros. Rewrite (au_plus_le_2 n m H0) in H. Discriminate H.
Qed.

Lemma au_plus_le_4 : (n,m:nat) ~(le m n) -> (au_plus m n)=false.
Proof.
  Intros. Elim (choix_bool (au_plus m n)). Intro. Elim (H (au_plus_le_1 n m H0)).
  Trivial.
Qed.

Lemma au_plus_refl : (m:nat) (au_plus m m)=true.
Proof.
  Induction m; Trivial.
Qed.

Lemma au_plus_trans : (m,n,k:nat) (au_plus m n)=true -> (au_plus n k)=true ->
                            (au_plus m k)=true.
Proof.
  Intros. Apply au_plus_le_2. (Apply (le_trans m n k); Apply au_plus_le_1; Assumption).
Qed.

Lemma au_plus_total : (m,n:nat) (au_plus m n)=false -> (au_plus n m)=true.
Proof.
  Induction m. Induction n. Trivial.
  Intros. Elim (au_plus_le_3 ? ? H0 (le_O_n (S n0))).
  Induction n0. Trivial.
  Intros. Simpl. Apply H. Exact H1.
Qed.

(* De meme, egal est le programme calculant si les deux entiers en entree sont
  egaux ou non. *)
Fixpoint egal [m,n:nat] : bool :=
  Cases m n of
      O O => true
    | (S m') (S n') => (egal m' n')
    | _ _ => false
  end.

Lemma egal_1 : (m,n:nat) (egal m n)=true -> m=n.
Proof.
  Induction m. Induction n. Trivial.
  Intros. Simpl in H0. Discriminate H0.
  Induction n0. Simpl. Intro. Discriminate H0.
  Simpl. Intros. Cut n=n1. Intro. Rewrite H2. Reflexivity.
  Apply H. Assumption.
Qed.

Lemma egal_refl : (m:nat) (egal m m)=true.
Proof.
  Induction m; Trivial.
Qed.

Lemma egal_imp_au_plus : (m,n:nat) (egal m n)=true -> (au_plus m n)=true.
Proof.
  Intros. Rewrite (egal_1 m n H). Apply au_plus_refl.
Qed.

Lemma non_au_plus_imp_non_egal : (m,n:nat) (au_plus m n)=false -> (egal m n)=false.
Proof.
  Intros. Elim (choix_bool (egal m n)). Intro. Rewrite (egal_imp_au_plus m n H0) in H.
  Discriminate H.
  Trivial.
Qed.



(* 2. Les listes d'entiers *)


Inductive liste : Set :=
  nil : liste | cons : nat -> liste -> liste.


(* 3. Analyse des proprietes des listes triees *)


Fixpoint minore [x:nat; l:liste] : Prop := (* un predicat disant si x est <= a
  tous les elements de la liste l. *)
  Cases l of
      nil => True
    | (cons m l') => (au_plus x m)=true /\ (minore x l')
  end.

Fixpoint ordonnee [l : liste] : Prop := (* un predicat disant si l est une liste
  ordonnee, c'est-a-dire triee en ordre croissant. *)
  Cases l of
      nil => True
    | (cons n l') => (minore n l') /\ (ordonnee l')
  end.

Lemma minore_ordonnee_1 : (l:liste) (m:nat) (ordonnee (cons m l)) ->
      (x:nat) (au_plus x m)=true -> (minore x l).

Lemma minore_ordonnee_2 : (l:liste) (m:nat) (ordonnee (cons m l)) ->
      (x:nat) (au_plus x m)=true -> (minore x (cons m l)).

Fixpoint insere [x:nat; l:liste] : liste :=
  Cases l of
      nil => (cons x nil)
    | (cons m l') =>
      if (au_plus x m)
      then (cons x l)
      else (cons m (insere x l'))
  end.

Lemma minore_insere_1 : (l:liste) (x,m:nat)
      (au_plus m x)=true -> (minore m l) -> (minore m (insere x l)).

Lemma insere_preserve_l_ordre : (l:liste) (ordonnee l) ->
      (x:nat) (ordonnee (insere x l)).


(* 4. Analyse des nombres d'occurrences de valeurs dans les listes *)

(* Le nombre d'occurrences de x dans l est le nombre de fois ou x apparait dans l.
  On dira que l et l' ont les memes elements si tout x apparait dans les deux
  exactement le meme nombre de fois. *)

Fixpoint nombre_d_occurrences [x:nat; l:liste] : nat :=
  Cases l of
      nil => O
    | (cons m l') =>
      if (egal x m)
      then (S (nombre_d_occurrences x l'))
      else (nombre_d_occurrences x l')
  end.

Lemma nocc_insere_1 : (l:liste) (x:nat)
    (nombre_d_occurrences x (insere x l))=(S (nombre_d_occurrences x l)).

Lemma nocc_insere_2 : (l:liste) (x:nat) (m:nat)
    (egal x m)=false ->
      (nombre_d_occurrences x (insere m l))=(nombre_d_occurrences x l).

Definition memes_elements := [l,l':liste]
  (x:nat) (nombre_d_occurrences x l)=(nombre_d_occurrences x l').

Lemma memes_elements_trans : (l,l',l'':liste)
  (memes_elements l l') -> (memes_elements l' l'') -> (memes_elements l l'').

Lemma insere_preserve_les_elements_1 : (l:liste)
      (x:nat) (memes_elements (cons x l) (insere x l)).

Lemma memes_elements_cons : (l,l':liste) (memes_elements l l') ->
      (x:nat) (memes_elements (cons x l) (cons x l')).

Lemma insere_preserve_les_elements_2 : (l,l':liste)
      (memes_elements l l') -> (x:nat) (memes_elements (cons x l) (insere x l')).


(* 5. Le tri par insertion *)


(* La modelisation du tri (en fait, un vrai programme de tri, essayez
  Eval Compute in (tri (cons (3) (cons (1) (cons (2) nil)))).
  par exemple.)
   *)

Fixpoint tri [l:liste] : liste :=
  Cases l of
      nil => nil
    | (cons x l') => (insere x (tri l'))
  end.

(* La specification du tri, en deux parties:
  (tri_ordonne) le resultat du tri sur toute liste l est une liste triee;
  (tri_preserve_les_elements) le resultat du tri sur toute liste l a les memes elements que l.
*)
Lemma tri_ordonne : (l:liste) (ordonnee (tri l)).

Lemma tri_preserve_les_elements : (l:liste) (memes_elements l (tri l)).

(* Exercice: prouvez les lemmes de ce fichier dont les preuves n'ont pas ete
  donnees.  Le but est de prouver que l'implementation tri ci-dessus implemente
  la specification, a savoir que les lemmes tri_ordonne et tri_preserve_les_elements
  sont valides.

  On peut ensuite extraire une implementation prouvee du tri par les commandes:
  Require Extraction.
  Write Caml File "tri" [ tri ].

  Consultez ensuite le fichier tri.ml.  (On peut faire mieux, voir la doc
  en http://coq.inria.fr/.)
*)