Library prosa.util.nat
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Require Export mathcomp.zify.zify.
Require Export prosa.util.tactics.
Require Export mathcomp.zify.zify.
Require Export prosa.util.tactics.
Additional lemmas about natural numbers.
First, we show that, given m ≥ p and n ≥ q, an
expression (m + n) - (p + q) can be transformed into
expression (m - p) + (n - q).
Lemma subnACA m n p q : p ≤ m → q ≤ n →
(m + n) - (p + q) = (m - p) + (n - q).
Proof. by move⇒ plem qlen; rewrite subnDA addnBAC// addnBA// subnAC. Qed.
(m + n) - (p + q) = (m - p) + (n - q).
Proof. by move⇒ plem qlen; rewrite subnDA addnBAC// addnBA// subnAC. Qed.
Next, we show that m + p ≤ n implies that m ≤ n - p. Note
that this lemma is similar to ssreflect's lemma leq_subRL;
however, the current lemma has no precondition n ≤ p, since it
has only one direction.
Lemma leq_subRL_impl m n p : m + n ≤ p → n ≤ p - m.
Proof.
have [mlep|pltm] := leqP m p; first by rewrite leq_subRL.
by move⇒ /(leq_trans (ltn_addr _ pltm)); rewrite ltnn.
Qed.
Proof.
have [mlep|pltm] := leqP m p; first by rewrite leq_subRL.
by move⇒ /(leq_trans (ltn_addr _ pltm)); rewrite ltnn.
Qed.
Given constants a, b, c, z such that b ≤ a, if there is no
constant m such that a = b + m × c, then it holds that there
is no constant n such that a + z × c = b + n × c.
Lemma mul_add_neq a b c z :
b ≤ a →
(∀ m, a ≠ b + m × c) →
∀ n, a + z × c ≠ b + n × c.
Proof. move⇒ b_le_a + n ⇒ /(_ (n - z)); rewrite mulnBl; lia. Qed.
End NatLemmas.
b ≤ a →
(∀ m, a ≠ b + m × c) →
∀ n, a + z × c ≠ b + n × c.
Proof. move⇒ b_le_a + n ⇒ /(_ (n - z)); rewrite mulnBl; lia. Qed.
End NatLemmas.
In this section, we prove a lemma about intervals of natural
numbers.
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'.
Proof.
move⇒ excl t /[swap]→ /andP[t1_le_t' t'_lt_t2].
have [t2_le_t'|t'_lt_t1] := excl.
- by move: (leq_trans t'_lt_t2 t2_le_t'); rewrite ltnn.
- by move: (leq_ltn_trans t1_le_t' t'_lt_t1); rewrite ltnn.
Qed.
End Interval.
(* 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_deprecated [n m p] : m < n → n ≤ p → m < p.
Proof. exact: leq_trans. Qed.
#[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
Notation ltn_leq_trans := ltn_leq_trans_deprecated.
t2 ≤ t' ∨ t' < t1 →
∀ t,
t1 ≤ t < t2 →
t ≠ t'.
Proof.
move⇒ excl t /[swap]→ /andP[t1_le_t' t'_lt_t2].
have [t2_le_t'|t'_lt_t1] := excl.
- by move: (leq_trans t'_lt_t2 t2_le_t'); rewrite ltnn.
- by move: (leq_ltn_trans t1_le_t' t'_lt_t1); rewrite ltnn.
Qed.
End Interval.
(* 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_deprecated [n m p] : m < n → n ≤ p → m < p.
Proof. exact: leq_trans. Qed.
#[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
Notation ltn_leq_trans := ltn_leq_trans_deprecated.