Tab_valeur.v

Require Export Tab_in.
(* lecture d'un element du tableau *)

Definition nieme:
  (l:(list assignement)) (n:nat) (lt n (length l)) ->assignement.
Induction l.
Simpl; Intros n H; Absurd (lt n O); Auto.
Intros t q; Simpl; Intros HR n H.
Generalize (refl_equal nat n); Pattern 2 n; Case n; Intros.
Exact t.
Cut (lt n0 (length q)).
Intros N; Exact (HR n0 N).
Apply lt_S_n; Rewrite <- H0; Auto.
Defined.

Definition valeur: (a:tableau) (i:int) (in_tab i a) ->assignement.
Intros a i; Case a; Intros.
Cut (lt (position i) (length l)).
Intros N; Exact (if_neg_opp i (nieme l (position i) N)).
Inversion H; Auto.
Defined.
(* lemmes pour nieme et val *)

Lemma nieme_dans_liste:
  (l:(list assignement)) (n:nat) (h:(lt n (length l)))(In (nieme l n h) l).
Induction l.
Simpl; Intros; Absurd (lt n O); Auto.
Intros t q Hyp n.
Case n.
Simpl; Intros; Auto.
Intros.
Cut (lt n0 (length q)); Auto.
Intros; Simpl; Auto.
Qed.
Hint nieme_dans_liste.

Lemma nieme_unicite:
  (l, l':(list assignement))
  (n, n':nat) (h:(lt n (length l))) (h':(lt n' (length l'))) l=l' -> n=n' ->
  (nieme l n h)=(nieme l' n' h').
Induction l; Induction l'.
Simpl; Intros; Absurd (lt n O); Auto.
Simpl; Intros; Absurd (lt n O); Auto.
Simpl; Intros; Absurd (lt n' O); Auto.
Intros t q HR n n'; Case n; Case n'; Simpl; Intros; Auto; Inversion H1; Auto.
Inversion H0; Auto.
Apply H; Auto.
Inversion H0; Auto.
Qed.
Hint nieme_unicite.

Lemma valeur_unicite:
  (a, a':tableau) (i, j:int) (h:(in_tab i a)) (h':(in_tab j a')) a=a' -> i=j ->
  (valeur a i h)=(valeur a' j h').
Intros a a' i j; Case a; Case a'; Intros.
Cut (lt (position i) (length l0)); Auto.
Cut (lt (position j) (length l)); Auto.
Intros.
Simpl.
LApply (f_equal int assignement ->assignement if_neg_opp i j); Auto.
Intros A; Rewrite A.
Apply (f_equal assignement assignement (if_neg_opp j)); Auto.
Apply nieme_unicite; Auto.
Inversion H; Auto.
Rewrite H0; Auto.
Qed.
Hint valeur_unicite.

Lemma valeur_moins:
  (a:tableau) (i:int) (h:(in_tab i a)) (h':(in_tab (moins i) a))
  (valeur a (moins i) h')=(opp (valeur a i h)).
Intros a; Case a; Intros b l i; Intros.
Simpl.
Apply if_neg_opp_moins.
Apply nieme_unicite; Auto.
Qed.
Hint valeur_moins.

14/09/98, 09:21