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 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 intro.
 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 intro.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 intro.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 intro. apply le_S.apply le_n.
 231 qed.
 232
 233 theorem le_pred_n : \forall n:nat. le (pred n) n.
 234 intro.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 intro.elim H.exact I.exact I.
 240 qed.
 241
 242 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
 243 intro.simplify.intro.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 intro.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 intro.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 intro.elim n.apply le_Sn_O.simplify.intro.
 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 intro.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 intro.whd.intro.
 266 apply le_n_O_eq.assumption.
 267 intro.whd.intro.apply sym_eq.apply le_n_O_eq.assumption.
 268 intro.whd.intro.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:nat) \def
 275    [\lambda n:nat.bool] match n:nat with
 276     [ O \Rightarrow true
 277     | (S p) \Rightarrow
 278         [\lambda n:nat.bool] match m:nat 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.intro.apply H.apply le_S_n.assumption.
 292 qed.