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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  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 (*
  61 naxiom RAA : ∀P:Prop.∀f:(¬P) → False.P.
  62
  63 nlemma nnprop_to_prop : ∀P.(¬¬P) → P.
  64  #P; nchange with (((¬P) → False) → P);
  65  #H; napply (RAA P H).
  66 nqed.
  67 *)
  68
  69 ninductive And (A,B:Prop) : Prop ≝
  70  conj : A → B → (And A B).
  71
  72 interpretation "logical and" 'and x y = (And x y).
  73
  74 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  75  #A; #B; #H;
  76  (* \ldots al posto di ??? *)
  77  napply (And_ind A B … H);
  78  #H1; #H2;
  79  napply H1.
  80 nqed.
  81
  82 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
  83  #A; #B; #H;
  84  napply (And_ind A B … H);
  85  #H1; #H2;
  86  napply H2.
  87 nqed.
  88
  89 ninductive Or (A,B:Prop) : Prop ≝
  90   or_introl : A → (Or A B)
  91 | or_intror : B → (Or A B).
  92
  93 interpretation "logical or" 'or x y = (Or x y).
  94
  95 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
  96
  97 (*
  98 nlemma decidable_prop : ∀P:Prop.decidable P.
  99  #P; nnormalize;
 100  napply RAA;
 101  #H;
 102  napply (absurd (P ∨ (¬P)) …);
 103  ##[ ##2: napply H
 104  ##| ##1: napply (or_intror P (¬P));
 105           napply RAA;
 106           #H1;
 107           napply (absurd (P ∨ (¬P)) …);
 108           ##[ ##2: napply H
 109           ##| ##1: napply (or_introl P (¬P));
 110                    napply (nnprop_to_prop P H1)
 111           ##]
 112  ##]
 113 nqed.
 114
 115 nlemma terzo_escluso : ∀P,G:Prop.∀ft:P → G.∀ff:(¬P) → G.G.
 116  #P; #G; nnormalize;
 117  #H; #H1;
 118  napply (Or_ind P (P → False) ? H H1 ?);
 119  napply (decidable_prop P).
 120 nqed.
 121 *)
 122
 123 nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
 124  #P; #Q; #G; #H; #H1; #H2;
 125  napply (Or_ind P Q ? H1 H2 ?);
 126  napply H.
 127 nqed.
 128
 129 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 130  ex_intro: ∀x:A.Q x → ex A Q.
 131
 132 interpretation "exists" 'exists x = (ex ? x).
 133
 134 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 135  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 136
 137 ndefinition iff ≝
 138 λA,B.(A → B) ∧ (B → A).
 139
 140 (* higher_order_defs/relations *)
 141
 142 ndefinition relation : Type → Type ≝
 143 λA:Type.A → A → Prop.
 144
 145 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 146 λA.λR.∀x:A.R x x.
 147
 148 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 149 λA.λR.∀x,y:A.R x y → R y x.
 150
 151 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 152 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 153
 154 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 155 λA.λR.∀x:A.¬ (R x x).
 156
 157 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 158 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 159
 160 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 161 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 162
 163 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 164 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 165
 166 (* logic/equality.ma *)
 167
 168 ninductive eq (A:Type) (x:A) : A → Prop ≝
 169  refl_eq : eq A x x.
 170
 171 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 172
 173 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 174
 175 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
 176  #T1; #T2; #x; #y; #f; #H;
 177  nrewrite < H;
 178  napply refl_eq.
 179 nqed.
 180
 181 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.
 182  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
 183  nrewrite < H1;
 184  nrewrite < H2;
 185  napply refl_eq.
 186 nqed.
 187
 188 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
 189  #T1; #T2; #x; #y; #f;
 190  nnormalize; #H; #H1;
 191  napply (H (eq_f … H1)).
 192 nqed.
 193
 194 (*
 195 nlemma neqf2_to_neq : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.f x1 x2 ≠ f y1 y2 → (x1 ≠ y1) ∨ (x2 ≠ y2).
 196  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; nnormalize; #H;
 197  napply (terzo_escluso (x1 = y1) …);
 198  ##[ ##2: #H1; napply (or_introl … H1)
 199  ##| ##1: #H1; napply (terzo_escluso (x2 = y2) …)
 200           ##[ ##2: #H2; napply (or_intror … H2)
 201           ##| ##1: #H2; nrewrite < H1 in H:(%);
 202                    nrewrite < H2; #H;
 203                    nelim (H (refl_eq …))
 204           ##]
 205  ##]
 206 nqed.
 207 *)
 208
 209 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 210  #A;
 211  nnormalize;
 212  #x; #y; #H;
 213  nrewrite < H;
 214  napply refl_eq.
 215 nqed.
 216
 217 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 218  #A; #x; #P; #H; #y; #H1;
 219  nrewrite < (symmetric_eq … H1);
 220  napply H.
 221 nqed.
 222
 223 ndefinition relationT : Type → Type → Type ≝
 224 λA,T:Type.A → A → T.
 225
 226 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 227 λA,T.λR.∀x,y:A.R x y = R y x.
 228
 229 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 230 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).