--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+include "basics/bool.ma".
+include "basics/lists/listb.ma".
+
+inductive coerc : Type[0] ≝
+ | CNat : nat → coerc
+ | CBool : bool → coerc.
+
+definition eq_c ≝ λa,b. match a with
+ [ CNat n ⇒ (match b with [ CNat m ⇒ eqb n m | _ ⇒ false ])
+ | CBool x ⇒ (match b with [ CBool y ⇒
+ beqb x y
+ | _ ⇒ false]
+ )
+ ].
+
+inductive type : Type[0] ≝
+ | Nat : type
+ | Bool: type.
+
+
+definition denotation_sem ≝ λn.
+ match n with
+ [ Nat ⇒ 1
+ | Bool ⇒ 2].
+(* Funzione di equivalenza tra tipi *)
+definition eqb_type ≝ λa,b. eqb (denotation_sem a) (denotation_sem b).
+definition getType : coerc → type ≝
+λ gt. match gt with
+ [ CNat _ ⇒ Nat
+ | CBool _ ⇒ Bool].
+
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "projdat/basic_type.ma".
+
+
+theorem base_iff: ∀b,y:bool. if b then y else y = y.
+* normalize // qed.
+
+theorem base_iff2: ∀b. if b then true else false = b.
+* normalize // qed.
+
+theorem hp_tesi: ∀D:DeqSet. ∀x,y:D. ∀b:bool. if (x==y) then b else false=true→b=true.
+#D #x #y #b elim b #Hp // normalize in Hp; > base_iff in Hp; // qed.
+
+theorem hp_tesi2: ∀D:DeqSet. ∀x,y:D. ∀b:bool. if (x==y) then b else false=true→(x==y)=true.
+#D #x #y #b #Hp lapply (hp_tesi … Hp) #Hp2
+destruct >base_iff2 in Hp; // qed.
+
+(******************************************************************************)
+(* Coercizione per i dati lista *)
+(******************************************************************************)
+
+let rec eqb_lD (T:DeqSet) (x,y:list T) on x : bool ≝
+ match x with
+ [ nil ⇒
+ match y with
+ [ nil ⇒ true
+ | _ ⇒ false]
+ | cons a b ⇒
+ match y with
+ [ nil ⇒ false
+ | cons c d ⇒ (eqb T a c)∧(eqb_lD T b d)]].
+
+lemma eqb_same_D: ∀D:DeqSet. ∀x:D. (eqb D x x)=true.
+#D #same @(proj2 … (eqb_true D ? ? ) …) // qed.
+
+theorem listD_elim2 :
+∀D:DeqSet.
+ ∀R:list D→ list D → Prop.
+ (∀n:list D. R [] n)
+ → (∀n,r. R (r::n) [])
+ → (∀n,m,r,u. R n m → R (r::n) (u::m))
+ → ∀n,m. R n m.
+#D
+#R #ROn #RSO #RSS #n (elim n) // #n0 #lN0 #Rn0m #m (cases m) /2/ qed.
+
+lemma list_destr_l: ∀D:DeqSet. ∀a,b:D.∀r,s:list D. (a=b)∧(r=s)→(a::r)=(b::s).
+#D #x #y #r #s #Hp
+lapply (proj1 (x=y) (r=s) Hp)
+ lapply (proj2 (x=y) (r=s) Hp)
+#H #H2 >H >H2 // qed.
+
+lemma list_destr_r: ∀D:DeqSet. ∀a,b:D.∀r,s:list D. (a::r)=(b::s)→(a=b)∧(r=s).
+#D #x #y *
+ [ *
+ [ #Hp %
+
+ [destruct @refl
+ |//
+ ]
+ | #d #lD #hp destruct
+ ]
+ | #d #lD #s #hp destruct % @refl] qed.
+
+lemma obv_eqb: ∀D:DeqSet.∀x:D. (x==x)=true.
+#D #l @(proj2 … (eqb_true ???) ) // qed.
+
+lemma obv_eb_l: ∀D. ∀e,l. (eqb_lD D (e::l) (e::l)=true).
+#D #x#y normalize elim y normalize >obv_eqb //
+#X #lX normalize #Hp >obv_eqb normalize @Hp qed.
+
+lemma liD_right: ∀D:DeqSet. ∀x,y:list D. (x=y)→(eqb_lD D x y)=true.
+#D
+@listD_elim2
+[ #n #asmpt <asmpt //
+| #L #r #Hp>Hp //
+| #l1 #l2 #e1 #e2 #Hp #eI lapply(list_destr_r D e1 e2 l1 l2 eI)
+ #HpE lapply (proj1 ? ? HpE) lapply (proj2 ? ? HpE) -HpE
+ #ls lapply (Hp ls) -Hp
+ #eqv #hp destruct
+ destruct
+ normalize >obv_eqb normalize @eqv] qed.
+
+lemma lid_left_1: ∀D:DeqSet. ∀x,y:D. ∀l1,l2:list D. ((x==y)=true)∧(l1=l2)→(x::l1=y::l2).
+#D #x #y #L #M * #Hp lapply (proj1 … (eqb_true D ? ? ) Hp) -Hp #Hp #LH destruct // qed.
+
+lemma tesi3: ∀D:DeqSet. ∀x,y:D. ∀M. (x=y)→(x::M=y::M).
+#T#a #b #L #hp destruct // qed.
+
+lemma liD_left: ∀D:DeqSet. ∀x,y:list D. (eqb_lD D x y)=true→(x=y).
+#D @listD_elim2
+ [ * normalize // #hp #HHp #abs destruct
+ | #L #el normalize #abs destruct
+ | #L #M #x #y #Hp normalize #N lapply (hp_tesi2… N) #Hp2
+ lapply(hp_tesi D … N) -N #N lapply(Hp N)
+ -Hp -N #HP destruct @tesi3 @(proj1 … (eqb_true D ? ? )) //] qed.
+
+lemma biimplication_lD: ∀D:DeqSet. ∀x,y:list D. iff ((eqb_lD D x y)=true) (x=y).
+#D #x #y %
+ [ @liD_left | @liD_right ]
+qed.
+
+
+definition DeqList ≝ λT:DeqSet. mk_DeqSet (list T) (eqb_lD T) (biimplication_lD T).
+
+unification hint 0 ≔ C1:DeqSet;
+ X ≟ DeqList C1
+(* ---------------------------------------- *) ⊢
+ DeqList C1 ≡ carr X.
+
+unification hint 0 ≔ C1:DeqSet,b1:list C1,b2: list C1;
+ X ≟ DeqList C1
+(* ---------------------------------------- *) ⊢
+ eqb_lD C1 b1 b2 ≡ eqb X b1 b2.
+
+
+(******************************************************************************)
+(* Coercizione per i dati Σ *)
+(******************************************************************************)
+
+definition Sig_fst ≝ λA:Type[0].λP:A→Prop.λx:Sig A P.
+ match x with [mk_Sig a h ⇒ a].
+
+definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
+ match x return λx.P (Sig_fst A P x) with [mk_Sig a h ⇒ h].
+
+definition Sig_eq ≝ λA:DeqSet.λP:A→Prop. λx,y:Sig A P.
+ ((Sig_fst A P x)==(Sig_fst A P y)).
+
+lemma biimplication_Sig: ∀A:DeqSet.∀P:A→Prop. ∀x,y:Sig A P.
+ (Sig_eq A P x y)=true↔(x=y).
+#A #P * #a1 #p1
+ * #a2 #p2
+ %
+ [ normalize #Hp
+ lapply (proj1 … (eqb_true A ? ?) Hp)
+ -Hp
+ #Hp destruct //
+ | #Hp destruct normalize //] qed.
+
+definition DeqSig ≝ λT:DeqSet.λP:T→Prop. mk_DeqSet (Sig T P) (Sig_eq T P) (biimplication_Sig T P).
+
+unification hint 0 ≔ C1:DeqSet,C2:C1→Prop;
+ X ≟ DeqSig C1 C2
+(* ---------------------------------------- *) ⊢
+ DeqSig C1 C2 ≡ carr X.
+
+unification hint 0 ≔ C1:DeqSet,C2:C1→Prop,b1:Sig C1 C2,b2:Sig C1 C2;
+ X ≟ DeqSig C1 C2
+(* ---------------------------------------- *) ⊢
+ Sig_eq C1 C2 b1 b2 ≡ eqb X b1 b2.
+
+definition mk_DeqSig : ∀T:DeqSet.∀P:T→Prop.∀x:T. (P x)→(DeqSig T P) ≝
+λT,P,x,p. mk_Sig T P x p.
+
+
+(******************************************************************************)
+(* Coercizione per i dati Cast *)
+(******************************************************************************)
+
+lemma eqc_b: ∀n1,hs. (eq_c (CBool n1) (CBool hs))=(beqb n1 hs).
+#n1 #hs normalize // qed.
+
+lemma eqc_n: ∀n1,hs. (eq_c (CNat n1) (CNat hs))=(eqb n1 hs).
+#n1 #hs normalize // qed.
+
+
+theorem dimplication_cast: ∀a,b. eq_c a b=true → a = b.
+* #n1
+ [* normalize #n2 [#Hp @eq_f @eqb_true_to_eq //
+ |#Hp @False_ind /2/]
+ |* [normalize #n2 #abs @False_ind /2/
+ | #b >eqc_b #hp @eq_f @(\P hp)]
+ ] qed.
+
+theorem eimplication_cast: ∀a,b. a = b →eq_c a b=true.
+*
+ [ #n * #m #Hp
+ [ normalize @eq_to_eqb_true destruct //
+ | <Hp normalize //]
+ | #b * #c #Hp
+ [ >Hp normalize //
+ | destruct @(proj2 … (beqb_true …) ) //
+ ]
+qed.
+
+
+theorem biimplication_cast: ∀a,b. iff (eq_c a b=true) (a = b).
+#A #B % [ @dimplication_cast | @eimplication_cast ] qed.
+
+definition DeqCoer ≝ mk_DeqSet coerc eq_c biimplication_cast.
+
+unification hint 0 ≔ ;
+ X ≟ DeqCoer
+(* ---------------------------------------- *) ⊢
+ coerc ≡ carr X.
+
+unification hint 0 ≔ b1,b2:coerc;
+ X ≟ DeqCoer
+(* ---------------------------------------- *) ⊢
+ eq_c b1 b2 ≡ eqb X b1 b2.
+
+(******************************************************************************)
+(* Coercizione per i dati Type *)
+(******************************************************************************)
+
+theorem biimplication_type: ∀a,b. iff (eqb_type a b=true) (a=b).
+* * % //
+ [ normalize #abs @False_ind /2/
+ | #Hp >Hp //
+ | normalize #abs @False_ind /2/
+ | #Hp >Hp //] qed.
+
+definition DeqType ≝ mk_DeqSet type eqb_type biimplication_type.
+
+unification hint 0 ≔ ;
+ X ≟ DeqType
+(* ---------------------------------------- *) ⊢
+ type ≡ carr X.
+
+unification hint 0 ≔ b1,b2:type;
+ X ≟ DeqType
+(* ---------------------------------------- *) ⊢
+ eqb_type b1 b2 ≡ eqb X b1 b2.
+
+(******************************************************************************)
+(* Coercizione per i dati naturali *)
+(******************************************************************************)
+
+definition eqb_nat ≝λx,y:nat. eqb x y.
+theorem biimplication_nat: ∀a,b. iff (eqb_nat a b=true) (a = b).
+#A #B % [ @eqb_true_to_eq | @eq_to_eqb_true ] qed.
+
+definition DeqNat ≝ mk_DeqSet ℕ eqb_nat biimplication_nat.
+
+unification hint 0 ≔ ;
+ X ≟ DeqNat
+(* ---------------------------------------- *) ⊢
+ nat ≡ carr X.
+
+unification hint 0 ≔ b1,b2:nat;
+ X ≟ DeqNat
+(* ---------------------------------------- *) ⊢
+ eqb_nat b1 b2 ≡ eqb X b1 b2.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "projdat/nth_proj.ma".
+
+(* Definizione della funzione di proiezione n-esima su valori *)
+let rec selection (l:DeqList DeqNat) s (t:DeqList s) ≝
+ match l with
+ [ nil ⇒ []
+ | cons a b ⇒ match (nth_opt ? a t ) with
+ [None ⇒ selection b s t
+ |Some w ⇒ w::(selection b s t)]
+ ].
+
+
+(* Data una lista di associazioni ID-Valori ed una lista di id, restituisce una
+ tupla *)
+definition ValueMap_tuple : ∀a. ∀b:(DeqList DeqNat). tuple (getSchema ( selection b ? (a))).
+#a #b %
+ [@( ( selection b ? ( a)))
+ | //
+ ]
+qed.
+
+
+(* NOTA: tutte le mappe debbono essere riconvertite in liste, dove gli elementi
+ si ottengono non per id k *)
+
+(* Definizione di un campo della tabella *)
+record table_record (schema: DeqList DeqType) (Tvaluemap: DeqList DeqCoer) (id:ℕ) : Type[0] ≝ {
+
+ (* Lista di id dei valori *)
+ Rids : DeqList DeqNat;
+
+ (* Preservazione dello schema *)
+ Rprop : (getSchema (selection Rids ? Tvaluemap)) = schema;
+ Rtuple : tuple schema;
+ RLen : length ? Rids = length ? schema;
+
+ (* Corrispondenza tra <chiavi,valoritupla>∈Tvaluemap *)
+ Rvalprop: getSchema (selection Rids ? (Sig_fst ? ? Rtuple)) =schema (*All ?
+ (λp. nth_opt ? (fst ?? p) (Tvaluemap)=Some ? (snd ?? p))
+ (compose DeqNat DeqCoer (DeqProd DeqNat DeqCoer) (λx,y. 〈x,y〉) ) *)
+
+}.
+
+(* Definizione di una tabella, contraddistinta da una particolare mappa di
+ associazione di tipi-etichette *)
+record table (Tlabelmap: DeqList DeqType) (Tvaluemap: DeqList DeqCoer) : Type[0] ≝ {
+ Tid : ℕ; (* ID della tabella *)
+ Tschema: DeqList DeqType; (* Schema della tabella *)
+ Tids : DeqList DeqNat; (* Elenco di identificativi dei tipi *)
+ cLen : (length ? Tschema)=(length ? Tids); (* Le liste hanno stessa lunghezza *)
+
+ (* Impongo che le coppie di Tschema-Tids appartengano alla mappa di etichette *)
+ cAss : All ?
+ (λp. nth_opt ? (fst ?? p) (getSchema Tvaluemap)=Some ? (snd ?? p) )
+ (compose DeqNat DeqType (DeqProd DeqNat DeqType) (λx,y. 〈x,y〉) Tids Tschema)
+ ;
+ (* Le tuple devono avere lo stesso schema*)
+ Ttuples: list (table_record Tschema Tvaluemap Tid);
+
+
+
+ (* Ed in particolare il loro schema *)
+ Preserv1: (Tschema=selection Tids DeqType Tlabelmap)
+
+
+
+}.
+
+
+(* Un database può essere visto come una lista di tabelle descritte come
+ sopra *)
+record database (Tlabelmap: DeqList DeqType) ( Dvaluemap: DeqList DeqCoer) : Type[0] ≝ {
+ DB : list (table Tlabelmap Dvaluemap);
+
+ (* Ogni tabella del DB deve avere ID unico *)
+ DTabUnique : uniqueb ? (map ? DeqNat (λx. Tid ?? x) DB)=true;
+
+ (* Per poter riuscire a garantire la unicità delle assoc....*)
+ DBTables: All ? (λp. length ? (Ttuples ?? p) > O) DB
+
+}.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "projdat/database.ma".
+
+definition eqbD ≝ λD:DeqSet.λa,b:D. eqb D a b.
+
+let rec nomismatch_id (A,B:DeqSet) (l:DeqList (DeqProd A B)) on l ≝
+ match l with
+ [ nil ⇒ true
+ | cons a b ⇒ andb (notb (exists ? (λp. andb (eqbD A (fst ?? a) (fst ?? p))
+ (notb (eqbD ? (snd ?? a) (snd ?? p))))
+ l))
+ (nomismatch_id A B b)].
+
+
+(* Definizione dell'insieme degli archi *)
+record HyperEdge (Tlabelmap: DeqList DeqType) (Tvaluemap: DeqList DeqCoer) : Type[0] ≝ {
+ Hid : ℕ;
+ Hids : DeqList DeqNat; (* Lista di id dei valori *)
+ HTids : DeqList DeqNat; (* Lista di id dei tipi *)
+ HLen : (length ? Hids)=(length ? HTids); (* Le tabelle hanno stessa lunghezza *)
+ HPTypes: (getSchema (selection Hids ? Tvaluemap))=
+ (selection HTids ? Tlabelmap);
+ (* Impongo che agli identificativi di valori corrispondano gli stessi
+ tipi *)
+ Htuple : tuple (getSchema (selection Hids ? Tvaluemap))
+}.
+
+(* XXX: riscrivibile come Σ-Type *)
+(* Definizione dell'insieme degli archi *)
+record HyperEdge_SET (Tlabelmap: DeqList DeqType) (Tvaluemap: DeqList DeqCoer)
+ (HSet: list (HyperEdge Tlabelmap Tvaluemap)) : Type[0] ≝ {
+
+ (* XXX: Controllo che ad uno stesso ID corrisponda un unico schema. Garantisce
+ l'unicità degli schemi per quello stesso ID ad ogni arco *)
+ CheckID_to_Schema: nomismatch_id ?? (map ? ( (DeqProd DeqNat (DeqList DeqType)))
+ (λx. 〈(Hid ?? x), (selection (HTids ?? x)? Tlabelmap)〉)
+ HSet)
+ =true
+
+}.
+
+(*
+definition is_HyperEdge_SET ≝
+ (λTlabelmap: DeqList DeqType) (λTvaluemap: DeqList DeqCoer)
+ (λHSet: list (HyperEdge Tlabelmap Tvaluemap)).
+ nomismatch_id ?? (map ? ( (DeqProd DeqNat (DeqList DeqType)))
+ (λx. 〈(Hid ?? x), (selection (HTids ?? x)? Tlabelmap)〉) HSet).
+*)
+
+(* Definizione dell'ipergrafo *)
+record HyperGraph (Tlabelmap : DeqList DeqType) (Nodes : DeqList DeqCoer) : Type[0] ≝ {
+ GSet: list (HyperEdge Tlabelmap Nodes);
+ (* Lista delle associazioni di tipo *)
+ (* Lista delle associazioni di valore *)
+ Edges : HyperEdge_SET Tlabelmap Nodes GSet
+}.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "projdat/tuples2.ma".
+
+(* Funzione di unione tra tuple di tipo 1 *)
+definition tup1_union: ∀S,T. tuple S → tuple T → tuple (S @T).
+*
+ [*
+ [ #u #_ @u
+ | #d #l #t #r @r
+ ]
+ | #d #ld #ts1 * #e1 #p1 * #e2 #p2 %
+ [ @(e1@e2) | >p1 >p2 normalize //
+ ]
+ ]
+qed.
+
+(* Definizione della funzione di proiezione n-esima su valori *)
+let rec tup1_projval (l:DeqList DeqNat) s (t:tuple s) : DeqList DeqCoer≝
+ match l with
+ [ nil ⇒ []
+ | cons a b ⇒ match (nth_opt ? a (Sig_fst ? ? t) ) with
+ [None ⇒ tup1_projval b s t
+ |Some w ⇒ w::(tup1_projval b s t)]
+ ].
+
+(* Definizione della funzione di proiezione n-aria *)
+definition tup1_projection ≝ λl,s,t. mk_tuple (getSchema (tup1_projval l s t)) (tup1_projval l s t) (refl ? ? ).
+
+(******************************************************************************)
+
+lemma gSchema_merge: ∀s1,i1,s2,i2.
+(s1=getSchema i1)→(s2=getSchema i2)→(s1@s2=getSchema(i1@i2)).
+#a #b #c#d #Hp #Hp2 >Hp >Hp2 normalize // qed.
+
+definition tup2_union : tuple_cast→tuple_cast→tuple_cast.
+* #s1 * #i1 #p1 * #s2 * #i2 #p2 %
+ [ @(s1@s2)
+ | lapply(gSchema_merge … p1 p2) -p1 -p2 #P %
+ [ @(i1@i2)
+ | @P
+ ]
+ ]
+qed.
+
+definition tup2_projval ≝ λl,c. tup1_projval l (Schema c) (Tuple c).
+
+definition tup2_projection : list DeqNat→tuple_cast→tuple_cast.
+#ids #tc %
+ [ @(getSchema (tup2_projval ids tc))
+ | % [ @(tup2_projval ids tc) | // ]]
+qed.
+
+(******************************************************************************)
+lemma gSchema_unpack:
+∀X,lX. (tail DeqType []=getSchema (tail DeqCoer (X::lX)))→([]=getSchema lX).
+#dc #ldc normalize // qed.
+
+
+lemma lemmata_tl_void0: ∀n,ld,dc,l,P.
+
+(tup1_projval (n::ld) [] «dc::l,P»=tup1_projval (ld) [] «dc::l,?»).
+[ 2: @P
+| #n #ln #d #ld #p lapply (gSchema_void2 … p) #pp >pp in p;
+ #e normalize //
+]
+qed.
+
+lemma lemmata_t1_void1: ∀dc, ldc,p,rpl. tup1_projval rpl [] «dc::ldc,p»=[].
+#dc #l #P #m elim m -m
+ [ //
+ | #n #ld #IH >lemmata_tl_void0 @IH]
+qed.
+
+lemma lemmata_t1_void2: ∀ ldc,p,rpl. tup1_projval rpl [] «ldc,p»=[].
+#l #P #m elim m -m
+ [ //
+ | #n #ld #IH lapply (gSchema_void2 … P) #pp >pp in P; #P normalize
+ elim ld -ld
+ [ //
+ | #dn #ldn #IH normalize @IH]
+ ]
+qed.
+
+lemma tup1_void_tl:
+∀rpl,X,lX,P. (tup1_projval rpl [] «X::lX,P»=tup1_projval rpl [] «lX,?»).
+ [ 2: lapply (gSchema_tltl … P) #Hp
+ lapply (gSchema_unpack … Hp) -Hp #Hp @Hp
+ | #rpl #dc #ldc #p >lemmata_t1_void1 >lemmata_t1_void2 //
+ ]
+qed.
+
+lemma tup1_voidt: ∀t,plist. (tup1_projval plist [] t) = [].
+#t elim t -t #p elim p -p
+ [ normalize #u #pl elim pl -pl
+ [ normalize //
+ | #n #ln #IH normalize @IH
+ ]
+ | #X #lX #IH #P #rpl
+ lapply (gSchema_tltl … P) #tl lapply (gSchema_unpack … tl) -tl #tl
+ lapply (IH tl) -IH #IH lapply (IH … rpl) -IH #IH
+ >lemmata_t1_void2 //]
+qed.
+
+
+(******************************************************************************)
+(* Dimostrazioni delle proprietà della seconda proiezione *)
+
+lemma voideton_proj_list_indiff:
+∀l,n.
+(tup2_projection (l::n) voideton2=tup2_projection (n) voideton2).
+#l #d normalize // qed.
+
+
+lemma voideton_proj : ∀plist. tup2_projection plist voideton2 = voideton2.
+#p elim p -p
+ [ normalize //
+ | #dn #ldn #HP >voideton_proj_list_indiff @HP] qed.
+
+
+(******************************************************************************)
+(* Lemmi accessori *)
+
+lemma gSchema_t1: ∀plist,t. (getSchema (tup1_projval plist [] t))=[].
+#p #t >tup1_voidt normalize // qed.
+
+
+lemma gSchema_null: getSchema [] = [].
+normalize // qed.
+
+lemma t_to_tcV:
+∀plist,t.
+t_to_tc (getSchema (tup1_projval plist [] t)) (tup1_projection plist [] t)=
+t_to_tc (getSchema []) ?.
+[ 2: >gSchema_null @t
+| #pl * #p #n >gSchema_null lapply (gSchema_void2 … n) #N destruct
+ elim pl -pl
+ [ //
+ | #dn #ld #IH normalize normalize in IH; @IH
+ ]
+qed.
+
+(******************************************************************************)
+
+(*
+ Si dimostra che le funzioni di proiezione preservano i contenuti delle tuple,
+ mantenendolo inalterato a meno di proiezione.
+ *)
+
+theorem preservation3: ∀s,t,l. tup2_projection l (t_to_tc s t) = (t_to_tc ? (tup1_projection l s t )).
+#s elim s -s
+ [ #t #plist >t_to_tc_void_as_voideton2
+ >voideton_proj
+ >t_to_tcV
+ normalize
+ elim t #p #gs
+ lapply (gSchema_void2 … gs)
+ #L destruct //
+ | #dt #ldt #IH
+ * #p #prop #ln
+ normalize //
+ ]
+qed.
+
+theorem preservation4: ∀t,l.
+(tup1_projection l (Schema t) (Tuple t)) = tc_to_t (tup2_projection l t ).
+normalize // qed.
+
+(* Si può notare come le funzioni che sono state qui fornite rendono confrontabili
+ le tuple, non rendendo più necessarie funzioni di coercizione, come invece
+ era necessario per i singoletti di tuple.
+ *)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "projdat/coerc.ma".
+
+(**************************************************************************)
+(* Definizione di alcuni lemmi sulle liste *)
+(**************************************************************************)
+lemma list_tail: ∀A:DeqSet. ∀a:A. ∀b:DeqList A. (tail A (a::b))=b. // qed.
+lemma list_head: ∀A:DeqSet. ∀a,c:A. ∀b:DeqList A. (hd A (a::b) c)=a. // qed.
+lemma list_lhdtl: ∀A:DeqSet. ∀a:A. ∀b,l:DeqList A. l=a::b → (a=hd ? l a)∧(b=tail ? l).
+#A #a #b #l #Hp destruct normalize /2/ qed.
+lemma list_hdtll: ∀A:DeqSet. ∀a:A. ∀b,l:DeqList A. a::b=l → (a=hd ? l a)∧(b=tail ? l).
+#A #a #b #l #Hp destruct normalize /2/ qed.
+(***************************************************************************)
+
+(* Definizione di istanza di una tupla *)
+definition tup_Inst ≝ DeqList DeqCoer.
+(* Definizione di uno schema di tupla *)
+definition tup_Sche ≝ DeqList DeqType.
+
+(* Dato un'istanza di tupla, riottiene il suo schema *)
+definition getSchema : tup_Inst → tup_Sche ≝
+ λl. map DeqCoer DeqType getType l.
+
+(* PRIMA DEFINIZIONE DI UNA TUPLA:
+ 1) Data una lista di schemi ed uno d'istanze, quest'ultimo rispetta i tipi
+ della prima
+ *)
+definition tuple ≝ λt. DeqSig tup_Inst (λc. t=(getSchema c)).
+ (* Funzione di creazione di una tupla di primo tipo *)
+definition mk_tuple : ∀s:tup_Sche. tup_Inst → ? → tuple s ≝
+λs:tup_Sche.λt:tup_Inst.λp. mk_Sig tup_Inst (λc. s=(getSchema c)) t p.
+
+(* Funzioni di equivalenza da getSchema nulla *)
+lemma gSchema_void: ∀tup. tup= [] → []=getSchema tup.
+#t elim t -t //
+ #Coer #ld #IH #Hp >Hp normalize @refl
+ qed.
+
+
+lemma gSchema_hd: ∀a,b. getSchema(a::b)=(getType a)::(getSchema b).
+#a elim a -a #el #l // qed.
+
+lemma gSchema_void2: ∀tup. []=getSchema tup→tup=[].
+#t elim t -t //
+ #Coer elim Coer -Coer #C #LD #IH #Hp >gSchema_hd in Hp; #Hp
+ @False_ind
+ destruct qed.
+
+lemma gSchema_hdtl: ∀a,b,c,d. a::b=getSchema(c::d)→a::b=(getType c)::(getSchema d).
+#a #b #c #d >gSchema_hd #hp @hp qed.
+
+
+
+
+
+
+
+
+
+
+(* SECONDA DEFINIZIONE DI UNA TUPLA:
+ 2) È un tipo, dove la prima definizione viene inglobata assieme allo schema,
+ ed incorporata in un unico dato
+ *)
+record tuple_cast : Type[0] ≝ {
+ Schema : tup_Sche;
+ Tuple : tuple Schema
+}.
+
+(* Lo schema di una tuple_cast è esattamente quello di parametro del suo tipo Σ *)
+lemma schemais:
+∀t,ldt,dc,ldc,t2.
+Schema ( (mk_tuple_cast (t::ldt) «dc::ldc,t2») )=t::ldt. // qed.
+
+(* Conversione 2 ⇒ 1 *)
+definition tc_to_t : ∀s:tuple_cast. (tuple (Schema s)).
+* #s #u @u qed.
+
+(* Conversione 1 ⇒ 2 *)
+definition t_to_tc : ∀S. tuple S → tuple_cast ≝ λS,x. mk_tuple_cast S x.
+
+(* Lemmi di preservazione della struttura dati: 2 ⇒ 1 ⇒ 2 *)
+lemma tc_t_tc : ∀x. t_to_tc (Schema x) (tc_to_t x) =x.
+* #s #t normalize // qed.
+(* Lemmi di preservazione della struttura dati: 1 ⇒ 2 ⇒ 1 *)
+lemma t_tc_t: ∀s,t. tc_to_t (t_to_tc s t) = t.
+#s #t normalize // qed.
+
+lemma base_coerc1: ∀x. (getType (CNat x))=Nat. // qed.
+lemma base_coerc2: ∀x. (getType (CBool x))=Bool. // qed.
+
+(* Definizione di una tupla con un singolo elemento: questa può essere effettuata
+ fornendo unicamente il valore del dato (1)
+ *)
+definition singleton: ∀c:DeqCoer. tuple [getType c].
+* #V
+ [ >base_coerc1 @(mk_tuple [Nat] [CNat V] (refl ? [Nat]))
+ | >base_coerc2 @(mk_tuple [Bool] [CBool V] (refl ? [Bool]))]. qed.
+
+(* Definizione di tuple vuote rispettivamente di tipo 1 e 2 *)
+definition voideton: tuple []. @(mk_tuple [] [] (refl ? [])) qed.
+definition voideton2 ≝ mk_tuple_cast [] voideton.
+
+lemma voideton_eq: ∀t:tuple[]. mk_tuple_cast [] t = voideton2.
+* #inst elim inst
+ [ #prop normalize @eq_f destruct //
+ | #dc #ldc #IH #AI lapply (gSchema_void2 … AI) #AI2 destruct
+ ]
+qed.
+
+(******************************************************************************)
+
+
+
+
+
+
+(**************************************************)
+(* Definizione della funzione di proiezione per 1 *)
+(**************************************************)
+(* Funzione per la restituzione del tipo di dato opportuno dato un valore opzionale *)
+definition optScheme : option DeqCoer→tup_Sche ≝ λu.
+ match u with
+ [ None ⇒ [ ]
+ | Some a ⇒ [getType a]].
+
+(* Funzione per l'istanziazione della tupla dal risultato della coercizione *)
+definition proj_5t: ∀x:option DeqCoer. tuple (optScheme x).
+* [ @voideton
+ | #arg @(singleton arg)] qed.
+
+(* Funzione di proiezione per 1 *)
+definition proj_t1: ∀s:tup_Sche.∀t:tuple s. ℕ→tuple ?.
+[ #s #t #i @(proj_5t (nth_opt ? i (Sig_fst ? ? t) )) ] skip qed.
+
+(* Definizione della proiezione in posizione (S n)-esima *)
+lemma optScheme1:
+ ∀n,dc,ld.
+ optScheme (nth_opt DeqCoer (S n) (dc::ld))=optScheme (nth_opt DeqCoer n ld).
+
+#n #dc #ld normalize // qed.
+
+
+
+
+
+(**************************************************)
+(* Definizione della funzione di proiezione per 2 *)
+(**************************************************)
+definition proj_t2 ≝ λtc,i.
+match nth_opt ? i (Sig_fst ? ? (Tuple tc)) with
+[ None ⇒ mk_tuple_cast [] voideton
+| Some a ⇒ mk_tuple_cast [getType a] (singleton a)].
+
+(* Lemmi sulla funzione di proiezione *)
+lemma proj_t2_null: ∀i. proj_t2 voideton2 i = voideton2.
+#i normalize // qed.
+lemma proj_t2_head: ∀a. proj_t2 (mk_tuple_cast [getType a] (singleton a)) O = mk_tuple_cast [getType a] (singleton a).
+#a elim a -a // qed.
+lemma proj_t2_head_N: ∀a,i. proj_t2 (mk_tuple_cast [getType a] (singleton a)) (S i)=voideton2.
+#a elim a -a // qed.
+
+
+(******************************************************************************)
+
+(* Definizione di proiezione dell'elemento (S x)-esimo elemento per ogni tipo di
+tupla *)
+theorem proj_t1_tl: ∀dt,ldt,ld,IH,prop,pos.
+
+ (proj_t1 (dt::ldt) «ld::IH,prop» (S pos)) = (proj_t1 (ldt) «IH,?» (pos)).
+
+[ #d #ld #dc #ldl #prop #pos //
+| lapply (list_hdtll … prop) * >list_tail >list_head
+ #h @(rewrite_r … (getSchema IH)) //
+] qed.
+
+
+
+(* Rappresentazione di una lista di "tipi" dalla rappresentazione del valore *)
+lemma proj_t2_tl_deq_Type:
+∀dt:DeqType. ∀ldt:list DeqType. ∀ld:DeqCoer.
+∀IH:list DeqCoer.∀prop: dt::ldt=getSchema (ld::IH).
+
+ (ldt=getSchema IH).
+
+#d #ld #dc #ldl #prop
+lapply (list_hdtll … prop) * >list_tail >list_head
+ #h @(rewrite_r … (getSchema ldl)) // qed.
+
+
+
+(* Definizione della proiezione sul secondo tipo di tupla *)
+theorem proj_t2_tl : ∀dt,ldt,ld,IH,prop,pos.
+
+ proj_t2 (t_to_tc (dt::ldt) «ld::IH,prop») (S pos)
+ = proj_t2 (t_to_tc ldt «IH,?») pos.
+
+[ #d #ld #dc #ldl #prop #pos //
+| @(proj_t2_tl_deq_Type dt ldt ld IH prop)
+] qed.
+
+
+
+(******************************************************************************)
+
+(* Una tupla vuota per 1) è un voideton 2) *)
+lemma t_to_tc_void_as_voideton2 : ∀t: tuple []. t_to_tc [] t = voideton2.
+ #t elim t
+ #tup #prop
+ normalize lapply (gSchema_void2 … prop) #Hp
+ destruct normalize
+ //
+qed.
+
+
+
+(* Una qualunque proiezione di un tipo di tupla 1) restituirà nessun elemento *)
+lemma voidopt_lemma: ∀t,pos.
+ (nth_opt DeqCoer pos (Sig_fst tup_Inst (λc:tup_Inst.[]=getSchema c) t))
+ = None DeqCoer.
+#t elim t -t #is #prop #n lapply (gSchema_void2 … prop) #Hp destruct
+ normalize // qed.
+
+
+
+lemma void_optS: (optScheme (None DeqCoer)) = []. // qed.
+lemma void_tup: (tuple (optScheme (None DeqCoer)))= tuple []. >void_optS // qed.
+
+
+
+(* Valutazione di una proiezione di tupla vuota 1) come eq_rect_Type0_r *)
+lemma proj_nothing_void : ∀t:tuple []. ∀pos. (proj_t1 [] t pos)= ?.
+[ 2: >voidopt_lemma >void_tup @t
+| #t elim t -t #s #prop lapply (gSchema_void2 … prop) #Hp #pos
+ destruct normalize // qed.
+(* check proj_nothing_void *)
+lemma proj_nothing_voideton: ∀pos. proj_t2 voideton2 pos = voideton2.
+#n elim n -n normalize // qed.
+
+(* Valutazione di una proiezione di una tupla vuota 2) come voideton2
+lemma t_to_c_proj1_void:
+∀dt, ldt, s1,n. proj_t2 (t_to_tc (dt::ldt) «[],s1») n = voideton2. // qed.
+*)
+
+
+
+
+(* Se la restituzione di uno schema per una istanza l è a::b, allora
+ b sarà pari allo schema ottenibile dal resto di l *)
+lemma gSchema_tl: ∀a,b,l. a::b=getSchema l → b = getSchema (tail DeqCoer l).
+
+#a @listD_elim2
+ [ #n #l elim l -l
+ [ #Hp normalize in Hp; normalize destruct
+ | #dc #ldc #IH #Hp >list_tail lapply (list_lhdtl …Hp) *
+ >list_head #oH1 >list_tail @(rewrite_l … (getSchema ldc)) //]
+ | #ldt #el1 -el1 #l elim l -l
+ [ #Hp //
+ | #DC #ldc #IH #hp >list_tail lapply (list_hdtll … hp) -hp
+ >list_head >list_tail * #oh1 @(rewrite_r … (getSchema ldc)) //
+ ]
+ | #ldt #m #d -d -ldt #u #IH #l elim l
+ [ #Hp lapply (IH … []) normalize #banal normalize in Hp; destruct
+ | #dc #ldc #IH #e1 >list_tail lapply (list_hdtll … e1) >list_head
+ * #oh1 >list_tail @(rewrite_r … (getSchema ldc)) //
+ ]
+ | @([a])
+ ]
+qed.
+
+
+lemma gSchema_tltl: ∀b,l. b=getSchema l → tail DeqType b = getSchema (tail DeqCoer l).
+#b elim b -b
+ [ #l #prop lapply(gSchema_void2 … prop) #lP >lP normalize //
+ | #dT #ldT #IH #tI #Hp whd in ⊢ (?? % ?); lapply (gSchema_tl … Hp) -Hp
+ #Hp //
+ ]
+qed.
+
+
+
+lemma gSchema_rest: ∀a,b,e,l. a::b=getSchema (e::l) → b = getSchema (l).
+#a #b #e #l @gSchema_tl qed.
+
+(* "Coercizione" per eq_rect_Type0_r *)
+theorem coerc1:
+∀ t,pos.t_to_tc
+ (optScheme
+ (nth_opt DeqCoer pos (Sig_fst tup_Inst (λc:tup_Inst.[]=getSchema c) t)))
+ (proj_t1 [] t pos)
+ =
+ mk_tuple_cast [] t.
+
+#t #pos>proj_nothing_void >voidopt_lemma normalize // qed.
+
+
+
+
+(******************************************************************************)
+
+(* Equivalenza tra schemi nell'elemento (S pos)-esimo *)
+lemma nthopt_S: ∀pos,t,ldt,dc,ldc,t2.
+
+ (nth_opt DeqCoer (S pos)
+ (Sig_fst tup_Inst (λc:tup_Inst.t::ldt=getSchema c)
+ (tc_to_t (mk_tuple_cast (t::ldt) «dc::ldc,t2»)))) =
+ (nth_opt DeqCoer ( pos)
+ (Sig_fst tup_Inst (λc:tup_Inst.ldt=getSchema c)
+ (tc_to_t (mk_tuple_cast (ldt) «ldc,?»)))).
+
+[ #p #dt #ldt #dc #ldc #hp normalize //
+| lapply (gSchema_tl … t2) #t3 normalize in t3;
+ normalize @t3
+] qed.
+
+
+(* Specializzazione del caso precedente, tramite estrazione diretta della
+ componente dello schema *)
+lemma nthopt_S2: ∀pos,t,ldt,dc,ldc,t2.
+
+ (nth_opt DeqCoer (S pos)
+ (Sig_fst tup_Inst (λc:tup_Inst.t::ldt=getSchema c)
+ (tc_to_t (mk_tuple_cast (t::ldt) «dc::ldc,t2»))))=
+ (nth_opt DeqCoer pos ldc).
+
+#pos #dt #ldt #dc #ldc #p >nthopt_S normalize // qed.
+
+(******************************************************************************)
+
+
+
+
+
+(* Qualsiasi proiezione di uno schema vuoto è esso stesso uno schema vuoto *)
+lemma coerc2: ∀t:tuple [].∀pos. (Schema (proj_t2 (mk_tuple_cast [] t) pos))=[].
+
+* #ti #prop #p >voideton_eq normalize @refl qed.
+
+
+
+lemma coerc3 : ∀t,ldt,ins,prop.
+
+(Sig_fst tup_Inst (λc:tup_Inst.t::ldt=getSchema c)
+ (tc_to_t (mk_tuple_cast (t::ldt) «ins,prop»)))=ins.
+
+#dt #ldt #ti #p normalize @refl qed.
+
+
+
+
+(* Le due definizioni di proiezione di tupla preservano la proiezione per il
+ tipo 1) lungo le funzioni di conversione per 2) *)
+theorem preservation1:
+∀s,t,i. proj_t2 (t_to_tc s t) i = (t_to_tc ? (proj_t1 s t i)).
+#s elim s -s
+ [ #t #pos >t_to_tc_void_as_voideton2
+ >proj_nothing_voideton
+ >coerc1
+ normalize elim t
+ #p #prop
+ lapply (gSchema_void2 … prop)
+ #Hp destruct //
+ | #dt #ldt #IH
+ #t elim t -t
+ #el1 elim el1 -el1
+ [ #prop #pos normalize //
+ | #ld #IH #Hp #prop #pos elim pos -pos
+ [ normalize //
+ | #pos #Hp2 >proj_t1_tl >proj_t2_tl //
+ ]
+ ]
+ ]
+qed.
+
+
+
+
+(* Equivalenza tra schemi di tuple cast *)
+lemma eqSchema: ∀a,b:tuple_cast. a=b → (Schema a)=(Schema b).
+* #ts1 #t1 * #ts2 #t2 #Hp destruct @refl qed.
+
+
+
+
+(* Data una tuple_schema a ed uno schema b, se i due schemi sono uguali,
+ allora posso restituire una tupla di schema b *)
+lemma tTupleSchema: ∀a,b. (Schema a)=b → tuple b.
+* #schema #inst #bschema #ref <ref @inst qed.
+
+
+
+(* Data una tupla a di schema s ed uno schema b, se s=b allora restituisco
+ la tupla come di schema b *)
+lemma tTuple: ∀s,b. ∀a:tuple s. s=b → tuple b.
+#a #b #inp #ref <ref @inp qed.
+
+
+
+(* Identità di t tra funzioni *)
+lemma tctt_void_preservation: ∀t:tuple []. (tc_to_t (mk_tuple_cast [] t)) = t.
+* #p #pr normalize @refl qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "projdat/tuples.ma".
+
+(* Computazione dello schema come proiezione (S pos)-esima *)
+lemma schemais2:
+∀t,ldt,dc,ldc,t2,pos.
+Schema (proj_t2 (mk_tuple_cast (t::ldt) «dc::ldc,t2») (S pos)) =
+Schema (proj_t2 (mk_tuple_cast (ldt) «ldc,?») ( pos)).
+ [ 2: @(proj_t2_tl_deq_Type t ldt dc ldc t2)
+ | 1: #t #l #d #c #t2 #p >(proj_t2_tl) //
+ ]
+qed.
+
+(******************************************************************************)
+
+(* Rappresentazione dell'ottenimento di uno schema di una proiezione su tupla
+ come la selezione del pos-esimo elemento dalla lista
+*)
+lemma coerc4:
+∀ldt,ldc,t2,pos.
+ (Schema (proj_t2 (mk_tuple_cast (ldt) «ldc,t2») ( pos))
+ =optScheme (nth_opt DeqCoer pos ldc)).
+
+#ldt elim ldt -ldt
+ [ #ldc elim ldc -ldc
+ [ //
+ | #c #ld #IH #prop #i
+ elim i -i
+ [ //
+ | #i #IH2 >coerc2
+ >coerc2 in IH2;
+ #IH2
+ lapply (gSchema_void2 … prop)
+ #IH3 >IH3 normalize @refl
+ ]
+ ]
+ | #dt #ldt #IH
+ #ldc elim ldc -ldc
+ [ //
+ | #c #lc #IH2 -IH2
+ #prop #pos elim pos -pos
+ [ //
+ | #i #IH3 -IH3
+ lapply (gSchema_rest … prop)
+ #prop2
+ lapply (IH lc prop2 i)
+ #IH3
+ >optScheme1
+ <IH3
+ >schemais2 //
+ ]
+ ]
+ ]
+qed.
+
+
+
+(* A questo punto debbo prima dimostrare che le tuple generate hanno lo stesso
+ schema, e quindi hanno lo stesso tipo di dato.
+ *)
+lemma coercition2:
+∀t,i.
+(Schema (proj_t2 t i))=(optScheme
+ (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))).
+* #ts elim ts -ts #t
+ [ #pos >coerc2 >tctt_void_preservation >voidopt_lemma normalize @refl
+ | #ldt #IH -IH * #ins elim ins -ins
+ [ #prop #pos
+ >coerc3 normalize //
+ | #dc #ldc #IH2 -IH2 #t2 #pos
+ elim pos -pos
+ [ normalize @refl
+ | #pos #IH3 -IH3
+ >nthopt_S2
+ lapply (gSchema_rest … t2)
+ #ct2 destruct
+ >coerc4 //
+ ]
+ ]
+ ]
+qed.
+
+
+lemma coercition2_tuple: ∀t,i.
+
+(tuple (Schema (proj_t2 t i)))
+ =
+(tuple (optScheme (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t))))).
+
+#t #i @eq_f @coercition2
+qed.
+
+
+
+lemma coercition2_tuple_transform: ∀t,i.
+(tuple (Schema (proj_t2 t i)))→
+ (tuple (optScheme
+ (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t))))).
+
+#t #i #Hp <coercition2_tuple @Hp qed.
+
+
+lemma coercition2_tuple_transform2: ∀t,i.
+(tuple (optScheme
+ (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))))
+ →
+ (tuple (Schema (proj_t2 t i))).
+#t #i #Hp >coercition2_tuple @Hp qed.
+
+lemma eqTup:
+∀t.
+tc_to_t t = Tuple t.
+#t elim t -t
+ #s #ts normalize // qed.
+
+lemma coercition2_tuple_transform_T: ∀t,i.
+(tuple (Schema (proj_t2 t i)))→
+ (tuple (optScheme
+ (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (Tuple t))))).
+
+// qed.
+
+
+lemma coercition2_tuple_transform2_T: ∀t,i.
+(tuple (optScheme
+ (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (λ c:tup_Inst.Schema t=getSchema c) (Tuple t)))))
+ →
+ (tuple (Schema (proj_t2 t i))).
+// qed.
+
+
+(*
+
+theorem preservation2:
+∀t,i.
+proj_t1 (Schema t) (Tuple t) i = (tc_to_t (proj_t2 t i)).
+…
+
+********** DISAMBIGUATION ERRORS: **********
+***** Errors obtained during phases 1: *****
+*Error at 70-91: The term
+(tc_to_t (proj_t2 t i))
+has type
+(tuple (Schema (proj_t2 t i)))
+but is here used with type
+(tuple
+ (optScheme
+ (nth_opt DeqCoer i
+ (Sig_fst tup_Inst (\lambda c:tup_Inst.Schema t=getSchema c) (tc_to_t t)))))
+
+In quanto aver dimostrato l'uguaglianza dei tipi come già dimostrato non consente
+di poter confrontare questi due elementi, allora è necessario mostrare d'ora in
+poi una forma d'uguaglianza più debole.
+
+*)
+
+
+theorem preservation2: ∀t,i.
+ coercition2_tuple_transform2_T t i(proj_t1 (Schema t) (Tuple t) i) = (tc_to_t (proj_t2 t i)).
+#t #i normalize @refl qed.
+
+theorem preservation2bis: ∀t,i.
+ (proj_t1 (Schema t) (Tuple t) i) = coercition2_tuple_transform_T t i (tc_to_t (proj_t2 t i)).
+normalize #t #i @refl qed.
projects / helm.git / commitdiff