From 6641c678192a17b286906463feff47becd9587e3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 26 Sep 2023 11:06:27 +0200 Subject: [PATCH] Adapting to interpretation of (x:T) now activating scope for T if any. These were situations where the cast was needed to hint type class inference but the body was expected to be interpreted in the type-class (current) scope rather than in the more specialized scope bound to the cast type. We add a "%mc" to force using the type-class based generic interpretation. --- ode/Picard.v | 2 +- reals/faster/ARArith.v | 2 +- reals/faster/ARarctan.v | 2 +- reals/faster/ARbigD.v | 16 +++++++------- reals/faster/ARcos.v | 2 +- reals/faster/ARroot.v | 34 ++++++++++++++--------------- reals/faster/ARsin.v | 4 ++-- reals/faster/ApproximateRationals.v | 2 +- util/Qdlog.v | 8 +++---- 9 files changed, 36 insertions(+), 36 deletions(-) diff --git a/ode/Picard.v b/ode/Picard.v index ce6b0111e..a9e4c597c 100644 --- a/ode/Picard.v +++ b/ode/Picard.v @@ -689,7 +689,7 @@ pose proof (CRdistance_CRle 1 1 y) as [_ H1]. specialize (H1 H). destruct H1 as [H1 H2]. change (1 - 1 ≤ y) in H1. change (y ≤ 1 + 1) in H2. change (abs y ≤ 2). rewrite plus_negate_r in H1. apply CRabs_AbsSmall. split; [| assumption]. -change (-2 ≤ y). transitivity (0 : CR); [| easy]. rewrite <- negate_0. +change (-2 ≤ y). transitivity (0%mc : CR); [| easy]. rewrite <- negate_0. apply flip_le_negate. apply (CRle_trans H1 H2). Qed. diff --git a/reals/faster/ARArith.v b/reals/faster/ARArith.v index 3de4fb8dd..d7f21706d 100644 --- a/reals/faster/ARArith.v +++ b/reals/faster/ARArith.v @@ -438,7 +438,7 @@ Next Obligation. rewrite <-(rings.mult_1_l (proj1_sig δ)) at 2. now apply (order_preserving (.* (proj1_sig δ))). apply rings.flip_nonneg_minus. - transitivity ('approximate x ((1#2) * 'ε)%Qpos - 'ε : Q). + transitivity (('approximate x ((1#2) * 'ε)%Qpos - 'ε)%mc : Q). apply (order_preserving (cast AQ Q)) in Pε. now apply rings.flip_nonneg_minus. apply rings.flip_le_minus_l. diff --git a/reals/faster/ARarctan.v b/reals/faster/ARarctan.v index 27a12b5a9..8d9d0fd74 100644 --- a/reals/faster/ARarctan.v +++ b/reals/faster/ARarctan.v @@ -145,7 +145,7 @@ Proof. rewrite rational_arctan_small_correct. rewrite rational_arctan_correct. apply CRIR.IRasCR_wd, InvTrigonom.ArcTan_wd, Q_in_CReals.inj_Q_wd. - mc_setoid_replace ('a / '1 : Q) with ('a). + mc_setoid_replace (('a / '1)%mc : Q) with ('a). reflexivity. rewrite rings.preserves_1. rewrite dec_fields.dec_recip_1. diff --git a/reals/faster/ARbigD.v b/reals/faster/ARbigD.v index e432067d6..ff4abc926 100644 --- a/reals/faster/ARbigD.v +++ b/reals/faster/ARbigD.v @@ -95,12 +95,12 @@ Qed. Lemma bigD_div_correct (x y : bigD) (k : Z) : Qball (2 ^ k) ('app_div x y k) ('x / 'y). Proof. assert (∀ xm xe ym ye : Z, - ('xm * 2 ^ xe : Q) / ('ym * 2 ^ ye : Q) = ('xm * 2 ^ (-(k - 1) + xe - ye)) / 'ym * 2 ^ (k - 1)) as E1. + (('xm * 2 ^ xe)%mc : Q) / (('ym * 2 ^ ye)%mc : Q) = ('xm * 2 ^ (-(k - 1) + xe - ye)) / 'ym * 2 ^ (k - 1)) as E1. intros. rewrite 2!int_pow_exp_plus by solve_propholds. rewrite dec_fields.dec_recip_distr. rewrite 2!int_pow_negate. - transitivity ('xm / 'ym * 2 ^ xe / 2 ^ ye * (2 ^ (k - 1) / 2 ^ (k - 1)) : Q); [| ring]. + transitivity (('xm / 'ym * 2 ^ xe / 2 ^ ye * (2 ^ (k - 1) / 2 ^ (k - 1)))%mc : Q); [| ring]. rewrite dec_recip_inverse by solve_propholds. ring. assert (∀ xm xe ym ye : Z, 'Z.div (Z.shiftl xm (-(k - 1) + xe - ye)) ym * 2 ^ (k - 1) - 2 ^ k ≤ ('xm * 2 ^ xe) / ('ym * 2 ^ ye : Q)) as Pleft. @@ -114,7 +114,7 @@ Proof. apply (order_preserving (.* _)). apply rings.flip_le_minus_l. apply semirings.plus_le_compat_r; [easy |]. - transitivity ('Z.shiftl xm (-(k - 1) + xe - ye) / 'ym - 1 : Q). + transitivity (('Z.shiftl xm (-(k - 1) + xe - ye) / 'ym - 1)%mc : Q). apply (order_preserving (+ -1)). now apply Qdiv_bounded_Zdiv. destruct (orders.le_or_lt 0 ym) as [E | E]. apply rings.flip_le_minus_l. @@ -123,7 +123,7 @@ Proof. apply dec_fields.nonneg_dec_recip_compat. now apply semirings.preserves_nonneg. now apply Qpow_bounded_Zshiftl. - transitivity (('Z.shiftl xm (-(k - 1) + xe - ye) + 1) / 'ym : Q). + transitivity ((('Z.shiftl xm (-(k - 1) + xe - ye) + 1) / 'ym)%mc : Q). rewrite rings.plus_mult_distr_r. apply semirings.plus_le_compat; [reflexivity |]. rewrite rings.mult_1_l. @@ -150,7 +150,7 @@ Proof. ring_simplify. apply sm_proper. now apply commutativity. intros. rewrite E1, E2. apply (order_preserving (.* _)). - transitivity ('Z.shiftl xm (-(k - 1) + xe - ye) / 'ym + 1 : Q). + transitivity (('Z.shiftl xm (-(k - 1) + xe - ye) / 'ym + 1)%mc : Q). 2: now apply (order_preserving (+1)); apply orders.lt_le, Qdiv_bounded_Zdiv. destruct (orders.le_or_lt ym 0) as [E3 | E3]. apply semirings.plus_le_compat_r; [easy |]. @@ -158,8 +158,8 @@ Proof. apply dec_fields.nonpos_dec_recip_compat. now apply semirings.preserves_nonpos. now apply Qpow_bounded_Zshiftl. - transitivity (('Z.shiftl xm (-(k - 1) + xe - ye) + 1) / ' ym : Q). - apply (maps.order_preserving_flip_nonneg (.*.) (/ 'ym : Q)). + transitivity ((('Z.shiftl xm (-(k - 1) + xe - ye) + 1) / ' ym)%mc : Q). + apply (maps.order_preserving_flip_nonneg (.*.) ((/ 'ym)%mc : Q)). apply dec_fields.nonneg_dec_recip_compat. apply semirings.preserves_nonneg. now apply orders.lt_le. @@ -187,7 +187,7 @@ Instance bigD_approx : AppApprox bigD := λ x k, Lemma bigD_approx_correct (x : bigD) (k : Z) : Qball (2 ^ k) ('app_approx x k) ('x). Proof. setoid_replace (app_approx x k) with (app_div x 1 k). - setoid_replace ('x : Q) with ('x / '1 : Q). + setoid_replace ('x : Q) with (('x / '1)%mc : Q). now apply bigD_div_correct. rewrite rings.preserves_1, dec_fields.dec_recip_1. now rewrite rings.mult_1_r. diff --git a/reals/faster/ARcos.v b/reals/faster/ARcos.v index a7fbc93a0..7a6c3b3e1 100644 --- a/reals/faster/ARcos.v +++ b/reals/faster/ARcos.v @@ -23,7 +23,7 @@ Local Open Scope uc_scope. Add Field Q : (dec_fields.stdlib_field_theory Q). -Definition AQcos_poly_fun (x : AQ) : AQ := 1 - 2 * x ^ (2:N). +Definition AQcos_poly_fun (x : AQ) : AQ := 1 - 2 * x ^ (2%mc:N). Lemma AQcos_poly_fun_correct (x : AQ) : 'AQcos_poly_fun x = cos_poly_fun ('x). diff --git a/reals/faster/ARroot.v b/reals/faster/ARroot.v index e6a8eda50..df6a68f4e 100644 --- a/reals/faster/ARroot.v +++ b/reals/faster/ARroot.v @@ -28,15 +28,15 @@ Fixpoint AQsqrt_loop (n : nat) : AQ * AQ := | S n => let (r, s) := AQsqrt_loop n in if decide_rel (≤) (s + 1) r - then ((r - (s + 1)) ≪ (2:Z), (s + 2) ≪ (1:Z)) - else (r ≪ (2:Z), s ≪ (1:Z)) + then ((r - (s + 1)) ≪ (2%mc:Z), (s + 2) ≪ (1%mc:Z)) + else (r ≪ (2%mc:Z), s ≪ (1%mc:Z)) end. Instance: Proper (=) AQsqrt_loop. Proof. intros x y E. change (x ≡ y) in E. now rewrite E. Qed. Lemma AQsqrt_loop_invariant1 (n : nat) : - snd (AQsqrt_loop n) ^ (2:N) + 4 * fst (AQsqrt_loop n) = 4 * 4 ^ n * a. + snd (AQsqrt_loop n) ^ (2%mc:N) + 4 * fst (AQsqrt_loop n) = 4 * 4 ^ n * a. Proof. rewrite nat_pow_2. induction n; unfold pow; simpl. @@ -136,7 +136,7 @@ Proof with auto. now apply rings.flip_le_negate, semirings.le_2_4. Qed. -Definition AQsqrt_mid_bounded_raw (n : N) := snd (AQsqrt_loop ('n)) ≪ -(1 + 'n : Z). +Definition AQsqrt_mid_bounded_raw (n : N) := snd (AQsqrt_loop ('n)) ≪ -((1 + 'n)%mc : Z). Instance AQsqrt_mid_bounded_raw_proper: Proper ((=) ==> (=)) AQsqrt_mid_bounded_raw. Proof. intros x y E. change (x ≡ y) in E. now subst. Qed. @@ -183,9 +183,9 @@ Proof. rewrite <-(shiftl_nat_pow_alt (f:=cast nat Z)). rewrite (naturals.to_semiring_twice _ _ (cast N Z)). rewrite <-shiftl_exp_plus, rings.preserves_plus. - mc_setoid_replace ('z - (1 + ('z + 'm)) : Z) with (-(1 + 'm) : Z) by ring. + mc_setoid_replace (('z - (1 + ('z + 'm)))%mc : Z) with ((-(1 + 'm))%mc : Z) by ring. rewrite shiftl_base_plus. ring_simplify. - mc_setoid_replace (1 - ' m : Z) with (2 - (1 + 'm) : Z) by ring. + mc_setoid_replace ((1 - ' m)%mc : Z) with ((2 - (1 + 'm))%mc : Z) by ring. now rewrite shiftl_exp_plus, shiftl_2, rings.mult_1_r. Qed. @@ -198,7 +198,7 @@ Proof. change (m ≡ z + n) in E. subst. unfold AQsqrt_mid_bounded_raw. rewrite 2!rings.preserves_plus. - mc_setoid_replace (-(1 + 'n) : Z) with ('z - (1 + ('z + 'n) : Z)) by ring. + mc_setoid_replace ((-(1 + 'n))%mc : Z) with (('z - (1 + ('z + 'n)))%mc : Z) by ring. rewrite shiftl_exp_plus. apply (order_preserving (≪ _)). rewrite shiftl_nat_pow_alt, <-(preserves_nat_pow_exp (f:=cast N nat)). @@ -206,14 +206,14 @@ Proof. Qed. Lemma AQsqrt_mid_bounded_spec (n : N) : - (AQsqrt_mid_bounded_raw n ^ (2:N)) = a - fst (AQsqrt_loop ('n)) ≪ -(2 * 'n). + (AQsqrt_mid_bounded_raw n ^ (2%mc:N)) = a - fst (AQsqrt_loop ('n)) ≪ -(2 * 'n). Proof. unfold AQsqrt_mid_bounded_raw. rewrite shiftl_base_nat_pow, rings.preserves_2. apply (injective (≪ (2 + 2 * 'n))). rewrite shiftl_reverse by ring. rewrite shiftl_base_plus, shiftl_negate, <-shiftl_exp_plus. - mc_setoid_replace (-(2 * 'n) + (2 + 2 * 'n) : Z) with (2 : Z) by ring. + mc_setoid_replace ((-(2 * 'n) + (2 + 2 * 'n))%mc : Z) with (2%mc : Z) by ring. rewrite shiftl_exp_plus, ?shiftl_2, <-shiftl_mult_l. rewrite <-(rings.preserves_2 (f:=cast N Z)), <-rings.preserves_mult. rewrite shiftl_nat_pow_alt, nat_pow_exp_mult. @@ -244,16 +244,16 @@ Proof. (AQsqrt_mid_bounded_raw (n + 3) : AQ_as_MetricSpace) (AQsqrt_mid_bounded_raw (m + 3))). intros n m E. simpl. apply Qball_Qabs. rewrite Qabs.Qabs_pos. - change ('AQsqrt_mid_bounded_raw (n + 3) - 'AQsqrt_mid_bounded_raw (m + 3) ≤ (2 ^ (-'m - 2) : Q)). + change ('AQsqrt_mid_bounded_raw (n + 3) - 'AQsqrt_mid_bounded_raw (m + 3) ≤ ((2 ^ (-'m - 2))%mc : Q)). rewrite <-rings.preserves_minus, <-(rings.mult_1_l (2 ^ (-'m - 2))). rewrite <-shiftl_int_pow. rewrite <-(rings.preserves_1 (f:=cast AQ Q)), <-(preserves_shiftl (f:=cast AQ Q)). apply (order_preserving _). - mc_setoid_replace (-'m - 2 : Z) with (1 - '(m + 3) : Z). + mc_setoid_replace ((-'m - 2)%mc : Z) with ((1 - '(m + 3))%mc : Z). apply AQsqrt_mid_bounded_regular_aux1. - now refine (order_preserving (+ (3:N)) _ _ _). + now refine (order_preserving (+ (3%mc:N)) _ _ _). rewrite rings.preserves_plus, rings.preserves_3. ring. - change (0 ≤ ('AQsqrt_mid_bounded_raw (n + 3) - 'AQsqrt_mid_bounded_raw (m + 3) : Q)). + change (0 ≤ (('AQsqrt_mid_bounded_raw (n + 3) - 'AQsqrt_mid_bounded_raw (m + 3))%mc : Q)). apply rings.flip_nonneg_minus. apply (order_preserving _). apply AQsqrt_mid_bounded_regular_aux2. @@ -263,7 +263,7 @@ Proof. { intros ε1 ε2 E. unfold AQsqrt_mid_raw. eapply ball_weak_le; auto. - change ((2:Q) ^ (-'N_of_Z (-Qdlog2 (proj1_sig ε2)) - 2) + change ((2%mc:Q) ^ (-'N_of_Z (-Qdlog2 (proj1_sig ε2)) - 2) ≤ proj1_sig ε1 + proj1_sig ε2). apply semirings.plus_le_compat_l. now apply orders.lt_le, Qpos_ispos. @@ -272,7 +272,7 @@ Proof. change (- (-Qdlog2 (proj1_sig ε2))%Z) with (- -Qdlog2 (proj1_sig ε2)). rewrite rings.negate_involutive. rewrite int_pow_exp_plus by solve_propholds. - transitivity (2 ^ Qdlog2 (proj1_sig ε2) : Q). + transitivity ((2 ^ Qdlog2 (proj1_sig ε2))%mc : Q). 2: now apply Qdlog2_spec, Qpos_ispos. rewrite <-(rings.mult_1_r (2 ^ Qdlog2 (proj1_sig ε2) : Q)) at 2. now apply (order_preserving (_ *.)). @@ -319,7 +319,7 @@ Proof. { intros ε. apply Qball_Qabs. rewrite Qabs.Qabs_neg. eapply Qle_trans. 2: now apply Qpos_dlog2_spec. - change (-( '(AQsqrt_mid_raw ε ^ 2) - 'a) ≤ (2 ^ Qdlog2 (proj1_sig ε) : Q)). + change (-( '(AQsqrt_mid_raw ε ^ 2) - 'a) ≤ ((2 ^ Qdlog2 (proj1_sig ε))%mc : Q)). rewrite <-rings.negate_swap_r. unfold AQsqrt_mid_raw. rewrite AQsqrt_mid_bounded_spec. rewrite rings.preserves_minus, preserves_shiftl. ring_simplify. @@ -386,7 +386,7 @@ Proof. rewrite <-preserves_nat_pow. rewrite AQsqrt_mid_spec. now apply ARtoCR_inject. - change (0%CR) with (0 : CR). + change (0%CR) with (0%mc : CR). rewrite <-(rings.preserves_0 (f:=cast AR CR)). apply (order_preserving _). now apply AQsqrt_mid_nonneg. diff --git a/reals/faster/ARsin.v b/reals/faster/ARsin.v index 5ceb42458..29692af6b 100644 --- a/reals/faster/ARsin.v +++ b/reals/faster/ARsin.v @@ -217,7 +217,7 @@ Qed. (** Sine's range can then be extended to [[0,3^n]] by [n] applications of the identity [sin(x) = 3*sin(x/3) - 4*(sin(x/3))^3]. *) -Definition AQsin_poly_fun (x : AQ) : AQ := x * (3 - 4 * x ^ (2:N)). +Definition AQsin_poly_fun (x : AQ) : AQ := x * (3 - 4 * x ^ (2%mc:N)). Lemma AQsin_poly_fun_correct (q : AQ) : 'AQsin_poly_fun q = sin_poly_fun ('q). @@ -362,7 +362,7 @@ Definition AQsin (a:AQ) : msp_car AR Lemma AQsin_correct : forall a, 'AQsin a = rational_sin ('a). Proof. intro a. - mc_setoid_replace ('a : Q) with ('a / '1 : Q). + mc_setoid_replace ('a : Q) with (('a / '1)%mc : Q). now apply AQsin_bounded_correct. rewrite rings.preserves_1, dec_fields.dec_recip_1. rewrite Qmult_1_r. reflexivity. diff --git a/reals/faster/ApproximateRationals.v b/reals/faster/ApproximateRationals.v index c2855c684..c25230ee1 100644 --- a/reals/faster/ApproximateRationals.v +++ b/reals/faster/ApproximateRationals.v @@ -150,7 +150,7 @@ Section approximate_rationals_more. Proof. split; try apply _. intros E. - destruct (rings.is_ne_0 (1:Q)). + destruct (rings.is_ne_0 (1%mc:Q)). rewrite <-(rings.preserves_1 (f:=cast AQ Q)). rewrite <-(rings.preserves_0 (f:=cast AQ Q)). now rewrite E. diff --git a/util/Qdlog.v b/util/Qdlog.v index e3df28940..3e0254bbe 100644 --- a/util/Qdlog.v +++ b/util/Qdlog.v @@ -109,12 +109,12 @@ Proof. apply (antisymmetry (≤)). apply nat_int.le_iff_lt_plus_1. rewrite commutativity. - apply int_pow_exp_lt_back with (2 : Q); [ apply semirings.lt_1_2 |]. + apply int_pow_exp_lt_back with (2%mc : Q); [ apply semirings.lt_1_2 |]. apply orders.le_lt_trans with x; [ intuition |]. now apply Qdlog2_spec. apply nat_int.le_iff_lt_plus_1. rewrite commutativity. - apply int_pow_exp_lt_back with (2 : Q); [ apply semirings.lt_1_2 |]. + apply int_pow_exp_lt_back with (2%mc : Q); [ apply semirings.lt_1_2 |]. apply orders.le_lt_trans with x; [|intuition]. now apply Qdlog2_spec. Qed. @@ -147,7 +147,7 @@ Lemma Qdlog2_preserving (x y : Q) : Proof. intros E1 E2. apply nat_int.le_iff_lt_plus_1. rewrite commutativity. - apply int_pow_exp_lt_back with (2:Q); [ apply semirings.lt_1_2 |]. + apply int_pow_exp_lt_back with (2%mc:Q); [ apply semirings.lt_1_2 |]. apply orders.le_lt_trans with x; [now apply Qdlog2_spec | ]. apply orders.le_lt_trans with y; [assumption |]. apply Qdlog2_spec. @@ -269,7 +269,7 @@ Lemma Qdlog4_spec (x : Q) : 0 < x → 4 ^ Qdlog4 x ≤ x ∧ x < 4 ^ (1 + Qdlog4 x). Proof. intros E1. unfold Qdlog4. - change (4:Q) with ((2:Q) ^ (2:Z))%mc. + change (4%mc:Q) with ((2%mc:Q) ^ (2:Z))%mc. rewrite <-2!int_pow_exp_mult. split. etransitivity.