Library prosa.util.nat


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


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

(* Additional lemmas about natural numbers. *)
Section NatLemmas.

  Lemma subh1:
     m n p,
      m n
      m - n + p = m + p - n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 20)
  
  ============================
  forall m n p : nat, n <= m -> m - n + p = m + p - n

----------------------------------------------------------------------------- *)


  Proof. by ins; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.

  Lemma subh2:
     m1 m2 n1 n2,
      m1 m2
      n1 n2
      (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 26)
  
  ============================
  forall m1 m2 n1 n2 : nat,
  m2 <= m1 -> n2 <= n1 -> m1 + n1 - (m2 + n2) = m1 - m2 + (n1 - n2)

----------------------------------------------------------------------------- *)


  Proof. by ins; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.

  Lemma subh3:
     m n p,
      m + p n
      m n - p.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 30)
  
  ============================
  forall m n p : nat, m + p <= n -> m <= n - p

----------------------------------------------------------------------------- *)


  Proof.
    clear.
    intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 34)
  
  m, n, p : nat
  H : m + p <= n
  ============================
  m <= n - p

----------------------------------------------------------------------------- *)


    rewrite <- leq_add2r with (p := p).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 35)
  
  m, n, p : nat
  H : m + p <= n
  ============================
  m + p <= n - p + p

----------------------------------------------------------------------------- *)


    rewrite subh1 //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 41)
  
  m, n, p : nat
  H : m + p <= n
  ============================
  m + p <= n + p - p

subgoal 2 (ID 42) is:
 p <= n

----------------------------------------------------------------------------- *)


    - by rewrite -addnBA // subnn addn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  m, n, p : nat
  H : m + p <= n
  ============================
  p <= n

----------------------------------------------------------------------------- *)


    - by apply leq_trans with (m+p); first rewrite leq_addl.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  (* Simplify [n + a - b + b - a = n] if [n >= b]. *)
  Lemma subn_abba:
     n a b,
      n b
      n + a - b + b - a = n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 35)
  
  ============================
  forall n a b : nat, b <= n -> n + a - b + b - a = n

----------------------------------------------------------------------------- *)


  Proof.
    moven a b le_bn.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 39)
  
  n, a, b : nat
  le_bn : b <= n
  ============================
  n + a - b + b - a = n

----------------------------------------------------------------------------- *)


    rewrite subnK;
      first by rewrite -addnBA // subnn addn0 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  n, a, b : nat
  le_bn : b <= n
  ============================
  b <= n + a

----------------------------------------------------------------------------- *)


    rewrite -[b]addn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 88)
  
  n, a, b : nat
  le_bn : b <= n
  ============================
  b + 0 <= n + a

----------------------------------------------------------------------------- *)


    apply leq_trans with (n := n + 0); rewrite !addn0 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  n, a, b : nat
  le_bn : b <= n
  ============================
  n <= n + a

----------------------------------------------------------------------------- *)


    apply leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  Lemma add_subC:
     a b c,
      a c
      b c
      a + (b - c) = a - c + b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  ============================
  forall a b c : nat, c <= a -> c <= b -> a + (b - c) = a - c + b

----------------------------------------------------------------------------- *)


  Proof.
    intros× AgeC BgeC.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  a, b, c : nat
  AgeC : c <= a
  BgeC : c <= b
  ============================
  a + (b - c) = a - c + b

----------------------------------------------------------------------------- *)


    induction b;induction c;intros;try ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  (* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
  Lemma ltn_subLR:
     a b c,
      a - c < b
      a < b + c.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  ============================
  forall a b c : nat, a - c < b -> a < b + c

----------------------------------------------------------------------------- *)


  Proof.
    intros× AC.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  a, b, c : nat
  AC : a - c < b
  ============================
  a < b + c

----------------------------------------------------------------------------- *)


ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

  (* We can drop additive terms on the lesser side of an inequality. *)
  Lemma leq_addk:
     m n k,
      n + k m
      n m.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  ============================
  forall m n k : nat, n + k <= m -> n <= m

----------------------------------------------------------------------------- *)


  Proof.
    movem n p.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  m, n, p : nat
  ============================
  n + p <= m -> n <= m

----------------------------------------------------------------------------- *)


    apply leq_trans.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  m, n, p : nat
  ============================
  n <= n + p

