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  *)