From d2e0a33c75842a10574ef904097803e02571536c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 12 Apr 2016 14:27:22 +0000 Subject: [PATCH] - first working commit of the static component .. - updates on some web pages --- matita/matita/contribs/BTM/web/BTM.ldw.xml | 1 + .../lambdadelta/apps_2/web/apps_2.ldw.xml | 1 + .../lambdadelta/basic_2/relocation/drops.ma | 14 ++-- .../lambdadelta/basic_2/static/lsuba_aaa.ma | 28 ++++---- .../lambdadelta/basic_2/static/lsuba_drops.ma | 71 ++++++++++--------- .../lambdadelta/basic_2/static/lsuba_lsuba.ma | 2 +- .../lambdadelta/basic_2/static/lsubr_drops.ma | 20 +++--- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 6 ++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 8 +-- 9 files changed, 81 insertions(+), 70 deletions(-) diff --git a/matita/matita/contribs/BTM/web/BTM.ldw.xml b/matita/matita/contribs/BTM/web/BTM.ldw.xml index 32ee158a1..5971089e6 100644 --- a/matita/matita/contribs/BTM/web/BTM.ldw.xml +++ b/matita/matita/contribs/BTM/web/BTM.ldw.xml @@ -3,6 +3,7 @@
Character classes
diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index 027c6b1d9..663745019 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -3,6 +3,7 @@ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index b540ec904..4fcb38e31 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -294,11 +294,11 @@ qed-. (* Inversion lemmas with test for uniformity ********************************) lemma drops_inv_isuni: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐔⦃f⦄ → - (𝐈⦃f⦄ ∧ L2 = L1) ∨ - ∃∃I,K,V,g. ⬇*[Ⓣ, g] K ≡ L2 & L1 = K.ⓑ{I}V & f = ⫯g. + (𝐈⦃f⦄ ∧ L1 = L2) ∨ + ∃∃I,K,V,g. ⬇*[Ⓣ, g] K ≡ L2 & 𝐔⦃g⦄ & L1 = K.ⓑ{I}V & f = ⫯g. #L1 #L2 #f * -L1 -L2 -f [ /4 width=1 by or_introl, conj/ -| /4 width=7 by ex3_4_intro, or_intror/ +| /4 width=8 by isuni_inv_next, ex4_4_intro, or_intror/ | /7 width=6 by drops_fwd_isid, lifts_fwd_isid, isuni_inv_push, isid_push, or_introl, conj, eq_f3, sym_eq/ ] qed-. @@ -306,24 +306,24 @@ qed-. (* Basic_2A1: was: drop_inv_O1_pair1 *) lemma drops_inv_pair1_isuni: ∀I,K,L2,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] K.ⓑ{I}V ≡ L2 → (𝐈⦃f⦄ ∧ L2 = K.ⓑ{I}V) ∨ - ∃∃g. ⬇*[c, g] K ≡ L2 & f = ⫯g. + ∃∃g. 𝐔⦃g⦄ & ⬇*[c, g] K ≡ L2 & f = ⫯g. #I #K #L2 #V #c #f #Hf #H elim (isuni_split … Hf) -Hf * #g #Hg #H0 destruct [ lapply (drops_inv_skip1 … H) -H * #Y #X #HY #HX #H destruct <(drops_fwd_isid … HY Hg) -Y >(lifts_fwd_isid … HX Hg) -X /4 width=3 by isid_push, or_introl, conj/ -| lapply (drops_inv_drop1 … H) -H /3 width=3 by ex2_intro, or_intror/ +| lapply (drops_inv_drop1 … H) -H /3 width=4 by ex3_intro, or_intror/ ] qed-. (* Basic_2A1: was: drop_inv_O1_pair2 *) lemma drops_inv_pair2_isuni: ∀I,K,V,c,f,L1. 𝐔⦃f⦄ → ⬇*[c, f] L1 ≡ K.ⓑ{I}V → (𝐈⦃f⦄ ∧ L1 = K.ⓑ{I}V) ∨ - ∃∃I1,K1,V1,g. ⬇*[c, g] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & f = ⫯g. + ∃∃I1,K1,V1,g. 𝐔⦃g⦄ & ⬇*[c, g] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & f = ⫯g. #I #K #V #c #f * [ #Hf #H elim (drops_inv_atom1 … H) -H #H destruct | #L1 #I1 #V1 #Hf #H elim (drops_inv_pair1_isuni … Hf H) -Hf -H * [ #Hf #H destruct /3 width=1 by or_introl, conj/ - | /3 width=7 by ex3_4_intro, or_intror/ + | /3 width=8 by ex4_4_intro, or_intror/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma index 9f1f9bcc5..84f997c82 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma @@ -17,19 +17,18 @@ include "basic_2/static/lsuba.ma". (* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) -(* Properties concerning atomic arity assignment ****************************) +(* Properties with atomic arity assignment **********************************) lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A → ∀L2. G ⊢ L1 ⫃⁝ L2 → ⦃G, L2⦄ ⊢ V ⁝ A. #G #L1 #V #A #H elim H -G -L1 -V -A [ // -| #I #G #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12 - elim (lsuba_drop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 - elim (lsuba_inv_pair1 … H) -H * #K2 - [ #HK12 #H destruct /3 width=5 by aaa_lref/ - | #W0 #V0 #A0 #HV0 #HW0 #_ #H1 #H2 #H3 destruct - lapply (aaa_mono … HV0 … HV) #H destruct -V0 /2 width=5 by aaa_lref/ - ] +| #I #G #L1 #V #A #HA #IH #L2 #H + elim (lsuba_inv_pair1 … H) -H * /3 width=1 by aaa_zero/ + #L0 #W0 #V0 #A0 #HV0 #HW0 #HL10 #H1 #H2 #H3 destruct + lapply (aaa_mono … HV0 … HA) #H destruct -V0 -L1 /2 width=1 by aaa_zero/ +| #I #G #K1 #V #A #i #_ #IH #L2 #H + elim (lsuba_inv_pair1 … H) -H * /3 width=1 by aaa_lref/ | /4 width=2 by lsuba_pair, aaa_abbr/ | /4 width=1 by lsuba_pair, aaa_abst/ | /3 width=3 by aaa_appl/ @@ -41,13 +40,12 @@ lemma lsuba_aaa_trans: ∀G,L2,V,A. ⦃G, L2⦄ ⊢ V ⁝ A → ∀L1. G ⊢ L1 ⫃⁝ L2 → ⦃G, L1⦄ ⊢ V ⁝ A. #G #L2 #V #A #H elim H -G -L2 -V -A [ // -| #I #G #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12 - elim (lsuba_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsuba_inv_pair2 … H) -H * #K1 - [ #HK12 #H destruct /3 width=5 by aaa_lref/ - | #V0 #A0 #HV0 #H2V #_ #H1 #H2 destruct - lapply (aaa_mono … H2V … H1V) #H destruct -K2 /2 width=5 by aaa_lref/ - ] +| #I #G #L2 #V #A #HA #IH #L1 #H + elim (lsuba_inv_pair2 … H) -H * /3 width=1 by aaa_zero/ + #L0 #V0 #A0 #HV0 #HV #HL02 #H1 #H2 destruct + lapply (aaa_mono … HV … HA) #H destruct -L2 /2 width=1 by aaa_zero/ +| #I #G #K2 #V #A #i #_ #IH #L1 #H + elim (lsuba_inv_pair2 … H) -H * /3 width=1 by aaa_lref/ | /4 width=2 by lsuba_pair, aaa_abbr/ | /4 width=1 by lsuba_pair, aaa_abst/ | /3 width=3 by aaa_appl/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma index f2440c801..29ff470b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma @@ -12,54 +12,57 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lrsubeqa_3.ma". -include "basic_2/static/lsubr.ma". -include "basic_2/static/aaa.ma". +include "basic_2/relocation/drops.ma". +include "basic_2/static/lsuba.ma". (* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************) -(* Basic properties *********************************************************) +(* Properties with generic slicing for local environments *******************) -(* Note: the constant 0 cannot be generalized *) -lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,c,k. ⬇[c, 0, k] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L2 ≡ K2. +(* Note: the premise 𝐔⦃f⦄ cannot be removed *) +(* Basic_2A1: includes: lsuba_drop_O1_conf *) +lemma lsuba_drops_conf_isuni: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → + ∀K1,c,f. 𝐔⦃f⦄ → ⬇*[c, f] L1 ≡ K1 → + ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇*[c, f] L2 ≡ K2. #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #_ #IHL12 #K1 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1 - [ destruct - elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/ - | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ +| #I #L1 #L2 #V #HL12 #IH #K1 #c #f #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by lsuba_pair, drops_refl, ex2_intro/ + | #g #Hg #HLK1 #H destruct -HL12 + elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/ ] -| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1 - [ destruct - elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ - | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ +| #L1 #L2 #W #V #A #HV #HW #HL12 #IH #K1 #c #f #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by drops_refl, lsuba_beta, ex2_intro/ + | #g #Hg #HLK1 #H destruct -HL12 + elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/ ] ] qed-. -(* Note: the constant 0 cannot be generalized *) -lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L1 ≡ K1. +(* Note: the premise 𝐔⦃f⦄ cannot be removed *) +(* Basic_2A1: includes: lsuba_drop_O1_trans *) +lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → + ∀K2,c,f. 𝐔⦃f⦄ → ⬇*[c, f] L2 ≡ K2 → + ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇*[c, f] L1 ≡ K1. #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #_ #IHL12 #K2 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2 - [ destruct - elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/ - | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ +| #I #L1 #L2 #V #HL12 #IH #K2 #c #f #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by lsuba_pair, drops_refl, ex2_intro/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ ] -| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #c #k #H - elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2 - [ destruct - elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ - | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ +| #L1 #L2 #W #V #A #HV #HW #HL12 #IH #K2 #c #f #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by drops_refl, lsuba_beta, ex2_intro/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma index ee7ab0de5..8332f80e9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma @@ -18,7 +18,7 @@ include "basic_2/static/lsuba_aaa.ma". (* Main properties **********************************************************) -theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⫃⁝ L → ∀L2. G ⊢ L ⫃⁝ L2 → G ⊢ L1 ⫃⁝ L2. +theorem lsuba_trans: ∀G. Transitive … (lsuba G). #G #L1 #L #H elim H -L1 -L [ #X #H >(lsuba_inv_atom1 … H) -H // | #I #L1 #L #Y #HL1 #IHL1 #X #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma index ca2154608..5aa248fbc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma @@ -27,16 +27,20 @@ lemma lsubr_fwd_drops2_pair: ∀L1,L2. L1 ⫃ L2 → #L1 #L2 #H elim H -L1 -L2 [ #L #I #K2 #W #c #f #_ #H elim (drops_inv_atom1 … H) -H #H destruct -| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #c #f #Hf #H - elim (drops_inv_pair1_isuni … Hf H) -H * #g #HLK2 try #H destruct [ -IHL12 | -HL12 ] - [ /4 width=4 by drops_refl, ex2_intro, or_introl/ - | elim (IHL12 … HLK2) -IHL12 -HLK2 /2 width=3 by isuni_inv_next/ * +| #J #L1 #L2 #V #HL12 #IH #I #K2 #W #c #f #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /4 width=4 by drops_refl, ex2_intro, or_introl/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -IH -Hg -HLK2 * /4 width=4 by drops_drop, ex3_2_intro, ex2_intro, or_introl, or_intror/ ] -| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #c #f #Hf #H - elim (drops_inv_pair1_isuni … Hf H) -H * #g #HLK2 try #H destruct [ -IHL12 | -HL12 ] - [ /4 width=4 by drops_refl, ex3_2_intro, or_intror/ - | elim (IHL12 … HLK2) -IHL12 -HLK2 /2 width=3 by isuni_inv_next/ * +| #L1 #L2 #V1 #V2 #HL12 #IH #I #K2 #W #c #f #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /4 width=4 by drops_refl, ex3_2_intro, or_intror/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -IH -Hg -HLK2 * /4 width=4 by drops_drop, ex3_2_intro, ex2_intro, or_introl, or_intror/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index a50dd0d88..d52fc854c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -34,6 +34,12 @@ Stage "A2": "Extending the Applicability Condition" + + Grammatical component reconstructed: + grammar, relocation, s_transition, s_computation, static + (anniversary milestone). + + Relocation with reference transforming maps (rtmap). diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 73a5a3977..35447f814 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -190,16 +190,14 @@ table { [ "sh" "sd" * ] } ] -(* - [ { "local env. ref. for atomic arity assignment" * } { - [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_aaa" + "lsuba_lsuba" * ] + [ { "restricted ref. for atomic arity assignment" * } { + [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] } ] [ { "atomic arity assignment" * } { - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_lleq" + "aaa_aaa" * ] + [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + (* "aaa_lleq" + *) "aaa_aaa" * ] } ] -*) [ { "restricted ref. for local env." * } { [ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] } -- 2.39.2