helm/matita/tests/match.ma

   1 inductive True: Prop \def
   2 I : True.
   3
   4 inductive False: Prop \def .
   5
   6 definition Not: Prop \to Prop \def
   7 \lambda A:Prop. (A \to False).
   8
   9 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
  10 intro.cut False.elim Hcut.apply H1.assumption.
  11 qed.
  12
  13 inductive And (A,B:Prop) : Prop \def
  14     conj : A \to B \to (And A B).
  15
  16 theorem proj1: \forall A,B:Prop. (And A B) \to A.
  17 intro. elim H. assumption.
  18 qed.
  19
  20 theorem proj2: \forall A,B:Prop. (And A B) \to A.
  21 intro. elim H. assumption.
  22 qed.
  23
  24 inductive Or (A,B:Prop) : Prop \def
  25      or_introl : A \to (Or A B)
  26    | or_intror : B \to (Or A B).
  27
  28 inductive ex (A:Type) (P:A \to Prop) : Prop \def
  29     ex_intro: \forall x:A. P x \to ex A P.
  30
  31 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
  32     ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
  33
  34 inductive eq (A:Type) (x:A) : A \to Prop \def
  35     refl_equal : eq A x x.
  36
  37 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y  \to eq A y x.
  38 intro. elim H. apply refl_equal.
  39 qed.
  40
  41 theorem trans_eq : \forall A:Type.
  42 \forall x,y,z:A. eq A x y  \to eq A y z \to eq A x z.
  43 intro.elim H1.assumption.
  44 qed.
  45
  46 theorem f_equal: \forall  A,B:Type.\forall f:A\to B.
  47 \forall x,y:A. eq A x y \to eq B (f x) (f y).
  48 intro.elim H.apply refl_equal.
  49 qed.
  50
  51 theorem f_equal2: \forall  A,B,C:Type.\forall f:A\to B \to C.
  52 \forall x1,x2:A. \forall y1,y2:B.
  53 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
  54 intro.elim H1.elim H.apply refl_equal.
  55 qed.
  56
  57 inductive nat : Set \def
  58   | O : nat
  59   | S : nat \to nat.
  60
  61 definition pred: nat \to nat \def
  62 \lambda n:nat. match n with
  63 [ O \Rightarrow  O
  64 | (S u) \Rightarrow u ].
  65
  66 theorem pred_Sn : \forall n:nat.
  67 (eq nat n (pred (S n))).
  68 intro.apply refl_equal.
  69 qed.
  70
  71 theorem injective_S : \forall n,m:nat.
  72 (eq nat (S n) (S m)) \to (eq nat n m).
  73 intro.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))).
  74 apply f_equal. assumption.
  75 qed.
  76
  77 theorem not_eq_S  : \forall n,m:nat.
  78 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
  79 intro. simplify.intro.
  80 apply H.apply injective_S.assumption.
  81 qed.
  82
  83 definition not_zero : nat \to Prop \def
  84 \lambda n: nat.
  85   match n with
  86   [ O \Rightarrow False
  87   | (S p) \Rightarrow True ].
  88
  89 theorem O_S : \forall n:nat. Not (eq nat O (S n)).
  90 intro.simplify.intro.
  91 cut (not_zero O).exact Hcut.elim (sym_eq ? ? ? H).
  92 exact I.
  93 qed.
  94
  95 theorem n_Sn : \forall n:nat. Not (eq nat n (S n)).
  96 intro.elim n.apply O_S.apply not_eq_S.assumption.
  97 qed.
  98
  99
 100 definition plus : nat \to nat \to nat \def
 101 let rec plus (n,m:nat) \def
 102  match n:nat with
 103  [ O \Rightarrow m
 104  | (S p) \Rightarrow S (plus p m) ]
 105 in
 106 plus.
 107
 108 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
 109 intro.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 110 qed.
 111
 112 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n  m)) (plus n (S m)).
 113 intro.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 114 qed.
 115
 116 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
 117 intro.elim n.simplify.apply plus_n_O.
 118 simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm.
 119 qed.
 120
 121 theorem assoc_plus:
 122 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
 123 intro.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 124 qed.
 125
 126 definition times : nat \to nat \to nat \def
 127 let rec times (n,m:nat) \def
 128  match n:nat with
 129  [ O \Rightarrow O
 130  | (S p) \Rightarrow (plus m (times p m)) ]
 131 in
 132 times.
 133
 134 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 135 intro.elim n.simplify.apply refl_equal.simplify.assumption.
 136 qed.
 137
 138 theorem times_n_Sm :
 139 \forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
 140 intro.elim n.simplify.apply refl_equal.
 141 simplify.apply f_equal.elim H.
 142 apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq.
 143 apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)).
 144 apply f_equal2.
 145 apply sym_plus.apply refl_equal.apply assoc_plus.
 146 qed.
 147
 148 theorem sym_times :
 149 \forall n,m:nat. eq nat (times n m) (times m n).
 150 intro.elim n.simplify.apply times_n_O.
 151 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 152 qed.
 153
 154 definition minus : nat \to nat \to nat \def
 155 let rec minus (n,m:nat) \def
 156  [\lambda n:nat.nat] match n:nat with
 157  [ O \Rightarrow O
 158  | (S p) \Rightarrow
 159         [\lambda n:nat.nat] match m:nat with
 160         [O \Rightarrow (S p)
 161         | (S q) \Rightarrow minus p q ]]
 162 in
 163 minus.
 164
 165 theorem nat_case :
 166 \forall n:nat.\forall P:nat \to Prop.
 167 P O \to  (\forall m:nat. P (S m)) \to P n.
 168 intro.elim n.assumption.apply H1.
 169 qed.
 170
 171 theorem nat_double_ind :
 172 \forall R:nat \to nat \to Prop.
 173 (\forall n:nat. R O n) \to
 174 (\forall n:nat. R (S n) O) \to
 175 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 176 intro.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
 177 apply nat_case m1.apply H1.intro.apply H2. apply H3.
 178 qed.
 179
 180 inductive le (n:nat) : nat \to Prop \def
 181   | le_n : le n n
 182   | le_S : \forall m:nat. le n m \to le n (S m).
 183
 184 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
 185 intro.
 186 elim H1.assumption.
 187 apply le_S.assumption.
 188 qed.
 189
 190 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
 191 intro.elim H.alias id "le_n" = "cic:/matita/andrea/le.ind#xpointer(1/1/1)".
 192 apply le_n.apply le_S.assumption.
 193 qed.
 194
 195 theorem le_O_n : \forall n:nat. le O n.
 196 intro.elim n.apply le_n.apply le_S. assumption.
 197 qed.
 198
 199 theorem le_n_Sn : \forall n:nat. le n (S n).
 200 intro. apply le_S.apply le_n.
 201 qed.
 202
 203 theorem le_pred_n : \forall n:nat. le (pred n) n.
 204 intro.elim n.simplify.apply le_n.simplify.
 205 apply le_n_Sn.
 206 qed.
 207
 208 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
 209 intro.elim H.exact I.exact I.
 210 qed.
 211
 212 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 213 intro.simplify.intro.apply not_zero_le ? O H.
 214 qed.
 215
 216 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
 217 intro.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
 218 elim n.apply refl_equal.apply False_ind.apply  (le_Sn_O ? H2).
 219 qed.
 220
 221 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
 222 intro.cut le (pred (S n)) (pred (S m)).exact Hcut.
 223 elim H.apply le_n.apply trans_le ? (pred x).assumption.
 224 apply le_pred_n.
 225 qed.
 226
 227 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
 228 intro.elim n.apply le_Sn_O.simplify.intro.
 229 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
 230 qed.
 231
 232 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 233 intro.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 234 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
 235 intro.whd.intro.alias id "le_n_O_eq" = "cic:/matita/andrea/le_n_O_eq.con".
 236 apply le_n_O_eq.assumption.
 237 intro.whd.intro.apply sym_eq.apply le_n_O_eq.assumption.
 238 intro.whd.intro.apply f_equal.apply H2.
 239 apply le_S_n.assumption.
 240 apply le_S_n.assumption.
 241 qed.
 242
 243 inductive bool : Set \def
 244   | true : bool
 245   | false : bool.
 246
 247 definition notn : bool \to bool \def
 248 \lambda b:bool.
 249  match b with
 250  [ true \Rightarrow false
 251  | false \Rightarrow true ].
 252
 253 definition andb : bool \to bool \to bool\def
 254 \lambda b1,b2:bool.
 255  match b1 with
 256  [ true \Rightarrow
 257         match b2 with [true \Rightarrow true | false \Rightarrow false]
 258  | false \Rightarrow false ].
 259
 260 definition orb : bool \to bool \to bool\def
 261 \lambda b1,b2:bool.
 262  match b1 with
 263  [ true \Rightarrow
 264         match b2 with [true \Rightarrow true | false \Rightarrow false]
 265  | false \Rightarrow false ].
 266
 267 definition leb : nat \to nat \to bool \def
 268 let rec leb (n,m:nat) \def
 269    [\lambda n:nat.bool] match n:nat with
 270     [ O \Rightarrow true
 271     | (S p) \Rightarrow
 272         [\lambda n:nat.bool] match m:nat with
 273         [ O \Rightarrow false
 274         | (S q) \Rightarrow leb p q]]
 275 in leb.
 276
 277 definition if_then_else : bool \to Prop \to Prop \to Prop \def
 278 \lambda b:bool.\lambda P,Q:Prop.
 279 match b with
 280 [ true \Rightarrow P
 281 | false  \Rightarrow Q].
 282
 283 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 284 intro.
 285 apply (nat_double_ind
 286 (\lambda n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
 287 intro.whd.apply le_O_n.intro.whd.apply le_Sn_O.
 288
 289 intros 2.
 290 simplify.
 291 cut ((
 292
 293 \lambda b:bool. [\lambda x:bool.Prop] match b:bool with
 294 [ true \Rightarrow (le n1 m1)
 295 | false \Rightarrow (Not(le n1 m1))]
 296
 297 \to
 298
 299  [\lambda x:bool.Prop] match b:bool with
 300 [ true \Rightarrow (le (S n1) (S m1))
 301 | false \Rightarrow (Not(le (S n1) (S m1)))]
 302 ) (leb n1 m1)).
 303 goal 8.
 304
 305 exact (
 306 [
 307 \lambda b:bool. [\lambda x:bool.Prop] match b:bool with
 308 [ true \Rightarrow (le n1 m1)
 309 | false \Rightarrow (Not(le n1 m1))]
 310
 311 \to
 312
 313  [\lambda x:bool.Prop] match b:bool with
 314 [ true \Rightarrow (le (S n1) (S m1))
 315 | false \Rightarrow (Not(le (S n1) (S m1)))]
 316
 317 ]
 318 match (leb n1 m1) : bool with
 319 [ true \Rightarrow \lambda p:(le n1 m1). le_n_S n1 m1 p
 320 | false \Rightarrow \lambda p:(Not(le n1 m1)). \lambda q:(le (S n1) (S m1)).p(le_S_n n1 m1 q)]
 321 ).
 322 apply Hcut.
 323
 324
 325 cut (eq bool (leb n1 m1) (leb (S n1) (S m1))).
 326 goal 8.
 327 simplify.apply refl_equal.
 328 cut
 329   (if_then_else
 330      (leb (S n1) (S m1))
 331      (le (S n1) (S m1))
 332      (Not (le (S n1) ( S m1)) )).
 333 apply Hcut1.elim Hcut.simplify.
 334 check ([\lambda b:bool. [\lambda b:bool.Prop]match (b:bool) with
 335      [ true \Rightarrow
 336              (if_then_else b (le n1 m1) (Not (le  n1 m1)))
 337      | false \Rightarrow
 338              (if_then_else b (le n1 m1) (Not (le  n1 m1)))
 339 ]
 340 ]
 341 match (leb n1 m1) : bool with
 342 [ true \Rightarrow H | false \Rightarrow H ]).
 343
 344
 345 exact (
 346 [\lambda b:bool. match (b:bool) with
 347      [ true \Rightarrow
 348              (if_then_else b (le (S n1 ) (S m1)) (Not ((le (S n1) (S m1)))))
 349      | false \Rightarrow
 350              (if_then_else b (le (S n1 ) (S m1)) (Not ((le (S n1) (S m1)))))
 351 ]
 352 ]
 353 match (leb n1 m1) : bool with
 354 [ true \Rightarrow le_n_S n1 m1 H
 355 | false \Rightarrow
 356       (\lambda p:(le (S n1) (S m1)).H (le_S_n n1 m1 p))]).
 357
 358
 359
 360
 361 elim n.simplify.apply le_O_n.elim m.
 362 simplify.apply le_Sn_O.simplify.
 363 cut (match (leb e e1):bool with
 364 [true \Rightarrow (eq bool (leb e e1) true)
 365 | false \Rightarrow (eq bool (leb e e1) false)]).
 366 goal 20.
 367 exact [\lambda b:bool. match b with
 368 [true \Rightarrow (eq bool b true)
 369 | false \Rightarrow (eq bool b false)]] match (leb e e1):bool with
 370 [true \Rightarrow refl_equal bool true
 371 | false \Rightarrow refl_equal bool false].