Library Coq.ZArith.Zmax


Require Import Arith_base.
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).

Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type),
  (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m).

Lemma Zmax_spec : forall x y:Z,
  x >= y /\ Zmax x y = x \/
  x < y /\ Zmax x y = y.

Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n.

Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m.

Least upper bound properties of max


Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.

Notation Zmax1 := Zle_max_l (only parsing).

Lemma Zle_max_r : forall n m:Z, m <= Zmax n m.

Notation Zmax2 := Zle_max_r (only parsing).

Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p.

Semi-lattice properties of max


Lemma Zmax_idempotent : forall n:Z, Zmax n n = n.

Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n.

Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p.

Additional properties of max


Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m.

Lemma Zmax_le_prime_inf : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m.

Operations preserving max


Lemma Zsucc_max_distr :
  forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).

Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p.

Maximum and Zpos


Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).

Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.

Characterization of Pminus in term of Zminus and Zmax


Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).