Strengthen RP def; add proof of property 5

Author: InnovativeInventor

coq_error_metrics/lemmas.v

@@ -17,17 +17,35 @@ Section HelperLemmas.
   Definition NonZeroSameSign (a b : R) : Prop :=
     (a > 0 /\ b > 0) \/ (a < 0 /\ b < 0).
 
+  Lemma NonZeroSameSignMulGen : forall (a a' b b' : R),
+    (NonZeroSameSign a a') -> (NonZeroSameSign b b') ->(NonZeroSameSign (a * b) (a' * b')).
+  Proof. Admitted.
+
+  (* TODO: prove that it is reflexive + derive the following from the above lemma *)
+
   Lemma NonZeroSameSignMul : forall (a b : R),
+    forall k, k != 0 ->
+              (NonZeroSameSign a b) -> (NonZeroSameSign (k * a) (k * b)).
+  Proof. Admitted.
+
+  Lemma NonZeroSameSignMulInv : 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 b) -> (NonZeroSameSign (a `^ k) (b `^ k)).
+  Proof. Admitted.
+
+  Lemma NonZeroSameSignExpInv : forall (a b : R),
     forall k, (NonZeroSameSign (a `^ k) (b `^ k) -> NonZeroSameSign a b).
   Proof. Admitted.
 
+  Lemma NonZeroSameSignDivPos : forall (a a' : R),
+    NonZeroSameSign (a) (a') -> 0 < a / a'.
+  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.
+  Lemma factor_exp : forall (a a' k : R), (a `^ k / a' `^ k = (a / a') `^ k). Admitted.
 End HelperLemmas.

coq_error_metrics/relative_prec.v

@@ -6,7 +6,7 @@ Section RelPrec.
   Context {R : realType}.
 
   Definition RelPrec (a a' α : R) : Prop :=
-    α >= 0 -> NonZeroSameSign a a' ->
+    α >= 0 /\ NonZeroSameSign a a' /\
     `|ln(a / a')| <= α.
 
 End RelPrec.
@@ -22,12 +22,12 @@ Section RPElementaryProperties.
 
   Theorem RPProp1 : (a ~ a' ; rp(α)) -> (a' ~ a ; rp(α)).
   Proof. rewrite /RelPrec /NonZeroSameSign.
-         move=> H1 H2 H3.
+         move=> [H1 [H2 H3]].
+         repeat split; auto.
+         destruct H2. left. destruct H; split; auto.
+         destruct H. right. destruct H3; split; auto.
          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.
+         rewrite sym => //.
          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')).
@@ -39,8 +39,8 @@ Section RPElementaryProperties.
          rewrite powRN.
          rewrite powRr1.
          reflexivity.
-         case: H3.
-         move=> [Ha' Ha].
+         case: H2.
+         move=> Ha.
          apply: divr_ge0.
          by [lra].
          by [lra].
@@ -55,34 +55,38 @@ Section RPElementaryProperties.
 
   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.
+         move=> del [H2 [H3 H4]] H5 H6. repeat split; auto.
+         rewrite (@le_trans _ _ α) => //.
+         rewrite (@le_trans _ _ α) => //.
+         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 => //.
+  Proof. rewrite /RelPrec; move => k [H1 [H2 H3]] H4. repeat split; auto.
          apply (NonZeroSameSignMul _ _ k) => //.
-         rewrite -mulf_div.
-         rewrite divff => //.
-         f_equal.
-         lra. Qed.
+         rewrite -mulf_div. rewrite divff => //. rewrite mul1r => //. 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.
-         Check factor_exp.
+  Proof. rewrite /RelPrec. move => k [H1 [H2 H3]] H4. repeat split; auto.
+         rewrite mulr_ge0 => //.
+         apply (NonZeroSameSignExp a a' k) => //.
          rewrite (factor_exp a a' k). 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) => //.
+         apply (le_mul_pos k _ _) => //. apply H3 => //.
   Qed.
 
   Theorem RPProp5 : forall (b b' β : R),
       a ~ a' ; rp(α) ->  b ~ b' ; rp(β) -> 0 <= β -> a * b ~ a' * b' ; rp(α + β).
-  Proof. Admitted.
+  Proof. rewrite /RelPrec. move=> b b' β [H1 [H2 H3]] [H4 [H5 H6]] H7. repeat split; auto.
+         rewrite addr_ge0 => //.
+         apply NonZeroSameSignMulGen => //.
+         suff sep_frac : (a * b / (a' * b') = (a / a') * (b / b')).
+         rewrite sep_frac lnM.
+         rewrite (@le_trans _ _ _ _ _ (ler_normD _ _)) => //.
+         suff add_le : forall (a b c d : R), a <= b -> c <= d -> a + c <= b + d.
+         rewrite add_le => //.
+         move=> w x y z P1 P2. lra.
+         apply NonZeroSameSignDivPos => //. apply NonZeroSameSignDivPos => //. lra. Qed.
 
   Theorem RPProp6 : forall (a'' δ : R ),
       a ~ a' ; rp(α) -> a' ~ a'' ; rp(δ) -> 0 <= δ -> a ~ a'' ; rp(α + δ).