Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import ZAxioms ZMulOrder GenericMinMax.

Properties of minimum and maximum specific to integer numbers

Module Type ZMaxMinProp (Import Z : ZAxiomsMiniSig').
Include ZMulOrderProp Z.

The following results are concrete instances of max_monotone and similar lemmas.

Succ

Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m).forall n m : t, S (max n m) == max (S n) (S m)
Proof.forall n m : t, S (max n m) == max (S n) (S m)
 intros.n, m:t
S (max n m) == max (S n) (S m) destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono.
Qed.

Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m).forall n m : t, S (min n m) == min (S n) (S m)
Proof.forall n m : t, S (min n m) == min (S n) (S m)
 intros.n, m:t
S (min n m) == min (S n) (S m) destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono.
Qed.

Pred

Lemma pred_max_distr : forall n m, P (max n m) == max (P n) (P m).forall n m : t, P (max n m) == max (P n) (P m)
Proof.forall n m : t, P (max n m) == max (P n) (P m)
 intros.n, m:t
P (max n m) == max (P n) (P m) destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?pred_le_mono.
Qed.

Lemma pred_min_distr : forall n m, P (min n m) == min (P n) (P m).forall n m : t, P (min n m) == min (P n) (P m)
Proof.forall n m : t, P (min n m) == min (P n) (P m)
 intros.n, m:t
P (min n m) == min (P n) (P m) destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?pred_le_mono.
Qed.

Add

Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m.forall n m p : t, max (p + n) (p + m) == p + max n m
Proof.forall n m p : t, max (p + n) (p + m) == p + max n m
 intros.n, m, p:t
max (p + n) (p + m) == p + max n m destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l.
Qed.

Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p.forall n m p : t, max (n + p) (m + p) == max n m + p
Proof.forall n m p : t, max (n + p) (m + p) == max n m + p
 intros.n, m, p:t
max (n + p) (m + p) == max n m + p destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r.
Qed.

Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m.forall n m p : t, min (p + n) (p + m) == p + min n m
Proof.forall n m p : t, min (p + n) (p + m) == p + min n m
 intros.n, m, p:t
min (p + n) (p + m) == p + min n m destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l.
Qed.

Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p.forall n m p : t, min (n + p) (m + p) == min n m + p
Proof.forall n m p : t, min (n + p) (m + p) == min n m + p
 intros.n, m, p:t
min (n + p) (m + p) == min n m + p destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r.
Qed.

Opp

Lemma opp_max_distr : forall n m, -(max n m) == min (-n) (-m).forall n m : t, - max n m == min (- n) (- m)
Proof.forall n m : t, - max n m == min (- n) (- m)
 intros.n, m:t
- max n m == min (- n) (- m) destruct (le_ge_cases n m).n, m:t
H:n <= m
- max n m == min (- n) (- m)
n, m:t
H:m <= n
- max n m == min (- n) (- m)
 rewrite max_r by trivial.n, m:t
H:n <= m
- m == min (- n) (- m)
n, m:t
H:m <= n
- max n m == min (- n) (- m) symmetry.n, m:t
H:n <= m
min (- n) (- m) == - m
n, m:t
H:m <= n
- max n m == min (- n) (- m) apply min_r.n, m:t
H:n <= m
- m <= - n
n, m:t
H:m <= n
- max n m == min (- n) (- m) now rewrite <- opp_le_mono.n, m:t
H:m <= n
- max n m == min (- n) (- m)
 rewrite max_l by trivial.n, m:t
H:m <= n
- n == min (- n) (- m) symmetry.n, m:t
H:m <= n
min (- n) (- m) == - n apply min_l.n, m:t
H:m <= n
- n <= - m now rewrite <- opp_le_mono.
Qed.

Lemma opp_min_distr : forall n m, -(min n m) == max (-n) (-m).forall n m : t, - min n m == max (- n) (- m)
Proof.forall n m : t, - min n m == max (- n) (- m)
 intros.n, m:t
- min n m == max (- n) (- m) destruct (le_ge_cases n m).n, m:t
H:n <= m
- min n m == max (- n) (- m)
n, m:t
H:m <= n
- min n m == max (- n) (- m)
 rewrite min_l by trivial.n, m:t
