NZAddOrder.v

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)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Import NZAxioms NZBase NZMul NZOrder.

Module Type NZAddOrderProp (Import NZ : NZOrdAxiomsSig').
Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ.

Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.forall n m p : t, n < m <-> p + n < p + m
Proof.forall n m p : t, n < m <-> p + n < p + m
  intros n m p; nzinduct p.n, m:t
n < m <-> 0 + n < 0 + m
n, m:t
forall n0 : t,
(n < m <-> n0 + n < n0 + m) <->
(n < m <-> S n0 + n < S n0 + m) -n, m:t
n < m <-> 0 + n < 0 + m now nzsimpl.
  -n, m:t
forall n0 : t,
(n < m <-> n0 + n < n0 + m) <->
(n < m <-> S n0 + n < S n0 + m) intro p.n, m, p:t
(n < m <-> p + n < p + m) <->
(n < m <-> S p + n < S p + m) nzsimpl.n, m, p:t
(n < m <-> p + n < p + m) <->
(n < m <-> S (p + n) < S (p + m)) now rewrite <- succ_lt_mono.
Qed.

Theorem add_lt_mono_r : forall n m p, n < m <-> n + p < m + p.forall n m p : t, n < m <-> n + p < m + p
Proof.forall n m p : t, n < m <-> n + p < m + p
intros n m p.n, m, p:t
n < m <-> n + p < m + p rewrite (add_comm n p), (add_comm m p); apply add_lt_mono_l.
Qed.

Theorem add_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.forall n m p q : t, n < m -> p < q -> n + p < m + q
Proof.forall n m p q : t, n < m -> p < q -> n + p < m + q
intros n m p q H1 H2.n, m, p, q:t
H1:n < m
H2:p < q
n + p < m + q
apply lt_trans with (m + p);
[now apply add_lt_mono_r | now apply add_lt_mono_l].
Qed.

Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.forall n m p : t, n <= m <-> p + n <= p + m
Proof.forall n m p : t, n <= m <-> p + n <= p + m
  intros n m p; nzinduct p.n, m:t
n <= m <-> 0 + n <= 0 + m
n, m:t
forall n0 : t,
(n <= m <-> n0 + n <= n0 + m) <->
(n <= m <-> S n0 + n <= S n0 + m) -n, m:t
n <= m <-> 0 + n <= 0 + m now nzsimpl.
  -n, m:t
forall n0 : t,
(n <= m <-> n0 + n <= n0 + m) <->
(n <= m <-> S n0 + n <= S n0 + m) intro p.n, m, p:t
(n <= m <-> p + n <= p + m) <->
(n <= m <-> S p + n <= S p + m) nzsimpl.n, m, p:t
(n <= m <-> p + n <= p + m) <->
(n <= m <-> S (p + n) <= S (p + m)) now rewrite <- succ_le_mono.
Qed.

Theorem add_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.forall n m p : t, n <= m <-> n + p <= m + p
Proof.forall n m p : t, n <= m <-> n + p <= m + p
intros n m p.n, m, p:t
n <= m <-> n + p <= m + p rewrite (add_comm n p), (add_comm m p); apply add_le_mono_l.
Qed.

Theorem add_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.forall n m p q : t, n <= m -> p <= q -> n + p <= m + q
Proof.forall n m p q : t, n <= m -> p <= q -> n + p <= m + q
intros n m p q H1 H2.n, m, p, q:t
H1:n <= m
H2:p <= q
n + p <= m + q
apply le_trans with (m + p);
[now apply add_le_mono_r | now apply add_le_mono_l].
Qed.

Theorem add_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.forall n m p q : t, n < m -> p <= q -> n + p < m + q
Proof.forall n m p q : t, n < m -> p <= q -> n + p < m + q
intros n m p q H1 H2.n, m, p, q:t
H1:n < m
H2:p <= q
n + p < m + q
apply lt_le_trans with (m + p);
[now apply add_lt_mono_r | now apply add_le_mono_l].
Qed.

Theorem add_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.forall n m p q : t, n <= m -> p < q -> n + p < m + q
Proof.forall n m p q : t, n <= m -> p < q -> n + p < m + q
intros n m p q H1 H2.n, m, p, q:t
H1:n <= m
H2:p < q
n + p < m + q
apply le_lt_trans with (m + p);
[now apply add_le_mono_r | now apply add_lt_mono_l].
Qed.

Theorem add_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n + m.forall n m : t, 0 < n -> 0 < m -> 0 < n + m
Proof.forall n m : t, 0 < n -> 0 < m -> 0 < n + m
intros n m H1 H2.n, m:t
H1:0 < n
H2:0 < m
0 < n + m rewrite <- (add_0_l 0).n, m:t
H1:0 < n
H2:0 < m
0 + 0 < n + m now apply add_lt_mono.
Qed.

Theorem add_pos_nonneg : forall n m, 0 < n -> 0 <= m -> 0 < n + m.forall n m : t, 0 < n -> 0 <= m -> 0 < n + m
Proof.forall n m : t, 0 < n -> 0 <= m -> 0 < n + m
intros n m H1 H2.n, m:t
H1:0 < n
H2:0 <= m
0 < n + m rewrite <- (add_0_l 0).n, m:t
H1:0 < n
H2:0 <= m
0 + 0 < n + m now apply add_lt_le_mono.
Qed.

Theorem add_nonneg_pos : forall n m, 0 <= n -> 0 < m -> 0 < n + m.forall n m : t, 0 <= n -> 0 < m -> 0 < n + m
Proof.forall n m : t, 0 <= n -> 0 < m -> 0 < n + m
intros n m H1 H2.n, m:t
H1:0 <= n
H2:0 < m
0 < n + m rewrite <- (add_0_l 0).n, m:t
H1:0 <= n
H2:0 < m
0 + 0 < n + m now apply add_le_lt_mono.
Qed.

Theorem add_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m.forall n m : t, 0 <= n -> 0 <= m -> 0 <= n + m
Proof.forall n m : t, 0 <= n -> 0 <= m -> 0 <= n + m
intros n m H1 H2.n, m:t
H1:0 <= n
H2:0 <= m
0 <= n + m rewrite <- (add_0_l 0).n, m:t
H1:0 <= n
H2:0 <= m
0 + 0 <= n + m now apply add_le_mono.
Qed.

Theorem lt_add_pos_l : forall n m, 0 < n -> m < n + m.forall n m : t, 0 < n -> m < n + m
Proof.forall n m : t, 0 < n -> m < n + m
intros n m.n, m:t
0 < n -> m < n + m rewrite (add_lt_mono_r 0 n m).n, m:t
0 + m < n + m -> m < n + m now nzsimpl.
Qed.

Theorem lt_add_pos_r : forall n m, 0 < n -> m < m + n.forall n m : t, 0 < n -> m < m + n
Proof.forall n m : t, 0 < n -> m < m + n
intros; rewrite add_comm; now apply lt_add_pos_l.
Qed.

Theorem le_lt_add_lt : forall n m p q, n <= m -> p + m < q + n -> p < q.forall n m p q : t, n <= m -> p + m < q + n -> p < q
Proof.forall n m p q : t, n <= m -> p + m < q + n -> p < q
intros n m p q H1 H2.n, m, p, q:t
H1:n <= m
H2:p + m < q + n
p < q destruct (le_gt_cases q p); [| assumption].n, m, p, q:t
H1:n <= m
H2:p + m < q + n
H:q <= p
p < q
contradict H2.n, m, p, q:t
H1:n <= m
H:q <= p
~ p + m < q + n rewrite nlt_ge.n, m, p, q:t
H1:n <= m
H:q <= p
q + n <= p + m now apply add_le_mono.
Qed.

Theorem lt_le_add_lt : forall n m p q, n < m -> p + m <= q + n -> p < q.forall n m p q : t, n < m -> p + m <= q + n -> p < q
Proof.forall n m p q : t, n < m -> p + m <= q + n -> p < q
intros n m p q H1 H2.n, m, p, q:t
H1:n < m
H2:p + m <= q + n
p < q destruct (le_gt_cases q p); [| assumption].n, m, p, q:t
H1:n < m
H2:p + m <= q + n
H:q <= p
p < q
contradict H2.n, m, p, q:t
H1:n < m
H:q <= p
~ p + m <= q + n rewrite nle_gt.n, m, p, q:t
H1:n < m
H:q <= p
q + n < p + m now apply add_le_lt_mono.
Qed.

Theorem le_le_add_le : forall n m p q, n <= m -> p + m <= q + n -> p <= q.forall n m p q : t, n <= m -> p + m <= q + n -> p <= q
Proof.forall n m p q : t, n <= m -> p + m <= q + n -> p <= q
intros n m p q H1 H2.n, m, p, q:t
H1:n <= m
H2:p + m <= q + n
p <= q destruct (le_gt_cases p q); [assumption |].n, m, p, q:t
H1:n <= m
H2:p + m <= q + n
H:q < p
p <= q
contradict H2.n, m, p, q:t
H1:n <= m
H:q < p
~ p + m <= q + n rewrite nle_gt.n, m, p, q:t
H1:n <= m
H:q < p
q + n < p + m now apply add_lt_le_mono.
Qed.

Theorem add_lt_cases : forall n m p q, n + m < p + q -> n < p \/ m < q.forall n m p q : t, n + m < p + q -> n < p \/ m < q
Proof.forall n m p q : t, n + m < p + q -> n < p \/ m < q
intros n m p q H;
destruct (le_gt_cases p n) as [H1 | H1]; [| now left].n, m, p, q:t
H:n + m < p + q
H1:p <= n
n < p \/ m < q
destruct (le_gt_cases q m) as [H2 | H2]; [| now right].n, m, p, q:t
H:n + m < p + q
H1:p <= n
H2:q <= m
n < p \/ m < q
contradict H; rewrite nlt_ge.n, m, p, q:t
H1:p <= n
H2:q <= m
p + q <= n + m now apply add_le_mono.
Qed.

Theorem add_le_cases : forall n m p q, n + m <= p + q -> n <= p \/ m <= q.forall n m p q : t, n + m <= p + q -> n <= p \/ m <= q
Proof.forall n m p q : t, n + m <= p + q -> n <= p \/ m <= q
intros n m p q H.n, m, p, q:t
H:n + m <= p + q
n <= p \/ m <= q
destruct (le_gt_cases n p) as [H1 | H1].n, m, p, q:t
H:n + m <= p + q
H1:n <= p
n <= p \/ m <= q
n, m, p, q:t
H:n + m <= p + q
H1:p < n
n <= p \/ m <= q -n, m, p, q:t
H:n + m <= p + q
H1:n <= p
n <= p \/ m <= q now left.
-n, m, p, q:t
H:n + m <= p + q
H1:p < n
n <= p \/ m <= q destruct (le_gt_cases m q) as [H2 | H2].n, m, p, q:t
H:n + m <= p + q
H1:p < n
H2:m <= q
n <= p \/ m <= q
n, m, p, q:t
H:n + m <= p + q
H1:p < n
H2:q < m
n <= p \/ m <= q +n, m, p, q:t
H:n + m <= p + q
H1:p < n
H2:m <= q
n <= p \/ m <= q now right.
  +n, m, p, q:t
H:n + m <= p + q
H1:p < n
H2:q < m
n <= p \/ m <= q contradict H; rewrite nle_gt.n, m, p, q:t
H1:p < n
H2:q < m
p + q < n + m now apply add_lt_mono.
Qed.

Theorem add_neg_cases : forall n m, n + m < 0 -> n < 0 \/ m < 0.forall n m : t, n + m < 0 -> n < 0 \/ m < 0
Proof.forall n m : t, n + m < 0 -> n < 0 \/ m < 0
intros n m H; apply add_lt_cases; now nzsimpl.
Qed.

Theorem add_pos_cases : forall n m, 0 < n + m -> 0 < n \/ 0 < m.forall n m : t, 0 < n + m -> 0 < n \/ 0 < m
Proof.forall n m : t, 0 < n + m -> 0 < n \/ 0 < m
intros n m H; apply add_lt_cases; now nzsimpl.
Qed.

Theorem add_nonpos_cases : forall n m, n + m <= 0 -> n <= 0 \/ m <= 0.forall n m : t, n + m <= 0 -> n <= 0 \/ m <= 0
Proof.forall n m : t, n + m <= 0 -> n <= 0 \/ m <= 0
intros n m H; apply add_le_cases; now nzsimpl.
Qed.

Theorem add_nonneg_cases : forall n m, 0 <= n + m -> 0 <= n \/ 0 <= m.forall n m : t, 0 <= n + m -> 0 <= n \/ 0 <= m
Proof.forall n m : t, 0 <= n + m -> 0 <= n \/ 0 <= m
intros n m H; apply add_le_cases; now nzsimpl.
Qed.

Subtraction

We can prove the existence of a subtraction of any number by a smaller one

Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p.forall n m : t,
n <= m -> exists p : t, m == p + n /\ 0 <= p
Proof.forall n m : t,
n <= m -> exists p : t, m == p + n /\ 0 <= p
  intros n m H.n, m:t
H:n <= m
exists p : t, m == p + n /\ 0 <= p apply le_ind with (4:=H).n, m:t
H:n <= m
Proper (eq ==> iff)
  (fun m0 : t => exists p : t, m0 == p + n /\ 0 <= p)
n, m:t
H:n <= m
exists p : t, n == p + n /\ 0 <= p
n, m:t
H:n <= m
forall m0 : t,
n <= m0 ->
(exists p : t, m0 == p + n /\ 0 <= p) ->
exists p : t, S m0 == p + n /\ 0 <= p -n, m:t
H:n <= m
Proper (eq ==> iff)
  (fun m0 : t => exists p : t, m0 == p + n /\ 0 <= p) solve_proper.
  -n, m:t
H:n <= m
exists p : t, n == p + n /\ 0 <= p exists 0; nzsimpl; split; order.
  -n, m:t
H:n <= m
forall m0 : t,
n <= m0 ->
(exists p : t, m0 == p + n /\ 0 <= p) ->
exists p : t, S m0 == p + n /\ 0 <= p clear m H.n:t
forall m : t,
n <= m ->
(exists p : t, m == p + n /\ 0 <= p) ->
exists p : t, S m == p + n /\ 0 <= p intros m H (p & EQ & LE).n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
exists p0 : t, S m == p0 + n /\ 0 <= p0 exists (S p).n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
S m == S p + n /\ 0 <= S p
    split.n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
S m == S p + n
n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
0 <= S p +n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
S m == S p + n nzsimpl.n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
S m == S (p + n) now f_equiv. +n, m:t
H:n <= m
p:t
EQ:m == p + n
LE:0 <= p
0 <= S p now apply le_le_succ_r.
Qed.

For the moment, it doesn't seem possible to relate this existing subtraction with sub.

End NZAddOrderProp.