diff options
author | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
tree | 1a46f0142a85df553388c932110793881f3af52f /theories/Numbers/Natural/SpecViaZ | |
parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ')
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 10 |
2 files changed, 6 insertions, 6 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index aaf44ca6..0b8bded0 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 2c7884ac..37d5db10 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -318,7 +318,7 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. zify. intros. apply Z_div_mod_eq_full; auto. +intros a b. zify. intros. apply Z.div_mod; auto. Qed. Theorem mod_bound_pos : forall a b, 0<=a -> 0<b -> @@ -444,7 +444,7 @@ Qed. (** Recursion *) Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) := - Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n). + N.peano_rect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n). Arguments recursion [A] a f n. Instance recursion_wd (A : Type) (Aeq : relation A) : @@ -457,7 +457,7 @@ unfold NN.to_N. rewrite <- Exx'; clear x' Exx'. induction (Z.to_N [x]) using N.peano_ind. simpl; auto. -rewrite 2 Nrect_step. now apply Eff'. +rewrite 2 N.peano_rect_succ. now apply Eff'. Qed. Theorem recursion_0 : @@ -474,7 +474,7 @@ Proof. unfold eq, recursion; intros A Aeq a f EAaa f_wd n. replace (to_N (succ n)) with (N.succ (to_N n)) by (zify; now rewrite <- Z2N.inj_succ by apply spec_pos). -rewrite Nrect_step. +rewrite N.peano_rect_succ. apply f_wd; auto. zify. now rewrite Z2N.id by apply spec_pos. fold (recursion a f n). apply recursion_wd; auto. red; auto. |