Library Coq.Numbers.NatInt.NZOrder
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.
Theorem NZeq_le_incl : forall n m : NZ, n == m -> n <= m.
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_neq : forall n m : NZ, n < m -> n ~= m.
Theorem NZle_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m.
Theorem NZle_refl : forall n : NZ, n <= n.
Theorem NZlt_succ_diag_r : forall n : NZ, n < S n.
Theorem NZle_succ_diag_r : forall n : NZ, n <= S n.
Theorem NZlt_0_1 : 0 < 1.
Theorem NZle_0_1 : 0 <= 1.
Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m.
Theorem NZle_le_succ_r : forall n m : NZ, n <= m -> n <= S m.
Theorem NZle_succ_r : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
Theorem NZneq_succ_diag_l : forall n : NZ, S n ~= n.
Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n.
Theorem NZnlt_succ_diag_l : forall n : NZ, ~ S n < n.
Theorem NZnle_succ_diag_l : forall n : NZ, ~ S n <= n.
Theorem NZle_succ_l : forall n m : NZ, S n <= m <-> n < m.
Theorem NZlt_succ_l : 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_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.
Theorem NZlt_1_l : forall n m : NZ, 0 < n -> n < m -> 1 < m.
Trichotomy, decidability, and double negation elimination
Theorem NZlt_trichotomy : forall n m : NZ, n < m \/ n == m \/ m < n.
Theorem NZeq_dec : forall n m : NZ, decidable (n == m).
Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m.
Theorem NZlt_gt_cases : forall n m : NZ, n ~= m <-> n < m \/ n > m.
Theorem NZle_gt_cases : forall n m : NZ, n <= m \/ n > m.
Theorem NZlt_ge_cases : forall n m : NZ, n < m \/ n >= m.
Theorem NZle_ge_cases : forall n m : NZ, n <= m \/ n >= m.
Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m.
Theorem NZnlt_ge : forall n m : NZ, ~ n < m <-> n >= m.
Theorem NZlt_dec : forall n m : NZ, decidable (n < m).
Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
Theorem NZnle_gt : forall n m : NZ, ~ n <= m <-> n > m.
Theorem NZlt_nge : forall n m : NZ, n < m <-> ~ n >= m.
Theorem NZle_dec : forall n m : NZ, decidable (n <= m).
Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
Theorem NZnlt_succ_r : forall n m : NZ, ~ m < S n <-> n < m.
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
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.
Theorem NZneq_succ_iter_l :
forall (n : nat) (m : NZ), NZsucc_iter (Datatypes.S n) m ~= m.
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.
Section Center.
Variable z : NZ.
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'.
Lemma NZrs'_rs'' : right_step' -> right_step''.
Lemma NZrbase : A' z.
Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n.
Theorem NZstrong_right_induction: right_step' -> forall n : NZ, z <= n -> A n.
Theorem NZright_induction : A z -> right_step -> forall n : NZ, z <= n -> A n.
Theorem NZright_induction' :
(forall n : NZ, n <= z -> A n) -> right_step -> forall n : NZ, A n.
Theorem NZstrong_right_induction' :
(forall n : NZ, n <= z -> A n) -> right_step' -> forall n : NZ, A n.
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'.
Lemma NZls'_ls'' : left_step' -> left_step''.
Lemma NZlbase : A' (S z).
Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n.
Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n.
Theorem NZleft_induction : A z -> left_step -> forall n : NZ, n <= z -> A n.
Theorem NZleft_induction' :
(forall n : NZ, z <= n -> A n) -> left_step -> forall n : NZ, A n.
Theorem NZstrong_left_induction' :
(forall n : NZ, z <= n -> A n) -> left_step' -> forall n : NZ, A n.
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.
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.
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.
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.
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.
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.
Add Morphism Rgt with signature NZeq ==> NZeq ==> iff as Rgt_wd.
Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc Rlt).
Lemma NZAcc_gt_wd : predicate_wd NZeq (Acc Rgt).
Theorem NZlt_wf : well_founded Rlt.
Theorem NZgt_wf : well_founded Rgt.
End WF.
End NZOrderPropFunct.