Faux.v

(****************************************************************************                                                                                         IEEE754  :  Faux                                                                                                                                            Laurent Thery     Sylvie Boldo                                                                                                                   ***************************************************************************** Auxillary properties about natural numbers, relative numbers and reals *)
Require Import Min.
Require Import Arith.
Require Import Reals.
Require Import Zpower.
Require Import fast_integer.
Require Import Zcomplements.
Require Import sTactic.
Hints Resolve R1_neq_R0 :real.
(*Missing rule for nat *)

Theorem minus_minus: (a, b:nat) (le a b) ->(minus b (minus b a))=a.

Theorem lte_comp_mult:
  (p, q, r, t:nat) (le p q) -> (le r t) ->(le (mult p r) (mult q t)).

Theorem le_refl_eq: (n, m:nat) n=m ->(le n m).

Theorem lt_le_pred: (n, m:nat) (lt n m) ->(le n (pred m)).

Theorem lt_comp_mult_l:
  (p, q, r:nat) (lt O p) -> (lt q r) ->(lt (mult p q) (mult p r)).

Theorem lt_comp_mult_r:
  (p, q, r:nat) (lt O p) -> (lt q r) ->(lt (mult q p) (mult r p)).

Theorem lt_comp_mult:
  (p, q, r, s:nat) (lt p q) -> (lt r s) ->(lt (mult p r) (mult q s)).

Theorem mult_eq_inv: (n, m, p:nat) (lt O n) -> (mult n m)=(mult n p) ->m=p.

Definition natEq: (n, m:nat){n=m}+{~ n=m}.

Theorem notEqLt: (n:nat) (lt O n) ->~ n=O.

Theorem lt_next: (n, m:nat) (lt n m) ->m=(S n) \/ (lt (S n) m).

Theorem le_next: (n, m:nat) (le n m) ->m=n \/ (le (S n) m).

Theorem min_or: (n, m:nat)(min n m)=n /\ (le n m) \/ (min n m)=m /\ (lt m n).

Theorem minus_inv_lt_aux: (n, m:nat) (minus n m)=O ->(minus n (S m))=O.

Theorem minus_inv_lt: (n, m:nat) (le m n) ->(minus m n)=O.

Theorem minus_le:
  (m, n, p, q:nat) (le m n) -> (le p q) ->(le (minus m q) (minus n p)).

Theorem lt_minus_inv:
  (n, m, p:nat) (le n p) -> (lt m n) ->(lt (minus p n) (minus p m)).

Theorem lt_mult_anti_compatibility:
  (n, n1, n2:nat) (lt O n) -> (lt (mult n n1) (mult n n2)) ->(lt n1 n2).

Theorem le_mult_anti_compatibility:
  (n, n1, n2:nat) (lt O n) -> (le (mult n n1) (mult n n2)) ->(le n1 n2).

Theorem min_n_0: (n:nat)(min n O)=O.
(*Simplification rules missing in R *)

Theorem Rplus_ne_l: (r:R)(Rplus r R0)==r.

Theorem Rplus_ne_r: (r:R)(Rplus R0 r)==r.

Theorem Rmult_ne_l: (r:R)(Rmult r R1)==r.

Theorem Rmult_ne_r: (r:R)(Rmult R1 r)==r.

Theorem Rminus_Ropp: (x, y:R)(Ropp (Rminus y x))==(Rminus x y).

Theorem Rle_ref: (x:R)(Rle x x).

Theorem Rle_monotony:
  (r, r1, r2:R) (Rle R0 r) -> (Rle r1 r2) ->(Rle (Rmult r r1) (Rmult r r2)).

Theorem Rle_monotony_r:
  (r, r1, r2:R) (Rle R0 r) -> (Rle r1 r2) ->(Rle (Rmult r1 r) (Rmult r2 r)).

Theorem Rlt_monotony_r:
  (r, r1, r2:R) (Rlt R0 r) -> (Rlt r1 r2) ->(Rlt (Rmult r1 r) (Rmult r2 r)).

Theorem Rlt_compatibility_r:
  (r0, r1, r2:R) (Rlt r1 r2) ->(Rlt (Rplus r1 r0) (Rplus r2 r0)).

Theorem Rle_Rmult_comp:
  (x, y, z, t:R) (Rle R0 x) -> (Rle R0 z) -> (Rle x y) -> (Rle z t) ->
  (Rle (Rmult x z) (Rmult y t)).

Theorem Rlt_Ropp: (x, y:R) (Rlt y x) ->(Rlt (Ropp x) (Ropp y)).

