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 universe constraint Type[1] < Type[2].
  25 universe constraint Type[2] < Type[3].
  26
  27 (* ********************************** *)
  28 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
  29 (* ********************************** *)
  30
  31 (* logic/connectives.ma *)
  32
  33 ninductive True: Prop ≝
  34  I : True.
  35
  36 ninductive False: Prop ≝.
  37
  38 ndefinition Not: Prop → Prop ≝
  39 λA.(A → False).
  40
  41 interpretation "logical not" 'not x = (Not x).
  42
  43 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  44  #A; #C; #H;
  45  nnormalize;
  46  #H1;
  47  nelim (H1 H);
  48 nqed.
  49
  50 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
  51  #A; #B; #H;
  52  nnormalize;
  53  #H1; #H2;
  54  nelim (H1 (H H2)).
  55 nqed.
  56
  57 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
  58  #P; nnormalize; #H; #H1;
  59  napply (H1 H).
  60 nqed.
  61
  62 ninductive And2 (A,B:Prop) : Prop ≝
  63  conj2 : A → B → (And2 A B).
  64
  65 interpretation "logical and" 'and x y = (And2 x y).
  66
  67 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
  68  #A; #B; #H;
  69  napply (And2_ind A B … H);
  70  #H1; #H2;
  71  napply H1.
  72 nqed.
  73
  74 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
  75  #A; #B; #H;
  76  napply (And2_ind A B … H);
  77  #H1; #H2;
  78  napply H2.
  79 nqed.
  80
  81 ninductive And3 (A,B,C:Prop) : Prop ≝
  82  conj3 : A → B → C → (And3 A B C).
  83
  84 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
  85  #A; #B; #C; #H;
  86  napply (And3_ind A B C … H);
  87  #H1; #H2; #H3;
  88  napply H1.
  89 nqed.
  90
  91 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
  92  #A; #B; #C; #H;
  93  napply (And3_ind A B C … H);
  94  #H1; #H2; #H3;
  95  napply H2.
  96 nqed.
  97
  98 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
  99  #A; #B; #C; #H;
 100  napply (And3_ind A B C … H);
 101  #H1; #H2; #H3;
 102  napply H3.
 103 nqed.
 104
 105 ninductive And4 (A,B,C,D:Prop) : Prop ≝
 106  conj4 : A → B → C → D → (And4 A B C D).
 107
 108 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
 109  #A; #B; #C; #D; #H;
 110  napply (And4_ind A B C D … H);
 111  #H1; #H2; #H3; #H4;
 112  napply H1.
 113 nqed.
 114
 115 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
 116  #A; #B; #C; #D; #H;
 117  napply (And4_ind A B C D … H);
 118  #H1; #H2; #H3; #H4;
 119  napply H2.
 120 nqed.
 121
 122 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
 123  #A; #B; #C; #D; #H;
 124  napply (And4_ind A B C D … H);
 125  #H1; #H2; #H3; #H4;
 126  napply H3.
 127 nqed.
 128
 129 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
 130  #A; #B; #C; #D; #H;
 131  napply (And4_ind A B C D … H);
 132  #H1; #H2; #H3; #H4;
 133  napply H4.
 134 nqed.
 135
 136 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
 137  conj5 : A → B → C → D → E → (And5 A B C D E).
 138
 139 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
 140  #A; #B; #C; #D; #E; #H;
 141  napply (And5_ind A B C D E … H);
 142  #H1; #H2; #H3; #H4; #H5;
 143  napply H1.
 144 nqed.
 145
 146 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
 147  #A; #B; #C; #D; #E; #H;
 148  napply (And5_ind A B C D E … H);
 149  #H1; #H2; #H3; #H4; #H5;
 150  napply H2.
 151 nqed.
 152
 153 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
 154  #A; #B; #C; #D; #E; #H;
 155  napply (And5_ind A B C D E … H);
 156  #H1; #H2; #H3; #H4; #H5;
 157  napply H3.
 158 nqed.
 159
 160 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
 161  #A; #B; #C; #D; #E; #H;
 162  napply (And5_ind A B C D E … H);
 163  #H1; #H2; #H3; #H4; #H5;
 164  napply H4.
 165 nqed.
 166
 167 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
 168  #A; #B; #C; #D; #E; #H;
 169  napply (And5_ind A B C D E … H);
 170  #H1; #H2; #H3; #H4; #H5;
 171  napply H5.
 172 nqed.
 173
 174 ninductive Or2 (A,B:Prop) : Prop ≝
 175   or2_intro1 : A → (Or2 A B)
 176 | or2_intro2 : B → (Or2 A B).
 177
 178 interpretation "logical or" 'or x y = (Or2 x y).
 179
 180 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 181
 182 nlemma or2_elim
 183  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
 184  #P1; #P2; #Q; #H; #f1; #f2;
 185  napply (Or2_ind P1 P2 ? f1 f2 ?);
 186  napply H.
 187 nqed.
 188
 189 nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
 190  #P1; #P2; #H;
 191  napply (or2_elim P1 P2 ? H);
 192  ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
 193  ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
 194  ##]
 195 nqed.
 196
 197 ninductive Or3 (A,B,C:Prop) : Prop ≝
 198   or3_intro1 : A → (Or3 A B C)
 199 | or3_intro2 : B → (Or3 A B C)
 200 | or3_intro3 : C → (Or3 A B C).
 201
 202 nlemma or3_elim
 203  : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
 204  #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
 205  napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
 206  napply H.
 207 nqed.
 208
 209 nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
 210  #P1; #P2; #P3; #H;
 211  napply (or3_elim P1 P2 P3 ? H);
 212  ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
 213  ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
 214  ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
 215  ##]
 216 nqed.
 217
 218 nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
 219  #P1; #P2; #P3; #H;
 220  napply (or3_elim P1 P2 P3 ? H);
 221  ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
 222  ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
 223  ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
 224  ##]
 225 nqed.
 226
 227 nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
 228  #P1; #P2; #P3; #H;
 229  napply (or3_elim P1 P2 P3 ? H);
 230  ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
 231  ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
 232  ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
 233  ##]
 234 nqed.
 235
 236 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
 237   or4_intro1 : A → (Or4 A B C D)
 238 | or4_intro2 : B → (Or4 A B C D)
 239 | or4_intro3 : C → (Or4 A B C D)
 240 | or4_intro4 : D → (Or4 A B C D).
 241
 242 nlemma or4_elim
 243  : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
 244    ∀f3:P3 → Q.∀f4:P4 → Q.Q.
 245  #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
 246  napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
 247  napply H.
 248 nqed.
 249
 250 nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
 251  #P1; #P2; #P3; #P4; #H;
 252  napply (or4_elim P1 P2 P3 P4 ? H);
 253  ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
 254  ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
 255  ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
 256  ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
 257  ##]
 258 nqed.
 259
 260 nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
 261  #P1; #P2; #P3; #P4; #H;
 262  napply (or4_elim P1 P2 P3 P4 ? H);
 263  ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
 264  ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
 265  ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
 266  ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
 267  ##]
 268 nqed.
 269
 270 nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
 271  #P1; #P2; #P3; #P4; #H;
 272  napply (or4_elim P1 P2 P3 P4 ? H);
 273  ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
 274  ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
 275  ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
 276  ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
 277  ##]
 278 nqed.
 279
 280 nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
 281  #P1; #P2; #P3; #P4; #H;
 282  napply (or4_elim P1 P2 P3 P4 ? H);
 283  ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
 284  ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
 285  ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
 286  ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
 287  ##]
 288 nqed.
 289
 290 nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
 291  #P1; #P2; #P3; #P4; #H;
 292  napply (or4_elim P1 P2 P3 P4 ? H);
 293  ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
 294  ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
 295  ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
 296  ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
 297  ##]
 298 nqed.
 299
 300 nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
 301  #P1; #P2; #P3; #P4; #H;
 302  napply (or4_elim P1 P2 P3 P4 ? H);
 303  ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
 304  ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
 305  ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
 306  ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
 307  ##]
 308 nqed.
 309
 310 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
 311   or5_intro1 : A → (Or5 A B C D E)
 312 | or5_intro2 : B → (Or5 A B C D E)
 313 | or5_intro3 : C → (Or5 A B C D E)
 314 | or5_intro4 : D → (Or5 A B C D E)
 315 | or5_intro5 : E → (Or5 A B C D E).
 316
 317 nlemma or5_elim
 318  : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
 319    ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
 320  #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
 321  napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
 322  napply H.
 323 nqed.
 324
 325 nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
 326  #P1; #P2; #P3; #P4; #P5; #H;
 327  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 328  ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
 329  ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
 330  ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
 331  ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
 332  ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
 333  ##]
 334 nqed.
 335
 336 nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
 337  #P1; #P2; #P3; #P4; #P5; #H;
 338  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 339  ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
 340  ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
 341  ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
 342  ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
 343  ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
 344  ##]
 345 nqed.
 346
 347 nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
 348  #P1; #P2; #P3; #P4; #P5; #H;
 349  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 350  ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
 351  ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
 352  ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
 353  ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
 354  ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
 355  ##]
 356 nqed.
 357
 358 nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
 359  #P1; #P2; #P3; #P4; #P5; #H;
 360  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 361  ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
 362  ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
 363  ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
 364  ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
 365  ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
 366  ##]
 367 nqed.
 368
 369 nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
 370  #P1; #P2; #P3; #P4; #P5; #H;
 371  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 372  ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
 373  ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
 374  ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
 375  ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
 376  ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
 377  ##]
 378 nqed.
 379
 380 nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
 381  #P1; #P2; #P3; #P4; #P5; #H;
 382  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 383  ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
 384  ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
 385  ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
 386  ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
 387  ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
 388  ##]
 389 nqed.
 390
 391 nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
 392  #P1; #P2; #P3; #P4; #P5; #H;
 393  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 394  ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
 395  ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
 396  ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
 397  ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
 398  ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
 399  ##]
 400 nqed.
 401
 402 nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
 403  #P1; #P2; #P3; #P4; #P5; #H;
 404  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 405  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
 406  ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
 407  ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
 408  ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
 409  ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
 410  ##]
 411 nqed.
 412
 413 nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
 414  #P1; #P2; #P3; #P4; #P5; #H;
 415  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 416  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
 417  ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
 418  ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
 419  ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
 420  ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
 421  ##]
 422 nqed.
 423
 424 nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
 425  #P1; #P2; #P3; #P4; #P5; #H;
 426  napply (or5_elim P1 P2 P3 P4 P5 ? H);
 427  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
 428  ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
 429  ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
 430  ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
 431  ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
 432  ##]
 433 nqed.
 434
 435 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 436  ex_intro: ∀x:A.Q x → ex A Q.
 437
 438 interpretation "exists" 'exists x = (ex ? x).
 439
 440 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 441  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 442
 443 ndefinition iff ≝
 444 λA,B.(A → B) ∧ (B → A).
 445
 446 (* higher_order_defs/relations *)
 447
 448 ndefinition relation : Type → Type ≝
 449 λA:Type.A → A → Prop.
 450
 451 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 452 λA.λR.∀x:A.R x x.
 453
 454 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 455 λA.λR.∀x,y:A.R x y → R y x.
 456
 457 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 458 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 459
 460 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 461 λA.λR.∀x:A.¬ (R x x).
 462
 463 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 464 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 465
 466 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 467 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 468
 469 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 470 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 471
 472 (* logic/equality.ma *)
 473
 474 ninductive eq (A:Type) (x:A) : A → Prop ≝
 475  refl_eq : eq A x x.
 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.∀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 nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
 515  #T; #x; #y;
 516  nnormalize;
 517  #H; #H1;
 518  nrewrite > H1 in H:(%); #H;
 519  napply (H (refl_eq …)).
 520 nqed.
 521
 522 ndefinition relationT : Type → Type → Type ≝
 523 λA,T:Type.A → A → T.
 524
 525 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 526 λA,T.λR.∀x,y:A.R x y = R y x.
 527
 528 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 529 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
 530
 531 (* aggiunta per bypassare i punti in cui le dimostrazioni sono equivalenti *)
 532 (*
 533 ninductive peqv (A:Prop) (x:A) : A → Prop ≝
 534  prefl_eqv : peqv A x x.
 535
 536 interpretation "prop equivalence" 'preqv t x y = (peqv t x y).
 537 *)
 538 (* \equiv *)
 539 (*
 540 notation > "hvbox(a break ≡ b)"
 541   non associative with precedence 45
 542 for @{ 'preqv ? $a $b }.
 543
 544 nlemma symmetric_peqv: ∀A:Prop. symmetric A (peqv A).
 545  #A;
 546  nnormalize;
 547  #x; #y; #H;
 548  napply (peqv_ind A x (λ_.?) ? y H);
 549  napply prefl_eqv.
 550 nqed.
 551
 552 nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P y.
 553  #A; #x; #P; #H; #y; #H1;
 554  napply (peqv_ind A x (λ_.?) H y (symmetric_peqv … H1)).
 555 nqed.
 556
 557 naxiom peqv_ax : ∀P:Prop.∀Q,R:P.Q ≡ R.
 558 *)
 559 (* uso P x → P y, H e' P x
 560    nrewrite > cioe' napply (peqv_ind ? x (λ_.?) H y (dimostrazione di x ≡ y));
 561    nrewrite < cioe' napply (peqv_ind_r ? x ? H y (dimostrazione y ≡ x)));
 562 *)