nat_iter n f x -> nat_rect _ x (fun _ => f) n

It is much beter for everything (includind guard condition and simpl refolding)
excepts typeclasse inference because unification does not recognize
(fun x => f x b) a when it sees f a b ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16112 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 0d9b08d6b..616445d06 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -25,7 +25,7 @@ Local Open Scope Z_scope.
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1.
+Definition Zpower_nat (z:Z) (n:nat) := nat_rect _ 1 (fun _ => Z.mul z) n.
 
 Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
 Proof. reflexivity. Qed.
@@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp :
 Proof.
  induction n.
  - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
- - intros. simpl. now rewrite 2 Zpower_nat_succ_r, IHn, Z.mul_assoc.
+ - intros. simpl. now rewrite IHn, Z.mul_assoc.
 Qed.
 
 (** Conversions between powers of unary and binary integers *)
@@ -94,7 +94,7 @@ Section Powers_of_2.
       calculus is possible. [shift n m] computes [2^n * m], i.e.
       [m] shifted by [n] positions *)
 
-  Definition shift_nat (n:nat) (z:positive) := nat_iter n xO z.
+  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 (n:Z) (z:positive) :=
     match n with
@@ -154,7 +154,7 @@ Section Powers_of_2.
   Lemma shift_nat_plus n m x :
     shift_nat (n + m) x = shift_nat n (shift_nat m x).
   Proof.
-   apply iter_nat_plus.
+   induction n; simpl; now f_equal.
   Qed.
 
   Theorem shift_nat_correct n x :
@@ -255,7 +255,7 @@ Section power_div_with_rest.
   Proof.
    rewrite Pos2Nat.inj_iter, two_power_pos_nat.
    induction (Pos.to_nat p); simpl; trivial.
-   destruct (nat_iter n Zdiv_rest_aux (x,0,1)) as ((q,r),d).
+   destruct (nat_rect _ _ _ n) as ((q,r),d).
    unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal.
   Qed.