Liste.v

Require Export Int.

Mutual Inductive inf_list: int -> (list int) ->Prop :=
     nil_inf: (i:int)(inf_list i (nil int))
    | cons_inf:
        (i, j:int) (l:(list int)) (lt_va i j) -> (inf_list i l) ->
        (inf_list i (cons j l)) .

Lemma th_inf_list:
  (l:(list int)) (i:int)(iff (inf_list i l) (j:int) (In j l) ->(lt_va i j)).
Induction l.
Simpl; Split; Intros; Contradiction Orelse Apply nil_inf.
Intros t q HR i; Elim (HR i); Intros Sens1 Sens2; Split; Simpl; Intros.
Elim H0; Inversion H; Intros A; Rewrite <- A Orelse Apply Sens1; Auto.
Apply cons_inf; Auto.
Qed.

Mutual Inductive sorted: (list int) ->Prop :=
     sorted_nil: (sorted (nil int))
    | sorted_cons:
        (i:int) (l:(list int)) (inf_list i l) -> (sorted l) ->
        (sorted (cons i l)) .
Hint nil_inf cons_inf sorted_nil sorted_cons.
(* insertion *)

Fixpoint ins[i:int; l:(list int)]: (list int) :=
   Cases l of
       nil => (cons i (nil int))
      | (cons t q) => Cases (le_lt_va_dec t i) of
                          left => (cons t (ins i q))
                         | right => (cons i l)
                      end
   end.

Lemma ins_conserve_elements:
  (l:(list int)) (i, j:int)(iff (In j (ins i l)) j=i \/ (In j l)).
Induction l.
Split; Simpl; Intros; Auto; Elim H; Auto Orelse Contradiction.
Intros t q HR i j.
Elim (HR i j); Intros Sens1 Sens2.
Split; Simpl; Case (le_lt_va_dec t i); Simpl; Intros; Elim H; Intros; Auto.
Elim Sens1; Auto.
Elim H0; Auto.
Qed.

Lemma ins_sorted:
  (l:(list int)) (hl:(sorted l)) (i:int) ~ (In_va i l) ->(sorted (ins i l)).
Induction l.
Simpl; Auto.
Intros t q HR Htq i Hi.
Simpl; Case (le_lt_va_dec t i); Intros.
Cut (lt_va t i); Intros; Auto.
Inversion Htq.
LApply (HR H3 i); Auto.
Intros.
Apply sorted_cons; Auto.
Elim (th_inf_list (ins i q) t); Intros Sens1 Sens2.
Apply Sens2.
Intros.
Elim (ins_conserve_elements q i j); Intros Sens1' Sens2'.
Elim Sens1'; Intros; Auto.
Rewrite H6; Auto.
Elim (th_inf_list q t); Intros Sens1'' Sens2''.
Apply Sens1''; Auto.
Red; Intros.
Absurd (In_va i (cons t q)); Auto.
LApply (lt_va_or_abs t i); Auto; Intros A; Elim A; Intros; Auto.
Absurd (In_va i (cons t q)); Auto.
Apply sorted_cons; Auto.
Inversion Htq.
Elim (th_inf_list q t); Intros Sens1 Sens2.
Elim (th_inf_list q i); Intros Sens1' Sens2'.
Apply cons_inf; Auto.
LApply Sens2'; Auto.
Intros.
Apply lt_va_trans with t; Auto.
Qed.

Fixpoint fusion[l1:(list int)]: (list int) ->(list int) :=
   Fix G {
    G/1: (l2:(list int))(list int) := [l2:(list int)]
                                         Cases l1 l2 of
                                             nil nil => (nil int)
                                            | nil (cons t2 q2) => (cons t2 q2)
                                            | (cons t1 q1) nil => (cons t1 q1)
                                            | (cons t1 q1) (cons t2 q2) =>
                                                Cases (le_lt_va_dec t1 t2) of
                                                    left =>
                                                      (cons
                                                         t1
                                                         (fusion
                                                            q1 (cons t2 q2)))
                                                   | right => (cons t2 (G q2))
                                                end
                                         end
   }.

Lemma fusion_conserve_elements:
  (l1, l2:(list int)) (j:int)(iff (In j (fusion l1 l2)) (In j l1) \/ (In j l2)).
Induction l1.
Simpl; Intros; Case l2; Split; Intros; Elim H; Intros; Auto Orelse Contradiction.
Intros t1 q1 HR1; Induction l2.
Simpl.
Split; Intros; Auto; Elim H; Intros; Auto; Elim H0; Auto.
Intros t2 q2 HR j; Simpl.
Case (le_lt_va_dec t1 t2); Simpl.
Elim (HR1 (cons t2 q2) j); Intros Sens1 Sens2.
Split; Intros; Elim H; Auto; Intros; [Elim Sens1 | Elim H0]; Auto.
Simpl in HR.
Elim (HR j); Intros Sens1 Sens2.
Split; Intros; Elim H; Auto; Intros; [Elim Sens1 | Elim H0]; Auto.
Qed.

Lemma fusion_conserve_inf_list:
  (l1, l2:(list int)) (t:int) (inf_list t l1) -> (inf_list t l2) ->
  (inf_list t (fusion l1 l2)).
Intros.
Elim (th_inf_list (fusion l1 l2) t); Intros Sens1 Sens2.
Apply Sens2; Intros.
Elim (fusion_conserve_elements l1 l2 j); Intros Sens1' Sens2'.
LApply Sens1'; Auto.
Intros A; Elim A; Intros.
Elim (th_inf_list l1 t); Intros Sens1'' Sens2''; Auto.
Elim (th_inf_list l2 t); Intros Sens1'' Sens2''; Auto.
Qed.

