From 5ea90cbbb01fe0bf3b77221d9e6c87002982621f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 19 Jul 2012 13:52:06 +0000 Subject: [PATCH] - intermediate commit to allow debugging of auto tactic in xprs.ma - extended computation is now defined (its De Vrijer's reduction rt) - stratified native validity is now defined (it's supposed to be easier to deal with than native type assignment) --- .../lambda_delta/apps_2/functional/subst.ma | 4 +- .../lambda_delta/basic_2/computation/cpe.ma | 2 +- .../basic_2/computation/cprs_delift.ma | 6 +- .../basic_2/computation/cprs_lift.ma | 10 +- .../lambda_delta/basic_2/computation/csn.ma | 16 +-- .../basic_2/computation/csn_aaa.ma | 2 +- .../basic_2/computation/csn_alt.ma | 24 ++-- .../basic_2/computation/csn_cpr.ma | 10 +- .../basic_2/computation/csn_cpr_vector.ma | 2 +- .../basic_2/computation/csn_lcpr.ma | 26 ++--- .../basic_2/computation/csn_lift.ma | 22 ++-- .../basic_2/computation/csn_tstc_vector.ma | 22 ++-- .../basic_2/computation/csn_vector.ma | 2 +- .../lambda_delta/basic_2/computation/xprs.ma | 64 +++++++++++ .../basic_2/computation/xprs_lift.ma | 52 +++++++++ .../lambda_delta/basic_2/dynamic/snv.ma | 69 ++++++++++++ .../lambda_delta/basic_2/dynamic/snv_lift.ma | 79 +++++++++++++ .../basic_2/equivalence/cpcs_cpcs.ma | 4 +- .../basic_2/equivalence/cpcs_delift.ma | 6 +- .../contribs/lambda_delta/basic_2/notation.ma | 36 +++--- .../basic_2/reducibility/cnf_lift.ma | 2 +- .../basic_2/reducibility/cpr_delift.ma | 4 +- .../basic_2/reducibility/cpr_lift.ma | 6 +- .../basic_2/reducibility/tpr_delift.ma | 4 +- .../lambda_delta/basic_2/reducibility/xpr.ma | 36 ++++++ .../basic_2/reducibility/xpr_lift.ma | 48 ++++++++ .../lambda_delta/basic_2/static/lsubss.ma | 106 ++++++++++++++++++ .../basic_2/static/lsubss_ldrop.ma | 65 +++++++++++ .../basic_2/static/lsubss_lsubss.ma | 36 ++++++ .../basic_2/static/lsubss_ssta.ma | 69 ++++++++++++ .../lambda_delta/basic_2/unfold/delift.ma | 44 ++++---- .../lambda_delta/basic_2/unfold/delift_alt.ma | 20 ++-- .../basic_2/unfold/delift_delift.ma | 2 +- .../basic_2/unfold/delift_lift.ma | 38 +++---- .../basic_2/unfold/delift_ltpss.ma | 6 +- .../basic_2/unfold/delift_tpss.ma | 32 +++--- .../lambda_delta/basic_2/unfold/thin.ma | 6 +- .../basic_2/unfold/thin_delift.ma | 46 ++++---- .../lambda_delta/basic_2/unfold/thin_ldrop.ma | 16 +-- .../basic_2/unwind/sstas_sstas.ma | 2 +- 40 files changed, 837 insertions(+), 209 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma index 4c164f018..814579790 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma @@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T). (* Main properties **********************************************************) theorem fsubst_delift: ∀K,V,T,L,d. - ⇩[0, d] L ≡ K. ⓓV → L ⊢ T ▼*[d, 1] ≡ [d ← V] T. + ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [d ← V] T. #K #V #T elim T -T [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ elim (lt_or_eq_or_gt i d) #Hid @@ -49,7 +49,7 @@ qed. (* Main inversion properties ************************************************) theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → - L ⊢ T1 ▼*[d, 1] ≡ T2 → [d ← V] T1 = T2. + L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ← V] T1 = T2. #K #V #T1 elim T1 -T1 [ * #i #L #T2 #d #HLK #H [ -HLK >(delift_inv_sort1 … H) -H // diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma index 8877fa44f..285e6e4fc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma @@ -26,7 +26,7 @@ interpretation "context-sensitive parallel evaluation (term)" (* Basic_properties *********************************************************) (* Basic_1: was: nf2_sn3 *) -lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄. +lemma cpe_csn: ∀L,T1. L ⊢ ⬊* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄. #L #T1 #H @(csn_ind … H) -T1 #T1 #_ #IHT1 elim (cnf_dec L T1) /3 width=3/ 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 5ce6bb59c..96dd5bab7 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 @@ -21,15 +21,15 @@ include "basic_2/computation/cprs.ma". (* Properties on inverse basic term relocation ******************************) (* Note: this should be stated with tprs *) -lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → L ⊢ ⓓV.T1 ➡* T2. +lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ 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 → - ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 ▼*[d, e] ≡ T2. + ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → + ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2. #L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/ #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma index c3cabda9e..de134f056 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma @@ -34,7 +34,7 @@ lemma cprs_inv_lref1: ∀L,T2,i. L ⊢ #i ➡* T2 → @or_intror @(ex4_3_intro … HLK … HT12) // /3 width=3/ (**) (* explicit constructors *) | * #K #V1 #T1 #HLK #HVT1 #HT1 #Hi lapply (ldrop_fwd_ldrop2 … HLK) #H0LK - elim (cpr_inv_lift … H0LK … HT1 … HT2) -H0LK -T /4 width=6/ + elim (cpr_inv_lift1 … H0LK … HT1 … HT2) -H0LK -T /4 width=6/ ] qed-. @@ -69,10 +69,10 @@ lemma cprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 qed. (* Basic_1: was: pr3_gen_lift *) -lemma cprs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡* U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡* T2. +lemma cprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡* U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡* T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 #HU12 @(cprs_ind … HU12) -U2 /2 width=3/ -HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 -elim (cpr_inv_lift … HLK … HTU … HU2) -U -HLK /3 width=5/ +elim (cpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/ qed. 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 6b5889327..3ed310164 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -25,11 +25,11 @@ interpretation (* Basic eliminators ********************************************************) lemma csn_ind: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬇* T1 → + (∀T1. L ⊢ ⬊* T1 → (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → - ∀T. L ⊢ ⬇* T → R T. + ∀T. L ⊢ ⬊* T → R T. #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 @H0 -H0 /3 width=1/ -IHT1 /4 width=1/ qed-. @@ -38,14 +38,14 @@ qed-. (* Basic_1: was: sn3_pr2_intro *) lemma csn_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* T2) → L ⊢ ⬊* T1. /4 width=1/ qed. (* Basic_1: was: sn3_nf2 *) -lemma csn_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ ⬇* T. +lemma csn_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ ⬊* T. /2 width=1/ qed. -lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ ⬇* T2. +lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ ⬊* T2. #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csn_intro #T #HLT2 #HT2 elim (term_eq_dec T1 T2) #HT12 @@ -54,7 +54,7 @@ elim (term_eq_dec T1 T2) #HT12 qed. (* Basic_1: was: sn3_cast *) -lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓝW. T. +lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW. T. #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_cast1 … H1) -H1 @@ -69,14 +69,14 @@ qed. (* Basic forward lemmas *****************************************************) -fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T. +fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬊* T. #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 @(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed. (* Basic_1: was: sn3_gen_flat *) -lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. +lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬊* ⓕ{I} V. T → L ⊢ ⬊* T. /2 width=5/ qed-. (* Basic_1: removed theorems 14: diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma index 8b36e75ae..67744a098 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/computation/csn_tstc_vector.ma". (* Properties concerning atomic arity assignment ****************************) -lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬇* T. +lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T. #L #T #A #H @(acp_aaa … csn_acp csn_acr … H) qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma index 980b4b700..eeba707dc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma @@ -27,10 +27,10 @@ interpretation (* Basic eliminators ********************************************************) lemma csna_ind: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬇⬇* T1 → + (∀T1. L ⊢ ⬊⬊* T1 → (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → - ∀T. L ⊢ ⬇⬇* T → R T. + ∀T. L ⊢ ⬊⬊* T → R T. #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 @H0 -H0 /3 width=1/ -IHT1 /4 width=1/ qed-. @@ -39,15 +39,15 @@ qed-. (* Basic_1: was: sn3_intro *) lemma csna_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → L ⊢ ⬊⬊* T1. /4 width=1/ qed. fact csna_intro_aux: ∀L,T1. - (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. + (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → L ⊢ ⬊⬊* T1. /4 width=3/ qed-. (* Basic_1: was: sn3_pr3_trans (old version) *) -lemma csna_cprs_trans: ∀L,T1. L ⊢ ⬇⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇⬇* T2. +lemma csna_cprs_trans: ∀L,T1. L ⊢ ⬊⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊⬊* T2. #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csna_intro #T #HLT2 #HT2 elim (term_eq_dec T1 T2) #HT12 @@ -57,8 +57,8 @@ qed. (* Basic_1: was: sn3_pr2_intro (old version) *) lemma csna_intro_cpr: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → - L ⊢ ⬇⬇* T1. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → + L ⊢ ⬊⬊* T1. #L #T1 #H @csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T [ -H #H destruct #H @@ -73,25 +73,25 @@ qed. (* Main properties **********************************************************) -theorem csn_csna: ∀L,T. L ⊢ ⬇* T → L ⊢ ⬇⬇* T. +theorem csn_csna: ∀L,T. L ⊢ ⬊* T → L ⊢ ⬊⬊* T. #L #T #H @(csn_ind … H) -T /4 width=1/ qed. -theorem csna_csn: ∀L,T. L ⊢ ⬇⬇* T → L ⊢ ⬇* T. +theorem csna_csn: ∀L,T. L ⊢ ⬊⬊* T → L ⊢ ⬊* T. #L #T #H @(csna_ind … H) -T /4 width=1/ qed. (* Basic_1: was: sn3_pr3_trans *) -lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2. +lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊* T2. /4 width=3/ qed. (* Main eliminators *********************************************************) lemma csn_ind_alt: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬇* T1 → + (∀T1. L ⊢ ⬊* T1 → (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → - ∀T. L ⊢ ⬇* T → R T. + ∀T. L ⊢ ⬊* T → R T. #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1 @H0 -H0 /2 width=1/ -HT1 /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma index fba583c78..594e76139 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma @@ -19,23 +19,23 @@ include "basic_2/computation/csn.ma". (* Advanced forvard lemmas **************************************************) -fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬇* V. +fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V. #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #V2 #HLV2 #HV2 @(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ qed. (* Basic_1: was: sn3_gen_head *) -lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬇* ②{I} V. T → L ⊢ ⬇* V. +lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V. /2 width=5/ qed. -fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬇* U → - ∀I,V,T. U = ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬇* T. +fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U → + ∀I,V,T. U = ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬊* T. #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 @(IH (ⓑ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed. (* Basic_1: was: sn3_gen_bind *) -lemma csn_fwd_bind_dx: ∀I,L,V,T. L ⊢ ⬇* ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬇* T. +lemma csn_fwd_bind_dx: ∀I,L,V,T. L ⊢ ⬊* ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬊* T. /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma index 375d645f2..70c00eb11 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma @@ -17,7 +17,7 @@ include "basic_2/computation/csn_vector.ma". (* Advanced forward lemmas **************************************************) -lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T. +lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T. #L #T #Vs elim Vs -Vs /2 width=1/ #V #Vs #IHVs #HVs lapply (csn_fwd_pair_sn … HVs) #HV diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma index 4b1b9d2fc..5aa47837d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma @@ -22,13 +22,13 @@ include "basic_2/computation/csn_alt.ma". (* Advanced properties ******************************************************) -lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T. +lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT @csn_intro #T0 #HLT0 #HT0 @IHT /2 width=2/ -IHT -HT0 /2 width=3/ qed. -lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T. +lemma csn_abbr: ∀L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓV. T. #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_abbr1 … H1) -H1 * @@ -46,8 +46,8 @@ elim (cpr_inv_abbr1 … H1) -H1 * ] qed. -fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U → - ∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T. +fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → + ∀V,T. U = ⓓV. T → L ⊢ ⬊* ⓐV. ⓛW. T. #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct lapply (csn_fwd_pair_sn … HVT) #HV lapply (csn_fwd_bind_dx … HVT) #HT -HVT @@ -71,12 +71,12 @@ elim (cpr_inv_appl1 … H) -H * qed. (* Basic_1: was: sn3_beta *) -lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* ⓓV. T → - L ⊢ ⬇* ⓐV. ⓛW. T. +lemma csn_appl_beta: ∀L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓV. T → + L ⊢ ⬊* ⓐV. ⓛW. T. /2 width=3/ qed. -fact csn_appl_theta_aux: ∀L,U. L ⊢ ⬇* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T. +fact csn_appl_theta_aux: ∀L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓV. T. #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct lapply (csn_fwd_pair_sn … HVT) #HV lapply (csn_fwd_bind_dx … HVT) -HVT #HVT @@ -116,14 +116,14 @@ elim (cpr_inv_appl1 … HL) -HL * qed. lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀L,V,T. L ⊢ ⬇* ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T. + ∀L,V,T. L ⊢ ⬊* ⓓV. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓV. T. /2 width=5/ qed. (* Basic_1: was only: sn3_appl_appl *) -lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1. - L ⊢ ⬇* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) → - 𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1. +lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1. + L ⊢ ⬊* T1 → + (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → + 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @csn_intro #X #HL #H elim (cpr_inv_appl1_simple … HL ?) -HL // diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma index 85cdef226..271cc8bc6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma @@ -21,18 +21,18 @@ include "basic_2/computation/csn.ma". (* Relocation properties ****************************************************) (* Basic_1: was: sn3_lift *) -lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 → - ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬇* T2. +lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 → + ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬊* T2. #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 @csn_intro #T #HLT2 #HT2 -elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10 +elim (cpr_inv_lift1 … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct >(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/ qed. (* Basic_1: was: sn3_gen_lift *) -lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 → - ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → L2 ⊢ ⬇* T2. +lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 → + ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → L2 ⊢ ⬊* T2. #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 @csn_intro #T #HLT2 #HT2 elim (lift_total T d e) #T0 #HT0 @@ -44,7 +44,7 @@ qed. (* Advanced properties ******************************************************) (* Basic_1: was: sn3_abbr *) -lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i. +lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬊* V → L ⊢ ⬊* #i. #L #K #V #i #HLK #HV @csn_intro #X #H #Hi elim (cpr_inv_lref1 … H) -H @@ -58,7 +58,7 @@ elim (cpr_inv_lref1 … H) -H ] qed. -lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T. +lemma csn_abst: ∀L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛW. T. #L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_abst1 … H1 I V) -H1 @@ -69,9 +69,9 @@ elim (eq_false_inv_tpair_sn … H2) -H2 ] qed. -lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) → - 𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1. +lemma csn_appl_simple: ∀L,V. L ⊢ ⬊* V → ∀T1. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → + 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 @csn_intro #X #H1 #H2 elim (cpr_inv_appl1_simple … H1 ?) // -H1 @@ -91,7 +91,7 @@ qed. (* Advanced inversion lemmas ************************************************) (* Basic_1: was: sn3_gen_def *) -lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬇* #i → K ⊢ ⬇* V. +lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬊* #i → K ⊢ ⬊* V. #L #K #V #i #HLK #Hi elim (lift_total V 0 (i+1)) #V0 #HV0 lapply (ldrop_fwd_ldrop2 … HLK) #H0LK diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma index 205642fac..a33fc0ddc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -23,7 +23,7 @@ include "basic_2/computation/csn_vector.ma". (* Basic_1: was only: sn3_appls_lref *) lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → - ∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T. + ∀Vs. L ⊢ ⬊* Vs → L ⊢ ⬊* ⒶVs.T. #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H elim (csnv_inv_cons … H) -H #HV #HVs @@ -34,9 +34,9 @@ elim (H0 ?) -H0 // qed. (* Basic_1: was: sn3_appls_beta *) -lemma csn_applv_beta: ∀L,W. L ⊢ ⬇* W → - ∀Vs,V,T. L ⊢ ⬇* ⒶVs.ⓓV.T → - L ⊢ ⬇* ⒶVs. ⓐV.ⓛW. T. +lemma csn_applv_beta: ∀L,W. L ⊢ ⬊* W → + ∀Vs,V,T. L ⊢ ⬊* ⒶVs.ⓓV.T → + L ⊢ ⬊* ⒶVs. ⓐV.ⓛW. T. #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW #V0 #Vs #IHV #V #T #H1T lapply (csn_fwd_pair_sn … H1T) #HV0 @@ -51,7 +51,7 @@ qed. lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → - ∀Vs.L ⊢ ⬇* (ⒶVs. V2) → L ⊢ ⬇* (ⒶVs. #i). + ∀Vs.L ⊢ ⬊* (ⒶVs. V2) → L ⊢ ⬊* (ⒶVs. #i). #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs [ #H lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 @@ -70,8 +70,8 @@ qed. (* Basic_1: was: sn3_appls_abbr *) lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → - L ⊢ ⬇* ⒶV1s. ⓓV. T. + ∀V,T. L ⊢ ⬊* ⓓV. ⒶV2s. T → L ⊢ ⬊* V → + L ⊢ ⬊* ⒶV1s. ⓓV. T. #L #V1s #V2s * -V1s -V2s /2 width=1/ #V1s #V2s #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 @@ -88,9 +88,9 @@ elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 qed. (* Basic_1: was: sn3_appls_cast *) -lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W → - ∀Vs,T. L ⊢ ⬇* ⒶVs. T → - L ⊢ ⬇* ⒶVs. ⓝW. T. +lemma csn_applv_tau: ∀L,W. L ⊢ ⬊* W → + ∀Vs,T. L ⊢ ⬊* ⒶVs. T → + L ⊢ ⬊* ⒶVs. ⓝW. T. #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW #V #Vs #IHV #T #H1T lapply (csn_fwd_pair_sn … H1T) #HV @@ -103,7 +103,7 @@ elim (cprs_fwd_tau_vector … H) -H #H ] qed. -theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). +theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬊* T). @mk_acr // [ /3 width=1/ | /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma index 92aae5465..7c26ef429 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma @@ -26,5 +26,5 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T @ Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts. +lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬊* T @ Ts → L ⊢ ⬊* T ∧ L ⊢ ⬊* Ts. normalize // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma new file mode 100644 index 000000000..775e136cb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr.ma". +(* +include "basic_2/reducibility/cnf.ma". +*) +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +definition xprs: ∀h. sd h → lenv → relation term ≝ + λh,g,L. TC … (xpr h g L). + +interpretation "extended parallel computation (term)" + 'XPRedStar h g L T1 T2 = (xprs h g L T1 T2). + +(* Basic eliminators ********************************************************) + +lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 → + (∀T,T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → R T → R T2) → + ∀T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T2 → R T2. +#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12 +@(TC_star_ind … HT1 IHT1 … HT12) // +qed-. + +lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 → + (∀T1,T. ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → R T → R T1) → + ∀T1. ⦃h, L⦄ ⊢ T1 ➸*[g] T2 → R T1. +#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12 +@(TC_star_ind_dx … HT2 IHT2 … HT12) // +qed-. + +(* Basic properties *********************************************************) + +lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T. +/2 width=1/ qed. + +lemma xprs_strap1: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. +/2 width=3/ qed. + +lemma xprs_strap2: ∀h,g,L,T1,T,T2. + ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. +/2 width=3/ qed. + +(* Basic inversion lemmas ***************************************************) +(* +axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. +(* +#L #T #U #H @(xprs_ind_dx … H) -T // +#T0 #T #H1T0 #_ #IHT #H2T0 +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ +qed-. +*)*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma new file mode 100644 index 000000000..534badc84 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/xpr_lift.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/xprs.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +(* Advanced forward lemmas **************************************************) + +lemma xprs_fwd_abst1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛV1. T1 ➸*[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛV2. T2. +#h #g #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/ +#U #U2 #_ #HU2 * #V #T #HV1 #H destruct +elim (xpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #_ #H destruct /3 width=4/ +qed-. + +(* Relocation properties ****************************************************) + +lemma xprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → + ∀h,g,T2. ⦃h, K⦄ ⊢ T1 ➸*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → + ⦃h, L⦄ ⊢ U1 ➸*[g] U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 #HT12 @(xprs_ind … HT12) -T2 +[ -HLK #T2 #HT12 + <(lift_mono … HTU1 … HT12) -T1 // +| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2 + elim (lift_total T d e) #U #HTU + lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK (* /3 width=3/ *) + #H @(step …H) /2 width=1/ (**) (* NTypeChecker failure *) +] +qed. + +lemma xprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 ➸*[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 ➸*[g] T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 #HU12 @(xprs_ind … HU12) -U2 /2 width=3/ +-HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 +elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK (* /3 width=5/ *) +#U #HU2 #HTU @(ex2_1_intro … HU2) @(step … HT1 HTU) (**) (* NTypeChecker failure *) +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma new file mode 100644 index 000000000..23a93550c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs.ma". +include "basic_2/computation/xprs.ma". +include "basic_2/equivalence/cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ +| snv_sort: ∀L,k. snv h g L (⋆k) +| snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i) +| snv_bind: ∀I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{I}V.T) +| snv_appl: ∀L,V,W,W0,T,U,l. snv h g L V → snv h g L T → + ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → + ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U → snv h g L (ⓐV.T) +| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → + ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T) +. + +interpretation "stratified native validity (term)" + 'NativeValid h g L T = (snv h g L T). + +(* Basic inversion lemmas ***************************************************) + +lemma snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀I,V,T. X = ⓑ{I}V.T → + ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. +#h #g #L #X * -L -X +[ #L #k #I #V #T #H destruct +| #I0 #L #K #V0 #i #_ #_ #I #V #T #H destruct +| #I0 #L #V0 #T0 #HV0 #HT0 #I #V #T #H destruct /2 width=1/ +| #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #I #V #T #H destruct +| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #I #V #T #H destruct +] +qed. + +lemma snv_inv_bind: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{I}V.T :[g] → + ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. +/2 width=3/ qed-. + +lemma snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → + ∃∃W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & + ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & + ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U. +#h #g #L #X * -L -X +[ #L #k #V #T #H destruct +| #I #L #K #V0 #i #_ #_ #V #T #H destruct +| #I #L #V0 #T0 #_ #_ #V #T #H destruct +| #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=7/ +| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct +] +qed. + +lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → + ∃∃W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & + ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & + ⦃h, L⦄ ⊢ T ➸*[g] ⓛW0.U. +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma new file mode 100644 index 000000000..a2e407e30 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma @@ -0,0 +1,79 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/xprs_lift.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Relocation properties ****************************************************) + +lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊩ U :[g]. +#h #g #K #T #H elim H -K -T +[ #K #k #L #d #e #_ #X #H + >(lift_inv_sort1 … H) -X -K -d -e // +| #I #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (ldrop_trans_le … HLK … HK0 ?) -K /2 width=2/ #X #HL0 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #L0 #W #HLK0 #HVW #H destruct + /3 width=8/ + | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/ + ] +| #I #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H + elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct + /4 width=4/ +| #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct + elim (lift_total V0 d e) #W0 #HVW0 + elim (lift_total V1 d e) #W1 #HVW1 + elim (lift_total T1 (d+1) e) #U1 #HTU1 + @(snv_appl … W0 … W1 … U1 l) + [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ] + @(xprs_lift … HLK … HTU … HT1) /2 width=1/ +| #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct + elim (lift_total V d e) #W #HVW + @(snv_cast … W l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ] +] +qed. + +lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊩ T :[g]. +#h #g #L #U #H elim H -L -U +[ #L #k #K #d #e #_ #X #H + >(lift_inv_sort2 … H) -X -L -d -e // +| #I #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H + elim (lift_inv_lref2 … H) * #Hid #H destruct + [ elim (ldrop_conf_le … HLK … HL0 ?) -L /2 width=2/ #X #HK0 #H + elim (ldrop_inv_skip1 … H ?) -H /2 width=1/ -Hid #K0 #V #HLK0 #HVW #H destruct + /3 width=8/ + | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/ + ] +| #I #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H + elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/ +| #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct + elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0 + elim (cprs_inv_lift1 … HLK … HVW0 … HW01) -W0 #V1 #HVW1 #HV01 + elim (xprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU + elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct + lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=7/ +| #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct + elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW + lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index cb34d78c5..31a8d0b49 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -83,8 +83,8 @@ lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → L ⊢ U1 ⬌* U2 → K ⊢ T1 ⬌* T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 -elim (cprs_inv_lift … HLK … HTU1 … HU1) -U1 #T #HTU #HT1 -elim (cprs_inv_lift … HLK … HTU2 … HU2) -L -U2 #X #HXU +elim (cprs_inv_lift1 … HLK … HTU1 … HU1) -U1 #T #HTU #HT1 +elim (cprs_inv_lift1 … HLK … HTU2 … HU2) -L -U2 #X #HXU >(lift_inj … HXU … HTU) -X -U -d -e /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 c568941a5..e6638ea3f 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 @@ -67,14 +67,14 @@ qed-. (* Properties on inverse basic term relocation ******************************) -lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → +lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ 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 → - ∀T2. L ⊢ U2 ▼*[d, e] ≡ T2 → K ⊢ T1 ⬌* T2. + ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → + ∀T2. L ⊢ ▼*[d, e] U2 ≡ T2 → K ⊢ T1 ⬌* T2. #L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2 elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2 elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 6bbde1839..509e6a7e8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -176,31 +176,31 @@ notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }. -notation "hvbox( T1 break ▶* [ d , break e ] break term 46 T2 )" +notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break ▶* [ d , break e ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break ▶▶* [ d , break e ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. -notation "hvbox( T1 break ▼* [ d , break e ] ≡ break term 46 T2 )" +notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break ▼* [ d , break e ] ≡ break term 46 T2 )" +notation "hvbox( L ⊢ break ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. -notation "hvbox( T1 break ▼▼* [ d , break e ] ≡ break term 46 T2 )" +notation "hvbox( ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break ▼▼* [ d , break e ] ≡ break term 46 T2 )" +notation "hvbox( L ⊢ break ▼ ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $L $T1 $d $e $T2 }. @@ -214,18 +214,22 @@ notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEqA $T1 $T2 }. -notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T ÷ break term 46 A )" non associative with precedence 45 - for @{ 'BinaryArity $L $T $A }. + for @{ 'BinaryArity $h $L $T $A }. -notation "hvbox( T1 ÷ ⊑ break term 46 T2 )" +notation "hvbox( h ⊢ break term 46 L1 ÷ ⊑ break term 46 L2 )" non associative with precedence 45 - for @{ 'CrSubEqB $T1 $T2 }. + for @{ 'CrSubEqB $h $L1 $L2 }. notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break l ] break term 46 T2 )" non associative with precedence 45 for @{ 'StaticType $h $g $l $L $T1 $T2 }. +notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'CrSubEqS $h $g $L1 $L2 }. + (* Unwind *******************************************************************) notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )" @@ -296,7 +300,7 @@ notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )" non associative with precedence 45 - for @{ 'XRed $h $g $L $T1 $T2 }. + for @{ 'XPRed $h $g $L $T1 $T2 }. (* Computation **************************************************************) @@ -316,15 +320,15 @@ notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. -notation "hvbox( ⬇ * term 46 T )" +notation "hvbox( ⬊ * term 46 T )" non associative with precedence 45 for @{ 'SN $T }. -notation "hvbox( L ⊢ ⬇ * break term 46 T )" +notation "hvbox( L ⊢ ⬊ * break term 46 T )" non associative with precedence 45 for @{ 'SN $L $T }. -notation "hvbox( L ⊢ ⬇ ⬇ * break term 46 T )" +notation "hvbox( L ⊢ ⬊ ⬊ * break term 46 T )" non associative with precedence 45 for @{ 'SNAlt $L $T }. @@ -338,7 +342,7 @@ notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )" notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ * break [ g ] break term 46 T2 )" non associative with precedence 45 - for @{ 'XRedStar $h $g $L $T1 $T2 }. + for @{ 'XPRedStar $h $g $L $T1 $T2 }. notation "hvbox( ⦃ h , break L ⦄ ⊢ ➷ * break [ g ] break term 46 T2 )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma index 3aefb3643..ecb32ceed 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma @@ -55,7 +55,7 @@ qed. lemma cnf_lift: ∀L0,L,T,T0,d,e. L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄. #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H -elim (cpr_inv_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1 +elim (cpr_inv_lift1 … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1 <(HLT … HT1) in HT0; -L #HT0 >(lift_mono … HT10 … HT0) -T1 -X // qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma index 40c9074bd..04eb4ae23 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma @@ -22,8 +22,8 @@ include "basic_2/reducibility/cpr.ma". (* Basic_1: was only: pr2_gen_cabbr *) lemma thin_cpr_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡ U2 → - ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 → - ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2. + ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → + ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ ▼*[d, e] U2 ≡ T2. #L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1 elim (tpr_delift_conf … HU1 … HTU1) -U1 #T #HT1 #HUT elim (le_or_ge (|L|) d) #Hd diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma index b3dbcf40c..4a9e057e0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma @@ -151,9 +151,9 @@ elim (lt_or_ge (|K|) d) #HKd qed. (* Basic_1: was: pr2_gen_lift *) -lemma cpr_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡ U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡ T2. +lemma cpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡ U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡ T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #T #HTU #T1 elim (lt_or_ge (|L|) d) #HLd diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma index ade2050e3..99e621d15 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma @@ -19,8 +19,8 @@ include "basic_2/reducibility/tpr_tpss.ma". (* Properties on inverse basic term relocation ******************************) -lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e] ≡ T1 → - ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2. +lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ ▼*[d, e] U1 ≡ T1 → + ∃∃T2. T1 ➡ T2 & L ⊢ ▼*[d, e] U2 ≡ T2. #U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1 elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21 elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma new file mode 100644 index 000000000..78dd4502a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta.ma". +include "basic_2/reducibility/cpr.ma". + +(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) + +definition xpr: ∀h. sd h → lenv → relation term ≝ + λh,g,L,T1,T2. L ⊢ T1 ➡ T2 ∨ ∃l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2. + +interpretation + "extended parallel reduction (term)" + 'XPRed h g L T1 T2 = (xpr h g L T1 T2). + +(* Basic properties *********************************************************) + +lemma cpr_xpr: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2. +/2 width=1/ qed. + +lemma ssta_xpr: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2. +/3 width=2/ qed. + +lemma xpr_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸[g] T. +/2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma new file mode 100644 index 000000000..9b1376aaa --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_lift.ma". +include "basic_2/reducibility/cpr_lift.ma". +include "basic_2/reducibility/xpr.ma". + +(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) + +(* Advanced inversion lemmas ************************************************) + +lemma xpr_inv_abst1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛV1.T1 ➸[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 ➸[g] T2 & + U2 = ⓛV2. T2. +#h #g #L #V1 #T1 #U2 * +[ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/ +| * #l #H elim (ssta_inv_bind1 … H) /3 width=5/ +] +qed-. + +(* Relocation properties ****************************************************) + +lemma xpr_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → + ∀h,g. ⦃h, K⦄ ⊢ T1 ➸[g] T2 → ⦃h, L⦄ ⊢ U1 ➸[g] U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * [2: * ] +/3 width=9/ /3 width=10/ +qed. + +lemma xpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 ➸[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 ➸[g] T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | * #l #HU12 ] +[ elim (cpr_inv_lift1 … HLK … HTU1 … HU12) -L -U1 /3 width=3/ +| elim (ssta_inv_lift1 … HU12 … HLK … HTU1) -L -U1 /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma new file mode 100644 index 000000000..356d7fe11 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss.ma @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) + +(* Note: may not be transitive *) +inductive lsubss (h:sh) (g:sd h): relation lenv ≝ +| lsubss_atom: lsubss h g (⋆) (⋆) +| lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 → + lsubss h g (L1. ⓑ{I} W) (L2. ⓑ{I} W) +| lsubss_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V •[g, l+1] W → ⦃h, L2⦄ ⊢ V •[g, l+1] W → + lsubss h g L1 L2 → lsubss h g (L1. ⓓV) (L2. ⓛW) +. + +interpretation + "local environment refinement (stratified static type assigment)" + 'CrSubEqS h g L1 L2 = (lsubss h g L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆. +#h #g #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #l #_ #_ #_ #H destruct +] +qed. + +lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆. +/2 width=5/ qed-. + +fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → + ∀I,K1,V. L1 = K1. ⓑ{I} V → + (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & + h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr. +#h #g #L1 #L2 * -L1 -L2 +[ #I #K1 #V #H destruct +| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/ +| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/ +] +qed. + +lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V. h ⊢ K1. ⓑ{I} V •⊑[g] L2 → + (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & + h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr. +/2 width=3/ qed-. + +fact lsubss_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L2 = ⋆ → L1 = ⋆. +#h #g #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #l #_ #_ #_ #H destruct +] +qed. + +lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆. +/2 width=5/ qed-. + +fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → + ∀I,K2,W. L2 = K2. ⓑ{I} W → + (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & + h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst. +#h #g #L1 #L2 * -L1 -L2 +[ #I #K2 #W #H destruct +| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/ +| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/ +] +qed. + +lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 •⊑[g] K2. ⓑ{I} W → + (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W & + h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst. +/2 width=3/ qed-. + +(* Basic_forward lemmas *****************************************************) + +lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +(* Basic properties *********************************************************) + +lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L. +#h #g #L elim L -L // /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma new file mode 100644 index 000000000..82ede6149 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ldrop.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lsubss.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) + +(* Properties concerning basic local environment slicing ********************) + +(* Note: the constant 0 cannot be generalized *) +lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → + ∀K1,e. ⇩[0, e] L1 ≡ K1 → + ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2. +#h #g #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3/ +| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +] +qed. + +(* Note: the constant 0 cannot be generalized *) +lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → + ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1. +#h #g #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3/ +| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma new file mode 100644 index 000000000..d9f9496ba --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_lsubss.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lsubss_ssta.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STATIC TYPE ASSIGNMENT ******************) + +(* Main properties **********************************************************) + +theorem lsubss_trans: ∀h,g,L1,L. h ⊢ L1 •⊑[g] L → ∀L2. h ⊢ L •⊑[g] L2 → + h ⊢ L1 •⊑[g] L2. +#h #g #L1 #L #H elim H -L1 -L +[ #X #H >(lsubss_inv_atom1 … H) -H // +| #I #L1 #L #W #HL1 #IHL1 #X #H + elim (lsubss_inv_pair1 … H) -H * #L2 + [ #HL2 #H destruct /3 width=1/ + | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/ + ] +| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H + elim (lsubss_inv_pair1 … H) -H * #L2 + [ #HL2 #H destruct /3 width=5/ + | #V #l0 #_ #_ #_ #_ #H destruct + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma new file mode 100644 index 000000000..f9c628921 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsubss_ssta.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_lift.ma". +include "basic_2/static/ssta_ssta.ma". +include "basic_2/static/lsubss_ldrop.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) + +(* Properties concerning stratified native type assignment ******************) + +lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U → + ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U. +#h #g #L2 #T #U #l #H elim H -L2 -T -U -l +[ /2 width=1/ +| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12 + elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ] + [ #HK12 #H destruct /3 width=6/ + | #V1 #l0 #_ #_ #_ #_ #H destruct + ] +| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12 + elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ] + [ #HK12 #H destruct /3 width=6/ + | #V1 #l0 #H1 #H2 #_ #H #_ destruct + elim (ssta_fwd_correct … H2) -H2 #V #H + elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/ + ] +| /4 width=1/ +| /3 width=1/ +| /3 width=1/ +] +qed. + +lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U → + ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U. +#h #g #L1 #T #U #l #H elim H -L1 -T -U -l +[ /2 width=1/ +| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12 + elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 + elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ] + [ #HK12 #H destruct /3 width=6/ + | #V2 #l0 #H1 #H2 #_ #H #_ destruct + elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct + elim (ssta_fwd_correct … H2) -H2 /2 width=6/ + ] +| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12 + elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 + elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ] + [ #HK12 #H destruct /3 width=6/ + | #V2 #l0 #_ #_ #_ #_ #H destruct + ] +| /4 width=1/ +| /3 width=1/ +| /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index bb5b3ac4e..3c9ecc3ca 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -25,59 +25,59 @@ interpretation "inverse basic relocation (term)" (* Basic properties *********************************************************) lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 → - ∀L. L ⊢ T2 ▼*[d, e] ≡ T1. + ∀L. L ⊢ ▼*[d, e] T2 ≡ T1. /2 width=3/ qed. -lemma delift_refl_O2: ∀L,T,d. L ⊢ T ▼*[d, 0] ≡ T. +lemma delift_refl_O2: ∀L,T,d. L ⊢ ▼*[d, 0] T ≡ T. /2 width=3/ qed. -lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼*[d, e] ≡ T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▼*[d, e] ≡ T2. +lemma delift_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼*[d, e] T1 ≡ T2 → + ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼*[d, e] T1 ≡ T2. #L1 #T1 #T2 #d #e * /3 width=3/ qed. -lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k ▼*[d, e] ≡ ⋆k. +lemma delift_sort: ∀L,d,e,k. L ⊢ ▼*[d, e] ⋆k ≡ ⋆k. /2 width=3/ qed. -lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i ▼*[d, e] ≡ #i. +lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ ▼*[d, e] #i ≡ #i. /3 width=3/ qed. -lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i ▼*[d, e] ≡ #(i - e). +lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ ▼*[d, e] #i ≡ #(i - e). /3 width=3/ qed. -lemma delift_gref: ∀L,d,e,p. L ⊢ §p ▼*[d, e] ≡ §p. +lemma delift_gref: ∀L,d,e,p. L ⊢ ▼*[d, e] §p ≡ §p. /2 width=3/ qed. lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e. - L ⊢ V1 ▼*[d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 → - L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ ⓑ{I} V2. T2. + L ⊢ ▼*[d, e] V1 ≡ V2 → L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 → + L ⊢ ▼*[d, e] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2. #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2 lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/ qed. lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e. - L ⊢ V1 ▼*[d, e] ≡ V2 → L ⊢ T1 ▼*[d, e] ≡ T2 → - L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ ⓕ{I} V2. T2. + L ⊢ ▼*[d, e] V1 ≡ V2 → L ⊢ ▼*[d, e] T1 ≡ T2 → + L ⊢ ▼*[d, e] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2. #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/ qed. (* Basic inversion lemmas ***************************************************) -lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k ▼*[d, e] ≡ U2 → U2 = ⋆k. +lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ▼*[d, e] ⋆k ≡ U2 → U2 = ⋆k. #L #U2 #d #e #k * #U #HU >(tpss_inv_sort1 … HU) -HU #HU2 >(lift_inv_sort2 … HU2) -HU2 // qed-. -lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p ▼*[d, e] ≡ U2 → U2 = §p. +lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ ▼*[d, e] §p ≡ U2 → U2 = §p. #L #U #d #e #p * #U #HU >(tpss_inv_gref1 … HU) -HU #HU2 >(lift_inv_gref2 … HU2) -HU2 // qed-. -lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ U2 → - ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 & - L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 & +lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓑ{I} V1. T1 ≡ U2 → + ∃∃V2,T2. L ⊢ ▼*[d, e] V1 ≡ V2 & + L. ⓑ{I} V2 ⊢ ▼*[d+1, e] T1 ≡ T2 & U2 = ⓑ{I} V2. T2. #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct @@ -85,16 +85,16 @@ elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2 lapply (tpss_lsubs_trans … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ qed-. -lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ U2 → - ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 & - L ⊢ T1 ▼*[d, e] ≡ T2 & +lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ▼*[d, e] ⓕ{I} V1. T1 ≡ U2 → + ∃∃V2,T2. L ⊢ ▼*[d, e] V1 ≡ V2 & + L ⊢ ▼*[d, e] T1 ≡ T2 & U2 = ⓕ{I} V2. T2. #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/ qed-. -lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▼*[d, 0] ≡ T2 → T1 = T2. +lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ ▼*[d, 0] T1 ≡ T2 → T1 = T2. #L #T1 #T2 #d * #T #HT1 >(tpss_inv_refl_O2 … HT1) -HT1 #HT2 >(lift_inv_refl_O2 … HT2) -HT2 // @@ -102,7 +102,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → #[T1] ≤ #[T2]. +lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #[T1] ≤ #[T2]. #L #T1 #T2 #d #e * #T #HT1 #HT2 >(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw / qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma index 4332ec249..53832e0be 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -38,8 +38,8 @@ interpretation "inverse basic relocation (term) alternative" (* Basic properties *********************************************************) -lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 → - ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▼▼*[d, e] ≡ T2. +lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 → + ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2. #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/ [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/ @@ -48,7 +48,7 @@ lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 → ] qed. -lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼▼*[d, e] ≡ T2. +lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2. #L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1 [ * #i #IH #T2 #d #e #H [ >(delift_inv_sort1 … H) -H // @@ -73,7 +73,7 @@ qed. (* Basic inversion lemmas ***************************************************) -lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 ▼▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2. +lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ ▼▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/ qed-. @@ -81,20 +81,20 @@ lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. (∀L,d,e,k. R d e L (⋆k) (⋆k)) → (∀L,d,e,i. i < d → R d e L (#i) (#i)) → (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → - ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▼*[O, d + e - i - 1] ≡ V2 → + ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 → ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 ) → (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) → (∀L,d,e,p. R d e L (§p) (§p)) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▼*[d, e] ≡ V2 → - L.ⓑ{I}V2 ⊢ T1 ▼*[d + 1, e] ≡ T2 → R d e L V1 V2 → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 → + L.ⓑ{I}V2 ⊢ ▼*[d + 1, e] T1 ≡ T2 → R d e L V1 V2 → R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2) ) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▼*[d, e] ≡ V2 → - L⊢ T1 ▼*[d, e] ≡ T2 → R d e L V1 V2 → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 → + L⊢ ▼*[d, e] T1 ≡ T2 → R d e L V1 V2 → R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) ) → - ∀d,e,L,T1,T2. L ⊢ T1 ▼*[d, e] ≡ T2 → R d e L T1 T2. + ∀d,e,L,T1,T2. L ⊢ ▼*[d, e] T1 ≡ T2 → R d e L T1 T2. #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e // /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/ qed-. 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 f6cb1fa3f..a5c563565 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 @@ -20,7 +20,7 @@ include "basic_2/unfold/delift.ma". (* Main properties **********************************************************) theorem delift_mono: ∀L,T,T1,T2,d,e. - L ⊢ T ▼*[d, e] ≡ T1 → L ⊢ T ▼*[d, e] ≡ T2 → T1 = T2. + L ⊢ ▼*[d, e] T ≡ T1 → L ⊢ ▼*[d, e] T ≡ T2 → T1 = T2. #L #T #T1 #T2 #d #e * #U1 #H1TU1 #H2TU1 * #U2 #H1TU2 #H2TU2 elim (tpss_conf_eq … H1TU1 … H1TU2) -T #U #HU1 #HU2 lapply (tpss_inv_lift1_eq … HU1 … H2TU1) -HU1 #H destruct 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 1fc544b1b..9fe72f82d 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 @@ -21,8 +21,8 @@ include "basic_2/unfold/delift.ma". (* Advanced properties ******************************************************) lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e → - ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 → - ⇧[0, d] V2 ≡ U2 → L ⊢ #i ▼*[d, e] ≡ U2. + ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 → + ⇧[0, d] V2 ≡ U2 → L ⊢ ▼*[d, e] #i ≡ U2. #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2 elim (lift_total V 0 (i+1)) #U #HVU lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus (lift_inv_lref2_lt … HU2) // @@ -73,10 +73,10 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i ▼*[d, e] ≡ U2 → +lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ ▼*[d, e] #i ≡ U2 → d ≤ i → i < d + e → ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 & - K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 & + K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 & ⇧[0, d] V2 ≡ U2. #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide elim (tpss_inv_lref1 … HU) -HU @@ -86,7 +86,7 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → +lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 → d + e ≤ i → U2 = #(i - e). #L #U2 #i #d #e * #U #HU #HU2 #Hdei elim (tpss_inv_lref1 … HU) -HU @@ -97,11 +97,11 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → +lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 → ∨∨ (i < d ∧ U2 = #i) | (∃∃K,V1,V2. d ≤ i & i < d + e & ⇩[0, i] L ≡ K. ⓓV1 & - K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 & + K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 & ⇧[0, d] V2 ≡ U2 ) | (d + e ≤ i ∧ U2 = #(i - e)). @@ -117,10 +117,10 @@ qed-. (* Properties on basic term relocation **************************************) -lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 → +lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ ▼*[dt, et] T1 ≡ T2 → ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 → - L ⊢ U1 ▼*[dt, et] ≡ U2. + L ⊢ ▼*[dt, et] U1 ≡ U2. #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2 elim (lift_total T d e) #U #HTU lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1 @@ -128,20 +128,20 @@ elim (lift_trans_ge … HT2 … HTU ?) -T // -Hdetd #T #HT2 #HTU >(lift_mono … HTU2 … HT2) -T2 /2 width=3/ qed. -lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 → +lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ ▼*[dt, et] T1 ≡ T2 → ∀L,U1,d,e. dt ≤ d → d ≤ dt + et → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → - L ⊢ U1 ▼*[dt, et + e] ≡ T2. + L ⊢ ▼*[dt, et + e] U1 ≡ T2. #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 elim (lift_total T d e) #U #HTU lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1 lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/ qed. -lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 → +lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ ▼*[dt, et] T1 ≡ T2 → ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → - L ⊢ U1 ▼*[dt + e, et] ≡ U2. + L ⊢ ▼*[dt + e, et] U1 ≡ U2. #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2 elim (lift_total T d e) #U #HTU lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1 @@ -149,16 +149,16 @@ 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 → +lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ ▼*[d, e] U1 ≡ 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 → +lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ ▼*[i, d + e - i] T1 ≡ T → ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e → - L ⊢ T1 ▼*[d, e] ≡ T2. + L ⊢ ▼*[d, e] T1 ≡ T2. #L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10 lapply (lift_trans_be … HT2 … HT0 ? ?) -T // diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma index ee3aec8be..ba4cae69d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma @@ -19,15 +19,15 @@ include "basic_2/unfold/delift.ma". (* Properties on partial unfold on local environments ***********************) -lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → - ∀K. L ▶* [d, e] K → K ⊢ T1 ▼*[d, e] ≡ T2. +lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → + ∀K. L ▶* [d, e] K → K ⊢ ▼*[d, e] T1 ≡ T2. #L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0 lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/ qed. lemma ltpss_delift_trans_eq: ∀L,K,d,e. L ▶* [d, e] K → - ∀T1,T2. K ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2. + ∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2. #L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2 lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma index aabd723ac..cebcf828e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma @@ -20,73 +20,73 @@ include "basic_2/unfold/delift.ma". (* Properties on partial unfold on terms ************************************) lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2. + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ ▼*[dd, ee] U2 ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/ qed. lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2. + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ ▼*[dd, ee] U2 ≡ T2. /3 width=3/ qed. lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & - L ⊢ U2 ▼*[dd, ee] ≡ T2. + L ⊢ ▼*[dd, ee] U2 ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/ qed. lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & - L ⊢ U2 ▼*[dd, ee] ≡ T2. + L ⊢ ▼*[dd, ee] U2 ≡ T2. /3 width=6/ qed. lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e → ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & - L ⊢ U2 ▼*[dd, ee] ≡ T2. + L ⊢ ▼*[dd, ee] U2 ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/ qed. lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ ▼*[dd, ee] U1 ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e → ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & - L ⊢ U2 ▼*[dd, ee] ≡ T2. + L ⊢ ▼*[dd, ee] U2 ≡ T2. /3 width=3/ qed. lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T. + ∀T. L ⊢ ▼*[d, e] U1 ≡ T → L ⊢ ▼*[d, e] U2 ≡ T. #L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 lapply (tpss_inv_lift1_eq … HXU1 … HTX1) -HXU1 #H destruct /2 width=3/ qed. lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T. + ∀T. L ⊢ ▼*[d, e] U1 ≡ T → L ⊢ ▼*[d, e] U2 ≡ T. /3 width=3/ qed. lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T. + ∀T. L ⊢ ▼*[d, e] U2 ≡ T → L ⊢ ▼*[d, e] U1 ≡ T. #L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1 lapply (tpss_trans_eq … HU12 … HUX1) -U2 /2 width=3/ qed. lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T. + ∀T. L ⊢ ▼*[d, e] U2 ≡ T → L ⊢ ▼*[d, e] U1 ≡ T. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma index c86d9b160..54ec6a581 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma @@ -24,13 +24,13 @@ interpretation "basic thinning (local environment)" (* Basic properties *********************************************************) -lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 ▼*[d, e] ≡ L2. +lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ▼*[d, e] L1 ≡ L2. /2 width=3/ qed. (* Basic inversion lemmas ***************************************************) -lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 ▼*[0, e] ≡ L2 → 0 < e → - K1 ▼*[0, e - 1] ≡ L2. +lemma thin_inv_thin1: ∀I,K1,V1,L2,e. ▼*[0, e] K1.ⓑ{I} V1 ≡ L2 → 0 < e → + ▼*[0, e - 1] K1 ≡ L2. #I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma index 97f4e1fde..faf9f4506 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma @@ -20,9 +20,9 @@ include "basic_2/unfold/thin.ma". (* Inversion lemmas on inverse basic term relocation ************************) -lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 ▼*[d, e] ≡ L2 → 0 < d → - ∃∃K2,V2. K1 ▼*[d - 1, e] ≡ K2 & - K1 ⊢ V1 ▼*[d - 1, e] ≡ V2 & +lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. ▼*[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d → + ∃∃K2,V2. ▼*[d - 1, e] K1 ≡ K2 & + K1 ⊢ ▼*[d - 1, e] V1 ≡ V2 & L2 = K2. ⓑ{I} V2. #I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct @@ -32,8 +32,8 @@ qed-. (* Properties on inverse basic term relocation ******************************) -lemma thin_delift1: ∀L1,L2,d,e. L1 ▼*[d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 ▼*[d, e] ≡ V2 → - ∀I. L1.ⓑ{I}V1 ▼*[d + 1, e] ≡ L2.ⓑ{I}V2. +lemma thin_delift1: ∀L1,L2,d,e. ▼*[d, e] L1 ≡ L2 → ∀V1,V2. L1 ⊢ ▼*[d, e] V1 ≡ V2 → + ∀I. ▼*[d + 1, e] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2. #L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0 elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 //