1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** THIS FILE IS DEPRECATED. *)
Require Import BinInt Zcompare Zorder.
Local Open Scope Z_scope.
(** Definition [Zmin] is now [BinInt.Z.min]. *)
(** * Characterization of the minimum on binary integer numbers *)
Definition Zmin_case := Z.min_case.
Definition Zmin_case_strong := Z.min_case_strong.
Lemma Zmin_spec x y :
x <= y /\ Z.min x y = x \/ x > y /\ Z.min x y = y.
Proof.
Z.swap_greater. rewrite Z.min_comm. destruct (Z.min_spec y x); auto.
Qed.
(** * Greatest lower bound properties of min *)
Lemma Zle_min_l : forall n m, Z.min n m <= n. Proof Z.le_min_l.
Lemma Zle_min_r : forall n m, Z.min n m <= m. Proof Z.le_min_r.
Lemma Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Z.min n m.
Proof Z.min_glb.
Lemma Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Z.min n m.
Proof Z.min_glb_lt.
(** * Compatibility with order *)
Lemma Zle_min_compat_r : forall n m p, n <= m -> Z.min n p <= Z.min m p.
Proof Z.min_le_compat_r.
Lemma Zle_min_compat_l : forall n m p, n <= m -> Z.min p n <= Z.min p m.
Proof Z.min_le_compat_l.
(** * Semi-lattice properties of min *)
Lemma Zmin_idempotent : forall n, Z.min n n = n. Proof Z.min_id.
Notation Zmin_n_n := Z.min_id (only parsing).
Lemma Zmin_comm : forall n m, Z.min n m = Z.min m n. Proof Z.min_comm.
Lemma Zmin_assoc : forall n m p, Z.min n (Z.min m p) = Z.min (Z.min n m) p.
Proof Z.min_assoc.
(** * Additional properties of min *)
Lemma Zmin_irreducible_inf : forall n m, {Z.min n m = n} + {Z.min n m = m}.
Proof Z.min_dec.
Lemma Zmin_irreducible n m : Z.min n m = n \/ Z.min n m = m.
Proof. destruct (Z.min_dec n m); auto. Qed.
Notation Zmin_or := Zmin_irreducible (only parsing).
Lemma Zmin_le_prime_inf n m p : Z.min n m <= p -> {n <= p} + {m <= p}.
Proof. apply Zmin_case; auto. Qed.
(** * Operations preserving min *)
Lemma Zsucc_min_distr :
forall n m, Z.succ (Z.min n m) = Z.min (Z.succ n) (Z.succ m).
Proof Z.succ_min_distr.
Notation Zmin_SS := Z.succ_min_distr (only parsing).
Lemma Zplus_min_distr_r :
forall n m p, Z.min (n + p) (m + p) = Z.min n m + p.
Proof Z.add_min_distr_r.
Notation Zmin_plus := Z.add_min_distr_r (only parsing).
(** * Minimum and Zpos *)
Lemma Zpos_min p q : Zpos (Pos.min p q) = Z.min (Zpos p) (Zpos q).
Proof.
unfold Z.min, Pos.min; simpl. destruct Pos.compare; auto.
Qed.
Lemma Zpos_min_1 p : Z.min 1 (Zpos p) = 1.
Proof.
now destruct p.
Qed.
|
