Library Coq.NArith.Nminmax


Require Import Orders BinNat Nnat NOrderedType GenericMinMax.

Maximum and Minimum of two N numbers


Local Open Scope N_scope.

The functions Nmax and Nmin implement indeed a maximum and a minimum

Lemma Nmax_l : forall x y, y<=x -> Nmax x y = x.

Lemma Nmax_r : forall x y, x<=y -> Nmax x y = y.

Lemma Nmin_l : forall x y, x<=y -> Nmin x y = x.

Lemma Nmin_r : forall x y, y<=x -> Nmin x y = y.

Module NHasMinMax <: HasMinMax N_as_OT.
 Definition max := Nmax.
 Definition min := Nmin.
 Definition max_l := Nmax_l.
 Definition max_r := Nmax_r.
 Definition min_l := Nmin_l.
 Definition min_r := Nmin_r.
End NHasMinMax.

Module N.

We obtain hence all the generic properties of max and min.

Include UsualMinMaxProperties N_as_OT NHasMinMax.

Properties specific to the positive domain


Simplifications

Lemma max_0_l : forall n, Nmax 0 n = n.

Lemma max_0_r : forall n, Nmax n 0 = n.

Lemma min_0_l : forall n, Nmin 0 n = 0.

Lemma min_0_r : forall n, Nmin n 0 = 0.

Compatibilities (consequences of monotonicity)

Lemma succ_max_distr :
 forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m).

Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m).

Lemma plus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m.

Lemma plus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p.

Lemma plus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m.

Lemma plus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p.

End N.