nat.v

Require Export prosa.util.tactics prosa.util.ssrlia. From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

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]

(** Additional lemmas about natural numbers. *) Section NatLemmas. (** First, we show that, given [m1 >= m2] and [n1 >= n2], an expression [(m1 + n1) - (m2 + n2)] can be transformed into expression [(m1 - m2) + (n1 - n2)]. *) Lemma subnD: forall m1 m2 n1 n2, m1 >= m2 -> n1 >= n2 -> (m1 + n1) - (m2 + n2) = (m1 - m2) + (n1 - n2).

forall m1 m2 n1 n2 : nat, m2 <= m1 -> n2 <= n1 -> m1 + n1 - (m2 + n2) = m1 - m2 + (n1 - n2)

Proof.

forall m1 m2 n1 n2 : nat, m2 <= m1 -> n2 <= n1 -> m1 + n1 - (m2 + n2) = m1 - m2 + (n1 - n2)

by ins; ssrlia. 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: forall m n p, m + n <= p -> m <= p - n.

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

Proof.

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

by intros; ssrlia. Qed. (** Simplify [n + a - b + b - a = n] if [n >= b]. *) Lemma subn_abba: forall n a b, n >= b -> n + a - b + b - a = n.

forall n a b : nat, b <= n -> n + a - b + b - a = n

Proof.

forall n a b : nat, b <= n -> n + a - b + b - a = n

by intros; ssrlia. Qed. (** We can drop additive terms on the lesser side of an inequality. *) Lemma leq_addk: forall m n k, n + k <= m -> n <= m.

forall m n k : nat, n + k <= m -> n <= m

Proof.

forall m n k : nat, n + k <= m -> n <= m

by intros; ssrlia. Qed. (** For any numbers [a], [b], and [m], either there exists a number [n] such that [m = a + n * b] or [m <> a + n * b] for any [n]. *) Lemma exists_or_not_add_mul_cases: forall a b m, (exists n, m = a + n * b) \/ (forall n, m <> a + n * b).

forall a b m : nat, (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

Proof.

forall a b m : nat, (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

move=> a b m.

a, b, m: nat
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

case: (leqP a m) => LE.

a, b, m: nat
LE: a <= m
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

a, b, m: nat
LE: m < a
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

{

a, b, m: nat
LE: a <= m
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

case: (boolP(b %| (m - a))) => DIV; [left | right].

a, b, m: nat
LE: a <= m
DIV: b %| m - a
exists n : nat, m = a + n * b

a, b, m: nat
LE: a <= m
DIV: ~~ (b %| m - a)
forall n : nat, m <> a + n * b

{

a, b, m: nat
LE: a <= m
DIV: b %| m - a
exists n : nat, m = a + n * b

exists ((m - a) %/ b).

a, b, m: nat
LE: a <= m
DIV: b %| m - a
m = a + (m - a) %/ b * b

by rewrite divnK // subnKC //. }

a, b, m: nat
LE: a <= m
DIV: ~~ (b %| m - a)
forall n : nat, m <> a + n * b

{

a, b, m: nat
LE: a <= m
DIV: ~~ (b %| m - a)
forall n : nat, m <> a + n * b

move => n EQ.

a, b, m: nat
LE: a <= m
DIV: ~~ (b %| m - a)
n: nat
EQ: m = a + n * b
False

move: DIV => /negP DIV; apply DIV.

a, b, m: nat
LE: a <= m
n: nat
EQ: m = a + n * b
DIV: ~ b %| m - a
b %| m - a

rewrite EQ.

a, b, m: nat
LE: a <= m
n: nat
EQ: m = a + n * b
DIV: ~ b %| m - a
b %| a + n * b - a

rewrite -addnBAC // subnn add0n.

a, b, m: nat
LE: a <= m
n: nat
EQ: m = a + n * b
DIV: ~ b %| m - a
b %| n * b

apply dvdn_mull.

a, b, m: nat
LE: a <= m
n: nat
EQ: m = a + n * b
DIV: ~ b %| m - a
b %| b

by apply dvdnn. } }

a, b, m: nat
LE: m < a
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

{

a, b, m: nat
LE: m < a
(exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

right; move=> n EQ.

a, b, m: nat
LE: m < a
n: nat
EQ: m = a + n * b
False

move: LE; rewrite EQ.

a, b, m, n: nat
EQ: m = a + n * b
a + n * b < a -> False

by rewrite -ltn_subRL subnn //. } Qed. (** The expression [n2 * a + b] can be written as [n1 * a + b + (n2 - n1) * a] for any integer [n1] such that [n1 <= n2]. *) Lemma add_mul_diff: forall n1 n2 a b, n1 <= n2 -> n2 * a + b = n1 * a + b + (n2 - n1) * a.

forall n1 n2 a b : nat, n1 <= n2 -> n2 * a + b = n1 * a + b + (n2 - n1) * a

Proof.

forall n1 n2 a b : nat, n1 <= n2 -> n2 * a + b = n1 * a + b + (n2 - n1) * a

intros * LT.

n1, n2, a, b: nat
LT: n1 <= n2
n2 * a + b = n1 * a + b + (n2 - n1) * a

rewrite mulnBl.

n1, n2, a, b: nat
LT: n1 <= n2
n2 * a + b = n1 * a + b + (n2 * a - n1 * a)

rewrite addnBA; first by ssrlia.

n1, n2, a, b: nat
LT: n1 <= n2
n1 * a <= n2 * a

destruct a; first by ssrlia.

n1, n2, a, b: nat
LT: n1 <= n2
n1 * a.+1 <= n2 * a.+1

by rewrite leq_pmul2r. 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: forall a b c z, b <= a -> (forall m, a <> b + m * c) -> forall n, a + z * c <> b + n * c.

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

Proof.

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

intros * LTE NEQ n EQ.

a, b, c, z: nat
LTE: b <= a
NEQ: forall m : nat, a <> b + m * c
n: nat
EQ: a + z * c = b + n * c
False

specialize (NEQ (n - z)).

a, b, c, z: nat
LTE: b <= a
n: nat
NEQ: a <> b + (n - z) * c
EQ: a + z * c = b + n * c
False

rewrite mulnBl in NEQ.

a, b, c, z: nat
LTE: b <= a
n: nat
EQ: a + z * c = b + n * c
NEQ: a <> b + (n * c - z * c)
False

by ssrlia. 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. *) Lemma point_not_in_interval: forall t1 t2 t', t2 <= t' \/ t' < t1 -> forall t, t1 <= t < t2 -> t <> t'.

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

Proof.

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

move=> t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ; subst.

t1, t2, t': nat
EXCLUDED: t2 <= t' \/ t' < t1
LT_t2: t' < t2
GEQ_t1: t1 <= t'
False

by case EXCLUDED => [INEQ | INEQ]; eapply leq_ltn_trans in INEQ; eauto; rewrite ltnn in INEQ. Qed. End Interval. (** In the section, we introduce an additional lemma about relation [<] over natural numbers. *) Section NatOrderLemmas. (* Mimic the way implicit arguments are used in [ssreflect]. *) Set Implicit Arguments. Unset Strict Implicit. (* [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.

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

Proof.

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

exact (@leq_trans n m.+1 p). Qed. End NatOrderLemmas.