Library rt.util.nat
Require Import rt.util.tactics rt.util.ssromega.
(* Additional lemmas about natural numbers. *)
Section NatLemmas.
Lemma addnb (b1 b2 : bool) : (b1 + b2) != 0 = b1 || b2.
Lemma subh1 :
∀ m n p,
m ≥ n →
m - n + p = m + p - n.
Lemma subh2 :
∀ m1 m2 n1 n2,
m1 ≥ m2 →
n1 ≥ n2 →
(m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
Lemma subh3:
∀ m n p,
m + p ≤ n →
m ≤ n - p.
Lemma subh4:
∀ m n p,
m ≤ n →
p ≤ n →
(m == n - p) = (p == n - m).
(* Simplify n + a - b + b - a = n if n >= b. *)
Lemma subn_abba:
∀ n a b,
n ≥ b →
n + a - b + b - a = n.
Lemma addmovr:
∀ m n p,
m ≥ n →
(m - n = p ↔ m = p + n).
Lemma addmovl:
∀ m n p,
m ≥ n →
(p = m - n ↔ p + n = m).
Lemma ltSnm : ∀ n m, n.+1 < m → n < m.
Lemma min_lt_same :
∀ x y z,
minn x z < minn y z → x < y.
Lemma add_subC:
∀ a b c,
a ≥ c →
b ≥c →
a + (b - c ) = a - c + b.
Lemma ltn_subLR:
∀ a b c,
a - c < b →
a < b + c.
(* We can drop additive terms on the lesser side of an inequality. *)
Lemma leq_addk:
∀ m n k,
n + k ≤ m →
n ≤ m.
End NatLemmas.
Section Interval.
(* Trivially, points before the start of an interval, or past the end of an
interval, are not included in the interval. *)
Lemma point_not_in_interval:
∀ t1 t2 t',
t2 ≤ t' ∨ t' < t1 →
∀ t,
t1 ≤ t < t2
→ t ≠ t'.
End Interval.
Section NatOrderLemmas.
(* Mimic the way implicit arguments are used in ssreflect. *)
Set Implicit Arguments.
(* ltn_leq_trans: Establish that m < p if m < n and n <= p, to mirror the
lemma leq_ltn_trans in ssrnat.
NB: There is a good reason for this lemma to be "missing" in ssrnat --
since m < n is defined as m.+1 <= n, ltn_leq_trans is just
m.+1 <= n -> n <= p -> m.+1 <= p, that is (@leq_trans n m.+1 p).
Nonetheless we introduce it here because an additional (even though
arguably redundant) lemma doesn't hurt, and for newcomers the apparent
absence of the mirror case of leq_ltn_trans can be somewhat confusing. *)
Lemma ltn_leq_trans n m p : m < n → n ≤ p → m < p.
End NatOrderLemmas.
(* Additional lemmas about natural numbers. *)
Section NatLemmas.
Lemma addnb (b1 b2 : bool) : (b1 + b2) != 0 = b1 || b2.
Lemma subh1 :
∀ m n p,
m ≥ n →
m - n + p = m + p - n.
Lemma subh2 :
∀ m1 m2 n1 n2,
m1 ≥ m2 →
n1 ≥ n2 →
(m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
Lemma subh3:
∀ m n p,
m + p ≤ n →
m ≤ n - p.
Lemma subh4:
∀ m n p,
m ≤ n →
p ≤ n →
(m == n - p) = (p == n - m).
(* Simplify n + a - b + b - a = n if n >= b. *)
Lemma subn_abba:
∀ n a b,
n ≥ b →
n + a - b + b - a = n.
Lemma addmovr:
∀ m n p,
m ≥ n →
(m - n = p ↔ m = p + n).
Lemma addmovl:
∀ m n p,
m ≥ n →
(p = m - n ↔ p + n = m).
Lemma ltSnm : ∀ n m, n.+1 < m → n < m.
Lemma min_lt_same :
∀ x y z,
minn x z < minn y z → x < y.
Lemma add_subC:
∀ a b c,
a ≥ c →
b ≥c →
a + (b - c ) = a - c + b.
Lemma ltn_subLR:
∀ a b c,
a - c < b →
a < b + c.
(* We can drop additive terms on the lesser side of an inequality. *)
Lemma leq_addk:
∀ m n k,
n + k ≤ m →
n ≤ m.
End NatLemmas.
Section Interval.
(* Trivially, points before the start of an interval, or past the end of an
interval, are not included in the interval. *)
Lemma point_not_in_interval:
∀ t1 t2 t',
t2 ≤ t' ∨ t' < t1 →
∀ t,
t1 ≤ t < t2
→ t ≠ t'.
End Interval.
Section NatOrderLemmas.
(* Mimic the way implicit arguments are used in ssreflect. *)
Set Implicit Arguments.
(* ltn_leq_trans: Establish that m < p if m < n and n <= p, to mirror the
lemma leq_ltn_trans in ssrnat.
NB: There is a good reason for this lemma to be "missing" in ssrnat --
since m < n is defined as m.+1 <= n, ltn_leq_trans is just
m.+1 <= n -> n <= p -> m.+1 <= p, that is (@leq_trans n m.+1 p).
Nonetheless we introduce it here because an additional (even though
arguably redundant) lemma doesn't hurt, and for newcomers the apparent
absence of the mirror case of leq_ltn_trans can be somewhat confusing. *)
Lemma ltn_leq_trans n m p : m < n → n ≤ p → m < p.
End NatOrderLemmas.