diff options
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 8 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 200 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZTimes.v | 18 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZTimesOrder.v | 67 |
4 files changed, 163 insertions, 130 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 9c9161e2b..f218ed6a6 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -60,8 +60,8 @@ Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). Axiom NZminus_0_r : forall n : NZ, n - 0 == n. Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (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. +Axiom NZtimes_0_l : forall n : NZ, 0 * n == 0. +Axiom NZtimes_succ_l : forall n m : NZ, S n * m == n * m + m. End NZAxiomsSig. @@ -84,9 +84,9 @@ Notation "x <= y" := (NZle x y) : NatIntScope. Notation "x > y" := (NZlt y x) (only parsing) : NatIntScope. Notation "x >= y" := (NZle y x) (only parsing) : NatIntScope. -Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. +Axiom NZlt_eq_cases : 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. +Axiom NZlt_succ_r : forall n m : NZ, n < S m <-> n <= m. Axiom NZmin_l : forall n m : NZ, n <= m -> NZmin n m == n. Axiom NZmin_r : forall n m : NZ, m <= n -> NZmin n m == m. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 4ded2b892..df2f224f4 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -12,14 +12,23 @@ Require Import NZAxioms. Require Import NZTimes. +Require Import Decidable. Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod. Open Local Scope NatIntScope. -Ltac le_less := rewrite NZle_lt_or_eq; left; try assumption. -Ltac le_equal := rewrite NZle_lt_or_eq; right; try reflexivity; try assumption. -Ltac le_elim H := rewrite NZle_lt_or_eq in H; destruct H as [H | H]. +Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H]. + +Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m. +Proof. +intros; apply <- NZlt_eq_cases; now left. +Qed. + +Theorem NZeq_le_incl : forall n m : NZ, n == m -> n <= m. +Proof. +intros; apply <- NZlt_eq_cases; now right. +Qed. Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y. Proof. @@ -46,106 +55,101 @@ 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. -Proof. -intros; now le_less. -Qed. - Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m. Proof. intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl. Qed. -Theorem NZlt_le_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m. +Theorem NZle_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m. Proof. intros n m; split; [intro H | intros [H1 H2]]. -split. le_less. now apply NZlt_neq. +split. now apply NZlt_le_incl. now apply NZlt_neq. le_elim H1. assumption. false_hyp H1 H2. Qed. Theorem NZle_refl : forall n : NZ, n <= n. Proof. -intro; now le_equal. +intro; now apply NZeq_le_incl. Qed. -Theorem NZlt_succ_r : forall n : NZ, n < S n. +Theorem NZlt_succ_diag_r : forall n : NZ, n < S n. Proof. -intro n. rewrite NZlt_succ_le. now le_equal. +intro n. rewrite NZlt_succ_r. now apply NZeq_le_incl. Qed. -Theorem NZle_succ_r : forall n : NZ, n <= S n. +Theorem NZle_succ_diag_r : forall n : NZ, n <= S n. Proof. -intro; le_less; apply NZlt_succ_r. +intro; apply NZlt_le_incl; apply NZlt_succ_diag_r. Qed. -Theorem NZlt_lt_succ : forall n m : NZ, n < m -> n < S m. +Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m. Proof. -intros. rewrite NZlt_succ_le. now le_less. +intros. rewrite NZlt_succ_r. now apply NZlt_le_incl. Qed. -Theorem NZle_le_succ : forall n m : NZ, n <= m -> n <= S m. +Theorem NZle_le_succ_r : forall n m : NZ, n <= m -> n <= S m. Proof. -intros n m H; rewrite <- NZlt_succ_le in H; now le_less. +intros n m H. rewrite <- NZlt_succ_r in H. now apply NZlt_le_incl. Qed. -Theorem NZle_succ_le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. +Theorem NZle_succ_r : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. Proof. -intros n m; rewrite NZle_lt_or_eq. now rewrite NZlt_succ_le. +intros n m; rewrite NZlt_eq_cases. now rewrite NZlt_succ_r. Qed. (* The following theorem is a special case of neq_succ_iter_l below, -but we prove it independently *) +but we prove it separately *) -Theorem NZneq_succ_l : forall n : NZ, S n ~= n. +Theorem NZneq_succ_diag_l : forall n : NZ, S n ~= n. Proof. -intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1. +intros n H. pose proof (NZlt_succ_diag_r n) as H1. rewrite H in H1. false_hyp H1 NZlt_irrefl. Qed. -Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n. +Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n. Proof. -intros n H; apply NZlt_lt_succ in H. false_hyp H NZlt_irrefl. +intro n; apply NZneq_symm; apply NZneq_succ_diag_l. Qed. -Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n. +Theorem NZnlt_succ_diag_l : forall n : NZ, ~ S n < n. +Proof. +intros n H; apply NZlt_lt_succ_r in H. false_hyp H NZlt_irrefl. +Qed. + +Theorem NZnle_succ_diag_l : forall n : NZ, ~ S n <= n. Proof. intros n H; le_elim H. -false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l. +false_hyp H NZnlt_succ_diag_l. false_hyp H NZneq_succ_diag_l. Qed. -Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m. +Theorem NZle_succ_l : forall n m : NZ, S n <= m <-> n < m. Proof. intro n; NZinduct m n. setoid_replace (n < n) with False using relation iff by (apply -> neg_false; apply NZlt_irrefl). now setoid_replace (S n <= n) with False using relation iff by - (apply -> neg_false; apply NZnle_succ_l). -intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ. -rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m). + (apply -> neg_false; apply NZnle_succ_diag_l). +intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r. +rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m). rewrite or_cancel_r. +intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l. apply NZlt_neq. -intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l. reflexivity. Qed. -Theorem NZlt_succ_lt : forall n m : NZ, S n < m -> n < m. -Proof. -intros n m H; apply <- NZlt_le_succ; now le_less. -Qed. - -Theorem NZle_succ_le : forall n m : NZ, S n <= m -> n <= m. +Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m. Proof. -intros n m H; le_less; now apply <- NZlt_le_succ. +intros n m H; apply -> NZle_succ_l; now apply NZlt_le_incl. Qed. Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m. Proof. -intros n m. rewrite NZlt_le_succ. symmetry. apply NZlt_succ_le. +intros n m. rewrite <- NZle_succ_l. symmetry. apply NZlt_succ_r. Qed. Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m. Proof. -intros n m. do 2 rewrite NZle_lt_or_eq. +intros n m. do 2 rewrite NZlt_eq_cases. rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd. Qed. @@ -154,9 +158,9 @@ Proof. intros n m; NZinduct n m. intros H _; false_hyp H NZlt_irrefl. intro n; split; intros H H1 H2. -apply NZlt_succ_lt in H1. apply -> NZlt_succ_le in H2. le_elim H2. +apply NZlt_succ_l in H1. apply -> NZlt_succ_r in H2. le_elim H2. now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl. -apply NZlt_lt_succ in H2. apply -> NZlt_le_succ in H1. le_elim H1. +apply NZlt_lt_succ_r in H2. apply <- NZle_succ_l in H1. le_elim H1. now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl. Qed. @@ -164,10 +168,10 @@ Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p. Proof. intros n m p; NZinduct p m. intros _ H; false_hyp H NZlt_irrefl. -intro p. do 2 rewrite NZlt_succ_le. +intro p. do 2 rewrite NZlt_succ_r. 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. +apply NZlt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. +assert (n <= p) as H3. apply H. assumption. now apply NZlt_le_incl. le_elim H3. assumption. rewrite <- H3 in H2. elimtype False; now apply (NZlt_asymm n m). Qed. @@ -175,8 +179,8 @@ Qed. Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p. Proof. intros n m p H1 H2; le_elim H1. -le_elim H2. le_less; now apply NZlt_trans with (m := m). -le_less; now rewrite <- H2. now rewrite H1. +le_elim H2. apply NZlt_le_incl; now apply NZlt_trans with (m := m). +apply NZlt_le_incl; now rewrite <- H2. now rewrite H1. Qed. Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p. @@ -197,17 +201,22 @@ intros n m H1 H2; now (le_elim H1; le_elim H2); [elimtype False; apply (NZlt_asymm n m) | | |]. Qed. +Theorem NZlt_1_l : forall n m : NZ, 0 < n -> n < m -> 1 < m. +Proof. +intros n m H1 H2. apply <- NZle_succ_l in H1. now apply NZle_lt_trans with n. +Qed. + (** Trichotomy, decidability, and double negation elimination *) Theorem NZlt_trichotomy : forall n m : NZ, n < m \/ n == m \/ m < n. 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). +intro n; rewrite NZlt_succ_r. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto. +rewrite <- (NZlt_eq_cases (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. +stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZlt_eq_cases. +apply or_iff_compat_r. symmetry; apply NZle_succ_l. Qed. (* Decidability of equality, even though true in each finite ring, does not @@ -215,7 +224,8 @@ 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. + +Theorem NZeq_dec : forall n m : NZ, decidable (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. @@ -226,7 +236,7 @@ Qed. Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m. Proof. intros n m; split; intro H. -destruct (NZeq_em n m) as [H1 | H1]. +destruct (NZeq_dec n m) as [H1 | H1]. assumption. false_hyp H1 H. intro H1; now apply H1. Qed. @@ -241,7 +251,7 @@ Qed. 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. +left; now apply NZlt_le_incl. left; now apply NZeq_le_incl. now right. Qed. (* The following theorem is cleary redundant, but helps not to @@ -255,7 +265,7 @@ Qed. Theorem NZle_ge_cases : forall n m : NZ, n <= m \/ n >= m. Proof. intros n m; destruct (NZle_gt_cases n m) as [H | H]. -now left. right; le_less. +now left. right; now apply NZlt_le_incl. Qed. Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m. @@ -267,12 +277,13 @@ assumption. false_hyp H1 H. Qed. (* 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. +Theorem NZlt_dec : forall n m : NZ, decidable (n < m). Proof. intros n m; destruct (NZle_gt_cases m n); [right; now apply -> NZle_ngt | now left]. @@ -281,7 +292,7 @@ Qed. Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m. Proof. intros n m; split; intro H; -[destruct (NZlt_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] | +[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | intro H1; false_hyp H H1]. Qed. @@ -291,12 +302,13 @@ 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; symmetry; apply NZnle_gt. Qed. -Theorem NZle_em : forall n m : NZ, n <= m \/ ~ n <= m. +Theorem NZle_dec : forall n m : NZ, decidable (n <= m). Proof. intros n m; destruct (NZle_gt_cases n m); [now left | right; now apply <- NZnle_gt]. @@ -305,13 +317,13 @@ Qed. Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m. Proof. intros n m; split; intro H; -[destruct (NZle_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] | +[destruct (NZle_dec 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. +Theorem NZnlt_succ_r : forall n m : NZ, ~ m < S n <-> n < m. Proof. -intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_gt. +intros n m; rewrite NZlt_succ_r; apply NZnle_gt. Qed. (* The difference between integers and natural numbers is that for @@ -327,9 +339,9 @@ Proof. intro z; NZinduct n z. 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]. -apply IH. assumption. now apply NZle_le_succ. +apply -> NZle_succ_r in H2; destruct H2 as [H2 | H2]. +now apply IH. exists n. now split; [| rewrite <- NZlt_succ_r; rewrite <- H2]. +apply IH. assumption. now apply NZle_le_succ_r. Qed. Theorem NZlt_exists_pred : @@ -351,7 +363,7 @@ Theorem NZlt_succ_iter_r : forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m. Proof. intros n m; induction n as [| n IH]; simpl in *. -apply NZlt_succ_r. now apply NZlt_lt_succ. +apply NZlt_succ_diag_r. now apply NZlt_lt_succ_r. Qed. Theorem NZneq_succ_iter_l : @@ -389,16 +401,16 @@ Lemma NZrs_rs' : A z -> right_step -> right_step'. Proof. intros Az RS n H1 H2. le_elim H1. apply NZlt_exists_pred in H1. destruct H1 as [k [H3 H4]]. -rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_r]]. +rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_diag_r]]. rewrite <- H1; apply Az. Qed. Lemma NZrs'_rs'' : right_step' -> right_step''. Proof. intros RS' n; split; intros H1 m H2 H3. -apply -> NZlt_succ_le in H3; le_elim H3; +apply -> NZlt_succ_r in H3; le_elim H3; [now apply H1 | rewrite H3 in *; now apply RS']. -apply H1; [assumption | now apply NZlt_lt_succ]. +apply H1; [assumption | now apply NZlt_lt_succ_r]. Qed. Lemma NZrbase : A' z. @@ -408,7 +420,7 @@ Qed. Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n. Proof. -intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_r]. +intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_diag_r]. Qed. Theorem NZstrong_right_induction: right_step' -> forall n : NZ, z <= n -> A n. @@ -427,9 +439,9 @@ Theorem NZright_induction' : Proof. intros L R n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply L; now le_less. -apply L; now le_equal. -apply NZright_induction. apply L; now le_equal. assumption. now le_less. +apply L; now apply NZlt_le_incl. +apply L; now apply NZeq_le_incl. +apply NZright_induction. apply L; now apply NZeq_le_incl. assumption. now apply NZlt_le_incl. Qed. Theorem NZstrong_right_induction' : @@ -437,9 +449,9 @@ Theorem NZstrong_right_induction' : Proof. intros L R n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply L; now le_less. -apply L; now le_equal. -apply NZstrong_right_induction. assumption. now le_less. +apply L; now apply NZlt_le_incl. +apply L; now apply NZeq_le_incl. +apply NZstrong_right_induction. assumption. now apply NZlt_le_incl. Qed. End RightInduction. @@ -454,28 +466,28 @@ Let left_step'' := forall n : NZ, A' n <-> A' (S n). Lemma NZls_ls' : A z -> left_step -> left_step'. Proof. intros Az LS n H1 H2. le_elim H1. -apply LS; [assumption | apply H2; [now apply -> NZlt_le_succ | now le_equal]]. +apply LS; [assumption | apply H2; [now apply <- NZle_succ_l | now apply NZeq_le_incl]]. rewrite H1; apply Az. Qed. Lemma NZls'_ls'' : left_step' -> left_step''. Proof. intros LS' n; split; intros H1 m H2 H3. -apply NZle_succ_le in H3. now apply H1. +apply -> NZle_succ_l in H3. apply NZlt_le_incl in H3. now apply H1. le_elim H3. -apply -> NZlt_le_succ in H3. now apply H1. +apply <- NZle_succ_l in H3. now apply H1. rewrite <- H3 in *; now apply LS'. Qed. Lemma NZlbase : A' (S z). Proof. -intros m H1 H2. apply <- NZlt_le_succ in H2. +intros m H1 H2. apply -> NZle_succ_l in H2. 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. Proof. -intros H1 n H2. apply H1 with (n := n); [assumption | now le_equal]. +intros H1 n H2. apply H1 with (n := n); [assumption | now apply NZeq_le_incl]. Qed. Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n. @@ -494,9 +506,9 @@ Theorem NZleft_induction' : Proof. intros R L n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply NZleft_induction. apply R. now le_equal. assumption. now le_less. -rewrite H; apply R; le_equal. -apply R; le_less. +apply NZleft_induction. apply R. now apply NZeq_le_incl. assumption. now apply NZlt_le_incl. +rewrite H; apply R; now apply NZeq_le_incl. +apply R; now apply NZlt_le_incl. Qed. Theorem NZstrong_left_induction' : @@ -504,9 +516,9 @@ Theorem NZstrong_left_induction' : Proof. intros R L n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply NZstrong_left_induction; auto. le_less. -rewrite H; apply R; le_equal. -apply R; le_less. +apply NZstrong_left_induction; auto. now apply NZlt_le_incl. +rewrite H; apply R; now apply NZeq_le_incl. +apply R; now apply NZlt_le_incl. Qed. End LeftInduction. @@ -519,9 +531,9 @@ Theorem NZorder_induction : Proof. intros Az RS LS n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -now apply NZleft_induction; [| | le_less]. +now apply NZleft_induction; [| | apply NZlt_le_incl]. now rewrite H. -now apply NZright_induction; [| | le_less]. +now apply NZright_induction; [| | apply NZlt_le_incl]. Qed. Theorem NZorder_induction' : @@ -531,7 +543,7 @@ Theorem NZorder_induction' : forall n : NZ, A n. Proof. intros Az AS AP n; apply NZorder_induction; try assumption. -intros m H1 H2. apply AP in H2; [| now apply -> NZlt_le_succ]. +intros m H1 H2. apply AP in H2; [| now apply <- NZle_succ_l]. unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); [assumption | apply NZpred_succ]. Qed. @@ -560,8 +572,8 @@ Theorem NZlt_ind : forall (n : NZ), forall m : NZ, n < m -> A m. Proof. intros n H1 H2 m H3. -apply NZright_induction with (S n); [assumption | | now apply -> NZlt_le_succ]. -intros; apply H2; try assumption. now apply <- NZlt_le_succ. +apply NZright_induction with (S n); [assumption | | now apply <- NZle_succ_l]. +intros; apply H2; try assumption. now apply -> NZle_succ_l. Qed. (** Elimintation principle for <= *) @@ -632,7 +644,7 @@ apply NZAcc_gt_wd. intros n H; constructor; intros y [H1 H2]. apply <- NZnle_gt in H2. elim H2. now apply NZle_lt_trans with n. intros n H1 H2; constructor; intros m [H3 H4]. -apply H2. assumption. now apply -> NZlt_le_succ. +apply H2. assumption. now apply <- NZle_succ_l. Qed. End WF. diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v index e0d1f6350..20bd3cdc6 100644 --- a/theories/Numbers/NatInt/NZTimes.v +++ b/theories/Numbers/NatInt/NZTimes.v @@ -17,20 +17,20 @@ Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig). Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod. Open Local Scope NatIntScope. -Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0. +Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0. Proof. NZinduct n. -now rewrite NZtimes_0_r. -intro. rewrite NZtimes_succ_r. now rewrite NZplus_0_r. +now rewrite NZtimes_0_l. +intro. rewrite NZtimes_succ_l. now rewrite NZplus_0_r. Qed. -Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m. +Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. Proof. -intros n m; NZinduct m. -do 2 rewrite NZtimes_0_r; now rewrite NZplus_0_l. -intro m. do 2 rewrite NZtimes_succ_r. do 2 rewrite NZplus_succ_r. -rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) n m). -rewrite (NZplus_comm n m). rewrite NZplus_assoc. +intros n m; NZinduct n. +do 2 rewrite NZtimes_0_l; now rewrite NZplus_0_l. +intro n. do 2 rewrite NZtimes_succ_l. do 2 rewrite NZplus_succ_r. +rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) m n). +rewrite (NZplus_comm m n). rewrite NZplus_assoc. now rewrite NZplus_cancel_r. Qed. diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 6fc0078c0..4b4516069 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -200,11 +200,11 @@ 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_gt in H2. false_hyp H1 H2. -intros p H IH n m H1. apply -> NZlt_le_succ in H. +intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. +intros p H IH n m H1. apply <- NZle_succ_l in H. le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). intros n1 m1 H2. apply (NZle_lt_plus_lt n1 m1). -now le_less. do 2 rewrite <- NZtimes_succ_l. now apply -> IH. +now apply NZlt_le_incl. do 2 rewrite <- NZtimes_succ_l. now apply -> IH. split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. apply <- NZle_ngt in H3. le_elim H3. apply NZlt_asymm in H2. apply H2. now apply LR. @@ -222,17 +222,17 @@ Qed. Theorem NZtimes_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. le_less. now apply -> NZtimes_lt_mono_pos_l. -le_equal; now rewrite H2. -le_equal; rewrite <- H1; now do 2 rewrite NZtimes_0_l. +le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_pos_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZtimes_0_l. Qed. Theorem NZtimes_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. le_less. now apply -> NZtimes_lt_mono_neg_l. -le_equal; now rewrite H2. -le_equal; rewrite H1; now do 2 rewrite NZtimes_0_l. +le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_neg_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZtimes_0_l. Qed. Theorem NZtimes_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. @@ -272,7 +272,7 @@ Qed. Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). Proof. -intros n m p H; do 2 rewrite NZle_lt_or_eq. +intros n m p H; do 2 rewrite NZlt_eq_cases. rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |]. now rewrite -> (NZtimes_cancel_l n m p); [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. @@ -286,7 +286,7 @@ Qed. Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). Proof. -intros n m p H; do 2 rewrite NZle_lt_or_eq. +intros n m p H; do 2 rewrite NZlt_eq_cases. rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |]. rewrite -> (NZtimes_cancel_l m n p); [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. @@ -304,7 +304,7 @@ Theorem NZtimes_lt_mono : Proof. intros n m p q H1 H2 H3 H4. apply NZle_lt_trans with (m * p). -apply NZtimes_le_mono_nonneg_r; [assumption | now le_less]. +apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. apply -> NZtimes_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. Qed. @@ -316,10 +316,10 @@ Theorem NZtimes_le_mono : Proof. intros n m p q H1 H2 H3 H4. le_elim H2; le_elim H4. -le_less; now apply NZtimes_lt_mono. -rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now le_less]. -rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now le_less]. -rewrite H2; rewrite H4; now le_equal. +apply NZlt_le_incl; now apply NZtimes_lt_mono. +rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. +rewrite H2; rewrite H4; now apply NZeq_le_incl. Qed. Theorem NZtimes_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. @@ -368,25 +368,46 @@ Proof. intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos. Qed. -Theorem NZtimes_eq_0 : forall n m : NZ, n * m == 0 -> n == 0 \/ m == 0. +Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. Proof. -intros n m H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1. +rewrite NZtimes_1_l in H1. now apply NZlt_1_l with m. +assumption. +Qed. + +Theorem NZeq_times_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0. +Proof. +intros n m; split. +intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; try (now right); try (now left). elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_neg_neg |]. elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_neg_pos |]. elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_pos_neg |]. elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_pos_pos |]. +intros [H | H]. now rewrite H, NZtimes_0_l. now rewrite H, NZtimes_0_r. Qed. -Theorem NZtimes_neq_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Theorem NZneq_times_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply NZtimes_eq_0 in H1. tauto. +intro H1; apply -> NZeq_times_0 in H1. tauto. split; intro H1; rewrite H1 in H; (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H. Qed. +Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. +Proof. +intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1]. +assumption. false_hyp H1 H2. +Qed. + +Theorem NZeq_times_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. +Proof. +intros n m H1 H2; apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1]. +false_hyp H1 H2. assumption. +Qed. + 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]]]. @@ -420,12 +441,12 @@ Qed. Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. Proof. -intros n m H. apply -> NZlt_le_succ in H. +intros n m H. apply <- NZle_succ_l in H. apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H. repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *. repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l. -now apply <- NZlt_le_succ. -apply NZplus_pos_pos; now apply NZlt_succ_r. +now apply -> NZle_succ_l. +apply NZplus_pos_pos; now apply NZlt_succ_diag_r. Qed. End NZTimesOrderPropFunct. |