diff options
Diffstat (limited to 'theories/Numbers/Integer/Axioms/ZTimes.v')
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZTimes.v | 47 |
1 files changed, 27 insertions, 20 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v index 5dc0b7505a..38311aa2b4 100644 --- a/theories/Numbers/Integer/Axioms/ZTimes.v +++ b/theories/Numbers/Integer/Axioms/ZTimes.v @@ -11,7 +11,7 @@ Notation "x * y" := (times x y) : IntScope. Add Morphism times with signature E ==> E ==> E as times_wd. Axiom times_0 : forall n, n * 0 == 0. -Axiom times_S : forall n m, n * (S m) == n * m + n. +Axiom times_succ : forall n m, n * (S m) == n * m + n. End ZTimesSignature. @@ -19,9 +19,9 @@ Module ZTimesProperties (Import ZTimesModule : ZTimesSignature). Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. Open Local Scope IntScope. -Theorem times_P : forall n m, n * (P m) == n * m - n. +Theorem times_pred : forall n m, n * (P m) == n * m - n. Proof. -intros n m. rewrite_S_P m at 2. rewrite times_S. rewrite <- plus_minus_distr. +intros n m. rewrite_succ_pred m at 2. rewrite times_succ. rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. Qed. @@ -29,26 +29,26 @@ Theorem times_0_n : forall n, 0 * n == 0. Proof. induct n. now rewrite times_0. -intros n IH. rewrite times_S. rewrite IH; now rewrite plus_0. -intros n IH. rewrite times_P. rewrite IH; now rewrite minus_0. +intros n IH. rewrite times_succ. rewrite IH; now rewrite plus_0. +intros n IH. rewrite times_pred. rewrite IH; now rewrite minus_0. Qed. -Theorem times_Sn_m : forall n m, (S n) * m == n * m + m. +Theorem times_succn_m : forall n m, (S n) * m == n * m + m. Proof. induct m. do 2 rewrite times_0. now rewrite plus_0. -intros m IH. do 2 rewrite times_S. rewrite IH. +intros m IH. do 2 rewrite times_succ. rewrite IH. do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity. -do 2 rewrite plus_n_Sm; now rewrite plus_comm. -intros m IH. do 2 rewrite times_P. rewrite IH. +do 2 rewrite plus_n_succm; now rewrite plus_comm. +intros m IH. do 2 rewrite times_pred. rewrite IH. rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr. apply plus_wd. reflexivity. -rewrite minus_S. now rewrite minus_Pn_m. +rewrite minus_succ. now rewrite minus_predn_m. Qed. -Theorem times_Pn_m : forall n m, (P n) * m == n * m - m. +Theorem times_predn_m : forall n m, (P n) * m == n * m - m. Proof. -intros n m. rewrite_S_P n at 2. rewrite times_Sn_m. +intros n m. rewrite_succ_pred n at 2. rewrite times_succn_m. rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0. Qed. @@ -56,17 +56,17 @@ Theorem times_comm : forall n m, n * m == m * n. Proof. intros n m; induct n. rewrite times_0_n; now rewrite times_0. -intros n IH. rewrite times_Sn_m; rewrite times_S; now rewrite IH. -intros n IH. rewrite times_Pn_m; rewrite times_P; now rewrite IH. +intros n IH. rewrite times_succn_m; rewrite times_succ; now rewrite IH. +intros n IH. rewrite times_predn_m; rewrite times_pred; now rewrite IH. Qed. Theorem times_opp_r : forall n m, n * (- m) == - (n * m). Proof. intros n m; induct m. rewrite uminus_0; rewrite times_0; now rewrite uminus_0. -intros m IH. rewrite uminus_S. rewrite times_P; rewrite times_S. rewrite IH. +intros m IH. rewrite uminus_succ. rewrite times_pred; rewrite times_succ. rewrite IH. rewrite <- plus_opp_minus; now rewrite opp_plus_distr. -intros m IH. rewrite uminus_P. rewrite times_P; rewrite times_S. rewrite IH. +intros m IH. rewrite uminus_pred. rewrite times_pred; rewrite times_succ. rewrite IH. now rewrite opp_minus_distr. Qed. @@ -85,9 +85,9 @@ Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p. Proof. intros n m p; induct m. rewrite times_0; now do 2 rewrite plus_0. -intros m IH. rewrite plus_S. do 2 rewrite times_S. rewrite IH. +intros m IH. rewrite plus_succ. do 2 rewrite times_succ. rewrite IH. do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm]. -intros m IH. rewrite plus_P. do 2 rewrite times_P. rewrite IH. +intros m IH. rewrite plus_pred. do 2 rewrite times_pred. rewrite IH. apply plus_minus_swap. Qed. @@ -113,8 +113,15 @@ Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p. Proof. intros n m p; induct p. now do 3 rewrite times_0. -intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH. -intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH. +intros p IH. do 2 rewrite times_succ. rewrite times_plus_distr_r. now rewrite IH. +intros p IH. do 2 rewrite times_pred. rewrite times_minus_distr_r. now rewrite IH. Qed. End ZTimesProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |