nat.v 2.9 KB
Newer Older
1
Require Export 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 14 15 16 17 18

  Lemma subh2 :
    forall m1 m2 n1 n2,
      m1 >= m2 ->
      n1 >= n2 ->
      (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
  Proof. by ins; ssromega. Qed.
Sergey Bozhko's avatar
Sergey Bozhko committed
19
  
20
  Lemma subh3:
Sergey Bozhko's avatar
Sergey Bozhko committed
21 22 23 24 25 26
    forall m n p,
      m + p <= n ->
      m <= n - p.
  Proof.
    clear.
    intros.
27 28 29 30
    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
31 32
  Qed.

33
  (* Simplify [n + a - b + b - a = n] if [n >= b]. *)
34 35 36 37 38 39 40 41 42 43 44 45 46
  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
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
  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.
64

65 66 67 68 69 70 71 72 73 74 75
  (* 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.

76 77
End NatLemmas.

78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
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.

98 99
Section NatOrderLemmas.

100
  (* Mimic the way implicit arguments are used in [ssreflect]. *)
101 102 103
  Set Implicit Arguments.
  Unset Strict Implicit.

104 105
  (* [ltn_leq_trans]: Establish that [m < p] if [m < n] and [n <= p], to mirror the
     lemma [leq_ltn_trans] in [ssrnat].
106

107 108 109
     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].
110 111 112

     Nonetheless we introduce it here because an additional (even though
     arguably redundant) lemma doesn't hurt, and for newcomers the apparent
113
     absence of the mirror case of [leq_ltn_trans] can be somewhat confusing.  *)
114 115 116 117
  Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
  Proof. exact (@leq_trans n m.+1 p). Qed.

End NatOrderLemmas.