From: Ferruccio Guidi Date: Mon, 3 Jun 2013 13:45:42 +0000 (+0000) Subject: - induction on supclosure replaces induction on weight for closures everywhere X-Git-Tag: make_still_working~1140 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e2fd96302d52266bec42a19f100dadc6111fc07b;p=helm.git - induction on supclosure replaces induction on weight for closures everywhere - bug fix in csn_alt --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma index 5dd59df28..9a3154784 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma @@ -51,7 +51,7 @@ lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ elim (term_eq_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ -qed. +qed-. (* Basic_1: was: sn3_cast *) lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW. T. @@ -60,10 +60,10 @@ lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW. elim (cpr_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 - [ /3 width=3/ + [ /3 width=3 by csn_cpr_trans/ | -HLW0 * #H destruct /3 width=1/ ] -| /3 width=3/ +| /3 width=3 by csn_cpr_trans/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma index c880b2dd2..eb10f0981 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma @@ -83,7 +83,8 @@ qed. (* Basic_1: was: sn3_pr3_trans *) lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊* T2. -/4 width=3/ qed. +#L #T1 #HT1 #T2 #H @(cprs_ind … H) -T2 // /2 width=3 by csn_cpr_trans/ +qed-. (* Main eliminators *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma index 1919c111a..14da31097 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma @@ -63,7 +63,7 @@ lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → elim (cpr_fwd_abst1 … H1 I V) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 -[ /3 width=5/ +[ /3 width=5 by csn_cpr_trans/ | -HLW0 * #H destruct /3 width=1/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma index da3337eee..b406fa3f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma @@ -34,7 +34,7 @@ elim (cpr_inv_abbr1 … H1) -H1 * [ #V1 #T1 #HLV1 #HLT1 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ + @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpr_trans/ | -IHV -HLV1 * #H destruct /3 width=1/ ] | -IHV -IHT -H2 #T0 #HLT0 #HT0 @@ -54,15 +54,15 @@ elim (cpr_inv_appl1 … H) -H * elim (cpr_fwd_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_beta … H2) -H2 [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 - @csn_abbr /2 width=3/ -HV - @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3/ + @csn_abbr /2 width=3 by csn_cpr_trans/ -HV + @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/ | -IHW -HLW0 -HV -HT * #H #HVT0 destruct @(IHVT … HVT0) -IHVT -HVT0 // /3 width=1/ ] | -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct lapply (cpr_lsubr_trans … HLT01 (L.ⓓV) ?) -HLT01 /2 width=1/ #HLT01 - @csn_abbr /2 width=3/ -HV - @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ + @csn_abbr /2 width=3 by csn_cpr_trans/ -HV + @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/ | -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct ] qed-. @@ -103,7 +103,7 @@ elim (cpr_inv_appl1 … HL) -HL * | -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct | -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct lapply (cpr_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 - @csn_abbr /2 width=3/ -HV + @csn_abbr /2 width=3 by csn_cpr_trans/ -HV @(csn_lpr_conf (L. ⓓW0)) /2 width=1/ -W1 @(csn_cprs_trans … HVT) -HVT /3 width=1/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma index 2a9802626..1f79433bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma @@ -28,12 +28,6 @@ lemma fw_shift: ∀a,K,I,V,T. ♯{K. ⓑ{I} V, T} < ♯{K, ⓑ{a,I} V. T}. normalize // qed. -lemma tw_shift: ∀L,T. ♯{L, T} ≤ ♯{L @@ T}. -#L elim L // -#K #I #V #IHL #T -@transitive_le [3: @IHL |2: /2 width=2/ | skip ] -qed. - lemma fw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}. normalize in ⊢ (?→?→?→?→?%%); // qed. @@ -42,26 +36,12 @@ lemma fw_tpair_dx: ∀I,L,V,T. ♯{L, T} < ♯{L, ②{I}V.T}. normalize in ⊢ (?→?→?→?→?%%); // qed. -lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. ♯{L, V2} < ♯{L, ②{I1}V1.②{I2}V2.T}. -normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *) -qed. - -lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T. - ♯{L.ⓑ{I}V1, T} < ♯{L, ②{I1}V1.②{I2}V2.T}. -normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/ -qed. - -lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T. - ♯{L.ⓑ{I}V2, T} < ♯{L, ②{I1}V1.②{I2}V2.T}. -normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1 by monotonic_le_plus_r/ (**) (* auto too slow without trace *) -qed. - lemma fw_lpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L.ⓑ{I}V, T}. normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *) qed. (* Basic_1: removed theorems 7: - flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans - flt_wf_ind + flt_thead_sx flt_thead_dx flt_trans + flt_arith0 flt_arith1 flt_arith2 flt_wf_ind *) (* Basic_1: removed local theorems 1: q_ind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index f9a63718a..fc3b65c60 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/grammar/lpx_sn_lpx_sn.ma". -include "basic_2/relocation/fsup.ma". +include "basic_2/substitution/fsupp.ma". include "basic_2/reduction/lpr_ldrop.ma". (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) @@ -26,7 +26,7 @@ fact cpr_conf_lpr_atom_atom: fact cpr_conf_lpr_atom_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -41,7 +41,7 @@ elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ @@ -50,7 +50,7 @@ qed-. (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *) fact cpr_conf_lpr_delta_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -70,7 +70,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 @@ -79,7 +79,7 @@ qed-. fact cpr_conf_lpr_bind_bind: ∀a,I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -96,7 +96,7 @@ qed-. fact cpr_conf_lpr_bind_zeta: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -113,7 +113,7 @@ qed-. fact cpr_conf_lpr_zeta_zeta: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -132,7 +132,7 @@ qed-. fact cpr_conf_lpr_flat_flat: ∀I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -149,7 +149,7 @@ qed-. fact cpr_conf_lpr_flat_tau: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -164,7 +164,7 @@ qed-. fact cpr_conf_lpr_tau_tau: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -179,7 +179,7 @@ qed-. fact cpr_conf_lpr_flat_beta: ∀a,L0,V0,W0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} → + ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -202,7 +202,7 @@ qed-. *) fact cpr_conf_lpr_flat_theta: ∀a,L0,V0,W0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} → + ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -231,7 +231,7 @@ qed-. fact cpr_conf_lpr_beta_beta: ∀a,L0,V0,W0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} → + ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -251,7 +251,7 @@ qed-. (* Basic_1: was: pr0_upsilon_upsilon *) fact cpr_conf_lpr_theta_theta: ∀a,L0,V0,W0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} → + ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ➡ T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ➡ L2 → ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 @@ -274,8 +274,8 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ qed-. theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. -#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] -[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct +#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*] +[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1 … H1) -H1 elim (cpr_inv_atom1 … H2) -H2 [ #H2 #H1 destruct @@ -288,7 +288,7 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct /3 width=17 by cpr_conf_lpr_delta_delta/ ] -| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #a #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_bind1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 | #T1 #HT01 #HXT1 #H11 #H12 @@ -302,7 +302,7 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. | /3 width=11 by cpr_conf_lpr_bind_zeta/ | /3 width=12 by cpr_conf_lpr_zeta_zeta/ ] -| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_flat1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 | #HX1 #H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma index 060f21648..9ce690f68 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/grammar/lpx_sn_lpx_sn.ma". +include "basic_2/substitution/fsupp.ma". include "basic_2/substitution/lpss_ldrop.ma". include "basic_2/reduction/lpr_ldrop.ma". @@ -26,7 +27,7 @@ fact cpr_cpss_conf_lpr_lpss_atom_atom: fact cpr_cpss_conf_lpr_lpss_atom_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -41,7 +42,7 @@ elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ @@ -49,7 +50,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_delta_atom: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T.⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -64,7 +65,7 @@ elim (lpss_inv_pair1 … H2) -H2 #K2 #V2 #HK02 #HV02 #H destruct elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 /3 width=9/ @@ -72,7 +73,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_delta_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -92,7 +93,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 @@ -101,7 +102,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_bind_bind: ∀a,I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -118,7 +119,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_bind_zeta: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -135,7 +136,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_flat_flat: ∀I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -152,7 +153,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_flat_tau: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -167,7 +168,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_flat_beta: ∀a,L0,V0,W0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓛ{a}W0.T0} → + ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -186,7 +187,7 @@ qed-. fact cpr_cpss_conf_lpr_lpss_flat_theta: ∀a,L0,V0,W0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓐV0.ⓓ{a}W0.T0} → + ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ➡ L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ➡ T0 @@ -208,8 +209,8 @@ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T qed-. lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss. -#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] -[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct +#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*] +[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1 … H1) -H1 elim (cpss_inv_atom1 … H2) -H2 [ #H2 #H1 destruct @@ -222,7 +223,7 @@ lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss. * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct /3 width=17 by cpr_cpss_conf_lpr_lpss_delta_delta/ ] -| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #a #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H2 elim (cpr_inv_bind1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 @@ -231,7 +232,7 @@ lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss. [ /3 width=10 by cpr_cpss_conf_lpr_lpss_bind_bind/ | /3 width=11 by cpr_cpss_conf_lpr_lpss_bind_zeta/ ] -| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H2 elim (cpr_inv_flat1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma index cffa08c68..16fbeb128 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/grammar/cl_weight.ma". include "basic_2/relocation/ldrop.ma". (* SUPCLOSURE ***************************************************************) @@ -46,7 +47,7 @@ qed. (* Basic forward lemmas *****************************************************) -lemma fsup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. +lemma fsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index 85d36c39f..7d3b3b0ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/grammar/cl_weight.ma". +include "basic_2/grammar/lenv_length.ma". +include "basic_2/grammar/lenv_weight.ma". include "basic_2/relocation/lift.ma". (* LOCAL ENVIRONMENT SLICING ************************************************) @@ -246,6 +247,14 @@ qed. (* Basic forvard lemmas *****************************************************) +lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize +[ /2 width=3/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 + >(lift_fwd_tw … HV21) -HV21 /2 width=1/ +] +qed-. + (* Basic_1: was: drop_S *) lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → ⇩[O, e + 1] L1 ≡ K2. @@ -263,21 +272,6 @@ lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/ qed-. -lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize -[ /2 width=3/ -| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 - >(lift_fwd_tw … HV21) -HV21 /2 width=1/ -] -qed-. - -lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → - ∀T. ♯{K, V} < ♯{L, T}. -#I #L #K #V #d #e #H #T -lapply (ldrop_fwd_lw … H) -H #H -@(le_to_lt_to_lt … H) -H /3 width=1/ -qed-. - lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|. #L1 elim L1 -L1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma index 762911576..6cae606c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_append.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/grammar/lenv_append.ma". include "basic_2/relocation/ldrop.ma". (* DROPPING *****************************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma index f6bae4fa2..a10cc99f5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpss.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/grammar/cl_shift.ma". include "basic_2/relocation/ldrop_append.ma". include "basic_2/substitution/lsubr.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma index 149a6bd82..fb75c7338 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma @@ -21,24 +21,6 @@ definition fsupp: bi_relation lenv term ≝ bi_TC … fsup. interpretation "plus-iterated structural successor (closure)" 'SupTermPlus L1 T1 L2 T2 = (fsupp L1 T1 L2 T2). -(* Basic eliminators ********************************************************) - -lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term. - (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) → - (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2. -#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H -@(bi_TC_ind … IH1 IH2 ? ? H) -qed-. - -lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. - (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) → - (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L1 T1. -#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H -@(bi_TC_ind_dx … IH1 IH2 ? ? H) -qed-. - (* Basic properties *********************************************************) lemma fsup_fsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. @@ -79,9 +61,36 @@ lemma fsupp_append_sn: ∀I,L,K,V,T. ⦃L.ⓑ{I}V@@K, T⦄ ⊃+ ⦃L, V⦄. normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *) qed. *) +(* Basic eliminators ********************************************************) + +lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term. + (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) → + (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2. +#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H +@(bi_TC_ind … IH1 IH2 ? ? H) +qed-. + +lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. + (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) → + (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L1 T1. +#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H +@(bi_TC_ind_dx … IH1 IH2 ? ? H) +qed-. + (* Basic forward lemmas *****************************************************) -lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. +lemma fsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. #L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -L2 -T2 -/3 width=3 by fsup_fwd_cw, transitive_lt/ +/3 width=3 by fsup_fwd_fw, transitive_lt/ +qed-. + +(* Advanced eliminators *****************************************************) + +lemma fsupp_wf_ind: ∀R:relation2 lenv term. ( + ∀L1,T1. (∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2) → + ∀L2,T2. L1 = L2 → T1 = T2 → R L2 T2 + ) → ∀L1,T1. R L1 T1. +#R #HR @(f2_ind … fw) #n #IHn #L1 #T1 #H destruct /4 width=5 by fsupp_fwd_fw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma index d915b89f1..07a7b836d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma @@ -63,17 +63,12 @@ lemma fsups_fsupp_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ → lemma fsupp_fsups_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. /2 width=4/ qed. -(* -lemma fsups_pippo: ∀L,T. ⦃L, T⦄ ⊃+ ⦃L, #0⦄. -#L * * -[ #i -*) (* Basic forward lemmas *****************************************************) -lemma fsups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}. +lemma fsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}. #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 // -/4 width=3 by fsup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *) +/4 width=3 by fsup_fwd_fw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *) qed-. (* (* Advanced inversion lemmas on plus-iterated supclosure ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma index c9c17fa19..71ab873af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_cpss.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/grammar/lpx_sn_lpx_sn.ma". +include "basic_2/substitution/fsupp.ma". include "basic_2/substitution/lpss_ldrop.ma". (* SN PARALLEL SUBSTITUTION FOR LOCAL ENVIRONMENTS **************************) @@ -20,8 +21,8 @@ include "basic_2/substitution/lpss_ldrop.ma". (* Main properties on context-sensitive parallel substitution for terms *****) theorem cpss_trans_lpss: lpx_sn_transitive cpss cpss. -#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*] -[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct +#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L0 #T0 #IH #L1 * [|*] +[ #I #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct elim (cpss_inv_atom1 … H1) -H1 [ #H destruct elim (cpss_inv_atom1 … HT2) -HT2 @@ -29,19 +30,19 @@ theorem cpss_trans_lpss: lpx_sn_transitive cpss cpss. | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct elim (lpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H elim (lpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + lapply (fsupp_lref … HLK1) /3 width=9/ ] | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + lapply (fsupp_lref … HLK1) /3 width=9/ ] -| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 +| #a #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2 elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ -| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 +| #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2 elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma index ad972cd4a..12bb02b07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_lpss.ma @@ -24,7 +24,7 @@ fact cpss_conf_lpss_atom_atom: fact cpss_conf_lpss_atom_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 @@ -39,7 +39,7 @@ elim (lpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ @@ -47,7 +47,7 @@ qed-. fact cpss_conf_lpss_delta_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 @@ -67,7 +67,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 @@ -76,7 +76,7 @@ qed-. fact cpss_conf_lpss_bind_bind: ∀a,I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 @@ -93,7 +93,7 @@ qed-. fact cpss_conf_lpss_flat_flat: ∀I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 @@ -109,8 +109,8 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ qed-. theorem cpss_conf_lpss: lpx_sn_confluent cpss cpss. -#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] -[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct +#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*] +[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpss_inv_atom1 … H1) -H1 elim (cpss_inv_atom1 … H2) -H2 [ #H2 #H1 destruct @@ -123,11 +123,11 @@ theorem cpss_conf_lpss: lpx_sn_confluent cpss cpss. * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct /3 width=17 by cpss_conf_lpss_delta_delta/ ] -| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #a #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct /3 width=10 by cpss_conf_lpss_bind_bind/ -| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct /3 width=10 by cpss_conf_lpss_flat_flat/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma index fb94a49de..7b8f17b4a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_cpqs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/grammar/lpx_sn_lpx_sn.ma". +include "basic_2/substitution/fsupp.ma". include "basic_2/unfold/lpqs_ldrop.ma". (* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************) @@ -20,8 +21,8 @@ include "basic_2/unfold/lpqs_ldrop.ma". (* Main properties on context-sensitive rest parallel computation for terms *) theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs. -#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*] -[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct +#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L0 #T0 #IH #L1 * [|*] +[ #I #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct elim (cpqs_inv_atom1 … H1) -H1 [ #H destruct elim (cpqs_inv_atom1 … HT2) -HT2 @@ -29,16 +30,16 @@ theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs. | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct elim (lpqs_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H elim (lpqs_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + lapply (fsupp_lref … HLK1) /3 width=9/ ] | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct elim (lpqs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpqs_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 elim (cpqs_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + lapply (fsupp_lref … HLK1) /3 width=9/ ] -| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 +| #a #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2 elim (cpqs_inv_bind1 … H1) -H1 * [ #V #T #HV1 #HT1 #H destruct elim (cpqs_inv_bind1 … H2) -H2 * @@ -49,7 +50,7 @@ theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs cpqs. elim (lift_total X2 0 1) #Y2 #HXY2 lapply (cpqs_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/ ] -| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 +| #I #V1 #T1 #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2 elim (cpqs_inv_flat1 … H1) -H1 * [ #V #T #HV1 #HT1 #H destruct elim (cpqs_inv_flat1 … H2) -H2 * diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma index 566dd5347..13f221e86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_lpqs.ma @@ -24,7 +24,7 @@ fact cpqs_conf_lpqs_atom_atom: fact cpqs_conf_lpqs_atom_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -39,7 +39,7 @@ elim (lpqs_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpqs_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ @@ -47,7 +47,7 @@ qed-. fact cpqs_conf_lpqs_delta_delta: ∀L0,i. ( - ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -67,7 +67,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +lapply (fsupp_lref … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpqs_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 @@ -76,7 +76,7 @@ qed-. fact cpqs_conf_lpqs_bind_bind: ∀a,I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -93,7 +93,7 @@ qed-. fact cpqs_conf_lpqs_bind_zeta: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -110,7 +110,7 @@ qed-. fact cpqs_conf_lpqs_zeta_zeta: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} → + ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -129,7 +129,7 @@ qed-. fact cpqs_conf_lpqs_flat_flat: ∀I,L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -146,7 +146,7 @@ qed-. fact cpqs_conf_lpqs_flat_tau: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -161,7 +161,7 @@ qed-. fact cpqs_conf_lpqs_tau_tau: ∀L0,V0,T0. ( - ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} → + ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L,T⦄ → ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 → ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 → ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0 @@ -175,8 +175,8 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/ qed-. theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs. -#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] -[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct +#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*] +[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpqs_inv_atom1 … H1) -H1 elim (cpqs_inv_atom1 … H2) -H2 [ #H2 #H1 destruct @@ -189,7 +189,7 @@ theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs. * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct /3 width=17 by cpqs_conf_lpqs_delta_delta/ ] -| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #a #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpqs_inv_bind1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 | #T1 #HT01 #HXT1 #H11 #H12 @@ -203,7 +203,7 @@ theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs cpqs. | /3 width=11 by cpqs_conf_lpqs_bind_zeta/ | /3 width=12 by cpqs_conf_lpqs_zeta_zeta/ ] -| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpqs_inv_flat1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 | #HX1 #H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma index 4235f281e..42af90e61 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/grammar/lenv_append.ma". include "basic_2/relocation/ldrop.ma". (* CONTEXT-SENSITIVE UNFOLD FOR TERMS ***************************************)