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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/pts.ma".
  28
  29 (* ********************************** *)
  30 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
  31 (* ********************************** *)
  32
  33 (* logic/connectives.ma *)
  34
  35 ninductive True: Prop ≝
  36  I : True.
  37
  38 ndefinition True_ind : ΠP:Prop.P → True → P ≝
  39 λP:Prop.λp:P.λH:True.
  40  match H with [ I ⇒ p ].
  41
  42 ndefinition True_rec : ΠP:Set.P → True → P ≝
  43 λP:Set.λp:P.λH:True.
  44  match H with [ I ⇒ p ].
  45
  46 ndefinition True_rect : ΠP:Type.P → True → P ≝
  47 λP:Type.λp:P.λH:True.
  48  match H with [ I ⇒ p ].
  49
  50 ninductive False: Prop ≝.
  51
  52 ndefinition False_ind : ΠP:Prop.False → P ≝
  53 λP:Prop.λH:False.
  54  match H in False return λH1:False.P with [].
  55
  56 ndefinition False_rec : ΠP:Set.False → P ≝
  57 λP:Set.λH:False.
  58  match H in False return λH1:False.P with [].
  59
  60 ndefinition False_rect : ΠP:Type.False → P ≝
  61 λP:Type.λH:False.
  62  match H in False return λH1:False.P with [].
  63
  64 ndefinition Not: Prop → Prop ≝
  65 λA.(A → False).
  66
  67 interpretation "logical not" 'not x = (Not x).
  68
  69 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  70  #A; #C; #H;
  71  nnormalize;
  72  #H1;
  73  nelim (H1 H).
  74 nqed.
  75
  76 nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
  77  #A; #B; #H;
  78  nnormalize;
  79  #H1; #H2;
  80  nelim (H1 (H H2)).
  81 nqed.
  82
  83 ninductive And (A,B:Prop) : Prop ≝
  84  conj : A → B → (And A B).
  85
  86 ndefinition And_ind : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
  87 λA,B:Prop.λP:Prop.λf:A → B → P.λH:And A B.
  88  match H with [conj H1 H2 ⇒ f H1 H2 ].
  89
  90 ndefinition And_rec : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
  91 λA,B:Prop.λP:Set.λf:A → B → P.λH:And A B.
  92  match H with [conj H1 H2 ⇒ f H1 H2 ].
  93
  94 ndefinition And_rect : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
  95 λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
  96  match H with [conj H1 H2 ⇒ f H1 H2 ].
  97
  98 interpretation "logical and" 'and x y = (And x y).
  99
 100 nlemma proj1: ∀A,B:Prop.A ∧ B → A.
 101  #A; #B; #H;
 102  napply (And_ind A B ?? H);
 103  #H1; #H2;
 104  napply H1.
 105 nqed.
 106
 107 nlemma proj2: ∀A,B:Prop.A ∧ B → B.
 108  #A; #B; #H;
 109  napply (And_ind A B ?? H);
 110  #H1; #H2;
 111  napply H2.
 112 nqed.
 113
 114 ninductive Or (A,B:Prop) : Prop ≝
 115   or_introl : A → (Or A B)
 116 | or_intror : B → (Or A B).
 117
 118 ndefinition Or_ind : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
 119 λA,B:Prop.λP:Prop.λf1:A → P.λf2:B → P.λH:Or A B.
 120  match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].
 121
 122 interpretation "logical or" 'or x y = (Or x y).
 123
 124 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 125
 126 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
 127  ex_intro: ∀x:A.Q x → ex A Q.
 128
 129 ndefinition ex_ind : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
 130 λA:Type.λQ:A → Prop.λP:Prop.λf:(Πa:A.Q a → P).λH:ex A Q.
 131  match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].
 132
 133 interpretation "exists" 'exists x = (ex ? x).
 134
 135 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
 136  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 137
 138 ndefinition ex2_ind : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
 139 λA:Type.λQ,R:A → Prop.λP:Prop.λf:(Πa:A.Q a → R a → P).λH:ex2 A Q R.
 140  match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].
 141
 142 ndefinition iff ≝
 143 λA,B.(A -> B) ∧ (B -> A).
 144
 145 (* higher_order_defs/relations *)
 146
 147 ndefinition relation : Type → Type ≝
 148 λA:Type.A → A → Prop.
 149
 150 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 151 λA.λR.∀x:A.R x x.
 152
 153 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
 154 λA.λR.∀x,y:A.R x y → R y x.
 155
 156 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
 157 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
 158
 159 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
 160 λA.λR.∀x:A.¬ (R x x).
 161
 162 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
 163 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
 164
 165 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
 166 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
 167
 168 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 169 λA.λR.∀x,y:A.R x y → ¬ (R y x).
 170
 171 (* logic/equality.ma *)
 172
 173 ninductive eq (A:Type) (x:A) : A → Prop ≝
 174  refl_eq : eq A x x.
 175
 176 ndefinition eq_ind : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
 177 λA:Type.λx:A.λP:A → Prop.λp:P x.λa:A.λH:eq A x a.
 178  match H with [refl_eq ⇒ p ].
 179
 180 ndefinition eq_rec : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
 181 λA:Type.λx:A.λP:A → Set.λp:P x.λa:A.λH:eq A x a.
 182  match H with [refl_eq ⇒ p ].
 183
 184 ndefinition eq_rect : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
 185 λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
 186  match H with [refl_eq ⇒ p ].
 187
 188 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 189
 190 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
 191
 192 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
 193  #A;
 194  nnormalize;
 195  #x; #y; #H;
 196  nrewrite < H;
 197  napply (refl_eq ??).
 198 nqed.
 199
 200 nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
 201  #A; #x; #P; #H; #y; #H1;
 202  napply (eq_ind ? x ? H y ?);
 203  nrewrite < H1;
 204  napply (refl_eq ??).
 205 nqed.
 206
 207 ndefinition relationT : Type → Type → Type ≝
 208 λA,T:Type.A → A → T.
 209
 210 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 211 λA,T.λR.∀x,y:A.R x y = R y x.
 212
 213 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 214 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
 215
 216 (* list/list.ma *)
 217
 218 ninductive list (A:Type) : Type ≝
 219   nil: list A
 220 | cons: A -> list A -> list A.
 221
 222 nlet rec list_ind (A:Type) (P:list A → Prop) (p:P (nil A)) (f:(Πa:A.Πl':list A.P l' → P (cons A a l'))) (l:list A) on l ≝
 223  match l with [ nil ⇒ p | cons h t ⇒ f h t (list_ind A P p f t) ].
 224
 225 nlet rec list_rec (A:Type) (P:list A → Set) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
 226  match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rec A P p f t) ].
 227
 228 nlet rec list_rect (A:Type) (P:list A → Type) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
 229  match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rect A P p f t) ].
 230
 231 nlet rec append A (l1: list A) l2 on l1 ≝
 232  match l1 with
 233   [ nil => l2
 234   | (cons hd tl) => cons A hd (append A tl l2) ].
 235
 236 notation "hvbox(hd break :: tl)"
 237   right associative with precedence 47
 238   for @{'cons $hd $tl}.
 239
 240 notation "[ list0 x sep ; ]"
 241   non associative with precedence 90
 242   for ${fold right @'nil rec acc @{'cons $x $acc}}.
 243
 244 notation "hvbox(l1 break @ l2)"
 245   right associative with precedence 47
 246   for @{'append $l1 $l2 }.
 247
 248 interpretation "nil" 'nil = (nil ?).
 249 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 250 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 251
 252 nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
 253  #T; #x1; #x2; #y1; #y2; #H;
 254  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
 255  nrewrite < H;
 256  nnormalize;
 257  napply (refl_eq ??).
 258 nqed.
 259
 260 nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
 261  #T; #x1; #x2; #y1; #y2; #H;
 262  nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
 263  nrewrite < H;
 264  nnormalize;
 265  napply (refl_eq ??).
 266 nqed.
 267
 268 nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
 269  #T; #x; #y; #H;
 270  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
 271  nrewrite > H;
 272  nnormalize;
 273  napply I.
 274 nqed.
 275
 276 nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
 277  #T; #x; #y; #H;
 278  nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
 279  nrewrite < H;
 280  nnormalize;
 281  napply I.
 282 nqed.
 283
 284 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
 285  #T; #l;
 286  napply (list_ind T ??? l);
 287  nnormalize;
 288  ##[ ##1: napply (refl_eq ??)
 289  ##| ##2: #x; #y; #H;
 290           nrewrite > H;
 291           napply (refl_eq ??)
 292  ##]
 293 nqed.
 294
 295 nlemma associative_list : ∀T.associative (list T) (append T).
 296  #T; #x; #y; #z;
 297  napply (list_ind T ??? x);
 298  nnormalize;
 299  ##[ ##1: napply (refl_eq ??)
 300  ##| ##2: #a; #b; #H;
 301           nrewrite > H;
 302           napply (refl_eq ??)
 303  ##]
 304 nqed.
 305
 306 nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
 307  #T; #l1; #l2; #a;
 308  nnormalize;
 309  napply (refl_eq ??).
 310 nqed.
 311
 312 nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
 313  #T; #a; #l; #l1;
 314  nrewrite > (associative_list T l [a] l1);
 315  nnormalize;
 316  napply (refl_eq ??).
 317 nqed.