From b0dce88ff4c55b5f811ce9e183418479f7d34d2a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Oct 2011 17:27:11 +0000 Subject: [PATCH] - cpr_lsubs_conf proved! (was pr2_change) - some "-" removed :) --- .../Basic_2/{Basic-1.txt => Basic_1.txt} | 0 .../lambda_delta/Basic_2/grammar/lsubs.ma | 32 +++++++++++++++++++ .../lambda_delta/Basic_2/reduction/cpr.ma | 9 +++++- matita/matita/contribs/lambda_delta/Makefile | 6 ++-- 4 files changed, 43 insertions(+), 4 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/{Basic-1.txt => Basic_1.txt} (100%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic-1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/Basic-1.txt rename to matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma index 93afc607a..83169d811 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma @@ -62,3 +62,35 @@ lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d → qed. (* Basic inversion lemmas ***************************************************) + +(* Basic forward lemmas ***************************************************) + +fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → + d = 0 → e = |L1| → |L1| ≤ |L2|. +#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize +[ // +| /2/ +| /3/ +| /3/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H + elim (plus_S_eq_O_false … H) +] +qed. + +lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|. +/2 width=5/ qed. + +fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → + d = 0 → e = |L2| → |L2| ≤ |L1|. +#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize +[ // +| /2/ +| /3/ +| /3/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H + elim (plus_S_eq_O_false … H) +] +qed. + +lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma index 03a500cf4..3d1280a65 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma @@ -50,6 +50,14 @@ lemma cpr_cast: ∀L,V,T1,T2. #L #V #T1 #T2 * /3/ qed. +(* Note: it does not hold replacing |L1| with |L2| *) +(* Basic_1: was only: pr2_change *) +lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → + ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2. +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/ +qed. + (* Basic inversion lemmas ***************************************************) (* Basic_1: was: pr2_gen_csort *) @@ -85,7 +93,6 @@ qed. (* pr2/fwd pr2_gen_appl pr2/fwd pr2_gen_abbr -pr2/props pr2_change pr2/subst1 pr2_subst1 pr2/subst1 pr2_gen_cabbr *) diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 77f49615d..9a7cdc1ec 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -2,10 +2,10 @@ H = @ XOA_DIR = ../../../components/binaries/xoa XOA = xoa.native -CONF = Ground-2/xoa.conf.xml -TARGETS = Ground-2/xoa_natation.ma Ground-2/xoa.ma +CONF = Ground_2/xoa.conf.xml +TARGETS = Ground_2/xoa_natation.ma Ground_2/xoa.ma -PACKAGES = Ground-2 Basic-2 +PACKAGES = Ground_2 Basic_2 all: -- 2.39.2