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

1 files changed, 68 insertions, 68 deletions

diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index facffef45..97a72e087 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -29,23 +29,23 @@ reasons we define an abstract semiring here. *)
 
 Open Local Scope NatScope.
 
-Lemma Nsemi_ring : semi_ring_theory 0 1 plus times Neq.
+Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq.
 Proof.
 constructor.
-exact plus_0_l.
-exact plus_comm.
-exact plus_assoc.
-exact times_1_l.
-exact times_0_l.
-exact times_comm.
-exact times_assoc.
-exact times_plus_distr_r.
+exact add_0_l.
+exact add_comm.
+exact add_assoc.
+exact mul_1_l.
+exact mul_0_l.
+exact mul_comm.
+exact mul_assoc.
+exact mul_add_distr_r.
 Qed.
 
 Add Ring NSR : Nsemi_ring.
 
-(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by
-the properties functor. Since we don't want Zplus_comm to refer to unfolded
+(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by
+the properties functor. Since we don't want Zadd_comm to refer to unfolded
 definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
 we will provide an extra layer of definitions. *)
 
@@ -61,13 +61,13 @@ elements is 0, and make all operations convert canonical values into other
 canonical values. In that case, we could get rid of setoids and arrive at
 integers as signed natural numbers. *)
 
-Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
+Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
 Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
 
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
 
-Definition Ztimes (n m : Z) : Z :=
+Definition Zmul (n m : Z) : Z :=
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
 Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
 Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
