diff options
| author | letouzey | 2008-06-02 23:26:13 +0000 |
|---|---|---|
| committer | letouzey | 2008-06-02 23:26:13 +0000 |
| commit | f82bfc64fca9fb46136d7aa26c09d64cde0432d2 (patch) | |
| tree | 471a75d813fb70072c384b926f334e27919cf889 /theories/Numbers/Integer/SpecViaZ | |
| parent | b37cc1ad85d2d1ac14abcd896f2939e871705f98 (diff) | |
In abstract parts of theories/Numbers, plus/times becomes add/mul,
for increased consistency with bignums parts
(commit part I: content of files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/SpecViaZ')
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 3d9d3d1901..bb56e6997c 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -41,9 +41,9 @@ Definition NZeq := Z.eq. Definition NZ0 := Z.zero. Definition NZsucc := Z.succ. Definition NZpred := Z.pred. -Definition NZplus := Z.add. +Definition NZadd := Z.add. Definition NZminus := Z.sub. -Definition NZtimes := Z.mul. +Definition NZmul := Z.mul. Theorem NZeq_equiv : equiv Z.t Z.eq. Proof. @@ -66,7 +66,7 @@ Proof. intros; zsimpl; f_equal; assumption. Qed. -Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd. +Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd. Proof. intros; zsimpl; f_equal; assumption. Qed. @@ -76,7 +76,7 @@ Proof. intros; zsimpl; f_equal; assumption. Qed. -Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd. +Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd. Proof. intros; zsimpl; f_equal; assumption. Qed. @@ -144,12 +144,12 @@ Qed. End Induction. -Theorem NZplus_0_l : forall n, 0 + n == n. +Theorem NZadd_0_l : forall n, 0 + n == n. Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). +Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). Proof. intros; zsimpl; auto with zarith. Qed. @@ -164,12 +164,12 @@ Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZtimes_0_l : forall n, 0 * n == 0. +Theorem NZmul_0_l : forall n, 0 * n == 0. Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m. +Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m. Proof. intros; zsimpl; ring. Qed. |