Merge pull request #199 from coq-community/master+adapting-cast-using…

…-scope-bound-to-type

Adapting to interpretation of (x:T) now activating scope for T if any.

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.
 

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.

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.

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,16 +150,16 @@ 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 |].
     apply semirings.flip_nonpos_mult_r.
      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.

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).

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,22 +198,22 @@ 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)).
   now apply AQsqrt_loop_snd_lower_bound.
 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.

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.

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.

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.