nat.v 2.72 KB
Newer Older
Xiaojie Guo's avatar
Xiaojie Guo committed
1
Require Import rt.util.tactics rt.util.ssromega.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
2
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
3 4 5 6 7 8 9 10 11

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

  Lemma subh1 :
    forall m n p,
      m >= n ->
      m - n + p = m + p - n.
  Proof. by ins; ssromega. Qed.
Sergey Bozhko's avatar
Sergey Bozhko committed
12
  
13
  Lemma subh3:
Sergey Bozhko's avatar
Sergey Bozhko committed
14 15 16 17 18 19
    forall m n p,
      m + p <= n ->
      m <= n - p.
  Proof.
    clear.
    intros.
20 21 22 23
    rewrite <- leq_add2r with (p := p).
    rewrite subh1 //.
    - by rewrite -addnBA // subnn addn0.
    - by apply leq_trans with (m+p); first rewrite leq_addl.
Sergey Bozhko's avatar
Sergey Bozhko committed
24 25
  Qed.

26 27 28 29 30 31 32 33 34 35 36 37 38 39
  (* 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.
  Proof.
    move=> n 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.

Xiaojie Guo's avatar
Xiaojie Guo committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  Lemma add_subC:
    forall a b c,
      a >= c ->
      b >=c ->
      a + (b - c ) = a - c + b.
  Proof.
    intros* AgeC BgeC.
    induction b;induction c;intros;try ssromega.
  Qed.

  Lemma ltn_subLR:
    forall a b c,
      a - c < b ->
      a < b + c.
  Proof.
    intros* AC. ssromega.
  Qed.
57

58 59 60 61 62 63 64 65 66 67 68
  (* We can drop additive terms on the lesser side of an inequality. *)
  Lemma leq_addk:
    forall m n k,
      n + k <= m ->
      n <= m.
  Proof.
    move=> m n p.
    apply leq_trans.
    by apply leq_addr.
  Qed.

69 70
End NatLemmas.

71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
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'.
  Proof.
    move=> t1 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.

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
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.
  Proof. exact (@leq_trans n m.+1 p). Qed.

End NatOrderLemmas.