]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/projdat/nth_proj.ma
fixing
[helm.git] / matita / matita / projdat / nth_proj.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/tuples2.ma".
16
17 (* Funzione di unione tra tuple di tipo 1 *)
18 definition tup1_union: ∀S,T. tuple S → tuple T → tuple (S @T).
19
20   [*
21     [ #u #_ @u
22     | #d #l #t #r @r
23     ]
24   | #d #ld #ts1 * #e1 #p1 * #e2 #p2 %
25     [ @(e1@e2) | >p1 >p2 normalize // 
26     ]
27   ]
28 qed.
29
30 (* Definizione della funzione di proiezione n-esima su valori *)
31 let rec tup1_projval (l:DeqList DeqNat) s (t:tuple s) : DeqList DeqCoer≝ 
32   match l with
33   [ nil ⇒ []
34   | cons a b ⇒ match (nth_opt ? a (Sig_fst ? ? t) ) with
35             [None ⇒ tup1_projval b s t
36             |Some w ⇒ w::(tup1_projval b s t)]
37   ].
38
39 (* Definizione della funzione di proiezione n-aria *)
40 definition tup1_projection ≝  λl,s,t. mk_tuple (getSchema (tup1_projval l s t)) (tup1_projval l s t) (refl ? ? ).
41
42 (******************************************************************************)
43
44 lemma gSchema_merge: ∀s1,i1,s2,i2.
45 (s1=getSchema i1)→(s2=getSchema i2)→(s1@s2=getSchema(i1@i2)).
46 #a #b #c#d #Hp #Hp2 >Hp >Hp2 normalize // qed.
47
48 definition tup2_union : tuple_cast→tuple_cast→tuple_cast.
49 * #s1 * #i1 #p1 * #s2 * #i2 #p2 % 
50   [ @(s1@s2)
51   | lapply(gSchema_merge … p1 p2) -p1 -p2 #P %
52     [ @(i1@i2)
53     | @P
54     ]
55   ]
56 qed.
57
58 definition tup2_projval  ≝ λl,c. tup1_projval l (Schema c) (Tuple c).
59
60 definition tup2_projection : list DeqNat→tuple_cast→tuple_cast.
61 #ids #tc %
62   [ @(getSchema (tup2_projval ids tc))
63   | % [ @(tup2_projval ids tc) | // ]]
64 qed.
65   
66 (******************************************************************************)
67 lemma gSchema_unpack:
68 ∀X,lX. (tail DeqType []=getSchema (tail DeqCoer (X::lX)))→([]=getSchema lX).
69 #dc #ldc normalize // qed.
70
71
72 lemma lemmata_tl_void0: ∀n,ld,dc,l,P. 
73
74 (tup1_projval (n::ld) [] «dc::l,P»=tup1_projval (ld) [] «dc::l,?»).
75 [ 2: @P
76 | #n #ln #d #ld #p lapply (gSchema_void2 … p) #pp >pp in p;
77   #e normalize //
78 ]
79 qed.
80
81 lemma lemmata_t1_void1: ∀dc, ldc,p,rpl. tup1_projval rpl [] «dc::ldc,p»=[].
82 #dc #l #P #m elim m -m 
83   [ //
84   | #n #ld #IH >lemmata_tl_void0 @IH]
85 qed.
86
87 lemma lemmata_t1_void2: ∀ ldc,p,rpl. tup1_projval rpl [] «ldc,p»=[].
88 #l #P #m elim m -m 
89   [ //
90   | #n #ld #IH lapply (gSchema_void2 … P) #pp >pp in P; #P normalize
91     elim ld -ld
92       [ //
93       | #dn #ldn #IH normalize @IH]
94   ]
95 qed.
96
97 lemma tup1_void_tl:
98 ∀rpl,X,lX,P. (tup1_projval rpl [] «X::lX,P»=tup1_projval rpl [] «lX,?»).
99   [ 2: lapply (gSchema_tltl … P) #Hp 
100        lapply (gSchema_unpack … Hp) -Hp #Hp @Hp
101   | #rpl #dc #ldc #p >lemmata_t1_void1 >lemmata_t1_void2 //
102   ]
103 qed.
104
105 lemma tup1_voidt: ∀t,plist. (tup1_projval plist [] t) = [].
106 #t elim t -t #p elim p -p 
107   [ normalize #u #pl elim pl -pl
108     [ normalize //
109     | #n #ln #IH normalize @IH
110     ]
111   | #X  #lX #IH #P #rpl 
112     lapply (gSchema_tltl … P) #tl lapply (gSchema_unpack … tl) -tl #tl
113     lapply (IH tl) -IH #IH lapply (IH … rpl) -IH #IH 
114     >lemmata_t1_void2 //]
115 qed.
116
117
118 (******************************************************************************)
119 (* Dimostrazioni delle proprietà della seconda proiezione *)
120
121 lemma voideton_proj_list_indiff:
122 ∀l,n.
123 (tup2_projection (l::n) voideton2=tup2_projection (n) voideton2).
124 #l #d normalize // qed.
125
126
127 lemma voideton_proj : ∀plist. tup2_projection plist voideton2 = voideton2.
128 #p elim p -p
129   [ normalize //
130   | #dn #ldn #HP >voideton_proj_list_indiff @HP] qed.
131
132
133 (******************************************************************************)
134 (* Lemmi accessori *)
135
136 lemma gSchema_t1: ∀plist,t. (getSchema (tup1_projval plist [] t))=[].
137 #p #t >tup1_voidt  normalize // qed.
138
139
140 lemma gSchema_null: getSchema [] = [].
141 normalize // qed.
142
143 lemma t_to_tcV:
144 ∀plist,t.
145 t_to_tc (getSchema (tup1_projval plist [] t)) (tup1_projection plist [] t)=
146 t_to_tc (getSchema []) ?.
147 [ 2: >gSchema_null @t
148 | #pl * #p #n  >gSchema_null lapply (gSchema_void2 … n) #N destruct
149   elim pl -pl
150     [ //
151     | #dn #ld #IH normalize  normalize in IH; @IH
152     ]
153 qed.
154
155 (******************************************************************************)
156
157 (*
158   Si dimostra che le funzioni di proiezione preservano i contenuti delle tuple,
159   mantenendolo inalterato a meno di proiezione.
160  *)
161
162 theorem preservation3: ∀s,t,l. tup2_projection l (t_to_tc s t)  = (t_to_tc ? (tup1_projection l s t )).
163 #s elim s -s
164   [ #t #plist >t_to_tc_void_as_voideton2
165               >voideton_proj
166               >t_to_tcV
167               normalize
168               elim t #p #gs
169               lapply (gSchema_void2 … gs)
170               #L destruct //
171   | #dt #ldt #IH
172     * #p #prop #ln
173     normalize //
174   ]
175 qed.
176
177 theorem preservation4: ∀t,l. 
178 (tup1_projection l (Schema t) (Tuple t)) = tc_to_t (tup2_projection l t ).
179 normalize // qed.
180
181 (* Si può notare come le funzioni che sono state qui fornite rendono confrontabili
182    le tuple, non rendendo più necessarie funzioni di coercizione, come invece
183    era necessario per i singoletti di tuple.
184  *)