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 intros.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 intros. elim H. assumption.
  18 qed.
  19
  20 theorem proj2: \forall A,B:Prop. (And A B) \to A.
  21 intros. 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 intros. 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 intros.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 intros.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 intros.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 intros.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 intros.(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 intros. simplify.intros.
  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 intros.simplify.intros.
  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 intros.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 \def
 102  match n 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 intros.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 intros.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 intros.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 intros.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 \def
 128  match n 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 intros.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 intros.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 intros.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 \def
 156  [\lambda n:nat.nat] match n with
 157  [ O \Rightarrow O
 158  | (S p) \Rightarrow
 159         [\lambda n:nat.nat] match m 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 intros.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 intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
 177 apply nat_case m1.apply H1.intros.apply H2. apply H3.
 178 qed.
 179
 180 inductive bool : Set \def
 181   | true : bool
 182   | false : bool.
 183
 184 definition notn : bool \to bool \def
 185 \lambda b:bool.
 186  match b with
 187  [ true \Rightarrow false
 188  | false \Rightarrow true ].
 189
 190 definition andb : bool \to bool \to bool\def
 191 \lambda b1,b2:bool.
 192  match b1 with
 193  [ true \Rightarrow
 194         match b2 with [true \Rightarrow true | false \Rightarrow false]
 195  | false \Rightarrow false ].
 196
 197 definition orb : bool \to bool \to bool\def
 198 \lambda b1,b2:bool.
 199  match b1 with
 200  [ true \Rightarrow
 201         match b2 with [true \Rightarrow true | false \Rightarrow false]
 202  | false \Rightarrow false ].
 203
 204 definition if_then_else : bool \to Prop \to Prop \to Prop \def
 205 \lambda b:bool.\lambda P,Q:Prop.
 206 match b with
 207 [ true \Rightarrow P
 208 | false  \Rightarrow Q].
 209
 210 inductive le (n:nat) : nat \to Prop \def
 211   | le_n : le n n
 212   | le_S : \forall m:nat. le n m \to le n (S m).
 213
 214 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
 215 intros.
 216 elim H1.assumption.
 217 apply le_S.assumption.
 218 qed.
 219
 220 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
 221 intros.elim H.
 222 apply le_n.apply le_S.assumption.
 223 qed.
 224
 225 theorem le_O_n : \forall n:nat. le O n.
 226 intros.elim n.apply le_n.apply le_S. assumption.
 227 qed.
 228
 229 theorem le_n_Sn : \forall n:nat. le n (S n).
 230 intros. apply le_S.apply le_n.
 231 qed.
 232
 233 theorem le_pred_n : \forall n:nat. le (pred n) n.
 234 intros.elim n.simplify.apply le_n.simplify.
 235 apply le_n_Sn.
 236 qed.
 237
 238 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
 239 intros.elim H.exact I.exact I.
 240 qed.
 241
 242 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 243 intros.simplify.intros.apply not_zero_le ? O H.
 244 qed.
 245
 246 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
 247 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
 248 elim n.apply refl_equal.apply False_ind.apply  (le_Sn_O ? H2).
 249 qed.
 250
 251 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
 252 intros.cut le (pred (S n)) (pred (S m)).exact Hcut.
 253 elim H.apply le_n.apply trans_le ? (pred x).assumption.
 254 apply le_pred_n.
 255 qed.
 256
 257 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
 258 intros.elim n.apply le_Sn_O.simplify.intros.
 259 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
 260 qed.
 261
 262 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 263 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 264 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
 265 intros.whd.intros.
 266 apply le_n_O_eq.assumption.
 267 intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption.
 268 intros.whd.intros.apply f_equal.apply H2.
 269 apply le_S_n.assumption.
 270 apply le_S_n.assumption.
 271 qed.
 272
 273 definition leb : nat \to nat \to bool \def
 274 let rec leb n m \def
 275    [\lambda n:nat.bool] match n with
 276     [ O \Rightarrow true
 277     | (S p) \Rightarrow
 278         [\lambda n:nat.bool] match m with
 279         [ O \Rightarrow false
 280         | (S q) \Rightarrow leb p q]]
 281 in leb.
 282
 283 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 284 intros.
 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 simplify.intros.apply le_O_n.
 288 simplify.exact le_Sn_O.
 289 intros 2.simplify.elim (leb n1 m1).
 290 simplify.apply le_n_S.apply H.
 291 simplify.intros.apply H.apply le_S_n.assumption.
 292 qed.
 293
 294 theorem prova :
 295 let three \def (S (S (S O))) in
 296 let nine \def (times three three) in
 297 let eightyone \def (times nine nine) in
 298 let square \def (times eightyone eightyone) in
 299 (eq nat square O).
 300 intro.
 301 intro.
 302 intro.intro.
 303 STOP normalize goal at (? ? % ?).
 304
 305