diff options
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 91 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAddOrder.v | 166 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 99 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 84 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 80 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMulOrder.v | 310 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 666 |
7 files changed, 1496 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v new file mode 100644 index 00000000..c9bb5c95 --- /dev/null +++ b/theories/Numbers/NatInt/NZAdd.v @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import NZAxioms. +Require Import NZBase. + +Module NZAddPropFunct (Import NZAxiomsMod : NZAxiomsSig). +Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod. +Open Local Scope NatIntScope. + +Theorem NZadd_0_r : forall n : NZ, n + 0 == n. +Proof. +NZinduct n. now rewrite NZadd_0_l. +intro. rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_succ_r : forall n m : NZ, n + S m == S (n + m). +Proof. +intros n m; NZinduct n. +now do 2 rewrite NZadd_0_l. +intro. repeat rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_comm : forall n m : NZ, n + m == m + n. +Proof. +intros n m; NZinduct n. +rewrite NZadd_0_l; now rewrite NZadd_0_r. +intros n. rewrite NZadd_succ_l; rewrite NZadd_succ_r. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_1_l : forall n : NZ, 1 + n == S n. +Proof. +intro n; rewrite NZadd_succ_l; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_1_r : forall n : NZ, n + 1 == S n. +Proof. +intro n; rewrite NZadd_comm; apply NZadd_1_l. +Qed. + +Theorem NZadd_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p. +Proof. +intros n m p; NZinduct n. +now do 2 rewrite NZadd_0_l. +intro. do 3 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q). +Proof. +intros n m p q. +rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_comm m (p + q)). +rewrite <- (NZadd_assoc p q m). rewrite (NZadd_assoc n p (q + m)). +now rewrite (NZadd_comm q m). +Qed. + +Theorem NZadd_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p). +Proof. +intros n m p q. +rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_assoc m p q). +rewrite (NZadd_comm (m + p) q). now rewrite <- (NZadd_assoc n q (m + p)). +Qed. + +Theorem NZadd_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. +Proof. +intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). +apply NZadd_cancel_l. +Qed. + +Theorem NZsub_1_r : forall n : NZ, n - 1 == P n. +Proof. +intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r. +Qed. + +End NZAddPropFunct. + diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v new file mode 100644 index 00000000..50d1c42f --- /dev/null +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -0,0 +1,166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZAddOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import NZAxioms. +Require Import NZOrder. + +Module NZAddOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). +Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod. +Open Local Scope NatIntScope. + +Theorem NZadd_lt_mono_l : forall n m p : NZ, n < m <-> p + n < p + m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono. +Qed. + +Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p. +Proof. +intros n m p. +rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l. +Qed. + +Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZlt_trans with (m + p); +[now apply -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l]. +Qed. + +Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono. +Qed. + +Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p. +Proof. +intros n m p. +rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l. +Qed. + +Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q. +Proof. +intros n m p q H1 H2. +apply NZle_trans with (m + p); +[now apply -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l]. +Qed. + +Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZlt_le_trans with (m + p); +[now apply -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l]. +Qed. + +Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZle_lt_trans with (m + p); +[now apply -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l]. +Qed. + +Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono. +Qed. + +Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono. +Qed. + +Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono. +Qed. + +Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono. +Qed. + +Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m. +Proof. +intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H. +now rewrite NZadd_0_l in H. +Qed. + +Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n. +Proof. +intros; rewrite NZadd_comm; now apply NZlt_add_pos_l. +Qed. + +Theorem NZle_lt_add_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 (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. +false_hyp H3 H2. +Qed. + +Theorem NZlt_le_add_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 (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZle_le_add_le : 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 (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZadd_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_gt_cases p n) as [H1 | H1]. +destruct (NZle_gt_cases q m) as [H2 | H2]. +pose proof (NZadd_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 NZadd_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 NZadd_lt_mono. +apply -> NZle_ngt in H. false_hyp H3 H. +Qed. + +Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. +Proof. +intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Proof. +intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof. +intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof. +intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. +Qed. + +End NZAddOrderPropFunct. + diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v new file mode 100644 index 00000000..26933646 --- /dev/null +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -0,0 +1,99 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NumPrelude. + +Module Type NZAxiomsSig. + +Parameter Inline NZ : Type. +Parameter Inline NZeq : NZ -> NZ -> Prop. +Parameter Inline NZ0 : NZ. +Parameter Inline NZsucc : NZ -> NZ. +Parameter Inline NZpred : NZ -> NZ. +Parameter Inline NZadd : NZ -> NZ -> NZ. +Parameter Inline NZsub : NZ -> NZ -> NZ. +Parameter Inline NZmul : NZ -> NZ -> NZ. + +(* Unary subtraction (opp) is not defined on natural numbers, so we have + it for integers only *) + +Axiom NZeq_equiv : equiv NZ NZeq. +Add Relation NZ NZeq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) +as NZeq_rel. + +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. + +Delimit Scope NatIntScope with NatInt. +Open Local Scope NatIntScope. +Notation "x == y" := (NZeq x y) (at level 70) : NatIntScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatIntScope. +Notation "0" := NZ0 : NatIntScope. +Notation S := NZsucc. +Notation P := NZpred. +Notation "1" := (S 0) : NatIntScope. +Notation "x + y" := (NZadd x y) : NatIntScope. +Notation "x - y" := (NZsub x y) : NatIntScope. +Notation "x * y" := (NZmul x y) : NatIntScope. + +Axiom NZpred_succ : forall n : NZ, P (S n) == n. + +Axiom NZinduction : + forall A : NZ -> Prop, predicate_wd NZeq A -> + A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n. + +Axiom NZadd_0_l : forall n : NZ, 0 + n == n. +Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). + +Axiom NZsub_0_r : forall n : NZ, n - 0 == n. +Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). + +Axiom NZmul_0_l : forall n : NZ, 0 * n == 0. +Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m. + +End NZAxiomsSig. + +Module Type NZOrdAxiomsSig. +Declare Module Export NZAxiomsMod : NZAxiomsSig. +Open Local Scope NatIntScope. + +Parameter Inline NZlt : NZ -> NZ -> Prop. +Parameter Inline NZle : NZ -> NZ -> Prop. +Parameter Inline NZmin : NZ -> NZ -> NZ. +Parameter Inline NZmax : NZ -> NZ -> NZ. + +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. +Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. +Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. + +Notation "x < y" := (NZlt x y) : NatIntScope. +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 NZlt_eq_cases : forall n m : NZ, n <= m <-> n < m \/ n == m. +Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). +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. +Axiom NZmax_l : forall n m : NZ, m <= n -> NZmax n m == n. +Axiom NZmax_r : forall n m : NZ, n <= m -> NZmax n m == m. + +End NZOrdAxiomsSig. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v new file mode 100644 index 00000000..8b01e353 --- /dev/null +++ b/theories/Numbers/NatInt/NZBase.v @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZBase.v 10934 2008-05-15 21:58:20Z letouzey $ i*) + +Require Import NZAxioms. + +Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig). +Open Local Scope NatIntScope. + +Theorem NZneq_symm : forall n m : NZ, n ~= m -> m ~= n. +Proof. +intros n m H1 H2; symmetry in H2; false_hyp H2 H1. +Qed. + +Theorem NZE_stepl : forall x y z : NZ, x == y -> x == z -> z == y. +Proof. +intros x y z H1 H2; now rewrite <- H1. +Qed. + +Declare Left Step NZE_stepl. +(* The right step lemma is just the transitivity of NZeq *) +Declare Right Step (proj1 (proj2 NZeq_equiv)). + +Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2. +Proof. +intros n1 n2 H. +apply NZpred_wd in H. now do 2 rewrite NZpred_succ in H. +Qed. + +(* The following theorem is useful as an equivalence for proving +bidirectional induction steps *) +Theorem NZsucc_inj_wd : forall n1 n2 : NZ, S n1 == S n2 <-> n1 == n2. +Proof. +intros; split. +apply NZsucc_inj. +apply NZsucc_wd. +Qed. + +Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m. +Proof. +intros; now rewrite NZsucc_inj_wd. +Qed. + +(* We cannot prove that the predecessor is injective, nor that it is +left-inverse to the successor at this point *) + +Section CentralInduction. + +Variable A : predicate NZ. + +Hypothesis A_wd : predicate_wd NZeq A. + +Add Morphism A with signature NZeq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Theorem NZcentral_induction : + forall z : NZ, A z -> + (forall n : NZ, A n <-> A (S n)) -> + forall n : NZ, A n. +Proof. +intros z Base Step; revert Base; pattern z; apply NZinduction. +solve_predicate_wd. +intro; now apply NZinduction. +intro; pose proof (Step n); tauto. +Qed. + +End CentralInduction. + +Tactic Notation "NZinduct" ident(n) := + induction_maker n ltac:(apply NZinduction). + +Tactic Notation "NZinduct" ident(n) constr(u) := + induction_maker n ltac:(apply NZcentral_induction with (z := u)). + +End NZBasePropFunct. + diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v new file mode 100644 index 00000000..fda8b7a3 --- /dev/null +++ b/theories/Numbers/NatInt/NZMul.v @@ -0,0 +1,80 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import NZAxioms. +Require Import NZAdd. + +Module NZMulPropFunct (Import NZAxiomsMod : NZAxiomsSig). +Module Export NZAddPropMod := NZAddPropFunct NZAxiomsMod. +Open Local Scope NatIntScope. + +Theorem NZmul_0_r : forall n : NZ, n * 0 == 0. +Proof. +NZinduct n. +now rewrite NZmul_0_l. +intro. rewrite NZmul_succ_l. now rewrite NZadd_0_r. +Qed. + +Theorem NZmul_succ_r : forall n m : NZ, n * (S m) == n * m + n. +Proof. +intros n m; NZinduct n. +do 2 rewrite NZmul_0_l; now rewrite NZadd_0_l. +intro n. do 2 rewrite NZmul_succ_l. do 2 rewrite NZadd_succ_r. +rewrite NZsucc_inj_wd. rewrite <- (NZadd_assoc (n * m) m n). +rewrite (NZadd_comm m n). rewrite NZadd_assoc. +now rewrite NZadd_cancel_r. +Qed. + +Theorem NZmul_comm : forall n m : NZ, n * m == m * n. +Proof. +intros n m; NZinduct n. +rewrite NZmul_0_l; now rewrite NZmul_0_r. +intro. rewrite NZmul_succ_l; rewrite NZmul_succ_r. now rewrite NZadd_cancel_r. +Qed. + +Theorem NZmul_add_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p. +Proof. +intros n m p; NZinduct n. +rewrite NZmul_0_l. now do 2 rewrite NZadd_0_l. +intro n. rewrite NZadd_succ_l. do 2 rewrite NZmul_succ_l. +rewrite <- (NZadd_assoc (n * p) p (m * p)). +rewrite (NZadd_comm p (m * p)). rewrite (NZadd_assoc (n * p) (m * p) p). +now rewrite NZadd_cancel_r. +Qed. + +Theorem NZmul_add_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p. +Proof. +intros n m p. +rewrite (NZmul_comm n (m + p)). rewrite (NZmul_comm n m). +rewrite (NZmul_comm n p). apply NZmul_add_distr_r. +Qed. + +Theorem NZmul_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p. +Proof. +intros n m p; NZinduct n. +now do 3 rewrite NZmul_0_l. +intro n. do 2 rewrite NZmul_succ_l. rewrite NZmul_add_distr_r. +now rewrite NZadd_cancel_r. +Qed. + +Theorem NZmul_1_l : forall n : NZ, 1 * n == n. +Proof. +intro n. rewrite NZmul_succ_l; rewrite NZmul_0_l. now rewrite NZadd_0_l. +Qed. + +Theorem NZmul_1_r : forall n : NZ, n * 1 == n. +Proof. +intro n; rewrite NZmul_comm; apply NZmul_1_l. +Qed. + +End NZMulPropFunct. + diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v new file mode 100644 index 00000000..c707bf73 --- /dev/null +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -0,0 +1,310 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import NZAxioms. +Require Import NZAddOrder. + +Module NZMulOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). +Module Export NZAddOrderPropMod := NZAddOrderPropFunct NZOrdAxiomsMod. +Open Local Scope NatIntScope. + +Theorem NZmul_lt_pred : + forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). +Proof. +intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l. +rewrite <- (NZadd_assoc (p * n) n m). +rewrite <- (NZadd_assoc (p * m) m n). +rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r. +Qed. + +Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m). +Proof. +NZord_induct p. +intros n m H; false_hyp H NZlt_irrefl. +intros p H IH n m H1. do 2 rewrite NZmul_succ_l. +le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m). +intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption]. +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. +rewrite H3 in H2; false_hyp H2 NZlt_irrefl. +rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. +intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1. +Qed. + +Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p). +Proof. +intros p n m. +rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l. +Qed. + +Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n). +Proof. +NZord_induct p. +intros n m H; false_hyp H NZlt_irrefl. +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_add_lt n1 m1). +now apply NZlt_le_incl. do 2 rewrite <- NZmul_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. +rewrite H3 in H2; false_hyp H2 NZlt_irrefl. +rewrite (NZmul_lt_pred p (S p)) by reflexivity. +rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. +Qed. + +Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p). +Proof. +intros p n m. +rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l. +Qed. + +Theorem NZmul_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. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l. +Qed. + +Theorem NZmul_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. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l. +Qed. + +Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. +Proof. +intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +now apply NZmul_le_mono_nonneg_l. +Qed. + +Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p. +Proof. +intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +now apply NZmul_le_mono_nonpos_l. +Qed. + +Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m). +Proof. +intros n m p H; split; intro H1. +destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]]. +apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. +assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |]. +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |]. +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +false_hyp H2 H. +apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. +assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l). +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l). +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +now rewrite H1. +Qed. + +Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m). +Proof. +intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l. +Qed. + +Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1). +Proof. +intros n m H. +stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r. +Qed. + +Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1). +Proof. +intros n m; rewrite NZmul_comm; apply NZmul_id_l. +Qed. + +Theorem NZmul_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 NZlt_eq_cases. +rewrite (NZmul_lt_mono_pos_l p n m) by assumption. +now rewrite -> (NZmul_cancel_l n m p) by +(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). +Qed. + +Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p). +Proof. +intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +apply NZmul_le_mono_pos_l. +Qed. + +Theorem NZmul_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 NZlt_eq_cases. +rewrite (NZmul_lt_mono_neg_l p n m); [| assumption]. +rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). +now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro). +Qed. + +Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p). +Proof. +intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +apply NZmul_le_mono_neg_l. +Qed. + +Theorem NZmul_lt_mono_nonneg : + forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof. +intros n m p q H1 H2 H3 H4. +apply NZle_lt_trans with (m * p). +apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. +Qed. + +(* There are still many variants of the theorem above. One can assume 0 < n +or 0 < p or n <= m or p <= q. *) + +Theorem NZmul_le_mono_nonneg : + forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof. +intros n m p q H1 H2 H3 H4. +le_elim H2; le_elim H4. +apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg. +rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. +rewrite H2; rewrite H4; now apply NZeq_le_incl. +Qed. + +Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r. +Qed. + +Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. +Qed. + +Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. +Qed. + +Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0. +Proof. +intros; rewrite NZmul_comm; now apply NZmul_pos_neg. +Qed. + +Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. +rewrite NZmul_1_l in H1. now apply NZlt_1_l with m. +assumption. +Qed. + +Theorem NZeq_mul_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 NZmul_neg_neg |]. +elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |]. +elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |]. +elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |]. +intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r. +Qed. + +Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof. +intros n m; split; intro H. +intro H1; apply -> NZeq_mul_0 in H1. tauto. +split; intro H1; rewrite H1 in H; +(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H. +Qed. + +Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0. +Proof. +intro n; rewrite NZeq_mul_0; tauto. +Qed. + +Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. +Proof. +intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. +assumption. false_hyp H1 H2. +Qed. + +Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. +Proof. +intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. +false_hyp H1 H2. assumption. +Qed. + +Theorem NZlt_0_mul : 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 NZmul_0_l in H; false_hyp H NZlt_irrefl |]; +(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite NZmul_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 NZmul_neg_pos. +elimtype False; now apply (NZlt_asymm (n * m) 0). +assert (H3 : n * m < 0) by now apply NZmul_pos_neg. +elimtype False; now apply (NZlt_asymm (n * m) 0). +now apply NZmul_pos_pos. now apply NZmul_neg_neg. +Qed. + +Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m. +Proof. +intros n m H1 H2. now apply NZmul_lt_mono_nonneg. +Qed. + +Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply NZmul_le_mono_nonneg. +Qed. + +(* The converse theorems require nonnegativity (or nonpositivity) of the +other variable *) + +Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +now apply NZlt_le_trans with 0. +destruct (NZlt_ge_cases n m). +assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg. +apply -> NZle_ngt in F. false_hyp H2 F. +Qed. + +Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +apply NZlt_le_incl; now apply NZlt_le_trans with 0. +destruct (NZle_gt_cases n m). +assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg. +apply -> NZlt_nge in F. false_hyp H2 F. +Qed. + +Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof. +intros n m H. apply <- NZle_succ_l in H. +apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H. +repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *. +repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l. +now apply -> NZle_succ_l. +apply NZadd_pos_pos; now apply NZlt_succ_diag_r. +Qed. + +End NZMulOrderPropFunct. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v new file mode 100644 index 00000000..15004824 --- /dev/null +++ b/theories/Numbers/NatInt/NZOrder.v @@ -0,0 +1,666 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import NZAxioms. +Require Import NZMul. +Require Import Decidable. + +Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). +Module Export NZMulPropMod := NZMulPropFunct NZAxiomsMod. +Open Local Scope NatIntScope. + +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. +intros x y z H1 H2; now rewrite <- H2. +Qed. + +Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z. +Proof. +intros x y z H1 H2; now rewrite <- H2. +Qed. + +Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y. +Proof. +intros x y z H1 H2; now rewrite <- H2. +Qed. + +Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z. +Proof. +intros x y z H1 H2; now rewrite <- H2. +Qed. + +Declare Left Step NZlt_stepl. +Declare Right Step NZlt_stepr. +Declare Left Step NZle_stepl. +Declare Right Step NZle_stepr. + +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 NZle_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m. +Proof. +intros n m; split; [intro H | intros [H1 H2]]. +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 apply NZeq_le_incl. +Qed. + +Theorem NZlt_succ_diag_r : forall n : NZ, n < S n. +Proof. +intro n. rewrite NZlt_succ_r. now apply NZeq_le_incl. +Qed. + +Theorem NZle_succ_diag_r : forall n : NZ, n <= S n. +Proof. +intro; apply NZlt_le_incl; apply NZlt_succ_diag_r. +Qed. + +Theorem NZlt_0_1 : 0 < 1. +Proof. +apply NZlt_succ_diag_r. +Qed. + +Theorem NZle_0_1 : 0 <= 1. +Proof. +apply NZle_succ_diag_r. +Qed. + +Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m. +Proof. +intros. rewrite NZlt_succ_r. now apply NZlt_le_incl. +Qed. + +Theorem NZle_le_succ_r : forall n m : NZ, n <= m -> n <= S m. +Proof. +intros n m H. rewrite <- NZlt_succ_r in H. now apply NZlt_le_incl. +Qed. + +Theorem NZle_succ_r : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. +Proof. +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 separately *) + +Theorem NZneq_succ_diag_l : forall n : NZ, S n ~= n. +Proof. +intros n H. pose proof (NZlt_succ_diag_r n) as H1. rewrite H in H1. +false_hyp H1 NZlt_irrefl. +Qed. + +Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n. +Proof. +intro n; apply NZneq_symm; apply NZneq_succ_diag_l. +Qed. + +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_diag_l. false_hyp H NZneq_succ_diag_l. +Qed. + +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_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. +reflexivity. +intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l. +apply NZlt_neq. +Qed. + +Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m. +Proof. +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 <- 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 NZlt_eq_cases. +rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZlt_asymm : forall n m, n < m -> ~ m < n. +Proof. +intros n m; NZinduct n m. +intros H _; false_hyp H NZlt_irrefl. +intro n; split; intros H H1 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_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. + +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_r. +split; intros H H1 H2. +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. + +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. 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. +Proof. +intros n m p H1 H2; le_elim H1. +now apply NZlt_trans with (m := m). now rewrite H1. +Qed. + +Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p. +Proof. +intros n m p H1 H2; le_elim H2. +now apply NZlt_trans with (m := m). now rewrite <- H2. +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_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_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 <- 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 +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_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. +now left. +right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl. +Qed. + +(* DNE stands for double-negation elimination *) + +Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m. +Proof. +intros n m; split; intro H. +destruct (NZeq_dec n m) as [H1 | H1]. +assumption. false_hyp H1 H. +intro H1; now apply H1. +Qed. + +Theorem NZlt_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_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 apply NZlt_le_incl. left; now apply NZeq_le_incl. now right. +Qed. + +(* 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_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; now apply NZlt_le_incl. +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_gt_cases n m) as [H1 | H1]. +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_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]. +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] | +intro H1; false_hyp H H1]. +Qed. + +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; symmetry; apply NZnle_gt. +Qed. + +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]. +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] | +intro H1; false_hyp H H1]. +Qed. + +Theorem NZnlt_succ_r : forall n m : NZ, ~ m < S n <-> n < m. +Proof. +intros n m; rewrite NZlt_succ_r; apply NZnle_gt. +Qed. + +(* 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. +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_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 : + forall z n : NZ, z < n -> exists k : NZ, n == S k /\ z <= k. +Proof. +intros z n H; apply NZlt_exists_pred_strong with (z := z) (n := n). +assumption. apply NZle_refl. +Qed. + +(** 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_rect (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. +Proof. +intros n m; induction n as [| n IH]; simpl in *. +apply NZlt_succ_diag_r. now apply NZlt_lt_succ_r. +Qed. + +Theorem NZneq_succ_iter_l : + forall (n : nat) (m : NZ), NZsucc_iter (Datatypes.S n) m ~= m. +Proof. +intros n m H. pose proof (NZlt_succ_iter_r n m) as H1. rewrite H in H1. +false_hyp H1 NZlt_irrefl. +Qed. + +(* 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 NZeq A. + +Add Morphism A with signature NZeq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +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. +Let right_step := forall n : NZ, z <= n -> A n -> A (S n). +Let right_step' := forall n : NZ, z <= n -> A' n -> A n. +Let right_step'' := forall n : NZ, A' n <-> A' (S n). + +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_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_r in H3; le_elim H3; +[now apply H1 | rewrite H3 in *; now apply RS']. +apply H1; [assumption | now apply NZlt_lt_succ_r]. +Qed. + +Lemma NZrbase : A' z. +Proof. +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. +Proof. +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. +Proof. +intro RS'; apply NZA'A_right; unfold A'; NZinduct n z; +[apply NZrbase | apply NZrs'_rs''; apply RS']. +Qed. + +Theorem NZright_induction : A z -> right_step -> forall n : NZ, z <= n -> A n. +Proof. +intros Az RS; apply NZstrong_right_induction; now apply NZrs_rs'. +Qed. + +Theorem NZright_induction' : + (forall n : NZ, n <= z -> A n) -> right_step -> forall n : NZ, A n. +Proof. +intros L R n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +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' : + (forall n : NZ, n <= z -> A n) -> right_step' -> forall n : NZ, A n. +Proof. +intros L R n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +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. + +Section LeftInduction. + +Let A' (n : NZ) := forall m : NZ, m <= z -> n <= m -> A m. +Let left_step := forall n : NZ, n < z -> A (S n) -> A n. +Let left_step' := forall n : NZ, n <= z -> A' (S n) -> A n. +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 <- 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_l in H3. apply NZlt_le_incl in H3. now apply H1. +le_elim H3. +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 -> 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 apply NZeq_le_incl]. +Qed. + +Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n. +Proof. +intro LS'; apply NZA'A_left; unfold A'; NZinduct n (S z); +[apply NZlbase | apply NZls'_ls''; apply LS']. +Qed. + +Theorem NZleft_induction : A z -> left_step -> forall n : NZ, n <= z -> A n. +Proof. +intros Az LS; apply NZstrong_left_induction; now apply NZls_ls'. +Qed. + +Theorem NZleft_induction' : + (forall n : NZ, z <= n -> A n) -> left_step -> forall n : NZ, A n. +Proof. +intros R L n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +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' : + (forall n : NZ, z <= n -> A n) -> left_step' -> forall n : NZ, A n. +Proof. +intros R L n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +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. + +Theorem NZorder_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. +Proof. +intros Az RS LS n. +destruct (NZlt_trichotomy n z) as [H | [H | H]]. +now apply NZleft_induction; [| | apply NZlt_le_incl]. +now rewrite H. +now apply NZright_induction; [| | apply NZlt_le_incl]. +Qed. + +Theorem NZorder_induction' : + A z -> + (forall n : NZ, z <= n -> A n -> A (S n)) -> + (forall n : NZ, n <= z -> A n -> A (P n)) -> + 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 <- NZle_succ_l]. +unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); +[assumption | apply NZpred_succ]. +Qed. + +End Center. + +Theorem NZorder_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. +Proof (NZorder_induction 0). + +Theorem NZorder_induction'_0 : + A 0 -> + (forall n : NZ, 0 <= n -> A n -> A (S n)) -> + (forall n : NZ, n <= 0 -> A n -> A (P n)) -> + forall n : NZ, A n. +Proof (NZorder_induction' 0). + +(** 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. +Proof. +intros n H1 H2 m H3. +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 <= *) + +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. +Proof. +intros n H1 H2 m H3. +now apply NZright_induction with n. +Qed. + +End Induction. + +Tactic Notation "NZord_induct" ident(n) := + induction_maker n ltac:(apply NZorder_induction_0). + +Tactic Notation "NZord_induct" ident(n) constr(z) := + induction_maker n ltac:(apply NZorder_induction with z). + +Section WF. + +Variable z : NZ. + +Let Rlt (n m : NZ) := z <= n /\ n < m. +Let Rgt (n m : NZ) := m < n /\ n <= z. + +Add Morphism Rlt with signature NZeq ==> NZeq ==> iff as Rlt_wd. +Proof. +intros x1 x2 H1 x3 x4 H2; unfold Rlt; rewrite H1; now rewrite H2. +Qed. + +Add Morphism Rgt with signature NZeq ==> NZeq ==> iff as Rgt_wd. +Proof. +intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2. +Qed. + +Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc Rlt). +Proof. +unfold predicate_wd, fun_wd. +intros x1 x2 H; split; intro H1; destruct H1 as [H2]; +constructor; intros; apply H2; now (rewrite H || rewrite <- H). +Qed. + +Lemma NZAcc_gt_wd : predicate_wd NZeq (Acc Rgt). +Proof. +unfold predicate_wd, fun_wd. +intros x1 x2 H; split; intro H1; destruct H1 as [H2]; +constructor; intros; apply H2; now (rewrite H || rewrite <- H). +Qed. + +Theorem NZlt_wf : well_founded Rlt. +Proof. +unfold well_founded. +apply NZstrong_right_induction' with (z := z). +apply NZAcc_lt_wd. +intros n H; constructor; intros y [H1 H2]. +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. + +Theorem NZgt_wf : well_founded Rgt. +Proof. +unfold well_founded. +apply NZstrong_left_induction' with (z := z). +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 <- NZle_succ_l. +Qed. + +End WF. + +End NZOrderPropFunct. + |