matita/matita/projdat/tuples2.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/tuples.ma".
  16
  17 (* Computazione dello schema come proiezione (S pos)-esima *)
  18 lemma schemais2:
  19 ∀t,ldt,dc,ldc,t2,pos.
  20 Schema (proj_t2 (mk_tuple_cast (t::ldt) «dc::ldc,t2») (S pos)) =
  21 Schema (proj_t2 (mk_tuple_cast (ldt) «ldc,?») ( pos)).
  22  [ 2: @(proj_t2_tl_deq_Type t ldt dc ldc t2)
  23  | 1: #t #l #d #c #t2 #p >(proj_t2_tl) //
  24  ]
  25 qed.
  26
  27 (******************************************************************************)
  28
  29 (* Rappresentazione dell'ottenimento di uno schema di una proiezione su tupla
  30    come la selezione del pos-esimo elemento dalla lista
  31 *)
  32 lemma coerc4:
  33 ∀ldt,ldc,t2,pos.
  34  (Schema (proj_t2 (mk_tuple_cast (ldt) «ldc,t2») ( pos))
  35   =optScheme (nth_opt DeqCoer pos ldc)).
  36
  37 #ldt elim ldt -ldt
  38   [ #ldc elim ldc -ldc
  39     [ //
  40     | #c #ld #IH #prop #i
  41       elim i -i
  42       [ //
  43       | #i #IH2 >coerc2
  44         >coerc2 in IH2;
  45         #IH2
  46         lapply (gSchema_void2 … prop)
  47         #IH3 >IH3 normalize @refl
  48       ]
  49     ]
  50   | #dt #ldt #IH
  51     #ldc elim ldc -ldc
  52     [ //
  53     | #c #lc #IH2 -IH2
  54       #prop #pos elim pos -pos
  55         [ //
  56         | #i #IH3 -IH3
  57           lapply (gSchema_rest … prop)
  58           #prop2
  59           lapply (IH lc prop2 i)
  60           #IH3
  61           >optScheme1
  62           <IH3
  63           >schemais2 //
  64       ]
  65     ]
  66   ]
  67 qed.
  68
  69
  70
  71 (* A questo punto debbo prima dimostrare che le tuple generate hanno lo stesso
  72    schema, e quindi hanno lo stesso tipo di dato.
  73  *)
  74 lemma coercition2:
  75 ∀t,i.
  76 (Schema (proj_t2 t i))=(optScheme
  77   (nth_opt DeqCoer i
  78    (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))).
  79 * #ts elim ts -ts #t
  80   [ #pos >coerc2 >tctt_void_preservation  >voidopt_lemma normalize @refl
  81   | #ldt #IH -IH * #ins elim ins -ins
  82     [ #prop #pos
  83       >coerc3 normalize //
  84     | #dc #ldc #IH2 -IH2 #t2 #pos
  85       elim pos -pos
  86       [ normalize @refl
  87       | #pos  #IH3  -IH3
  88         >nthopt_S2
  89         lapply (gSchema_rest … t2)
  90         #ct2 destruct
  91         >coerc4 //
  92       ]
  93     ]
  94   ]
  95 qed.
  96
  97
  98 lemma coercition2_tuple: ∀t,i.
  99
 100 (tuple (Schema (proj_t2 t i)))
 101                =
 102 (tuple (optScheme (nth_opt DeqCoer i
 103       (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t))))).
 104
 105 #t #i @eq_f @coercition2
 106 qed.
 107
 108
 109
 110 lemma coercition2_tuple_transform:  ∀t,i.
 111 (tuple (Schema (proj_t2 t i)))→
 112   (tuple (optScheme
 113     (nth_opt DeqCoer i
 114      (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t))))).
 115
 116 #t #i #Hp <coercition2_tuple @Hp qed.
 117
 118
 119 lemma coercition2_tuple_transform2:  ∀t,i.
 120 (tuple (optScheme
 121   (nth_opt DeqCoer i
 122    (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))))
 123    →
 124       (tuple (Schema (proj_t2 t i))).
 125 #t #i #Hp >coercition2_tuple @Hp qed.
 126
 127 lemma eqTup:
 128 ∀t.
 129 tc_to_t t = Tuple t.
 130 #t elim t -t
 131  #s #ts normalize // qed.
 132
 133 lemma coercition2_tuple_transform_T:  ∀t,i.
 134 (tuple (Schema (proj_t2 t i)))→
 135   (tuple (optScheme
 136     (nth_opt DeqCoer i
 137      (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (Tuple t))))).
 138
 139 //  qed.
 140
 141
 142 lemma coercition2_tuple_transform2_T:  ∀t,i.
 143 (tuple (optScheme
 144   (nth_opt DeqCoer i
 145    (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (Tuple t)))))
 146    →
 147       (tuple (Schema (proj_t2 t i))).
 148 //  qed.
 149
 150
 151 (*
 152
 153 theorem preservation2:
 154 ∀t,i.
 155 proj_t1 (Schema t) (Tuple t) i = (tc_to_t (proj_t2 t i)).
 156 …
 157
 158 ********** DISAMBIGUATION ERRORS: **********
 159 ***** Errors obtained during phases 1: *****
 160 *Error at 70-91: The term
 161 (tc_to_t (proj_t2 t i))
 162 has type
 163 (tuple (Schema (proj_t2 t i)))
 164 but is here used with type
 165 (tuple
 166  (optScheme
 167   (nth_opt DeqCoer i
 168    (Sig_fst tup_Inst (\lambda c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))))
 169
 170 In quanto aver dimostrato l'uguaglianza dei tipi come già dimostrato non consente
 171 di poter confrontare questi due elementi, allora è necessario mostrare d'ora in
 172 poi una forma d'uguaglianza più debole.
 173
 174 *)
 175
 176
 177 theorem preservation2: ∀t,i.
 178  coercition2_tuple_transform2_T t i(proj_t1 (Schema t) (Tuple t) i) = (tc_to_t (proj_t2 t i)).
 179 #t #i normalize @refl qed.
 180
 181 theorem preservation2bis: ∀t,i.
 182  (proj_t1 (Schema t) (Tuple t) i) = coercition2_tuple_transform_T t i (tc_to_t (proj_t2 t i)).
 183 normalize #t #i @refl qed.