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