Merge pull request #8 from Yosuke-Ito-345/update_for_CoqPlatform.2023.03

update_for_CoqPlatform.2023.03
Yosuke-Ito-345 · Nov 10, 2023 · e031068 · e031068
2 parents 1e8aa29 + d6348c2
commit e031068
Show file tree

Hide file tree

Showing 6 changed files with 40 additions and 50 deletions.
diff --git a/README.md b/README.md
@@ -4,9 +4,9 @@ This is an experimental package where the basic part of actuarial mathematics is
 
 ## Requirements
 
-- [Coq 8.13](https://coq.inria.fr/download) or later
-- [Mathematical Components 1.15.0](https://math-comp.github.io) or later
-- [Coquelicot 3.1.0](https://gitlab.inria.fr/coquelicot/coquelicot) or later
+- [Coq 8.17.1](https://coq.inria.fr/download) or later
+- [Mathematical Components 1.17.0 or 1.18.0](https://math-comp.github.io) 
+- [Coquelicot 3.4.0](https://gitlab.inria.fr/coquelicot/coquelicot) or later
 
 ## Building and installation instructions
 

diff --git a/theories/Basics.v b/theories/Basics.v
@@ -135,35 +135,35 @@ Proof.
  move => x; apply (Rgt_not_eq x 0).
 Qed.
 
-Hint Resolve pos_neq0 : core.
+#[export]Hint Resolve pos_neq0 : core.
 
 Lemma neg_neq0 : forall x:R, x < 0 -> x <> 0.
 Proof.
  move => x; apply (Rlt_not_eq x 0).
 Qed.
 
-Hint Resolve neg_neq0 : core.
+#[export]Hint Resolve neg_neq0 : core.
 
 Lemma Sn_pos : forall n:nat, 0 < INR (n + 1).
 Proof.
  move => n; rewrite plus_INR; apply INRp1_pos.
 Qed.
 
-Hint Resolve Sn_pos : core.
+#[export]Hint Resolve Sn_pos : core.
 
 Lemma INR1_pos : 0 < INR 1.
 Proof.
  by rewrite -(add0n 1%N).
 Qed.
 
-Hint Resolve INR1_pos : core.
+#[export]Hint Resolve INR1_pos : core.
 
 Lemma Sn_neq0 : forall n:nat, INR (n + 1) <> 0.
 Proof.
  move => n; auto.
 Qed.
 
-Hint Resolve Sn_neq0 : core.
+#[export]Hint Resolve Sn_neq0 : core.
 
 Lemma one_pow : forall r:R, 1^r = 1.
 Proof.
@@ -230,7 +230,7 @@ Proof.
   move => x y Hy.
   rewrite /Rdiv.
   rewrite Rabs_mult.
-  rewrite Rabs_Rinv //.
+  rewrite Rabs_inv //.
 Qed.
 
 Lemma Rbar_mult_1_r : forall x : Rbar, Rbar_mult x 1 = x.
@@ -275,12 +275,12 @@ Qed.
 
 Lemma Rpower_lt' : forall x y z : R, 0 < x < 1 -> y < z -> x ^ z < x ^ y.
 Proof.
- move => x y z Hx Hyz.
- rewrite -(Rinv_involutive x); [| apply pos_neq0; apply Hx].
- rewrite -!(Rpower_Ropp' (x:=/x)); try apply Rinv_0_lt_compat; try apply Hx.
- apply (Rpower_lt (/x) (-z) (-y)).
+  move => x y z Hx Hyz.
+  rewrite -(Rinv_inv x).
+  rewrite -!(Rpower_Ropp' (x:=/x)); try apply Rinv_0_lt_compat; try apply Hx.
+  apply (Rpower_lt (/x) (-z) (-y)).
   rewrite -Rinv_1; apply (Rinv_lt_contravar x 1); lra.
- lra.
+  lra.
 Qed.
 
 Lemma Rmax_same : forall x:R, Rmax x x = x.

diff --git a/theories/Interest.v b/theories/Interest.v
@@ -214,8 +214,7 @@ Proof.
   move => n.
   rewrite {3}plus_INR /Rpower -/i_force.
   rewrite -(Rinv_r_simpl_m \δ (n+1)); auto.
-  rewrite (Rmult_assoc \δ _) -/(Rdiv _ \δ) -(Rinv_Rdiv \δ (n+1));
-  [| auto | apply (pos_neq0 (INRp1_pos n))].
+  rewrite (Rmult_assoc \δ _) -/(Rdiv _ \δ) -(Rinv_div \δ (n+1)).
   rewrite Rmult_assoc (Rmult_comm (/_) _) -/(Rdiv _ (_ /_)) -(plus_INR n 1).
   by rewrite {5}/Rdiv (Rmult_comm _ \δ) -/(Rdiv \δ _).
  rewrite -(Rbar_mult_1_r \δ).
@@ -251,8 +250,8 @@ Proof.
  rewrite -(Rmult_1_l (/ _)) {1}(Rinv_r_sym (1 + \i^{m} / m));
  [rewrite -RIneq.Rdiv_minus_distr | lra].
  rewrite Rplus_comm /Rminus Rplus_assoc Rplus_opp_r Rplus_0_r /d_nom /Rdiv Rmult_assoc
- -Rinv_mult_distr; try lra.
- rewrite (Rmult_comm (1+_)) Rinv_mult_distr; try lra.
+ -Rinv_mult; try lra.
+ rewrite (Rmult_comm (1+_)) Rinv_mult; try lra.
  by rewrite -Rmult_assoc Rplus_comm.
 Qed.
 
@@ -346,7 +345,7 @@ Proof.
   move => m Hmpos.
   rewrite /d_nom.
   rewrite i_nom_i // i_v Rpower_mult -(Ropp_mult_distr_l) Rmult_1_l /Rdiv Rpower_Ropp.
-    by rewrite Rinv_involutive; [| apply /pos_neq0 /exp_pos].
+    by rewrite Rinv_inv.
 Qed.
 
 Lemma a_calc : forall (n m : nat), 0 < m -> \a^{m}_:n = (1 - (\v)^n) / (\i^{m}).
@@ -366,10 +365,8 @@ Proof.
  [| apply exp_pos
  | apply /Rlt_not_eq /lt_vpow_1 /Rinv_0_lt_compat => //].
  rewrite Rpower_mult mult_INR (Rmult_comm _ (n*m)) Rinv_r_simpl_l; [| lra].
- rewrite -/(Rdiv _ m) -(Rinv_Rdiv _ ((\v)^(/m))); [| lra | apply /pos_neq0 /exp_pos].
- rewrite /Rdiv Rmult_assoc -Rinv_mult_distr;
- [| apply /Rminus_eq_contra /Rgt_not_eq /lt_vpow_1 /Rinv_0_lt_compat => //
- | apply /pos_neq0 /Rmult_gt_0_compat => //; apply /Rinv_0_lt_compat /exp_pos].
+ rewrite -/(Rdiv _ m) -(Rinv_div _ ((\v)^(/m))).
+ rewrite /Rdiv Rmult_assoc -Rinv_mult.
  rewrite (Rmult_comm m _) -Rmult_assoc -/(Rdiv _ ((\v)^(/m))) RIneq.Rdiv_minus_distr.
  rewrite /Rdiv Rinv_r; [| apply /pos_neq0 /exp_pos].
  rewrite Rmult_1_l -Rpower_Ropp {2}/v_pres -Rpower_Ropp'; [| lra]; rewrite Ropp_involutive.
@@ -428,10 +425,8 @@ Lemma a''_calc : forall (n m : nat), 0 < m -> \a''^{m}_:n = (1 - (\v)^n) / \d^{m
 Proof.
  move => n m Hmpos.
  rewrite a''_a //; rewrite a_calc //.
- rewrite -(Rinv_involutive (1 + \i^{m} / m)); [| apply /pos_neq0 /i_nom_add_pos => //].
- rewrite Rmult_comm {1}/Rdiv Rmult_assoc -/Rdiv -Rinv_mult_distr;
-   [| apply /pos_neq0 /i_nom_pos => // |
-    apply /Rinv_neq_0_compat /pos_neq0 /i_nom_add_pos => //].
+ rewrite -(Rinv_inv (1 + \i^{m} / m)).
+ rewrite Rmult_comm {1}/Rdiv Rmult_assoc -/Rdiv -Rinv_mult.
  by[].
 Qed.
 
@@ -459,10 +454,8 @@ Lemma s''_calc : forall (n m : nat), 0 < m -> \s''^{m}_:n = ((1+\i)^n - 1) / \d^
 Proof.
   move => n m Hmpos.
   rewrite s''_s //; rewrite s_calc //.
-  rewrite -(Rinv_involutive (1 + \i^{m} / m)); [| apply /pos_neq0 /i_nom_add_pos => //].
-  rewrite Rmult_comm {1}/Rdiv Rmult_assoc -/Rdiv -Rinv_mult_distr;
-    [| apply /pos_neq0 /i_nom_pos => // |
-     apply /Rinv_neq_0_compat /pos_neq0 /i_nom_add_pos => //].
+  rewrite -(Rinv_inv (1 + \i^{m} / m)).
+  rewrite Rmult_comm {1}/Rdiv Rmult_assoc -/Rdiv -Rinv_mult.
     by[].
 Qed.
 
@@ -667,7 +660,7 @@ Proof.
  rewrite mult_INR !Rpower_mult.
  rewrite 2!(Rmult_comm (/m)) (Rmult_plus_distr_r _ _ (/m))
  Rinv_r_simpl_l; [| apply pos_neq0 => //].
- rewrite {1}/Rdiv 2!Rmult_assoc -Rinv_mult_distr; try apply /pos_neq0 /exp_pos.
+ rewrite {1}/Rdiv 2!Rmult_assoc -Rinv_mult; try apply /pos_neq0 /exp_pos.
  rewrite Rpower_mult_distr; [| apply /Rgt_minus /lt_vpow_1 /Rinv_0_lt_compat => // | done].
  by rewrite -Rmult_assoc (Rmult_comm (1-(\v)^(/m)) m) -/(Rdiv _ (_^2)).
 Qed.
@@ -688,7 +681,7 @@ Proof.
           -Rmult_plus_distr_r Rplus_opp_l Rmult_0_l Rpower_O; [| apply /v_pos]].
   rewrite -Rmult_assoc (Rmult_comm m (\v ^ _)) (Rmult_assoc (\v ^ _) m).
   rewrite -(Rpower_mult_distr (\v ^ (-1 * / m)) _ 2) //; [| apply exp_pos].
-  rewrite Rinv_mult_distr; try apply pos_neq0; try apply exp_pos.
+  rewrite Rinv_mult; try apply pos_neq0; try apply exp_pos.
   rewrite Rpower_mult -Rmult_assoc.
   rewrite (_ : / \v ^ (-1 * / m * 2) = \v ^ (2 */ m));
     [| rewrite -Rpower_Ropp -Ropp_mult_distr_l Rmult_1_l
@@ -837,7 +830,7 @@ Proof.
   - rewrite /is_Rbar_div /is_Rbar_mult /= Rmult_1_r.
     rewrite {1}(_ : (\v)^(/m) = /((\v)^(-/m)));
       [| by rewrite -{1}(Ropp_involutive (/m)) (Rpower_Ropp \v (-/m))].
-    rewrite -Rinv_mult_distr; try apply /pos_neq0 /exp_pos.
+    rewrite -Rinv_mult; try apply /pos_neq0 /exp_pos.
     rewrite Rpower_2;
       [| apply Rmult_gt_0_compat => //; apply /Rgt_minus /lt_vpow_1 /Rinv_0_lt_compat => //].
     rewrite -3!Rmult_assoc (Rmult_comm (\v ^ _) m) (Rmult_assoc m (\v ^ _)).
@@ -869,9 +862,7 @@ Proof.
       by rewrite i_nom_i // i_v Rpower_mult -Ropp_mult_distr_l Rmult_1_l Rpower_Ropp.    
   - rewrite Rpower_2; [| apply d_nom_pos => //].
     rewrite {1}d_nom_i_nom_v // (Rmult_comm _ (\v ^ _)) Rmult_assoc.
-    rewrite Rinv_mult_distr;
-      [| apply /pos_neq0 /exp_pos |
-       apply /pos_neq0 /Rmult_gt_0_compat; [apply i_nom_pos | apply d_nom_pos] => //].
+    rewrite Rinv_mult.
     apply (is_lim_seq_scal_l _ _ (/ (\i^{m} * \d^{m}))).
     apply lim_Imam => //.
 Qed.

diff --git a/theories/LifeTable.v b/theories/LifeTable.v
@@ -17,7 +17,7 @@ Record life : Type := Life {
   l_decr : decreasing l_fun
 }.
 
-Hint Resolve l_0_pos l_neg_nil l_infty_0 l_decr : core.
+#[export] Hint Resolve l_0_pos l_neg_nil l_infty_0 l_decr : core.
 
 Notation "\l[ l ]_ u" := (l_fun l u) (at level 9).
 
@@ -627,7 +627,7 @@ Proof.
   rewrite /survive.
   rewrite (l_exp_RInt_mu (u+t)) //; [| lra].
   rewrite (l_exp_RInt_mu u) //; [| apply (Rbar_le_lt_trans _ (u+t)) => //=; lra].
-  rewrite /Rdiv Rinv_mult_distr; auto; [| apply /pos_neq0 /exp_pos].
+  rewrite /Rdiv Rinv_mult.
   rewrite -!Rmult_assoc (Rmult_comm \l_0) (Rmult_assoc _ \l_0) Rinv_r;
     auto; rewrite Rmult_1_r.
   rewrite -exp_Ropp -exp_plus -Ropp_plus_distr.

diff --git a/theories/Premium.v b/theories/Premium.v
@@ -880,7 +880,7 @@ Proof.
     { rewrite /survive.
       apply /pos_neq0 /Rdiv_lt_0_compat; auto.
       rewrite /Rminus !Rplus_assoc Rplus_opp_l Rplus_0_r //. }
-    rewrite Rinv_mult_distr //; [| apply /pos_neq0 /exp_pos].
+    rewrite Rinv_mult.
     rewrite Rmult_assoc (Rmult_comm _ (/ _ * / _)) -3!Rmult_assoc Rmult_assoc
       (Rmult_comm \p_{_&_}) -Rmult_assoc (Rmult_assoc _ (/ \p_{_&_}) (\p_{_&_}))
       Rinv_l ?Rmult_1_r; auto.
@@ -916,7 +916,7 @@ Proof.
     { rewrite /survive.
       apply /pos_neq0 /Rdiv_lt_0_compat; auto.
       rewrite /Rminus !Rplus_assoc Rplus_opp_l Rplus_0_r //. }
-    rewrite Rinv_mult_distr //; [| apply /pos_neq0 /exp_pos].
+    rewrite Rinv_mult.
     rewrite Rmult_assoc (Rmult_comm _ (/ _ * / _)) -3!Rmult_assoc Rmult_assoc
       (Rmult_comm \p_{_&_}) -Rmult_assoc (Rmult_assoc _ (/ \p_{_&_}) (\p_{_&_}))
       Rinv_l ?Rmult_1_r; auto.
@@ -947,14 +947,13 @@ Proof.
     2:{ rewrite /Rminus Rplus_assoc Rplus_opp_l Rplus_0_r -plus_INR.
         apply /pos_neq0 /l_x_pos.
         rewrite plus_INR; lra. }
-    rewrite Rinv_mult_distr ?Hxnkk;
-      [| apply /pos_neq0 /exp_pos | by apply Rmult_integral_contrapositive_currified].
-    rewrite Rinv_mult_distr // -Rmult_assoc (Rmult_assoc \v) (Rmult_comm \p_(x+n))
+    rewrite Rinv_mult ?Hxnkk.
+    rewrite Rinv_mult // -Rmult_assoc (Rmult_assoc \v) (Rmult_comm \p_(x+n))
       -(Rmult_assoc \v) Rmult_assoc (Rmult_comm (/ _)) -(Rmult_assoc \p_(x+n)) Rinv_r //
       Rmult_1_l.
     rewrite -Rpower_Ropp -{1}(Rpower_1 \v); auto.
     rewrite -Rpower_plus Ropp_plus_distr (Rplus_comm 1) Rplus_assoc Rplus_opp_l Rplus_0_r.
-    rewrite Rpower_Ropp -Rinv_mult_distr //; [| apply /pos_neq0 /exp_pos].
+    rewrite Rpower_Ropp -Rinv_mult.
     over. }
     by rewrite acc_annual.
 Qed.
@@ -1080,7 +1079,7 @@ Proof.
       apply Rdiv_lt_0_compat; auto.
       by rewrite (_ : x + k / m + (t - k / m) = x + t); [| lra]. }
     rewrite /ins_pure_endow_life.
-    rewrite Rinv_mult_distr; [| apply /pos_neq0 /exp_pos | auto].
+    rewrite Rinv_mult.
     rewrite -Rmult_assoc (Rmult_assoc _ _ (\v^t)) (Rmult_comm _ (\v^t))
       -Rmult_assoc Rmult_assoc.
     rewrite -Rpower_Ropp -Rpower_plus (_ : - (t - k / m) + t = k/m); [| lra].
@@ -1291,7 +1290,7 @@ Proof.
           rewrite /N.
           rewrite INR_Ztonat_IZR; by [| apply le_0_IZR; lra].
         + rewrite /N /=.
-          rewrite -{2}(Rinv_involutive delta); auto.
+          rewrite -{2}(Rinv_inv delta); auto.
           rewrite /Rdiv Rmult_1_l.
           apply Rinv_le_contravar; auto; [by apply Rinv_0_lt_compat |].
           rewrite INR_Ztonat_IZR; [apply ceil_correct | apply le_0_IZR; lra]. }
@@ -1749,7 +1748,7 @@ Proof.
   rewrite -(Rmult_assoc _ (-1)) (Rmult_comm \A_{_:_`1})
                                 Rmult_opp1_l Ropp_mult_distr_l Ropp_involutive.
   rewrite /ins_pure_endow_life.
-  rewrite Rinv_mult_distr; [| apply /pos_neq0 /exp_pos | done].
+  rewrite Rinv_mult.
   rewrite -(Rmult_assoc (\v^n*\p_{n&u})) (Rmult_assoc (\v^n)).
   rewrite (Rmult_comm \p_{n&u}) -Rmult_assoc Rmult_assoc.
   rewrite -Rpower_Ropp -Rpower_plus (_ : n+-(n-t) = t); [| lra].

diff --git a/theories/Reserve.v b/theories/Reserve.v
@@ -320,7 +320,7 @@ Proof.
   rewrite Rplus_opp_r !Rplus_0_l.
   rewrite Ropp_involutive Ropp_mult_distr_r.
   rewrite -Rmult_plus_distr_l.
-  rewrite /Rdiv Rinv_mult_distr // -Rmult_assoc Rinv_r_simpl_m //.
+  rewrite /Rdiv Rinv_mult // -Rmult_assoc Rinv_r_simpl_m //.
   rewrite Rmult_plus_distr_r Rinv_r //; lra.
 Qed.
 
@@ -341,7 +341,7 @@ Proof.
   rewrite /Rminus Ropp_plus_distr (Rplus_comm _ (--_))
     -Rplus_assoc !(Rplus_assoc _ (-\d^{m})) Rplus_opp_l Rplus_opp_r Rplus_0_r.
   rewrite Rdiv_plus_distr.
-  rewrite /Rdiv Rinv_r; [| apply Rinv_neq_0_compat => //]; rewrite Rinv_involutive //; lra.
+  rewrite /Rdiv Rinv_r; [| apply Rinv_neq_0_compat => //]; rewrite Rinv_inv //; lra.
 Qed.
 
 Lemma res_whole_prem_ann_due : forall m t x : nat, 0 < m -> x+t < \ω ->