1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "projdat/tuples.ma".
17 (* Computazione dello schema come proiezione (S pos)-esima *)
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) //
27 (******************************************************************************)
29 (* Rappresentazione dell'ottenimento di uno schema di una proiezione su tupla
30 come la selezione del pos-esimo elemento dalla lista
34 (Schema (proj_t2 (mk_tuple_cast (ldt) «ldc,t2») ( pos))
35 =optScheme (nth_opt DeqCoer pos ldc)).
46 lapply (gSchema_void2 … prop)
47 #IH3 >IH3 normalize @refl
54 #prop #pos elim pos -pos
57 lapply (gSchema_rest … prop)
59 lapply (IH lc prop2 i)
71 (* A questo punto debbo prima dimostrare che le tuple generate hanno lo stesso
72 schema, e quindi hanno lo stesso tipo di dato.
76 (Schema (proj_t2 t i))=(optScheme
78 (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))).
80 [ #pos >coerc2 >tctt_void_preservation >voidopt_lemma normalize @refl
81 | #ldt #IH -IH * #ins elim ins -ins
84 | #dc #ldc #IH2 -IH2 #t2 #pos
89 lapply (gSchema_rest … t2)
98 lemma coercition2_tuple: ∀t,i.
100 (tuple (Schema (proj_t2 t i)))
102 (tuple (optScheme (nth_opt DeqCoer i
103 (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t))))).
105 #t #i @eq_f @coercition2
110 lemma coercition2_tuple_transform: ∀t,i.
111 (tuple (Schema (proj_t2 t i)))→
114 (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t))))).
116 #t #i #Hp <coercition2_tuple @Hp qed.
119 lemma coercition2_tuple_transform2: ∀t,i.
122 (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))))
124 (tuple (Schema (proj_t2 t i))).
125 #t #i #Hp >coercition2_tuple @Hp qed.
131 #s #ts normalize // qed.
133 lemma coercition2_tuple_transform_T: ∀t,i.
134 (tuple (Schema (proj_t2 t i)))→
137 (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (Tuple t))))).
142 lemma coercition2_tuple_transform2_T: ∀t,i.
145 (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (Tuple t)))))
147 (tuple (Schema (proj_t2 t i))).
153 theorem preservation2:
155 proj_t1 (Schema t) (Tuple t) i = (tc_to_t (proj_t2 t i)).
158 ********** DISAMBIGUATION ERRORS: **********
159 ***** Errors obtained during phases 1: *****
160 *Error at 70-91: The term
161 (tc_to_t (proj_t2 t i))
163 (tuple (Schema (proj_t2 t i)))
164 but is here used with type
168 (Sig_fst tup_Inst (\lambda c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))))
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.
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.
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.