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/orders_op.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
  30 theorem minus_n_O: \forall n:nat.eq nat n (minus n O).
  31 intros.elim n.simplify.reflexivity.
  32 simplify.reflexivity.
  33 qed.
  34
  35 theorem minus_n_n: \forall n:nat.eq nat O (minus n n).
  36 intros.elim n.simplify.
  37 reflexivity.
  38 simplify.apply H.
  39 qed.
  40
  41 theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n).
  42 intro.elim n.
  43 simplify.reflexivity.
  44 elim H.reflexivity.
  45 qed.
  46
  47 theorem minus_Sn_m: \forall n,m:nat.
  48 le m n \to eq nat (minus (S n) m) (S (minus n m)).
  49 intros 2.
  50 apply nat_elim2
  51 (\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))).
  52 intros.apply le_n_O_elim n1 H.
  53 simplify.reflexivity.
  54 intros.simplify.reflexivity.
  55 intros.rewrite < H.reflexivity.
  56 apply le_S_S_to_le. assumption.
  57 qed.
  58
  59 theorem plus_minus:
  60 \forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m).
  61 intros 2.
  62 apply nat_elim2
  63 (\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)).
  64 intros.apply le_n_O_elim ? H.
  65 simplify.rewrite < minus_n_O.reflexivity.
  66 intros.simplify.reflexivity.
  67 intros.simplify.apply H.apply le_S_S_to_le.assumption.
  68 qed.
  69
  70 theorem plus_minus_m_m: \forall n,m:nat.
  71 le m n \to eq nat n (plus (minus n m) m).
  72 intros 2.
  73 apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)).
  74 intros.apply le_n_O_elim n1 H.
  75 reflexivity.
  76 intros.simplify.rewrite < plus_n_O.reflexivity.
  77 intros.simplify.rewrite < sym_plus.simplify.
  78 apply eq_f.rewrite < sym_plus.apply H.
  79 apply le_S_S_to_le.assumption.
  80 qed.
  81
  82 theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to
  83 eq nat n (plus m p).
  84 intros.apply trans_eq ? ? (plus (minus n m) m) ?.
  85 apply plus_minus_m_m.
  86 apply H.elim H1.
  87 apply sym_plus.
  88 qed.
  89
  90 theorem plus_to_minus :\forall n,m,p:nat.le m n \to
  91 eq nat n (plus m p) \to eq nat (minus n m) p.
  92 intros.
  93 apply inj_plus_r m.
  94 rewrite < H1.
  95 rewrite < sym_plus.
  96 symmetry.
  97 apply plus_minus_m_m.assumption.
  98 qed.
  99
 100 theorem eq_minus_n_m_O: \forall n,m:nat.
 101 le n m \to eq nat (minus n m) O.
 102 intros 2.
 103 apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
 104 intros.simplify.reflexivity.
 105 intros.apply False_ind.
 106 (* ancora problemi con il not *)
 107 apply not_le_Sn_O n1 H.
 108 intros.
 109 simplify.apply H.apply le_S_S_to_le. apply H1.
 110 qed.
 111
 112 theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
 113 intros.elim H.elim minus_Sn_n n.apply le_n.
 114 rewrite > minus_Sn_m.
 115 apply le_S.assumption.
 116 apply lt_to_le.assumption.
 117 qed.
 118
 119 (*
 120 theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
 121 intros 3.
 122 elim p.simplify.apply trans_le ? (plus n m) ?.
 123 elim sym_plus ? ?.
 124 apply plus_le.assumption.
 125 apply le_n_Sm_elim ? ? H1.
 126 intros.
 127 *)
 128
 129 theorem distributive_times_minus: distributive nat times minus.
 130 simplify.
 131 intros.
 132 apply (leb_elim z y).intro.
 133 cut eq nat (plus (times x (minus y z)) (times x z))
 134            (plus (minus (times x y) (times x z)) (times x z)).
 135 apply inj_plus_l (times x z).
 136 assumption.
 137 apply trans_eq nat ? (times x y).
 138 rewrite < times_plus_distr.
 139 rewrite < plus_minus_m_m ? ? H.reflexivity.
 140 rewrite < plus_minus_m_m ? ? ?.reflexivity.
 141 apply le_times_r.
 142 assumption.
 143 intro.
 144 rewrite > eq_minus_n_m_O.
 145 rewrite > eq_minus_n_m_O (times x y).
 146 rewrite < sym_times.simplify.reflexivity.
 147 apply lt_to_le.
 148 apply not_le_to_lt.assumption.
 149 apply le_times_r.apply lt_to_le.
 150 apply not_le_to_lt.assumption.
 151 qed.
 152
 153 theorem distr_times_minus: \forall n,m,p:nat.
 154 eq nat (times n (minus m p)) (minus (times n m) (times n p))
 155 \def distributive_times_minus.
 156
 157 theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
 158 intro.elim n.simplify.apply le_n.
 159 elim m.simplify.apply le_n.
 160 simplify.apply le_S.apply H.
 161 qed.