H:n <= m
- n == max (- n) (- m)
n, m:t
H:m <= n
- min n m == max (- n) (- m) symmetry.n, m:t
H:n <= m
max (- n) (- m) == - n
n, m:t
H:m <= n
- min n m == max (- n) (- m) apply max_l.n, m:t
H:n <= m
- m <= - n
n, m:t
H:m <= n
- min n m == max (- n) (- m) now rewrite <- opp_le_mono.n, m:t
H:m <= n
- min n m == max (- n) (- m)
 rewrite min_r by trivial.n, m:t
H:m <= n
- m == max (- n) (- m) symmetry.n, m:t
H:m <= n
max (- n) (- m) == - m apply max_r.n, m:t
H:m <= n
- n <= - m now rewrite <- opp_le_mono.
Qed.

Sub

Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m.forall n m p : t, max (p - n) (p - m) == p - min n m
Proof.forall n m p : t, max (p - n) (p - m) == p - min n m
 intros.n, m, p:t
max (p - n) (p - m) == p - min n m destruct (le_ge_cases n m).n, m, p:t
H:n <= m
max (p - n) (p - m) == p - min n m
n, m, p:t
H:m <= n
max (p - n) (p - m) == p - min n m
 rewrite min_l by trivial.n, m, p:t
H:n <= m
max (p - n) (p - m) == p - n
n, m, p:t
H:m <= n
max (p - n) (p - m) == p - min n m apply max_l.n, m, p:t
H:n <= m
p - m <= p - n
n, m, p:t
H:m <= n
max (p - n) (p - m) == p - min n m now rewrite <- sub_le_mono_l.n, m, p:t
H:m <= n
max (p - n) (p - m) == p - min n m
 rewrite min_r by trivial.n, m, p:t
H:m <= n
max (p - n) (p - m) == p - m apply max_r.n, m, p:t
H:m <= n
p - n <= p - m now rewrite <- sub_le_mono_l.
Qed.

Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p.forall n m p : t, max (n - p) (m - p) == max n m - p
Proof.forall n m p : t, max (n - p) (m - p) == max n m - p
 intros.n, m, p:t
max (n - p) (m - p) == max n m - p destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r.
Qed.

Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m.forall n m p : t, min (p - n) (p - m) == p - max n m
Proof.forall n m p : t, min (p - n) (p - m) == p - max n m
 intros.n, m, p:t
min (p - n) (p - m) == p - max n m destruct (le_ge_cases n m).n, m, p:t
H:n <= m
min (p - n) (p - m) == p - max n m
n, m, p:t
H:m <= n
min (p - n) (p - m) == p - max n m
 rewrite max_r by trivial.n, m, p:t
H:n <= m
min (p - n) (p - m) == p - m
n, m, p:t
H:m <= n
min (p - n) (p - m) == p - max n m apply min_r.n, m, p:t
H:n <= m
p - m <= p - n
n, m, p:t
H:m <= n
min (p - n) (p - m) == p - max n m now rewrite <- sub_le_mono_l.n, m, p:t
H:m <= n
min (p - n) (p - m) == p - max n m
 rewrite max_l by trivial.n, m, p:t
H:m <= n
min (p - n) (p - m) == p - n apply min_l.n, m, p:t
H:m <= n
p - n <= p - m now rewrite <- sub_le_mono_l.
Qed.

Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p.forall n m p : t, min (n - p) (m - p) == min n m - p
Proof.forall n m p : t, min (n - p) (m - p) == min n m - p
 intros.n, m, p:t
min (n - p) (m - p) == min n m - p destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r.
Qed.

Mul

Lemma mul_max_distr_nonneg_l : forall n m p, 0 <= p ->
 max (p * n) (p * m) == p * max n m.forall n m p : t,
0 <= p -> max (p * n) (p * m) == p * max n m
Proof.forall n m p : t,
0 <= p -> max (p * n) (p * m) == p * max n m
 intros.n, m, p:t
H:0 <= p
max (p * n) (p * m) == p * max n m destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l.
Qed.

Lemma mul_max_distr_nonneg_r : forall n m p, 0 <= p ->
 max (n * p) (m * p) == max n m * p.forall n m p : t,
0 <= p -> max (n * p) (m * p) == max n m * p
Proof.forall n m p : t,
0 <= p -> max (n * p) (m * p) == max n m * p
 intros.n, m, p:t
