Rpower.v

(****************************************************************************                                                                                         IEEE754  :  Rpower                                                                                                                                          Laurent Thery                                                                                                                                     ***************************************************************************** Definition of an exponential function over relative numbers *)
Require Import Omega.
Require Import Reals.
Require Import Zpower.
Require Import fast_integer.
Require Import Digit.
Require Import Faux.
Require Import sTactic.
(* We have already an exponential over natural number,    we prove some basic properties for this function *)

Theorem pow_O: (e:R)(pow e O)==R1.
Simpl; Auto with real.
Qed.

Theorem pow_1: (e:R)(pow e (1))==e.
Simpl; Auto with real.
Qed.

Theorem pow_NR0: (e:R) (n:nat) ~ e==R0 ->~ (pow e n)==R0.
Intros e n; Elim n; Simpl; Auto with real.
Intros n0 H' H'0; Red; Intros H'1.
Case without_div_Od with 1 := H'1; Auto with real.
Intuition.
Qed.

Theorem pow_add:
  (e:R) (n, m:nat)(pow e (plus n m))==(Rmult (pow e n) (pow e m)).
Intros e n; Elim n; Simpl; Auto with real.
Intros n0 H' m; Rewrite H'; Auto with real.
Qed.
Hints Resolve pow_O pow_1 pow_NR0 pow_add :real.

Theorem pow_is_exp_on_nat: (n, m:nat)(pow (INR n) m)==(INR (exp n m)).
Intros n m; Elim m; Simpl; Auto with real.
Intros n0 H'; Rewrite H'; Auto with real.
Qed.

Theorem pow_RN_plus:
  (e:R) (n, m:nat) ~ e==R0 ->
  (pow e n)==(Rmult (pow e (plus n m)) (Rinv (pow e m))).
Intros e n; Elim n; Simpl; Auto with real.
Intros m H'; AutoRewrite [Rsimpl]; Auto with real.
Intros n0 H' m H'0.
Rewrite Rmult_assoc; Rewrite <- H'; Auto.
Qed.

Theorem pow_lt: (e:R) (n:nat) (Rlt R0 e) ->(Rlt R0 (pow e n)).
Intros e n; Elim n; Simpl; Auto with real.
Intros n0 H' H'0; Replace R0 with (Rmult e R0); Auto with real.
Qed.
Hints Resolve pow_lt :real.

Theorem Rlt_pow_R1: (e:R) (n:nat) (Rlt R1 e) -> (lt O n) ->(Rlt R1 (pow e n)).
Intros e n; Elim n; Simpl; Auto.
Intros H' H'0; Contradict H'0; Auto with arith.
Intros n0; Case n0.
Simpl; AutoRewrite [Rsimpl]; Auto.
Intros n1 H' H'0 H'1.
Replace R1 with (Rmult R1 R1).
Apply Rlt_trans with r2 := (Rmult e R1); Auto with real.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_monotony; Auto with real.
Apply Rlt_trans with r2 := R1; Auto with real.
Apply H'; Auto with arith.
AutoRewrite [Rsimpl]; Auto.
Qed.
Hints Resolve Rlt_pow_R1 :real.

Theorem Rlt_pow:
  (e:R) (n, m:nat) (Rlt R1 e) -> (lt n m) ->(Rlt (pow e n) (pow e m)).
Intros e n m H' H'0; Replace m with (plus (minus m n) n).
Rewrite pow_add.
Pattern 1 (pow e n); Replace (pow e n) with (Rmult R1 (pow e n)); Auto with real.
Apply Rminus_lt.
Repeat Rewrite [x:R](Rmult_sym x (pow e n)); Rewrite <- Rmult_Rminus_distr.
Replace R0 with (Rmult (pow e n) R0); Auto with real.
Apply Rlt_monotony; Auto with real.
Apply pow_lt; Auto with real.
Apply Rlt_trans with r2 := R1; Auto with real.
Apply Rlt_minus; Auto with real.
Apply Rlt_pow_R1; Auto with arith.
Apply simpl_lt_plus_l with p := n; Auto with arith.
Rewrite le_plus_minus_r; Auto with arith; Rewrite <- plus_n_O; Auto.
Rewrite plus_sym; Auto with arith.
Qed.
Hints Resolve Rlt_pow :real.

Theorem pow_abs: (r:R) (n:nat)(Rabsolu (pow r n))==(pow (Rabsolu r) n).
Intros r n; Elim n; Simpl; AutoRewrite [Rsimpl]; Auto.
Intros n0 H'; AutoRewrite [Rsimpl]; Auto with real.
Qed.

Theorem pow_inv: (r:R) (n:nat) ~ r==R0 ->(Rinv (pow r n))==(pow (Rinv r) n).
Intros r n; Elim n; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Intros n0 H' H'0; Rewrite <- H'; AutoRewrite [Rsimpl]; Auto with real.
Qed.

