Library Coq.Numbers.NatInt.NZOrder

Lemmas about orders for modules implementing NZOrdSig'

This file defines the NZOrderProp functor type, meant to be Included in a module implementing the NZOrdSig' module type.

It contains lemmas and tactics about le, lt and eq.

The firt part contains important basic lemmas about le and lt, for instance

succ_lt_mono, succ_le_mono, lt_succ_diag_r, le_succ_diag_r, ...
le_refl, le_antisymm, lt_asymm, le_trans, lt_trans, ...
decidability lemmas like le_gt_cases, eq_decidable, ...

It also adds the following tactics:

le_elim H to reason by cases on an hypothesis (H) : n <= m
the domain-agnostic order (see Coq.Structures.OrdersTac) and order' which knows that 0 < 1 < 2

The second part proves many induction principles involving the orders and defines the tactic notation nzord_induct.

From Coq.Numbers.NatInt Require Import NZAxioms NZBase.
From Coq.Logic Require Import Decidable.
From Coq.Structures Require Import OrdersTac.

Module Type NZOrderProp
(Import NZ : NZOrdSig')(Import NZBase : NZBaseProp NZ).

Basic facts about le, lt, eq and succ

Direct consequences of the specifications of lt and le

#[global]
Instance le_wd : Proper (eq ==>eq ==>iff) le.

Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H].

Theorem lt_le_incl : forall n m, n < m -> n <= m.

Theorem le_refl : forall n, n <= n.

Theorem lt_succ_diag_r : forall n, n < S n.

Theorem le_succ_diag_r : forall n, n <= S n.

Theorem neq_succ_diag_l : forall n, S n ~= n.

Theorem neq_succ_diag_r : forall n, n ~= S n.

Theorem nlt_succ_diag_l : forall n, ~ S n < n.

Theorem nle_succ_diag_l : forall n, ~ S n <= n.

Theorem le_succ_l : forall n m, S n <= m <-> n < m.

Trichotomy

Theorem le_gt_cases : forall n m, n <= m \/ n > m.

Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n.

Notation lt_eq_gt_cases := lt_trichotomy (only parsing).

Asymmetry and transitivity.

Theorem lt_asymm : forall n m, n < m -> ~ m < n.

Notation lt_ngt := lt_asymm (only parsing).

Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.

Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.

Some type classes about order

#[global]
Instance lt_strorder : StrictOrder lt.

#[global]
Instance le_preorder : PreOrder le.

#[global]
Instance le_partialorder : PartialOrder _ le.

Making the generic order tactic

Definition lt_compat := lt_wd.
Definition lt_total := lt_trichotomy.
Definition le_lteq := lt_eq_cases.

Module Private_OrderTac.
Module IsTotal.
Definition eq_equiv := eq_equiv.
Definition lt_strorder := lt_strorder.
Definition lt_compat := lt_compat.
Definition lt_total := lt_total.
Definition le_lteq := le_lteq.
End IsTotal.
Module Tac := !MakeOrderTac NZ IsTotal.
End Private_OrderTac.
Ltac order := Private_OrderTac.Tac.order.

Some direct consequences of order

Theorem lt_neq : forall n m, n < m -> n ~= m.

Theorem le_neq : forall n m, n < m <-> n <= m /\ n ~= m.

Theorem eq_le_incl : forall n m, n == m -> n <= m.

Lemma lt_stepl : forall x y z, x < y -> x == z -> z < y.

Lemma lt_stepr : forall x y z, x < y -> y == z -> x < z.

Lemma le_stepl : forall x y z, x <= y -> x == z -> z <= y.

Lemma le_stepr : forall x y z, x <= y -> y == z -> x <= z.

Declare Left Step lt_stepl.
Declare Right Step lt_stepr.
Declare Left Step le_stepl.
Declare Right Step le_stepr.

Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.

Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.

Theorem le_antisymm : forall n m, n <= m -> m <= n -> n == m.

More properties of < and <= with respect to S and 0

Theorem le_succ_r : forall n m, n <= S m <-> n <= m \/ n == S m.

Theorem lt_succ_l : forall n m, S n < m -> n < m.

Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.

Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.

Theorem succ_lt_mono : forall n m, n < m <-> S n < S m.

Theorem succ_le_mono : forall n m, n <= m <-> S n <= S m.

Theorem lt_0_1 : 0 < 1.

Theorem le_0_1 : 0 <= 1.

Theorem lt_1_2 : 1 < 2.

Theorem lt_0_2 : 0 < 2.

Theorem le_0_2 : 0 <= 2.

The order tactic enriched with some knowledge of 0,1,2

Ltac order' := generalize lt_0_1 lt_1_2; order.

Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.

More Trichotomy, decidability and double negation elimination

The following theorem is cleary redundant, but helps not to remember whether one has to say le_gt_cases or lt_ge_cases.

Theorem lt_ge_cases : forall n m, n < m \/ n >= m.

Theorem le_ge_cases : forall n m, n <= m \/ n >= m.

