From 65383ff6ec2236b0a61310b872ea4cd5fcc26fb7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 Mar 2017 11:54:10 +0000 Subject: [PATCH] cpxs_drops completed --- .../lambdadelta/apps_2/web/apps_2.ldw.xml | 7 ++ .../basic_2/rt_computation/cpxs_drops.ma | 65 ++++++++++++++----- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../contribs/lambdadelta/partial_compile.sh | 5 ++ 4 files changed, 63 insertions(+), 18 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/partial_compile.sh 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 663745019..a242c3124 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 @@ -23,12 +23,19 @@ The validation algorithm for λδ as implemented in Helena 0.8. + + + Terms of λδ with special features. + Summary of the Specification Here is a numerical account of the specification's contents and its timeline. + + The Examples component is moved from the Core directory. + The Applications directory is started. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma index 26fb988b5..08eed1481 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/drops_lstar.ma". include "basic_2/rt_transition/cpx_drops.ma". include "basic_2/rt_computation/cpxs.ma". @@ -55,35 +56,67 @@ lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i. elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2 [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ - | /2 width=3 by drops_isuni_fwd_drop2/ + | /2 width=3 by drops_isuni_fwd_drop2/ ] ] qed. -(* + (* Advanced inversion lemmas ************************************************) -lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 → - T2 = #i ∨ - ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 & - ⬆[0, i+1] T1 ≡ T2. -#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ +lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 → + T2 = #0 ∨ + ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓑ{I}V1. +#h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ +| * #I #K #V1 #T1 #HVT1 #HT1 #H destruct + elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T + /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/ +] +qed-. + +lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈*[h] T2 → + T2 = #(⫯i) ∨ + ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V. +#h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ #T #T2 #_ #HT2 * [ #H destruct elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ +| * #I #K #V1 #T1 #Hi #HT1 #H destruct + elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T + /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/ +] +qed-. + +(* Basic_2A1: was: cpxs_inv_lref1 *) +lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 → + T2 = #i ∨ + ∃∃I,K,V1,T1. ⬇*[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h] T1 & + ⬆*[⫯i] T1 ≡ T2. +#h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpx_inv_lref1_drops … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ | * #I #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (drop_fwd_drop2 … HLK) #H0LK - elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK + elim (cpx_inv_lifts … HT2 … H0LK … HT1) -H0LK -T /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ ] qed-. -(* Relocation properties ****************************************************) +(* Properties with generic relocation ***************************************) -lemma cpxs_lift: ∀h,o,G. d_liftable (cpxs h o G). -/3 width=10 by cpx_lift, cpxs_strap1, d_liftable_LTC/ qed. +(* Basic_2A1: includes: cpxs_lift *) +lemma cpxs_lifts: ∀h,G. d_liftable2 (cpxs h G). +/3 width=10 by cpx_lifts, cpxs_strap1, d2_liftable_LTC/ qed-. -lemma cpxs_inv_lift1: ∀h,o,G. d_deliftable_sn (cpxs h o G). -/3 width=6 by d_deliftable_sn_LTC, cpx_inv_lift1/ -qed-. -*) +(* Inversion lemmas with generic relocation *********************************) + +(* Basic_2A1: includes: cpxs_inv_lift1 *) +lemma cpxs_inv_lifts: ∀h,G. d_deliftable2_sn (cpxs h G). +/3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts/ qed-. 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 fe1040d58..729331c1d 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 @@ -155,8 +155,8 @@ table { ] class "water" [ { "iterated static typing" * } { - [ { "generic extension on referred entries" * } { - [ "lfxss ( ? ⦻**[?,?] ? )" * ] + [ { "iterated extension on referred entries" * } { + [ "tc_lfxs ( ? ⦻**[?,?] ? )" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/partial_compile.sh b/matita/matita/contribs/lambdadelta/partial_compile.sh new file mode 100644 index 000000000..319fa8704 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/partial_compile.sh @@ -0,0 +1,5 @@ +cd basic_2/rt_transition/ +../../../../matitac.opt `cat partial.txt` +cd ../rt_computation/ +../../../../matitac.opt `cat partial.txt` +cd ../../ -- 2.39.2