Theorem Ropp_Rlt: (x, y:R) (Rlt (Ropp y) (Ropp x)) ->(Rlt x y).

Theorem Rle_Ropp: (x, y:R) (Rle y x) ->(Rle (Ropp x) (Ropp y)).

Theorem Ropp_Rle: (x, y:R) (Rle (Ropp y) (Ropp x)) ->(Rle x y).

Theorem Rplus_Rminus: (p, q:R)(Rplus p (Rminus q p))==q.

Theorem Rinv_RN: (e:R) ~ e==R0 ->~ (Rinv e)==R0.

Theorem Rinv_Rinv: (e:R) ~ e==R0 ->(Rinv (Rinv e))==e.

Theorem Rmult_Rminus_distr:
  (r1, r2, r3:R)(Rmult r1 (Rminus r2 r3))==(Rminus (Rmult r1 r2) (Rmult r1 r3)).

Theorem Rle_or_lt: (n, m:R)(Rle n m) \/ (Rlt m n).

Theorem le_IZR: (p, q:Z) (Rle (IZR p) (IZR q)) ->(Zle p q).

Theorem Rlt_not: (r1, r2:R) (Rle r2 r1) ->~ (Rlt r1 r2).

Theorem Rlt_mult_anticompatibility:
  (x, y, z:R) (Rlt (Rmult z x) (Rmult z y)) -> (Rlt R0 z) ->(Rlt x y).

Theorem Rle_mult_anticompatibility:
  (x, y, z:R) (Rle (Rmult z x) (Rmult z y)) -> (Rlt R0 z) ->(Rle x y).

Theorem Rmult_anticompatibility:
  (r1, r2, r3:R) ~ r1==R0 -> (Rmult r1 r2)==(Rmult r1 r3) ->r2==r3.

Theorem Rlt_Rinv_R1: (x, y:R) (Rle R1 x) -> (Rlt x y) ->(Rlt (Rinv y) (Rinv x)).

Theorem R1_Rinv: (Rinv R1)==R1.

Theorem Rabsolu_R1: (Rabsolu R1)==R1.

Theorem Rle_antisym: (r, s:R) (Rle r s) -> (Rle s r) ->r==s.

Theorem RabsoluR0Inv: (r:R) (Rle (Rabsolu r) R0) ->r==R0.

Theorem Rminus_Rabsolu:
  (p, q:R) (Rle q p) ->(Rabsolu (Rminus p q))==(Rminus p q).

Theorem Rabsolu_Ropp: (r:R)(Rabsolu (Ropp r))==(Rabsolu r).

Theorem Rabsolu_simpl1: (x:R) (Rle R0 x) ->(Rabsolu x)==x.

Theorem Rabsolu_simpl2: (x:R) (Rle x R0) ->(Rabsolu x)==(Ropp x).

Theorem RabsoluR0: (r:R)(Rle R0 (Rabsolu r)).

Theorem Rabsolu_Rabsolu: (r:R)(Rabsolu (Rabsolu r))==(Rabsolu r).

Theorem Rplus_le:
  (r1, r2, r3, r4:R) (Rle r1 r2) -> (Rle r3 r4) ->
  (Rle (Rplus r1 r3) (Rplus r2 r4)).

Theorem Rmult_Rle_O: (x, y:R) (Rle R0 x) -> (Rle R0 y) ->(Rle R0 (Rmult x y)).

Theorem Rmult_not_zero: (x, y:R) ~ x==R0 -> ~ y==R0 ->~ (Rmult x y)==R0.

Theorem Rle_compatibility_r:
  (r, r1, r2:R) (Rle r1 r2) ->(Rle (Rplus r1 r) (Rplus r2 r)).

Theorem Rle_Rinv: (x, y:R) (Rlt R0 x) -> (Rle x y) ->(Rle (Rinv y) (Rinv x)).

Definition Rmax: R -> R ->R :=
   [x, y:R]
      Cases (total_order_Rle x y) of
          (leftT _) => y
         | (rightT _) => x
      end.

Theorem RmaxLess1: (r1, r2:R)(Rle r1 (Rmax r1 r2)).

Theorem RmaxLess2: (r1, r2:R)(Rle r2 (Rmax r1 r2)).

Theorem RmaxSym: (p, q:R)(Rmax p q)==(Rmax q p).

Theorem RmaxAbs:
  (p, q, r:R) (Rle p q) -> (Rle q r) ->
  (Rle (Rabsolu q) (Rmax (Rabsolu p) (Rabsolu r))).

