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 let rec plus n m : nat \def
 101  match n with
 102  [ O \Rightarrow m
 103  | (S p) \Rightarrow S (plus p m) ].
 104
 105 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
 106 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 107 qed.
 108
 109 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n  m)) (plus n (S m)).
 110 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 111 qed.
 112
 113 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
 114 intros.elim n.simplify.apply plus_n_O.
 115 simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm.
 116 qed.
 117
 118 theorem assoc_plus:
 119 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
 120 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 121 qed.
 122
 123 let rec times n m : nat \def
 124  match n with
 125  [ O \Rightarrow O
 126  | (S p) \Rightarrow (plus m (times p m)) ].
 127
 128 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 129 intros.elim n.simplify.apply refl_equal.simplify.assumption.
 130 qed.
 131
 132 theorem times_n_Sm :
 133 \forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
 134 intros.elim n.simplify.apply refl_equal.
 135 simplify.apply f_equal.elim H.
 136 apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq.
 137 apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)).
 138 apply f_equal2.
 139 apply sym_plus.apply refl_equal.apply assoc_plus.
 140 qed.
 141
 142 theorem sym_times :
 143 \forall n,m:nat. eq nat (times n m) (times m n).
 144 intros.elim n.simplify.apply times_n_O.
 145 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 146 qed.
 147
 148 let rec minus n m : nat \def
 149  [\lambda n:nat.nat] match n with
 150  [ O \Rightarrow O
 151  | (S p) \Rightarrow
 152         [\lambda n:nat.nat] match m with
 153         [O \Rightarrow (S p)
 154         | (S q) \Rightarrow minus p q ]].
 155
 156 theorem nat_case :
 157 \forall n:nat.\forall P:nat \to Prop.
 158 P O \to  (\forall m:nat. P (S m)) \to P n.
 159 intros.elim n.assumption.apply H1.
 160 qed.
 161
 162 theorem nat_double_ind :
 163 \forall R:nat \to nat \to Prop.
 164 (\forall n:nat. R O n) \to
 165 (\forall n:nat. R (S n) O) \to
 166 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 167 intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
 168 apply nat_case m1.apply H1.intros.apply H2. apply H3.
 169 qed.
 170
 171 inductive bool : Set \def
 172   | true : bool
 173   | false : bool.
 174
 175 definition notn : bool \to bool \def
 176 \lambda b:bool.
 177  match b with
 178  [ true \Rightarrow false
 179  | false \Rightarrow true ].
 180
 181 definition andb : bool \to bool \to bool\def
 182 \lambda b1,b2:bool.
 183  match b1 with
 184  [ true \Rightarrow
 185         match b2 with [true \Rightarrow true | false \Rightarrow false]
 186  | false \Rightarrow false ].
 187
 188 definition orb : bool \to bool \to bool\def
 189 \lambda b1,b2:bool.
 190  match b1 with
 191  [ true \Rightarrow
 192         match b2 with [true \Rightarrow true | false \Rightarrow false]
 193  | false \Rightarrow false ].
 194
 195 definition if_then_else : bool \to Prop \to Prop \to Prop \def
 196 \lambda b:bool.\lambda P,Q:Prop.
 197 match b with
 198 [ true \Rightarrow P
 199 | false  \Rightarrow Q].
 200
 201 inductive le (n:nat) : nat \to Prop \def
 202   | le_n : le n n
 203   | le_S : \forall m:nat. le n m \to le n (S m).
 204
 205 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
 206 intros.
 207 elim H1.assumption.
 208 apply le_S.assumption.
 209 qed.
 210
 211 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
 212 intros.elim H.
 213 apply le_n.apply le_S.assumption.
 214 qed.
 215
 216 theorem le_O_n : \forall n:nat. le O n.
 217 intros.elim n.apply le_n.apply le_S. assumption.
 218 qed.
 219
 220 theorem le_n_Sn : \forall n:nat. le n (S n).
 221 intros. apply le_S.apply le_n.
 222 qed.
 223
 224 theorem le_pred_n : \forall n:nat. le (pred n) n.
 225 intros.elim n.simplify.apply le_n.simplify.
 226 apply le_n_Sn.
 227 qed.
 228
 229 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
 230 intros.elim H.exact I.exact I.
 231 qed.
 232
 233 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 234 intros.simplify.intros.apply not_zero_le ? O H.
 235 qed.
 236
 237 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
 238 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
 239 elim n.apply refl_equal.apply False_ind.apply  (le_Sn_O ? H2).
 240 qed.
 241
 242 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
 243 intros.cut le (pred (S n)) (pred (S m)).exact Hcut.
 244 elim H.apply le_n.apply trans_le ? (pred x).assumption.
 245 apply le_pred_n.
 246 qed.
 247
 248 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
 249 intros.elim n.apply le_Sn_O.simplify.intros.
 250 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
 251 qed.
 252
 253 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
 254 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
 255 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
 256 intros.whd.intros.
 257 apply le_n_O_eq.assumption.
 258 intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption.
 259 intros.whd.intros.apply f_equal.apply H2.
 260 apply le_S_n.assumption.
 261 apply le_S_n.assumption.
 262 qed.
 263
 264 let rec leb n m : bool \def
 265    [\lambda n:nat.bool] match n with
 266     [ O \Rightarrow true
 267     | (S p) \Rightarrow
 268         [\lambda n:nat.bool] match m with
 269         [ O \Rightarrow false
 270         | (S q) \Rightarrow leb p q]].
 271
 272 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 273 intros.
 274 apply (nat_double_ind
 275 (\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
 276 simplify.intros.apply le_O_n.
 277 simplify.exact le_Sn_O.
 278 intros 2.simplify.elim (leb n1 m1).
 279 simplify.apply le_n_S.apply H.
 280 simplify.intros.apply H.apply le_S_n.assumption.
 281 qed.
 282
 283 theorem prova :
 284 let three \def (S (S (S O))) in
 285 let nine \def (times three three) in
 286 let eightyone \def (times nine nine) in
 287 let square \def (times eightyone eightyone) in
 288 (eq nat square O).
 289 intro.
 290 intro.
 291 intro.intro.
 292 STOP normalize goal at (? ? % ?).
 293
 294