Merge PR #6155: Get rid of ' notation for Zpos in QArith

8 files changed, 48 insertions, 50 deletions

diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index abf8be72e..d163dfbcd 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -40,7 +40,7 @@ Proof.
 Qed.
 
 
-Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z.
+Lemma QdenZpower : forall x : Q, Zpos (Qden (x ^ 2)%Q) = (Zpos (Qden x) ^ 2) %Z.
 Proof.
   intros.
   destruct x.
@@ -54,9 +54,9 @@ Qed.
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
  unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
+ assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
  by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
- apply integer_statement; exists (Qnum x); exists (' Qden x); auto.
+ apply integer_statement; exists (Qnum x); exists (Zpos (Qden x)); auto.
 Qed.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 467f263be..35706e7fa 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -227,9 +227,7 @@ Infix "/" := Qdiv : Q_scope.
 
 (** A light notation for [Zpos] *)
 
-Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope.
-
-Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b).
+Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).
 Proof.
 unfold Qeq. simpl. ring.
 Qed.
@@ -242,9 +240,9 @@ Proof.
   Open Scope Z_scope.
   intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
   simpl_mult; ring_simplify.
-  replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring.
+  replace (p1 * Zpos r2 * Zpos q2) with (p1 * Zpos q2 * Zpos r2) by ring.
   rewrite H.
-  replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring.
+  replace (r1 * Zpos p2 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * Zpos p2 * Zpos q2) by ring.
   rewrite H0.
   ring.
   Close Scope Z_scope.
@@ -255,7 +253,7 @@ Proof.
   unfold Qeq, Qopp; simpl.
   Open Scope Z_scope.
   intros x y H; simpl.
-  replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring.
+  replace (- Qnum x * Zpos (Qden y)) with (- (Qnum x * Zpos (Qden y))) by ring.
   rewrite H;  ring.
   Close Scope Z_scope.
 Qed.
@@ -272,9 +270,9 @@ Proof.
   Open Scope Z_scope.
   intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
   intros; simpl_mult; ring_simplify.
-  replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring.
+  replace (q1 * s1 * Zpos p2) with (q1 * Zpos p2 * s1) by ring.
   rewrite <- H.
-  replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring.
+  replace (p1 * r1 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * p1 * Zpos q2) by ring.
   rewrite H0.
   ring.
   Close Scope Z_scope.
@@ -305,13 +303,13 @@ Proof.
   unfold Qeq, Qcompare.
   Open Scope Z_scope.
   intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *.
-  rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)).
-  rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)).
-  change ('(q2*s2)) with ('q2 * 's2).
-  change ('(p2*r2)) with ('p2 * 'r2).
-  replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring.
+  rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)).
+  rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)).
+  change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2).
+  change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2).
+  replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring.
   rewrite H.
-  replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring.
+  replace (Zpos q2 * Zpos s2 * (r1*Zpos p2)) with ((r1*Zpos s2)*Zpos q2*Zpos p2) by ring.
   rewrite H'.
   f_equal; ring.
   Close Scope Z_scope.
@@ -572,8 +570,8 @@ Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
 Proof.
   unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
   Open Scope Z_scope.
-  apply Z.mul_le_mono_pos_r with ('y2); [easy|].
-  apply Z.le_trans with (y1 * 'x2 * 'z2).
+  apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|].
+  apply Z.le_trans with (y1 * Zpos x2 * Zpos z2).
   - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
   - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
     now apply Z.mul_le_mono_pos_r.
@@ -620,8 +618,8 @@ Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
 Proof.
   unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
   Open Scope Z_scope.
-  apply Z.mul_lt_mono_pos_r with ('y2); [easy|].
-  apply Z.le_lt_trans with (y1 * 'x2 * 'z2).
+  apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].
+  apply Z.le_lt_trans with (y1 * Zpos x2 * Zpos z2).
   - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
   - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
     now apply Z.mul_lt_mono_pos_r.
@@ -632,8 +630,8 @@ Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z.
 Proof.
   unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
   Open Scope Z_scope.
-  apply Z.mul_lt_mono_pos_r with ('y2); [easy|].
-  apply Z.lt_le_trans with (y1 * 'x2 * 'z2).
+  apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].
+  apply Z.lt_le_trans with (y1 * Zpos x2 * Zpos z2).
   - rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r.
   - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
     now apply Z.mul_le_mono_pos_r.
@@ -723,9 +721,9 @@ Proof.
   match goal with |- ?a <= ?b => ring_simplify a b end.
   rewrite Z.add_comm.
   apply Z.add_le_mono.
-  match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+  match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.
   auto with zarith.
-  match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+  match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.
   auto with zarith.
   Close Scope Z_scope.
 Qed.
@@ -740,9 +738,9 @@ Proof.
   match goal with |- ?a < ?b => ring_simplify a b end.
   rewrite Z.add_comm.
   apply Z.add_le_lt_mono.
-  match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+  match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.
   auto with zarith.
