diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:40 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:40 +0000 |
commit | 7b64e1d3b368bca3c8b4ebe2ccacdf6d79eef815 (patch) | |
tree | 17a859cb5664a0ac0f4b0839cedc8f25ccb8ef93 | |
parent | 88cf0acb11ae2b4a7e0fb7df8289c15eb0748f19 (diff) |
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
-rw-r--r-- | theories/Arith/Wf_nat.v | 30 | ||||
-rw-r--r-- | theories/Init/Peano.v | 27 | ||||
-rw-r--r-- | theories/NArith/BinNat.v | 6 | ||||
-rw-r--r-- | theories/NArith/BinNatDef.v | 3 | ||||
-rw-r--r-- | theories/PArith/BinPos.v | 8 | ||||
-rw-r--r-- | theories/PArith/BinPosDef.v | 7 | ||||
-rw-r--r-- | theories/PArith/Pnat.v | 10 | ||||
-rw-r--r-- | theories/ZArith/Zpower.v | 4 |
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. |