@@ -80,9 +80,9 @@ Notation "x == y"  := (Zeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
 Notation "0" := Z0 : IntScope.
 Notation "1" := (Zsucc Z0) : IntScope.
-Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x + y" := (Zadd x y) : IntScope.
 Notation "x - y" := (Zminus x y) : IntScope.
-Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x * y" := (Zmul x y) : IntScope.
 Notation "x < y" := (Zlt x y) : IntScope.
 Notation "x <= y" := (Zle x y) : IntScope.
 Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
@@ -91,7 +91,7 @@ Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
 Notation Local N := NZ.
 (* To remember N without having to use a long qualifying name. since NZ will be redefined *)
 Notation Local NE := NZeq (only parsing).
-Notation Local plus_wd := NZplus_wd (only parsing).
+Notation Local add_wd := NZadd_wd (only parsing).
 
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
@@ -101,9 +101,9 @@ Definition NZeq := Zeq.
 Definition NZ0 := Z0.
 Definition NZsucc := Zsucc.
 Definition NZpred := Zpred.
-Definition NZplus := Zplus.
+Definition NZadd := Zadd.
 Definition NZminus := Zminus.
-Definition NZtimes := Ztimes.
+Definition NZmul := Zmul.
 
 Theorem ZE_refl : reflexive Z Zeq.
 Proof.
@@ -119,10 +119,10 @@ Theorem ZE_trans : transitive Z Zeq.
 Proof.
 unfold transitive, Zeq. intros n m p H1 H2.
 assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
-by now apply plus_wd.
+by now apply add_wd.
 stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
 stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
-now apply -> plus_cancel_r in H3.
+now apply -> add_cancel_r in H3.
 Qed.
 
 Theorem NZeq_equiv : equiv Z Zeq.
@@ -144,20 +144,20 @@ Qed.
 Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
 Proof.
 unfold NZsucc, Zeq; intros n m H; simpl.
-do 2 rewrite plus_succ_l; now rewrite H.
+do 2 rewrite add_succ_l; now rewrite H.
 Qed.
 
 Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
 Proof.
 unfold NZpred, Zeq; intros n m H; simpl.
-do 2 rewrite plus_succ_r; now rewrite H.
+do 2 rewrite add_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd.
+Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd.
 Proof.
-unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
-by now apply plus_wd.
+by now apply add_wd.
 stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
@@ -167,28 +167,28 @@ Proof.
 unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
 assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
-by now apply plus_wd.
+by now apply add_wd.
 stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd.
+Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd.
 Proof.
-unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
-apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
+apply add_mul_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
 stepl (snd n1 * snd n2 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (snd n1 * fst n2 + (fst n1 * snd m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply plus_times_repl_pair with (n := snd m2) (m := fst m2);
+apply add_mul_repl_pair with (n := snd m2) (m := fst m2);
 [| (stepl (fst n2 + snd m2) by ring); now stepr (fst m2 + snd n2) by ring].
 stepl (snd m2 * snd n1 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (snd m2 * fst n1 + (snd n1 * fst m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply plus_times_repl_pair with (n := snd m1) (m := fst m1);
+apply add_mul_repl_pair with (n := snd m1) (m := fst m1);
 [ | (stepl (fst n1 + snd m1) by ring); now stepr (fst m1 + snd n1) by ring].
 stepl (fst m2 * fst n1 + (snd m2 * snd m1 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst m2 * snd n1 + (snd m2 * fst m1 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
+apply add_mul_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
 ring.
 Qed.
 
@@ -209,12 +209,12 @@ intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
-destruct (plus_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0, p)) by (rewrite plus_0_l; now rewrite plus_comm).
+destruct (add_dichotomy n m) as [[p H] | [p H]].
+rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
-rewrite (A_wd (n, m) (p, 0)) by now rewrite plus_0_r. apply H1.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
 induct p. assumption. intros p IH.
-apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l].
+apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite add_0_l, add_1_l].
 now apply <- AS.
 induct p. assumption. intros p IH.
 replace 0 with (snd (p, 0)); [| reflexivity].
@@ -230,39 +230,39 @@ Open Local Scope IntScope.
 Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
 Proof.
 unfold NZpred, NZsucc, Zeq; intro n; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
+rewrite add_succ_l; now rewrite add_succ_r.
 Qed.
 
-Theorem NZplus_0_l : forall n : Z, 0 + n == n.
+Theorem NZadd_0_l : forall n : Z, 0 + n == n.
 Proof.
-intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l.
+intro n; unfold NZadd, Zeq; simpl. now do 2 rewrite add_0_l.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
+Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
 Proof.
-intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l.
+intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l.
 Qed.
 
 Theorem NZminus_0_r : forall n : Z, n - 0 == n.
 Proof.
-intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r.
+intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite add_0_r.
 Qed.
 
 Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
 Proof.
-intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r.
+intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite add_succ_r.
 Qed.
 
-Theorem NZtimes_0_l : forall n : Z, 0 * n == 0.
+Theorem NZmul_0_l : forall n : Z, 0 * n == 0.
 Proof.
-intro n; unfold NZtimes, Zeq; simpl.
-repeat rewrite times_0_l. now rewrite plus_assoc.
+intro n; unfold NZmul, Zeq; simpl.
+repeat rewrite mul_0_l. now rewrite add_assoc.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.
+Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.
 Proof.
-intros n m; unfold NZtimes, NZsucc, Zeq; simpl.
-do 2 rewrite times_succ_l. ring.
+intros n m; unfold NZmul, NZsucc, Zeq; simpl.
+do 2 rewrite mul_succ_l. ring.
 Qed.
 
 End NZAxiomsMod.
@@ -275,20 +275,20 @@ Definition NZmax := Zmax.
 Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
 Proof.
 unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
-stepr (snd m1 + fst m2) by apply plus_comm.
-apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption].
-stepl (snd m2 + fst n1) by apply plus_comm.
-stepr (fst m2 + snd n1) by apply plus_comm.
-apply (plus_lt_repl_pair (snd n2) (fst n2)).
-now stepl (fst n1 + snd n2) by apply plus_comm.
-stepl (fst m2 + snd n2) by apply plus_comm. now stepr (fst n2 + snd m2) by apply plus_comm.
-stepr (snd n1 + fst n2) by apply plus_comm.
-apply (plus_lt_repl_pair (fst m1) (snd m1)); [| now symmetry].
-stepl (snd n2 + fst m1) by apply plus_comm.
-stepr (fst n2 + snd m1) by apply plus_comm.
-apply (plus_lt_repl_pair (snd m2) (fst m2)).
-now stepl (fst m1 + snd m2) by apply plus_comm.
-stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm.
+stepr (snd m1 + fst m2) by apply add_comm.
+apply (add_lt_repl_pair (fst n1) (snd n1)); [| assumption].
+stepl (snd m2 + fst n1) by apply add_comm.
+stepr (fst m2 + snd n1) by apply add_comm.
+apply (add_lt_repl_pair (snd n2) (fst n2)).
+now stepl (fst n1 + snd n2) by apply add_comm.
+stepl (fst m2 + snd n2) by apply add_comm. now stepr (fst n2 + snd m2) by apply add_comm.
+stepr (snd n1 + fst n2) by apply add_comm.
+apply (add_lt_repl_pair (fst m1) (snd m1)); [| now symmetry].
+stepl (snd n2 + fst m1) by apply add_comm.
+stepr (fst n2 + snd m1) by apply add_comm.
+apply (add_lt_repl_pair (snd m2) (fst m2)).
+now stepl (fst m1 + snd m2) by apply add_comm.
+stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm.
 Qed.
 
 Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
@@ -345,7 +345,7 @@ Qed.
 
 Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m.
 Proof.
-intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_r.
+intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite add_succ_l; apply lt_succ_r.
 Qed.
 
 Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
@@ -381,8 +381,8 @@ Notation "- x" := (Zopp x) : IntScope.
 Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 Proof.
 unfold Zeq; intros n m H; simpl. symmetry.
-stepl (fst n + snd m) by apply plus_comm.
-now stepr (fst m + snd n) by apply plus_comm.
+stepl (fst n + snd m) by apply add_comm.
+now stepr (fst m + snd n) by apply add_comm.
 Qed.
 
 Open Local Scope IntScope.
@@ -390,12 +390,12 @@ Open Local Scope IntScope.
 Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
 Proof.
 intro n; unfold Zsucc, Zpred, Zeq; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
+rewrite add_succ_l; now rewrite add_succ_r.
 Qed.
 
 Theorem Zopp_0 : - 0 == 0.
 Proof.
-unfold Zopp, Zeq; simpl. now rewrite plus_0_l.
+unfold Zopp, Zeq; simpl. now rewrite add_0_l.
 Qed.
 
 Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).