Int_def.v

Require Export Bool.

Mutual Inductive int: Set :=
     Un: int
    | Moins_Un: int
    | P: nat ->int
    | M: nat ->int .

(* fonctions diverses*)

Definition abs: int ->int :=
   [i:int]
      Cases i of
          Un => Un
         | Moins_Un => Un
         | (P n) => (P n)
         | (M n) => (P n)
      end.

Definition moins :=
   [i:int]
      Cases i of
          Un => Moins_Un
         | Moins_Un => Un
         | (P n) => (M n)
         | (M n) => (P n)
      end.

Definition nat_of_int :=
   [i:int]
      Cases i of
          Un => O
         | Moins_Un => O
         | (P n) => n
         | (M n) => n
      end.

Definition position :=
   [i:int]
      Cases i of
          Un => O
         | Moins_Un => O
         | (P n) => (S n)
         | (M n) => (S n)
      end.

Definition eval_int: (nat ->bool) -> int ->bool :=
   [f:nat ->bool] [i:int]
      Cases i of
          Un => true
         | Moins_Un => false
         | (P n) => (f n)
         | (M n) => (negb (f n))
      end.

Definition positif :=
   [i:int]
      Cases i of
          Un => true
         | Moins_Un => false
         | (P n) => true
         | (M n) => false
      end.

Lemma th_eval_int:
  (f, g:nat ->bool) (i:int) (f (nat_of_int i))=(g (nat_of_int i)) ->
  (eval_int f i)=(eval_int g i).
Intros f g i; Case i; Intros; Simpl; Auto.
Cut (f n)=(g n); Auto.
Intros H0; Rewrite H0; Auto.
Qed.
Hint th_eval_int.

14/09/98, 09:21