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

3 files changed, 8 insertions, 8 deletions

diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 08e1138f0..3c0bbbad9 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -325,8 +325,8 @@ Definition lxor n m :=
 
 (** Shifts *)
 
-Definition shiftl_nat (a:N)(n:nat) := nat_iter n double a.
-Definition shiftr_nat (a:N)(n:nat) := nat_iter n div2 a.
+Definition shiftl_nat (a:N)(n:nat) := nat_rect _ a (fun _ => double) n.
+Definition shiftr_nat (a:N)(n:nat) := nat_rect _ a (fun _ => div2) n.
 
 Definition shiftl a n :=
   match a with
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 4ea8e1d46..b50adaab8 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -86,7 +86,7 @@ Lemma Nshiftl_nat_equiv :
  forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.
 Proof.
  intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial.
- apply nat_iter_invariant; intros; now subst.
+ induction (Pos.to_nat n) as [|? H]; simpl; now try rewrite H.
  rewrite <- Pos2Nat.inj_iter. symmetry. now apply Pos.iter_swap_gen.
 Qed.
 
@@ -103,7 +103,7 @@ Lemma Nshiftr_nat_spec : forall a n m,
 Proof.
  induction n; intros m.
  now rewrite <- plus_n_O.
- simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S.
+ simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn.
  destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
@@ -113,7 +113,7 @@ Proof.
  induction n; intros m H.
  now rewrite <- minus_n_O.
  destruct m. inversion H. apply le_S_n in H.
- simpl. rewrite <- IHn, Nshiftl_nat_S; trivial.
+ simpl. rewrite <- IHn; trivial.
  destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
@@ -148,7 +148,7 @@ Lemma Pshiftl_nat_plus : forall n m p,
   Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.
 Proof.
  induction m; simpl; intros. reflexivity.
- rewrite 2 Pshiftl_nat_S. now f_equal.
+ now f_equal.
 Qed.
 
 (** Semantics of bitwise operations with respect to [N.testbit_nat] *)
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 1b7e2f241..346169e7f 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -113,7 +113,7 @@ Proof.
 Qed.
 
 Lemma inj_iter a {A} (f:A->A) (x:A) :
-  N.iter a f x = nat_iter (N.to_nat a) f x.
+  N.iter a f x = nat_rect (fun _ => A) x (fun _ => f) (N.to_nat a).
 Proof.
  destruct a as [|a]. trivial. apply Pos2Nat.inj_iter.
 Qed.
@@ -194,7 +194,7 @@ Lemma inj_max n n' :
 Proof. nat2N. Qed.
 
 Lemma inj_iter n {A} (f:A->A) (x:A) :
-  nat_iter n f x = N.iter (N.of_nat n) f x.
+  nat_rect (fun _ => A) x (fun _ => f) n = N.iter (N.of_nat n) f x.
 Proof. now rewrite N2Nat.inj_iter, !id. Qed.
 
 End Nat2N.