diff options
-rw-r--r-- | theories/NArith/BinNat.v | 4 | ||||
-rw-r--r-- | theories/NArith/BinNatDef.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 | ||||
-rw-r--r-- | theories/PArith/BinPos.v | 10 | ||||
-rw-r--r-- | theories/PArith/BinPosDef.v | 14 | ||||
-rw-r--r-- | theories/PArith/Pnat.v | 2 | ||||
-rw-r--r-- | theories/ZArith/BinInt.v | 6 | ||||
-rw-r--r-- | theories/ZArith/BinIntDef.v | 8 | ||||
-rw-r--r-- | theories/ZArith/Zpow_alt.v | 6 | ||||
-rw-r--r-- | theories/ZArith/Zpower.v | 14 |
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. |