From 38571b4c3881f2b59b7a2cdd016c83b161d3d755 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 19 Feb 2017 18:56:35 +0000 Subject: [PATCH] - advances on cnx - generic reducibility moved to the "static" component --- .../lambdadelta/basic_2/relocation/drops.ma | 4 +++ .../basic_2/rt_computation/partial.txt | 2 -- .../basic_2/rt_transition/cnx_drops.ma | 36 +++++++++---------- .../basic_2/rt_transition/partial.txt | 2 +- .../basic_2/{rt_computation => static}/gcp.ma | 0 .../{rt_computation => static}/gcp_aaa.ma | 2 +- .../{rt_computation => static}/gcp_cr.ma | 2 +- .../{rt_computation => static}/lsubc.ma | 2 +- .../{rt_computation => static}/lsubc_drops.ma | 2 +- .../{rt_computation => static}/lsubc_lsuba.ma | 2 +- .../{rt_computation => static}/lsubc_lsubr.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +++---- 12 files changed, 34 insertions(+), 34 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/gcp.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/gcp_aaa.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/gcp_cr.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/lsubc.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/lsubc_drops.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/lsubc_lsuba.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation => static}/lsubc_lsubr.ma (96%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index d35fb52a2..7a4ad7662 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -42,6 +42,10 @@ definition d_liftable1: predicate (relation2 lenv term) ≝ λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K → ∀U. ⬆*[f] T ≡ U → R L U. +definition d_deliftable1: predicate (relation2 lenv term) ≝ + λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K → + ∀T. ⬆*[f] T ≡ U → R K T. + definition d_liftable2: predicate (lenv → relation term) ≝ λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K → ∀U1. ⬆*[f] T1 ≡ U1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index b47d0e449..41a6c9556 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,3 +1 @@ -lsubc.ma lsubc_drops.ma lsubc_lsubr.ma lsubc_lsuba.ma -gcp.ma gcp_cr.ma gcp_aaa.ma cpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma index b4f5e8c3d..1dcbdf2a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/rt_transition/cpx_drops.ma". include "basic_2/rt_transition/cnx.ma". @@ -24,6 +25,15 @@ lemma cnx_lref_atom: ∀h,o,G,L,i. ⬇*[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ⬈[h, o #I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct qed. +(* Basic_2A1: includes: cnx_lift *) +lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G). +#h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H +elim (cpx_inv_lifts … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 +lapply (HT … HT0) -G -K #HT0 +elim (tdeq_lifts … HT0 … HTU) -T #X #HX #HU +<(lifts_mono … HX … HTU0) -T0 // +qed-. + (* Inversion lemmas with generic slicing ************************************) (* Basic_2A1: was: cnx_inv_delta *) @@ -35,23 +45,11 @@ lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK /2 width=5 by lifts_inv_lref2_uni_lt/ qed-. -(* -(* Relocation properties ****************************************************) - -lemma cnx_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⬇[c, l, k] L0 ≡ L → - ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄. -#h #o #G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H -elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 -<(HLT … HT1) in HT0; -L #HT0 ->(lift_mono … HT10 … HT0) -T1 -X // -qed. - -lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L → - ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄. -#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H -elim (lift_total X l k) #X0 #HX0 -lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0 ->(HLT0 … HTX0) in HX0; -L0 -X0 #H ->(lift_inj … H … HT0) -T0 -X -l -k // +(* Basic_2A1: includes: cnx_inv_lift *) +lemma cnx_inv_lifts: ∀h,o,G. d_deliftable1 … (cnx h o G). +#h #o #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H +elim (cpx_lifts … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 +lapply (HU … HU0) -G -L #HU0 +elim (tdeq_inv_lifts … HU0 … HTU) -U #X #HX #HT +<(lifts_inj … HX … HTU0) -U0 // qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 9760148c1..9ed6e4104 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,7 +1,7 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma -cnx.ma cnx_simple.ma +cnx.ma cnx_simple.ma cnx_drops.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma index 111d967e5..53b415bde 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/aaa_aaa.ma". -include "basic_2/rt_computation/lsubc_drops.ma". +include "basic_2/static/lsubc_drops.ma". (* GENERIC COMPUTATION PROPERTIES *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma index 4493ae7af..09dd1d346 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma @@ -17,7 +17,7 @@ include "basic_2/syntax/aarity.ma". include "basic_2/relocation/lifts_simple.ma". include "basic_2/relocation/lifts_lifts_vector.ma". include "basic_2/relocation/drops_drops.ma". -include "basic_2/rt_computation/gcp.ma". +include "basic_2/static/gcp.ma". (* GENERIC COMPUTATION PROPERTIES *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma index 5b994b741..7b5315d4f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/lrsubeqc_4.ma". include "basic_2/static/aaa.ma". -include "basic_2/rt_computation/gcp_cr.ma". +include "basic_2/static/gcp_cr.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma index 59ba61ad2..d39dd6816 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/aaa_drops.ma". -include "basic_2/rt_computation/lsubc.ma". +include "basic_2/static/lsubc.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma index 2969b9a52..625aed556 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/lsuba.ma". -include "basic_2/rt_computation/gcp_aaa.ma". +include "basic_2/static/gcp_aaa.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma rename to matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma index 045ad95bd..ddf571d83 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/lsubr.ma". -include "basic_2/rt_computation/lsubc.ma". +include "basic_2/static/lsubc.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) 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 a7fc0d856..4a5a696ac 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 @@ -124,12 +124,6 @@ table { [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] } ] - [ { "generic reducibility" * } { - [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] - [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] - [ "gcp" *] - } - ] } ] class "water" @@ -166,6 +160,12 @@ table { ] class "green" [ { "static typing" * } { + [ { "generic reducibility" * } { + [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] + [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] + [ "gcp" *] + } + ] [ { "atomic arity assignment" * } { [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] -- 2.39.2