Library Coq.NArith.Pminmax


Require Import Orders BinPos Pnat POrderedType GenericMinMax.

Maximum and Minimum of two positive numbers


Local Open Scope positive_scope.

The functions Pmax and Pmin implement indeed a maximum and a minimum

Lemma Pmax_l : forall x y, y<=x -> Pmax x y = x.

Lemma Pmax_r : forall x y, x<=y -> Pmax x y = y.

Lemma Pmin_l : forall x y, x<=y -> Pmin x y = x.

Lemma Pmin_r : forall x y, y<=x -> Pmin x y = y.

Module PositiveHasMinMax <: HasMinMax Positive_as_OT.
 Definition max := Pmax.
 Definition min := Pmin.
 Definition max_l := Pmax_l.
 Definition max_r := Pmax_r.
 Definition min_l := Pmin_l.
 Definition min_r := Pmin_r.
End PositiveHasMinMax.

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

Include UsualMinMaxProperties Positive_as_OT PositiveHasMinMax.

Properties specific to the positive domain


Simplifications

Lemma max_1_l : forall n, Pmax 1 n = n.

Lemma max_1_r : forall n, Pmax n 1 = n.

Lemma min_1_l : forall n, Pmin 1 n = 1.

Lemma min_1_r : forall n, Pmin n 1 = 1.

Compatibilities (consequences of monotonicity)

Lemma succ_max_distr :
 forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m).

Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m).

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

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

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

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

End P.