products/Sources/formale Sprachen/Coq/theories/Numbers/Integer/Abstract image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ZLt.v   Sprache: Coq

Original von: Coq©

(************************************************************************)
(*         *   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.
Proof.
introapply lt_gt_cases.
Qed.

Theorem nonpos_pos_cases : forall n, n <= 0 \/ n > 0.
Proof.
introapply le_gt_cases.
Qed.

Theorem neg_nonneg_cases : forall n, n < 0 \/ n >= 0.
Proof.
introapply lt_ge_cases.
Qed.

Theorem nonpos_nonneg_cases : forall n, n <= 0 \/ n >= 0.
Proof.
introapply 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.
Proof.
intro n; rewrite <- (succ_pred n) at 2; apply lt_succ_diag_r.
Qed.

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

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

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

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

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

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

Theorem lt_pred_lt : forall n m, n < P m -> n < m.
Proof.
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.
Proof.
introsapply lt_le_incl; now apply lt_le_pred.
Qed.

Theorem pred_lt_mono : forall n m, n < m <-> P n < P m.
Proof.
introsrewrite lt_le_pred; symmetryapply lt_pred_le.
Qed.

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

Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.
Proof.
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.
Proof.
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.
Proof.
introsrewrite lt_pred_le; symmetryapply lt_succ_r.
Qed.

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

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

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

End ZOrderProp.


¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff