summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zmax.v
blob: ae3bbf416bf479b56bd3290e3e2b2f78484fc421 (plain)
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
96
97
98
99
100
101
102
103
104
105
106
107
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.