From 7b64e1d3b368bca3c8b4ebe2ccacdf6d79eef815 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:40 +0000 Subject: 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 --- theories/PArith/BinPos.v | 8 ++------ theories/PArith/BinPosDef.v | 7 ++----- theories/PArith/Pnat.v | 10 +++++----- 3 files changed, 9 insertions(+), 16 deletions(-) (limited to 'theories/PArith') 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). -- cgit v1.2.3