Pos.compare_cont takes the comparison as first argument

Helps cbn tactic refolding

3 files changed, 25 insertions, 25 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 7f478546e..d576c3eb4 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -766,15 +766,15 @@ Definition switch_Eq c c' :=
  end.
 
 Lemma compare_cont_spec p q c :
-  compare_cont p q c = switch_Eq c (p ?= q).
+  compare_cont c p q = switch_Eq c (p ?= q).
 Proof.
   unfold compare.
   revert q c.
   induction p; destruct q; simpl; trivial.
   intros c.
-  rewrite 2 IHp. now destruct (compare_cont p q Eq).
+  rewrite 2 IHp. now destruct (compare_cont Eq p q).
   intros c.
-  rewrite 2 IHp. now destruct (compare_cont p q Eq).
+  rewrite 2 IHp. now destruct (compare_cont Eq p q).
 Qed.
 
 (** From this general result, we now describe particular cases
@@ -785,31 +785,31 @@ Qed.
 *)
 
 Theorem compare_cont_Eq p q c :
- compare_cont p q c = Eq -> c = Eq.
+ compare_cont c p q = Eq -> c = Eq.
 Proof.
   rewrite compare_cont_spec. now destruct (p ?= q).
 Qed.
 
 Lemma compare_cont_Lt_Gt p q :
-  compare_cont p q Lt = Gt <-> p > q.
+  compare_cont Lt p q = Gt <-> p > q.
 Proof.
   rewrite compare_cont_spec. unfold gt. destruct (p ?= q); now split.
 Qed.
 
 Lemma compare_cont_Lt_Lt p q :
-  compare_cont p q Lt = Lt <-> p <= q.
+  compare_cont Lt p q = Lt <-> p <= q.
 Proof.
   rewrite compare_cont_spec. unfold le. destruct (p ?= q); easy'.
 Qed.
 
 Lemma compare_cont_Gt_Lt p q :
-  compare_cont p q Gt = Lt <-> p < q.
+  compare_cont Gt p q = Lt <-> p < q.
 Proof.
   rewrite compare_cont_spec. unfold lt. destruct (p ?= q); now split.
 Qed.
 
 Lemma compare_cont_Gt_Gt p q :
-  compare_cont p q Gt = Gt <-> p >= q.
+  compare_cont Gt p q = Gt <-> p >= q.
 Proof.
   rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'.
 Qed.
@@ -874,13 +874,13 @@ Qed.
 (** Basic facts about [compare_cont] *)
 
 Theorem compare_cont_refl p c :
-  compare_cont p p c = c.
+  compare_cont c p p = c.
 Proof.
   now induction p.
 Qed.
 
 Lemma compare_cont_antisym p q c :
-  CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c).
+  CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p.
 Proof.
   revert q c.
   induction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl;
@@ -1903,7 +1903,7 @@ Notation Pdiv2 := Pos.div2 (compat "8.3").
 Notation Pdiv2_up := Pos.div2_up (compat "8.3").
 Notation Psize := Pos.size_nat (compat "8.3").
 Notation Psize_pos := Pos.size (compat "8.3").
-Notation Pcompare := Pos.compare_cont (compat "8.3").
+Notation Pcompare x y m := (Pos.compare_cont m x y) (compat "8.3").
 Notation Plt := Pos.lt (compat "8.3").
 Notation Pgt := Pos.gt (compat "8.3").
 Notation Ple := Pos.le (compat "8.3").
@@ -2062,11 +2062,11 @@ Lemma Pplus_one_succ_r p : Pos.succ p = p + 1.
 Proof (eq_sym (Pos.add_1_r p)).
 Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p.
 Proof (eq_sym (Pos.add_1_l p)).
-Lemma Pcompare_refl p : Pos.compare_cont p p Eq = Eq.
+Lemma Pcompare_refl p : Pos.compare_cont Eq p p = Eq.
 Proof (Pos.compare_cont_refl p Eq).
-Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont p q Eq = Eq -> p = q.
+Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont Eq p q = Eq -> p = q.
 Proof Pos.compare_eq.
-Lemma ZC4 p q : Pos.compare_cont p q Eq = CompOpp (Pos.compare_cont q p Eq).
+Lemma ZC4 p q : Pos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p).
 Proof (Pos.compare_antisym q p).
 Lemma Ppred_minus p : Pos.pred p = p - 1.
 Proof (eq_sym (Pos.sub_1_r p)).
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 61bee69f8..6674943a6 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -255,20 +255,20 @@ Fixpoint size p :=
 
 (** ** Comparison on binary positive numbers *)
 
-Fixpoint compare_cont (x y:positive) (r:comparison) {struct y} : comparison :=
+Fixpoint compare_cont (r:comparison) (x y:positive) {struct y} : comparison :=
   match x, y with
-    | p~1, q~1 => compare_cont p q r
-    | p~1, q~0 => compare_cont p q Gt
+    | p~1, q~1 => compare_cont r p q
+    | p~1, q~0 => compare_cont Gt p q
     | p~1, 1 => Gt
-    | p~0, q~1 => compare_cont p q Lt
-    | p~0, q~0 => compare_cont p q r
+    | p~0, q~1 => compare_cont Lt p q
+    | p~0, q~0 => compare_cont r p q
     | p~0, 1 => Gt
     | 1, q~1 => Lt
     | 1, q~0 => Lt
     | 1, 1 => r
   end.
 
-Definition compare x y := compare_cont x y Eq.
+Definition compare x y := compare_cont Eq x y.
 
 Infix "?=" := compare (at level 70, no associativity) : positive_scope.
 
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 33505ccb3..12042f76c 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -410,24 +410,24 @@ Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (compat "8.3").
 Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (compat "8.3").
 
 Lemma nat_of_P_minus_morphism p q :
- Pos.compare_cont p q Eq = Gt ->
+ Pos.compare_cont Eq p q = Gt ->
   Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
 Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)).
 
 Lemma nat_of_P_lt_Lt_compare_morphism p q :
- Pos.compare_cont p q Eq = Lt -> Pos.to_nat p < Pos.to_nat q.
+ Pos.compare_cont Eq p q = Lt -> Pos.to_nat p < Pos.to_nat q.
 Proof (proj1 (Pos2Nat.inj_lt p q)).
 
 Lemma nat_of_P_gt_Gt_compare_morphism p q :
- Pos.compare_cont p q Eq = Gt -> Pos.to_nat p > Pos.to_nat q.
+ Pos.compare_cont Eq p q = Gt -> Pos.to_nat p > Pos.to_nat q.
 Proof (proj1 (Pos2Nat.inj_gt p q)).
 
 Lemma nat_of_P_lt_Lt_compare_complement_morphism p q :
- Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont p q Eq = Lt.
+ Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont Eq p q = Lt.
 Proof (proj2 (Pos2Nat.inj_lt p q)).
 
 Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
- Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont p q Eq = Gt.
+ Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont Eq p q = Gt.
 Proof (proj2 (Pos2Nat.inj_gt p q)).
 
 (** Old intermediate results about [Pmult_nat] *)