ZLt.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Export ZMul.

Module ZOrderProp (Import Z : ZAxiomsMiniSig').
Include ZMulProp Z.

Instances of earlier theorems for m == 0

Theorem neg_pos_cases : forall n, n ~= 0 <-> n < 0 \/ n > 0.forall n : t, n ~= 0 <-> n < 0 \/ 0 < n
Proof.forall n : t, n ~= 0 <-> n < 0 \/ 0 < n
intro; apply lt_gt_cases.
Qed.

Theorem nonpos_pos_cases : forall n, n <= 0 \/ n > 0.forall n : t, n <= 0 \/ 0 < n
Proof.forall n : t, n <= 0 \/ 0 < n
intro; apply le_gt_cases.
Qed.

Theorem neg_nonneg_cases : forall n, n < 0 \/ n >= 0.forall n : t, n < 0 \/ 0 <= n
Proof.forall n : t, n < 0 \/ 0 <= n
intro; apply lt_ge_cases.
Qed.

Theorem nonpos_nonneg_cases : forall n, n <= 0 \/ n >= 0.forall n : t, n <= 0 \/ 0 <= n
Proof.forall n : t, n <= 0 \/ 0 <= n
intro; apply le_ge_cases.
Qed.

Ltac zinduct n := induction_maker n ltac:(apply order_induction_0).

Theorems that are either not valid on N or have different proofs on N and Z

Theorem lt_pred_l : forall n, P n < n.forall n : t, P n < n
Proof.forall n : t, P n < n
intro n; rewrite <- (succ_pred n) at 2; apply lt_succ_diag_r.
Qed.

Theorem le_pred_l : forall n, P n <= n.forall n : t, P n <= n
Proof.forall n : t, P n <= n
intro; apply lt_le_incl; apply lt_pred_l.
Qed.

Theorem lt_le_pred : forall n m, n < m <-> n <= P m.forall n m : t, n < m <-> n <= P m
Proof.forall n m : t, n < m <-> n <= P m
intros n m; rewrite <- (succ_pred m); rewrite pred_succ.n, m:t
n < S (P m) <-> n <= P m apply lt_succ_r.
Qed.

Theorem nle_pred_r : forall n, ~ n <= P n.forall n : t, ~ n <= P n
Proof.forall n : t, ~ n <= P n
intro; rewrite <- lt_le_pred; apply lt_irrefl.
Qed.

Theorem lt_pred_le : forall n m, P n < m <-> n <= m.forall n m : t, P n < m <-> n <= m
Proof.forall n m : t, P n < m <-> n <= m
intros n m; rewrite <- (succ_pred n) at 2.n, m:t
P n < m <-> S (P n) <= m
symmetry; apply le_succ_l.
Qed.

Theorem lt_lt_pred : forall n m, n < m -> P n < m.forall n m : t, n < m -> P n < m
Proof.forall n m : t, n < m -> P n < m
intros; apply lt_pred_le; now apply lt_le_incl.
Qed.

Theorem le_le_pred : forall n m, n <= m -> P n <= m.forall n m : t, n <= m -> P n <= m
Proof.forall n m : t, n <= m -> P n <= m
intros; apply lt_le_incl; now apply lt_pred_le.
Qed.

Theorem lt_pred_lt : forall n m, n < P m -> n < m.forall n m : t, n < P m -> n < m
Proof.forall n m : t, n < P m -> n < m
intros n m H; apply lt_trans with (P m); [assumption | apply lt_pred_l].
Qed.

Theorem le_pred_lt : forall n m, n <= P m -> n <= m.forall n m : t, n <= P m -> n <= m
Proof.forall n m : t, n <= P m -> n <= m
intros; apply lt_le_incl; now apply lt_le_pred.
Qed.

Theorem pred_lt_mono : forall n m, n < m <-> P n < P m.forall n m : t, n < m <-> P n < P m
Proof.forall n m : t, n < m <-> P n < P m
intros; rewrite lt_le_pred; symmetry; apply lt_pred_le.
Qed.

Theorem pred_le_mono : forall n m, n <= m <-> P n <= P m.forall n m : t, n <= m <-> P n <= P m
Proof.forall n m : t, n <= m <-> P n <= P m
intros; rewrite <- lt_pred_le; now rewrite lt_le_pred.
Qed.

Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.forall n m : t, S n < m <-> n < P m
Proof.forall n m : t, S n < m <-> n < P m
intros n m; now rewrite (pred_lt_mono (S n) m), pred_succ.
Qed.

Theorem le_succ_le_pred : forall n m, S n <= m <-> n <= P m.forall n m : t, S n <= m <-> n <= P m
Proof.forall n m : t, S n <= m <-> n <= P m
intros n m; now rewrite (pred_le_mono (S n) m), pred_succ.
Qed.

Theorem lt_pred_lt_succ : forall n m, P n < m <-> n < S m.forall n m : t, P n < m <-> n < S m
Proof.forall n m : t, P n < m <-> n < S m
intros; rewrite lt_pred_le; symmetry; apply lt_succ_r.
Qed.

Theorem le_pred_lt_succ : forall n m, P n <= m <-> n <= S m.forall n m : t, P n <= m <-> n <= S m
Proof.forall n m : t, P n <= m <-> n <= S m
intros n m; now rewrite (pred_le_mono n (S m)), pred_succ.
Qed.

Theorem neq_pred_l : forall n, P n ~= n.forall n : t, P n ~= n
Proof.forall n : t, P n ~= n
intro; apply lt_neq; apply lt_pred_l.
Qed.

Theorem lt_m1_r : forall n m, n < m -> m < 0 -> n < -1.forall n m : t, n < m -> m < 0 -> n < -1
Proof.forall n m : t, n < m -> m < 0 -> n < -1
intros n m H1 H2.n, m:t
H1:n < m
H2:m < 0
n < -1 apply lt_le_pred in H2.n, m:t
H1:n < m
H2:m <= P 0
n < -1
setoid_replace (P 0) with (-1) in H2.n, m:t
H1:n < m
H2:m <= -1
n < -1
n, m:t
H1:n < m
H2:m <= P 0
P 0 == -1 now apply lt_le_trans with m.n, m:t
H1:n < m
H2:m <= P 0
P 0 == -1
apply eq_opp_r.n, m:t
H1:n < m
H2:m <= P 0
- P 0 == 1 now rewrite one_succ, opp_pred, opp_0.
Qed.

End ZOrderProp.