Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)

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

8 files changed, 45 insertions, 50 deletions

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index d3d7b5835..b4468dd1b 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -258,30 +258,6 @@ Qed.
 
 Unset Implicit Arguments.
 
-(** [n]th iteration of the function [f] *)
-
-Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) : A :=
-  match n with
-    | O => x
-    | S n' => f (iter_nat n' A f x)
-  end.
-
-Theorem iter_nat_plus :
-  forall (n m:nat) (A:Type) (f:A -> A) (x:A),
-    iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
-Proof.
-  induction n; simpl; trivial.
-  intros. now f_equal.
-Qed.
-
-(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv],
-    then the iterates of [f] also preserve it. *)
-
-Theorem iter_nat_invariant :
-  forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop),
-    (forall x:A, Inv x -> Inv (f x)) ->
-    forall x:A, Inv x -> Inv (iter_nat n A f x).
-Proof.
-  induction n; simpl; trivial.
-  intros A f Inv Hf x Hx. apply Hf, IHn; trivial.
-Qed.
+Notation iter_nat := @nat_iter (only parsing).
+Notation iter_nat_plus := @nat_iter_plus (only parsing).
+Notation iter_nat_invariant := @nat_iter_invariant (only parsing).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 03487b6d6..cfe78b40c 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -261,3 +261,30 @@ Proof.
 induction n; destruct m; simpl; auto. inversion 1.
 intros. apply f_equal. apply IHn. apply le_S_n. trivial.
 Qed.
+
+(** [n]th iteration of the function [f] *)
+
+Fixpoint nat_iter (n:nat) {A} (f:A->A) (x:A) : A :=
+  match n with
+    | O => x
+    | S n' => f (nat_iter n' f x)
+  end.
+
+Theorem nat_iter_plus :
+  forall (n m:nat) {A} (f:A -> A) (x:A),
+    nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
+Proof.
+  induction n; intros; simpl; rewrite ?IHn; trivial.
+Qed.
+
+(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv],
+    then the iterates of [f] also preserve it. *)
+
+Theorem nat_iter_invariant :
+  forall (n:nat) {A} (f:A -> A) (P : A -> Prop),
+    (forall x, P x -> P (f x)) ->
+    forall x, P x -> P (nat_iter n f x).
+Proof.
+  induction n; simpl; trivial.
+  intros A f P Hf x Hx. apply Hf, IHn; trivial.
+Qed.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 7d9f4d64f..f150f12c8 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -8,7 +8,7 @@
 
 Require Export BinNums.
 Require Import BinPos RelationClasses Morphisms Setoid
- Equalities GenericMinMax Wf_nat Bool NAxioms NProperties.
+ Equalities GenericMinMax Bool NAxioms NProperties.
 Require BinNatDef.
 
 (**********************************************************************)
@@ -36,10 +36,6 @@ Module N
 
 Include BinNatDef.N.
 
-(* TODO : fix the location of iter_nat *)
-Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a.
-Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a.
-
 (** Logical predicates *)
 
 Definition eq := @Logic.eq t.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index cb5cfe7f0..535f88c86 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -316,6 +316,9 @@ 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 a n :=
   match a with
     | 0 => 0
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 4ef91362f..5284afe95 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -9,7 +9,7 @@
 
 Require Export BinNums.
 Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
- Equalities Orders GenericMinMax Le Plus Wf_nat.
+ Equalities Orders GenericMinMax Le Plus.
 
 Require Export BinPosDef.
 
@@ -38,10 +38,6 @@ Module Pos
 
 Include BinPosDef.Pos.
 
-(* TODO : fix the location of iter_nat *)
-Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
-Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p.
-
 (** * Logical Predicates *)
 
 Definition eq := @Logic.eq t.
@@ -1882,7 +1878,7 @@ Notation Pminus_mask := Pos.sub_mask (only parsing).
 Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing).
 Notation Pminus := Pos.sub (only parsing).
 Notation Pmult := Pos.mul (only parsing).
-Notation iter_pos p A := (@Pos.iter p A) (only parsing).
+Notation iter_pos := @Pos.iter (only parsing).
 Notation Ppow := Pos.pow (only parsing).
 Notation Pdiv2 := Pos.div2 (only parsing).
 Notation Pdiv2_up := Pos.div2_up (only parsing).
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index cf7e450f4..9b6081176 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -478,11 +478,8 @@ Fixpoint lxor (p q:positive) : N :=
 
 (** Shifts. NB: right shift of 1 stays at 1. *)
 
-(*
-Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
-
-Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p.
-*)
+Definition shiftl_nat (p:positive)(n:nat) := nat_iter n xO p.
+Definition shiftr_nat (p:positive)(n:nat) := nat_iter n div2 p.
 
 Definition shiftl (p:positive)(n:N) :=
   match n with
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 5c46c8210..a0ca9f5b6 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec Wf_nat.
+Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec.
 
 (** Properties of the injection from binary positive numbers
     to Peano natural numbers *)
@@ -143,11 +143,11 @@ Proof.
  now apply lt_le_weak, inj_lt.
 Qed.
 
-(** [Pos.to_nat] is a morphism for [iter_pos] and [iter_nat] *)
+(** [Pos.to_nat] is a morphism for [Pos.iter] and [nat_iter] *)
 
 Theorem inj_iter :
-  forall p (A:Type) (f:A->A) (x:A),
-    Pos.iter p f x = iter_nat (to_nat p) _ f x.
+  forall p {A} (f:A->A) (x:A),
+    Pos.iter p f x = nat_iter (to_nat p) f x.
 Proof.
  induction p using peano_ind. trivial.
  intros. rewrite inj_succ, iter_succ. simpl. now f_equal.
@@ -298,7 +298,7 @@ Notation Pgt_gt := Pos2Nat.inj_gt (only parsing).
 Notation Ple_le := Pos2Nat.inj_le (only parsing).
 Notation Pge_ge := Pos2Nat.inj_ge (only parsing).
 Notation Pminus_minus := Pos2Nat.inj_sub (only parsing).
-Notation iter_nat_of_P := Pos2Nat.inj_iter (only parsing).
+Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing).
 
 Notation nat_of_P_of_succ_nat := SuccNat2Pos.bij (only parsing).
 Notation P_of_succ_nat_of_P := Pos2SuccNat.bij (only parsing).
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index c021b01a9..ce99427f2 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -243,7 +243,7 @@ Section power_div_with_rest.
 	simpl in |- *;
 	  [ trivial with zarith
 	    | intro n; rewrite (two_power_nat_S n); unfold Zdiv_rest_aux at 2 in |- *;
-	      elim (iter_nat n (Z * Z * Z) Zdiv_rest_aux (x, 0, 1));
+	      elim (iter_nat n _ Zdiv_rest_aux (x, 0, 1));
 		destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z);
 		  assumption ].
   Qed.
@@ -302,7 +302,7 @@ Section power_div_with_rest.
   Proof.
     intros x p.
     generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-    elim (iter_pos p (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)).
+    elim (iter_pos p _ Zdiv_rest_aux (x, 0, 1)).
     simple induction a.
     intros.
     elim H; intros H1 H2; clear H.