helm/software/matita/contribs/ng_assembly/freescale/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 include "freescale/pts.ma".
  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 ninductive And (A,B:Prop) : Prop ≝
  56  conj : A → B → (And A B).
  57
  58 interpretation "logical and" 'and x y = (And x y).
  59
  60 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
  61  #A; #B; #H;
  62  napply (And_ind A B ?? H);
  63  #H1; #H2;
  64  napply H1.
  65 nqed.
  66
  67 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
  68  #A; #B; #H;
  69  napply (And_ind A B ?? H);
  70  #H1; #H2;
  71  napply H2.
  72 nqed.
  73
  74 ninductive Or (A,B:Prop) : Prop ≝
  75   or_introl : A → (Or A B)
  76 | or_intror : B → (Or A B).
  77
  78 interpretation "logical or" 'or x y = (Or x y).
  79
  80 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
  81
  82 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
  83  ex_intro: ∀x:A.Q x → ex A Q.
  84
  85 interpretation "exists" 'exists x = (ex ? x).
  86
  87 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  88  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
  89
  90 ndefinition iff ≝
  91 λA,B.(A -> B) ∧ (B -> A).
  92
  93 (* higher_order_defs/relations *)
  94
  95 ndefinition relation : Type → Type ≝
  96 λA:Type.A → A → Prop.
  97
  98 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
  99 λA.λR.∀x:A.R x x.
 100
 101 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 102 λA.λR.∀x,y:A.R x y → R y x.
 103
 104 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 105 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 106
 107 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 108 λA.λR.∀x:A.¬ (R x x).
 109
 110 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 111 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 112
 113 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 114 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 115
 116 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 117 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 118
 119 (* logic/equality.ma *)
 120
 121 ninductive eq (A:Type) (x:A) : A → Prop ≝
 122  refl_eq : eq A x x.
 123
 124 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 125
 126 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 127
 128 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 129  #A;
 130  nnormalize;
 131  #x; #y; #H;
 132  nrewrite < H;
 133  napply (refl_eq ??).
 134 nqed.
 135
 136 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 137  #A; #x; #P; #H; #y; #H1;
 138  nrewrite < (symmetric_eq ??? H1);
 139  napply H.
 140 nqed.
 141
 142 ndefinition relationT : Type → Type → Type ≝
 143 λA,T:Type.A → A → T.
 144
 145 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 146 λA,T.λR.∀x,y:A.R x y = R y x.
 147
 148 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 149 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
 150
 151 (* list/list.ma *)
 152
 153 ninductive list (A:Type) : Type ≝
 154   nil: list A
 155 | cons: A -> list A -> list A.
 156
 157 nlet rec append A (l1: list A) l2 on l1 ≝
 158  match l1 with
 159   [ nil => l2
 160   | (cons hd tl) => cons A hd (append A tl l2) ].
 161
 162 notation "hvbox(hd break :: tl)"
 163   right associative with precedence 47
 164   for @{'cons $hd $tl}.
 165
 166 notation "[ list0 x sep ; ]"
 167   non associative with precedence 90
 168   for ${fold right @'nil rec acc @{'cons $x $acc}}.
 169
 170 notation "hvbox(l1 break @ l2)"
 171   right associative with precedence 47
 172   for @{'append $l1 $l2 }.
 173
 174 interpretation "nil" 'nil = (nil ?).
 175 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 176 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 177
 178 nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
 179  #T; #x1; #x2; #y1; #y2; #H;
 180  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
 181  nrewrite < H;
 182  nnormalize;
 183  napply (refl_eq ??).
 184 nqed.
 185
 186 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
 187  #T; #x1; #x2; #y1; #y2; #H;
 188  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
 189  nrewrite < H;
 190  nnormalize;
 191  napply (refl_eq ??).
 192 nqed.
 193
 194 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
 195  #T; #x; #y; #H;
 196  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
 197  nrewrite > H;
 198  nnormalize;
 199  napply I.
 200 nqed.
 201
 202 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
 203  #T; #x; #y; #H;
 204  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
 205  nrewrite < H;
 206  nnormalize;
 207  napply I.
 208 nqed.
 209
 210 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
 211  #T; #l;
 212  nelim l;
 213  nnormalize;
 214  ##[ ##1: napply (refl_eq ??)
 215  ##| ##2: #x; #y; #H;
 216           nrewrite > H;
 217           napply (refl_eq ??)
 218  ##]
 219 nqed.
 220
 221 nlemma associative_list : ∀T.associative (list T) (append T).
 222  #T; #x; #y; #z;
 223  nelim x;
 224  nnormalize;
 225  ##[ ##1: napply (refl_eq ??)
 226  ##| ##2: #a; #b; #H;
 227           nrewrite > H;
 228           napply (refl_eq ??)
 229  ##]
 230 nqed.
 231
 232 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
 233  #T; #l1; #l2; #a;
 234  nnormalize;
 235  napply (refl_eq ??).
 236 nqed.
 237
 238 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
 239  #T; #a; #l; #l1;
 240  nrewrite > (associative_list T l [a] l1);
 241  nnormalize;
 242  napply (refl_eq ??).
 243 nqed.