helm/matita/library/nat/minus.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16 set "baseuri" "cic:/matita/nat/minus".
  17
  18 include "nat/le_arith.ma".
  19 include "nat/compare.ma".
  20
  21 let rec minus n m \def
  22  match n with
  23  [ O \Rightarrow O
  24  | (S p) \Rightarrow
  25         match m with
  26         [O \Rightarrow (S p)
  27         | (S q) \Rightarrow minus p q ]].
  28
  29 (*CSC: the URI must disappear: there is a bug now *)
  30 interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
  31
  32 theorem minus_n_O: \forall n:nat.n=n-O.
  33 intros.elim n.simplify.reflexivity.
  34 simplify.reflexivity.
  35 qed.
  36
  37 theorem minus_n_n: \forall n:nat.O=n-n.
  38 intros.elim n.simplify.
  39 reflexivity.
  40 simplify.apply H.
  41 qed.
  42
  43 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
  44 intro.elim n.
  45 simplify.reflexivity.
  46 elim H.reflexivity.
  47 qed.
  48
  49 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
  50 intros 2.
  51 apply nat_elim2
  52 (\lambda n,m.m \leq n \to (S n)-m = S (n-m)).
  53 intros.apply le_n_O_elim n1 H.
  54 simplify.reflexivity.
  55 intros.simplify.reflexivity.
  56 intros.rewrite < H.reflexivity.
  57 apply le_S_S_to_le. assumption.
  58 qed.
  59
  60 theorem plus_minus:
  61 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
  62 intros 2.
  63 apply nat_elim2
  64 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m).
  65 intros.apply le_n_O_elim ? H.
  66 simplify.rewrite < minus_n_O.reflexivity.
  67 intros.simplify.reflexivity.
  68 intros.simplify.apply H.apply le_S_S_to_le.assumption.
  69 qed.
  70
  71 theorem plus_minus_m_m: \forall n,m:nat.
  72 m \leq n \to n = (n-m)+m.
  73 intros 2.
  74 apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m).
  75 intros.apply le_n_O_elim n1 H.
  76 reflexivity.
  77 intros.simplify.rewrite < plus_n_O.reflexivity.
  78 intros.simplify.rewrite < sym_plus.simplify.
  79 apply eq_f.rewrite < sym_plus.apply H.
  80 apply le_S_S_to_le.assumption.
  81 qed.
  82
  83 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
  84 n = m+p.
  85 intros.apply trans_eq ? ? ((n-m)+m) ?.
  86 apply plus_minus_m_m.
  87 apply H.elim H1.
  88 apply sym_plus.
  89 qed.
  90
  91 theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
  92 n = m+p \to n-m = p.
  93 intros.
  94 apply inj_plus_r m.
  95 rewrite < H1.
  96 rewrite < sym_plus.
  97 symmetry.
  98 apply plus_minus_m_m.assumption.
  99 qed.
 100
 101 theorem minus_S_S : \forall n,m:nat.
 102 eq nat (minus (S n) (S m)) (minus n m).
 103 intros.
 104 reflexivity.
 105 qed.
 106
 107 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
 108 eq nat (minus (pred n) (pred m)) (minus n m).
 109 intros.
 110 apply lt_O_n_elim n H.intro.
 111 apply lt_O_n_elim m H1.intro.
 112 simplify.reflexivity.
 113 qed.
 114
 115 theorem eq_minus_n_m_O: \forall n,m:nat.
 116 n \leq m \to n-m = O.
 117 intros 2.
 118 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 119 intros.simplify.reflexivity.
 120 intros.apply False_ind.
 121 (* ancora problemi con il not *)
 122 apply not_le_Sn_O n1 H.
 123 intros.
 124 simplify.apply H.apply le_S_S_to_le. apply H1.
 125 qed.
 126
 127 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 128 intros.elim H.elim minus_Sn_n n.apply le_n.
 129 rewrite > minus_Sn_m.
 130 apply le_S.assumption.
 131 apply lt_to_le.assumption.
 132 qed.
 133
 134 (*
 135 theorem le_plus_minus: \forall n,m,p. n+m \leq p \to n \leq p-m.
 136 intros 3.
 137 elim p.simplify.apply trans_le ? (n+m) ?.
 138 elim sym_plus ? ?.
 139 apply plus_le.assumption.
 140 apply le_n_Sm_elim ? ? H1.
 141 intros.
 142 *)
 143
 144 theorem distributive_times_minus: distributive nat times minus.
 145 simplify.
 146 intros.
 147 apply (leb_elim z y).intro.
 148 cut x*(y-z)+x*z = (x*y-x*z)+x*z.
 149 apply inj_plus_l (x*z).
 150 assumption.
 151 apply trans_eq nat ? (x*y).
 152 rewrite < times_plus_distr.
 153 rewrite < plus_minus_m_m ? ? H.reflexivity.
 154 rewrite < plus_minus_m_m ? ? ?.reflexivity.
 155 apply le_times_r.
 156 assumption.
 157 intro.
 158 rewrite > eq_minus_n_m_O.
 159 rewrite > eq_minus_n_m_O (x*y).
 160 rewrite < sym_times.simplify.reflexivity.
 161 apply lt_to_le.
 162 apply not_le_to_lt.assumption.
 163 apply le_times_r.apply lt_to_le.
 164 apply not_le_to_lt.assumption.
 165 qed.
 166
 167 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 168 \def distributive_times_minus.
 169
 170 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 171 intro.elim n.simplify.apply le_n.
 172 elim m.simplify.apply le_n.
 173 simplify.apply le_S.apply H.
 174 qed.