matita/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 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 universe constraint Type[0] < Type[1].
  24 universe constraint Type[1] < Type[2].
  25 universe constraint Type[2] < Type[3].
  26 universe constraint Type[3] < Type[4].
  27
  28 (* ********************************** *)
  29 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
  30 (* ********************************** *)
  31
  32 (* logic/connectives.ma *)
  33
  34 ninductive True: Prop ≝
  35  I : True.
  36
  37 ninductive False: Prop ≝.
  38
  39 ndefinition Not: Prop → Prop ≝
  40 λA.(A → False).
  41
  42 interpretation "logical not" 'not x = (Not x).
  43
  44 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  45  #A; #C; #H;
  46  nnormalize;
  47  #H1;
  48  nelim (H1 H).
  49 nqed.
  50
  51 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
  52  #A; #B; #H;
  53  nnormalize;
  54  #H1; #H2;
  55  nelim (H1 (H H2)).
  56 nqed.
  57
  58 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
  59  #P; nnormalize; #H; #H1;
  60  napply (H1 H).
  61 nqed.
  62
  63 ninductive And2 (A,B:Prop) : Prop ≝
  64  conj2 : A → B → (And2 A B).
  65
  66 interpretation "logical and" 'and x y = (And2 x y).
  67
  68 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
  69  #A; #B; #H;
  70  napply (And2_ind A B … H);
  71  #H1; #H2;
  72  napply H1.
  73 nqed.
  74
  75 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
  76  #A; #B; #H;
  77  napply (And2_ind A B … H);
  78  #H1; #H2;
  79  napply H2.
  80 nqed.
  81
  82 ninductive And3 (A,B,C:Prop) : Prop ≝
  83  conj3 : A → B → C → (And3 A B C).
  84
  85 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
  86  #A; #B; #C; #H;
  87  napply (And3_ind A B C … H);
  88  #H1; #H2; #H3;
  89  napply H1.
  90 nqed.
  91
  92 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
  93  #A; #B; #C; #H;
  94  napply (And3_ind A B C … H);
  95  #H1; #H2; #H3;
  96  napply H2.
  97 nqed.
  98
  99 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
 100  #A; #B; #C; #H;
 101  napply (And3_ind A B C … H);
 102  #H1; #H2; #H3;
 103  napply H3.
 104 nqed.
 105
 106 ninductive And4 (A,B,C,D:Prop) : Prop ≝
 107  conj4 : A → B → C → D → (And4 A B C D).
 108
 109 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
 110  #A; #B; #C; #D; #H;
 111  napply (And4_ind A B C D … H);
 112  #H1; #H2; #H3; #H4;
 113  napply H1.
 114 nqed.
 115
 116 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
 117  #A; #B; #C; #D; #H;
 118  napply (And4_ind A B C D … H);
 119  #H1; #H2; #H3; #H4;
 120  napply H2.
 121 nqed.
 122
 123 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
 124  #A; #B; #C; #D; #H;
 125  napply (And4_ind A B C D … H);
 126  #H1; #H2; #H3; #H4;
 127  napply H3.
 128 nqed.
 129
 130 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
 131  #A; #B; #C; #D; #H;
 132  napply (And4_ind A B C D … H);
 133  #H1; #H2; #H3; #H4;
 134  napply H4.
 135 nqed.
 136
 137 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
 138  conj5 : A → B → C → D → E → (And5 A B C D E).
 139
 140 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
 141  #A; #B; #C; #D; #E; #H;
 142  napply (And5_ind A B C D E … H);
 143  #H1; #H2; #H3; #H4; #H5;
 144  napply H1.
 145 nqed.
 146
 147 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
 148  #A; #B; #C; #D; #E; #H;
 149  napply (And5_ind A B C D E … H);
 150  #H1; #H2; #H3; #H4; #H5;
 151  napply H2.
 152 nqed.
 153
 154 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
 155  #A; #B; #C; #D; #E; #H;
 156  napply (And5_ind A B C D E … H);
 157  #H1; #H2; #H3; #H4; #H5;
 158  napply H3.
 159 nqed.
 160
 161 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
 162  #A; #B; #C; #D; #E; #H;
 163  napply (And5_ind A B C D E … H);
 164  #H1; #H2; #H3; #H4; #H5;
 165  napply H4.
 166 nqed.
 167
 168 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
 169  #A; #B; #C; #D; #E; #H;
 170  napply (And5_ind A B C D E … H);
 171  #H1; #H2; #H3; #H4; #H5;
 172  napply H5.
 173 nqed.
 174
 175 ninductive Or2 (A,B:Prop) : Prop ≝
 176   or2_intro1 : A → (Or2 A B)
 177 | or2_intro2 : B → (Or2 A B).
 178
 179 interpretation "logical or" 'or x y = (Or2 x y).
 180
 181 ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
 182
 183 nlemma or2_elim
 184  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
 185  #P1; #P2; #Q; #H; #f1; #f2;
 186  napply (Or2_ind P1 P2 ? f1 f2 ?);
 187  napply H.
 188 nqed.
 189
 190 nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
 191  #P1; #P2; #H;
 192  napply (or2_elim P1 P2 ? H);
 193  ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
 194  ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
 195  ##]
 196 nqed.
 197
 198 ninductive Or3 (A,B,C:Prop) : Prop ≝
 199   or3_intro1 : A → (Or3 A B C)
 200 | or3_intro2 : B → (Or3 A B C)
 201 | or3_intro3 : C → (Or3 A B C).
 202
 203 nlemma or3_elim
 204  : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
 205  #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
 206  napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
 207  napply H.
 208 nqed.
 209
 210 nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
 211  #P1; #P2; #P3; #H;
 212  napply (or3_elim P1 P2 P3 ? H);
 213  ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
 214  ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
 215  ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
 216  ##]
 217 nqed.
 218
 219 nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
 220  #P1; #P2; #P3; #H;
 221  napply (or3_elim P1 P2 P3 ? H);
 222  ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
 223  ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
 224  ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
 225  ##]
 226 nqed.
 227
 228 nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
 229  #P1; #P2; #P3; #H;
 230  napply (or3_elim P1 P2 P3 ? H);
 231  ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
 232  ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
 233  ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
 234  ##]
 235 nqed.
 236
 237 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
 238   or4_intro1 : A → (Or4 A B C D)
 239 | or4_intro2 : B → (Or4 A B C D)
 240 | or4_intro3 : C → (Or4 A B C D)
 241 | or4_intro4 : D → (Or4 A B C D).
 242
 243 nlemma or4_elim
 244  : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
 245    ∀f3:P3 → Q.∀f4:P4 → Q.Q.
 246  #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
 247  napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
 248  napply H.
 249 nqed.
 250
 251 nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
 252  #P1; #P2; #P3; #P4; #H;
 253  napply (or4_elim P1 P2 P3 P4 ? H);
 254  ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
 255  ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
 256  ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
 257  ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
 258  ##]
 259 nqed.
 260
 261 nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
 262  #P1; #P2; #P3; #P4; #H;
 263  napply (or4_elim P1 P2 P3 P4 ? H);
 264  ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
 265  ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
 266  ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
 267  ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
 268  ##]
 269 nqed.
 270
 271 nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
 272  #P1; #P2; #P3; #P4; #H;
 273  napply (or4_elim P1 P2 P3 P4 ? H);
 274  ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
 275  ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
 276  ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
 277  ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
 278  ##]
 279 nqed.
 280
 281 nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
 282  #P1; #P2; #P3; #P4; #H;
 283  napply (or4_elim P1 P2 P3 P4 ? H);
 284  ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
 285  ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
 286  ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
 287  ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
 288  ##]
 289 nqed.
 290
 291 nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
 292  #P1; #P2; #P3; #P4; #H;
 293  napply (or4_elim P1 P2 P3 P4 ? H);
 294  ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
 295  ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
 296  ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
 297  ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
 298  ##]
 299 nqed.
 300
 301 nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
 302  #P1; #P2; #P3; #P4; #H;
 303  napply (or4_elim P1 P2 P3 P4 ? H);
 304  ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
 305  ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
 306  ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
 307  ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
 308  ##]
 309 nqed.
 310
 311 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
 312   or5_intro1 : A → (Or5 A B C D E)
 313 | or5_intro2 : B → (Or5 A B C D E)
 314 | or5_intro3 : C → (Or5 A B C D E)
 315 | or5_intro4 : D → (Or5 A B C D E)
 316 | or5_intro5 : E → (Or5 A B C D E).
 317
 318 nlemma or5_elim
 319  : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
 320    ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
 321  #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
 322  napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
 323  napply H.
 324 nqed.
 325
 326 nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
 327  #P1; #P2; #P3; #P4; #P5; #H;
 328  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 329  ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
 330  ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
 331  ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
 332  ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
 333  ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
 334  ##]
 335 nqed.
 336
 337 nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
 338  #P1; #P2; #P3; #P4; #P5; #H;
 339  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 340  ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
 341  ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
 342  ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
 343  ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
 344  ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
 345  ##]
 346 nqed.
 347
 348 nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
 349  #P1; #P2; #P3; #P4; #P5; #H;
 350  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 351  ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
 352  ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
 353  ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
 354  ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
 355  ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
 356  ##]
 357 nqed.
 358
 359 nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
 360  #P1; #P2; #P3; #P4; #P5; #H;
 361  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 362  ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
 363  ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
 364  ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
 365  ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
 366  ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
 367  ##]
 368 nqed.
 369
 370 nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
 371  #P1; #P2; #P3; #P4; #P5; #H;
 372  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 373  ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
 374  ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
 375  ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
 376  ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
 377  ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
 378  ##]
 379 nqed.
 380
 381 nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
 382  #P1; #P2; #P3; #P4; #P5; #H;
 383  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 384  ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
 385  ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
 386  ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
 387  ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
 388  ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
 389  ##]
 390 nqed.
 391
 392 nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
 393  #P1; #P2; #P3; #P4; #P5; #H;
 394  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 395  ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
 396  ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
 397  ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
 398  ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
 399  ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
 400  ##]
 401 nqed.
 402
 403 nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
 404  #P1; #P2; #P3; #P4; #P5; #H;
 405  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 406  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
 407  ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
 408  ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
 409  ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
 410  ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
 411  ##]
 412 nqed.
 413
 414 nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
 415  #P1; #P2; #P3; #P4; #P5; #H;
 416  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 417  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
 418  ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
 419  ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
 420  ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
 421  ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
 422  ##]
 423 nqed.
 424
 425 nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
 426  #P1; #P2; #P3; #P4; #P5; #H;
 427  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 428  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
 429  ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
 430  ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
 431  ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
 432  ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
 433  ##]
 434 nqed.
 435
 436 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 437  ex_intro: ∀x:A.Q x → ex A Q.
 438
 439 interpretation "exists" 'exists x = (ex ? x).
 440
 441 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 442  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 443
 444 (* higher_order_defs/relations *)
 445
 446 ndefinition relation : Type → Type ≝
 447 λA.A → A → Prop.
 448
 449 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 450 λA.λR.∀x:A.R x x.
 451
 452 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 453 λA.λR.∀x,y:A.R x y → R y x.
 454
 455 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 456 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 457
 458 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 459 λA.λR.∀x:A.¬ (R x x).
 460
 461 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 462 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 463
 464 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 465 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 466
 467 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 468 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 469
 470 (* logic/equality.ma *)
 471
 472 ninductive eq (A:Type) (x:A) : A → Prop ≝
 473  refl_eq : eq A x x.
 474
 475 ndefinition refl ≝ refl_eq.
 476
 477 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 478
 479 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 480
 481 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
 482  #T1; #T2; #x; #y; #f; #H;
 483  nrewrite < H;
 484  napply refl_eq.
 485 nqed.
 486
 487 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.
 488  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
 489  nrewrite < H1;
 490  nrewrite < H2;
 491  napply refl_eq.
 492 nqed.
 493
 494 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
 495  #T1; #T2; #x; #y; #f;
 496  nnormalize; #H; #H1;
 497  napply (H (eq_f … H1)).
 498 nqed.
 499
 500 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 501  #A;
 502  nnormalize;
 503  #x; #y; #H;
 504  nrewrite < H;
 505  napply refl_eq.
 506 nqed.
 507
 508 nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 509  #A; #x; #P; #H; #y; #H1;
 510  nrewrite < (symmetric_eq … H1);
 511  napply H.
 512 nqed.
 513
 514 ndefinition R0 ≝ λT:Type[0].λt:T.t.
 515
 516 ndefinition R1 ≝ eq_rect_Type0.
 517
 518 ndefinition R2 :
 519   ∀T0:Type[0].
 520   ∀a0:T0.
 521   ∀T1:∀x0:T0. a0=x0 → Type[0].
 522   ∀a1:T1 a0 (refl_eq ? a0).
 523   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 524   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
 525   ∀b0:T0.
 526   ∀e0:a0 = b0.
 527   ∀b1: T1 b0 e0.
 528   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 529   T2 b0 e0 b1 e1.
 530  #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
 531  napply (eq_rect_Type0 ????? e1);
 532  napply (R1 ?? ? ?? e0);
 533  napply a2;
 534 nqed.
 535
 536 ndefinition R3 :
 537   ∀T0:Type[0].
 538   ∀a0:T0.
 539   ∀T1:∀x0:T0. a0=x0 → Type[0].
 540   ∀a1:T1 a0 (refl_eq ? a0).
 541   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
 542   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
 543   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
 544       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
 545   ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
 546   ∀b0:T0.
 547   ∀e0:a0 = b0.
 548   ∀b1: T1 b0 e0.
 549   ∀e1:R1 ?? T1 a1 ? e0 = b1.
 550   ∀b2: T2 b0 e0 b1 e1.
 551   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
 552   T3 b0 e0 b1 e1 b2 e2.
 553  #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
 554  napply (eq_rect_Type0 ????? e2);
 555  napply (R2 ?? ? ???? e0 ? e1);
 556  napply a3;
 557 nqed.
 558
 559 ndefinition R4 :
 560   ∀T0:Type[0].
 561   ∀a0:T0.
 562   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 563   ∀a1:T1 a0 (refl_eq T0 a0).
 564   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 565   ∀a2:T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1).
 566   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 567       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 568   ∀a3:T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
 569       a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2).
 570   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 571       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 572       ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
 573       Type[0].
 574   ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
 575       a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2)
 576       a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
 577                    a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
 578                    a3).
 579   ∀b0:T0.
 580   ∀e0:eq (T0 …) a0 b0.
 581   ∀b1: T1 b0 e0.
 582   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 583   ∀b2: T2 b0 e0 b1 e1.
 584   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 585   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 586   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 587   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 588  #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
 589  napply (eq_rect_Type0 ????? e3);
 590  napply (R3 ????????? e0 ? e1 ? e2);
 591  napply a4;
 592 nqed.
 593
 594 nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
 595  #T; #x; #y;
 596  nnormalize;
 597  #H; #H1;
 598  nrewrite > H1 in H:(%); #H;
 599  napply (H (refl_eq …)).
 600 nqed.
 601
 602 ndefinition relationT : Type → Type → Type ≝
 603 λA,T:Type.A → A → T.
 604
 605 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 606 λA,T.λR.∀x,y:A.R x y = R y x.
 607
 608 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 609 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).