Lemma fusion_sorted:
  (l1, l2:(list int)) (inter_va_vide l1 l2) -> (sorted l1) -> (sorted l2) ->
  (sorted (fusion l1 l2)).
Induction l1.
Simpl; Intros l2; Case l2; Auto.
Intros t1 q1 HR1; Induction l2.
Simpl; Auto.
Intros t2 q2 HR Hinter Hl1 Hl2.
Inversion Hl1; Inversion Hl2.
Simpl.
Case (le_lt_va_dec t1 t2); Simpl.
Intros.
Cut (lt_va t1 t2); Intros.
Apply sorted_cons; Auto.
Elim (th_inf_list (fusion q1 (cons t2 q2)) t1); Intros Sens1 Sens2.
Apply Sens2; Intros.
Elim (fusion_conserve_elements q1 (cons t2 q2) j); Intros Sens1' sens2'.
Elim Sens1'; Intros; Auto.
Elim (th_inf_list q1 t1); Intros; Auto.
Apply lt_le_va_trans with t2; Auto.
Simpl in H9; Elim H9; Intros.
Rewrite H10; Auto.
Apply lt_le_va_weak.
Elim (th_inf_list q2 t2); Intros; Auto.
Apply HR1; Auto.
Unfold inter_va_vide.
Intros.
Unfold inter_va_vide in Hinter.
Apply (Hinter j); Auto.
LApply (lt_va_or_abs t1 t2); Auto; Intros A; Elim A; Auto; Intros.
Cut (In_va t1 (cons t1 q1)); Auto; Intros.
LApply (Hinter t1 H8); Auto; Intros; Contradiction.
Intros.
Simpl in HR.
Apply sorted_cons; Auto.
Cut (inf_list t2 (cons t1 q1)); Intros.
LApply (fusion_conserve_inf_list (cons t1 q1) q2 t2 H7); Auto.
Elim (th_inf_list (cons t1 q1) t2); Intros; Auto.
Apply H8; Intros.
Apply lt_le_va_trans with t1; Auto.
Simpl in H9; Elim H9; Intros.
Rewrite H10; Auto.
Apply lt_le_va_weak.
Elim (th_inf_list q1 t1); Intros; Auto.
Apply HR; Auto.
Unfold inter_va_vide.
Intros.
Unfold inter_va_vide in Hinter.
Apply (Hinter j); Auto.
Qed.

Fixpoint prog_inf_list_decide[i:int; l:(list int)]: bool :=
   Cases l of
       nil => true
      | (cons t q) => Cases (le_lt_va_dec t i) of
                          left => false
                         | right => (prog_inf_list_decide i q)
                      end
   end.

Lemma th_prog_inf_list:
  (l:(list int)) (i:int)(iff (inf_list i l) (prog_inf_list_decide i l)=true).
Induction l.
Simpl; Split; Intros; Auto.
Intros t q HR i; Simpl; Case (le_lt_va_dec t i); Intros; Split; Intros.
Inversion H.
Absurd (le_va t i); Auto.
Absurd false=true; Auto.
Inversion H.
Elim (HR i); Intros; Auto.
Elim (HR i); Intros; Auto.
Qed.

Lemma inf_list_decide:
  (i:int) (l:(list int)){(inf_list i l)}+{~ (inf_list i l)}.
Intros.
Generalize (refl_equal bool (prog_inf_list_decide i l));
Pattern 2 (prog_inf_list_decide i l); Case (prog_inf_list_decide i l); Intros.
Elim (th_prog_inf_list l i); Intros; Auto.
Elim (th_prog_inf_list l i); Intros; Auto.
Right; Red; Intros.
Absurd (prog_inf_list_decide i l)=true; Auto.
Rewrite H; Auto.
Qed.

Lemma sorted_decide: (l:(list int)){(sorted l)}+{~ (sorted l)}.
Induction l.
Left; Auto.
Intros t q HR; Elim HR; Intros.
Case (inf_list_decide t q); Intros; Auto.
Right; Red; Intros H; Inversion H; Auto.
Right; Red; Intros H; Inversion H; Auto.
Qed.
(* un lemme qui n'a rien a faire ici, mais bon ... *)

Lemma th_In_va_inf_list:
  (q:(list int)) (t:int) (inf_list t q) -> (In_va t q) ->False.
Intros.
Unfold In_va in H0.
Elim (th_inf_list q t); Intros Sens1 Sens2.
Elim H0; Intros.
Absurd (lt (position t) (position t)); Auto.
LApply (Sens1 H t); Auto.
Absurd (lt (position t) (position (moins t))); Auto.
Case t; Simpl; Auto.
LApply (Sens1 H (moins t)); Auto.
Qed.
(* moins et le tri *)

Lemma inf_list_moins:
  (t:int) (l:(list int)) (inf_list t l) ->(inf_list (moins t) (map moins l)).
Induction l.
Simpl; Auto.
Intros t q HR; Simpl; Intros.
Inversion H.
Apply cons_inf; Auto.
Qed.
Hint inf_list_moins.

Lemma sorted_opp: (l:(list int)) (sorted l) ->(sorted (map moins l)).
Induction l.
Simpl; Auto.
Intros t q HR; Simpl; Intros.
Inversion H.
Apply sorted_cons; Auto.
Qed.
Hint sorted_opp.

14/09/98, 09:21