Theorem pow_R1: (r:R) (n:nat) (pow r n)==R1 ->(Rabsolu r)==R1 \/ n=O.
Intros r n H'.
Case (Req_EM (Rabsolu r) R1); Auto; Intros H'1.
Case (not_Req ? ? H'1); Intros H'2.
Generalize H'; Case n; Auto.
Intros n0 H'0.
Cut ~ r==R0; [Intros Eq1 | Idtac].
2:Contradict H'0; Auto with arith.
2:Simpl; Rewrite H'0; Rewrite Rmult_Ol; Auto with real.
Cut ~ (Rabsolu r)==R0; [Intros Eq2 | Apply Rabsolu_no_R0]; Auto.
Absurd (Rlt (pow (Rabsolu (Rinv r)) O) (pow (Rabsolu (Rinv r)) (S n0))); Auto.
Replace (pow (Rabsolu (Rinv r)) (S n0)) with R1.
Simpl; Apply Rlt_antirefl; Auto.
AutoRewrite [Rsimpl]; Auto with real.
Rewrite <- pow_inv; Auto.
Rewrite <- pow_abs; Auto.
Rewrite H'0; AutoRewrite [Rsimpl]; Auto with real.
Apply Rlt_pow; Auto with arith.
AutoRewrite [Rsimpl]; Auto with real.
Rewrite <- R1_Rinv; Auto with real.
Apply Rlt_mult_anticompatibility with z := (Rabsolu r).
AutoRewrite [Rsimpl]; Auto with real.
Case (Rabsolu_pos r); Auto.
Intros H'3; Case Eq2; Auto.
Generalize H'; Case n; Auto.
Intros n0 H'0.
Cut ~ r==R0; [Intros Eq1 | Idtac].
2:Contradict H'0; Auto with arith.
2:Simpl; Rewrite H'0; AutoRewrite [Rsimpl]; Auto with real.
Cut ~ (Rabsolu r)==R0; [Intros Eq2 | Apply Rabsolu_no_R0]; Auto.
Absurd (Rlt (pow (Rabsolu r) O) (pow (Rabsolu r) (S n0))); Auto with real arith.
Repeat Rewrite <- pow_abs; Rewrite H'0; Simpl; AutoRewrite [Rsimpl];
Auto with real.
Qed.

(* To define exponential over relative number, we simply do    a case analysis on the sign of the number *)

Definition powerRZ :=
   [e:R] [n:Z]
      Cases n of
          ZERO => R1
         | (POS p) => (pow e (convert p))
         | (NEG p) => (Rinv (pow e (convert p)))
      end.
(* we now prove some basic properties of our exponential *)

Theorem powerRZ_O: (e:R)(powerRZ e ZERO)==R1.
Simpl; Auto.
Qed.

Theorem powerRZ_1: (e:R)(powerRZ e (Zs ZERO))==e.
Simpl; Auto with real.
Qed.

Theorem powerRZ_NOR: (e:R) (z:Z) ~ e==R0 ->~ (powerRZ e z)==R0.
Intros e z; Case z; Simpl; Auto with real.
Qed.
Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR :real.

Theorem powerRZ_add:
  (e:R) (n, m:Z) ~ e==R0 ->
  (powerRZ e (Zplus n m))==(Rmult (powerRZ e n) (powerRZ e m)).
Intros e n m; Case n; Case m; Simpl; Auto with real.
Intros n1 m1; Rewrite convert_add; Auto with real.
Intros n1 m1; CaseEq (compare m1 n1 EGAL); Simpl; Auto with real.
Intros H' H'0; Rewrite compare_convert_EGAL with 1 := H'; Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Intros H' H'0; Rewrite (true_sub_convert n1 m1); Auto with real.
Rewrite (pow_RN_plus e (minus (convert n1) (convert m1)) (convert m1));
Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
Apply lt_le_weak.
Apply compare_convert_INFERIEUR; Auto.
Apply ZC2; Auto.
Intros H' H'0; Rewrite (true_sub_convert m1 n1); Auto with real.
Rewrite (pow_RN_plus e (minus (convert m1) (convert n1)) (convert n1));
Auto with real.
Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
Apply lt_le_weak.
Change (gt (convert m1) (convert n1)).
Apply compare_convert_SUPERIEUR; Auto.
Intros n1 m1; CaseEq (compare m1 n1 EGAL); Simpl; Auto with real.
Intros H' H'0; Rewrite compare_convert_EGAL with 1 := H'; Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Intros H' H'0; Rewrite (true_sub_convert n1 m1); Auto with real.
Rewrite (pow_RN_plus e (minus (convert n1) (convert m1)) (convert m1));
Auto with real.
Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
Apply lt_le_weak.
Apply compare_convert_INFERIEUR; Auto.
Apply ZC2; Auto.
Intros H' H'0; Rewrite (true_sub_convert m1 n1); Auto with real.
Rewrite (pow_RN_plus e (minus (convert m1) (convert n1)) (convert n1));
Auto with real.
Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Apply lt_le_weak.
Change (gt (convert m1) (convert n1)).
Apply compare_convert_SUPERIEUR; Auto.
Intros n1 m1; Rewrite convert_add; Auto with real.
Intros H'; Rewrite pow_add; Auto with real.
Apply Rinv_Rmult; Auto.
Apply pow_NR0; Auto.
Apply pow_NR0; Auto.
Qed.
Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add :real.

Theorem powerRZ_Zs:
  (e:R) (n:Z) ~ e==R0 ->(powerRZ e (Zs n))==(Rmult e (powerRZ e n)).
Intros e n H'0.
Replace (Zs n) with (Zplus n (Zs ZERO)).
Rewrite powerRZ_add; Auto.
Rewrite powerRZ_1.
Rewrite Rmult_sym; Auto.
Auto with zarith.
Qed.
(* Conversion theorem between relative numbers and reals *)

Theorem Zpower_nat_powerRZ:
  (n, m:nat)
  (IZR (Zpower_nat (inject_nat n) m))==(powerRZ (INR n) (inject_nat m)).
Intros n m; Elim m; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Intros m1 H'; Rewrite bij1; Simpl.
Replace (Zpower_nat (inject_nat n) (S m1))
     with (Zmult (inject_nat n) (Zpower_nat (inject_nat n) m1)).
AutoRewrite [Rsimpl]; Auto with real.
Rewrite H'; Auto with real.
Case m1; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Intros m2; Rewrite bij1; Auto.
Unfold Zpower_nat; Auto.
Qed.

Theorem powerRZ_lt: (e:R) (z:Z) (Rlt R0 e) ->(Rlt R0 (powerRZ e z)).
Intros e z; Case z; Simpl; Auto with real.
Intros p H'.
Case (total_order R0 (Rinv (pow e (convert p)))); Auto;
(Intros temp; Case temp; Clear temp; Intros Le0).
Absurd (Rmult (Rinv (pow e (convert p))) (pow e (convert p)))==R1;
Auto with real.
Rewrite <- Le0; AutoRewrite [Rsimpl]; Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Apply pow_NR0; Auto.
Apply imp_not_Req; Auto.
Absurd (Rle R1 R0); Auto with real.
Apply Rlt_le.
Replace (Rlt R1 R0)
     with (Rlt
             (Rmult (pow e (convert p)) (Rinv (pow e (convert p))))
             (Rmult (pow e (convert p)) R0)); Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Apply pow_NR0; Auto with real.
Apply imp_not_Req; Auto.
Qed.
Hints Resolve powerRZ_lt :real.

Theorem powerRZ_le: (e:R) (z:Z) (Rlt R0 e) ->(Rle R0 (powerRZ e z)).
Intros e z H'; Apply Rlt_le; Auto with real.
Qed.
Hints Resolve powerRZ_le :real.

Theorem Rlt_powerRZ:
  (e:R) (n, m:Z) (Rlt R1 e) -> (Zlt n m) ->(Rlt (powerRZ e n) (powerRZ e m)).
Intros e n m; Case n; Case m; Simpl; Try (Unfold Zlt; Intros; Discriminate);
Auto with real.
Intros p H' H'1; Apply Rlt_pow_R1; Auto with real.
Generalize (convert_not_O p); Case (convert p); Auto with arith.
Intros p p0 H' H'0; Apply Rlt_pow; Auto with real.
Apply compare_convert_INFERIEUR; Auto.
Intros p H' H'0; Replace R1 with (Rinv R1); Auto with real.
Apply Rlt_Rinv_R1; Auto with real.
Apply Rlt_pow_R1; Auto with real.
Generalize (convert_not_O p); Case (convert p); Auto with arith.
Intros p p0 H' H'0; Apply Rlt_trans with r2 := R1.
Replace R1 with (Rinv R1); Auto with real.
Apply Rlt_Rinv_R1; Auto with real.
Apply Rlt_pow_R1; Auto with real.
Generalize (convert_not_O p0); Case (convert p0); Auto with arith.
Apply Rlt_pow_R1; Auto with real.
Generalize (convert_not_O p); Case (convert p); Auto with arith.
Intros p p0 H' H'0; Apply Rlt_Rinv_R1; Auto with real.
Apply Rlt_le.
Apply Rlt_pow_R1; Auto with real.
Generalize (convert_not_O p); Case (convert p); Auto with arith.
Apply Rlt_pow; Auto with real.
Apply compare_convert_INFERIEUR; Rewrite ZC4; Auto.
Qed.
Hints Resolve Rlt_powerRZ :real.

Theorem Rpow_R1:
  (r:R) (z:Z) ~ r==R0 -> (powerRZ r z)==R1 ->(Rabsolu r)==R1 \/ z=ZERO.
Intros r z; Case z; Simpl; Auto; Intros p H' H'1; Left.
Case (pow_R1 ? ? H'1); Auto.
Intros H'0; Contradict H'0; Auto with zarith; Apply convert_not_O.
Rewrite pow_inv in H'1; Auto.
Case (pow_R1 ? ? H'1); Auto.
Intros H'0.
Rewrite <- H'0.
Apply r_Rmult_mult with r := R1; Auto with real.
Pattern 1 R1; Rewrite <- H'0; Auto with real.
AutoRewrite [Rsimpl]; Auto with real.
Rewrite <- H'0; AutoRewrite [Rsimpl]; Auto with real.
Apply Rabsolu_no_R0; Auto.
Intros H'0; Contradict H'0; Auto with zarith; Apply convert_not_O.
Qed.

Theorem Rpow_eq_inv:
  (r:R) (p, q:Z) ~ r==R0 -> ~ (Rabsolu r)==R1 -> (powerRZ r p)==(powerRZ r q) ->
  p=q.
Intros r p q H' H'0 H'1.
Cut (powerRZ r (Zminus p q))==R1; [Intros Eq0 | Idtac].
Case (Rpow_R1 ? ? H' Eq0); Auto with zarith.
Intros H'2; Case H'0; Auto.
Apply r_Rmult_mult with r := (powerRZ r q); Auto with real.
Rewrite <- powerRZ_add; Auto.
Replace (Zplus q (Zminus p q)) with p; AutoRewrite [Rsimpl]; Auto with zarith.
Qed.

Theorem Zpower_nat_powerRZ_absolu:
  (n, m:Z) (Zle ZERO m) ->(IZR (Zpower_nat n (absolu m)))==(powerRZ (IZR n) m).
Intros n m; Case m; Simpl; Auto with zarith.
Intros p H'; Elim (convert p); Simpl; Auto with zarith.
Intros n0 H'0; Rewrite <- H'0; Simpl; Auto with zarith.
Rewrite <- Rmult_IZR; Auto.
Intros p H'; Contradict H'; Auto with zarith.
Qed.

Theorem absolu_comp_Rpower:
  (p:Z) (n:nat)(absolu (Zpower_nat p n))=(exp (absolu p) n).
Intros p n; Elim n; Simpl.
Unfold convert; Simpl; Auto.
Intros n0 H'; Replace (S n0) with (plus (1) n0); Auto.
Rewrite Zpower_nat_is_exp; Rewrite absolu_comp_mult; Simpl.
Rewrite <- H'; Unfold Zpower_nat; Simpl; Rewrite Zmult_sym; Simpl; Case p;
Auto with zarith.
Qed.

Theorem powerRZ_R1: (n:Z)(powerRZ R1 n)==R1.
Intros n; Case n; Simpl; Auto.
Intros p; Elim (convert p); Simpl; Auto; Intros n0 H'; Rewrite H'; Ring.
Intros p; Elim (convert p); Simpl.
Exact R1_Rinv.
Intros n H'; Rewrite Rinv_Rmult; Try Rewrite R1_Rinv; Try Rewrite H';
Auto with real.
Qed.

Theorem Rle_powerRZ:
  (e:R) (n, m:Z) (Rle R1 e) -> (Zle n m) ->(Rle (powerRZ e n) (powerRZ e m)).
Intros e n m H' H'0.
Case H'; Intros E1.
Case (Zle_lt_or_eq ? ? H'0); Intros E2.
Apply Rlt_le; Auto with real.
Rewrite <- E2; Auto with real.
Repeat Rewrite <- E1; Repeat Rewrite powerRZ_R1; Auto with real.
Qed.
(* Conversion theorem between natural numbers and reals *)

Theorem powerRZ_is_exp:
  (m, n:nat) (lt O m) ->(powerRZ (INR m) (INZ n))==(INR (exp m n)).
Intros m n.
Elim n; Auto.
Intros n0 H' H'1.
Replace (INZ (S n0)) with (Zplus (INZ n0) (INZ (1))).
Rewrite powerRZ_add; Auto.
Rewrite H'; Auto.
Simpl; AutoRewrite [Rsimpl]; Auto with real.
Red; Intros H'0; Absurd (Rlt (INR O) (INR m)); Auto with real.
Rewrite H'0; Simpl; Auto with real.
Rewrite <- inj_plus.
Auto with zarith.
Qed.

10/11/100, 17:24