From 1432318faa4cb6a50eca2c7a371b43b3b9969666 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
Date: Fri, 25 Apr 2014 16:17:15 +0200
Subject: Pos.iter arguments in a better order for cbn.

---
 theories/PArith/BinPos.v    | 10 +++++-----
 theories/PArith/BinPosDef.v | 14 +++++++-------
 theories/PArith/Pnat.v      |  2 +-
 3 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'theories/PArith')

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.
-- 
cgit v1.2.3