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.