Theorem RmaxRmult:
  (p, q, r:R) (Rle R0 r) ->(Rmax (Rmult r p) (Rmult r q))==(Rmult r (Rmax p q)).
(* Properties of Z *)

Theorem convert_not_O: (p:positive)~ (convert p)=O.

Theorem inj_abs: (x:Z) (Zle ZERO x) ->(inject_nat (absolu x))=x.

Theorem inject_nat_convert:
  (p:Z) (q:positive) p=(POS q) ->(inject_nat (convert q))=p.

Theorem ZleLe: (x, y:nat) (Zle (INZ x) (INZ y)) ->(le x y).

Theorem inject_nat_eq: (x, y:nat) (inject_nat x)=(inject_nat y) ->x=y.

Theorem Zcompare_EGAL: (p, q:Z) (Zcompare p q)=EGAL ->p=q.

Theorem Zlt_Zopp: (x, y:Z) (Zlt x y) ->(Zlt (Zopp y) (Zopp x)).

Theorem Zle_Zopp: (x, y:Z) (Zle x y) ->(Zle (Zopp y) (Zopp x)).

Theorem absolu_INR: (n:nat)(absolu (inject_nat n))=n.

Theorem absolu_Zopp: (p:Z)(absolu (Zopp p))=(absolu p).

Theorem Zabs_absolu: (z:Z)(Zabs z)=(inject_nat (absolu z)).

Theorem absolu_comp_mult:
  (p, q:Z)(absolu (Zmult p q))=(mult (absolu p) (absolu q)).

Theorem Zmin_sym: (m, n:Z)(Zmin n m)=(Zmin m n).

Theorem Zpower_nat_O: (z:Z)(Zpower_nat z O)=(inject_nat (S O)).

Theorem Zpower_nat_1: (z:Z)(Zpower_nat z (S O))=z.

Theorem Zmin_le1: (z1, z2:Z) (Zle z1 z2) ->(Zmin z1 z2)=z1.

Theorem Zmin_le2: (z1, z2:Z) (Zle z2 z1) ->(Zmin z1 z2)=z2.

Theorem Zmin_Zle:
  (z1, z2, z3:Z) (Zle z1 z2) -> (Zle z1 z3) ->(Zle z1 (Zmin z2 z3)).

Theorem Zminus_n_predm: (n, m:Z)(Zs (Zminus n m))=(Zminus n (Zpred m)).

Theorem Zopp_Zpred_Zs: (z:Z)(Zopp (Zpred z))=(Zs (Zopp z)).

Theorem Zle_mult_gen:
  (x, y:Z) (Zle ZERO x) -> (Zle ZERO y) ->(Zle ZERO (Zmult x y)).

Definition Zmax: (_, _:Z)Z :=
   [n, m:Z]
      Cases (Zcompare n m) of
          EGAL => m
         | INFERIEUR => m
         | SUPERIEUR => n
      end.

Theorem ZmaxLe1: (z1, z2:Z)(Zle z1 (Zmax z1 z2)).

Theorem ZmaxSym: (z1, z2:Z)(Zmax z1 z2)=(Zmax z2 z1).

Theorem Zmax_le2: (z1, z2:Z) (Zle z1 z2) ->(Zmax z1 z2)=z2.

Theorem Zmax_le1: (z1, z2:Z) (Zle z2 z1) ->(Zmax z1 z2)=z1.

Theorem ZmaxLe2: (z1, z2:Z)(Zle z2 (Zmax z1 z2)).

Theorem Zeq_Zs: (p, q:Z) (Zle p q) -> (Zlt q (Zs p)) ->p=q.

Theorem Zmin_Zmax: (z1, z2:Z)(Zle (Zmin z1 z2) (Zmax z1 z2)).

Theorem Zabs_Zmult: (z1, z2:Z)(Zabs (Zmult z1 z2))=(Zmult (Zabs z1) (Zabs z2)).

Theorem Zle_Zmult_comp_r:
  (x, y, z:Z) (Zle ZERO z) -> (Zle x y) ->(Zle (Zmult x z) (Zmult y z)).

Theorem Zle_Zmult_comp_l:
  (x, y, z:Z) (Zle ZERO z) -> (Zle x y) ->(Zle (Zmult z x) (Zmult z y)).
(* Conversions from R <-> Z  <-> N *)

Theorem IZR_zero: (p:Z) p=ZERO ->(IZR p)==R0.

Theorem IZR_zero_r: (p:Z) (IZR p)==R0 ->p=ZERO.

