From ec8332223b1f6716e49bbf78e0489881ca7bfa2b Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 21 Dec 2012 21:47:43 +0000 Subject: 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 --- theories/NArith/BinNatDef.v | 4 ++-- theories/NArith/Ndigits.v | 8 ++++---- theories/NArith/Nnat.v | 4 ++-- 3 files changed, 8 insertions(+), 8 deletions(-) (limited to 'theories/NArith') 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. -- cgit v1.2.3