H:0 <= p
max (n * p) (m * p) == max n m * p destruct (le_ge_cases n m);
  [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_r.
Qed.

Lemma mul_min_distr_nonneg_l : forall n m p, 0 <= p ->
 min (p * n) (p * m) == p * min n m.forall n m p : t,
0 <= p -> min (p * n) (p * m) == p * min n m
Proof.forall n m p : t,
0 <= p -> min (p * n) (p * m) == p * min n m
 intros.n, m, p:t
H:0 <= p
min (p * n) (p * m) == p * min n m destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_l.
Qed.

Lemma mul_min_distr_nonneg_r : forall n m p, 0 <= p ->
 min (n * p) (m * p) == min n m * p.forall n m p : t,
0 <= p -> min (n * p) (m * p) == min n m * p
Proof.forall n m p : t,
0 <= p -> min (n * p) (m * p) == min n m * p
 intros.n, m, p:t
H:0 <= p
min (n * p) (m * p) == min n m * p destruct (le_ge_cases n m);
  [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_r.
Qed.

Lemma mul_max_distr_nonpos_l : forall n m p, p <= 0 ->
 max (p * n) (p * m) == p * min n m.forall n m p : t,
p <= 0 -> max (p * n) (p * m) == p * min n m
Proof.forall n m p : t,
p <= 0 -> max (p * n) (p * m) == p * min n m
 intros.n, m, p:t
H:p <= 0
max (p * n) (p * m) == p * min n m destruct (le_ge_cases n m).n, m, p:t
H:p <= 0
H0:n <= m
max (p * n) (p * m) == p * min n m
n, m, p:t
H:p <= 0
H0:m <= n
max (p * n) (p * m) == p * min n m
 rewrite min_l by trivial.n, m, p:t
H:p <= 0
H0:n <= m
max (p * n) (p * m) == p * n
n, m, p:t
H:p <= 0
H0:m <= n
max (p * n) (p * m) == p * min n m rewrite max_l.n, m, p:t
H:p <= 0
H0:n <= m
p * n == p * n
n, m, p:t
H:p <= 0
H0:n <= m
p * m <= p * n
n, m, p:t
H:p <= 0
H0:m <= n
max (p * n) (p * m) == p * min n m reflexivity.n, m, p:t
H:p <= 0
H0:n <= m
p * m <= p * n
n, m, p:t
H:p <= 0
H0:m <= n
max (p * n) (p * m) == p * min n m now apply mul_le_mono_nonpos_l.n, m, p:t
H:p <= 0
H0:m <= n
max (p * n) (p * m) == p * min n m
 rewrite min_r by trivial.n, m, p:t
H:p <= 0
H0:m <= n
max (p * n) (p * m) == p * m rewrite max_r.n, m, p:t
H:p <= 0
H0:m <= n
p * m == p * m
n, m, p:t
H:p <= 0
H0:m <= n
p * n <= p * m reflexivity.n, m, p:t
H:p <= 0
H0:m <= n
p * n <= p * m now apply mul_le_mono_nonpos_l.
Qed.

Lemma mul_max_distr_nonpos_r : forall n m p, p <= 0 ->
 max (n * p) (m * p) == min n m * p.forall n m p : t,
p <= 0 -> max (n * p) (m * p) == min n m * p
Proof.forall n m p : t,
p <= 0 -> max (n * p) (m * p) == min n m * p
 intros.n, m, p:t
H:p <= 0
max (n * p) (m * p) == min n m * p destruct (le_ge_cases n m).n, m, p:t
H:p <= 0
H0:n <= m
max (n * p) (m * p) == min n m * p
n, m, p:t
H:p <= 0
H0:m <= n
max (n * p) (m * p) == min n m * p
 rewrite min_l by trivial.n, m, p:t
H:p <= 0
H0:n <= m
max (n * p) (m * p) == n * p
n, m, p:t
H:p <= 0
H0:m <= n
max (n * p) (m * p) == min n m * p rewrite max_l.n, m, p:t
H:p <= 0
H0:n <= m
n * p == n * p
n, m, p:t
H:p <= 0
H0:n <= m
m * p <= n * p
n, m, p:t
H:p <= 0
H0:m <= n
max (n * p) (m * p) == min n m * p reflexivity.n, m, p:t
H:p <= 0
H0:n <= m
m * p <= n * p
n, m, p:t
H:p <= 0
H0:m <= n
max (n * p) (m * p) == min n m * p now apply mul_le_mono_nonpos_r.n, m, p:t
H:p <= 0
H0:m <= n
max (n * p) (m * p) == min n m * p
 rewrite min_r by trivial.n, m, p:t
H:p <= 0
H0:m <= n
max (n * p) (m * p) == m * p rewrite max_r.n, m, p:t
H:p <= 0
H0:m <= n
m * p == m * p
n, m, p:t
H:p <= 0
H0:m <= n
n * p <= m * p reflexivity.n, m, p:t
H:p <= 0
H0:m <= n
n * p <= m * p now apply mul_le_mono_nonpos_r.
Qed.

Lemma mul_min_distr_nonpos_l : forall n m p, p <= 0 ->
 min (p * n) (p * m) == p * max n m.forall n m p : t,
p <= 0 -> min (p * n) (p * m) == p * max n m
Proof.forall n m p : t,
p <= 0 -> min (p * n) (p * m) == p * max n m
 intros.n, m, p:t
H:p <= 0
min (p * n) (p * m) == p * max n m destruct (le_ge_cases n m).n, m, p:t
H:p <= 0
H0:n <= m
min (p * n) (p * m) == p * max n m
n, m, p:t
H:p <= 0
H0:m <= n
min (p * n) (p * m) == p * max n m
 rewrite max_r by trivial.n, m, p:t
H:p <= 0
H0:n <= m
min (p * n) (p * m) == p * m
n, m, p:t
H:p <= 0
H0:m <= n
min (p * n) (p * m) == p * max n m rewrite min_r.n, m, p:t
H:p <= 0
H0:n <= m
p * m == p * m
n, m, p:t
H:p <= 0
H0:n <= m
p * m <= p * n
n, m, p:t
H:p <= 0
H0:m <= n
min (p * n) (p * m) == p * max n m reflexivity.n, m, p:t
H:p <= 0
H0:n <= m
p * m <= p * n
n, m, p:t
H:p <= 0
H0:m <= n
min (p * n) (p * m) == p * max n m now apply mul_le_mono_nonpos_l.n, m, p:t
H:p <= 0
H0:m <= n
min (p * n) (p * m) == p * max n m
 rewrite max_l by trivial.n, m, p:t
H:p <= 0
H0:m <= n
min (p * n) (p * m) == p * n rewrite min_l.n, m, p:t
H:p <= 0
H0:m <= n
p * n == p * n
n, m, p:t
H:p <= 0
H0:m <= n
p * n <= p * m reflexivity.n, m, p:t
H:p <= 0
H0:m <= n
p * n <= p * m now apply mul_le_mono_nonpos_l.
Qed.

Lemma mul_min_distr_nonpos_r : forall n m p, p <= 0 ->
 min (n * p) (m * p) == max n m * p.forall n m p : t,
p <= 0 -> min (n * p) (m * p) == max n m * p
Proof.forall n m p : t,
p <= 0 -> min (n * p) (m * p) == max n m * p
 intros.n, m, p:t
H:p <= 0
min (n * p) (m * p) == max n m * p destruct (le_ge_cases n m).n, m, p:t
H:p <= 0
H0:n <= m
min (n * p) (m * p) == max n m * p
n, m, p:t
H:p <= 0
H0:m <= n
min (n * p) (m * p) == max n m * p
 rewrite max_r by trivial.n, m, p:t
H:p <= 0
H0:n <= m
min (n * p) (m * p) == m * p
n, m, p:t
H:p <= 0
H0:m <= n
min (n * p) (m * p) == max n m * p rewrite min_r.n, m, p:t
H:p <= 0
H0:n <= m
m * p == m * p
n, m, p:t
H:p <= 0
H0:n <= m
m * p <= n * p
n, m, p:t
H:p <= 0
H0:m <= n
min (n * p) (m * p) == max n m * p reflexivity.n, m, p:t
H:p <= 0
H0:n <= m
m * p <= n * p
n, m, p:t
H:p <= 0
H0:m <= n
min (n * p) (m * p) == max n m * p now apply mul_le_mono_nonpos_r.n, m, p:t
H:p <= 0
H0:m <= n
min (n * p) (m * p) == max n m * p
 rewrite max_l by trivial.n, m, p:t
H:p <= 0
H0:m <= n
min (n * p) (m * p) == n * p rewrite min_l.n, m, p:t
H:p <= 0
H0:m <= n
n * p == n * p
n, m, p:t
H:p <= 0
H0:m <= n
n * p <= m * p reflexivity.n, m, p:t
H:p <= 0
H0:m <= n
n * p <= m * p now apply mul_le_mono_nonpos_r.
Qed.

End ZMaxMinProp.