From 605b021549ea8684dfd17e1458643732d13efe4e Mon Sep 17 00:00:00 2001 From: amethyst Date: Fri, 3 Nov 2023 20:13:19 +0900 Subject: [PATCH 1/3] update_for_CoqPlatform.2023.03 --- README.md | 6 +++--- _CoqProject | 2 +- theories/Basics.v | 22 +++++++++++----------- theories/Interest.v | 37 ++++++++++++++----------------------- theories/LifeTable.v | 4 ++-- theories/Premium.v | 17 ++++++++--------- theories/Reserve.v | 4 ++-- 7 files changed, 41 insertions(+), 51 deletions(-) diff --git a/README.md b/README.md index cf7b53b..01d6552 100644 --- 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](https://math-comp.github.io) or later +- [Coquelicot 3.4.0](https://gitlab.inria.fr/coquelicot/coquelicot) or later ## Building and installation instructions diff --git a/_CoqProject b/_CoqProject index f24e524..3ca40bf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,4 @@ --Q theories Actuary +-R theories Actuary -arg -w -arg -notation-overridden -arg -w -arg -ambiguous-paths diff --git a/theories/Basics.v b/theories/Basics.v index 0696302..d31d4b5 100644 --- 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 index 527cb41..91cf1d4 100644 --- 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 index 235cd2d..7739cee 100644 --- 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 index 305a7db..b7358bf 100644 --- 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 index e9749b9..032882a 100644 --- 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 < \ω -> From 7ba20c9de0d6682d4269c284b11de500088d6f07 Mon Sep 17 00:00:00 2001 From: Yosuke Ito Date: Fri, 10 Nov 2023 20:26:50 +0900 Subject: [PATCH 2/3] Update _CoqProject I got it! Thank you for the suggestion. Co-authored-by: Karl Palmskog --- _CoqProject | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_CoqProject b/_CoqProject index 3ca40bf..f24e524 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,4 @@ --R theories Actuary +-Q theories Actuary -arg -w -arg -notation-overridden -arg -w -arg -ambiguous-paths From d6348c2c32fe6f3cc5aa1e8d6e6625f6aead4505 Mon Sep 17 00:00:00 2001 From: Yosuke Ito Date: Fri, 10 Nov 2023 20:28:15 +0900 Subject: [PATCH 3/3] Update README.md Thank you for the advice. I adopt this description. Co-authored-by: Karl Palmskog --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 01d6552..5b7da44 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ This is an experimental package where the basic part of actuarial mathematics is ## Requirements - [Coq 8.17.1](https://coq.inria.fr/download) or later -- [Mathematical Components 1.17.0](https://math-comp.github.io) 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