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 tas. *)

Inductive pretas : Set := V : pretas | B : pretas -> nat -> pretas -> pretas.

Fixpoint minore [n:nat; t:pretas] : Prop :=
  Cases t of
      V => True
    | (B g m d) => (au_plus n m)=true /\ (minore n g) /\ (minore n d)
  end.

Fixpoint tas [t:pretas] : Prop :=
  Cases t of
      V => True
    | (B g n d) => (minore n g) /\ (tas g) /\ (minore n d) /\ (tas d)
  end.

Fixpoint ajoute [n:nat; t:pretas] : pretas :=
  Cases t of
      V => (B V n V)
    | (B g m d) => if (au_plus n m)
                   then (B (ajoute m d) n g)
                   else (B (ajoute n d) m g)
  end.

Lemma ajoute_minore : (t:pretas) (m,n:nat) (au_plus m n)=true -> (minore m t)
                          -> (minore m (ajoute n t)).
Proof.
  Induction t. Simpl. Intros. (Split; Trivial). (Split; Trivial).
  Simpl. Intros. Elim (choix_bool (au_plus n0 n)). Intro. Rewrite H3. Simpl. Split. Assumption.
  Split. Apply H0. (Apply (au_plus_trans m n0 n); Assumption).
  Elim H2. Intros. Elim H5. Trivial.
  Elim H2. Intros. (Elim H5; Trivial).
  Intro. Rewrite H3. Simpl. Elim H2. Intros. Elim H5. Intros. Split. Assumption.
  Split. Apply H0. Assumption.
  Assumption.
  Assumption.
Qed.

Lemma au_plus_minore : (t:pretas) (m,n:nat) (au_plus m n)=true -> (minore n t)
                           -> (minore m t).
Proof.
  Induction t. Trivial.
  Simpl. Intros. Elim H2. Intros. Elim H4. Intros. Split. Apply (au_plus_trans m n0 n). Assumption.
  Assumption.
  Split. Apply H with n:=n0. Assumption.
  Assumption.
  Apply H0 with n:=n0. Assumption.
  Assumption.
Qed.

Lemma ajoute_preserve_tas : (t:pretas) (tas t) -> (n:nat) (tas (ajoute n t)).
Proof.
  Induction t. Simpl. Intros. Split; Trivial. Split; Trivial. Split; Trivial.
  Intros. Simpl. Elim (choix_bool (au_plus n0 n)). Intro. Rewrite H2. Simpl. Simpl in H1.
  Elim H1. Intros. Elim H4. Intros. Elim H6. Intros. Split. Apply ajoute_minore. Assumption.
  (Apply au_plus_minore with n:=n; Assumption).
  Split. (Apply H0; Assumption).
  Split. (Apply au_plus_minore with n:=n; Assumption).
  Assumption.
  Intro. Rewrite H2. Simpl. Simpl in H1. Elim H1. Intros. Elim H4. Intros. Elim H6. Intros. Split.
  Apply ajoute_minore. Apply au_plus_total. Assumption.
  Assumption.
  Split. (Apply H0; Assumption).
  (Split; Assumption).
Qed.

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

Fixpoint conversion [l:liste] : pretas :=
  Cases l of
      nil => V
    | (cons n l') => (ajoute n (conversion l'))
  end.

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

Fixpoint nocc_tas [x:nat; t:pretas] : nat :=
  Cases t of
      V => O
    | (B g n d) =>
      if (egal x n)
      then (S (plus (nocc_tas x g) (nocc_tas x d)))
      else (plus (nocc_tas x g) (nocc_tas x d))
  end.

Definition memes_elements := [l:liste; t:pretas]
  (x:nat) (nocc_l x l)=(nocc_tas x t).

Lemma conversion_produit_tas : (l:liste) (tas (conversion l)).
Proof.
  Induction l. Simpl. Trivial.
  Simpl. Intros. Apply ajoute_preserve_tas. Assumption.
Qed.

Lemma nocc_ajoute : (t:pretas) (x,n:nat)
  ((egal x n)=true  -> (nocc_tas x (ajoute n t))=(S (nocc_tas x t))) /\
  ((egal x n)=false -> (nocc_tas x (ajoute n t))=(nocc_tas x t)).
  (* On ne peut prouver ces deux proprietes qu'ensemble,
  ce qu'on appelle usuellement en mathematiques "par recurrence simultanee". *)
Proof.
  Induction t. Simpl. Intros. Split. Intro. Rewrite H. Reflexivity.
  Intro. Rewrite H. Reflexivity.
  Simpl. Intros. Elim (choix_bool (egal x n0)). Intro. Rewrite H1. Split. Intro.
  Elim (choix_bool (au_plus n0 n)). Intro. Rewrite H3. Simpl. Rewrite H1.Elim (H0 x n). Intros.
  Elim (choix_bool (egal x n)). Intro. Rewrite H6. Rewrite (H4 H6). Simpl. Rewrite plus_sym.
  Reflexivity.
  Intro. Rewrite H6. Rewrite (H5 H6). Rewrite plus_sym. Reflexivity.
  Intro. Rewrite H3. Simpl. Elim (choix_bool (egal x n)). Intro. Rewrite <- (egal_1 x n0 H1) in H3.
  Rewrite (egal_imp_au_plus x n H4) in H3. Discriminate H3.
  Intro. Rewrite H4. Elim (H0 x n0). Intros. Rewrite (H5 H1). Simpl. Rewrite plus_sym. Reflexivity.
  Intro. Discriminate H2.
  Intro. Rewrite H1. Split. Intro. Discriminate H2.
  Intro. Elim (H0 x n). Intros. Elim (choix_bool (au_plus n0 n)). Intro. Rewrite H5. Simpl.
  Rewrite H1. Elim (choix_bool (egal x n)). Intro. Rewrite H6. Rewrite (H3 H6). Simpl.
  Rewrite plus_sym. Reflexivity.
  Intro. Rewrite H6. Rewrite (H4 H6). Apply plus_sym.
  Intro. Rewrite H5. Simpl. Elim (H0 x n0). Intros. Elim (choix_bool (egal x n)). Intro.
  Rewrite H8. Rewrite (H7 H1). Rewrite plus_sym. Reflexivity.
  Intro. Rewrite H8. Rewrite (H7 H1). Apply plus_sym.
Qed.

Lemma nocc_ajoute_1 : (t:pretas) (n:nat) (nocc_tas n (ajoute n t))=(S (nocc_tas n t)).
Proof.
  Intros. Elim (nocc_ajoute t n n). Intros. Apply H. Apply egal_refl.
Qed.

Lemma nocc_ajoute_2 : (t:pretas) (x,n:nat) (egal x n)=false
                         -> (nocc_tas x (ajoute n t))=(nocc_tas x t).
Proof.
  Intros. Elim (nocc_ajoute t x n). Intros. Apply H1. Assumption.
Qed.


Lemma conversion_memes_elements : (l:liste) (memes_elements l (conversion l)).
Proof.
  Induction l. Simpl. Unfold memes_elements. Intro. Reflexivity.
  Unfold memes_elements. Simpl. Intros. Elim (choix_bool (egal x n)). Intro. Rewrite H0.
  Rewrite (egal_1 x n H0). Rewrite (nocc_ajoute_1 (conversion l0) n). Rewrite (H n). Reflexivity.
  Intro. Rewrite H0. Rewrite (nocc_ajoute_2 (conversion l0) x n H0). Apply H.
Qed.