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