Theorem Rminus_IZR: (z, t:Z)(IZR (Zminus z t))==(Rminus (IZR z) (IZR t)).

Theorem Rlt_INR: (n, m:nat) (lt n m) ->(Rlt (INR n) (INR m)).

Theorem Rlt_INR0: (n:nat) (lt O n) ->(Rlt R0 (INR n)).

Theorem Rlt_INR1: (n:nat) (lt (S O) n) ->(Rlt R1 (INR n)).

Theorem NEq_INR: (n, m:nat) ~ n=m ->~ (INR n)==(INR m).

Theorem NEq_INRO: (n:nat) ~ n=O ->~ (INR n)==R0.

Theorem NEq_INR1: (n:nat) ~ n=(S O) ->~ (INR n)==R1.

Theorem not_O_lt: (n:nat) ~ n=O ->(lt O n).

Theorem Rlt_IZR: (p, q:Z) (Zlt p q) ->(Rlt (IZR p) (IZR q)).

Theorem Rle_IZR: (x, y:Z) (Zle x y) ->(Rle (IZR x) (IZR y)).

Theorem lt_Rlt: (n, m:nat) (Rlt (INR n) (INR m)) ->(lt n m).

Theorem INR_inv: (n, m:nat) (INR n)==(INR m) ->n=m.

Theorem Rle_INR: (x, y:nat) (le x y) ->(Rle (INR x) (INR y)).

Theorem le_Rle: (n, m:nat) (Rle (INR n) (INR m)) ->(le n m).

Theorem Rmult_INR: (n, m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)).

Theorem Rmult_IZR: (z, t:Z)(IZR (Zmult z t))==(Rmult (IZR z) (IZR t)).

Theorem absolu_Zs: (z:Z) (Zle ZERO z) ->(absolu (Zs z))=(S (absolu z)).

Theorem Zlt_next: (n, m:Z) (Zlt n m) ->m=(Zs n) \/ (Zlt (Zs n) m).

Theorem Zle_next: (n, m:Z) (Zle n m) ->m=n \/ (Zle (Zs n) m).

Theorem Zlt_Zopp_Inv: (p, q:Z) (Zlt (Zopp p) (Zopp q)) ->(Zlt q p).

Theorem Zle_Zopp_Inv: (p, q:Z) (Zle (Zopp p) (Zopp q)) ->(Zle q p).

Theorem absolu_Zs_neg:
  (z:Z) (Zlt z ZERO) -><nat> (S (absolu (Zs z)))=(absolu z).

Theorem Zlt_absolu: (x:Z) (n:nat) (lt (absolu x) n) ->(Zlt x (inject_nat n)).

Theorem inj_pred: (n:nat) ~ n=O ->(inject_nat (pred n))=(Zpred (inject_nat n)).

Theorem Zle_abs: (p:Z)(Zle p (inject_nat (absolu p))).

Theorem ZleAbs:
  (z:Z) (n:nat) (Zle (Zopp (inject_nat n)) z) -> (Zle z (inject_nat n)) ->
  (le (absolu z) n).

Theorem Rabsolu_Zabs: (z:Z)(Rabsolu (IZR z))==(IZR (Zabs z)).

Theorem lt_Zlt_inv: (n, m:nat) (Zlt (INZ n) (INZ m)) ->(lt n m).

Theorem NconvertO: (p:positive)~ (convert p)=O.

Theorem absolu_lt_nz: (z:Z) ~ z=ZERO ->(lt O (absolu z)).

Theorem Rlt2: (Rlt R0 (INR (S (S O)))).

Theorem RlIt2: (Rlt R0 (Rinv (INR (S (S O))))).

Theorem Rledouble: (r:R) (Rle R0 r) ->(Rle r (Rmult (INR (S (S O))) r)).

Theorem Rltdouble: (r:R) (Rlt R0 r) ->(Rlt r (Rmult (INR (2)) r)).

Theorem Rlt_RinvDouble: (r:R) (Rlt R0 r) ->(Rlt (Rmult (Rinv (INR (2))) r) r).

Theorem Int_part_INR: (n:nat)(Int_part (INR n))=(inject_nat n).

Theorem Ropp_Zopp: (z:Z)(Ropp (IZR z))==(IZR (Zopp z)).

Theorem Rle_lt: (r1, r2:R) (Rle r1 r2) -> ~ <R> r1==r2 ->(Rlt r1 r2).

Theorem Rle_Rabs: (x:R)(Rle x (Rabsolu x)).

30/05/01, 17:44