From ebb3fe944b6bd1cd363e3348465d7ea2fd85c62c Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 3 Jun 2008 00:04:16 +0000 Subject: In abstract parts of theories/Numbers, plus/times becomes add/mul, for increased consistency with bignums parts (commit part II: names of files + additional translation minus --> sub) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'theories/Numbers/Cyclic/Abstract') diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 113945e0de..92ada3d748 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -40,7 +40,7 @@ Definition NZ0 := w_op.(znz_0). Definition NZsucc := w_op.(znz_succ). Definition NZpred := w_op.(znz_pred). Definition NZadd := w_op.(znz_add). -Definition NZminus := w_op.(znz_sub). +Definition NZsub := w_op.(znz_sub). Definition NZmul := w_op.(znz_mul). Theorem NZeq_equiv : equiv NZ NZeq. @@ -71,7 +71,7 @@ unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). now rewrite H1, H2. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). now rewrite H1, H2. @@ -93,7 +93,7 @@ Notation "'S'" := NZsucc : IntScope. Notation "'P'" := NZpred : IntScope. (*Notation "1" := (S 0) : IntScope.*) Notation "x + y" := (NZadd x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. +Notation "x - y" := (NZsub x y) : IntScope. Notation "x * y" := (NZmul x y) : IntScope. Theorem gt_wB_1 : 1 < wB. @@ -204,15 +204,15 @@ rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. Qed. -Theorem NZminus_0_r : forall n : NZ, n - 0 == n. +Theorem NZsub_0_r : forall n : NZ, n - 0 == n. Proof. -intro n; unfold NZminus, NZ0, NZeq. rewrite w_spec.(spec_sub). +intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub). rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. -Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Proof. -intros n m; unfold NZminus, NZsucc, NZpred, NZeq. +intros n m; unfold NZsub, NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r. rewrite Zminus_mod_idemp_l. -- cgit v1.2.3