diff options
Diffstat (limited to 'theories')
47 files changed, 1039 insertions, 1381 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 0a275c850..96083891b 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -286,24 +286,6 @@ Qed. (** Properties of subtraction. *) -(*Lemma Nle_Nminus_N0 : forall n n' : N, n <= n' -> n - n' = N0. -Proof. - destruct n; destruct n'; simpl; intros; auto. - elim H; auto. - red in H; simpl in *. - intros; destruct (Pcompare p p0 Eq); auto. - elim H; auto. -Qed. -Proof. -destruct n as [| p]; destruct n' as [| q]; simpl; intros; auto. -now elim H. -red in H; simpl in *. -case_eq (Pcompare p q Eq); intro H1. -assert (H2 : p = q); [now apply Pcompare_Eq_eq |]. now rewrite H2, Pminus_mask_diag. -now rewrite Pminus_mask_Lt. -false_hyp H1 H. -Qed.*) - Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'. Proof. destruct n as [| p]; destruct n' as [| q]; unfold Nle; simpl; @@ -406,6 +388,11 @@ destruct n; destruct m; simpl; auto. exact (Pcompare_antisym p p0 Eq). Qed. +Theorem Nlt_irrefl : forall n : N, ~ n < n. +Proof. +intro n; unfold Nlt; now rewrite Ncompare_refl. +Qed. + Theorem Ncompare_n_Sm : forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m. Proof. 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: -*) diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 0a89132ea..1509b5f7d 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -72,9 +72,3 @@ Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m. End NZOrdAxiomsSig. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index fbccf049c..121f78813 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -74,9 +74,3 @@ Tactic Notation "NZinduct" ident(n) constr(u) := End NZBasePropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) - diff --git a/theories/Numbers/NatInt/NZOrdRing.v b/theories/Numbers/NatInt/NZOrdRing.v deleted file mode 100644 index f35e030e1..000000000 --- a/theories/Numbers/NatInt/NZOrdRing.v +++ /dev/null @@ -1,26 +0,0 @@ -Require Export NZAxioms. -Require Import NZTimes. - -Module Type NZOrdAxiomsSig. -Declare Module Export NZAxiomsMod : NZAxiomsSig. -Open Local Scope NatIntScope. - -Parameter Inline NZlt : NZ -> NZ -> Prop. -Parameter Inline NZle : NZ -> NZ -> Prop. - -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. - -Notation "x < y" := (NZlt x y) : NatIntScope. -Notation "x <= y" := (NZle x y) : NatIntScope. - -Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. -Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). -Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m. -End NZOrdAxiomsSig. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZOrder.g b/theories/Numbers/NatInt/NZOrder.g deleted file mode 100644 index fd7cf608a..000000000 --- a/theories/Numbers/NatInt/NZOrder.g +++ /dev/null @@ -1,219 +0,0 @@ -Require Export NZBase. - -Module Type NZOrderSig. -Declare Module Export NZBaseMod : NZBaseSig. -Open Local Scope NatIntScope. - -Parameter Inline NZlt : NZ -> NZ -> Prop. -Parameter Inline NZle : NZ -> NZ -> Prop. - -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. - -Notation "x < y" := (NZlt x y) : NatIntScope. -Notation "x <= y" := (NZle x y) : NatIntScope. - -Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. -Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). -Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m. -End NZOrderSig. - -Module NZOrderPropFunct (Import NZOrderMod : NZOrderSig). -Module Export NZBasePropMod := NZBasePropFunct NZBaseMod. -Open Local Scope NatIntScope. - -Ltac NZle_intro1 := rewrite NZle_lt_or_eq; left. -Ltac NZle_intro2 := rewrite NZle_lt_or_eq; right. -Ltac NZle_elim H := rewrite NZle_lt_or_eq in H; destruct H as [H | H]. - -Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y. - -Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z. - -Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y. - -Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z. - -Declare Left Step NZlt_stepl. -Declare Right Step NZlt_stepr. -Declare Left Step NZle_stepl. -Declare Right Step NZle_stepr. - -Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m. - -Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m. - -Theorem NZle_refl : forall n : NZ, n <= n. - -Theorem NZlt_succ_r : forall n : NZ, n < S n. - -Theorem NZle_succ_r : forall n : NZ, n <= S n. - -Theorem NZlt_lt_succ : forall n m : NZ, n < m -> n < S m. - -Theorem NZle_le_succ : forall n m : NZ, n <= m -> n <= S m. - -Theorem NZle_succ_le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. - -(* The following theorem is a special case of neq_succ_iter_l below, -but we prove it independently *) - -Theorem neq_succ_l : forall n : NZ, S n ~= n. - -Theorem nlt_succ_l : forall n : NZ, ~ S n < n. - -Theorem nle_succ_l : forall n : NZ, ~ S n <= n. - -Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m. - -Theorem NZlt_succ_lt : forall n m : NZ, S n < m -> n < m. - -Theorem NZle_succ_le : forall n m : NZ, S n <= m -> n <= m. - -Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m. - -Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m. - -Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False. - -Theorem NZlt_asymm : forall n m, n < m -> ~ m < n. - -Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p. - -Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p. - -Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p. - -Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p. - -Theorem NZle_antisymm : forall n m : NZ, n <= m -> m <= n -> n == m. - -(** Trichotomy, decidability, and double negation elimination *) - -Theorem NZlt_trichotomy : forall n m : NZ, n < m \/ n == m \/ m < n. - -Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n. - -Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n. - -Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m. - -Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m. - -Theorem nle_lt : forall n m : NZ, ~ n <= m <-> m < n. - -Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m. - -Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m. - -Theorem NZlt_nlt_succ : forall n m : NZ, n < m <-> ~ m < S n. - -(* The difference between integers and natural numbers is that for -every integer there is a predecessor, which is not true for natural -numbers. However, for both classes, every number that is bigger than -some other number has a predecessor. The proof of this fact by regular -induction does not go through, so we need to use strong -(course-of-value) induction. *) - -Lemma NZlt_exists_pred_strong : - forall z n m : NZ, z < m -> m <= n -> exists k : NZ, m == S k /\ z <= k. - -Theorem NZlt_exists_pred : - forall z n : NZ, z < n -> exists k : NZ, n == S k /\ z <= k. - -(** A corollary of having an order is that NZ is infinite *) - -(* This section about infinity of NZ relies on the type nat and can be -safely removed *) - -Definition NZsucc_iter (n : nat) (m : NZ) := - nat_rec (fun _ => NZ) m (fun _ l => S l) n. - -Theorem NZlt_succ_iter_r : - forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m. - -Theorem neq_succ_iter_l : - forall (n : nat) (m : NZ), NZsucc_iter (Datatypes.S n) m ~= m. - -(* End of the section about the infinity of NZ *) - -(** Stronger variant of induction with assumptions n >= 0 (n < 0) -in the induction step *) - -Section Induction. - -Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZE A. - -Add Morphism A with signature NZE ==> iff as A_morph. -Proof A_wd. - -Section Center. - -Variable z : NZ. (* A z is the basis of induction *) - -Section RightInduction. - -Let A' (n : NZ) := forall m : NZ, z <= m -> m < n -> A m. - -Add Morphism A' with signature NZE ==> iff as A'_pos_wd. -Proof. -unfold A'; solve_predicate_wd. -Qed. - -Theorem right_induction : - A z -> (forall n : NZ, z <= n -> A n -> A (S n)) -> forall n : NZ, z <= n -> A n. - -End RightInduction. - -Section LeftInduction. - -Let A' (n : NZ) := forall m : NZ, m <= z -> n <= m -> A m. - -Add Morphism A' with signature NZE ==> iff as A'_neg_wd. -Proof. -unfold A'; solve_predicate_wd. -Qed. - -Theorem NZleft_induction : - A z -> (forall n : NZ, n < z -> A (S n) -> A n) -> forall n : NZ, n <= z -> A n. - -End LeftInduction. - -Theorem central_induction : - A z -> - (forall n : NZ, z <= n -> A n -> A (S n)) -> - (forall n : NZ, n < z -> A (S n) -> A n) -> - forall n : NZ, A n. - -End Center. - -Theorem induction_0 : - A 0 -> - (forall n : NZ, 0 <= n -> A n -> A (S n)) -> - (forall n : NZ, n < 0 -> A (S n) -> A n) -> - forall n : NZ, A n. - -(** Elimintation principle for < *) - -Theorem NZlt_ind : forall (n : NZ), - A (S n) -> - (forall m : NZ, n < m -> A m -> A (S m)) -> - forall m : NZ, n < m -> A m. - -(** Elimintation principle for <= *) - -Theorem NZle_ind : forall (n : NZ), - A n -> - (forall m : NZ, n <= m -> A m -> A (S m)) -> - forall m : NZ, n <= m -> A m. - -End Induction. - -End NZOrderPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index f5b757a20..5c6369fe4 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -127,7 +127,7 @@ intros n m. do 2 rewrite NZle_lt_or_eq. rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd. Qed. -Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False. +Theorem NZlt_asymm : forall n m, n < m -> ~ m < n. Proof. intros n m; NZinduct n m. intros H _; false_hyp H NZlt_irrefl. @@ -138,11 +138,6 @@ apply NZlt_lt_succ in H2. apply -> NZlt_le_succ in H1. le_elim H1. now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl. Qed. -Theorem NZlt_asymm : forall n m, n < m -> ~ m < n. -Proof. -intros n m; unfold not; apply NZlt_lt_false. -Qed. - Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p. Proof. intros n m p; NZinduct p m. @@ -151,8 +146,8 @@ intro p. do 2 rewrite NZlt_succ_le. split; intros H H1 H2. le_less; le_elim H2; [now apply H | now rewrite H2 in H1]. assert (n <= p) as H3. apply H. assumption. now le_less. -le_elim H3. assumption. rewrite <- H3 in H2. elimtype False. -now apply (NZlt_lt_false n m). +le_elim H3. assumption. rewrite <- H3 in H2. +elimtype False; now apply (NZlt_asymm n m). Qed. Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p. @@ -177,7 +172,7 @@ Qed. Theorem NZle_antisymm : forall n m : NZ, n <= m -> m <= n -> n == m. Proof. intros n m H1 H2; now (le_elim H1; le_elim H2); -[elimtype False; apply (NZlt_lt_false n m) | | |]. +[elimtype False; apply (NZlt_asymm n m) | | |]. Qed. (** Trichotomy, decidability, and double negation elimination *) @@ -187,12 +182,18 @@ Proof. intros n m; NZinduct n m. right; now left. intro n; rewrite NZlt_succ_le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto. -rewrite <- (NZle_lt_or_eq (S n) m). symmetry (n == m). +rewrite <- (NZle_lt_or_eq (S n) m). +setoid_replace (n == m) with (m == n) using relation iff by now split. stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZle_lt_or_eq. apply or_iff_compat_r. apply NZlt_le_succ. Qed. -Theorem NZE_dec : forall n m : NZ, n == m \/ n ~= m. +(* Decidability of equality, even though true in each finite ring, does not +have a uniform proof. Otherwise, the proof for two fixed numbers would +reduce to a normal form that will say if the numbers are equal or not, +which cannot be true in all finite rings. Therefore, we prove decidability +in the presence of order. *) +Theorem NZeq_em : forall n m : NZ, n == m \/ n ~= m. Proof. intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]]. right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl. @@ -200,69 +201,88 @@ now left. right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl. Qed. -Theorem NZE_dne : forall n m, ~ ~ n == m <-> n == m. +Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m. Proof. intros n m; split; intro H. -destruct (NZE_dec n m) as [H1 | H1]. +destruct (NZeq_em n m) as [H1 | H1]. assumption. false_hyp H1 H. intro H1; now apply H1. Qed. -Theorem NZneq_lt_or_gt : forall n m : NZ, n ~= m <-> n < m \/ m < n. +Theorem NZneq_lt_gt_cases : forall n m : NZ, n ~= m <-> n < m \/ n > m. Proof. intros n m; split. pose proof (NZlt_trichotomy n m); tauto. intros H H1; destruct H as [H | H]; rewrite H1 in H; false_hyp H NZlt_irrefl. Qed. -Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n. +Theorem NZle_gt_cases : forall n m : NZ, n <= m \/ n > m. Proof. intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]]. left; now le_less. left; now le_equal. now right. Qed. -Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n. +(* The following theorem is cleary redundant, but helps not to +remember whether one has to say le_gt_cases or lt_ge_cases *) +Theorem NZlt_ge_cases : forall n m : NZ, n < m \/ n >= m. +Proof. +intros n m; destruct (NZle_gt_cases m n); try (now left); try (now right). +Qed. + +Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m. Proof. intros n m. split; intro H; [intro H1 |]. eapply NZle_lt_trans in H; [| eassumption ..]. false_hyp H NZlt_irrefl. -destruct (NZle_lt_dec n m) as [H1 | H1]. +destruct (NZle_gt_cases n m) as [H1 | H1]. assumption. false_hyp H1 H. Qed. -Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m. +(* Redundant but useful *) +Theorem NZnlt_ge : forall n m : NZ, ~ n < m <-> n >= m. +Proof. +intros n m; symmetry; apply NZle_ngt. +Qed. + +Theorem NZlt_em : forall n m : NZ, n < m \/ ~ n < m. Proof. -intros n m; destruct (NZle_lt_dec m n); -[right; now apply -> NZle_nlt | now left]. +intros n m; destruct (NZle_gt_cases m n); +[right; now apply -> NZle_ngt | now left]. Qed. Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m. Proof. intros n m; split; intro H; -[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | +[destruct (NZlt_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] | intro H1; false_hyp H H1]. Qed. -Theorem NZnle_lt : forall n m : NZ, ~ n <= m <-> m < n. +Theorem NZnle_gt : forall n m : NZ, ~ n <= m <-> n > m. +Proof. +intros n m. rewrite NZle_ngt. apply NZlt_dne. +Qed. + +(* Redundant but useful *) +Theorem NZlt_nge : forall n m : NZ, n < m <-> ~ n >= m. Proof. -intros n m. rewrite NZle_nlt. apply NZlt_dne. +intros n m; symmetry; apply NZnle_gt. Qed. -Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m. +Theorem NZle_em : forall n m : NZ, n <= m \/ ~ n <= m. Proof. -intros n m; destruct (NZle_lt_dec n m); -[now left | right; now apply <- NZnle_lt]. +intros n m; destruct (NZle_gt_cases n m); +[now left | right; now apply <- NZnle_gt]. Qed. Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m. Proof. intros n m; split; intro H; -[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | +[destruct (NZle_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] | intro H1; false_hyp H H1]. Qed. Theorem NZlt_nlt_succ : forall n m : NZ, n < m <-> ~ m < S n. Proof. -intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_lt. +intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_gt. Qed. (* The difference between integers and natural numbers is that for @@ -276,7 +296,7 @@ Lemma NZlt_exists_pred_strong : forall z n m : NZ, z < m -> m <= n -> exists k : NZ, m == S k /\ z <= k. Proof. intro z; NZinduct n z. -intros m H1 H2; apply <- NZnle_lt in H1; false_hyp H2 H1. +intros m H1 H2; apply <- NZnle_gt in H1; false_hyp H2 H1. intro n; split; intros IH m H1 H2. apply -> NZle_succ_le_or_eq_succ in H2; destruct H2 as [H2 | H2]. now apply IH. exists n. now split; [| rewrite <- NZlt_succ_le; rewrite <- H2]. @@ -354,7 +374,7 @@ Qed. Lemma NZrbase : A' z. Proof. -intros m H1 H2. apply -> NZle_nlt in H1. false_hyp H2 H1. +intros m H1 H2. apply -> NZle_ngt in H1. false_hyp H2 H1. Qed. Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n. @@ -401,7 +421,7 @@ Qed. Lemma NZlbase : A' (S z). Proof. intros m H1 H2. apply <- NZlt_le_succ in H2. -apply -> NZle_nlt in H1. false_hyp H2 H1. +apply -> NZle_ngt in H1. false_hyp H2 H1. Qed. Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n. @@ -523,7 +543,7 @@ unfold well_founded. apply NZstrong_right_induction' with (z := z). apply NZAcc_lt_wd. intros n H; constructor; intros y [H1 H2]. -apply <- NZnle_lt in H2. elim H2. now apply NZle_trans with z. +apply <- NZnle_gt in H2. elim H2. now apply NZle_trans with z. intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. Qed. @@ -531,8 +551,3 @@ End WF. End NZOrderPropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v index 061ab84bb..4380cb1b6 100644 --- a/theories/Numbers/NatInt/NZPlus.v +++ b/theories/Numbers/NatInt/NZPlus.v @@ -77,9 +77,3 @@ Qed. End NZPlusPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v index f43b549e2..6368fa557 100644 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ b/theories/Numbers/NatInt/NZPlusOrder.v @@ -65,9 +65,3 @@ Qed. End NZPlusOrderPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZRing.v b/theories/Numbers/NatInt/NZRing.v deleted file mode 100644 index 2425224b8..000000000 --- a/theories/Numbers/NatInt/NZRing.v +++ /dev/null @@ -1,45 +0,0 @@ -Require Export NumPrelude. - -Module Type NZRingSig. - -Parameter Inline NZ : Set. -Parameter Inline NZE : NZ -> NZ -> Prop. -Parameter Inline NZ0 : NZ. -Parameter Inline NZsucc : NZ -> NZ. -Parameter Inline NZplus : NZ -> NZ -> NZ. -Parameter Inline NZtimes : NZ -> NZ -> NZ. - -Axiom NZE_equiv : equiv NZ NZE. -Add Relation NZ NZE - reflexivity proved by (proj1 NZE_equiv) - symmetry proved by (proj2 (proj2 NZE_equiv)) - transitivity proved by (proj1 (proj2 NZE_equiv)) -as NZE_rel. - -Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. - -Delimit Scope NatIntScope with NatInt. -Open Local Scope NatIntScope. -Notation "x == y" := (NZE x y) (at level 70) : NatIntScope. -Notation "x ~= y" := (~ NZE x y) (at level 70) : NatIntScope. -Notation "0" := NZ0 : NatIntScope. -Notation "'S'" := NZsucc. -Notation "1" := (S 0) : NatIntScope. -Notation "x + y" := (NZplus x y) : NatIntScope. -Notation "x * y" := (NZtimes x y) : NatIntScope. - -Axiom NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2. - -Axiom NZinduction : - forall A : NZ -> Prop, predicate_wd NZE A -> - A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n. - -Axiom NZplus_0_l : forall n : NZ, 0 + n == n. -Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). - -Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0. -Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. - -End NZRingSig. diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v index ca78ced69..517a8b7ff 100644 --- a/theories/Numbers/NatInt/NZTimes.v +++ b/theories/Numbers/NatInt/NZTimes.v @@ -66,9 +66,3 @@ Qed. End NZTimesPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 95275f8c0..6f702067d 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -61,31 +61,64 @@ apply NZle_lt_trans with (m + p); [now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l]. Qed. -Theorem NZplus_le_lt_mono_opp : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. +Theorem NZle_lt_plus_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. Proof. -intros n m p q H1 H2. destruct (NZle_lt_dec q p); [| assumption]. -pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_lt in H2. +intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. +pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. false_hyp H3 H2. Qed. -Theorem NZplus_lt_inv : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. +Theorem NZlt_le_plus_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. +pose proof (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZle_le_plus_lt : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. +pose proof (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZplus_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. Proof. intros n m p q H; -destruct (NZle_lt_dec p n) as [H1 | H1]. -destruct (NZle_lt_dec q m) as [H2 | H2]. -pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_nlt in H3. +destruct (NZle_gt_cases p n) as [H1 | H1]. +destruct (NZle_gt_cases q m) as [H2 | H2]. +pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. false_hyp H H3. now right. now left. Qed. -Theorem NZplus_lt_inv_0 : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. +Theorem NZplus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Proof. +intros n m p q H. +destruct (NZle_gt_cases n p) as [H1 | H1]. now left. +destruct (NZle_gt_cases m q) as [H2 | H2]. now right. +assert (H3 : p + q < n + m) by now apply NZplus_lt_mono. +apply -> NZle_ngt in H. false_hyp H3 H. +Qed. + +Theorem NZplus_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. +Proof. +intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l. +Qed. + +Theorem NZplus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Proof. +intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l. +Qed. + +Theorem NZplus_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. Proof. -intros n m H; apply NZplus_lt_inv; now rewrite NZplus_0_l. +intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l. Qed. -Theorem NZplus_gt_inv_0 : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Theorem NZplus_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. Proof. -intros n m H; apply NZplus_lt_inv; now rewrite NZplus_0_l. +intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l. Qed. (** Multiplication and order *) @@ -107,7 +140,7 @@ intros p H IH n m H1. do 2 rewrite NZtimes_succ_l. le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m). intros n1 m1 H2. apply NZplus_lt_mono; [now apply -> IH | assumption]. split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. -apply <- NZle_nlt in H3. le_elim H3. +apply <- NZle_ngt in H3. le_elim H3. apply NZlt_asymm in H2. apply H2. now apply LR. rewrite H3 in H2; false_hyp H2 NZlt_irrefl. rewrite <- H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l. @@ -124,13 +157,13 @@ Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p Proof. NZord_induct p. intros n m H; false_hyp H NZlt_irrefl. -intros p H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_lt in H2. false_hyp H1 H2. +intros p H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. intros p H IH n m H1. apply -> NZlt_le_succ in H. le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). -intros n1 m1 H2. apply (NZplus_le_lt_mono_opp n1 m1). +intros n1 m1 H2. apply (NZle_lt_plus_lt n1 m1). now le_less. do 2 rewrite <- NZtimes_succ_l. now apply -> IH. split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. -apply <- NZle_nlt in H3. le_elim H3. +apply <- NZle_ngt in H3. le_elim H3. apply NZlt_asymm in H2. apply H2. now apply LR. rewrite H3 in H2; false_hyp H2 NZlt_irrefl. rewrite (NZtimes_lt_pred p (S p)); [reflexivity |]. @@ -175,13 +208,13 @@ Theorem NZtimes_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == Proof. intros n m p H; split; intro H1. destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]]. -apply -> NZE_dne; intro H3. apply -> NZneq_lt_or_gt in H3. destruct H3 as [H3 | H3]. +apply -> NZeq_dne; intro H3. apply -> NZneq_lt_gt_cases in H3. destruct H3 as [H3 | H3]. assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_neg_l |]. rewrite H1 in H4; false_hyp H4 NZlt_irrefl. assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |]. rewrite H1 in H4; false_hyp H4 NZlt_irrefl. false_hyp H2 H. -apply -> NZE_dne; intro H3. apply -> NZneq_lt_or_gt in H3. destruct H3 as [H3 | H3]. +apply -> NZeq_dne; intro H3. apply -> NZneq_lt_gt_cases in H3. destruct H3 as [H3 | H3]. assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |]. rewrite H1 in H4; false_hyp H4 NZlt_irrefl. assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |]. @@ -306,10 +339,35 @@ split; intro H1; rewrite H1 in H; (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H. Qed. -End NZTimesOrderPropFunct. +Theorem NZtimes_pos : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite NZtimes_0_l in H; false_hyp H NZlt_irrefl |]; +(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite NZtimes_0_r in H; false_hyp H NZlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m < 0) by now apply NZtimes_neg_pos. +elimtype False; now apply (NZlt_asymm (n * m) 0). +assert (H3 : n * m < 0) by now apply NZtimes_pos_neg. +elimtype False; now apply (NZlt_asymm (n * m) 0). +now apply NZtimes_pos_pos. now apply NZtimes_neg_neg. +Qed. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) +Theorem NZtimes_neg : + forall n m : NZ, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite NZtimes_0_l in H; false_hyp H NZlt_irrefl |]; +(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite NZtimes_0_r in H; false_hyp H NZlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m > 0) by now apply NZtimes_neg_neg. +elimtype False; now apply (NZlt_asymm (n * m) 0). +assert (H3 : n * m > 0) by now apply NZtimes_pos_pos. +elimtype False; now apply (NZlt_asymm (n * m) 0). +now apply NZtimes_neg_pos. now apply NZtimes_pos_neg. +Qed. + +End NZTimesOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index a30c81682..444175c14 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -31,9 +31,3 @@ Axiom recursion_succ : End NAxiomsSig. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index b999240fb..9705d05ba 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -37,6 +37,12 @@ Proof NZsucc_inj_wd. Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m. Proof NZsucc_inj_wd_neg. +(* Decidability of equality was proved only in NZOrder, but since it +does not mention order, we'll put it here *) + +Theorem eq_em : forall n m : N, n == m \/ n ~= m. +Proof NZeq_em. + (* Now we prove that the successor of a number is not zero by defining a function (by recursion) that maps 0 to false and the successor to true *) @@ -241,9 +247,3 @@ Ltac double_induct n m := End NBasePropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NDepRec.v b/theories/Numbers/Natural/Abstract/NDepRec.v index 9ad0b4650..648786854 100644 --- a/theories/Numbers/Natural/Abstract/NDepRec.v +++ b/theories/Numbers/Natural/Abstract/NDepRec.v @@ -70,9 +70,3 @@ Qed. End NDepRecTimesProperties. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NDomain.v b/theories/Numbers/Natural/Abstract/NDomain.v index a95c94ca0..8f326ffec 100644 --- a/theories/Numbers/Natural/Abstract/NDomain.v +++ b/theories/Numbers/Natural/Abstract/NDomain.v @@ -100,9 +100,3 @@ Ltac stepr_ring t := stepr t; [| ring]. End NDomainProperties. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 9ee79022e..66e028abe 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -110,9 +110,3 @@ Qed. End Isomorphism. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index 811126123..07fc67499 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -70,13 +70,18 @@ intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |]. rewrite plus_comm. apply plus_minus. Qed. -Theorem plus_minus_eq : forall n m p : N, m + p == n -> n - m == p. +Theorem plus_minus_eq_l : forall n m p : N, m + p == n -> n - m == p. Proof. intros n m p H. symmetry. -assert (H1 : m + p - m == n - m). now rewrite H. +assert (H1 : m + p - m == n - m) by now rewrite H. rewrite plus_comm in H1. now rewrite plus_minus in H1. Qed. +Theorem plus_minus_eq_r : forall n m p : N, m + p == n -> n - p == m. +Proof. +intros n m p H; rewrite plus_comm in H; now apply plus_minus_eq_l. +Qed. + (* This could be proved by adding m to both sides. Then the proof would use plus_minus_assoc and le_minus_0, which is proven below. *) Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. @@ -137,7 +142,7 @@ Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. Proof. intros n m p; induct n. now rewrite minus_0_l, times_0_l, minus_0_l. -intros n IH. destruct (le_lt_dec m n) as [H | H]. +intros n IH. destruct (le_gt_cases m n) as [H | H]. rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l. rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p). rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |]. @@ -156,9 +161,3 @@ Qed. End NMinusPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v index 362dc0516..4333d9e46 100644 --- a/theories/Numbers/Natural/Abstract/NMiscFunct.v +++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v @@ -396,9 +396,3 @@ Module Export DefaultTimesOrderProperties := End MiscFunctFunctor. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index e8311c63c..f62b5ecb2 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -8,17 +8,17 @@ Open Local Scope NatIntScope. (* Axioms *) -Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y. +Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m. Proof NZle_lt_or_eq. -Theorem lt_succ_le : forall x y, x < S y <-> x <= y. +Theorem lt_irrefl : forall n : N, ~ n < n. +Proof NZlt_irrefl. + +Theorem lt_succ_le : forall n m : N, n < S m <-> n <= m. Proof NZlt_succ_le. (* Renaming theorems from NZOrder.v *) -Theorem lt_irrefl : forall n : N, ~ (n < n). -Proof NZOrdAxiomsMod.NZlt_irrefl. - Theorem lt_le_incl : forall n m : N, n < m -> n <= m. Proof NZlt_le_incl. @@ -67,9 +67,6 @@ Proof NZsucc_lt_mono. Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m. Proof NZsucc_le_mono. -Theorem lt_lt_false : forall n m, n < m -> m < n -> False. -Proof NZlt_lt_false. - Theorem lt_asymm : forall n m, n < m -> ~ m < n. Proof NZlt_asymm. @@ -93,23 +90,32 @@ Proof NZle_antisymm. Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n. Proof NZlt_trichotomy. -Theorem le_lt_dec : forall n m : N, n <= m \/ m < n. -Proof NZle_lt_dec. +Theorem le_gt_cases : forall n m : N, n <= m \/ n > m. +Proof NZle_gt_cases. + +Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m. +Proof NZlt_ge_cases. -Theorem le_nlt : forall n m : N, n <= m <-> ~ m < n. -Proof NZle_nlt. +Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m. +Proof NZle_ngt. -Theorem lt_dec : forall n m : N, n < m \/ ~ n < m. -Proof NZlt_dec. +Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m. +Proof NZnlt_ge. + +Theorem lt_em : forall n m : N, n < m \/ ~ n < m. +Proof NZlt_em. Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m. Proof NZlt_dne. -Theorem nle_lt : forall n m : N, ~ n <= m <-> m < n. -Proof NZnle_lt. +Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m. +Proof NZnle_gt. + +Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m. +Proof NZlt_nge. -Theorem le_dec : forall n m : N, n <= m \/ ~ n <= m. -Proof NZle_dec. +Theorem le_em : forall n m : N, n <= m \/ ~ n <= m. +Proof NZle_em. Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m. Proof NZle_dne. @@ -196,7 +202,7 @@ Proof NZle_ind. Theorem nlt_0_r : forall n : N, ~ n < 0. Proof. -intro n; apply -> le_nlt. apply le_0_l. +intro n; apply -> le_ngt. apply le_0_l. Qed. Theorem nle_succ_0 : forall n, ~ (S n <= 0). @@ -382,9 +388,3 @@ Qed. End NOrderPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NOtherInd.v b/theories/Numbers/Natural/Abstract/NOtherInd.v index 9b01e5143..7faae620a 100644 --- a/theories/Numbers/Natural/Abstract/NOtherInd.v +++ b/theories/Numbers/Natural/Abstract/NOtherInd.v @@ -159,9 +159,3 @@ End Recursion. Implicit Arguments recursion [A]. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v index f1e0e6ace..8ca3ba000 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NPlus.v @@ -42,7 +42,7 @@ Proof NZplus_cancel_l. Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m. Proof NZplus_cancel_r. -(** Theorems that are valid for natural numbers but cannot be proved for N *) +(** Theorems that are valid for natural numbers but cannot be proved for Z *) Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. Proof. @@ -135,9 +135,3 @@ Qed. End NPlusPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v index df4c94614..c4640858e 100644 --- a/theories/Numbers/Natural/Abstract/NPlusOrder.v +++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v @@ -85,9 +85,3 @@ Qed. End NPlusOrderProperties. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NPred.v b/theories/Numbers/Natural/Abstract/NPred.v index 711d6b883..d3d22651c 100644 --- a/theories/Numbers/Natural/Abstract/NPred.v +++ b/theories/Numbers/Natural/Abstract/NPred.v @@ -44,9 +44,3 @@ Qed. End NDefPred. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index c35a6693b..d1f4aac26 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -67,9 +67,3 @@ Implicit Arguments strong_rec [A]. End StrongRecProperties. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v index a0d255892..bcf073ffa 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NTimes.v @@ -39,7 +39,7 @@ Proof NZtimes_1_l. Theorem times_1_r : forall n : N, n * 1 == n. Proof NZtimes_1_r. -Lemma semi_ring : semi_ring_theory 0 1 NZplus NZtimes E. +Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes E. Proof. constructor. exact plus_0_l. @@ -52,7 +52,7 @@ exact times_assoc. exact times_plus_distr_r. Qed. -Add Ring SR : semi_ring. +Add Ring NSR : Nsemi_ring. (** Theorems that cannot be proved in NZTimes *) @@ -112,9 +112,3 @@ Qed. End NTimesPropFunct. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index 68c6c4494..2dbfd8f97 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -28,14 +28,23 @@ Proof NZplus_lt_le_mono. Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. Proof NZplus_le_lt_mono. -Theorem plus_le_lt_mono_opp : forall n m p q : N, n <= m -> p + m < q + n -> p < q. -Proof NZplus_le_lt_mono_opp. +Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_plus_lt. -Theorem plus_lt_inv : forall n m p q : N, n + m < p + q -> n < p \/ m < q. -Proof NZplus_lt_inv. +Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_plus_lt. -Theorem plus_gt_inv_0 : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. -Proof NZplus_gt_inv_0. +Theorem le_le_plus_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_lt. + +Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. +Proof NZplus_lt_cases. + +Theorem plus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Proof NZplus_le_cases. + +Theorem plus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZplus_pos_cases. (** Theorems true for natural numbers *) @@ -123,11 +132,12 @@ Proof NZtimes_eq_0. Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof NZtimes_neq_0. -End NTimesOrderPropFunct. +Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. +Proof. +intros n m; split; [intro H | intros [H1 H2]]. +apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. +now apply times_pos_pos. +Qed. +End NTimesOrderPropFunct. -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 90b338773..557177907 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -194,9 +194,3 @@ end. *) (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 2f6c13cac..f8a9ecd63 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -172,9 +172,3 @@ End NPeanoAxiomsMod. Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 6d3ad55a9..7feed2b14 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -226,12 +226,15 @@ Ltac rewrite_true P H := setoid_replace P with True using relation iff; [| split; intro; [constructor | apply H]]. -Tactic Notation "symmetry" constr(Eq) := +(*Ltac symmetry Eq := lazymatch Eq with | ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff; [| split; intro; symmetry; assumption] | _ => fail Eq "does not have the form (E t1 t2)" -end. +end.*) +(* This does not work because there already is a tactic "symmetry". +Declaring "symmetry" a tactic notation does not work because it conflicts +with "symmetry in": it thinks that "in" is a term. *) Theorem and_cancel_l : forall A B C : Prop, (B -> A) -> (C -> A ) -> ((A /\ B <-> A /\ C) <-> (B <-> C)). diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v index a781411a2..e41052f95 100644 --- a/theories/Numbers/QRewrite.v +++ b/theories/Numbers/QRewrite.v @@ -104,8 +104,8 @@ lazymatch (type of H) with let x1 := fresh "x" in let x2 := fresh "x" in set (x1 := t1); set (x2 := t2); - assert (H1 : E x1 x2); [apply H |]; - assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2); [qiff x1 x2 H1 |]; + assert (H1 : E x1 x2) by apply H; + assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2) by qiff x1 x2 H1; unfold x1 in *; unfold x2 in *; apply <- H2; clear H1 H2 x1 x2 | _ => pattern t1; qsetoid_rewrite H @@ -114,11 +114,15 @@ lazymatch (type of H) with end. Tactic Notation "qsetoid_rewrite" "<-" constr(H) := -let H1 := fresh in - pose proof H as H1; - symmetry in H1; - qsetoid_rewrite H1; - clear H1. +match goal with +| |- ?G => + let H1 := fresh in + pose proof H as H1; + symmetry in H1; (* symmetry unfolds the beta-redex in the goal (!), so we have to restore the goal *) + change G; + qsetoid_rewrite H1; + clear H1 +end. Tactic Notation "qsetoid_replace" constr(t1) "with" constr(t2) "using" "relation" constr(E) := @@ -141,8 +145,19 @@ as E_rel. Notation "x == y" := (E x y) (at level 70). +Parameter P : nat -> nat. +Add Morphism S with signature E ==> E as S_morph. Admitted. +Add Morphism P with signature E ==> E as P_morph. Admitted. Add Morphism plus with signature E ==> E ==> E as plus_morph. Admitted. +Theorem Zplus_pred : forall n m : nat, P n + m == P (n + m). +Proof. +intros n m. +cut (forall n : nat, S (P n) == n). intro H. +pattern n at 2. +qsetoid_rewrite <- (H n). +Admitted. + Goal forall x, x == x + x -> (exists y, forall z, y == y + z -> exists u, x == u) /\ x == 0. intros x H1. pattern x at 1. |