----------------------------------------------------------------------------- *)


    by apply leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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:
     a b m,
      ( n, m = a + n × b)
      ( n, m a + n × b).

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


  Proof.
    movea b m.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


    case: (leqP a m) ⇒ LE.

(* ----------------------------------[ coqtop ]---------------------------------

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

subgoal 2 (ID 78) is:
 (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 89)
  
  a, b, m : nat
  LE : a <= m
  DIV : b %| m - a
  ============================
  (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

subgoal 2 (ID 90) is:
 (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  a, b, m : nat
  LE : a <= m
  DIV : b %| m - a
  ============================
  (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


left; ((m - a) %/ b).

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


        now rewrite divnK // subnKC //.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 90) is:
 (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)
subgoal 2 (ID 78) is:
 (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 90)
  
  a, b, m : nat
  LE : a <= m
  DIV : ~~ (b %| m - a)
  ============================
  (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 90)
  
  a, b, m : nat
  LE : a <= m
  DIV : ~~ (b %| m - a)
  ============================
  (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


right.
(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


moven EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


        rewrite EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 162)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


        apply dvdn_mull.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


        now apply dvdnn.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 78) is:
 (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


}
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 78) is:
 (exists n : nat, m = a + n * b) \/ (forall n : nat, m <> a + n * b)

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


right; moven EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 207)
  
  a, b, m : nat
  LE : m < a
  n : nat
  EQ : m = a + n * b
  ============================
  False

----------------------------------------------------------------------------- *)


      move: LE; rewrite EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 211)
  
  a, b, m, n : nat
  EQ : m = a + n * b
  ============================
  a + n * b < a -> False

----------------------------------------------------------------------------- *)


      now rewrite -ltn_subRL subnn //.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  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:
     n1 n2 a b,
      n1 n2
      n2 × a + b = n1 × a + b + (n2 - n1) × a.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)


  Proof.
    intros × LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  n1, n2, a, b : nat
  LT : n1 <= n2
  ============================
  n2 * a + b = n1 * a + b + (n2 - n1) * a

----------------------------------------------------------------------------- *)


    rewrite mulnBl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  n1, n2, a, b : nat
  LT : n1 <= n2
  ============================
  n2 * a + b = n1 * a + b + (n2 * a - n1 * a)

----------------------------------------------------------------------------- *)


    rewrite addnBA; first by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  n1, n2, a, b : nat
  LT : n1 <= n2
  ============================
  n1 * a <= n2 * a

----------------------------------------------------------------------------- *)


    destruct a; first by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 229)
  
  n1, n2, a, b : nat
  LT : n1 <= n2
  ============================
  n1 * a.+1 <= n2 * a.+1

----------------------------------------------------------------------------- *)


    now rewrite leq_pmul2r.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

Given constants [a, b, c, z] such that [b <= a] and there is no constant [m] such that [a = b + m * c], 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 73)
  
  ============================
  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.
    intros × LTE NEQ n EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 82)
  
  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)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 107)
  
  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

----------------------------------------------------------------------------- *)


    now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

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'.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 21)
  
  ============================
  forall t1 t2 t' : nat,
  t2 <= t' \/ t' < t1 -> forall t : nat, t1 <= t < t2 -> t <> t'

----------------------------------------------------------------------------- *)


  Proof.
    movet1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 67)
  
  t1, t2, t' : nat
  EXCLUDED : t2 <= t' \/ t' < t1
  t : nat
  GEQ_t1 : t1 <= t
  LT_t2 : t < t2
  EQ : t = t'
  ============================
  False

----------------------------------------------------------------------------- *)


    subst.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 75)
  
  t1, t2, t' : nat
  EXCLUDED : t2 <= t' \/ t' < t1
  LT_t2 : t' < t2
  GEQ_t1 : t1 <= t'
  ============================
  False

----------------------------------------------------------------------------- *)


    case EXCLUDED ⇒ [INEQ | INEQ];
      eapply leq_ltn_trans in INEQ; eauto;
      by rewrite ltnn in INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End Interval.

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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 22)
  
  n, m, p : nat
  ============================
  m < n -> n <= p -> m < p

----------------------------------------------------------------------------- *)


  Proof. exact (@leq_trans n m.+1 p).
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


Qed.

End NatOrderLemmas.