Pos.iter arguments in a better order for cbn.

10 files changed, 35 insertions, 35 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 61a77bf0e..256dce782 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -944,7 +944,7 @@ Proof.
  destruct n as [|n]; simpl in *.
  destruct m. now destruct p. elim (Pos.nlt_1_r _ H).
  rewrite Pos.iter_succ. simpl.
- set (u:=Pos.iter n xO p) in *; clearbody u.
+ set (u:=Pos.iter xO p n) in *; clearbody u.
  destruct m as [|m]. now destruct u.
  rewrite <- (IHn (Pos.pred_N m)).
  rewrite <- (testbit_odd_succ _ (Pos.pred_N m)).
@@ -968,7 +968,7 @@ Proof.
  rewrite <- IHn.
  rewrite testbit_succ_r_div2 by apply le_0_l.
  f_equal. simpl. rewrite Pos.iter_succ.
- now destruct (Pos.iter n xO p).
+ now destruct (Pos.iter xO p n).
  apply succ_le_mono. now rewrite succ_pos_pred.
 Qed.
 
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index c4e6bd254..6aeeccaf5 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -337,7 +337,7 @@ Definition shiftl a n :=
 Definition shiftr a n :=
   match n with
     | 0 => a
-    | pos p => Pos.iter p div2 a
+    | pos p => Pos.iter div2 a p
   end.
 
 (** Checking whether a particular bit is set or not *)
@@ -375,7 +375,7 @@ Definition of_nat (n:nat) :=
 Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
   match n with
     | 0 => x
-    | pos p => Pos.iter p f x
+    | pos p => Pos.iter f x p
   end.
 
 End N.
\ No newline at end of file
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 5aa31d7bd..03fc58c55 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -2232,7 +2232,7 @@ Section Int31_Specs.
    2: simpl; unfold Z.pow_pos; simpl; auto with zarith.
    case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4.
    unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4.
-   unfold phi2,Z.pow, Z.pow_pos. simpl Pos.iter; auto with zarith. }
+   unfold phi2. cbn [Z.pow Z.pow_pos Pos.iter]. auto with zarith. }
  case (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith.
  change [|Tn|] with 2147483647; auto with zarith.
  intros j1 _ HH; contradict HH.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index d576c3eb4..a30c555c1 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -576,21 +576,21 @@ Qed.
 
 Lemma iter_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B),
  (forall a, f (g a) = h (f a)) -> forall p a,
- f (iter p g a) = iter p h (f a).
+ f (iter g a p) = iter h (f a) p.
 Proof.
  induction p; simpl; intros; now rewrite ?H, ?IHp.
 Qed.
 
 Theorem iter_swap :
   forall p (A:Type) (f:A -> A) (x:A),
-    iter p f (f x) = f (iter p f x).
+    iter f (f x) p = f (iter f x p).
 Proof.
  intros. symmetry. now apply iter_swap_gen.
 Qed.
 
 Theorem iter_succ :
   forall p (A:Type) (f:A -> A) (x:A),
-    iter (succ p) f x = f (iter p f x).
+    iter f x (succ p) = f (iter f x p).
 Proof.
  induction p as [p IHp|p IHp|]; intros; simpl; trivial.
  now rewrite !IHp, iter_swap.
@@ -598,7 +598,7 @@ Qed.
 
 Theorem iter_add :
   forall p q (A:Type) (f:A -> A) (x:A),
-    iter (p+q) f x = iter p f (iter q f x).
+    iter f x (p+q) = iter f (iter f x q) p.
 Proof.
  induction p using peano_ind; intros.
  now rewrite add_1_l, iter_succ.
@@ -608,7 +608,7 @@ Qed.
 Theorem iter_invariant :
   forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
-    forall x:A, Inv x -> Inv (iter p f x).
+    forall x:A, Inv x -> Inv (iter f x p).
 Proof.
  induction p as [p IHp|p IHp|]; simpl; trivial.
  intros A f Inv H x H0. apply H, IHp, IHp; trivial.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 4541fce0d..aed4fef05 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -195,16 +195,16 @@ Infix "*" := mul : positive_scope.
 
 (** ** Iteration over a positive number *)
 
-Fixpoint iter (n:positive) {A} (f:A -> A) (x:A) : A :=
-  match n with
+Definition iter {A} (f:A -> A) : A -> positive -> A :=
+  fix iter_fix x n := match n with
     | xH => f x
-    | xO n' => iter n' f (iter n' f x)
-    | xI n' => f (iter n' f (iter n' f x))
+    | xO n' => iter_fix (iter_fix x n') n'
+    | xI n' => f (iter_fix (iter_fix x n') n')
   end.
 
 (** ** Power *)
 
-Definition pow (x y:positive) := iter y (mul x) 1.
+Definition pow (x:positive) := iter (mul x) 1.
 
 Infix "^" := pow : positive_scope.
 
@@ -488,13 +488,13 @@ Definition shiftr_nat (p:positive) := nat_rect _ p (fun _ => div2).
 Definition shiftl (p:positive)(n:N) :=
   match n with
     | N0 => p
-    | Npos n => iter n xO p
+    | Npos n => iter xO p n
   end.
 
 Definition shiftr (p:positive)(n:N) :=
   match n with
     | N0 => p
-    | Npos n => iter n div2 p
+    | Npos n => iter div2 p n
   end.
 
 (** Checking whether a particular bit is set or not *)
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 12042f76c..9ce399beb 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -192,7 +192,7 @@ Qed.
 
 Theorem inj_iter :
   forall p {A} (f:A->A) (x:A),
