Library prosa.util.nat

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.
  Proof. by ins; ssrlia. Qed.

  Lemma subh2:
     m1 m2 n1 n2,
      m1 m2
      n1 n2
      (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
  Proof. by ins; ssrlia. Qed.

  Lemma subh3:
     m n p,
      m + p n
      m n - p.
  Proof.
    clear.
    intros.
    rewrite <- leq_add2r with (p := p).
    rewrite subh1 //.
    - by rewrite -addnBA // subnn addn0.
    - by apply leq_trans with (m+p); first rewrite leq_addl.
  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.
  Proof.
    moven a b le_bn.
    rewrite subnK;
      first by rewrite -addnBA // subnn addn0 //.
    rewrite -[b]addn0.
    apply leq_trans with (n := n + 0); rewrite !addn0 //.
    apply leq_addr.
  Qed.

  Lemma add_subC:
     a b c,
      a c
      b c
      a + (b - c) = a - c + b.
  Proof.
    intros× AgeC BgeC.
    induction b;induction c;intros;try ssrlia.
  Qed.

  (* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
  Lemma ltn_subLR:
     a b c,
      a - c < b
      a < b + c.
  Proof.
    intros× AC. ssrlia.
  Qed.

  (* We can drop additive terms on the lesser side of an inequality. *)
  Lemma leq_addk:
     m n k,
      n + k m
      n m.
  Proof.
    movem n p.
    apply leq_trans.
    by apply leq_addr.
  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).
  Proof.
    movea b m.
    case: (leqP a m) ⇒ LE.
    { case: (boolP(b %| (m - a))) ⇒ DIV.
      { left; ((m - a) %/ b).
        now rewrite divnK // subnKC //. }
      { right. moven EQ.
        move: DIV ⇒ /negP DIV; apply DIV.
        rewrite EQ.
        rewrite -addnBAC // subnn add0n.
        apply dvdn_mull.
        now apply dvdnn. }}
    { right; moven EQ.
      move: LE; rewrite EQ.
      now 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:
     n1 n2 a b,
      n1 n2
      n2 × a + b = n1 × a + b + (n2 - n1) × a.
  Proof.
    intros × LT.
    rewrite mulnBl.
    rewrite addnBA; first by ssrlia.
    destruct a; first by ssrlia.
    now rewrite leq_pmul2r.
  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.
  Proof.
    intros × LTE NEQ n EQ.
    specialize (NEQ (n - z)).
    rewrite mulnBl in NEQ.
    now ssrlia.
  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'.
  Proof.
    movet1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ.
    subst.
    case EXCLUDED ⇒ [INEQ | INEQ];
      eapply leq_ltn_trans in INEQ; eauto;
      by rewrite ltnn in INEQ.
  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 nltn_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.
  Proof. exact (@leq_trans n m.+1 p). Qed.

End NatOrderLemmas.