Tab_in.v

Require Export Tab_def.

(* un entier est-il hors limites du tableau ? *)

Definition in_tab := [i:int] [a:tableau](lt (position i) (taille a)).
(* idem pour une liste d'entiers *)

Mutual Inductive in_tab_rec: (list int) -> tableau ->Prop :=
     in_tab_rec_nil: (a:tableau)(in_tab_rec (nil int) a)
    | in_tab_rec_cons:
        (a:tableau) (l:(list int)) (i:int) (in_tab_rec l a) -> (in_tab i a) ->
        (in_tab_rec (cons i l) a) .
Hint in_tab_rec_nil in_tab_rec_cons.

Definition in_tab_all :=
   [l:(list int)] [a:tableau] (i:int) (In i l) ->(in_tab i a).
(* lemmes associes a in_tab_rec *)

Lemma th_in_tab_all:
  (l:(list int)) (a:tableau)(iff (in_tab_all l a) (in_tab_rec l a)).
Unfold in_tab_all.
Induction l; Split.
Intros; Simpl; Auto.
Simpl; Intros; Contradiction.
Elim (H a0); Intros Sens1 Sens2.
Intros.
Apply in_tab_rec_cons; Auto.
Elim (H a0); Intros Sens1 Sens2.
Intros.
Inversion H1; Inversion H0; Auto.
Rewrite <- H2; Auto.
Qed.

Lemma in_tab_moins: (a:tableau) (i:int) (in_tab i a) ->(in_tab (moins i) a).
Intros.
Unfold in_tab.
Cut (position (moins i))=(position i); [Intros A; Rewrite A | Case i; Simpl];
Auto.
Qed.
Hint in_tab_moins.

Lemma in_tab_rec_opp:
  (a:tableau) (l:(list int)) (in_tab_rec l a) ->(in_tab_rec (map moins l) a).
Induction l.
Simpl; Auto.
Intros t q HR H; Simpl; Intros.
Inversion H.
Apply in_tab_rec_cons; Auto.
Qed.
Hint in_tab_rec_opp.

14/09/98, 09:21