Int_signe.v

Require Export Int_def.
(* moins *)

Lemma moins_moins: (i:int)(moins (moins i))=i.
Intros; Case i; Simpl; Auto.
Qed.
Hint moins_moins.

Lemma moins_inj: (i, j:int) (moins i)=(moins j) ->i=j.
Intros i j.
Case i; Case j; Simpl; Intros; Inversion H; Auto.
Qed.

Lemma nat_of_int_moins: (i:int)(nat_of_int (moins i))=(nat_of_int i).
Induction i; Intros; Simpl; Auto.
Qed.
Hint nat_of_int_moins.

Lemma eval_int_moins:
(f:nat ->bool) (i:int)(eval_int f (moins i))=(negb (eval_int f i)).
Induction i; Intros; Simpl; Auto.
Rewrite negb_elim; Auto.
Qed.
Hint eval_int_moins.

Lemma position_moins: (i:int)(position (moins i))=(position i).
Induction i; Intros; Simpl; Auto.
Qed.
Hint position_moins.

Lemma abs_moins: (i:int)(abs (moins i))=(abs i).
Intros; Case i; Simpl; Auto.
Qed.
Hint abs_moins.

(* abs *)

Lemma position_abs_inj: (i, j:int) (position i)=(position j) ->(abs i)=(abs j).
Intros i j; Case i; Case j; Unfold position; Simpl; Intros; Inversion H; Auto.
Qed.
Hint position_abs_inj.

Lemma abs_position_inj: (i, j:int) (abs i)=(abs j) ->(position i)=(position j).
Intros i j; Case i; Case j; Unfold position; Simpl; Intros; Inversion H; Auto.
Qed.
Hint abs_position_inj.

Lemma abs_inj: (i, j:int) (abs i)=(abs j) ->{i=j}+{i=(moins j)}.
Intros i j; Case i; Case j; Simpl; Intros; Inversion H; Auto.
Qed.
Hint abs_inj.

Lemma non_abs1: (i, j:int) ~ (abs i)=(abs j) ->~ i=j.
Intros; Red; Intros A; Rewrite A in H; Auto.
Qed.
Hint non_abs1.

Lemma non_abs2: (i, j:int) ~ (abs i)=(abs j) ->~ i=(moins j).
Intros; Red; Intros A; Rewrite A in H; Auto.
Qed.
Hint non_abs2.

(* positif *)

Lemma pos_abs: (i:int) (positif i)=true ->(abs i)=i.
Induction i; Simpl; Auto; Intros; Absurd false=true; Auto.
Qed.
Hint pos_abs.

Lemma neg_moins_abs: (i:int) (positif i)=false ->(abs i)=(moins i).
Induction i; Simpl; Auto; Intros; Absurd false=true; Auto.
Qed.
Hint neg_moins_abs.

Lemma positif_moins: (x:int)(positif (moins x))=(negb (positif x)).
Induction x; Simpl; Auto.
Qed.
Hint positif_moins.

14/09/98, 09:21