Restructure theorem and lemmas

Author: InnovativeInventor

coq_error_metrics/_CoqProject

@@ -1,3 +1,5 @@
 -Q . ErrorMetrics
 
+lemmas.v
 absolute_prec.v
+relative_prec.v

coq_error_metrics/absolute_prec.v

@@ -1,11 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import mathcomp_extra exp reals signed.
-From mathcomp Require Import boolp Rstruct.
-
-From mathcomp.algebra_tactics Require Import ring lra. 
-
-Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-
+Require Import ErrorMetrics.lemmas.
 Local Open Scope ring_scope.
 
 Section AbsPrec.
@@ -18,13 +11,10 @@ End AbsPrec.
 
 Notation "a ~ a' ; ap( α )" := (AbsPrec a a' α) (at level 99).
 
-Fact abs_eq : forall {R : realType} (a b : R), a = b -> `|a| = `|b|. 
-Proof. move => HR a b H1; by rewrite H1. Qed.
-
 (* Properties from Olver Section 2.2 *)
 Section APElementaryProperties.
-
   Context {R : realType}.
+
   Variables (a a' α : R). 
   Hypothesis Halpha : 0 <= α.  
 
@@ -143,121 +133,3 @@ Hypothesis Hbeta  : 0 <= β.
 End MultDiv2.
 
 
-Section RelPrec.
-
-  Context {R : realType}.
-
-  Definition NonZeroSameSign (a b : R) : Prop :=
-    (a > 0 /\ b > 0) \/ (a < 0 /\ b < 0).
-
-  Lemma NonZeroSameSignMul (a b : R) :
-    forall k, k != 0 ->
-              (NonZeroSameSign (k * a) (k * b) -> NonZeroSameSign a b).
-  Proof. Admitted.
-
-  Definition RelPrec (a a' α : R) : Prop :=
-    α >= 0 -> NonZeroSameSign a a' ->
-    `|ln(a / a')| <= α.
-
-End RelPrec.
-
-Notation "a ~ a' ; rp( α )" := (RelPrec a a' α) (at level 99).
-
-(* Section 3.2. *)
-Section RPElementaryProperties.
-
-  Context {R : realType}.
-  Variables (a a' α : R).
-  Hypothesis Halpha : 0 <= α.
-
-  (* Proof. rewrite /AbsPrec. move => H1 H2.  *)
-  (*        rewrite Num.Theory.distrC H1 => //=. Qed. *)
-  Theorem RPProp1 : (a ~ a' ; rp(α)) -> (a' ~ a ; rp(α)).
-  Proof. rewrite /RelPrec /NonZeroSameSign.
-         move=> H1 H2 H3.
-         suff sym : ((`|ln (R:=R) (a' / a)|) = `|ln (R:=R) (a / a')|).
-         rewrite sym.
-         apply: H1.
-         done.
-         destruct H3; auto; destruct H; try split; auto.
-         suff inv_neg : (ln (R:=R) (a' / a) =  - 1 * ln (R:=R) (a / a')).
-         rewrite inv_neg.
-         suff neg_1_swap : ( - 1 * ln (R:=R) (a / a') = - ln (R:=R) (a / a')).
-         rewrite neg_1_swap.
-         apply: normrN.
-         apply: mulN1r.
-         rewrite - (GRing.invf_div a a').
-         rewrite - ln_powR.
-         rewrite powRN.
-         rewrite powRr1.
-         reflexivity.
-         case: H3.
-         move=> [Ha' Ha].
-         apply: divr_ge0.
-         by [lra].
-         by [lra].
-         move=> [Ha' Ha].
-         suff temp: 0 <= (- a) / (- a') by lra.
-         suff neg_a: 0 <= - a'.
-         suff neg_a': 0 <= - a.
-         apply: divr_ge0; lra.
-         by [lra].
-         by [lra].
-         Qed.
-
-  Theorem RPProp2 : forall (δ : R), (a ~ a' ; rp(α)) -> 0 <= α -> α <= δ -> (a ~ a' ; rp(δ)).
-  Proof. rewrite /RelPrec.
-         move=> del H2 H3 H4 H5 H6.
-         rewrite (@le_trans _ _ α) => //. rewrite H2 => //=. Qed.
-
-  Theorem RPProp3 : forall (k : R), (a ~ a'; rp(α)) -> k != 0 -> (k * a ~ k * a' ; rp(α)).
-  Proof. rewrite /RelPrec; move => k H1 H2 H3 H4.
-         rewrite (abs_eq _ (ln (a / a'))).
-         apply H1 => //.
-         apply (NonZeroSameSignMul _ _ k) => //.
-         rewrite -mulf_div.
-         rewrite divff => //.
-         f_equal.
-         lra. Qed.
-
-  Fact RPabs_mul_eq : forall (k : R), `|k * a| = `|k| * `|a|.
-  Proof. Admitted.
-
-  Theorem RPProp4 : forall (k : R), (a ~ a' ; rp(α)) -> 0 <= α -> a*k ~ a'*k ; rp(`|k|*α).
-  Proof. Admitted.
-
-  Lemma RPProp4_1 :  a ~ a' ; rp(α) -> -a ~ -a' ; rp(α).
-  Proof. Admitted.
-
-  Theorem RPProp5 : forall (b b' β : R),
-      a ~ a' ; rp(α) ->  b ~ b' ; rp(β) -> 0 <= β -> a + b ~ a' + b' ; rp(α + β).
-  Proof. Admitted.
-
-  Theorem RPProp6 : forall (a'' δ : R ),
-      a ~ a' ; rp(α) -> a' ~ a'' ; rp(δ) -> 0 <= δ -> a ~ a'' ; rp(α + δ).
-  Proof. Admitted.
-
-End RPElementaryProperties.
-
-(* Section 3.3 *)
-Section RPAddSub.
-  Context {R : realType}.
-  Variables (a a' b b' α β : R).
-
-  Variables (e : R).
-  (* change with canonical def in mathcomp *)
-  Parameter e_is_e : ln(e) = 1.
-
-  Hypothesis Halpha : 0 <= α.
-
-  (* Theorem 3.1 *)
-  Theorem RPAdd : a ~ a' ; rp(α) -> b ~ b' ; rp(β) ->
-                  a + b ~ a' + b'; rp(ln(a' * (e `^ α) +  b * (e `^ β) / (a' + b') )).
-    Admitted.
-
-  (* Theorem 3.2 *)
-  Theorem RPSub : a ~ a' ; rp(α) -> b ~ b' ; rp(β) -> `|a'| * (e `^ -α) > `|b'| * (e `^ β) ->
-                  a + b ~ a' + b'; rp(ln(a' * (e `^ α) -  b * (e `^ -β) / (a' - b') )).
-    Admitted.
-
-End RPAddSub.

coq_error_metrics/lemmas.v

@@ -0,0 +1,33 @@
+From mathcomp Require Export all_ssreflect ssralg ssrnum.
+From mathcomp Require Export mathcomp_extra exp reals signed.
+From mathcomp Require Export boolp Rstruct.
+
+From mathcomp.algebra_tactics Require Export ring lra.
+
+Export Order.TTheory GRing.Theory Num.Def Num.Theory.
+
+Local Open Scope ring_scope.
+
+Section HelperLemmas.
+  Context {R : realType}.
+
+  Fact abs_eq : forall (a b : R), a = b -> `|a| = `|b|.
+  Proof. move => a b H1; by rewrite H1. Qed.
+
+  Definition NonZeroSameSign (a b : R) : Prop :=
+    (a > 0 /\ b > 0) \/ (a < 0 /\ b < 0).
+
+  Lemma NonZeroSameSignMul : forall (a b : R),
+    forall k, k != 0 ->
+              (NonZeroSameSign (k * a) (k * b) -> NonZeroSameSign a b).
+  Proof. Admitted.
+
+  Lemma NonZeroSameSignExp : forall (a b : R),
+    forall k, (NonZeroSameSign (a `^ k) (b `^ k) -> NonZeroSameSign a b).
+  Proof. Admitted.
+
+
+  Lemma le_mul_pos : forall (k a b : R), a <= b -> (`|k| * a <= `|k| * b). Admitted.
+  Lemma norm_mul_split : forall (a b : R), `| a * b | = `| a | * `| b |. Admitted.
+  Lemma factor_exp : forall (a a' b k : R), (a `^ k / a' `^ k = (a / a') `^ k). Admitted.
+End HelperLemmas.

coq_error_metrics/relative_prec.v

@@ -0,0 +1,114 @@
+Require Import ErrorMetrics.lemmas.
+Local Open Scope ring_scope.
+
+Section RelPrec.
+
+  Context {R : realType}.
+
+  Definition RelPrec (a a' α : R) : Prop :=
+    α >= 0 -> NonZeroSameSign a a' ->
+    `|ln(a / a')| <= α.
+
+End RelPrec.
+
+Notation "a ~ a' ; rp( α )" := (RelPrec a a' α) (at level 99).
+
+(* Section 3.2. *)
+Section RPElementaryProperties.
+
+  Context {R : realType}.
+  Variables (a a' α : R).
+  Hypothesis Halpha : 0 <= α.
+
+  Theorem RPProp1 : (a ~ a' ; rp(α)) -> (a' ~ a ; rp(α)).
+  Proof. rewrite /RelPrec /NonZeroSameSign.
+         move=> H1 H2 H3.
+         suff sym : ((`|ln (R:=R) (a' / a)|) = `|ln (R:=R) (a / a')|).
+         rewrite sym.
+         apply: H1.
+         done.
+         destruct H3; auto; destruct H; try split; auto.
+         suff inv_neg : (ln (R:=R) (a' / a) =  - 1 * ln (R:=R) (a / a')).
+         rewrite inv_neg.
+         suff neg_1_swap : ( - 1 * ln (R:=R) (a / a') = - ln (R:=R) (a / a')).
+         rewrite neg_1_swap.
+         apply: normrN.
+         apply: mulN1r.
+         rewrite - (GRing.invf_div a a').
+         rewrite - ln_powR.
+         rewrite powRN.
+         rewrite powRr1.
+         reflexivity.
+         case: H3.
+         move=> [Ha' Ha].
+         apply: divr_ge0.
+         by [lra].
+         by [lra].
+         move=> [Ha' Ha].
+         suff temp: 0 <= (- a) / (- a') by lra.
+         suff neg_a: 0 <= - a'.
+         suff neg_a': 0 <= - a.
+         apply: divr_ge0; lra.
+         by [lra].
+         by [lra].
+         Qed.
+
+  Theorem RPProp2 : forall (δ : R), (a ~ a' ; rp(α)) -> 0 <= α -> α <= δ -> (a ~ a' ; rp(δ)).
+  Proof. rewrite /RelPrec.
+         move=> del H2 H3 H4 H5 H6.
+         rewrite (@le_trans _ _ α) => //. rewrite H2 => //=. Qed.
+
+  Theorem RPProp3 : forall (k : R), (a ~ a'; rp(α)) -> k != 0 -> (k * a ~ k * a' ; rp(α)).
+  Proof. rewrite /RelPrec; move => k H1 H2 H3 H4.
+         rewrite (abs_eq _ (ln (a / a'))).
+         apply H1 => //.
+         apply (NonZeroSameSignMul _ _ k) => //.
+         rewrite -mulf_div.
+         rewrite divff => //.
+         f_equal.
+         lra. Qed.
+
+  Theorem RPProp4 : forall (k : R), (a ~ a' ; rp(α)) -> 0 <= α -> a `^ k ~ a' `^ k ; rp(`|k|*α).
+  Proof. rewrite /RelPrec. move => k H1 H2 H3 H4.
+         rewrite factor_exp. rewrite ln_powR.
+         rewrite norm_mul_split.
+         suff key_rel : `|ln (R:=R) (a / a')| <= α.
+         apply (le_mul_pos k _ _) => //.
+         apply H1 => //=.
+         Check NonZeroSameSignMul.
+         apply (NonZeroSameSignExp a a' k) => //.
+         give_up.
+  Admitted.
+
+  Theorem RPProp5 : forall (b b' β : R),
+      a ~ a' ; rp(α) ->  b ~ b' ; rp(β) -> 0 <= β -> a * b ~ a' * b' ; rp(α + β).
+  Proof. Admitted.
+
+  Theorem RPProp6 : forall (a'' δ : R ),
+      a ~ a' ; rp(α) -> a' ~ a'' ; rp(δ) -> 0 <= δ -> a ~ a'' ; rp(α + δ).
+  Proof. Admitted.
+
+End RPElementaryProperties.
+
+(* Section 3.3 *)
+Section RPAddSub.
+  Context {R : realType}.
+  Variables (a a' b b' α β : R).
+
+  Variables (e : R).
+  (* change with canonical def in mathcomp *)
+  Parameter e_is_e : ln(e) = 1.
+
+  Hypothesis Halpha : 0 <= α.
+
+  (* Theorem 3.1 *)
+  Theorem RPAdd : a ~ a' ; rp(α) -> b ~ b' ; rp(β) ->
+                  a + b ~ a' + b'; rp(ln(a' * (e `^ α) +  b * (e `^ β) / (a' + b') )).
+    Admitted.
+
+  (* Theorem 3.2 *)
+  Theorem RPSub : a ~ a' ; rp(α) -> b ~ b' ; rp(β) -> `|a'| * (e `^ -α) > `|b'| * (e `^ β) ->
+                  a + b ~ a' + b'; rp(ln(a' * (e `^ α) -  b * (e `^ -β) / (a' - b') )).
+    Admitted.
+
+End RPAddSub.