Tab_def.v

Require Export Int.
Require Export Liste.
(* assignement *)

Mutual Inductive assignement: Set :=
     V: int ->assignement
    | L: (list int) ->assignement .

Definition opp :=
   [x:assignement]
      Cases x of
          (V i) => (V (moins i))
         | (L li) => (L (map moins li))
      end.

Definition if_neg_opp :=
   [i:int]
      Cases (positif i) of
          true => [x:assignement]x
         | false => opp
      end.
(* lemmes pour if_neg_opp *)

Lemma opp_opp: (x:assignement)(opp (opp x))=x.
Unfold opp.
Intros x; Case x.
Unfold moins; Intros i; Case i; Auto.
Intros; Apply (f_equal (list int) assignement).
Elim l.
Simpl; Auto.
Intros t q HR.
Simpl.
Rewrite HR.
Unfold moins; Case t; Auto.
Qed.
Hint opp_opp.

Lemma if_neg_opp_involutif:
  (i:int) (x:assignement)(if_neg_opp i (if_neg_opp i x))=x.
Intros.
Unfold if_neg_opp.
Case (positif i); Intros; Auto.
Qed.
Hint if_neg_opp_involutif.

Lemma if_neg_opp_moins:
  (i:int) (x, x':assignement) x=x' ->
  (if_neg_opp (moins i) x)=(opp (if_neg_opp i x')).
Intros.
Unfold if_neg_opp.
Rewrite (positif_moins i).
Case (positif i); Simpl; Intros; Auto.
Rewrite H; Auto.
Rewrite H; Auto.
Qed.
Hint if_neg_opp_moins.
(* type Etat *)

Mutual Inductive etat: Set :=
     Contrad: etat
    | Ras: etat .
(* tableau *)

Mutual Inductive tableau: Set :=
     Tab: etat -> (list assignement) ->tableau .

Definition taille :=
   [a:tableau]
      Cases a of
          (Tab b l) => (length l)
      end.

14/09/98, 09:21