matita/matita/projdat/tuples.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "projdat/coerc.ma".
  16
  17 (**************************************************************************)
  18 (*                Definizione di alcuni lemmi sulle liste                 *)
  19 (**************************************************************************)
  20 lemma list_tail: ∀A:DeqSet. ∀a:A. ∀b:DeqList A. (tail A (a::b))=b. // qed.
  21 lemma list_head: ∀A:DeqSet. ∀a,c:A. ∀b:DeqList A. (hd A (a::b) c)=a. // qed.
  22 lemma list_lhdtl: ∀A:DeqSet. ∀a:A. ∀b,l:DeqList A. l=a::b → (a=hd ? l a)∧(b=tail ? l).
  23 #A #a #b #l #Hp destruct normalize /2/ qed.
  24 lemma list_hdtll: ∀A:DeqSet. ∀a:A. ∀b,l:DeqList A. a::b=l → (a=hd ? l a)∧(b=tail ? l).
  25 #A #a #b #l #Hp destruct normalize /2/ qed.
  26 (***************************************************************************)
  27
  28 (* Definizione di istanza di una tupla *)
  29 definition tup_Inst ≝ DeqList DeqCoer.
  30 (* Definizione di uno schema di tupla *)
  31 definition tup_Sche ≝ DeqList DeqType.
  32
  33 (* Dato un'istanza di tupla, riottiene il suo schema *)
  34 definition getSchema : tup_Inst → tup_Sche ≝
  35   λl. map DeqCoer DeqType getType l.
  36
  37 (* PRIMA DEFINIZIONE DI UNA TUPLA:
  38    1) Data una lista di schemi ed uno d'istanze, quest'ultimo rispetta i tipi
  39       della prima
  40  *)
  41 definition tuple ≝ λt. DeqSig tup_Inst (λc. t=(getSchema c)).
  42     (* Funzione di creazione di una tupla di primo tipo *)
  43 definition mk_tuple : ∀s:tup_Sche. tup_Inst → ? → tuple s ≝
  44 λs:tup_Sche.λt:tup_Inst.λp. mk_Sig tup_Inst (λc. s=(getSchema c)) t p.
  45
  46 (* Funzioni di equivalenza da getSchema nulla *)
  47 lemma gSchema_void: ∀tup. tup= [] → []=getSchema tup.
  48 #t elim t -t //
  49   #Coer #ld #IH #Hp >Hp normalize @refl
  50   qed.
  51
  52
  53 lemma gSchema_hd: ∀a,b. getSchema(a::b)=(getType a)::(getSchema b).
  54 #a elim a -a #el #l // qed.
  55
  56 lemma gSchema_void2: ∀tup. []=getSchema tup→tup=[].
  57 #t elim t -t //
  58   #Coer elim Coer -Coer #C #LD #IH #Hp >gSchema_hd in Hp; #Hp
  59   @False_ind
  60   destruct qed.
  61
  62 lemma gSchema_hdtl: ∀a,b,c,d. a::b=getSchema(c::d)→a::b=(getType c)::(getSchema d).
  63 #a #b #c #d >gSchema_hd #hp @hp qed.
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74 (* SECONDA DEFINIZIONE DI UNA TUPLA:
  75     2) È un tipo, dove la prima definizione viene inglobata assieme allo schema,
  76        ed incorporata in un unico dato
  77  *)
  78 record tuple_cast : Type[0] ≝ {
  79   Schema : tup_Sche;
  80   Tuple  : tuple Schema
  81 }.
  82
  83 (* Lo schema di una tuple_cast è esattamente quello di parametro del suo tipo Σ *)
  84 lemma schemais:
  85 ∀t,ldt,dc,ldc,t2.
  86 Schema ( (mk_tuple_cast (t::ldt) «dc::ldc,t2») )=t::ldt. // qed.
  87
  88 (* Conversione 2 ⇒ 1 *)
  89 definition tc_to_t : ∀s:tuple_cast.  (tuple (Schema s)).
  90 * #s #u @u qed.
  91
  92 (* Conversione 1 ⇒ 2 *)
  93 definition t_to_tc : ∀S. tuple S → tuple_cast ≝ λS,x. mk_tuple_cast S x.
  94
  95 (* Lemmi di preservazione della struttura dati: 2 ⇒ 1 ⇒ 2 *)
  96 lemma tc_t_tc : ∀x. t_to_tc (Schema x) (tc_to_t x) =x.
  97 * #s #t normalize // qed.
  98 (* Lemmi di preservazione della struttura dati: 1 ⇒ 2 ⇒ 1 *)
  99 lemma t_tc_t: ∀s,t. tc_to_t (t_to_tc s t) = t.
 100 #s #t normalize // qed.
 101
 102 lemma base_coerc1: ∀x. (getType (CNat x))=Nat. // qed.
 103 lemma base_coerc2: ∀x. (getType (CBool x))=Bool. // qed.
 104
 105 (* Definizione di una tupla con un singolo elemento: questa può essere effettuata
 106    fornendo unicamente il valore del dato (1)
 107  *)
 108 definition singleton: ∀c:DeqCoer. tuple [getType c].
 109 * #V
 110   [ >base_coerc1 @(mk_tuple [Nat] [CNat V] (refl ? [Nat]))
 111   | >base_coerc2 @(mk_tuple [Bool] [CBool V] (refl ? [Bool]))]. qed.
 112
 113 (* Definizione di tuple vuote rispettivamente di tipo 1 e 2 *)
 114 definition voideton: tuple []. @(mk_tuple [] [] (refl ? [])) qed.
 115 definition voideton2 ≝ mk_tuple_cast [] voideton.
 116
 117 lemma voideton_eq: ∀t:tuple[]. mk_tuple_cast [] t = voideton2.
 118 * #inst elim inst
 119   [ #prop normalize @eq_f destruct //
 120   | #dc #ldc #IH #AI lapply (gSchema_void2 … AI) #AI2 destruct
 121   ]
 122 qed.
 123
 124 (******************************************************************************)
 125
 126
 127
 128
 129
 130
 131 (**************************************************)
 132 (* Definizione della funzione di proiezione per 1 *)
 133 (**************************************************)
 134 (* Funzione per la restituzione del tipo di dato opportuno dato un valore opzionale *)
 135 definition optScheme : option DeqCoer→tup_Sche ≝  λu.
 136  match u with
 137  [ None ⇒ [ ]
 138  | Some a ⇒ [getType a]].
 139
 140 (* Funzione per l'istanziazione della tupla dal risultato della coercizione *)
 141 definition proj_5t: ∀x:option DeqCoer. tuple (optScheme x).
 142 * [ @voideton
 143   | #arg @(singleton arg)] qed.
 144
 145 (* Funzione di proiezione per 1 *)
 146 definition proj_t1: ∀s:tup_Sche.∀t:tuple s. ℕ→tuple ?.
 147 [ #s #t #i @(proj_5t (nth_opt ? i (Sig_fst ? ? t) )) ] skip qed.
 148
 149 (* Definizione della proiezione in posizione (S n)-esima *)
 150 lemma optScheme1:
 151   ∀n,dc,ld.
 152   optScheme (nth_opt DeqCoer (S n) (dc::ld))=optScheme (nth_opt DeqCoer n ld).
 153
 154 #n #dc #ld normalize // qed.
 155
 156
 157
 158
 159
 160 (**************************************************)
 161 (* Definizione della funzione di proiezione per 2 *)
 162 (**************************************************)
 163 definition proj_t2 ≝ λtc,i.
 164 match nth_opt ? i (Sig_fst ? ? (Tuple tc)) with
 165 [ None ⇒ mk_tuple_cast [] voideton
 166 | Some a ⇒ mk_tuple_cast [getType a] (singleton a)].
 167
 168 (* Lemmi sulla funzione di proiezione *)
 169 lemma proj_t2_null: ∀i. proj_t2 voideton2 i = voideton2.
 170 #i normalize // qed.
 171 lemma proj_t2_head: ∀a. proj_t2 (mk_tuple_cast [getType a] (singleton a)) O = mk_tuple_cast [getType a] (singleton a).
 172 #a elim a -a // qed.
 173 lemma proj_t2_head_N: ∀a,i. proj_t2 (mk_tuple_cast [getType a] (singleton a)) (S i)=voideton2.
 174 #a elim a -a // qed.
 175
 176
 177 (******************************************************************************)
 178
 179 (* Definizione di proiezione dell'elemento (S x)-esimo elemento per ogni tipo di
 180 tupla *)
 181 theorem proj_t1_tl: ∀dt,ldt,ld,IH,prop,pos.
 182
 183     (proj_t1 (dt::ldt) «ld::IH,prop» (S pos)) = (proj_t1 (ldt) «IH,?» (pos)).
 184
 185 [ #d #ld #dc #ldl #prop #pos //
 186 | lapply (list_hdtll … prop) * >list_tail >list_head
 187   #h @(rewrite_r … (getSchema IH)) //
 188 ] qed.
 189
 190
 191
 192 (* Rappresentazione di una lista di "tipi" dalla rappresentazione del valore *)
 193 lemma proj_t2_tl_deq_Type:
 194 ∀dt:DeqType. ∀ldt:list DeqType. ∀ld:DeqCoer.
 195 ∀IH:list DeqCoer.∀prop: dt::ldt=getSchema (ld::IH).
 196
 197      (ldt=getSchema IH).
 198
 199 #d #ld #dc #ldl #prop
 200 lapply (list_hdtll … prop) * >list_tail >list_head
 201   #h @(rewrite_r … (getSchema ldl)) // qed.
 202
 203
 204
 205 (* Definizione della proiezione sul secondo tipo di tupla *)
 206 theorem proj_t2_tl :  ∀dt,ldt,ld,IH,prop,pos.
 207
 208     proj_t2 (t_to_tc (dt::ldt) «ld::IH,prop») (S pos)
 209       = proj_t2 (t_to_tc ldt «IH,?») pos.
 210
 211 [ #d #ld #dc #ldl #prop #pos //
 212 | @(proj_t2_tl_deq_Type dt ldt ld IH prop)
 213 ] qed.
 214
 215
 216
 217 (******************************************************************************)
 218
 219 (* Una tupla vuota per 1) è un voideton 2) *)
 220 lemma t_to_tc_void_as_voideton2 : ∀t: tuple [].        t_to_tc [] t = voideton2.
 221   #t elim t
 222   #tup #prop
 223   normalize lapply (gSchema_void2 … prop) #Hp
 224   destruct normalize
 225   //
 226 qed.
 227
 228
 229
 230 (* Una qualunque proiezione di un tipo di tupla 1) restituirà nessun elemento *)
 231 lemma voidopt_lemma: ∀t,pos.
 232  (nth_opt DeqCoer pos (Sig_fst tup_Inst (λc:tup_Inst.[]=getSchema c) t))
 233     = None DeqCoer.
 234 #t elim t -t #is #prop #n lapply (gSchema_void2 … prop) #Hp destruct
 235    normalize // qed.
 236
 237
 238
 239 lemma void_optS:             (optScheme (None DeqCoer)) = [].            // qed.
 240 lemma void_tup: (tuple (optScheme (None DeqCoer)))= tuple []. >void_optS // qed.
 241
 242
 243
 244 (* Valutazione di una proiezione di tupla vuota 1) come eq_rect_Type0_r  *)
 245 lemma proj_nothing_void : ∀t:tuple []. ∀pos. (proj_t1 [] t pos)= ?.
 246 [ 2: >voidopt_lemma  >void_tup @t
 247 | #t elim t -t #s #prop lapply (gSchema_void2 … prop) #Hp #pos
 248   destruct normalize // qed.
 249 (* check proj_nothing_void *)
 250 lemma proj_nothing_voideton: ∀pos. proj_t2 voideton2 pos = voideton2.
 251 #n elim n -n normalize // qed.
 252
 253 (* Valutazione di una proiezione di una tupla vuota 2) come voideton2
 254 lemma t_to_c_proj1_void:
 255 ∀dt, ldt, s1,n. proj_t2 (t_to_tc (dt::ldt) «[],s1») n = voideton2. // qed.
 256 *)
 257
 258
 259
 260
 261 (* Se la restituzione di uno schema per una istanza l è a::b, allora
 262    b sarà pari allo schema ottenibile dal resto di l *)
 263 lemma gSchema_tl: ∀a,b,l.     a::b=getSchema l → b = getSchema (tail DeqCoer l).
 264
 265 #a @listD_elim2
 266   [ #n #l elim l -l
 267     [ #Hp normalize in Hp; normalize destruct
 268     | #dc #ldc #IH #Hp >list_tail lapply (list_lhdtl …Hp)  *
 269       >list_head #oH1 >list_tail @(rewrite_l … (getSchema ldc)) //]
 270   | #ldt #el1 -el1 #l elim l -l
 271     [ #Hp //
 272     | #DC #ldc #IH #hp >list_tail lapply (list_hdtll … hp) -hp
 273       >list_head >list_tail * #oh1 @(rewrite_r … (getSchema ldc)) //
 274     ]
 275   | #ldt #m #d -d -ldt #u #IH  #l elim l
 276     [ #Hp lapply (IH … []) normalize #banal normalize in Hp; destruct
 277     | #dc #ldc #IH #e1 >list_tail lapply (list_hdtll … e1) >list_head
 278       * #oh1 >list_tail @(rewrite_r … (getSchema ldc)) //
 279     ]
 280   | @([a])
 281   ]
 282 qed.
 283
 284
 285 lemma gSchema_tltl: ∀b,l.     b=getSchema l → tail DeqType b = getSchema (tail DeqCoer l).
 286 #b elim b -b
 287   [ #l #prop lapply(gSchema_void2 … prop) #lP >lP normalize //
 288   | #dT #ldT #IH #tI #Hp whd in ⊢ (?? % ?); lapply (gSchema_tl … Hp) -Hp
 289     #Hp //
 290   ]
 291 qed.
 292
 293
 294
 295 lemma gSchema_rest: ∀a,b,e,l.         a::b=getSchema (e::l) → b = getSchema (l).
 296 #a #b #e #l @gSchema_tl qed.
 297
 298 (* "Coercizione" per eq_rect_Type0_r *)
 299 theorem coerc1:
 300 ∀ t,pos.t_to_tc
 301    (optScheme
 302     (nth_opt DeqCoer pos (Sig_fst tup_Inst (λc:tup_Inst.[]=getSchema c) t)))
 303    (proj_t1 [] t pos)
 304    =
 305    mk_tuple_cast [] t.
 306
 307 #t #pos>proj_nothing_void >voidopt_lemma normalize // qed.
 308
 309
 310
 311
 312 (******************************************************************************)
 313
 314 (* Equivalenza tra schemi nell'elemento (S pos)-esimo *)
 315 lemma nthopt_S: ∀pos,t,ldt,dc,ldc,t2.
 316
 317   (nth_opt DeqCoer (S pos)
 318       (Sig_fst tup_Inst (λc:tup_Inst.t::ldt=getSchema c)
 319        (tc_to_t (mk_tuple_cast (t::ldt) «dc::ldc,t2»))))  =
 320   (nth_opt DeqCoer ( pos)
 321       (Sig_fst tup_Inst (λc:tup_Inst.ldt=getSchema c)
 322        (tc_to_t (mk_tuple_cast (ldt) «ldc,?»)))).
 323
 324 [ #p #dt #ldt #dc #ldc #hp normalize //
 325 | lapply (gSchema_tl … t2)  #t3 normalize in t3;
 326   normalize @t3
 327 ] qed.
 328
 329
 330 (* Specializzazione del caso precedente, tramite estrazione diretta della
 331    componente dello schema *)
 332 lemma nthopt_S2: ∀pos,t,ldt,dc,ldc,t2.
 333
 334   (nth_opt DeqCoer (S pos)
 335       (Sig_fst tup_Inst (λc:tup_Inst.t::ldt=getSchema c)
 336        (tc_to_t (mk_tuple_cast (t::ldt) «dc::ldc,t2»))))=
 337   (nth_opt DeqCoer pos ldc).
 338
 339 #pos #dt #ldt #dc #ldc #p >nthopt_S normalize // qed.
 340
 341 (******************************************************************************)
 342
 343
 344
 345
 346
 347 (* Qualsiasi proiezione di uno schema vuoto è esso stesso uno schema vuoto *)
 348 lemma coerc2: ∀t:tuple [].∀pos.  (Schema (proj_t2 (mk_tuple_cast [] t) pos))=[].
 349
 350 * #ti #prop #p >voideton_eq normalize @refl qed.
 351
 352
 353
 354 lemma coerc3 :  ∀t,ldt,ins,prop.
 355
 356 (Sig_fst tup_Inst (λc:tup_Inst.t::ldt=getSchema c)
 357          (tc_to_t (mk_tuple_cast (t::ldt) «ins,prop»)))=ins.
 358
 359 #dt #ldt #ti #p normalize @refl qed.
 360
 361
 362
 363
 364 (* Le due definizioni di proiezione di tupla preservano la proiezione per il
 365    tipo 1) lungo le funzioni di conversione per 2) *)
 366 theorem preservation1:
 367 ∀s,t,i. proj_t2 (t_to_tc s t) i = (t_to_tc ? (proj_t1 s t i)).
 368 #s elim s -s
 369   [ #t #pos >t_to_tc_void_as_voideton2
 370             >proj_nothing_voideton
 371             >coerc1
 372             normalize elim t
 373             #p #prop
 374             lapply (gSchema_void2 … prop)
 375             #Hp destruct //
 376   | #dt #ldt #IH
 377     #t elim t -t
 378        #el1 elim el1 -el1
 379     [ #prop #pos normalize //
 380     | #ld #IH #Hp #prop #pos elim pos -pos
 381       [ normalize //
 382       | #pos #Hp2 >proj_t1_tl >proj_t2_tl //
 383       ]
 384     ]
 385   ]
 386 qed.
 387
 388
 389
 390
 391 (* Equivalenza tra schemi di tuple cast *)
 392 lemma eqSchema: ∀a,b:tuple_cast.                    a=b → (Schema a)=(Schema b).
 393 * #ts1 #t1 * #ts2 #t2 #Hp destruct @refl qed.
 394
 395
 396
 397
 398 (* Data una tuple_schema a ed uno schema b, se i due schemi sono uguali,
 399    allora posso restituire una tupla di schema b *)
 400 lemma tTupleSchema: ∀a,b.                                (Schema a)=b → tuple b.
 401 * #schema #inst #bschema #ref <ref @inst qed.
 402
 403
 404
 405 (* Data una tupla a di schema s ed uno schema b, se s=b allora restituisco
 406    la tupla come di schema b *)
 407 lemma tTuple: ∀s,b. ∀a:tuple s.                                   s=b → tuple b.
 408 #a #b #inp #ref <ref @inp qed.
 409
 410
 411
 412 (* Identità di t tra funzioni *)
 413 lemma tctt_void_preservation: ∀t:tuple [].   (tc_to_t (mk_tuple_cast [] t)) = t.
 414 * #p #pr normalize @refl qed.