summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/BinInt.v6
-rw-r--r--theories/ZArith/Wf_Z.v60
-rw-r--r--theories/ZArith/ZArith.v2
-rw-r--r--theories/ZArith/ZArith_base.v6
-rw-r--r--theories/ZArith/ZArith_dec.v2
-rw-r--r--theories/ZArith/Zabs.v2
-rw-r--r--theories/ZArith/Zbinary.v2
-rw-r--r--theories/ZArith/Zbool.v4
-rw-r--r--theories/ZArith/Zcomplements.v2
-rw-r--r--theories/ZArith/Zdiv.v4
-rw-r--r--theories/ZArith/Zeven.v2
-rw-r--r--theories/ZArith/Zhints.v2
-rw-r--r--theories/ZArith/Zlogarithm.v3
-rw-r--r--theories/ZArith/Zmax.v108
-rw-r--r--theories/ZArith/Zmin.v112
-rw-r--r--theories/ZArith/Zminmax.v82
-rw-r--r--theories/ZArith/Zmisc.v2
-rw-r--r--theories/ZArith/Znat.v2
-rw-r--r--theories/ZArith/Znumtheory.v19
-rw-r--r--theories/ZArith/Zorder.v28
-rw-r--r--theories/ZArith/Zpower.v2
-rw-r--r--theories/ZArith/Zsqrt.v6
-rw-r--r--theories/ZArith/Zwf.v2
-rw-r--r--theories/ZArith/auxiliary.v2
24 files changed, 373 insertions, 89 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 11fa3872..02cf5f2d 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: BinInt.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
+(*i $Id: BinInt.v 6295 2004-11-12 16:40:39Z gregoire $ i*)
(***********************************************************)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
@@ -17,6 +17,8 @@ Require Export Pnat.
Require Import BinNat.
Require Import Plus.
Require Import Mult.
+
+Unset Boxed Definitions.
(**********************************************************************)
(** Binary integer numbers *)
@@ -1035,4 +1037,4 @@ Definition Zabs_N (z:Z) :=
Definition Z_of_N (x:N) := match x with
| N0 => Z0
| Npos p => Zpos p
- end. \ No newline at end of file
+ end.
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 069ddd42..af1fdd0b 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Wf_Z.v,v 1.20.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
+(*i $Id: Wf_Z.v 6984 2005-05-02 10:50:15Z herbelin $ i*)
Require Import BinInt.
Require Import Zcompare.
@@ -176,11 +176,11 @@ apply X; auto; unfold R in |- *; intuition; apply Zlt_pred.
intros; elim H; simpl in |- *; trivial.
Qed.
-(** A more general induction principal using [Zlt]. *)
+(** A more general induction principle on non-negative numbers using [Zlt]. *)
-Lemma Z_lt_rec :
+Lemma Zlt_0_rec :
forall P:Z -> Type,
- (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+ (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
forall x:Z, 0 <= x -> P x.
Proof.
intros P Hrec z; pattern z in |- *; apply (well_founded_induction_type R_wf).
@@ -189,10 +189,29 @@ apply Hrec; intros.
assert (H2 : 0 < 0).
apply Zle_lt_trans with y; intuition.
inversion H2.
+assumption.
firstorder.
unfold Zle, Zcompare in H; elim H; auto.
Defined.
+Lemma Zlt_0_ind :
+ forall P:Z -> Prop,
+ (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
+ forall x:Z, 0 <= x -> P x.
+Proof.
+exact Zlt_0_rec.
+Qed.
+
+(** Obsolete version of [Zlt] induction principle on non-negative numbers *)
+
+Lemma Z_lt_rec :
+ forall P:Z -> Type,
+ (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+ forall x:Z, 0 <= x -> P x.
+Proof.
+intros P Hrec; apply Zlt_0_rec; auto.
+Qed.
+
Lemma Z_lt_induction :
forall P:Z -> Prop,
(forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
@@ -201,4 +220,37 @@ Proof.
exact Z_lt_rec.
Qed.
+(** An even more general induction principle using [Zlt]. *)
+
+Lemma Zlt_lower_bound_rec :
+ forall P:Z -> Type, forall z:Z,
+ (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
+ forall x:Z, z <= x -> P x.
+Proof.
+intros P z Hrec x.
+assert (Hexpand : forall x, x = x - z + z).
+ intro; unfold Zminus; rewrite <- Zplus_assoc; rewrite Zplus_opp_l;
+ rewrite Zplus_0_r; trivial.
+intro Hz.
+rewrite (Hexpand x); pattern (x - z) in |- *; apply Zlt_0_rec.
+2: apply Zplus_le_reg_r with z; rewrite <- Hexpand; assumption.
+intros x0 Hlt_x0 H.
+apply Hrec.
+ 2: change z with (0+z); apply Zplus_le_compat_r; assumption.
+ intro y; rewrite (Hexpand y); intros.
+destruct H0.
+apply Hlt_x0.
+split.
+ apply Zplus_le_reg_r with z; assumption.
+ apply Zplus_lt_reg_r with z; assumption.
+Qed.
+
+Lemma Zlt_lower_bound_ind :
+ forall P:Z -> Prop, forall z:Z,
+ (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
+ forall x:Z, z <= x -> P x.
+Proof.
+exact Zlt_lower_bound_rec.
+Qed.
+
End Efficient_Rec.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 7e361621..45749fa3 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ZArith.v,v 1.5.2.2 2004/08/03 17:56:30 herbelin Exp $ i*)
+(*i $Id: ZArith.v 6013 2004-08-03 17:56:19Z herbelin $ i*)
(** Library for manipulating integers based on binary encoding *)
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 694e071e..20fd6b5f 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ZArith_base.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ *)
+(* $Id: ZArith_base.v 8032 2006-02-12 21:20:48Z herbelin $ *)
(** Library for manipulating integers based on binary encoding.
These are the basic modules, required by [Omega] and [Ring] for instance.
@@ -19,6 +19,8 @@ Require Export Zcompare.
Require Export Zorder.
Require Export Zeven.
Require Export Zmin.
+Require Export Zmax.
+Require Export Zminmax.
Require Export Zabs.
Require Export Znat.
Require Export auxiliary.
@@ -31,4 +33,4 @@ Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
Zmult_plus_distr_r: zarith.
-Require Export Zhints. \ No newline at end of file
+Require Export Zhints.
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index dbd0df6c..40c5860c 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ZArith_dec.v,v 1.11.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
+(*i $Id: ZArith_dec.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Sumbool.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 90e4c2a4..fed6ad76 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zabs.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zabs.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v
index fa5f00dc..353f0d5d 100644
--- a/theories/ZArith/Zbinary.v
+++ b/theories/ZArith/Zbinary.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zbinary.v,v 1.6.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zbinary.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Bit vectors interpreted as integers.
Contribution by Jean Duprat (ENS Lyon). *)
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index bb8abef4..a195b951 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Zbool.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ *)
+(* $Id: Zbool.v 6295 2004-11-12 16:40:39Z gregoire $ *)
Require Import BinInt.
Require Import Zeven.
@@ -15,6 +15,8 @@ Require Import Zcompare.
Require Import ZArith_dec.
Require Import Sumbool.
+Unset Boxed Definitions.
+
(** The decidability of equality and order relations over
type [Z] give some boolean functions with the adequate specification. *)
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index b60cd37c..817fbc1b 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zcomplements.v,v 1.26.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zcomplements.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import ZArithRing.
Require Import ZArith_base.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 84eb2259..e391d087 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zdiv.v 6295 2004-11-12 16:40:39Z gregoire $ i*)
(* Contribution by Claude Marché and Xavier Urbain *)
@@ -36,7 +36,7 @@ Open Local Scope Z_scope.
*)
-Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} :
+Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} :
Z * Z :=
match a with
| xH => if Zge_bool b 2 then (0, 1) else (1, 0)
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index a4a9abde..72d2d828 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zeven.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zeven.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import BinInt.
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index a9ee2c87..d0a2d2a0 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zhints.v,v 1.8.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zhints.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** This file centralizes the lemmas about [Z], classifying them
according to the way they can be used in automatic search *)
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index b575de88..653ee951 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zlogarithm.v,v 1.14.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zlogarithm.v 6295 2004-11-12 16:40:39Z gregoire $ i*)
(**********************************************************************)
(** The integer logarithms with base 2.
@@ -36,6 +36,7 @@ Fixpoint log_inf (p:positive) : Z :=
| xO q => Zsucc (log_inf q) (* 2n *)
| xI q => Zsucc (log_inf q) (* 2n+1 *)
end.
+
Fixpoint log_sup (p:positive) : Z :=
match p with
| xH => 0 (* 1 *)
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
new file mode 100644
index 00000000..ae3bbf41
--- /dev/null
+++ b/theories/ZArith/Zmax.v
@@ -0,0 +1,108 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(*i $Id: Zmax.v 8032 2006-02-12 21:20:48Z herbelin $ i*)
+
+Require Import Arith.
+Require Import BinInt.
+Require Import Zcompare.
+Require Import Zorder.
+
+Open Local Scope Z_scope.
+
+(**********************************************************************)
+(** *** Maximum of two binary integer numbers *)
+
+Definition Zmax m n :=
+ match m ?= n with
+ | Eq | Gt => m
+ | Lt => n
+ end.
+
+(** Characterization of maximum on binary integer numbers *)
+
+Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m).
+Proof.
+intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith.
+Qed.
+
+Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type),
+ (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m).
+Proof.
+intros n m P H1 H2; unfold Zmax, Zle, Zge in *.
+rewrite <- (Zcompare_antisym n m) in H1.
+destruct (n ?= m); (apply H1|| apply H2); discriminate.
+Qed.
+
+(** Least upper bound properties of max *)
+
+Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
+Proof.
+intros; apply Zmax_case_strong; auto with zarith.
+Qed.
+
+Notation Zmax1 := Zle_max_l (only parsing).
+
+Lemma Zle_max_r : forall n m:Z, m <= Zmax n m.
+Proof.
+intros; apply Zmax_case_strong; auto with zarith.
+Qed.
+
+Notation Zmax2 := Zle_max_r (only parsing).
+
+Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p.
+Proof.
+intros; apply Zmax_case; assumption.
+Qed.
+
+(** Semi-lattice properties of max *)
+
+Lemma Zmax_idempotent : forall n:Z, Zmax n n = n.
+Proof.
+intros; apply Zmax_case; auto.
+Qed.
+
+Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n.
+Proof.
+intros; do 2 apply Zmax_case_strong; intros;
+ apply Zle_antisym; auto with zarith.
+Qed.
+
+Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p.
+Proof.
+intros n m p; repeat apply Zmax_case_strong; intros;
+ reflexivity || (try apply Zle_antisym); eauto with zarith.
+Qed.
+
+(** Additional properties of max *)
+
+Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m.
+Proof.
+intros; apply Zmax_case; auto.
+Qed.
+
+Lemma Zmax_le_prime_inf : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m.
+Proof.
+intros n m p; apply Zmax_case; auto.
+Qed.
+
+(** Operations preserving max *)
+
+Lemma Zsucc_max_distr :
+ forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
+Proof.
+intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m);
+ elim_compare n m; intros E; rewrite E; auto with arith.
+Qed.
+
+Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p.
+Proof.
+intros x y n; unfold Zmax in |- *.
+rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
+ rewrite (Zcompare_plus_compat x y n).
+case (x ?= y); apply Zplus_comm.
+Qed.
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index d48e62c5..d79ebe98 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -5,9 +5,12 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zmin.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+(*i $Id: Zmin.v 8032 2006-02-12 21:20:48Z herbelin $ i*)
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
+ Further extensions by the Coq development team, with suggestions
+ from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
+ *)
Require Import Arith.
Require Import BinInt.
@@ -17,23 +20,31 @@ Require Import Zorder.
Open Local Scope Z_scope.
(**********************************************************************)
-(** Minimum on binary integer numbers *)
+(** *** Minimum on binary integer numbers *)
-Definition Zmin (n m:Z) :=
- match n ?= m return Z with
- | Eq => n
- | Lt => n
+Unboxed Definition Zmin (n m:Z) :=
+ match n ?= m with
+ | Eq | Lt => n
| Gt => m
end.
-(** Properties of minimum on binary integer numbers *)
+(** Characterization of the minimum on binary integer numbers *)
-Lemma Zmin_SS : forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
+Lemma Zmin_case_strong : forall (n m:Z) (P:Z -> Type),
+ (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m).
Proof.
-intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m);
- elim_compare n m; intros E; rewrite E; auto with arith.
+intros n m P H1 H2; unfold Zmin, Zle, Zge in *.
+rewrite <- (Zcompare_antisym n m) in H2.
+destruct (n ?= m); (apply H1|| apply H2); discriminate.
Qed.
+Lemma Zmin_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmin n m).
+Proof.
+intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
+Qed.
+
+(** Greatest lower bound properties of min *)
+
Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.
Proof.
intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E;
@@ -50,57 +61,70 @@ intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E;
| apply Zle_refl ].
Qed.
-Lemma Zmin_case : forall (n m:Z) (P:Z -> Set), P n -> P m -> P (Zmin n m).
+Lemma Zmin_glb : forall n m p:Z, p <= n -> p <= m -> p <= Zmin n m.
Proof.
-intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
+intros; apply Zmin_case; assumption.
Qed.
-Lemma Zmin_or : forall n m:Z, Zmin n m = n \/ Zmin n m = m.
+(** Semi-lattice properties of min *)
+
+Lemma Zmin_idempotent : forall n:Z, Zmin n n = n.
Proof.
-unfold Zmin in |- *; intros; elim (n ?= m); auto.
+unfold Zmin in |- *; intros; elim (n ?= n); auto.
Qed.
-Lemma Zmin_n_n : forall n:Z, Zmin n n = n.
+Notation Zmin_n_n := Zmin_idempotent (only parsing).
+
+Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n.
Proof.
-unfold Zmin in |- *; intros; elim (n ?= n); auto.
+intros n m; unfold Zmin.
+rewrite <- (Zcompare_antisym n m).
+assert (H:=Zcompare_Eq_eq n m).
+destruct (n ?= m); simpl; auto.
Qed.
-Lemma Zmin_plus : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p.
+Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (Zmin n m) p.
Proof.
-intros x y n; unfold Zmin in |- *.
-rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
- rewrite (Zcompare_plus_compat x y n).
-case (x ?= y); apply Zplus_comm.
+intros n m p; repeat apply Zmin_case_strong; intros;
+ reflexivity || (try apply Zle_antisym); eauto with zarith.
Qed.
-(**********************************************************************)
-(** Maximum of two binary integer numbers *)
+(** Additional properties of min *)
-Definition Zmax a b := match a ?= b with
- | Lt => b
- | _ => a
- end.
+Lemma Zmin_irreducible_inf : forall n m:Z, {Zmin n m = n} + {Zmin n m = m}.
+Proof.
+unfold Zmin in |- *; intros; elim (n ?= m); auto.
+Qed.
-(** Properties of maximum on binary integer numbers *)
+Lemma Zmin_irreducible : forall n m:Z, Zmin n m = n \/ Zmin n m = m.
+Proof.
+intros n m; destruct (Zmin_irreducible_inf n m); [left|right]; trivial.
+Qed.
-Ltac CaseEq name :=
- generalize (refl_equal name); pattern name at -1 in |- *; case name.
+Notation Zmin_or := Zmin_irreducible (only parsing).
-Theorem Zmax1 : forall a b, a <= Zmax a b.
+Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}.
Proof.
-intros a b; unfold Zmax in |- *; CaseEq (a ?= b); simpl in |- *;
- auto with zarith.
-unfold Zle in |- *; intros H; rewrite H; red in |- *; intros; discriminate.
+intros n m p; apply Zmin_case; auto.
Qed.
-Theorem Zmax2 : forall a b, b <= Zmax a b.
+(** Operations preserving min *)
+
+Lemma Zsucc_min_distr :
+ forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
-intros a b; unfold Zmax in |- *; CaseEq (a ?= b); simpl in |- *;
- auto with zarith.
-intros H;
- (case (Zle_or_lt b a); auto; unfold Zlt in |- *; rewrite H; intros;
- discriminate).
-intros H;
- (case (Zle_or_lt b a); auto; unfold Zlt in |- *; rewrite H; intros;
- discriminate).
+intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m);
+ elim_compare n m; intros E; rewrite E; auto with arith.
Qed.
+
+Notation Zmin_SS := Zsucc_min_distr (only parsing).
+
+Lemma Zplus_min_distr_r : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p.
+Proof.
+intros x y n; unfold Zmin in |- *.
+rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
+ rewrite (Zcompare_plus_compat x y n).
+case (x ?= y); apply Zplus_comm.
+Qed.
+
+Notation Zmin_plus := Zplus_min_distr_r (only parsing).
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
new file mode 100644
index 00000000..ebe9318e
--- /dev/null
+++ b/theories/ZArith/Zminmax.v
@@ -0,0 +1,82 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+(*i $Id: Zminmax.v 8034 2006-02-12 22:08:04Z herbelin $ i*)
+
+Require Import Zmin Zmax.
+Require Import BinInt Zorder.
+
+Open Local Scope Z_scope.
+
+(** *** Lattice properties of min and max on Z *)
+
+(** Absorption *)
+
+Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n.
+Proof.
+intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro;
+ reflexivity || apply Zle_antisym; trivial.
+Qed.
+
+Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n.
+Proof.
+intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro;
+ reflexivity || apply Zle_antisym; trivial.
+Qed.
+
+(** Distributivity *)
+
+Lemma Zmax_min_distr_r :
+ forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p).
+Proof.
+intros.
+repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+ reflexivity ||
+ apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+Lemma Zmin_max_distr_r :
+ forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p).
+Proof.
+intros.
+repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+ reflexivity ||
+ apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+(** Modularity *)
+
+Lemma Zmax_min_modular_r :
+ forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p).
+Proof.
+intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+ reflexivity ||
+ apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+Lemma Zmin_max_modular_r :
+ forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p).
+Proof.
+intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+ reflexivity ||
+ apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+(** Disassociativity *)
+
+Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p.
+Proof.
+intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+ apply Zle_refl || (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+
+
+
+
+
+
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index adcaf0ba..8246e324 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zmisc.v,v 1.20.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Zmisc.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import BinInt.
Require Import Zcompare.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index d051ed74..3e27878c 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Znat.v,v 1.3.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Znat.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 715cdc7d..a1963446 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Znumtheory.v,v 1.5.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Znumtheory.v 6984 2005-05-02 10:50:15Z herbelin $ i*)
Require Import ZArith_base.
Require Import ZArithRing.
@@ -278,12 +278,12 @@ Lemma euclid_rec :
(forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid.
Proof.
intros v3 Hv3; generalize Hv3; pattern v3 in |- *.
-apply Z_lt_rec.
+apply Zlt_0_rec.
clear v3 Hv3; intros.
elim (Z_zerop x); intro.
apply Euclid_intro with (u := u1) (v := u2) (d := u3).
assumption.
-apply H2.
+apply H3.
rewrite a0; auto with zarith.
set (q := u3 / x) in *.
assert (Hq : 0 <= u3 - q * x < x).
@@ -297,9 +297,9 @@ apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)).
tauto.
replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with
(u1 * a + u2 * b - q * (v1 * a + v2 * b)).
-rewrite H0; rewrite H1; trivial.
+rewrite H1; rewrite H2; trivial.
ring.
-intros; apply H2.
+intros; apply H3.
apply Zis_gcd_for_euclid with q; assumption.
assumption.
Qed.
@@ -377,11 +377,11 @@ Definition Zgcd_pos :
Proof.
intros a Ha.
apply
- (Z_lt_rec
+ (Zlt_0_rec
(fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}));
try assumption.
intro x; case x.
-intros _ b; exists (Zabs b).
+intros _ _ b; exists (Zabs b).
elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)).
intros H0; split.
apply Zabs_ind.
@@ -393,7 +393,7 @@ intros _ b; exists (Zabs b).
rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *.
split; [ apply Zis_gcd_0 | idtac ]; auto with zarith.
-intros p Hrec b.
+intros p Hrec _ b.
generalize (Z_div_mod b (Zpos p)).
case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
elim Hqr; clear Hqr; intros; auto with zarith.
@@ -405,8 +405,7 @@ split; auto.
rewrite H.
apply Zis_gcd_for_euclid2; auto.
-intros p Hrec b.
-exists 0; intros.
+intros p _ H b.
elim H; auto.
Defined.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 27eb02cd..b81cc580 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zorder.v,v 1.6.2.3 2005/03/29 15:35:12 herbelin Exp $ i*)
+(*i $Id: Zorder.v 6983 2005-05-02 10:47:51Z herbelin $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
@@ -905,23 +905,23 @@ Qed.
(** Simplification of square wrt order *)
Lemma Zgt_square_simpl :
- forall n m:Z, n >= 0 -> m >= 0 -> n * n > m * m -> n > m.
+ forall n m:Z, n >= 0 -> n * n > m * m -> n > m.
Proof.
-intros x y H0 H1 H2.
-case (dec_Zlt y x).
+intros n m H0 H1.
+case (dec_Zlt m n).
intro; apply Zlt_gt; trivial.
-intros H3; cut (y >= x).
+intros H2; cut (m >= n).
intros H.
-elim Zgt_not_le with (1 := H2).
+elim Zgt_not_le with (1 := H1).
apply Zge_le.
apply Zmult_ge_compat; auto.
apply Znot_lt_ge; trivial.
Qed.
Lemma Zlt_square_simpl :
- forall n m:Z, 0 <= n -> 0 <= m -> m * m < n * n -> m < n.
+ forall n m:Z, 0 <= n -> m * m < n * n -> m < n.
Proof.
-intros x y H0 H1 H2.
+intros x y H0 H1.
apply Zgt_lt.
apply Zgt_square_simpl; try apply Zle_ge; try apply Zlt_gt; assumption.
Qed.
@@ -967,5 +967,17 @@ intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l;
rewrite Zplus_comm; exact H.
Qed.
+Lemma Zle_0_minus_le : forall n m:Z, 0 <= n - m -> m <= n.
+Proof.
+intros n m H; apply Zplus_le_reg_l with (p := - m); rewrite Zplus_opp_l;
+ rewrite Zplus_comm; exact H.
+Qed.
+
+Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m.
+Proof.
+intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m);
+rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H.
+Qed.
+
(* For compatibility *)
Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index e5bf8b04..70a2bd45 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zpower.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Zpower.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import ZArith_base.
Require Import Omega.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 583c5828..cf4acb5f 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Zsqrt.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ *)
+(* $Id: Zsqrt.v 6199 2004-10-11 11:39:18Z herbelin $ *)
Require Import Omega.
Require Export ZArith_base.
@@ -22,12 +22,12 @@ Ltac compute_POS :=
match goal with
| |- context [(Zpos (xI ?X1))] =>
match constr:X1 with
- | context [1%positive] => fail
+ | context [1%positive] => fail 1
| _ => rewrite (BinInt.Zpos_xI X1)
end
| |- context [(Zpos (xO ?X1))] =>
match constr:X1 with
- | context [1%positive] => fail
+ | context [1%positive] => fail 1
| _ => rewrite (BinInt.Zpos_xO X1)
end
end.
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 8633986b..4ff663fb 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Zwf.v,v 1.7.2.1 2004/07/16 19:31:22 herbelin Exp $ *)
+(* $Id: Zwf.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Import ZArith_base.
Require Export Wf_nat.
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index ecd2daab..28cbd1e4 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auxiliary.v,v 1.12.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: auxiliary.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 11:04:11 +0000