diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZAdd.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 87 |
1 files changed, 43 insertions, 44 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index c9bb5c95..9535cfdb 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -8,84 +8,83 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NZAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id$ i*) -Require Import NZAxioms. -Require Import NZBase. +Require Import NZAxioms NZBase. -Module NZAddPropFunct (Import NZAxiomsMod : NZAxiomsSig). -Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod. -Open Local Scope NatIntScope. +Module Type NZAddPropSig + (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). -Theorem NZadd_0_r : forall n : NZ, n + 0 == n. +Hint Rewrite + pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. +Ltac nzsimpl := autorewrite with nz. + +Theorem add_0_r : forall n, n + 0 == n. Proof. -NZinduct n. now rewrite NZadd_0_l. -intro. rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +nzinduct n. now nzsimpl. +intro. nzsimpl. now rewrite succ_inj_wd. Qed. -Theorem NZadd_succ_r : forall n m : NZ, n + S m == S (n + m). +Theorem add_succ_r : forall n m, n + S m == S (n + m). Proof. -intros n m; NZinduct n. -now do 2 rewrite NZadd_0_l. -intro. repeat rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +intros n m; nzinduct n. now nzsimpl. +intro. nzsimpl. now rewrite succ_inj_wd. Qed. -Theorem NZadd_comm : forall n m : NZ, n + m == m + n. +Hint Rewrite add_0_r add_succ_r : nz. + +Theorem add_comm : forall n m, n + m == m + n. Proof. -intros n m; NZinduct n. -rewrite NZadd_0_l; now rewrite NZadd_0_r. -intros n. rewrite NZadd_succ_l; rewrite NZadd_succ_r. now rewrite NZsucc_inj_wd. +intros n m; nzinduct n. now nzsimpl. +intro. nzsimpl. now rewrite succ_inj_wd. Qed. -Theorem NZadd_1_l : forall n : NZ, 1 + n == S n. +Theorem add_1_l : forall n, 1 + n == S n. Proof. -intro n; rewrite NZadd_succ_l; now rewrite NZadd_0_l. +intro n; now nzsimpl. Qed. -Theorem NZadd_1_r : forall n : NZ, n + 1 == S n. +Theorem add_1_r : forall n, n + 1 == S n. Proof. -intro n; rewrite NZadd_comm; apply NZadd_1_l. +intro n; now nzsimpl. Qed. -Theorem NZadd_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p. +Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. -intros n m p; NZinduct n. -now do 2 rewrite NZadd_0_l. -intro. do 3 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +intros n m p; nzinduct n. now nzsimpl. +intro. nzsimpl. now rewrite succ_inj_wd. Qed. -Theorem NZadd_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q). +Theorem add_cancel_l : forall n m p, p + n == p + m <-> n == m. Proof. -intros n m p q. -rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_comm m (p + q)). -rewrite <- (NZadd_assoc p q m). rewrite (NZadd_assoc n p (q + m)). -now rewrite (NZadd_comm q m). +intros n m p; nzinduct p. now nzsimpl. +intro p. nzsimpl. now rewrite succ_inj_wd. Qed. -Theorem NZadd_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p). +Theorem add_cancel_r : forall n m p, n + p == m + p <-> n == m. Proof. -intros n m p q. -rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_assoc m p q). -rewrite (NZadd_comm (m + p) q). now rewrite <- (NZadd_assoc n q (m + p)). +intros n m p. rewrite (add_comm n p), (add_comm m p). apply add_cancel_l. Qed. -Theorem NZadd_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m. +Theorem add_shuffle0 : forall n m p, n+m+p == n+p+m. Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +intros n m p. rewrite <- 2 add_assoc, add_cancel_l. apply add_comm. Qed. -Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. +Theorem add_shuffle1 : forall n m p q, (n + m) + (p + q) == (n + p) + (m + q). Proof. -intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). -apply NZadd_cancel_l. +intros n m p q. rewrite 2 add_assoc, add_cancel_r. apply add_shuffle0. Qed. -Theorem NZsub_1_r : forall n : NZ, n - 1 == P n. +Theorem add_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p). Proof. -intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r. +intros n m p q. +rewrite 2 add_assoc, add_shuffle0, add_cancel_r. apply add_shuffle0. Qed. -End NZAddPropFunct. +Theorem sub_1_r : forall n, n - 1 == P n. +Proof. +intro n; now nzsimpl. +Qed. +End NZAddPropSig. |