-  match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+  match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.
   do 2 (apply Z.mul_lt_mono_pos_r;try easy).
   Close Scope Z_scope.
 Qed.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 48be89417..31eb41bc9 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -28,8 +28,8 @@ intros [xn xd] [yn yd] H.
 simpl.
 unfold Qeq in *.
 simpl in *.
-change (' yd)%Z with (Z.abs (' yd)).
-change (' xd)%Z with (Z.abs (' xd)).
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
 repeat rewrite <- Z.abs_mul.
 congruence.
 Qed.
@@ -88,8 +88,8 @@ unfold Qplus.
 unfold Qle.
 simpl.
 apply Z.mul_le_mono_nonneg_r;auto with *.
-change (' yd)%Z with (Z.abs (' yd)).
-change (' xd)%Z with (Z.abs (' xd)).
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
 repeat rewrite <- Z.abs_mul.
 apply Z.abs_triangle.
 Qed.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index e25f69c31..1510a7b82 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -30,7 +30,7 @@ Lemma Qred_identity :
 Proof.
   intros (a,b) H; simpl in *.
   rewrite <- Z.ggcd_gcd in H.
-  generalize (Z.ggcd_correct_divisors a ('b)).
+  generalize (Z.ggcd_correct_divisors a (Zpos b)).
   destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst.
   rewrite !Z.mul_1_l. now intros (<-,<-).
 Qed.
@@ -39,7 +39,7 @@ Lemma Qred_identity2 :
   forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
 Proof.
   intros (a,b) H; simpl in *.
-  generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+  generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
   rewrite <- Z.ggcd_gcd.
   destruct Z.ggcd as (g,(aa,bb)); simpl in *.
   injection H as <- <-. intros H (_,H').
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 3fd78f092..010782209 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -90,7 +90,7 @@ rewrite Qinv_power.
 reflexivity.
 Qed.
 
-Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n.
+Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z (Zpos p))^n.
 Proof.
 intros n p.
 rewrite Qmake_Qdiv.
@@ -190,7 +190,7 @@ unfold Z.succ.
 rewrite Zpower_exp; auto with *; try discriminate.
 rewrite Qpower_plus' by discriminate.
 rewrite <- IHn by discriminate.
-replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring.
+replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring.
 ring_simplify.
 reflexivity.
 Qed.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 14ab1700e..c83296259 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -167,8 +167,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden.
 simpl; intros; elim H; trivial.
 intros; field; auto. 
 intros;
-  change (IZR (Zneg x2)) with (- IZR (' x2))%R;
-  change (IZR (Zneg p)) with (- IZR (' p))%R;
+  change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R;
+  change (IZR (Zneg p)) with (- IZR (Zpos p))%R;
   simpl; field; (*auto 8 with real.*)
   repeat split; auto; auto with real.
 Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 7b08515d2..17307c827 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -21,14 +21,14 @@ Notation Z2P_correct := Z2Pos.id (only parsing).
 
 Definition Qred (q:Q) :=
   let (q1,q2) := q in
-  let (r1,r2) := snd (Z.ggcd q1 ('q2))
+  let (r1,r2) := snd (Z.ggcd q1 (Zpos q2))
   in r1#(Z.to_pos r2).
 
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
   unfold Qred, Qeq; intros (n,d); simpl.
-  generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d))
-    (Z.ggcd_correct_divisors n ('d)).
+  generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d))
+    (Z.ggcd_correct_divisors n (Zpos d)).
   destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl.
   Open Scope Z_scope.
   intros Hg LE (Hn,Hd). rewrite Hd, Hn.
@@ -45,13 +45,13 @@ Proof.
   unfold Qred, Qeq in *; simpl in *.
   Open Scope Z_scope.
   intros H.
-  generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
-    (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+  generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b))
+    (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
   destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).
   simpl. intros <- Hg1 Hg2 (Hg3,Hg4).
   assert (Hg0 : g <> 0) by (intro; now subst g).
-  generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
-    (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)).
+  generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d))
+    (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)).
   destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).
   simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4).
   assert (Hg'0 : g' <> 0) by (intro; now subst g').
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index e4e974972..7c5ddbb6a 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -80,11 +80,11 @@ unfold Qlt.
 simpl.
 replace (n*1)%Z with n by ring.
 ring_simplify.
-replace (n / ' d * ' d + ' d)%Z with
-  (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring.
+replace (n / Zpos d * Zpos d + Zpos d)%Z with
+  ((Zpos d * (n / Zpos d) + n mod Zpos  d) + Zpos  d - n mod Zpos d)%Z by ring.
 rewrite <- Z_div_mod_eq; auto with*.
 rewrite <- Z.lt_add_lt_sub_r.
-destruct (Z_mod_lt n ('d)); auto with *.
+destruct (Z_mod_lt n (Zpos d)); auto with *.
 Qed.
 
 Hint Resolve Qlt_floor : qarith.
@@ -107,9 +107,9 @@ Proof.
 intros [xn xd] [yn yd] Hxy.
 unfold Qle in *.
 simpl in *.
-rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *.
-rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *.
-rewrite (Z.mul_comm ('yd) ('xd)).
+rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *.
+rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *.
+rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
 apply Z_div_le; auto with *.
 Qed.