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.
  49 apply refl_equal.
  50 qed.
  51
  52 theorem injective_S : \forall n,m:nat.
  53 (eq nat (S n) (S m)) \to (eq nat n m).
  54 intros.
  55 (elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (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.elim (sym_eq ? ? ? 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
  82 let rec plus n m \def
  83  match n with
  84  [ O \Rightarrow m
  85  | (S p) \Rightarrow S (plus p m) ].
  86
  87 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
  88 intros.elim n.simplify.apply refl_equal.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.apply refl_equal.simplify.apply f_equal.assumption.
  93 qed.
  94
  95 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
  96 intros.elim n.simplify.apply plus_n_O.
  97 simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm.
  98 qed.
  99
 100 theorem assoc_plus:
 101 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
 102 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 103 qed.
 104
 105 let rec times n m \def
 106  match n with
 107  [ O \Rightarrow O
 108  | (S p) \Rightarrow (plus m (times p m)) ].
 109
 110 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 111 intros.elim n.simplify.apply refl_equal.simplify.assumption.
 112 qed.
 113
 114 theorem times_n_Sm :
 115 \forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
 116 intros.elim n.simplify.apply refl_equal.
 117 simplify.apply f_equal.elim H.
 118 apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq.
 119 apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)).
 120 apply f_equal2.
 121 apply sym_plus.apply refl_equal.apply assoc_plus.
 122 qed.
 123
 124 theorem sym_times :
 125 \forall n,m:nat. eq nat (times n m) (times m n).
 126 intros.elim n.simplify.apply times_n_O.
 127 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 128 qed.
 129
 130 let rec minus n m \def
 131  match n with
 132  [ O \Rightarrow O
 133  | (S p) \Rightarrow
 134         match m with
 135         [O \Rightarrow (S p)
 136         | (S q) \Rightarrow minus p q ]].
 137
 138 theorem nat_case :
 139 \forall n:nat.\forall P:nat \to Prop.
 140 P O \to  (\forall m:nat. P (S m)) \to P n.
 141 intros.elim n.assumption.apply H1.
 142 qed.
 143
 144 theorem nat_double_ind :
 145 \forall R:nat \to nat \to Prop.
 146 (\forall n:nat. R O n) \to
 147 (\forall n:nat. R (S n) O) \to
 148 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 149 intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
 150 apply nat_case m1.apply H1.intros.apply H2. apply H3.
 151 qed.
 152
 153 inductive le (n:nat) : nat \to Prop \def
 154   | le_n : le n n
 155   | le_S : \forall m:nat. le n m \to le n (S m).
 156
 157 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
 158 intros.
 159 elim H1.assumption.
 160 apply le_S.assumption.
 161 qed.
 162
 163 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
 164 intros.elim H.
 165 apply le_n.apply le_S.assumption.
 166 qed.
 167
 168 theorem le_O_n : \forall n:nat. le O n.
 169 intros.elim n.apply le_n.apply le_S. assumption.
 170 qed.
 171
 172 theorem le_n_Sn : \forall n:nat. le n (S n).
 173 intros. apply le_S.apply le_n.
 174 qed.
 175
 176 theorem le_pred_n : \forall n:nat. le (pred n) n.
 177 intros.elim n.simplify.apply le_n.simplify.
 178 apply le_n_Sn.
 179 qed.
 180
 181 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
 182 intros.elim H.exact I.exact I.
 183 qed.
 184
 185 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 186 intros.simplify.intros.apply not_zero_le ? O H.
 187 qed.
 188
 189 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
 190 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
 191 elim n.apply refl_equal.
 192 apply False_ind.apply  (le_Sn_O ? H2).
 193 qed.
 194
 195 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
 196 intros.cut le (pred (S n)) (pred (S m)).exact Hcut.
 197 elim H.apply le_n.apply trans_le ? (pred x).assumption.
 198 apply le_pred_n.
 199 qed.
 200
 201 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
 202 intros.elim n.apply le_Sn_O.simplify.intros.
 203 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
 204 qed.
 205
 206 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 207 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 208 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
 209 intros.whd.intros.
 210 apply le_n_O_eq.assumption.
 211 intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption.
 212 intros.whd.intros.apply f_equal.apply H2.
 213 apply le_S_n.assumption.
 214 apply le_S_n.assumption.
 215 qed.
 216
 217 let rec leb n m \def
 218     match n with
 219     [ O \Rightarrow true
 220     | (S p) \Rightarrow
 221         match m with
 222         [ O \Rightarrow false
 223         | (S q) \Rightarrow leb p q]].
 224
 225 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 226 intros.
 227 apply (nat_double_ind
 228 (\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
 229 simplify.intros.apply le_O_n.
 230 simplify.exact le_Sn_O.
 231 intros 2.simplify.elim (leb n1 m1).
 232 simplify.apply le_n_S.apply H.
 233 simplify.intros.apply H.apply le_S_n.assumption.
 234 qed.
 235
 236 let rec nat_compare n m: compare \def
 237 match n with
 238 [ O \Rightarrow
 239     match m with
 240       [ O \Rightarrow EQ
 241       | (S q) \Rightarrow LT ]
 242 | (S p) \Rightarrow
 243     match m with
 244       [ O \Rightarrow GT
 245       | (S q) \Rightarrow nat_compare p q]].
 246
 247 theorem nat_compare_invert: \forall n,m:nat.
 248 eq compare (nat_compare n m) (compare_invert (nat_compare m n)).
 249 intros.
 250 apply nat_double_ind (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))).
 251 intros.elim n1.simplify.apply refl_equal.
 252 simplify.apply refl_equal.
 253 intro.elim n1.simplify.apply refl_equal.
 254 simplify.apply refl_equal.
 255 intros.simplify.elim H.apply refl_equal.
 256 qed.
 257