Theorem lt_gt_cases : forall n m, n ~= m <-> n < m \/ n > m.

Decidability of equality, even though true in each finite ring, does not have a uniform proof. Otherwise, the proof for two fixed numbers would reduce to a normal form that will say if the numbers are equal or not, which cannot be true in all finite rings. Therefore, we prove decidability in the presence of order.

Theorem eq_decidable : forall n m, decidable (n == m).

DNE stands for double-negation elimination.

Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m.

Theorem le_ngt : forall n m, n <= m <-> ~ n > m.

Redundant but useful

Theorem nlt_ge : forall n m, ~ n < m <-> n >= m.

Theorem lt_decidable : forall n m, decidable (n < m).

Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.

Theorem nle_gt : forall n m, ~ n <= m <-> n > m.

Redundant but useful

Theorem lt_nge : forall n m, n < m <-> ~ n >= m.

Theorem le_decidable : forall n m, decidable (n <= m).

Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m.

Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m.

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.

Theorem lt_exists_pred :
forall z n, z < n -> exists k , n == S k /\ z <= k.

Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n.

Order-based induction principles

Section WF.

Variable z : t.

Let Rlt (n m : t) := z <= n < m.
Let Rgt (n m : t) := m < n <= z.

Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt.

Instance Rgt_wd : Proper (eq ==> eq ==> iff) Rgt.

Theorem lt_wf : well_founded Rlt.

Theorem gt_wf : well_founded Rgt.

End WF.

Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step

Section Induction.

Variable A : t -> Prop.
Hypothesis A_wd : Proper (eq ==>iff) A.

Section Center.

Variable z : t.
Section RightInduction.

Let A' (n : t) := forall m, z <= m -> m < n -> A m.
Let right_step := forall n, z <= n -> A n -> A (S n).
Let right_step' := forall n, z <= n -> A' n -> A n.
Let right_step'' := forall n, A' n <-> A' (S n).

Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n.

Theorem right_induction : A z -> right_step -> forall n, z <= n -> A n.

Theorem right_induction' :
  (forall n, n <= z -> A n ) -> right_step -> forall n, A n.

Theorem strong_right_induction' :
  (forall n, n <= z -> A n ) -> right_step' -> forall n, A n.

End RightInduction.

Section LeftInduction.

Let A' (n : t) := forall m, m <= z -> n <= m -> A m.
Let left_step := forall n, n < z -> A (S n) -> A n.
Let left_step' := forall n, n <= z -> A' (S n) -> A n.
Let left_step'' := forall n, A' n <-> A' (S n).

Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.

Theorem left_induction : A z -> left_step -> forall n, n <= z -> A n.

Theorem left_induction' :
  (forall n, z <= n -> A n ) -> left_step -> forall n, A n.

Theorem strong_left_induction' :
  (forall n, z <= n -> A n ) -> left_step' -> forall n, A n.

End LeftInduction.

Theorem order_induction :
  A z ->
  (forall n, z <= n -> A n -> A (S n)) ->
  (forall n, n < z -> A (S n) -> A n ) ->
    forall n, A n.

Theorem order_induction' :
  A z ->
  (forall n, z <= n -> A n -> A (S n)) ->
  (forall n, n <= z -> A n -> A (P n)) ->
    forall n, A n.

End Center.

Theorem order_induction_0 :
  A 0 ->
  (forall n, 0 <= n -> A n -> A (S n)) ->
  (forall n, n < 0 -> A (S n) -> A n ) ->
    forall n, A n.

Theorem order_induction'_0 :
  A 0 ->
  (forall n, 0 <= n -> A n -> A (S n)) ->
  (forall n, n <= 0 -> A n -> A (P n)) ->
    forall n, A n.

Elimination principle for <

Theorem lt_ind : forall (n : t),
  A (S n) ->
  (forall m, n < m -> A m -> A (S m)) ->
   forall m, n < m -> A m.

Elimination principle for <=

Theorem le_ind : forall (n : t),
  A n ->
  (forall m, n <= m -> A m -> A (S m)) ->
   forall m, n <= m -> A m.

End Induction.

Tactic Notation "nzord_induct" ident(n) :=
  induction_maker n ltac:(apply order_induction_0).

Tactic Notation "nzord_induct" ident(n) constr(z) :=
  induction_maker n ltac:(apply order_induction with z).

Induction principles with respect to a measure

Section MeasureInduction.

Variable X : Type.
Variable f : X -> t.

Theorem measure_right_induction : forall (A : X -> Type) (z : t),
  (forall x, z <= f x -> (forall y, z <= f y < f x -> A y ) -> A x ) ->
  forall x, z <= f x -> A x.

Lemma measure_left_induction : forall (A : X -> Type) (z : t),
  (forall x, f x <= z -> (forall y, f x < f y <= z -> A y ) -> A x ) ->
  forall x, f x <= z -> A x.

End MeasureInduction.

End NZOrderProp.