helm/software/matita/contribs/ng_assembly/common/theory.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 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 universe constraint Type[0] < Type[1].
  24
  25 (* ********************************** *)
  26 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
  27 (* ********************************** *)
  28
  29 (* logic/connectives.ma *)
  30
  31 ninductive True: Prop ≝
  32  I : True.
  33
  34 ninductive False: Prop ≝.
  35
  36 ndefinition Not: Prop → Prop ≝
  37 λA.(A → False).
  38
  39 interpretation "logical not" 'not x = (Not x).
  40
  41 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  42  #A; #C; #H;
  43  nnormalize;
  44  #H1;
  45  nelim (H1 H);
  46 nqed.
  47
  48 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
  49  #A; #B; #H;
  50  nnormalize;
  51  #H1; #H2;
  52  nelim (H1 (H H2)).
  53 nqed.
  54
  55 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
  56  #P; nnormalize; #H; #H1;
  57  napply (H1 H).
  58 nqed.
  59
  60 ninductive And2 (A,B:Prop) : Prop ≝
  61  conj2 : A → B → (And2 A B).
  62
  63 interpretation "logical and" 'and x y = (And2 x y).
  64
  65 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
  66  #A; #B; #H;
  67  napply (And2_ind A B … H);
  68  #H1; #H2;
  69  napply H1.
  70 nqed.
  71
  72 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
  73  #A; #B; #H;
  74  napply (And2_ind A B … H);
  75  #H1; #H2;
  76  napply H2.
  77 nqed.
  78
  79 ninductive And3 (A,B,C:Prop) : Prop ≝
  80  conj3 : A → B → C → (And3 A B C).
  81
  82 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
  83  #A; #B; #C; #H;
  84  napply (And3_ind A B C … H);
  85  #H1; #H2; #H3;
  86  napply H1.
  87 nqed.
  88
  89 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
  90  #A; #B; #C; #H;
  91  napply (And3_ind A B C … H);
  92  #H1; #H2; #H3;
  93  napply H2.
  94 nqed.
  95
  96 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
  97  #A; #B; #C; #H;
  98  napply (And3_ind A B C … H);
  99  #H1; #H2; #H3;
 100  napply H3.
 101 nqed.
 102
 103 ninductive And4 (A,B,C,D:Prop) : Prop ≝
 104  conj4 : A → B → C → D → (And4 A B C D).
 105
 106 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
 107  #A; #B; #C; #D; #H;
 108  napply (And4_ind A B C D … H);
 109  #H1; #H2; #H3; #H4;
 110  napply H1.
 111 nqed.
 112
 113 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
 114  #A; #B; #C; #D; #H;
 115  napply (And4_ind A B C D … H);
 116  #H1; #H2; #H3; #H4;
 117  napply H2.
 118 nqed.
 119
 120 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
 121  #A; #B; #C; #D; #H;
 122  napply (And4_ind A B C D … H);
 123  #H1; #H2; #H3; #H4;
 124  napply H3.
 125 nqed.
 126
 127 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
 128  #A; #B; #C; #D; #H;
 129  napply (And4_ind A B C D … H);
 130  #H1; #H2; #H3; #H4;
 131  napply H4.
 132 nqed.
 133
 134 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
 135  conj5 : A → B → C → D → E → (And5 A B C D E).
 136
 137 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
 138  #A; #B; #C; #D; #E; #H;
 139  napply (And5_ind A B C D E … H);
 140  #H1; #H2; #H3; #H4; #H5;
 141  napply H1.
 142 nqed.
 143
 144 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
 145  #A; #B; #C; #D; #E; #H;
 146  napply (And5_ind A B C D E … H);
 147  #H1; #H2; #H3; #H4; #H5;
 148  napply H2.
 149 nqed.
 150
 151 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
 152  #A; #B; #C; #D; #E; #H;
 153  napply (And5_ind A B C D E … H);
 154  #H1; #H2; #H3; #H4; #H5;
 155  napply H3.
 156 nqed.
 157
 158 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
 159  #A; #B; #C; #D; #E; #H;
 160  napply (And5_ind A B C D E … H);
 161  #H1; #H2; #H3; #H4; #H5;
 162  napply H4.
 163 nqed.
 164
 165 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
 166  #A; #B; #C; #D; #E; #H;
 167  napply (And5_ind A B C D E … H);
 168  #H1; #H2; #H3; #H4; #H5;
 169  napply H5.
 170 nqed.
 171
 172 ninductive Or2 (A,B:Prop) : Prop ≝
 173   or2_intro1 : A → (Or2 A B)
 174 | or2_intro2 : B → (Or2 A B).
 175
 176 interpretation "logical or" 'or x y = (Or2 x y).
 177
 178 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 179
 180 nlemma or2_elim
 181  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
 182  #P1; #P2; #Q; #H; #f1; #f2;
 183  napply (Or2_ind P1 P2 ? f1 f2 ?);
 184  napply H.
 185 nqed.
 186
 187 ninductive Or3 (A,B,C:Prop) : Prop ≝
 188   or3_intro1 : A → (Or3 A B C)
 189 | or3_intro2 : B → (Or3 A B C)
 190 | or3_intro3 : C → (Or3 A B C).
 191
 192 nlemma or3_elim
 193  : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
 194  #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
 195  napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
 196  napply H.
 197 nqed.
 198
 199 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
 200   or4_intro1 : A → (Or4 A B C D)
 201 | or4_intro2 : B → (Or4 A B C D)
 202 | or4_intro3 : C → (Or4 A B C D)
 203 | or4_intro4 : D → (Or4 A B C D).
 204
 205 nlemma or4_elim
 206  : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
 207    ∀f3:P3 → Q.∀f4:P4 → Q.Q.
 208  #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
 209  napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
 210  napply H.
 211 nqed.
 212
 213 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
 214   or5_intro1 : A → (Or5 A B C D E)
 215 | or5_intro2 : B → (Or5 A B C D E)
 216 | or5_intro3 : C → (Or5 A B C D E)
 217 | or5_intro4 : D → (Or5 A B C D E)
 218 | or5_intro5 : E → (Or5 A B C D E).
 219
 220 nlemma or5_elim
 221  : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
 222    ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
 223  #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
 224  napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
 225  napply H.
 226 nqed.
 227
 228 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 229  ex_intro: ∀x:A.Q x → ex A Q.
 230
 231 interpretation "exists" 'exists x = (ex ? x).
 232
 233 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 234  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 235
 236 ndefinition iff ≝
 237 λA,B.(A → B) ∧ (B → A).
 238
 239 (* higher_order_defs/relations *)
 240
 241 ndefinition relation : Type → Type ≝
 242 λA:Type.A → A → Prop.
 243
 244 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 245 λA.λR.∀x:A.R x x.
 246
 247 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 248 λA.λR.∀x,y:A.R x y → R y x.
 249
 250 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 251 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 252
 253 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 254 λA.λR.∀x:A.¬ (R x x).
 255
 256 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 257 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 258
 259 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 260 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 261
 262 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 263 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 264
 265 (* logic/equality.ma *)
 266
 267 ninductive eq (A:Type) (x:A) : A → Prop ≝
 268  refl_eq : eq A x x.
 269
 270 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 271
 272 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 273
 274 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
 275  #T1; #T2; #x; #y; #f; #H;
 276  nrewrite < H;
 277  napply refl_eq.
 278 nqed.
 279
 280 nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2.
 281  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
 282  nrewrite < H1;
 283  nrewrite < H2;
 284  napply refl_eq.
 285 nqed.
 286
 287 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
 288  #T1; #T2; #x; #y; #f;
 289  nnormalize; #H; #H1;
 290  napply (H (eq_f … H1)).
 291 nqed.
 292
 293 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 294  #A;
 295  nnormalize;
 296  #x; #y; #H;
 297  nrewrite < H;
 298  napply refl_eq.
 299 nqed.
 300
 301 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 302  #A; #x; #P; #H; #y; #H1;
 303  nrewrite < (symmetric_eq … H1);
 304  napply H.
 305 nqed.
 306
 307 nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
 308  #T; #x; #y;
 309  nnormalize;
 310  #H; #H1;
 311  nrewrite > H1 in H:(%); #H;
 312  napply (H (refl_eq …)).
 313 nqed.
 314
 315 ndefinition relationT : Type → Type → Type ≝
 316 λA,T:Type.A → A → T.
 317
 318 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 319 λA,T.λR.∀x,y:A.R x y = R y x.
 320
 321 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 322 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).