Int_liste.v

Require Export Int_comp.
Require Export PolyList.
(* l' appartenance a une liste est decidable *)

Lemma In_int_decide: (l:(list int)) (i:int){(In i l)}+{~ (In i l)}.
Induction l.
Intros; Right; Red; Intros; Inversion H.
Intros t q HR i.
Case (eq_int_decide i t); Intros.
Left; LApply (eq_int_eq i t); Auto.
Intros A; Rewrite A; Auto.
Elim (HR i); [Left | Right]; Auto.
Red; Simpl; Intros A; Elim A; Auto; Intros.
Absurd (eq_int i t); Auto; Rewrite <- H; Auto.
Qed.

Lemma In_moins: (l:(list int)) (i:int) (In i l) ->(In (moins i) (map moins l)).
Induction l.
Simpl; Auto.
Intros t q HR i.
Simpl; Intros A; Elim A; Intros; Auto.
Left; Rewrite H; Auto.
Qed.
Hint In_moins.

Lemma In_map_moins:
  (l:(list int)) (i:int) (In i (map moins l)) ->(In (moins i) l).
Induction l.
Intros; Simpl; Auto.
Intros; Simpl; Auto.
Simpl in H0; Elim H0; Intros; Auto.
Left; Rewrite <- H1; Auto.
Qed.
Hint In_map_moins.

(* liste des int dont la position est <=  n   utile pour les programmes de decidabilite *)

Fixpoint int_position_le_n[n:nat]: (list int) :=
   Cases n of
       O => (cons Moins_Un (cons Un (nil int)))
      | (S p) => (cons (M p) (cons (P p) (int_position_le_n p)))
   end.

Lemma liste_int_complete:
  (n:nat) (i:int)(iff (le (position i) n) (In i (int_position_le_n n))).
Induction n; Split.
Case i; Simpl; Intros; Inversion H.
Right; Left; Auto.
Left; Auto.
Simpl.
Intros H; Elim H.
Intros A; Rewrite <- A; Auto.
Intros H1; Elim H1.
Intros A; Rewrite <- A; Auto.
Intros; Contradiction.
Case (le_lt_dec (position i) n0).
Intros.
Elim (H i); Intros Sens1 Sens2.
Simpl; Right; Right; Auto.
Intros.
Cut (position i)=(S n0); Auto.
Case i; Simpl; Intros; Inversion H1.
Right; Left; Auto.
Left; Auto.
Simpl.
Intros A; Elim A; Auto.
Intros B; Rewrite <- B; Auto.
Intros B; Elim B; Auto.
Intros C; Rewrite <- C; Auto.
Elim (H i); Intros Sens1 Sens2.
Intros; Auto.
Qed.
(* liste des int  positifs dont la position est <=  n  *)

Fixpoint int_positif_position_le_n[n:nat]: (list int) :=
   Cases n of
       O => (cons Un (nil int))
      | (S p) => (cons (P p) (int_positif_position_le_n p))
   end.

Definition int_positif_position_lt_n :=
   [n:nat]
      Cases n of
          O => (nil int)
         | (S p) => (int_positif_position_le_n p)
      end.

Lemma liste_int_positif_complete:
  (n:nat) (i:int)
  (iff
     (le (position i) n) /\ (positif i)=true
     (In i (int_positif_position_le_n n))).
Induction n; Split.
Case i; Simpl; Intros; Inversion H; Auto.
Absurd (le (S n0) O); Auto.
Simpl.
Intros H; Elim H.
Intros A; Rewrite <- A; Auto.
Intros A; Contradiction.
Simpl.
Case (le_lt_dec (position i) n0); Intros; Elim H0; Intros.
Elim (H i); Intros Sens1 Sens2.
Right; Apply Sens1; Auto.
Cut (position i)=(S n0); Auto.
Generalize H1 H2.
Case i; Simpl; Intros; Inversion H5; Auto.
Inversion H4.
Simpl.
Intros H1; Elim H1; Intros.
Split; Rewrite <- H0; Auto.
Elim (H i); Intros Sens1 Sens2.
Elim (Sens2 H0); Intros.
Split; Auto.
Qed.

Lemma liste_int_positif_lt_complete:
  (n:nat) (i:int)
  (iff
     (lt (position i) n) /\ (positif i)=true
     (In i (int_positif_position_lt_n n))).
Intros n i.
Case n.
Simpl; Split; Auto.
Intros H; Elim H; Intros; Absurd (lt (position i) O); Auto.
Intros H; Contradiction.
Unfold int_positif_position_lt_n.
Clear n; Intros n.
Elim (liste_int_positif_complete n i); Intros Sens1 Sens2.
Split.
Intros H; Elim H; Intros.
Apply Sens1; Auto.
Intros H; LApply Sens2; Auto.
Intros H1; Elim H1; Intros.
Split; Auto.
Qed.

(* appartenance "en valeur absolue" a une liste *)

Definition In_va := [i:int] [l:(list int)](In i l) \/ (In (moins i) l).

Lemma In_va_cons1:
  (i, t:int) (q:(list int)) (In_va i (cons t q)) ->
  (abs i)=(abs t) \/ (In_va i q).
Unfold In_va; Simpl.
Intros.
Elim H; Intros; Elim H0; Intros; Auto.
Left; Rewrite H1; Auto.
Left; Rewrite H1; Auto.
Qed.
Hint In_va_cons1.

Lemma In_va_cons21:
  (i, t:int) (q:(list int)) (abs i)=(abs t) ->(In_va i (cons t q)).
Unfold In_va; Simpl; Intros.
LApply (abs_inj i t); Intros; Auto.
Elim H0; Intros; Auto.
Right; Left; Rewrite y; Auto.
Qed.
Hint In_va_cons21.

Lemma In_va_cons22:
  (i, t:int) (q:(list int)) (In_va i q) ->(In_va i (cons t q)).
Unfold In_va; Simpl; Intros.
Elim H; Intros; Auto.
Qed.
Hint In_va_cons22.

Lemma In_va_map_moins:
  (l:(list int)) (i:int) (In_va i l) ->(In_va i (map moins l)).
Induction l.
Simpl; Auto.
Intros t q HR i.
Simpl; Intros.
LApply (In_va_cons1 i t q); Auto; Intros.
Elim H0; Intros; Auto.
Cut (abs i)=(abs (moins t)); [Auto | Rewrite H1; Auto].
Qed.
Hint In_va_map_moins.

(* intersection vide "en valeur absolue" *)

Definition inter_va_vide :=
   [l1, l2:(list int)] (j:int) (In_va j l1) -> (In_va j l2) ->False.

14/09/98, 09:21