From fde3b3d2e6cc48f6c9880136b1a0d565e2c78c1f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Jun 2012 20:34:11 +0000 Subject: [PATCH] - lambda_delta: subject reduction for nativa type assignment begins ... dependecnes between source files improved - matitadep: little application for optimizing dependences between .ma files (used by lambda_delta Makefile) --- matita/components/binaries/matitadep/Makefile | 6 + .../binaries/matitadep/matitadep.ml | 47 +++++ matita/matita/contribs/lambda_delta/Makefile | 10 + .../basic_2/computation/cprs_delift.ma | 6 + .../lambda_delta/basic_2/computation/csn.ma | 1 - .../basic_2/computation/lsubc_ldrop.ma | 1 - .../lambda_delta/basic_2/dynamic/nta_ltpr.ma | 179 ++++++++++++++++++ .../basic_2/equivalence/cpcs_cprs.ma | 6 + .../basic_2/equivalence/cpcs_delift.ma | 4 + .../basic_2/equivalence/cpcs_ltpss.ma | 1 - .../lambda_delta/basic_2/reducibility/cpr.ma | 1 - .../basic_2/reducibility/lcpr_aaa.ma | 1 - .../basic_2/reducibility/lcpr_lcpr.ma | 1 - .../lambda_delta/basic_2/substitution/tps.ma | 1 - .../basic_2/unfold/delift_delift.ma | 1 - .../basic_2/unfold/delift_lift.ma | 7 + 16 files changed, 265 insertions(+), 8 deletions(-) create mode 100644 matita/components/binaries/matitadep/Makefile create mode 100644 matita/components/binaries/matitadep/matitadep.ml create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma diff --git a/matita/components/binaries/matitadep/Makefile b/matita/components/binaries/matitadep/Makefile new file mode 100644 index 000000000..7695ab288 --- /dev/null +++ b/matita/components/binaries/matitadep/Makefile @@ -0,0 +1,6 @@ +EXEC = matitadep +VERSION=0.1.0 + +REQUIRES = + +include ../Makefile.common diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml new file mode 100644 index 000000000..ebb87695f --- /dev/null +++ b/matita/components/binaries/matitadep/matitadep.ml @@ -0,0 +1,47 @@ +module StringSet = Set.Make (String) + +type file = { + ddeps: string list; + rdeps: StringSet.t option +} + +let graph = Hashtbl.create 503 + +let add fname = + if Hashtbl.mem graph fname then () else + Hashtbl.add graph fname {ddeps = []; rdeps = None} + +let add_ddep fname dname = + let file = Hashtbl.find graph fname in + Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps} + +let init fname dname = + add fname; add dname; add_ddep fname dname + +let rec compute fname file = match file.rdeps with + | Some rdeps -> rdeps + | None -> + let rdeps = List.fold_left (iter fname) StringSet.empty file.ddeps in + Hashtbl.replace graph fname {file with rdeps = Some rdeps}; + rdeps + +and iter fname rdeps dname = + if StringSet.mem dname rdeps then + begin Printf.printf "%s: redundant %s\n" fname dname; rdeps end + else + let file = Hashtbl.find graph dname in + StringSet.add dname (StringSet.union (compute dname file) rdeps) + +let check () = + let iter fname file = + if StringSet.mem fname (compute fname file) then + Printf.printf "%s: circular\n" fname + in + Hashtbl.iter iter graph + +let rec read ich = + let _ = Scanf.fscanf ich "./%s@:include \"%s@\". " init in + read ich + +let _ = + try read stdin with End_of_file -> check () diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 71dff0f41..964277d7f 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -1,6 +1,8 @@ H = @ XOA_DIR = ../../../components/binaries/xoa XOA = xoa.native +DEP_DIR = ../../../components/binaries/matitadep +DEP = matitadep.native CONF = ground_2/xoa.conf.xml TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma @@ -27,6 +29,14 @@ orig: $(ORIGS) @echo " ORIG basic_2" $(H)$(ORIG) basic_2 < $(ORIGS) +# dep ######################################################################## + +deps: MAS = $(shell find $* -name "*.ma") + +deps: $(DEP_DIR)/$(DEP) + @echo " MATITADEP" + $(H)grep "include \"" $(MAS) | $< + # stats ###################################################################### stats: $(PACKAGES:%=%.stats) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma index 14b516624..3965d1619 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma @@ -13,12 +13,18 @@ (**************************************************************************) include "basic_2/reducibility/cpr_delift.ma". +include "basic_2/reducibility/cpr_cpr.ma". include "basic_2/computation/cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) (* Properties on inverse basic term relocation ******************************) +lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → L ⊢ ⓓV.T1 ➡* T2. +#L #V #T1 #T2 * #T #HT1 #HT2 +@(cprs_strap2 … (ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *) +qed. + (* Basic_1: was only: pr3_gen_cabbr *) lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 → ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma index c9b39fce3..6b5889327 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/cnf.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma index e9f8062c8..a7c7c7a99 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/static/aaa_lift.ma". -include "basic_2/computation/acp_cr.ma". include "basic_2/computation/lsubc.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma new file mode 100644 index 000000000..6ecc0bb81 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma @@ -0,0 +1,179 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/dynamic/nta_ltpss.ma". +include "basic_2/dynamic/nta_thin.ma". +include "basic_2/dynamic/lsubn_nta.ma". + +lemma cpr_beta: ∀L,V1,V2,W,T1,T2. + V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2. +#L #V1 #V2 #W #T1 #T2 #HV12 * #T #HT1 #HT2 +lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2 +lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 +@(ex2_1_intro … (ⓓV2.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *) +qed. + +lemma cpr_beta2: ∀L,V1,V2,W,T1,T2. + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2. +#L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2 +lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2 +lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 +@(ex2_1_intro … (ⓓV.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *) +qed. + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Properties on context-free parallel reduction for local environments ******) + +lemma nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 → + ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. +#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U +[ #L1 #k #L2 #_ #T2 #H + >(tpr_inv_atom1 … H) -H // +| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H + >(tpr_inv_atom1 … H) -T2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ +| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H + >(tpr_inv_atom1 … H) -T2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + elim (lift_total V1 0 (i+1)) #W #HW + lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12 + @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *) +| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H + elim (tpr_inv_bind1 … H) -H * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + lapply (IHVW1 … HL12 … HV12) #HV2W1 + lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1 + lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1 + lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H + lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 + lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1 + elim (nta_fwd_correct … H) -H #U2 #HU12 + @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | #T #HT1 #HTX #H destruct + lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1 + elim (lift_total X 0 1) #Y #HXY + lapply (tpr_lift … HTX … HT1 … HXY) -T #H + lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H + elim (nta_fwd_correct … H) #T1 #HUT1 + elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H + normalize in ⊢ (??%??? → ?); #HU1 + lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct + @(nta_conv … U) // /2 width=2/ + ] +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H + elim (tpr_inv_appl1 … H) -H * + [ #V2 #Y #HV12 #HY #H destruct + elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct + lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H + elim (nta_fwd_correct … H) -H #X #H + elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ + @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) + | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + lapply (IHVW1 … HL12 … HV12) #HVW2 + lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2 + lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1 + elim (nta_fwd_correct … H1) #T #H2 + elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H + elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21 + elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 + lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2 + @(nta_conv … (ⓓV2.U2)) + [2: /2 width=2/ + |3: -h -L1 -T0 -T2 -W -U0 + |4: /3 width=2/ + ] + | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct + ] + + + + + +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU + @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) +| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct + lapply (cpr_tpss … HU12) /4 width=4/ +| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 + @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) +] +qed. + + + + + + + + + + + + + + + + + + + +fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. + + +| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/ + | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + elim (nta_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 + lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/ + | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct + elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 + lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 + lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 + lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2 + @(nta_abbr … HW2) -HW2 + @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) + ] +| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 + lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ + | -HV1 #HT1X + lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/ + ] +] +qed. + +/2 width=9/ qed. + +lemma nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A. +/2 width=5/ qed. + +lemma nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma index 1fb994c71..7394858ef 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma @@ -24,11 +24,17 @@ lemma cpcs_cprs_dx: ∀L,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ T1 ⬌* T2. #L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/ qed. +lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2. +/3 width=1/ qed. + (* Basic_1: was: pc3_pr3_x *) lemma cpcs_cprs_sn: ∀L,T1,T2. L ⊢ T2 ➡* T1 → L ⊢ T1 ⬌* T2. #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/ qed. +lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2. +/3 width=1/ qed. + lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2. #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma index e57f9f32b..b812830ee 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma @@ -20,6 +20,10 @@ include "basic_2/equivalence/cpcs_cpcs.ma". (* Properties on inverse basic term relocation ******************************) +lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → + L ⊢ T2 ⬌* ⓓV.T1. +/3 width=1/ qed. + (* Basic_1: was only: pc3_gen_cabbr *) lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 → ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma index 1bec6e57d..6dc6714a9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_ltpss.ma". include "basic_2/equivalence/cpcs_cpcs.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma index 072d951ba..401a4be64 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/grammar/cl_shift.ma". include "basic_2/unfold/tpss.ma". include "basic_2/reducibility/tpr.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma index c620b4eca..50c559734 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/aaa_ltpss.ma". include "basic_2/reducibility/ltpr_aaa.ma". include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/lcpr.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma index 2b1f4a4fd..4b1f9b51a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ltpss_ltpss.ma". include "basic_2/reducibility/ltpr_ltpss.ma". include "basic_2/reducibility/ltpr_ltpr.ma". include "basic_2/reducibility/lcpr.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma index d284060f1..303604958 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/grammar/cl_weight.ma". include "basic_2/substitution/ldrop.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma index a4c94fedc..f6cb1fa3f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lift_lift.ma". include "basic_2/unfold/tpss_tpss.ma". include "basic_2/unfold/delift.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index d8c746697..a6846d3b8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -117,6 +117,13 @@ elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU >(lift_mono … HTU2 … HT2) -T2 /2 width=3/ qed. +lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ U1 ▼*[d, e] ≡ T2 → + ∀K. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → T1 = T2. +#L #U1 #T2 #d #e * #U2 #HU12 #HTU2 #K #HLK #T1 #HTU1 +lapply (tpss_inv_lift1_eq … HU12 … HTU1) -L -K #H destruct +lapply (lift_inj … HTU1 … HTU2) -U2 // +qed-. + lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T → ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e → L ⊢ T1 ▼*[d, e] ≡ T2. -- 2.39.2