Int_comp.v

Require Export Int_signe.
Require Export Arith.
Require Export EqNat.
Require Export Compare_dec.

(* egalite decidable sur mes int *)

Definition eq_int :=
   [i, j:int]
      Cases i j of
          Un Un => True
         | Un _ => False
         | Moins_Un Moins_Un => True
         | Moins_Un _ => False
         | (P n) (P m) => (eq_nat n m)
         | (P n) _ => False
         | (M n) (M m) => (eq_nat n m)
         | (M n) _ => False
      end.

Lemma eq_int_refl: (i:int)(eq_int i i).
Induction i; Simpl; Auto.
Qed.
Hint eq_int_refl.

Lemma eq_eq_int: (i, j:int) i=j ->(eq_int i j).
Intros i j N; Rewrite N; Auto.
Qed.
Immediate eq_eq_int.

Lemma eq_int_eq: (i, j:int) (eq_int i j) ->i=j.
Intros i j; Elim i; Elim j; Simpl; Intros; Contradiction Orelse Auto;
Rewrite (eq_nat_eq n0 n); Auto.
Qed.
Immediate eq_int_eq.

Lemma non_eq_moins_1: (i:int)~ (eq_int i (moins i)).
Intros; Elim i; Simpl; Red; Intros; Contradiction.
Qed.
Immediate non_eq_moins_1.

Lemma non_eq_moins_2: (i:int)~ (eq_int (moins i) i).
Intros; Elim i; Simpl; Red; Intros; Contradiction.
Qed.
Immediate non_eq_moins_2.

Lemma eq_int_decide: (i, j:int){(eq_int i j)}+{~ (eq_int i j)}.
Intros; Elim i; Auto.
Elim j; Auto; Right; Red; Auto.
Elim j; Auto; Right; Red; Auto.
Elim j.
Right; Red; Auto.
Right; Red; Auto.
Intros; Simpl; Case (eq_nat_decide n0 n); [Left | Right]; Auto.
Right; Red; Auto.
Elim j.
Right; Red; Auto.
Right; Red; Auto.
Right; Red; Auto.
Intros; Simpl; Case (eq_nat_decide n0 n); [Left | Right]; Auto.
Qed.

(* ordre en valeur absolue *)

Definition le_va := [i, j:int](le (position i) (position j)).

Definition lt_va := [i, j:int](lt (position i) (position j)).
Hint Unfold le_va.
Hint Unfold lt_va.
(* lemmes pour le_va *)
Lemma le_va_le_pos: (i, j:int) (le_va i j) ->(le (position i) (position j)).
Intros; Auto.
Qed.
Hint le_va_le_pos.

Lemma le_va_refl: (i:int)(le_va i i).
Auto.
Qed.
Hint le_va_refl.

Lemma le_va_trans: (i, j, k:int) (le_va i j) -> (le_va j k) ->(le_va i k).
Unfold le_va; Intros; Apply le_trans with (position j); Auto.
Qed.

Lemma le_va_antisym: (i, j:int) (le_va i j) -> (le_va j i) ->(abs i)=(abs j).
Auto.
Qed.
Hint le_va_antisym.
(* lemmes pour lt_va *)

Lemma lt_va_not_refl: (i:int)~ (lt_va i i).
Unfold lt_va; Intros; Apply lt_n_n; Auto.
Qed.
Hint lt_va_not_refl.

Lemma lt_va_not_sym: (i, j:int) (lt_va i j) ->~ (lt_va j i).
Unfold lt_va; Intros; Apply lt_not_sym; Auto.
Qed.
Hint lt_va_not_sym.

Lemma lt_va_trans: (i, j, k:int) (lt_va i j) -> (lt_va j k) ->(lt_va i k).
Unfold lt_va; Intros; Apply lt_trans with (position j); Auto.
Qed.
(* lt_va et le_va melanges *)

Lemma le_lt_va_exclus: (i, j:int) (le_va i j) -> (lt_va j i) ->False.
Unfold lt_va; Unfold le_va; Intros; Auto.
Absurd (lt (position j) (position i)); Auto.
Qed.

Lemma le_va_non_lt: (i, j:int) (le_va i j) ->~ (lt_va j i).
Intros; Red; Intros; LApply (le_lt_va_exclus i j H); Auto; Contradiction.
Qed.
Hint le_va_non_lt.

Lemma lt_va_non_le: (i, j:int) (lt_va i j) ->~ (le_va j i).
Intros; Red; Intros; LApply (le_lt_va_exclus j i H0); Auto; Contradiction.
Qed.
Hint lt_va_non_le.

Lemma lt_va_ordre_total:
  (i, j:int) ~ (abs i)=(abs j) ->(lt_va i j) \/ (lt_va j i).
Unfold le_va lt_va; Intros; Apply nat_total_order; Auto.
Red; Intros; Absurd (abs i)=(abs j); Auto.
Qed.
Hint lt_va_ordre_total.

Lemma lt_va_or_abs: (i, j:int) (le_va i j) ->(lt_va i j) \/ (abs i)=(abs j).
Intros; Case (eq_int_decide (abs i) (abs j)); [Right | Left]; Auto.
LApply (lt_va_ordre_total i j);
[Intro A; Elim A; Auto; Intros; LApply (le_lt_va_exclus i j H);
   Try Contradiction | Red; Intros; Absurd (eq_int (abs i) (abs j))]; Auto.
Qed.
Hint lt_va_or_abs.

Lemma lt_va_non_eq: (i, j:int) (lt_va i j) ->~ (abs i)=(abs j).
Intros; Red; Intros.
Absurd (lt (position i) (position j)); Auto.
Rewrite (abs_position_inj i j); Auto.
Qed.
Hint lt_va_non_eq.

Lemma lt_le_va_trans: (i, j, k:int) (lt_va i j) -> (le_va j k) ->(lt_va i k).
Unfold lt_va le_va; Intros; Auto.
Apply lt_le_trans with m := (position j); Auto.
Qed.

Lemma le_lt_va_trans: (i, j, k:int) (le_va i j) -> (lt_va j k) ->(lt_va i k).
Unfold lt_va le_va; Intros; Auto.
Apply le_lt_trans with m := (position j); Auto.
Qed.

Lemma lt_le_va_weak: (i, j:int) (lt_va i j) ->(le_va i j).
Auto.
Qed.
Hint lt_le_va_weak.

Lemma le_lt_va_dec: (i, j:int){(le_va i j)}+{(lt_va j i)}.
Intros; Case (le_lt_dec (position i) (position j)); Auto.
Qed.
(* ordre et moins *)

Lemma le_va_moins1: (i, j:int) (le_va i j) ->(le_va i (moins j)).
Unfold lt_va le_va; Intros i j; Case j; Simpl; Auto.
Qed.

Lemma le_va_moins2: (i, j:int) (le_va i j) ->(le_va (moins i) j).
Unfold lt_va le_va; Intros i j; Case i; Simpl; Auto.
Qed.

Lemma lt_va_moins1: (i, j:int) (lt_va i j) ->(lt_va i (moins j)).
Unfold lt_va le_va; Intros i j; Case j; Simpl; Auto.
Qed.

Lemma lt_va_moins2: (i, j:int) (lt_va i j) ->(lt_va (moins i) j).
Unfold lt_va le_va; Intros i j; Case i; Simpl; Auto.
Qed.
Hint le_va_moins1 le_va_moins2 lt_va_moins1 lt_va_moins2.

14/09/98, 09:21