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