helm/matita/library/nat.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/".
  16
  17 alias id "eq" = "cic:/matita/equality/eq.ind#xpointer(1/1)".
  18 alias id "refl_equal" = "cic:/matita/equality/eq.ind#xpointer(1/1/1)".
  19 alias id "sym_eq" = "cic:/matita/equality/sym_eq.con".
  20 alias id "f_equal" = "cic:/matita/equality/f_equal.con".
  21 alias id "Not" = "cic:/matita/logic/Not.con".
  22 alias id "False" = "cic:/matita/logic/False.ind#xpointer(1/1)".
  23 alias id "True" = "cic:/matita/logic/True.ind#xpointer(1/1)".
  24 alias id "trans_eq" = "cic:/matita/equality/trans_eq.con".
  25 alias id "I" = "cic:/matita/logic/True.ind#xpointer(1/1/1)".
  26 alias id "f_equal2" = "cic:/matita/equality/f_equal2.con".
  27 alias id "False_ind" = "cic:/matita/logic/False_ind.con".
  28 alias id "false" = "cic:/matita/bool/bool.ind#xpointer(1/1/2)".
  29 alias id "true" = "cic:/matita/bool/bool.ind#xpointer(1/1/1)".
  30 alias id "if_then_else" = "cic:/matita/bool/if_then_else.con".
  31 alias id "EQ" = "cic:/matita/compare/compare.ind#xpointer(1/1/2)".
  32 alias id "GT" = "cic:/matita/compare/compare.ind#xpointer(1/1/3)".
  33 alias id "LT" = "cic:/matita/compare/compare.ind#xpointer(1/1/1)".
  34 alias id "compare" = "cic:/matita/compare/compare.ind#xpointer(1/1)".
  35 alias id "compare_invert" = "cic:/matita/compare/compare_invert.con".
  36
  37 inductive nat : Set \def
  38   | O : nat
  39   | S : nat \to nat.
  40
  41 definition pred: nat \to nat \def
  42 \lambda n:nat. match n with
  43 [ O \Rightarrow  O
  44 | (S u) \Rightarrow u ].
  45
  46 theorem pred_Sn : \forall n:nat.
  47 (eq nat n (pred (S n))).
  48 intros.reflexivity.
  49 qed.
  50
  51 theorem injective_S : \forall n,m:nat.
  52 (eq nat (S n) (S m)) \to (eq nat n m).
  53 intros.
  54 rewrite > pred_Sn n.
  55 rewrite > pred_Sn m.
  56 apply f_equal. assumption.
  57 qed.
  58
  59 theorem not_eq_S  : \forall n,m:nat.
  60 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
  61 intros. simplify.intros.
  62 apply H.apply injective_S.assumption.
  63 qed.
  64
  65 definition not_zero : nat \to Prop \def
  66 \lambda n: nat.
  67   match n with
  68   [ O \Rightarrow False
  69   | (S p) \Rightarrow True ].
  70
  71 theorem O_S : \forall n:nat. Not (eq nat O (S n)).
  72 intros.simplify.intros.
  73 cut (not_zero O).exact Hcut.rewrite > H.
  74 exact I.
  75 qed.
  76
  77 theorem n_Sn : \forall n:nat. Not (eq nat n (S n)).
  78 intros.elim n.apply O_S.apply not_eq_S.assumption.
  79 qed.
  80
  81 let rec plus n m \def
  82  match n with
  83  [ O \Rightarrow m
  84  | (S p) \Rightarrow S (plus p m) ].
  85
  86 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
  87 intros.elim n.simplify.reflexivity.
  88 simplify.apply f_equal.assumption.
  89 qed.
  90
  91 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n  m)) (plus n (S m)).
  92 intros.elim n.simplify.reflexivity.
  93 simplify.apply f_equal.assumption.
  94 qed.
  95
  96 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
  97 intros.elim n.simplify.apply plus_n_O.
  98 simplify.rewrite > H.apply plus_n_Sm.
  99 qed.
 100
 101 theorem assoc_plus:
 102 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
 103 intros.elim n.simplify.reflexivity.
 104 simplify.apply f_equal.assumption.
 105 qed.
 106
 107 let rec times n m \def
 108  match n with
 109  [ O \Rightarrow O
 110  | (S p) \Rightarrow (plus m (times p m)) ].
 111
 112 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 113 intros.elim n.simplify.reflexivity.
 114 simplify.assumption.
 115 qed.
 116
 117 theorem times_n_Sm :
 118 \forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
 119 intros.elim n.simplify.reflexivity.
 120 simplify.apply f_equal.rewrite < H.
 121 transitivity (plus (plus e m) (times e m)).symmetry.
 122 apply assoc_plus.transitivity (plus (plus m e) (times e m)).
 123 apply f_equal2.
 124 apply sym_plus.reflexivity.apply assoc_plus.
 125 qed.
 126
 127 theorem sym_times :
 128 \forall n,m:nat. eq nat (times n m) (times m n).
 129 intros.elim n.simplify.apply times_n_O.
 130 simplify.rewrite < sym_eq ? ? ? H.apply times_n_Sm.
 131 qed.
 132
 133 let rec minus n m \def
 134  match n with
 135  [ O \Rightarrow O
 136  | (S p) \Rightarrow
 137         match m with
 138         [O \Rightarrow (S p)
 139         | (S q) \Rightarrow minus p q ]].
 140
 141 theorem nat_case :
 142 \forall n:nat.\forall P:nat \to Prop.
 143 P O \to  (\forall m:nat. P (S m)) \to P n.
 144 intros.elim n.assumption.apply H1.
 145 qed.
 146
 147 theorem nat_double_ind :
 148 \forall R:nat \to nat \to Prop.
 149 (\forall n:nat. R O n) \to
 150 (\forall n:nat. R (S n) O) \to
 151 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 152 intros 5.elim n.apply H.
 153 apply nat_case m.apply H1.intros.apply H2. apply H3.
 154 qed.
 155
 156 inductive le (n:nat) : nat \to Prop \def
 157   | le_n : le n n
 158   | le_S : \forall m:nat. le n m \to le n (S m).
 159
 160 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
 161 intros.
 162 elim H1.assumption.
 163 apply le_S.assumption.
 164 qed.
 165
 166 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
 167 intros.elim H.
 168 apply le_n.apply le_S.assumption.
 169 qed.
 170
 171 theorem le_O_n : \forall n:nat. le O n.
 172 intros.elim n.apply le_n.apply le_S. assumption.
 173 qed.
 174
 175 theorem le_n_Sn : \forall n:nat. le n (S n).
 176 intros. apply le_S.apply le_n.
 177 qed.
 178
 179 theorem le_pred_n : \forall n:nat. le (pred n) n.
 180 intros.elim n.simplify.apply le_n.simplify.
 181 apply le_n_Sn.
 182 qed.
 183
 184 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
 185 intros.elim H.exact I.exact I.
 186 qed.
 187
 188 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 189 intros.simplify.intros.apply not_zero_le ? O H.
 190 qed.
 191
 192 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
 193 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
 194 elim n.reflexivity.
 195 apply False_ind.apply  (le_Sn_O ? H2).
 196 qed.
 197
 198 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
 199 intros.change with le (pred (S n)) (pred (S m)).
 200 elim H.apply le_n.apply trans_le ? (pred x).assumption.
 201 apply le_pred_n.
 202 qed.
 203
 204 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
 205 intros.elim n.apply le_Sn_O.simplify.intros.
 206 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
 207 qed.
 208
 209 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 210 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 211 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
 212 intros.whd.intros.
 213 apply le_n_O_eq.assumption.
 214 intros.symmetry.apply le_n_O_eq.assumption.
 215 intros.apply f_equal.apply H2.
 216 apply le_S_n.assumption.
 217 apply le_S_n.assumption.
 218 qed.
 219
 220 let rec leb n m \def
 221     match n with
 222     [ O \Rightarrow true
 223     | (S p) \Rightarrow
 224         match m with
 225         [ O \Rightarrow false
 226         | (S q) \Rightarrow leb p q]].
 227
 228 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 229 intros.
 230 apply (nat_double_ind
 231 (\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
 232 simplify.intros.apply le_O_n.
 233 simplify.exact le_Sn_O.
 234 intros 2.simplify.elim (leb n1 m1).
 235 simplify.apply le_n_S.apply H.
 236 simplify.intros.apply H.apply le_S_n.assumption.
 237 qed.
 238
 239 let rec nat_compare n m: compare \def
 240 match n with
 241 [ O \Rightarrow
 242     match m with
 243       [ O \Rightarrow EQ
 244       | (S q) \Rightarrow LT ]
 245 | (S p) \Rightarrow
 246     match m with
 247       [ O \Rightarrow GT
 248       | (S q) \Rightarrow nat_compare p q]].
 249
 250 theorem nat_compare_invert: \forall n,m:nat.
 251 eq compare (nat_compare n m) (compare_invert (nat_compare m n)).
 252 intros.
 253 apply nat_double_ind (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))).
 254 intros.elim n1.simplify.reflexivity.
 255 simplify.reflexivity.
 256 intro.elim n1.simplify.reflexivity.
 257 simplify.reflexivity.
 258 intros.simplify.elim H.simplify.reflexivity.
 259 qed.
 260