Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 390 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
deleted file mode 100644
index 9b452039cb..0000000000
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ /dev/null
@@ -1,390 +0,0 @@
-(************************************************************************)
-(*  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 i*)
-
-Require Export ZTimes.
-
-Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
-
-(* Axioms *)
-
-Theorem Zlt_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
-Proof NZlt_wd.
-
-Theorem Zle_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
-Proof NZle_wd.
-
-Theorem Zmin_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
-Proof NZmin_wd.
-
-Theorem Zmax_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
-Proof NZmax_wd.
-
-Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
-Proof NZle_lt_or_eq.
-
-Theorem Zlt_irrefl : forall n : Z, ~ n < n.
-Proof NZlt_irrefl.
-
-Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m.
-Proof NZlt_succ_le.
-
-Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
-Proof NZmin_l.
-
-Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
-Proof NZmin_r.
-
-Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
-Proof NZmax_l.
-
-Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
-Proof NZmax_r.
-
-(* Renaming theorems from NZOrder.v *)
-
-Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
-Proof NZlt_le_incl.
-
-Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
-Proof NZlt_neq.
-
-Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
-Proof NZlt_le_neq.
-
-Theorem Zle_refl : forall n : Z, n <= n.
-Proof NZle_refl.
-
-Theorem Zlt_succ_r : forall n : Z, n < S n.
-Proof NZlt_succ_r.
-
-Theorem Zle_succ_r : forall n : Z, n <= S n.
-Proof NZle_succ_r.
-
-Theorem Zlt_lt_succ : forall n m : Z, n < m -> n < S m.
-Proof NZlt_lt_succ.
-
-Theorem Zle_le_succ : forall n m : Z, n <= m -> n <= S m.
-Proof NZle_le_succ.
-
-Theorem Zle_succ_le_or_eq_succ : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
-Proof NZle_succ_le_or_eq_succ.
-
-Theorem Zneq_succ_l : forall n : Z, S n ~= n.
-Proof NZneq_succ_l.
-
-Theorem Znlt_succ_l : forall n : Z, ~ S n < n.
-Proof NZnlt_succ_l.
-
-Theorem Znle_succ_l : forall n : Z, ~ S n <= n.
-Proof NZnle_succ_l.
-
-Theorem Zlt_le_succ : forall n m : Z, n < m <-> S n <= m.
-Proof NZlt_le_succ.
-
-Theorem Zlt_succ_lt : forall n m : Z, S n < m -> n < m.
-Proof NZlt_succ_lt.
-
-Theorem Zle_succ_le : forall n m : Z, S n <= m -> n <= m.
-Proof NZle_succ_le.
-
-Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
-Proof NZsucc_lt_mono.
-
-Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m.
-Proof NZsucc_le_mono.
-
-Theorem Zlt_asymm : forall n m, n < m -> ~ m < n.
-Proof NZlt_asymm.
-
-Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
-Proof NZlt_trans.
-
-Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p.
-Proof NZle_trans.
-
-Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p.
-Proof NZle_lt_trans.
-
-Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p.
-Proof NZlt_le_trans.
-
-Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
-Proof NZle_antisymm.
-
-(** Trichotomy, decidability, and double negation elimination *)
-
-Theorem Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
-Proof NZlt_trichotomy.
-
-Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
-Proof NZlt_gt_cases.
-
-Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
-Proof NZle_gt_cases.
-
-Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
-Proof NZlt_ge_cases.
-
-Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
-Proof NZle_ge_cases.
-
-Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
-Proof NZle_ngt.
-
-Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
-Proof NZnlt_ge.
-
-Theorem Zlt_em : forall n m : Z, n < m \/ ~ n < m.
-Proof NZlt_em.
-
-Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
-Proof NZlt_dne.
-
-Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m.
-Proof NZnle_gt.
-
-Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
-Proof NZlt_nge.
-
-Theorem Zle_em : forall n m : Z, n <= m \/ ~ n <= m.
-Proof NZle_em.
-
-Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
-Proof NZle_dne.
-
-Theorem Zlt_nlt_succ : forall n m : Z, n < m <-> ~ m < S n.
-Proof NZlt_nlt_succ.
-
-Theorem Zlt_exists_pred :
-  forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
-Proof NZlt_exists_pred.
-
-Theorem Zlt_succ_iter_r :
-  forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m.
-Proof NZlt_succ_iter_r.
-
-Theorem Zneq_succ_iter_l :
-  forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m.
-Proof NZneq_succ_iter_l.
-
-(** Stronger variant of induction with assumptions n >= 0 (n < 0)
-in the induction step *)
-
-Theorem Zright_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z, A z ->
-      (forall n : Z, z <= n -> A n -> A (S n)) ->
-        forall n : Z, z <= n -> A n.
-Proof NZright_induction.
-
-Theorem Zleft_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z, A z ->
-      (forall n : Z, n < z -> A (S n) -> A n) ->
-        forall n : Z, n <= z -> A n.
-Proof NZleft_induction.
-
-Theorem Zright_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z,
-      (forall n : Z, n <= z -> A n) ->
-      (forall n : Z, z <= n -> A n -> A (S n)) ->
-        forall n : Z, A n.
-Proof NZright_induction'.
-
-Theorem Zleft_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z,
-    (forall n : Z, z <= n -> A n) ->
-    (forall n : Z, n < z -> A (S n) -> A n) ->
-      forall n : Z, A n.
-Proof NZleft_induction'.
-
-Theorem Zstrong_right_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z,
-    (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
-       forall n : Z, z <= n -> A n.
-Proof NZstrong_right_induction.
-
-Theorem Zstrong_left_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z,
-      (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
-        forall n : Z, n <= z -> A n.
-Proof NZstrong_left_induction.
-
-Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z,
-      (forall n : Z, n <= z -> A n) ->
-      (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
-        forall n : Z, A n.
-Proof NZstrong_right_induction'.
-
-Theorem Zstrong_left_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z,
-    (forall n : Z, z <= n -> A n) ->
-    (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
-      forall n : Z, A n.
-Proof NZstrong_left_induction'.
-
-Theorem Zorder_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z, A z ->
-    (forall n : Z, z <= n -> A n -> A (S n)) ->
-    (forall n : Z, n < z -> A (S n) -> A n) ->
-      forall n : Z, A n.
-Proof NZorder_induction.
-
-Theorem Zorder_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall z : Z, A z ->
-    (forall n : Z, z <= n -> A n -> A (S n)) ->
-    (forall n : Z, n <= z -> A n -> A (P n)) ->
-      forall n : Z, A n.
-Proof NZorder_induction'.
-
-Theorem Zorder_induction_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    A 0 ->
-    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
-    (forall n : Z, n < 0 -> A (S n) -> A n) ->
-      forall n : Z, A n.
-Proof NZorder_induction_0.
-
-Theorem Zorder_induction'_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    A 0 ->
-    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
-    (forall n : Z, n <= 0 -> A n -> A (P n)) ->
-      forall n : Z, A n.
-Proof NZorder_induction'_0.
-
-Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
-
-(** Elimintation principle for < *)
-
-Theorem Zlt_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall n : Z, A (S n) ->
-      (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
-Proof NZlt_ind.
-
-(** Elimintation principle for <= *)
-
-Theorem Zle_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
-    forall n : Z, A n ->
-      (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
-Proof NZle_ind.
-
-(** Well-founded relations *)
-
-Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m).
-Proof NZlt_wf.
-
-Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
-Proof NZgt_wf.
-
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
-
-Theorem Zlt_pred_l : forall n : Z, P n < n.
-Proof.
-intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_r.
-Qed.
-
-Theorem Zle_pred_l : forall n : Z, P n <= n.
-Proof.
-intro; le_less; apply Zlt_pred_l.
-Qed.
-
-Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m.
-Proof.
-intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_le.
-Qed.
-
-Theorem Znle_pred_r : forall n : Z, ~ n <= P n.
-Proof.
-intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl.
-Qed.
-
-Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m.
-Proof.
-intros n m; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n).
-apply Zlt_le_succ.
-Qed.
-
-Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
-Proof.
-intros; apply <- Zlt_pred_le; le_less.
-Qed.
-
-Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
-Proof.
-intros; le_less; now apply <- Zlt_pred_le.
-Qed.
-
-Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.
-Proof.
-intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l].
-Qed.
-
-Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m.
-Proof.
-intros; le_less; now apply <- Zlt_le_pred.
-Qed.
-
-Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.
-Proof.
-intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le.
-Qed.
-
-Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m.
-Proof.
-intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred.
-Qed.
-
-Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m.
-Proof.
-intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ.
-Qed.
-
-Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m.
-Proof.
-intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ.
-Qed.
-
-Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m.
-Proof.
-intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_le.
-Qed.
-
-Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m.
-Proof.
-intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_succ.
-Qed.
-
-Theorem Zneq_pred_l : forall n : Z, P n ~= n.
-Proof.
-intro; apply Zlt_neq; apply Zlt_pred_l.
-Qed.
-
-End ZOrderPropFunct.
-