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 And (A,B:Prop) : Prop ≝
  61  conj : A → B → (And A B).
  62
  63 interpretation "logical and" 'and x y = (And x y).
  64
  65 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  66  #A; #B; #H;
  67  (* \ldots al posto di ??? *)
  68  napply (And_ind A B … H);
  69  #H1; #H2;
  70  napply H1.
  71 nqed.
  72
  73 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
  74  #A; #B; #H;
  75  napply (And_ind A B … H);
  76  #H1; #H2;
  77  napply H2.
  78 nqed.
  79
  80 ninductive Or (A,B:Prop) : Prop ≝
  81   or_introl : A → (Or A B)
  82 | or_intror : B → (Or A B).
  83
  84 interpretation "logical or" 'or x y = (Or x y).
  85
  86 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
  87
  88 nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
  89  #P; #Q; #G; #H; #H1; #H2;
  90  napply (Or_ind P Q ? H1 H2 ?);
  91  napply H.
  92 nqed.
  93
  94 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
  95  ex_intro: ∀x:A.Q x → ex A Q.
  96
  97 interpretation "exists" 'exists x = (ex ? x).
  98
  99 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 100  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 101
 102 ndefinition iff ≝
 103 λA,B.(A → B) ∧ (B → A).
 104
 105 (* higher_order_defs/relations *)
 106
 107 ndefinition relation : Type → Type ≝
 108 λA:Type.A → A → Prop.
 109
 110 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 111 λA.λR.∀x:A.R x x.
 112
 113 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 114 λA.λR.∀x,y:A.R x y → R y x.
 115
 116 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 117 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 118
 119 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 120 λA.λR.∀x:A.¬ (R x x).
 121
 122 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 123 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 124
 125 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 126 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 127
 128 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 129 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 130
 131 (* logic/equality.ma *)
 132
 133 ninductive eq (A:Type) (x:A) : A → Prop ≝
 134  refl_eq : eq A x x.
 135
 136 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 137
 138 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 139
 140 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
 141  #T1; #T2; #x; #y; #f; #H;
 142  nrewrite < H;
 143  napply refl_eq.
 144 nqed.
 145
 146 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.
 147  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
 148  nrewrite < H1;
 149  nrewrite < H2;
 150  napply refl_eq.
 151 nqed.
 152
 153 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
 154  #T1; #T2; #x; #y; #f;
 155  nnormalize; #H; #H1;
 156  napply (H (eq_f … H1)).
 157 nqed.
 158
 159 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 160  #A;
 161  nnormalize;
 162  #x; #y; #H;
 163  nrewrite < H;
 164  napply refl_eq.
 165 nqed.
 166
 167 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 168  #A; #x; #P; #H; #y; #H1;
 169  nrewrite < (symmetric_eq … H1);
 170  napply H.
 171 nqed.
 172
 173 ndefinition relationT : Type → Type → Type ≝
 174 λA,T:Type.A → A → T.
 175
 176 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 177 λA,T.λR.∀x,y:A.R x y = R y x.
 178
 179 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 180 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).