-    Pos.iter p f x = nat_rect (fun _ => A) x (fun _ => f) (to_nat p).
+    Pos.iter f x p = nat_rect (fun _ => A) x (fun _ => f) (to_nat p).
 Proof.
  induction p using peano_ind. trivial.
  intros. rewrite inj_succ, iter_succ. simpl. now f_equal.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 6948d420a..452e3d148 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -959,7 +959,7 @@ Proof.
   destruct m; easy || now destruct Hm.
  destruct a as [ |a|a].
  (* a = 0 *)
- replace (Pos.iter n div2 0) with 0
+ replace (Pos.iter div2 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
  now rewrite 2 testbit_0_l.
  (* a > 0 *)
@@ -982,7 +982,7 @@ Proof.
   rewrite ?Pos.iter_succ; apply testbit_even_0.
  destruct a as [ |a|a].
  (* a = 0 *)
- replace (Pos.iter n (mul 2) 0) with 0
+ replace (Pos.iter (mul 2) 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
  apply testbit_0_l.
  (* a > 0 *)
@@ -1013,7 +1013,7 @@ Proof.
   f_equal. now rewrite Pos.add_comm, Pos.add_sub.
  destruct a; unfold shiftl.
  (* ... a = 0 *)
- replace (Pos.iter n (mul 2) 0) with 0
+ replace (Pos.iter (mul 2) 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
  now rewrite 2 testbit_0_l.
  (* ... a > 0 *)
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 958ce2ef7..4e7fdcdff 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -126,7 +126,7 @@ Infix "*" := mul : Z_scope.
 
 (** ** Power function *)
 
-Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.
+Definition pow_pos (z:Z) := Pos.iter (mul z) 1.
 
 Definition pow x y :=
   match y with
@@ -306,7 +306,7 @@ Definition to_pos (z:Z) : positive :=
 
 Definition iter (n:Z) {A} (f:A -> A) (x:A) :=
   match n with
-    | pos p => Pos.iter p f x
+    | pos p => Pos.iter f x p
     | _ => x
   end.
 
@@ -568,8 +568,8 @@ Definition testbit a n :=
 Definition shiftl a n :=
  match n with
    | 0 => a
-   | pos p => Pos.iter p (mul 2) a
-   | neg p => Pos.iter p div2 a
+   | pos p => Pos.iter (mul 2) a p
+   | neg p => Pos.iter div2 a p
  end.
 
 Definition shiftr a n := shiftl a (-n).
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v
index f3eb63a8a..73b1989e4 100644
--- a/theories/ZArith/Zpow_alt.v
+++ b/theories/ZArith/Zpow_alt.v
@@ -30,12 +30,12 @@ Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
 
 Lemma Piter_mul_acc : forall f,
  (forall x y:Z, (f x)*y = f (x*y)) ->
- forall p k, Pos.iter p f k = (Pos.iter p f 1)*k.
+ forall p k, Pos.iter f k p = (Pos.iter f 1 p)*k.
 Proof.
  intros f Hf.
  induction p; simpl; intros.
- - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Hf, Z.mul_assoc.
- - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Z.mul_assoc.
+ - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Hf, Z.mul_assoc.
+ - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Z.mul_assoc.
  - now rewrite Hf, Z.mul_1_l.
 Qed.
 
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 7ccaa119c..1da3c7992 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -95,11 +95,11 @@ Section Powers_of_2.
       [m] shifted by [n] positions *)
 
   Definition shift_nat (n:nat) (z:positive) := nat_rect _ z (fun _ => xO) n.
-  Definition shift_pos (n z:positive) := Pos.iter n xO z.
+  Definition shift_pos (n z:positive) := Pos.iter xO z n.
   Definition shift (n:Z) (z:positive) :=
     match n with
       | Z0 => z
-      | Zpos p => Pos.iter p xO z
+      | Zpos p => Pos.iter xO z p
       | Zneg p => z
     end.
 
@@ -247,10 +247,10 @@ Section power_div_with_rest.
        end, 2 * d).
 
   Definition Zdiv_rest (x:Z) (p:positive) :=
-    let (qr, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in qr.
+    let (qr, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in qr.
 
   Lemma Zdiv_rest_correct1 (x:Z) (p:positive) :
-    let (_, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+    let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
     d = two_power_pos p.
   Proof.
    rewrite Pos2Nat.inj_iter, two_power_pos_nat.
@@ -260,7 +260,7 @@ Section power_div_with_rest.
   Qed.
 
   Lemma Zdiv_rest_correct2 (x:Z) (p:positive) :
-    let '(q,r,d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+    let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
     x = q * d + r /\ 0 <= r < d.
   Proof.
    apply Pos.iter_invariant; [|omega].
@@ -287,7 +287,7 @@ Section power_div_with_rest.
   Lemma Zdiv_rest_correct (x:Z) (p:positive) : Zdiv_rest_proofs x p.
   Proof.
     generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-    destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+    destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d).
     intros (H1,(H2,H3)) ->. now exists q r.
   Qed.
 
@@ -299,7 +299,7 @@ Section power_div_with_rest.
   Proof.
    unfold Zdiv_rest.
    generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-   destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+   destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d).
    intros H ->. now rewrite two_power_pos_equiv in H.
   Qed.