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 set "baseuri" "cic:/matita/nat/minus".
  16
  17 include "nat/orders_op.ma".
  18 include "nat/times.ma".
  19
  20 let rec minus n m \def
  21  match n with
  22  [ O \Rightarrow O
  23  | (S p) \Rightarrow
  24         match m with
  25         [O \Rightarrow (S p)
  26         | (S q) \Rightarrow minus p q ]].
  27
  28
  29 theorem minus_n_O: \forall n:nat.eq nat n (minus n O).
  30 intros.elim n.simplify.reflexivity.
  31 simplify.reflexivity.
  32 qed.
  33
  34 theorem minus_n_n: \forall n:nat.eq nat O (minus n n).
  35 intros.elim n.simplify.
  36 reflexivity.
  37 simplify.apply H.
  38 qed.
  39
  40 theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n).
  41 intro.elim n.
  42 simplify.reflexivity.
  43 elim H.reflexivity.
  44 qed.
  45
  46 theorem minus_Sn_m: \forall n,m:nat.
  47 le m n \to eq nat (minus (S n) m) (S (minus n m)).
  48 intros 2.
  49 apply nat_elim2
  50 (\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))).
  51 intros.apply le_n_O_elim n1 H.
  52 simplify.reflexivity.
  53 intros.simplify.reflexivity.
  54 intros.rewrite < H.reflexivity.
  55 apply le_S_S_to_le. assumption.
  56 qed.
  57
  58 theorem plus_minus:
  59 \forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m).
  60 intros 2.
  61 apply nat_elim2
  62 (\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)).
  63 intros.apply le_n_O_elim ? H.
  64 simplify.rewrite < minus_n_O.reflexivity.
  65 intros.simplify.reflexivity.
  66 intros.simplify.apply H.apply le_S_S_to_le.assumption.
  67 qed.
  68
  69 theorem plus_minus_m_m: \forall n,m:nat.
  70 le m n \to eq nat n (plus (minus n m) m).
  71 intros 2.
  72 apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)).
  73 intros.apply le_n_O_elim n1 H.
  74 reflexivity.
  75 intros.simplify.rewrite < plus_n_O.reflexivity.
  76 intros.simplify.rewrite < sym_plus.simplify.
  77 apply eq_f.rewrite < sym_plus.apply H.
  78 apply le_S_S_to_le.assumption.
  79 qed.
  80
  81 theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to
  82 eq nat n (plus m p).
  83 intros.apply trans_eq ? ? (plus (minus n m) m) ?.
  84 apply plus_minus_m_m.
  85 apply H.elim H1.
  86 apply sym_plus.
  87 qed.
  88
  89 theorem plus_to_minus :\forall n,m,p:nat.le m n \to
  90 eq nat n (plus m p) \to eq nat (minus n m) p.
  91 intros.
  92 apply inj_plus_r m.
  93 rewrite < H1.
  94 rewrite < sym_plus.
  95 symmetry.
  96 apply plus_minus_m_m.assumption.
  97 qed.
  98
  99 theorem minus_ge_O: \forall n,m:nat.
 100 le n m \to eq nat (minus n m) O.
 101 intros 2.
 102 apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
 103 intros.simplify.reflexivity.
 104 intros.apply False_ind.
 105 (* ancora problemi con il not *)
 106 apply not_le_Sn_O n1 H.
 107 intros.
 108 simplify.apply H.apply le_S_S_to_le. apply H1.
 109 qed.
 110
 111 theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
 112 intros.elim H.elim minus_Sn_n n.apply le_n.
 113 rewrite > minus_Sn_m.
 114 apply le_S.assumption.
 115 apply lt_to_le.assumption.
 116 qed.
 117
 118 (*
 119 theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
 120 intros 3.
 121 elim p.simplify.apply trans_le ? (plus n m) ?.
 122 elim sym_plus ? ?.
 123 apply plus_le.assumption.
 124 apply le_n_Sm_elim ? ? H1.
 125 intros.
 126 *)
 127 check distributive.
 128
 129 theorem times_minus_distr: \forall n,m,p:nat.
 130 eq nat (times n (minus m p)) (minus (times n m) (times n p)).
 131 intros.
 132 apply (leb_ind p m).intro.
 133 cut eq nat (plus (times n (minus m p)) (times n p)) (plus (minus (times n m) (times n p)) (times n p)).
 134 apply plus_injective_right ? ? (times n p).
 135 assumption.
 136 apply trans_eq nat ? (times n m).
 137 elim (times_plus_distr ? ? ?).
 138 elim (minus_plus ? ? H).apply refl_equal.
 139 elim (minus_plus ? ? ?).apply refl_equal.
 140 apply times_le_monotony_left.
 141 assumption.
 142 intro.
 143 elim sym_eq ? ? ? (minus_ge_O ? ? ?).
 144 elim sym_eq ? ? ? (minus_ge_O ? ? ?).
 145 elim (sym_times ? ?).simplify.apply refl_equal.
 146 simplify.
 147 apply times_le_monotony_left.
 148 cut (lt m p) \to (le m p).
 149 apply Hcut.simplify.apply not_le_lt ? ? H.
 150 intro.apply lt_le.apply H1.
 151 cut (lt m p) \to (le m p).
 152 apply Hcut.simplify.apply not_le_lt ? ? H.
 153 intro.apply lt_le.apply H1.
 154 qed.
 155
 156 theorem minus_le: \forall n,m:nat. le (minus n m) n.
 157 intro.elim n.simplify.apply le_n.
 158 elim m.simplify.apply le_n.
 159 simplify.apply le_S.apply H.
 160 qed.