Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Require Export mathcomp.zify.zify. Require Export prosa.util.tactics. (** Additional lemmas about natural numbers. *) Section NatLemmas. (** 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)]. *)
m, n, p, q: nat

p <= m -> q <= n -> m + n - (p + q) = m - p + (n - q)
m, n, p, q: nat

p <= m -> q <= n -> m + n - (p + q) = m - p + (n - q)
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. *)
m, n, p: nat

m + n <= p -> n <= p - m
m, n, p: nat

m + n <= p -> n <= p - m
m, n, p: nat
pltm: p < m

m + n <= p -> n <= p - m
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]. *)
a, b, c, z: nat

b <= a -> (forall m : nat, a <> b + m * c) -> forall n : nat, a + z * c <> b + n * c
a, b, c, z: nat

b <= a -> (forall m : nat, a <> b + m * c) -> forall n : nat, a + z * c <> b + n * c
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. *) Section Interval. (** Trivially, points before the start of an interval, or past the end of an interval, are not included in the interval. *)
t1, t2, t': nat

t2 <= t' \/ t' < t1 -> forall t : nat, t1 <= t < t2 -> t <> t'
t1, t2, t': nat

t2 <= t' \/ t' < t1 -> forall t : nat, t1 <= t < t2 -> t <> t'
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2

False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t2_le_t': t2 <= t'

False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1
False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t2_le_t': t2 <= t'

False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1
False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1

False
t1, t2, t': nat
excl: t2 <= t' \/ t' < t1
t: nat
t1_le_t': t1 <= t'
t'_lt_t2: t' < t2
t'_lt_t1: t' < t1

False
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. *)
n, m, p: nat

m < n -> n <= p -> m < p
n, m, p: nat

m < n -> n <= p -> m < p
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.