From 4672640dc168a3adcbea86887c38d895358288e8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 28 May 2013 09:56:51 +0000 Subject: [PATCH] Error to debug --- matita/matita/projdat/basic_type.ma | 48 ++++ matita/matita/projdat/coerc.ma | 256 +++++++++++++++++ matita/matita/projdat/database.ma | 95 +++++++ matita/matita/projdat/hypergraph.ma | 69 +++++ matita/matita/projdat/nth_proj.ma | 184 +++++++++++++ matita/matita/projdat/tuples.ma | 414 ++++++++++++++++++++++++++++ matita/matita/projdat/tuples2.ma | 183 ++++++++++++ 7 files changed, 1249 insertions(+) create mode 100644 matita/matita/projdat/basic_type.ma create mode 100644 matita/matita/projdat/coerc.ma create mode 100644 matita/matita/projdat/database.ma create mode 100644 matita/matita/projdat/hypergraph.ma create mode 100644 matita/matita/projdat/nth_proj.ma create mode 100644 matita/matita/projdat/tuples.ma create mode 100644 matita/matita/projdat/tuples2.ma diff --git a/matita/matita/projdat/basic_type.ma b/matita/matita/projdat/basic_type.ma new file mode 100644 index 000000000..4cb63284c --- /dev/null +++ b/matita/matita/projdat/basic_type.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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]. + + + diff --git a/matita/matita/projdat/coerc.ma b/matita/matita/projdat/coerc.ma new file mode 100644 index 000000000..20144b235 --- /dev/null +++ b/matita/matita/projdat/coerc.ma @@ -0,0 +1,256 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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 // + | 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. diff --git a/matita/matita/projdat/database.ma b/matita/matita/projdat/database.ma new file mode 100644 index 000000000..65856a027 --- /dev/null +++ b/matita/matita/projdat/database.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ∈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 diff --git a/matita/matita/projdat/hypergraph.ma b/matita/matita/projdat/hypergraph.ma new file mode 100644 index 000000000..88b2620f9 --- /dev/null +++ b/matita/matita/projdat/hypergraph.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/matita/matita/projdat/nth_proj.ma b/matita/matita/projdat/nth_proj.ma new file mode 100644 index 000000000..b7de08ddd --- /dev/null +++ b/matita/matita/projdat/nth_proj.ma @@ -0,0 +1,184 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/matita/matita/projdat/tuples.ma b/matita/matita/projdat/tuples.ma new file mode 100644 index 000000000..1eea2f80c --- /dev/null +++ b/matita/matita/projdat/tuples.ma @@ -0,0 +1,414 @@ +(**************************************************************************) +(* ___ *) +(* ||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 (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 + 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 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. -- 2.39.2