diff options
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 19 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 20 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDec.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDomain.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZOrder.v | 560 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlus.v | 256 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlusOrder.v | 390 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPred.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimes.v | 155 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimesOrder.v | 194 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigInts/EZBase.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigInts/Zeqmod.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsAxioms.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsOrder.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsPlus.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsTimes.v | 6 |
17 files changed, 810 insertions, 841 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index d3c0410ea..ab863eb1f 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -10,14 +10,17 @@ Open Local Scope NatIntScope. Notation Z := NZ (only parsing). Notation E := NZE (only parsing). -(** Integers are obtained by postulating that every number has a predecessor *) -Axiom S_P : forall n : Z, S (P n) == n. +Parameter Inline Zopp : Z -> Z. -End ZAxiomsSig. +Add Morphism Zopp with signature E ==> E as Zopp_wd. + +Notation "- x" := (Zopp x) (at level 35, right associativity) : NatIntScope. + +(* Integers are obtained by postulating that every number has a predecessor *) +Axiom Zsucc_pred : forall n : Z, S (P n) == n. +Axiom Zopp_0 : - 0 == 0. +Axiom Zopp_succ : forall n : Z, - (S n) == P (- n). + +End ZAxiomsSig. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 8f5c284e7..9f5ff8bd3 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -6,6 +6,9 @@ Open Local Scope NatIntScope. Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. +Theorem Zpred_succ : forall n : Z, P (S n) == n. +Proof NZpred_succ. + Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n. Proof NZneq_symm. @@ -25,10 +28,17 @@ forall A : Z -> Prop, predicate_wd E A -> forall n : Z, A n. Proof NZcentral_induction. +(* Theorems that are true for integers but not for natural numbers *) + +Theorem Zpred_inj : forall n m : Z, P n == P m -> n == m. +Proof. +intros n m H. apply NZsucc_wd in H. now do 2 rewrite Zsucc_pred in H. +Qed. + +Theorem Zpred_inj_wd : forall n1 n2 : Z, P n1 == P n2 <-> n1 == n2. +Proof. +intros n1 n2; split; [apply Zpred_inj | apply NZpred_wd]. +Qed. + End ZBasePropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v index 9a7aaa099..843b48b93 100644 --- a/theories/Numbers/Integer/Abstract/ZDec.v +++ b/theories/Numbers/Integer/Abstract/ZDec.v @@ -1,8 +1,3 @@ Axiom E_equiv_e : forall x y : Z, E x y <-> e x y. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v index 028128cf7..7ace860f3 100644 --- a/theories/Numbers/Integer/Abstract/ZDomain.v +++ b/theories/Numbers/Integer/Abstract/ZDomain.v @@ -55,8 +55,3 @@ Declare Right Step (proj1 (proj2 E_equiv)). End ZDomainProperties. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v index cc834b442..295f5355a 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZOrder.v @@ -1,458 +1,296 @@ -Require Export ZAxioms. +Require Export ZTimes. -Module Type ZOrderSignature. -Declare Module Export ZBaseMod : ZBaseSig. -Open Local Scope IntScope. +Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod. +Open Local Scope NatIntScope. -Parameter Inline lt : Z -> Z -> bool. -Parameter Inline le : Z -> Z -> bool. -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +(* Axioms *) -Notation "n < m" := (lt n m) : IntScope. -Notation "n <= m" := (le n m) : IntScope. +Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m. +Proof NZle_lt_or_eq. -Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m. -Axiom lt_irr : forall n, ~ (n < n). -Axiom lt_succ : forall n m, n < (S m) <-> n <= m. +Theorem Zlt_irrefl : forall n : Z, ~ n < n. +Proof NZlt_irrefl. -End ZOrderSignature. +Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m. +Proof NZlt_succ_le. +(* Renaming theorems from NZOrder.v *) -Module ZOrderProperties (Import ZOrderModule : ZOrderSignature). -Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod. -Open Local Scope IntScope. +Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m. +Proof NZlt_le_incl. -Ltac Zle_intro1 := rewrite le_lt; left. -Ltac Zle_intro2 := rewrite le_lt; right. -Ltac Zle_elim H := rewrite le_lt in H; destruct H as [H | H]. +Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m. +Proof NZlt_neq. -Theorem le_refl : forall n, n <= n. -Proof. -intro n; now Zle_intro2. -Qed. +Theorem Zle_refl : forall n : Z, n <= n. +Proof NZle_refl. -Theorem lt_n_succn : forall n, n < S n. -Proof. -intro n. rewrite lt_succ. now Zle_intro2. -Qed. +Theorem Zlt_succ_r : forall n : Z, n < S n. +Proof NZlt_succ_r. -Theorem le_n_succn : forall n, n <= S n. -Proof. -intro; Zle_intro1; apply lt_n_succn. -Qed. +Theorem Zle_succ_r : forall n : Z, n <= S n. +Proof NZle_succ_r. -Theorem lt_predn_n : forall n, P n < n. -Proof. -intro n; rewrite_succ_pred n at 2; apply lt_n_succn. -Qed. +Theorem Zlt_lt_succ : forall n m : Z, n < m -> n < S m. +Proof NZlt_lt_succ. -Theorem le_predn_n : forall n, P n <= n. -Proof. -intro; Zle_intro1; apply lt_predn_n. -Qed. +Theorem Zle_le_succ : forall n m : Z, n <= m -> n <= S m. +Proof NZle_le_succ. -Theorem lt_n_succm : forall n m, n < m -> n < S m. -Proof. -intros. rewrite lt_succ. now Zle_intro1. -Qed. +Theorem Zle_succ_le_or_eq_succ : forall n m : Z, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_le_or_eq_succ. -Theorem le_n_succm : forall n m, n <= m -> n <= S m. -Proof. -intros n m H; rewrite <- lt_succ in H; now Zle_intro1. -Qed. +Theorem Zneq_succ_l : forall n : Z, S n ~= n. +Proof NZneq_succ_l. -Theorem lt_n_m_pred : forall n m, n < m <-> n <= P m. -Proof. -intros n m; rewrite_succ_pred m; rewrite pred_succ; apply lt_succ. -Qed. +Theorem Znlt_succ_l : forall n : Z, ~ S n < n. +Proof NZnlt_succ_l. -Theorem not_le_n_predn : forall n, ~ n <= P n. -Proof. -intros n H; Zle_elim H. -apply lt_n_succm in H; rewrite succ_pred in H; false_hyp H lt_irr. -pose proof (lt_predn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr. -Qed. +Theorem Znle_succ_l : forall n : Z, ~ S n <= n. +Proof NZnle_succ_l. -Theorem le_succ : forall n m, n <= S m <-> n <= m \/ n == S m. -Proof. -intros n m; rewrite le_lt. now rewrite lt_succ. -Qed. +Theorem Zlt_le_succ : forall n m : Z, n < m <-> S n <= m. +Proof NZlt_le_succ. -Theorem lt_pred : forall n m, (P n) < m <-> n <= m. -Proof. -intro n; induct_n m (P n). -split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_predn. -intros m IH; split; intro H. -apply -> lt_succ in H; Zle_elim H. -apply -> IH in H; now apply le_n_succm. -rewrite <- H; rewrite succ_pred; now Zle_intro2. -apply -> le_succ in H; destruct H as [H | H]. -apply <- IH in H. now apply lt_n_succm. rewrite H; rewrite pred_succ; apply lt_n_succn. -intros m IH; split; intro H. -pose proof H as H1. apply lt_n_succm in H; rewrite succ_pred in H. -apply -> IH in H; Zle_elim H. now apply -> lt_n_m_pred. -rewrite H in H1; false_hyp H1 lt_irr. -pose proof H as H1. apply le_n_succm in H. rewrite succ_pred in H. -apply <- IH in H. apply -> lt_n_m_pred in H. Zle_elim H. -assumption. apply pred_inj in H; rewrite H in H1; false_hyp H1 not_le_n_predn. -Qed. +Theorem Zlt_succ_lt : forall n m : Z, S n < m -> n < m. +Proof NZlt_succ_lt. -Theorem lt_predn_m : forall n m, n < m -> P n < m. -Proof. -intros; rewrite lt_pred; now Zle_intro1. -Qed. +Theorem Zle_succ_le : forall n m : Z, S n <= m -> n <= m. +Proof NZle_succ_le. -Theorem le_predn_m : forall n m, n <= m -> P n <= m. -Proof. -intros n m H; rewrite <- lt_pred in H; now Zle_intro1. -Qed. +Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m. +Proof NZsucc_lt_mono. -Theorem lt_n_m_succ : forall n m, n < m <-> S n <= m. -Proof. -intros n m; rewrite_pred_succ n; rewrite succ_pred; apply lt_pred. -Qed. +Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m. +Proof NZsucc_le_mono. -Theorem lt_succn_m : forall n m, S n < m -> n < m. -Proof. -intros n m H; rewrite_pred_succ n; now apply lt_predn_m. -Qed. +Theorem Zlt_asymm : forall n m, n < m -> ~ m < n. +Proof NZlt_asymm. -Theorem le_succn_m : forall n m, S n <= m -> n <= m. -Proof. -intros n m H; rewrite <- lt_n_m_succ in H; now Zle_intro1. -Qed. +Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p. +Proof NZlt_trans. -Theorem lt_n_predm : forall n m, n < P m -> n < m. -Proof. -intros n m H; rewrite_succ_pred m; now apply lt_n_succm. -Qed. +Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p. +Proof NZle_trans. -Theorem le_n_predm : forall n m, n <= P m -> n <= m. -Proof. -intros n m H; rewrite <- lt_n_m_pred in H; now Zle_intro1. -Qed. +Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p. +Proof NZle_lt_trans. -Theorem lt_respects_succ : forall n m, n < m <-> S n < S m. -Proof. -intros n m. rewrite lt_n_m_succ. symmetry. apply lt_succ. -Qed. +Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p. +Proof NZlt_le_trans. -Theorem le_respects_succ : forall n m, n <= m <-> S n <= S m. -Proof. -intros n m. do 2 rewrite le_lt. -firstorder using lt_respects_succ succ_wd succ_inj. -Qed. +Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m. +Proof NZle_antisymm. -Theorem lt_respects_pred : forall n m, n < m <-> P n < P m. -Proof. -intros n m. rewrite lt_n_m_pred. symmetry; apply lt_pred. -Qed. +(** Trichotomy, decidability, and double negation elimination *) -Theorem le_respects_pred : forall n m, n <= m <-> P n <= P m. -Proof. -intros n m. do 2 rewrite le_lt. -firstorder using lt_respects_pred pred_wd pred_inj. -Qed. +Theorem Zlt_trichotomy : forall n m : Z, n < m \/ n == m \/ m < n. +Proof NZlt_trichotomy. -Theorem lt_succ_pred : forall n m, S n < m <-> n < P m. -Proof. -intros n m; rewrite_pred_succ n at 2; apply lt_respects_pred. -Qed. +Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m. +Proof NZle_gt_cases. -Theorem le_succ_pred : forall n m, S n <= m <-> n <= P m. -Proof. -intros n m; rewrite_pred_succ n at 2; apply le_respects_pred. -Qed. +Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m. +Proof NZlt_ge_cases. -Theorem lt_pred_succ : forall n m, P n < m <-> n < S m. -Proof. -intros n m; rewrite_succ_pred n at 2; apply lt_respects_succ. -Qed. +Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m. +Proof NZle_ngt. -Theorem le_pred_succ : forall n m, P n <= m <-> n <= S m. -Proof. -intros n m; rewrite_succ_pred n at 2; apply le_respects_succ. -Qed. +Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m. +Proof NZnlt_ge. -Theorem lt_neq : forall n m, n < m -> n # m. -Proof. -intros n m H1 H2; rewrite H2 in H1; false_hyp H1 lt_irr. -Qed. +Theorem Zlt_em : forall n m : Z, n < m \/ ~ n < m. +Proof NZlt_em. -Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. -Proof. -intros n m; induct_n n m. -intros p H _; false_hyp H lt_irr. -intros n IH p H1 H2. apply lt_succn_m in H1. pose proof (IH p H1 H2) as H3. -rewrite lt_n_m_succ in H3; Zle_elim H3. -assumption. rewrite <- H3 in H2. rewrite lt_succ in H2; Zle_elim H2. -elimtype False; apply lt_irr with (n := n); now apply IH. -rewrite H2 in H1; false_hyp H1 lt_irr. -intros n IH p H1 H2. apply lt_predn_m. rewrite lt_pred in H1; Zle_elim H1. -now apply IH. now rewrite H1. -Qed. +Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m. +Proof NZlt_dne. -Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. -Proof. -intros n m p H1 H2; Zle_elim H1. -Zle_elim H2. Zle_intro1; now apply lt_trans with (m := m). -Zle_intro1; now rewrite <- H2. now rewrite H1. -Qed. +Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m. +Proof NZnle_gt. -Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. -Proof. -intros n m p H1 H2; Zle_elim H1. -now apply lt_trans with (m := m). now rewrite H1. -Qed. +Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m. +Proof NZlt_nge. -Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. -Proof. -intros n m p H1 H2; Zle_elim H2. -now apply lt_trans with (m := m). now rewrite <- H2. -Qed. +Theorem Zle_em : forall n m : Z, n <= m \/ ~ n <= m. +Proof NZle_em. -Theorem lt_asymm : forall n m, n < m -> ~ m < n. -Proof. -intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m). -Qed. +Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m. +Proof NZle_dne. -Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m. -Proof. -intros n m H1 H2; Zle_elim H1; Zle_elim H2. -elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m). -now symmetry. assumption. assumption. -Qed. +Theorem Zlt_nlt_succ : forall n m : Z, n < m <-> ~ m < S n. +Proof NZlt_nlt_succ. -Theorem not_lt_succn_n : forall n, ~ S n < n. -Proof. -intros n H; apply (lt_asymm n (S n)). apply lt_n_succn. assumption. -Qed. +Theorem Zlt_exists_pred : + forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k. +Proof NZlt_exists_pred. -Theorem not_le_succn_n : forall n, ~ S n <= n. -Proof. -intros n H; Zle_elim H. false_hyp H not_lt_succn_n. -pose proof (lt_n_succn n) as H1. rewrite H in H1; false_hyp H1 lt_irr. -Qed. +Theorem Zlt_succ_iter_r : + forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m. +Proof NZlt_succ_iter_r. -Theorem lt_gt : forall n m, n < m -> m < n -> False. -Proof. -intros n m H1 H2; apply lt_irr with (n := n); now apply lt_trans with (m := m). -Qed. +Theorem Zneq_succ_iter_l : + forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m. +Proof NZneq_succ_iter_l. + +(** Stronger variant of induction with assumptions n >= 0 (n < 0) +in the induction step *) + +Theorem Zright_induction : + forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + forall n : Z, z <= n -> A n. +Proof NZright_induction. -Theorem lt_total : forall n m, n < m \/ n == m \/ m < n. +Theorem Zleft_induction : + forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, A z -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : Z, n <= z -> A n. +Proof NZleft_induction. + +Theorem Zorder_induction : + forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : Z, A n. +Proof NZorder_induction. + +Theorem Zorder_induction' : + forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + (forall n : Z, n <= z -> A n -> A (P n)) -> + forall n : Z, A n. Proof. -intros n m; induct_n n m. -right; now left. -intros n IH; destruct IH as [H | [H | H]]. -rewrite lt_n_m_succ in H. rewrite le_lt in H; tauto. -right; right; rewrite H; apply lt_n_succn. -right; right; now apply lt_n_succm. -intros n IH; destruct IH as [H | [H | H]]. -left; now apply lt_predn_m. -left; rewrite H; apply lt_predn_n. -rewrite lt_n_m_pred in H. rewrite le_lt in H. -setoid_replace (m == P n) with (P n == m) in H using relation iff. tauto. -split; intro; now symmetry. +intros A A_wd z Az AS AP n; apply Zorder_induction with (z := z); try assumption. +intros m H1 H2. apply AP in H2; [| now apply -> Zlt_le_succ]. +unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); +[assumption | apply Zpred_succ]. Qed. -Theorem le_gt : forall n m, n <= m <-> ~ m < n. +Theorem Zright_induction' : + forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, + (forall n : Z, n <= z -> A n) -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + forall n : Z, A n. +Proof NZright_induction'. + +Theorem Zstrong_right_induction' : + forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, + (forall n : Z, n <= z -> A n) -> + (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) -> + forall n : Z, A n. +Proof NZstrong_right_induction'. + +(** Elimintation principle for < *) + +Theorem Zlt_ind : + forall A : Z -> Prop, predicate_wd E A -> + forall n : Z, + A (S n) -> + (forall m : Z, n < m -> A m -> A (S m)) -> + forall m : Z, n < m -> A m. +Proof NZlt_ind. + +(** Elimintation principle for <= *) + +Theorem Zle_ind : + forall A : Z -> Prop, predicate_wd E A -> + forall n : Z, + A n -> + (forall m : Z, n <= m -> A m -> A (S m)) -> + forall m : Z, n <= m -> A m. +Proof NZle_ind. + +Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction with (z := 0)). + +(** Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zlt_pred_l : forall n : Z, P n < n. Proof. -intros n m. rewrite -> le_lt. -pose proof (lt_total n m). pose proof (lt_gt n m). -assert (n == m -> ~ m < n); [intro A; rewrite A; apply lt_irr |]. -tauto. +intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_r. Qed. -Theorem lt_ge : forall n m, n < m <-> ~ m <= n. +Theorem Zle_pred_l : forall n : Z, P n <= n. Proof. -intros n m. rewrite -> le_lt. -pose proof (lt_total m n). pose proof (lt_gt n m). -assert (n < m -> m # n); [intros A B; rewrite B in A; false_hyp A lt_irr |]. -tauto. +intro; le_less; apply Zlt_pred_l. Qed. -Theorem lt_discrete : forall n m, n < m -> m < S n -> False. +Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m. Proof. -intros n m H1 H2; apply -> lt_succ in H2; apply -> lt_ge in H1; false_hyp H2 H1. +intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_le. Qed. -(* Decidability of order can be proved either from totality or from the fact -that < and <= are boolean functions *) - -(** A corollary of having an order is that Z is infinite in both -directions *) - -Theorem neq_succn_n : forall n, S n # n. +Theorem Znle_pred_r : forall n : Z, ~ n <= P n. Proof. -intros n H. pose proof (lt_n_succn n) as H1. rewrite H in H1. false_hyp H1 lt_irr. +intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl. Qed. -Theorem neq_predn_n : forall n, P n # n. +Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m. Proof. -intros n H. apply succ_wd in H. rewrite succ_pred in H. now apply neq_succn_n with (n := n). +intros n m; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). +apply Zlt_le_succ. Qed. -Definition nth_succ (n : nat) (m : Z) := - nat_rec (fun _ => Z) m (fun _ l => S l) n. -Definition nth_pred (n : nat) (m : Z) := - nat_rec (fun _ => Z) m (fun _ l => P l) n. - -Lemma lt_m_succkm : - forall (n : nat) (m : Z), m < nth_succ (Datatypes.S n) m. +Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m. Proof. -intros n m; induction n as [| n IH]; simpl in *. -apply lt_n_succn. now apply lt_n_succm. +intros; apply <- Zlt_pred_le; le_less. Qed. -Lemma lt_predkm_m : - forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m < m. +Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m. Proof. -intros n m; induction n as [| n IH]; simpl in *. -apply lt_predn_n. now apply lt_predn_m. +intros; le_less; now apply <- Zlt_pred_le. Qed. -Theorem neq_m_succkm : - forall (n : nat) (m : Z), nth_succ (Datatypes.S n) m # m. +Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m. Proof. -intros n m H. pose proof (lt_m_succkm n m) as H1. rewrite H in H1. -false_hyp H1 lt_irr. +intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l]. Qed. -Theorem neq_predkm_m : - forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m # m. +Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m. Proof. -intros n m H. pose proof (lt_predkm_m n m) as H1. rewrite H in H1. -false_hyp H1 lt_irr. +intros; le_less; now apply <- Zlt_le_pred. Qed. -(** Stronger variant of induction with assumptions n >= 0 (n <= 0) -in the induction step *) - -Section Induction. - -Variable A : Z -> Prop. -Hypothesis Q_wd : predicate_wd E A. - -Add Morphism A with signature E ==> iff as Q_morph. -Proof Q_wd. - -Section Center. - -Variable z : Z. (* A z is the basis of induction *) - -Section RightInduction. - -Let Q' := fun n : Z => forall m, z <= m -> m < n -> A m. - -Add Morphism Q' with signature E ==> iff as Q'_pos_wd. +Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m. Proof. -intros x1 x2 H; unfold Q'; qmorphism x1 x2. +intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le. Qed. -Theorem right_induction : - A z -> (forall n, z <= n -> A n -> A (S n)) -> forall n, z <= n -> A n. +Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m. Proof. -intros Qz QS k k_ge_z. -assert (H : forall n, Q' n). induct_n n z; unfold Q'. -intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1. -intros n IH m H2 H3. -rewrite lt_succ in H3; Zle_elim H3. now apply IH. -Zle_elim H2. rewrite_succ_pred m. -apply QS. now apply -> lt_n_m_pred. apply IH. now apply -> lt_n_m_pred. -rewrite H3; apply lt_predn_n. now rewrite <- H2. -intros n IH m H2 H3. apply IH. assumption. now apply lt_n_predm. -pose proof (H (S k)) as H1; unfold Q' in H1. apply H1. -apply k_ge_z. apply lt_n_succn. +intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred. Qed. -End RightInduction. - -Section LeftInduction. - -Let Q' := fun n : Z => forall m, m <= z -> n < m -> A m. - -Add Morphism Q' with signature E ==> iff as Q'_neg_wd. +Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m. Proof. -intros x1 x2 H; unfold Q'; qmorphism x1 x2. +intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ. Qed. -Theorem left_induction : - A z -> (forall n, n <= z -> A n -> A (P n)) -> forall n, n <= z -> A n. +Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m. Proof. -intros Qz QP k k_le_z. -assert (H : forall n, Q' n). induct_n n z; unfold Q'. -intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1. -intros n IH m H2 H3. apply IH. assumption. now apply lt_succn_m. -intros n IH m H2 H3. -rewrite lt_pred in H3; Zle_elim H3. now apply IH. -Zle_elim H2. rewrite_pred_succ m. -apply QP. now apply -> lt_n_m_succ. apply IH. now apply -> lt_n_m_succ. -rewrite H3; apply lt_n_succn. now rewrite H2. -pose proof (H (P k)) as H1; unfold Q' in H1. apply H1. -apply k_le_z. apply lt_predn_n. +intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ. Qed. -End LeftInduction. - -Theorem induction_ord_n : - A z -> - (forall n, z <= n -> A n -> A (S n)) -> - (forall n, n <= z -> A n -> A (P n)) -> - forall n, A n. +Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m. Proof. -intros Qz QS QP n. -destruct (lt_total n z) as [H | [H | H]]. -now apply left_induction; [| | Zle_intro1]. -now rewrite H. -now apply right_induction; [| | Zle_intro1]. +intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_le. Qed. -End Center. - -Theorem induction_ord : - A 0 -> - (forall n, 0 <= n -> A n -> A (S n)) -> - (forall n, n <= 0 -> A n -> A (P n)) -> - forall n, A n. -Proof (induction_ord_n 0). - -Theorem lt_ind : forall (n : Z), - A (S n) -> - (forall m : Z, n < m -> A m -> A (S m)) -> - forall m : Z, n < m -> A m. +Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m. Proof. -intros n H1 H2 m H3. -apply right_induction with (S n). assumption. -intros; apply H2; try assumption. now apply <- lt_n_m_succ. -now apply -> lt_n_m_succ. +intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_succ. Qed. -Theorem le_ind : forall (n : Z), - A n -> - (forall m : Z, n <= m -> A m -> A (S m)) -> - forall m : Z, n <= m -> A m. +Theorem Zneq_pred_l : forall n : Z, P n ~= n. Proof. -intros n H1 H2 m H3. -now apply right_induction with n. +intro; apply Zlt_neq; apply Zlt_pred_l. Qed. -End Induction. - -Ltac induct_ord n := - try intros until n; - pattern n; apply induction_ord; clear n; - [unfold NumPrelude.predicate_wd; - let n := fresh "n" in - let m := fresh "m" in - let H := fresh "H" in intros n m H; qmorphism n m | | |]. - -End ZOrderProperties. - - +End ZOrderPropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v index 624f85f04..c22b346b4 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZPlus.v @@ -1,228 +1,218 @@ -Require Export ZAxioms. +Require Export ZBase. -Module Type ZPlusSignature. -Declare Module Export ZBaseMod : ZBaseSig. -Open Local Scope IntScope. +Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod. +Open Local Scope NatIntScope. -Parameter Inline plus : Z -> Z -> Z. -Parameter Inline minus : Z -> Z -> Z. -Parameter Inline uminus : Z -> Z. +Theorem Zplus_0_l : forall n : Z, 0 + n == n. +Proof NZplus_0_l. -Notation "x + y" := (plus x y) : IntScope. -Notation "x - y" := (minus x y) : IntScope. -Notation "- x" := (uminus x) : IntScope. +Theorem Zplus_succ_l : forall n m : Z, (S n) + m == S (n + m). +Proof NZplus_succ_l. -Add Morphism plus with signature E ==> E ==> E as plus_wd. -Add Morphism minus with signature E ==> E ==> E as minus_wd. -Add Morphism uminus with signature E ==> E as uminus_wd. +Theorem Zminus_0_r : forall n : Z, n - 0 == n. +Proof NZminus_0_r. -Axiom plus_0 : forall n, 0 + n == n. -Axiom plus_succ : forall n m, (S n) + m == S (n + m). +Theorem Zminus_succ_r : forall n m : Z, n - (S m) == P (n - m). +Proof NZminus_succ_r. -Axiom minus_0 : forall n, n - 0 == n. -Axiom minus_succ : forall n m, n - (S m) == P (n - m). +Theorem Zopp_0 : - 0 == 0. +Proof Zopp_0. -Axiom uminus_0 : - 0 == 0. -Axiom uminus_succ : forall n, - (S n) == P (- n). +Theorem Zopp_succ : forall n : Z, - (S n) == P (- n). +Proof Zopp_succ. -End ZPlusSignature. +(** Theorems that are valid for both natural numbers and integers *) -Module ZPlusProperties (Import ZPlusModule : ZPlusSignature). -Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod. -Open Local Scope IntScope. +Theorem Zplus_0_r : forall n : Z, n + 0 == n. +Proof NZplus_0_r. -Theorem plus_pred : forall n m, P n + m == P (n + m). -Proof. -intros n m. rewrite_succ_pred n at 2. rewrite plus_succ. now rewrite pred_succ. -Qed. +Theorem Zplus_succ_r : forall n m : Z, n + S m == S (n + m). +Proof NZplus_succ_r. -Theorem minus_pred : forall n m, n - (P m) == S (n - m). -Proof. -intros n m. rewrite_succ_pred m at 2. rewrite minus_succ. now rewrite succ_pred. -Qed. +Theorem Zplus_comm : forall n m : Z, n + m == m + n. +Proof NZplus_comm. -Theorem uminus_pred : forall n, - (P n) == S (- n). -Proof. -intro n. rewrite_succ_pred n at 2. rewrite uminus_succ. now rewrite succ_pred. -Qed. +Theorem Zplus_assoc : forall n m p : Z, n + (m + p) == (n + m) + p. +Proof NZplus_assoc. + +Theorem Zplus_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZplus_shuffle1. -Theorem plus_n_0 : forall n, n + 0 == n. +Theorem Zplus_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZplus_shuffle2. + +Theorem Zplus_1_l : forall n : Z, 1 + n == S n. +Proof NZplus_1_l. + +Theorem Zplus_1_r : forall n : Z, n + 1 == S n. +Proof NZplus_1_r. + +Theorem Zplus_cancel_l : forall n m p : Z, p + n == p + m <-> n == m. +Proof NZplus_cancel_l. + +Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m. +Proof NZplus_cancel_r. + +(** Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m). Proof. -induct n. -now rewrite plus_0. -intros n IH. rewrite plus_succ. now rewrite IH. -intros n IH. rewrite plus_pred. now rewrite IH. +intros n m. +pattern n at 2. qsetoid_rewrite <- (Zsucc_pred n). +rewrite Zplus_succ_l. now rewrite Zpred_succ. Qed. -Theorem plus_n_succm : forall n m, n + S m == S (n + m). +Theorem Zplus_pred_r : forall n m : Z, n + P m == P (n + m). Proof. -intros n m; induct n. -now do 2 rewrite plus_0. -intros n IH. do 2 rewrite plus_succ. now rewrite IH. -intros n IH. do 2 rewrite plus_pred. rewrite IH. rewrite pred_succ; now rewrite succ_pred. +intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m); +apply Zplus_pred_l. Qed. -Theorem plus_n_predm : forall n m, n + P m == P (n + m). +Theorem Zplus_opp_minus : forall n m : Z, n + (- m) == n - m. Proof. -intros n m; rewrite_succ_pred m at 2. rewrite plus_n_succm; now rewrite pred_succ. +NZinduct m. +rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r. +intro m. rewrite Zopp_succ, Zminus_succ_r, Zplus_pred_r; now rewrite Zpred_inj_wd. Qed. -Theorem plus_opp_minus : forall n m, n + (- m) == n - m. +Theorem Zminus_0_l : forall n : Z, 0 - n == - n. Proof. -induct m. -rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0. -intros m IH. rewrite uminus_succ; rewrite minus_succ. rewrite plus_n_predm; now rewrite IH. -intros m IH. rewrite uminus_pred; rewrite minus_pred. rewrite plus_n_succm; now rewrite IH. +intro n; rewrite <- Zplus_opp_minus; now rewrite Zplus_0_l. Qed. -Theorem minus_0_n : forall n, 0 - n == - n. +Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m). Proof. -intro n; rewrite <- plus_opp_minus; now rewrite plus_0. +intros n m; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_succ_l. Qed. -Theorem minus_succn_m : forall n m, S n - m == S (n - m). +Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m). Proof. -intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_succ. +intros n m. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). +rewrite Zminus_succ_l; now rewrite Zpred_succ. Qed. -Theorem minus_predn_m : forall n m, P n - m == P (n - m). +Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m). Proof. -intros n m. rewrite_succ_pred n at 2; rewrite minus_succn_m; now rewrite pred_succ. +intros n m. pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m). +rewrite Zminus_succ_r; now rewrite Zsucc_pred. Qed. -Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p. +Theorem Zopp_pred : forall n : Z, - (P n) == S (- n). Proof. -intros n m p; induct n. -now do 2 rewrite plus_0. -intros n IH. do 3 rewrite plus_succ. now rewrite IH. -intros n IH. do 3 rewrite plus_pred. now rewrite IH. +intro n. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). +rewrite Zopp_succ. now rewrite Zsucc_pred. Qed. -Theorem plus_comm : forall n m, n + m == m + n. +Theorem Zminus_diag : forall n : Z, n - n == 0. Proof. -intros n m; induct n. -rewrite plus_0; now rewrite plus_n_0. -intros n IH; rewrite plus_succ; rewrite plus_n_succm; now rewrite IH. -intros n IH; rewrite plus_pred; rewrite plus_n_predm; now rewrite IH. +NZinduct n. +now rewrite Zminus_0_r. +intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ. Qed. -Theorem minus_diag : forall n, n - n == 0. +Theorem Zplus_opp_r : forall n : Z, n + (- n) == 0. Proof. -induct n. -now rewrite minus_0. -intros n IH. rewrite minus_succ; rewrite minus_succn_m; rewrite pred_succ; now rewrite IH. -intros n IH. rewrite minus_pred; rewrite minus_predn_m; rewrite succ_pred; now rewrite IH. +intro n; rewrite Zplus_opp_minus; now rewrite Zminus_diag. Qed. -Theorem plus_opp_r : forall n, n + (- n) == 0. +Theorem Zplus_opp_l : forall n : Z, - n + n == 0. Proof. -intro n; rewrite plus_opp_minus; now rewrite minus_diag. +intro n; rewrite Zplus_comm; apply Zplus_opp_r. Qed. -Theorem plus_opp_l : forall n, - n + n == 0. +Theorem Zminus_swap : forall n m : Z, - m + n == n - m. Proof. -intro n; rewrite plus_comm; apply plus_opp_r. +intros n m; rewrite <- Zplus_opp_minus; now rewrite Zplus_comm. Qed. -Theorem minus_swap : forall n m, - m + n == n - m. +Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. Proof. -intros n m; rewrite <- plus_opp_minus; now rewrite plus_comm. +intros n m p; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_assoc. Qed. -Theorem plus_minus_inverse : forall n m, n + (m - n) == m. +Theorem Zopp_involutive : forall n : Z, - (- n) == n. Proof. -intros n m; rewrite <- minus_swap. rewrite plus_assoc; -rewrite plus_opp_r; now rewrite plus_0. +NZinduct n. +now do 2 rewrite Zopp_0. +intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd. Qed. -Theorem plus_minus_distr : forall n m p, n + (m - p) == (n + m) - p. +Theorem Zopp_plus_distr : forall n m : Z, - (n + m) == - n + (- m). Proof. -intros n m p; do 2 rewrite <- plus_opp_minus; now rewrite plus_assoc. +intros n m; NZinduct n. +rewrite Zopp_0; now do 2 rewrite Zplus_0_l. +intro n. rewrite Zplus_succ_l; do 2 rewrite Zopp_succ; rewrite Zplus_pred_l. +now rewrite Zpred_inj_wd. Qed. -Theorem double_opp : forall n, - (- n) == n. +Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m. Proof. -induct n. -now do 2 rewrite uminus_0. -intros n IH. rewrite uminus_succ; rewrite uminus_pred; now rewrite IH. -intros n IH. rewrite uminus_pred; rewrite uminus_succ; now rewrite IH. +intros n m; rewrite <- Zplus_opp_minus, Zopp_plus_distr. +now rewrite Zopp_involutive. Qed. -Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m). +Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m. Proof. -intros n m; induct n. -rewrite uminus_0; now do 2 rewrite plus_0. -intros n IH. rewrite plus_succ; do 2 rewrite uminus_succ. rewrite IH. now rewrite plus_pred. -intros n IH. rewrite plus_pred; do 2 rewrite uminus_pred. rewrite IH. now rewrite plus_succ. +intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H. Qed. -Theorem opp_minus_distr : forall n m, - (n - m) == - n + m. +Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m. Proof. -intros n m; rewrite <- plus_opp_minus; rewrite opp_plus_distr. -now rewrite double_opp. +intros n m; split; [apply Zopp_inj | apply Zopp_wd]. Qed. -Theorem opp_inj : forall n m, - n == - m -> n == m. +Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p. Proof. -intros n m H. apply uminus_wd in H. now do 2 rewrite double_opp in H. +intros n m p; rewrite <- Zplus_opp_minus, Zopp_plus_distr, Zplus_assoc. +now do 2 rewrite Zplus_opp_minus. Qed. -Theorem minus_plus_distr : forall n m p, n - (m + p) == (n - m) - p. +Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p. Proof. -intros n m p; rewrite <- plus_opp_minus. rewrite opp_plus_distr. rewrite plus_assoc. -now do 2 rewrite plus_opp_minus. +intros n m p; rewrite <- Zplus_opp_minus, Zopp_minus_distr, Zplus_assoc. +now rewrite Zplus_opp_minus. Qed. -Theorem minus_minus_distr : forall n m p, n - (m - p) == (n - m) + p. +Theorem Zminus_opp : forall n m : Z, n - (- m) == n + m. Proof. -intros n m p; rewrite <- plus_opp_minus. rewrite opp_minus_distr. rewrite plus_assoc. -now rewrite plus_opp_minus. +intros n m; rewrite <- Zplus_opp_minus; now rewrite Zopp_involutive. Qed. -Theorem plus_minus_swap : forall n m p, n + m - p == n - p + m. +Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m. Proof. -intros n m p. rewrite <- plus_minus_distr. -rewrite <- (plus_opp_minus n p). rewrite <- plus_assoc. now rewrite minus_swap. +intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_minus n p), <- Zplus_assoc. +now rewrite Zminus_swap. Qed. -Theorem plus_cancel_l : forall n m p, n + m == n + p -> m == p. +Theorem Zminus_plus_diag : forall n m : Z, n - m + m == n. Proof. -intros n m p H. -assert (H1 : - n + n + m == -n + n + p). -do 2 rewrite <- plus_assoc; now rewrite H. -rewrite plus_opp_l in H1; now do 2 rewrite plus_0 in H1. +intros; rewrite <- Zplus_minus_swap; rewrite <- Zplus_minus_assoc; +rewrite Zminus_diag; now rewrite Zplus_0_r. Qed. -Theorem plus_cancel_r : forall n m p, n + m == p + m -> n == p. +Theorem Zplus_minus_diag : forall n m : Z, n + m - m == n. Proof. -intros n m p H. -rewrite plus_comm in H. set (k := m + n) in H. rewrite plus_comm in H. -unfold k in H; clear k. now apply plus_cancel_l with m. +intros; rewrite <- Zplus_minus_assoc; rewrite Zminus_diag; now rewrite Zplus_0_r. Qed. -Theorem plus_minus_l : forall n m p, m + p == n -> p == n - m. +Theorem Zplus_minus_eq_l : forall n m p : Z, m + p == n <-> n - m == p. Proof. -intros n m p H. -assert (H1 : - m + m + p == - m + n). -rewrite <- plus_assoc; now rewrite H. -rewrite plus_opp_l in H1. rewrite plus_0 in H1. now rewrite minus_swap in H1. +intros n m p. +stepl (-m + (m + p) == -m + n) by apply Zplus_cancel_l. +stepr (p == n - m) by now split. +rewrite Zplus_assoc, Zplus_opp_l, Zplus_0_l. now rewrite Zminus_swap. Qed. -Theorem plus_minus_r : forall n m p, m + p == n -> m == n - p. +Theorem Zplus_minus_eq_r : forall n m p : Z, m + p == n <-> n - p == m. Proof. -intros n m p H; rewrite plus_comm in H; now apply plus_minus_l in H. +intros n m p; rewrite Zplus_comm; now apply Zplus_minus_eq_l. Qed. -Lemma minus_eq : forall n m, n - m == 0 -> n == m. +Theorem Zminus_eq : forall n m : Z, n - m == 0 <-> n == m. Proof. -intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0. +intros n m. rewrite <- Zplus_minus_eq_l, Zplus_0_r; now split. Qed. -End ZPlusProperties. - +End ZPlusPropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index 95f0fa8c6..bab1bb4a0 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -1,167 +1,365 @@ Require Export ZOrder. -Require Export ZPlus. -Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature) - (Import ZOrderModule : ZOrderSignature with - Module ZBaseMod := ZPlusModule.ZBaseMod). -Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. -Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule. -(* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *) -Open Local Scope IntScope. +Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod. +Open Local Scope NatIntScope. -Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m. +(** Theorems that are true on both natural numbers and integers *) + +Theorem Zplus_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m. +Proof NZplus_lt_mono_l. + +Theorem Zplus_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p. +Proof NZplus_lt_mono_r. + +Theorem Zplus_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q. +Proof NZplus_lt_mono. + +Theorem Zplus_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m. +Proof NZplus_le_mono_l. + +Theorem Zplus_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p. +Proof NZplus_le_mono_r. + +Theorem Zplus_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q. +Proof NZplus_le_mono. + +Theorem Zplus_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q. +Proof NZplus_lt_le_mono. + +Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q. +Proof NZplus_le_lt_mono. + +Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_plus_lt. + +Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_plus_lt. + +Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_lt. + +Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q. +Proof NZplus_lt_cases. + +Theorem Zplus_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q. +Proof NZplus_le_cases. + +Theorem Zplus_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0. +Proof NZplus_neg_cases. + +Theorem Zplus_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZplus_pos_cases. + +Theorem Zplus_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof NZplus_nonpos_cases. + +Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof NZplus_nonneg_cases. + +(** Multiplication and order *) + +Theorem Ztimes_lt_pred : + forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). +Proof NZtimes_lt_pred. + +Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). +Proof NZtimes_lt_mono_pos_l. + +Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). +Proof NZtimes_lt_mono_pos_r. + +Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). +Proof NZtimes_lt_mono_neg_l. + +Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). +Proof NZtimes_lt_mono_neg_r. + +Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. +Proof NZtimes_le_mono_nonneg_l. + +Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. +Proof NZtimes_le_mono_nonpos_l. + +Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. +Proof NZtimes_le_mono_nonneg_r. + +Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. +Proof NZtimes_le_mono_nonpos_r. + +Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZtimes_cancel_l. + +Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZtimes_le_mono_pos_l. + +Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZtimes_le_mono_pos_r. + +Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). +Proof NZtimes_le_mono_neg_l. + +Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). +Proof NZtimes_le_mono_neg_r. + +Theorem Ztimes_lt_mono : + forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof NZtimes_lt_mono. + +Theorem Ztimes_le_mono : + forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof NZtimes_le_mono. + +Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. +Proof NZtimes_pos_pos. + +Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. +Proof NZtimes_nonneg_nonneg. + +Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. +Proof NZtimes_neg_neg. + +Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. +Proof NZtimes_nonpos_nonpos. + +Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. +Proof NZtimes_pos_neg. + +Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. +Proof NZtimes_nonneg_nonpos. + +Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. +Proof NZtimes_neg_pos. + +Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. +Proof NZtimes_nonpos_nonneg. + +Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0. +Proof NZtimes_eq_0. + +Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZtimes_neq_0. + +(** Theorems that are either not valid on N or have different proofs on N and Z *) + +(** Minus and order *) + +Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n. +Proof. +intros n m. stepr (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r. +rewrite Zplus_0_l; now rewrite Zminus_plus_diag. +Qed. + +Theorem Zle_le_minus : forall n m : Z, n <= m <-> 0 <= m - n. +Proof. +intros n m; stepr (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r. +rewrite Zplus_0_l; now rewrite Zminus_plus_diag. +Qed. + +Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n. +Proof. +intros n m. stepr (m + - m < m + - n) by symmetry; apply Zplus_lt_mono_l. +do 2 rewrite Zplus_opp_minus. rewrite Zminus_diag. apply Zlt_lt_minus. +Qed. + +Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n. +Proof. +intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zplus_le_mono_l. +do 2 rewrite Zplus_opp_minus. rewrite Zminus_diag. apply Zle_le_minus. +Qed. + +Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0. +Proof. +intro n; rewrite (Zopp_lt_mono n 0); now rewrite Zopp_0. +Qed. + +Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n. +Proof. +intro n. rewrite (Zopp_lt_mono 0 n). now rewrite Zopp_0. +Qed. + +Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0. +Proof. +intro n; rewrite (Zopp_le_mono n 0); now rewrite Zopp_0. +Qed. + +Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n. +Proof. +intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0. +Qed. + +Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n. +Proof. +intros n m p. do 2 rewrite <- Zplus_opp_minus. rewrite <- Zplus_lt_mono_l. +apply Zopp_lt_mono. +Qed. + +Theorem Zminus_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p. +Proof. +intros n m p; do 2 rewrite <- Zplus_opp_minus; apply Zplus_lt_mono_r. +Qed. + +Theorem Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZlt_trans with (m - p); +[now apply -> Zminus_lt_mono_r | now apply -> Zminus_lt_mono_l]. +Qed. + +Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n. +Proof. +intros n m p; do 2 rewrite <- Zplus_opp_minus; rewrite <- Zplus_le_mono_l; +apply Zopp_le_mono. +Qed. + +Theorem Zminus_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p. +Proof. +intros n m p; do 2 rewrite <- Zplus_opp_minus; apply Zplus_le_mono_r. +Qed. + +Theorem Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q. +Proof. +intros n m p q H1 H2. +apply NZle_trans with (m - p); +[now apply -> Zminus_le_mono_r | now apply -> Zminus_le_mono_l]. +Qed. + +Theorem Zminus_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZlt_le_trans with (m - p); +[now apply -> Zminus_lt_mono_r | now apply -> Zminus_le_mono_l]. +Qed. + +Theorem Zminus_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q. Proof. -intros n m p; induct p. -now do 2 rewrite plus_0. -intros p IH. do 2 rewrite plus_succ. now rewrite <- lt_respects_succ. -intros p IH. do 2 rewrite plus_pred. now rewrite <- lt_respects_pred. +intros n m p q H1 H2. +apply NZle_lt_trans with (m - p); +[now apply -> Zminus_le_mono_r | now apply -> Zminus_lt_mono_l]. Qed. -Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p. +Theorem Zle_lt_minus_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q. Proof. -intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p); -apply plus_lt_compat_l. +intros n m p q H1 H2. apply (Zle_lt_plus_lt (- m) (- n)); +[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus]. Qed. -Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m. +Theorem Zlt_le_minus_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q. Proof. -intros n m p; do 2 rewrite <- lt_succ. rewrite <- plus_n_succm; -apply plus_lt_compat_l. +intros n m p q H1 H2. apply (Zlt_le_plus_lt (- m) (- n)); +[now apply -> Zopp_lt_mono | now do 2 rewrite Zplus_opp_minus]. Qed. -Theorem plus_le_compat_r : forall n m p, n <= m <-> n + p <= m + p. +Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q. Proof. -intros n m p; rewrite (plus_comm n p); rewrite (plus_comm m p); -apply plus_le_compat_l. +intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n)); +[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus]. Qed. -Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. +Theorem Zlt_plus_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p. Proof. -intros n m p q H1 H2. apply lt_trans with (m := m + p). -now apply -> plus_lt_compat_r. now apply -> plus_lt_compat_l. +intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zminus_lt_mono_r. +now rewrite Zplus_minus_diag. Qed. -Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. +Theorem Zle_plus_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p. Proof. -intros n m p q H1 H2. Zle_elim H2. now apply plus_lt_compat. -rewrite H2. now apply -> plus_lt_compat_r. +intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zminus_le_mono_r. +now rewrite Zplus_minus_diag. Qed. -Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. +Theorem Zlt_plus_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n. Proof. -intros n m p q H1 H2. Zle_elim H1. now apply plus_lt_compat. -rewrite H1. now apply -> plus_lt_compat_l. +intros n m p. rewrite Zplus_comm; apply Zlt_plus_lt_minus_r. Qed. -Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. +Theorem Zle_plus_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n. Proof. -intros n m p q H1 H2. Zle_elim H1. Zle_intro1; now apply plus_lt_le_compat. -rewrite H1. now apply -> plus_le_compat_l. +intros n m p. rewrite Zplus_comm; apply Zle_plus_le_minus_r. Qed. -Theorem plus_pos : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m. +Theorem Zlt_minus_lt_plus_r : forall n m p : Z, n - p < m <-> n < m + p. Proof. -intros; rewrite <- (plus_0 0); now apply plus_le_compat. +intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zplus_lt_mono_r. +now rewrite Zminus_plus_diag. Qed. -Lemma lt_opp_forward : forall n m, n < m -> - m < - n. +Theorem Zle_minus_le_plus_r : forall n m p : Z, n - p <= m <-> n <= m + p. Proof. -induct n. -induct_ord m. -intro H; false_hyp H lt_irr. -intros m H1 IH H2. rewrite uminus_succ. rewrite uminus_0 in *. -Zle_elim H1. apply IH in H1. now apply lt_predn_m. -rewrite <- H1; rewrite uminus_0; apply lt_predn_n. -intros m H1 IH H2. apply lt_n_predm in H2. apply -> le_gt in H1. false_hyp H2 H1. -intros n IH m H. rewrite uminus_succ. -apply -> lt_succ_pred in H. apply IH in H. rewrite uminus_pred in H. now apply -> lt_succ_pred. -intros n IH m H. rewrite uminus_pred. -apply -> lt_pred_succ in H. apply IH in H. rewrite uminus_succ in H. now apply -> lt_pred_succ. +intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zplus_le_mono_r. +now rewrite Zminus_plus_diag. Qed. -Theorem lt_opp : forall n m, n < m <-> - m < - n. +Theorem Zlt_minus_lt_plus_l : forall n m p : Z, n - m < p <-> n < m + p. Proof. -intros n m; split. -apply lt_opp_forward. -intro; rewrite <- (double_opp n); rewrite <- (double_opp m); -now apply lt_opp_forward. +intros n m p. rewrite Zplus_comm; apply Zlt_minus_lt_plus_r. Qed. -Theorem le_opp : forall n m, n <= m <-> - m <= - n. +Theorem Zle_minus_le_plus_l : forall n m p : Z, n - m <= p <-> n <= m + p. Proof. -intros n m; do 2 rewrite -> le_lt; rewrite <- lt_opp. -assert (n == m <-> - m == - n). -split; intro; [now apply uminus_wd | now apply opp_inj]. -tauto. +intros n m p. rewrite Zplus_comm; apply Zle_minus_le_plus_r. Qed. -Theorem lt_opp_neg : forall n, n < 0 <-> 0 < - n. +Theorem Zlt_minus_lt_plus : forall n m p q : Z, n - m < p - q <-> n + q < m + p. Proof. -intro n. set (k := 0) in |-* at 2. -setoid_replace k with (- k); unfold k; clear k. -apply lt_opp. now rewrite uminus_0. +intros n m p q. rewrite Zlt_minus_lt_plus_l. rewrite Zplus_minus_assoc. +now rewrite <- Zlt_plus_lt_minus_r. Qed. -Theorem le_opp_neg : forall n, n <= 0 <-> 0 <= - n. +Theorem Zle_minus_le_plus : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p. Proof. -intro n. set (k := 0) in |-* at 2. -setoid_replace k with (- k); unfold k; clear k. -apply le_opp. now rewrite uminus_0. +intros n m p q. rewrite Zle_minus_le_plus_l. rewrite Zplus_minus_assoc. +now rewrite <- Zle_plus_le_minus_r. Qed. -Theorem lt_opp_pos : forall n, 0 < n <-> - n < 0. +Theorem Zlt_minus_pos : forall n m : Z, 0 < m <-> n - m < n. Proof. -intro n. set (k := 0) in |-* at 2. -setoid_replace k with (- k); unfold k; clear k. -apply lt_opp. now rewrite uminus_0. +intros n m. stepr (n - m < n - 0) by now rewrite Zminus_0_r. apply Zminus_lt_mono_l. Qed. -Theorem le_opp_pos : forall n, 0 <= n <-> - n <= 0. +Theorem Zle_minus_nonneg : forall n m : Z, 0 <= m <-> n - m <= n. Proof. -intro n. set (k := 0) in |-* at 2. -setoid_replace k with (- k); unfold k; clear k. -apply le_opp. now rewrite uminus_0. +intros n m. stepr (n - m <= n - 0) by now rewrite Zminus_0_r. apply Zminus_le_mono_l. Qed. -Theorem minus_lt_decr_r : forall n m p, n < m <-> p - m < p - n. +Theorem Zminus_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p. Proof. -intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_lt_compat_l. -apply lt_opp. +intros n m p q H. rewrite Zlt_minus_lt_plus in H. now apply Zplus_lt_cases. Qed. -Theorem minus_le_nonincr_r : forall n m p, n <= m <-> p - m <= p - n. +Theorem Zminus_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p. Proof. -intros n m p. do 2 rewrite <- plus_opp_minus. rewrite <- plus_le_compat_l. -apply le_opp. +intros n m p q H. rewrite Zle_minus_le_plus in H. now apply Zplus_le_cases. Qed. -Theorem minus_lt_incr_l : forall n m p, n < m <-> n - p < m - p. +Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m. Proof. -intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_lt_compat_r. +intros n m H; rewrite <- Zplus_opp_minus in H. +setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos). +now apply Zplus_neg_cases. Qed. -Theorem minus_le_nondecr_l : forall n m p, n <= m <-> n - p <= m - p. +Theorem Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0. Proof. -intros n m p. do 2 rewrite <- plus_opp_minus. now rewrite <- plus_le_compat_r. +intros n m H; rewrite <- Zplus_opp_minus in H. +setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg). +now apply Zplus_pos_cases. Qed. -Theorem lt_plus_swap : forall n m p, n + p < m <-> n < m - p. +Theorem Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m. Proof. -intros n m p. rewrite (minus_lt_incr_l (n + p) m p). -rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. +intros n m H; rewrite <- Zplus_opp_minus in H. +setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg). +now apply Zplus_nonpos_cases. Qed. -Theorem le_plus_swap : forall n m p, n + p <= m <-> n <= m - p. +Theorem Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0. Proof. -intros n m p. rewrite (minus_le_nondecr_l (n + p) m p). -rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. +intros n m H; rewrite <- Zplus_opp_minus in H. +setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos). +now apply Zplus_nonneg_cases. Qed. -End ZPlusOrderProperties. +End ZPlusOrderPropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v index ffcb2dea8..4814ab086 100644 --- a/theories/Numbers/Integer/Abstract/ZPred.v +++ b/theories/Numbers/Integer/Abstract/ZPred.v @@ -52,9 +52,3 @@ rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x)) than in the goal. For the reason of many possible variants, the core of the tactic is factored out. *) - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v index 38311aa2b..bc7321cba 100644 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ b/theories/Numbers/Integer/Abstract/ZTimes.v @@ -1,127 +1,108 @@ +Require Export Ring. Require Export ZPlus. -Module Type ZTimesSignature. -Declare Module Export ZPlusModule : ZPlusSignature. -Open Local Scope IntScope. +Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod. +Open Local Scope NatIntScope. -Parameter Inline times : Z -> Z -> Z. +Theorem Ztimes_0_r : forall n : Z, n * 0 == 0. +Proof NZtimes_0_r. -Notation "x * y" := (times x y) : IntScope. +Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n. +Proof NZtimes_succ_r. -Add Morphism times with signature E ==> E ==> E as times_wd. +(** Theorems that are valid for both natural numbers and integers *) -Axiom times_0 : forall n, n * 0 == 0. -Axiom times_succ : forall n m, n * (S m) == n * m + n. +Theorem Ztimes_0_l : forall n : Z, 0 * n == 0. +Proof NZtimes_0_l. -End ZTimesSignature. +Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m. +Proof NZtimes_succ_l. -Module ZTimesProperties (Import ZTimesModule : ZTimesSignature). -Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. -Open Local Scope IntScope. +Theorem Ztimes_comm : forall n m : Z, n * m == m * n. +Proof NZtimes_comm. -Theorem times_pred : forall n m, n * (P m) == n * m - n. -Proof. -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. +Theorem Ztimes_plus_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p. +Proof NZtimes_plus_distr_r. -Theorem times_0_n : forall n, 0 * n == 0. -Proof. -induct n. -now rewrite times_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 Ztimes_plus_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p. +Proof NZtimes_plus_distr_l. -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_succ. rewrite IH. -do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity. -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_succ. now rewrite minus_predn_m. -Qed. +Theorem Ztimes_assoc : forall n m p : Z, n * (m * p) == (n * m) * p. +Proof NZtimes_assoc. -Theorem times_predn_m : forall n m, (P n) * m == n * m - m. -Proof. -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. +Theorem Ztimes_1_l : forall n : Z, 1 * n == n. +Proof NZtimes_1_l. -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_succn_m; rewrite times_succ; now rewrite IH. -intros n IH. rewrite times_predn_m; rewrite times_pred; now rewrite IH. -Qed. +Theorem Ztimes_1_r : forall n : Z, n * 1 == n. +Proof NZtimes_1_r. + +(* The following two theorems are true in an ordered ring, +but since they don't mention order, we'll put them here *) + +Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0. +Proof NZtimes_eq_0. -Theorem times_opp_r : forall n m, n * (- m) == - (n * m). +Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZtimes_neq_0. + +(** Z forms a ring *) + +Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZE. Proof. -intros n m; induct m. -rewrite uminus_0; rewrite times_0; now rewrite uminus_0. -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_pred. rewrite times_pred; rewrite times_succ. rewrite IH. -now rewrite opp_minus_distr. +constructor. +exact Zplus_0_l. +exact Zplus_comm. +exact Zplus_assoc. +exact Ztimes_1_l. +exact Ztimes_comm. +exact Ztimes_assoc. +exact Ztimes_plus_distr_r. +intros; now rewrite Zplus_opp_minus. +exact Zplus_opp_r. Qed. -Theorem times_opp_l : forall n m, (- n) * m == - (n * m). +Add Ring ZR : Zring. + +(** Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n. Proof. -intros n m; rewrite (times_comm (- n) m); rewrite (times_comm n m); -now rewrite times_opp_r. +intros n m. +pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m). +now rewrite Ztimes_succ_r, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r. Qed. -Theorem times_opp_opp : forall n m, (- n) * (- m) == n * m. +Theorem Ztimes_pred_l : forall n m : Z, (P n) * m == n * m - m. Proof. -intros n m. rewrite times_opp_l. rewrite times_opp_r. now rewrite double_opp. +intros n m; rewrite (Ztimes_comm (P n) m), (Ztimes_comm n m). apply Ztimes_pred_r. Qed. -Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p. +Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m). Proof. -intros n m p; induct m. -rewrite times_0; now do 2 rewrite plus_0. -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_pred. do 2 rewrite times_pred. rewrite IH. -apply plus_minus_swap. +intros; ring. Qed. -Theorem times_plus_distr_l : forall n m p, (n + m) * p == n * p + m * p. +Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m). Proof. -intros n m p; rewrite (times_comm (n + m) p); rewrite times_plus_distr_r; -rewrite (times_comm p n); now rewrite (times_comm p m). +intros; ring. Qed. -Theorem times_minus_distr_r : forall n m p, n * (m - p) == n * m - n * p. +Theorem Ztimes_opp_opp : forall n m : Z, (- n) * (- m) == n * m. Proof. -intros n m p. -do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_r. now rewrite times_opp_r. +intros; ring. Qed. -Theorem times_minus_distr_l : forall n m p, (n - m) * p == n * p - m * p. +Theorem Ztimes_minus_distr_r : forall n m p : Z, n * (m - p) == n * m - n * p. Proof. -intros n m p. -do 2 rewrite <- plus_opp_minus. rewrite times_plus_distr_l. now rewrite times_opp_l. +intros; ring. Qed. -Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p. +Theorem Ztimes_minus_distr_l : forall n m p : Z, (n - m) * p == n * p - m * p. Proof. -intros n m p; induct p. -now do 3 rewrite times_0. -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. +intros; ring. Qed. -End ZTimesProperties. +End ZTimesPropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index 055342bcc..d63dc0d8c 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -1,96 +1,102 @@ -Require Export ZTimes. Require Export ZPlusOrder. -Module ZTimesOrderProperties (Import ZTimesModule : ZTimesSignature) - (Import ZOrderModule : ZOrderSignature with - Module ZBaseMod := ZTimesModule.ZPlusModule.ZBaseMod). -Module Export ZTimesPropertiesModule := ZTimesProperties ZTimesModule. -Module Export ZPlusOrderPropertiesModule := - ZPlusOrderProperties ZTimesModule.ZPlusModule ZOrderModule. -Open Local Scope IntScope. - -Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p. -Proof. -intros n m p; induct_ord p. -intros H _; false_hyp H lt_irr. -intros p H IH H1 H2. do 2 rewrite times_succ. -apply -> lt_succ in H1; Zle_elim H1. -apply plus_lt_compat. now apply IH. assumption. -rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0. -intros p H IH H1 H2. apply lt_n_predm in H1. apply -> le_gt in H. -false_hyp H1 H. -Qed. - -Theorem mult_lt_compat_l : forall n m p, 0 < p -> n < m -> p * n < p * m. -Proof. -intros n m p. rewrite (times_comm p n); rewrite (times_comm p m). -apply mult_lt_compat_r. -Qed. - -Theorem mult_lt_le_compat_r : forall n m p, 0 < p -> n <= m -> n * p <= m * p. -Proof. -intros n m p H1 H2; Zle_elim H2. -Zle_intro1; now apply mult_lt_compat_r. -rewrite H2. now Zle_intro2. -Qed. - -Theorem mult_lt_le_compat_l : forall n m p, 0 < p -> n <= m -> p * n <= p * m. -Proof. -intros n m p. rewrite (times_comm p n); rewrite (times_comm p m). -apply mult_lt_le_compat_r. -Qed. - -(* And so on *) - -Theorem mult_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. -Proof. -intros n m; set (k := 0) in |-* at 3; -setoid_replace k with (n * 0); unfold k; clear k. -apply mult_lt_compat_l. now rewrite times_0. -Qed. - -Theorem mult_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0. -Proof. -intros n m; set (k := 0) in |-* at 3; -setoid_replace k with (n * 0); unfold k; clear k. -apply mult_lt_compat_l. now rewrite times_0. -Qed. -(* The same proof script as for mult_pos_pos! *) - -Theorem mult_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0. -Proof. -intros n m H1 H2; rewrite times_comm; now apply mult_pos_neg. -Qed. - -Theorem mult_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m. -Proof. -intros n m H1 H2. setoid_replace (n * m) with (- - (n * m)); -[| symmetry; apply double_opp]. -rewrite <- times_opp_l. rewrite <- times_opp_r. -apply -> lt_opp_neg in H1. apply -> lt_opp_neg in H2. -now apply mult_pos_pos. -Qed. - -(** With order, Z is an integral domain *) -Theorem mult_neq_0 : forall n m, n # 0 -> m # 0 -> n * m # 0. -Proof. -intros n m H1 H2. -destruct (lt_total n 0) as [H3 | [H3 | H3]]; -destruct (lt_total m 0) as [H4 | [H4 | H4]]. -apply neq_symm. apply lt_neq. now apply mult_neg_neg. -false_hyp H4 H2. -apply lt_neq; now apply mult_neg_pos. -false_hyp H3 H1. false_hyp H3 H1. false_hyp H3 H1. -apply lt_neq; now apply mult_pos_neg. -false_hyp H4 H2. -apply neq_symm. apply lt_neq. now apply mult_pos_pos. -Qed. - -End ZTimesOrderProperties. - - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) +Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod. +Open Local Scope NatIntScope. + +(** Theorems that are true on both natural numbers and integers *) + +Theorem Ztimes_lt_pred : + forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). +Proof NZtimes_lt_pred. + +Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). +Proof NZtimes_lt_mono_pos_l. + +Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). +Proof NZtimes_lt_mono_pos_r. + +Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). +Proof NZtimes_lt_mono_neg_l. + +Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). +Proof NZtimes_lt_mono_neg_r. + +Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. +Proof NZtimes_le_mono_nonneg_l. + +Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. +Proof NZtimes_le_mono_nonpos_l. + +Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. +Proof NZtimes_le_mono_nonneg_r. + +Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. +Proof NZtimes_le_mono_nonpos_r. + +Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZtimes_cancel_l. + +Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZtimes_le_mono_pos_l. + +Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZtimes_le_mono_pos_r. + +Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). +Proof NZtimes_le_mono_neg_l. + +Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). +Proof NZtimes_le_mono_neg_r. + +Theorem Ztimes_lt_mono : + forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof NZtimes_lt_mono. + +Theorem Ztimes_le_mono : + forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof NZtimes_le_mono. + +Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. +Proof NZtimes_pos_pos. + +Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. +Proof NZtimes_nonneg_nonneg. + +Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. +Proof NZtimes_neg_neg. + +Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. +Proof NZtimes_nonpos_nonpos. + +Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. +Proof NZtimes_pos_neg. + +Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. +Proof NZtimes_nonneg_nonpos. + +Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. +Proof NZtimes_neg_pos. + +Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. +Proof NZtimes_nonpos_nonneg. + +Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0. +Proof NZtimes_eq_0. + +Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZtimes_neq_0. + +Theorem Ztimes_pos : forall n m : Z, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). +Proof NZtimes_pos. + +Theorem Ztimes_neg : + forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). +Proof NZtimes_neg. + +(** Theorems that are either not valid on N or have different proofs on N and Z *) + +(* None? *) + +End ZTimesOrderPropFunct. + diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v index f5c19c611..a1e52a202 100644 --- a/theories/Numbers/Integer/BigInts/EZBase.v +++ b/theories/Numbers/Integer/BigInts/EZBase.v @@ -159,9 +159,3 @@ Qed. End Induction. End EZBaseMod. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v index ca3286211..b31dcdf9d 100644 --- a/theories/Numbers/Integer/BigInts/Zeqmod.v +++ b/theories/Numbers/Integer/BigInts/Zeqmod.v @@ -40,9 +40,3 @@ Theorem Zplus_eqmod_compat_r : intros p n m k; rewrite (Zplus_comm n k); rewrite (Zplus_comm m k); apply Zplus_eqmod_compat_l. Qed. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 217d08850..0fd1be7a9 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -197,8 +197,3 @@ End ZBinOrder. Module Export ZTimesOrderPropertiesModule := ZTimesOrderProperties ZBinTimes ZBinOrder. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v index 73b0bee7e..2a9b4f386 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v @@ -140,9 +140,3 @@ End Induction. End NatPairsInt. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v index 8943afde9..dc258f873 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v @@ -110,9 +110,3 @@ End NatPairsPlusOrderProperties.*) NatPairsOrderModule.ZBaseMod are the same *) - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v index d1ae7679b..2e658c181 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v @@ -81,9 +81,3 @@ Module Export NatPairsPlusModule := NatPairsPlus NPlusMod. Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule. End NatPairsPlusProperties. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v index 47bf8cd08..553c6df22 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v @@ -54,9 +54,3 @@ Module Export NatPairsTimesModule := NatPairsTimes NTimesMod. Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule. End NatPairsTimesProperties. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) |