From: Ferruccio Guidi Date: Fri, 25 Oct 2019 15:59:07 +0000 (+0200) Subject: update in basic_2 X-Git-Tag: make_still_working~223 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=21e6d5cb0c9b6d6a6b9975b78ae752120a969cd6;p=helm.git update in basic_2 + cpce parked for now + some renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma deleted file mode 100644 index b9b6560fb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma +++ /dev/null @@ -1,71 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/rt_computation/cpmuwe_cpmuwe.ma". -include "basic_2/rt_conversion/cpce_drops.ma". -include "basic_2/dynamic/cnv_cpmuwe.ma". - -(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) - -(* Properties with context-sensitive parallel eta-conversion for terms ******) - -axiom cpce_total_cnv (h) (a) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2. -(* -#h #a #G #L #T1 #HT1 -lapply (cnv_fwd_csx … HT1) #H -generalize in match HT1; -HT1 -@(csx_ind_fpbg … H) -G -L -T1 -#G #L * * -[ #s #_ #_ /2 width=2 by cpce_sort, ex_intro/ -| #i #H1i #IH #H2i - elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ] - [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W - lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W - elim (cpmuwe_total_csx … H1W) -H1W #X #n #HWX - elim (abst_dec X) [ * | -IH ] - [ #p #V1 #U #H destruct - lapply (cpmuwe_fwd_cpms … HWX) -HWX #HWX - elim (IH G K V1) -IH - [ #V2 #HV12 - elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2 - /3 width=12 by cpce_eta_drops, ex_intro/ - | /3 width=6 by cnv_cpms_trans, cnv_fwd_pair_sn/ - | /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ - ] - | #HnX - @(ex_intro … (#i)) - @cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0 - lapply (drops_mono … HLK0 … HLK) -i -L #H destruct - lapply (cpmuwe_abst … HWU0) -HWU0 #HWU0 - elim (cnv_cpmuwe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W - elim (tweq_inv_abst_sn … H) -V0 -U0 #V0 #U0 #H destruct - /2 width=4 by/ - ] - | /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/ - ] -| #l #_ #_ /2 width=2 by cpce_gref, ex_intro/ -| #p #I #V1 #T1 #_ #IH #H - elim (cnv_inv_bind … H) -H #HV1 #HT1 - elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12 - elim (IH … HT1) [| /4 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #T2 #HT12 - /3 width=2 by cpce_bind, ex_intro/ -| #I #V1 #T1 #_ #IH #H - elim (cnv_fwd_flat … H) -H #HV1 #HT1 - elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12 - elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #T2 #HT12 - /3 width=2 by cpce_flat, ex_intro/ -] -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma deleted file mode 100644 index 401b10bdb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma +++ /dev/null @@ -1,99 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/rt_transition/lpr_drops.ma". -include "basic_2/rt_computation/cpms_lpr.ma". -include "basic_2/rt_computation/fpbg_fqup.ma". -include "basic_2/rt_conversion/cpce_drops.ma". -include "basic_2/rt_conversion/lpce_drops.ma". -include "basic_2/dynamic/cnv_drops.ma". - -(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) - -definition IH (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] → - ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 → - ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 → - ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡[n,h] T. - -(* Properties with eta-conversion for full local environments ***************) - -lemma pippo_aux (h) (a) (G0) (L0) (T0): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH h a G L T) → - IH h a G0 L0 T0. -#h #a #G0 #L0 * * -[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 - elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct - lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct - /3 width=3 by cpce_sort, cpm_sort, ex2_intro/ -| #i #IH #Hi #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 - elim (cnv_inv_lref_drops … Hi) -Hi #I #K0 #W0 #HLK0 #HW0 - elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1 - elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct - elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2 - elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct - elim (cpm_inv_lref1_drops … HX1) -HX1 * - [ #H1 #H2 destruct - elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 * - [ #H1 #H2 destruct -L0 -K0 -W0 - /3 width=3 by cpce_ldef_drops, ex2_intro/ - | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02 - @(ex2_intro … (#i)) [| // ] - @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0 - /4 width=10 by lpr_cpms_trans, cpms_step_sn/ - | #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct - ] - | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1 - #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02 - lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct - lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct - elim (IH … HW0 … HW01 … HW02 … HK01 … HK02) - [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2 - elim (lifts_total W (𝐔❴↑i❵)) #V #HWV - /3 width=9 by cpce_lifts_bi, cpm_delta_drops, ex2_intro/ - | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1 - #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02 - lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct - elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 * - [ #_ #H destruct - elim (IH … HW0 … HW01 … HW02 … HK01 … HK02) - [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2 - elim (lifts_total W (𝐔❴↑i❵)) #V #HWV - /3 width=9 by cpce_lifts_bi, cpm_ell_drops, ex2_intro/ - | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2 - #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0 - elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) - [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2 - elim (lifts_total W (𝐔❴↑i❵)) #V #HWV - /4 width=11 by cpce_lifts_bi, cpm_lifts_bi, cpm_ee, ex2_intro/ - ] - ] -| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 - elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct - lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct - /3 width=3 by cpce_gref, cpr_refl, ex2_intro/ - -(* -lemma cpce_inv_eta_drops (h) (n) (G) (L) (i): - ∀X. ⦃G,L⦄ ⊢ #i ⬌η[h] X → - ∀K,W. ⇩*[i] L ≘ K.ⓛW → - ∀p,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U → - ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 → - ∀W2. ⇧*[↑i] V2 ≘ W2 → X = +ⓛW2.ⓐ#0.#↑i. - -theorem cpce_mono_cnv (h) (a) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![h,a] → - ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → T1 = T2. -#h #a #G #L #T #HT -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma index 2ff320b82..6df83d988 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma @@ -74,7 +74,7 @@ fact lsubv_inv_atom_dx_aux (h) (a) (G): qed-. (* Basic_2A1: uses: lsubsv_inv_atom2 *) -lemma lsubv_inv_atom2 (h) (a) (G): +lemma lsubv_inv_atom_dx (h) (a) (G): ∀L1. G ⊢ L1 ⫃![h,a] ⋆ → L1 = ⋆. /2 width=6 by lsubv_inv_atom_dx_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc new file mode 100644 index 000000000..c8e1d66ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv_cpce.etc @@ -0,0 +1,13 @@ +(* +lemma cpce_inv_eta_drops (h) (n) (G) (L) (i): + ∀X. ⦃G,L⦄ ⊢ #i ⬌η[h] X → + ∀K,W. ⇩*[i] L ≘ K.ⓛW → + ∀p,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U → + ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 → + ∀W2. ⇧*[↑i] V2 ≘ W2 → X = +ⓛW2.ⓐ#0.#↑i. + +theorem cpce_mono_cnv (h) (a) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → + ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → T1 = T2. +#h #a #G #L #T #HT +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc deleted file mode 100644 index 5c3b02334..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce.etc +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/rt_conversion/cpce.ma". -include "basic_2/dynamic/cnv_preserve.ma". - -(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) - -theorem cnv_cpce_mono (a) (h) (G) (L) (T): - ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ⦃G,L⦄ ⊢ T ![a,h] → - ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. -#h #G #L #T @(fqup_wf_ind (Ⓣ) … G L T) -G -L -T -#G0 #L0 #T0 #IH #T1 -@(insert_eq_0 … G0) #G -@(insert_eq_0 … L0) #L -@(insert_eq_0 … T0) #T -* -G -L -T -[ #G #L1 #s #_ #_ #_ #_ #L2 #_ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_1.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_1.etc new file mode 100644 index 000000000..b9b6560fb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_1.etc @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/cpmuwe_cpmuwe.ma". +include "basic_2/rt_conversion/cpce_drops.ma". +include "basic_2/dynamic/cnv_cpmuwe.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with context-sensitive parallel eta-conversion for terms ******) + +axiom cpce_total_cnv (h) (a) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2. +(* +#h #a #G #L #T1 #HT1 +lapply (cnv_fwd_csx … HT1) #H +generalize in match HT1; -HT1 +@(csx_ind_fpbg … H) -G -L -T1 +#G #L * * +[ #s #_ #_ /2 width=2 by cpce_sort, ex_intro/ +| #i #H1i #IH #H2i + elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ] + [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W + lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W + elim (cpmuwe_total_csx … H1W) -H1W #X #n #HWX + elim (abst_dec X) [ * | -IH ] + [ #p #V1 #U #H destruct + lapply (cpmuwe_fwd_cpms … HWX) -HWX #HWX + elim (IH G K V1) -IH + [ #V2 #HV12 + elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2 + /3 width=12 by cpce_eta_drops, ex_intro/ + | /3 width=6 by cnv_cpms_trans, cnv_fwd_pair_sn/ + | /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ + ] + | #HnX + @(ex_intro … (#i)) + @cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0 + lapply (drops_mono … HLK0 … HLK) -i -L #H destruct + lapply (cpmuwe_abst … HWU0) -HWU0 #HWU0 + elim (cnv_cpmuwe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W + elim (tweq_inv_abst_sn … H) -V0 -U0 #V0 #U0 #H destruct + /2 width=4 by/ + ] + | /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/ + ] +| #l #_ #_ /2 width=2 by cpce_gref, ex_intro/ +| #p #I #V1 #T1 #_ #IH #H + elim (cnv_inv_bind … H) -H #HV1 #HT1 + elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12 + elim (IH … HT1) [| /4 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #T2 #HT12 + /3 width=2 by cpce_bind, ex_intro/ +| #I #V1 #T1 #_ #IH #H + elim (cnv_fwd_flat … H) -H #HV1 #HT1 + elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12 + elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #T2 #HT12 + /3 width=2 by cpce_flat, ex_intro/ +] +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_2.etc new file mode 100644 index 000000000..5c3b02334 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_cpce_2.etc @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_conversion/cpce.ma". +include "basic_2/dynamic/cnv_preserve.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +theorem cnv_cpce_mono (a) (h) (G) (L) (T): + ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ⦃G,L⦄ ⊢ T ![a,h] → + ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. +#h #G #L #T @(fqup_wf_ind (Ⓣ) … G L T) -G -L -T +#G0 #L0 #T0 #IH #T1 +@(insert_eq_0 … G0) #G +@(insert_eq_0 … L0) #L +@(insert_eq_0 … T0) #T +* -G -L -T +[ #G #L1 #s #_ #_ #_ #_ #L2 #_ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc deleted file mode 100644 index 0e84ad097..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce.etc +++ /dev/null @@ -1,51 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "static_2/s_computation/fqup_weight.ma". -include "basic_2/rt_conversion/lpce.ma". -include "basic_2/dynamic/cnv_drops.ma". - -(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) - -theorem cnv_cpce_trans_lpce (h) (G): - ∀L1,T1,T2. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T2 → ⦃G,L1⦄ ⊢ T1 !*[h] → - ∀L2. ⦃G,L1⦄ ⊢ ⬌η[h] L2 → ⦃G,L2⦄ ⊢ T2 !*[h]. -#h #G #L1 #T1 @(fqup_wf_ind (Ⓣ) … G L1 T1) -G -L1 -T1 -#G0 #L0 #T0 #IH #T2 -@(insert_eq_0 … G0) #G -@(insert_eq_0 … L0) #L1 -@(insert_eq_0 … T0) #T1 -* -G -L1 -T1 -[ #G #L1 #s #_ #_ #_ #_ #L2 #_ // -| #G #K1 #V1 #HT #HL #HG #H0 #Y2 #HY2 destruct - elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct - elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct - /4 width=6 by cnv_zero, fqu_fqup, fqu_lref_O/ -| #n #G #K1 #V1 #s #_ #HT #HL #HG #H0 #Y2 #HY2 destruct - elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct - elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct - /4 width=6 by cnv_zero, fqu_fqup, fqu_lref_O/ -| #n #p #G #K1 #V1 #W1 #W2 #T1 #HVT1 #HW12 #HT #HL #HG #H0 #Y2 #HY2 destruct - elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct - elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct -| #I #G #K1 #T1 #U1 #i #H0 #HTU1 #HT #HL #HG #H0 #Y2 #HY2 destruct - elim (cnv_inv_lref … H0) -H0 #Z1 #Y1 #Hi #H destruct - elim (lpce_inv_bind_sn … HY2) -HY2 #Z2 #K2 #HK12 #_ #H destruct - @(cnv_lifts … K2 … (Ⓣ) … HTU1) [| /3 width=1 by drops_refl, drops_drop/ ] -U1 - /3 width=6 by fqu_fqup/ -| #p #I #G #K1 #V1 #V2 #T1 #T2 #HV12 #HT12 #HT #HL #HG #H0 #K2 #HK12 destruct - elim (cnv_inv_bind … H0) -H0 #HV1 #HT1 - /4 width=8 by lpce_pair, cnv_bind/ -| * #G #L1 #V1 #V2 #T1 #T2 #HV12 #HT12 #HT #HL #HG #H0 #L2 #HK12 destruct - \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc new file mode 100644 index 000000000..807b9fdc7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cnv_lpce_1.etc @@ -0,0 +1,193 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_conversion/cpce_drops.ma". +include "basic_2/rt_conversion/lpce_drops.ma". +include "basic_2/dynamic/cnv_preserve.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +definition IH_cnv_cpce_cpm_conf (h) (a): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] → + ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 → + ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T. + +definition IH_cnv_cpce_cpms_conf (h) (a): relation3 genv lenv term ≝ + λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] → + ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 → + ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T. + +(* Properties with eta-conversion for full local environments ***************) + +fact cnv_cpce_cpms_conf_sub (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) → + ∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpms_conf h a G L T. +#h #a #GX #LX #TX #HX #G #L0 #T0 #HX0 #HT0 #n #X1 #HX1 +@(cpms_ind_dx … HX1) -n -X1 +[ #T2 #HT02 #L1 #HL01 #L2 #HL02 + /2 width=8 by/ +| #n1 #n2 #T3 #T1 #HT03 #IH #HT31 #T2 #HT02 #L1 #HL01 #L2 #HL02 + lapply (cnv_cpms_trans … HT0 … HT03) -HT0 #HT3 + elim (IH … HT02 … L0 … HL02) -IH -HT02 [| // ] #T4 #HT34 #HT24 + elim (HX … HT3 … HT31 … HT34 … HL01 … HL02) + [| /2 width=4 by fpbg_cpms_trans/ ] -GX -LX -L0 -TX -T0 -T3 #T3 #HT13 #HT43 + /3 width=5 by cpms_trans, ex2_intro/ +] +qed-. + +fact cnv_cpce_cpm_conf_aux (h) (a) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) → + IH_cnv_cpce_cpm_conf h a G0 L0 T0. +#h #a #G0 #L0 * * [|||| * ] +[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 + elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct + lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct + /3 width=3 by cpce_sort, ex2_intro/ +| #i #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 + elim (cnv_inv_lref_drops … H0) -H0 #I #K0 #W0 #HLK0 #HW0 + elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1 + elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct + elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2 + elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct + elim (cpm_inv_lref1_drops … HX1) -HX1 * + [ #H1 #H2 destruct + elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 * + [ #H1 #H2 destruct -L0 -K0 -W0 + /3 width=3 by cpce_ldef_drops, ex2_intro/ + | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02 + @(ex2_intro … (#i)) [| // ] + @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0 + /4 width=10 by lpr_cpms_trans, cpms_step_sn/ + | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2 + #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct + lapply (cnv_cpms_trans … HW0 … HWU0) #H + elim (cnv_inv_bind … H) -H #HV0 #_ + elim (cnv_cpms_conf_lpr … HW0 … HWU0 0 W1 … K0 … HK01) [| // ] + [| /2 width=1 by cpm_cpms/ ] plus_S1 + /3 width=7 by cpce_lref_drops, ex2_intro/ +| #G #K #l #b #f #L #HLK #X #HX + lapply (lifts_inv_gref1 … HX) -HX #H destruct + /2 width=3 by cpce_gref, lifts_gref, ex2_intro/ +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX + elim (lifts_inv_bind1 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HLK … HVW1) -IHV #W2 #HVW2 #HW12 + elim (IHT … HTU1) -IHT -HTU1 [|*: /3 width=3 by drops_skip, ext2_pair/ ] -HVW1 #U2 #HTU2 #HU12 + /3 width=5 by cpce_bind, lifts_bind, ex2_intro/ +| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX + elim (lifts_inv_flat1 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HLK … HVW1) -IHV -HVW1 #W2 #HVW2 #HW12 + elim (IHT … HLK … HTU1) -IHT -HTU1 -HLK #U2 #HTU2 #HU12 + /3 width=5 by cpce_flat, lifts_flat, ex2_intro/ +] +qed-. +*) +lemma cpce_lifts_bi (h) (G): + d_liftable2_bi … lifts (cpce h G). +/3 width=12 by cpce_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-. + +(* Inversion lemmas with uniform slicing for local environments *************) + +axiom cpce_inv_lifts_sn (h) (G): + d_deliftable2_sn … lifts (cpce h G). +(* +#h #G #K #T1 #T2 #H elim H -G -K -T1 -T2 +[ #G #K #s #b #f #L #HLK #X #HX + lapply (lifts_inv_sort2 … HX) -HX #H destruct + /2 width=3 by cpce_sort, lifts_sort, ex2_intro/ +| #G #i #b #f #L #HLK #X #HX + elim (lifts_inv_lref2 … HX) -HX #j #Hf #H destruct + @(ex2_intro … (#j)) + [ /2 width=1 by lifts_lref/ + | @cpce_zero_drops #n #p #Y #W #V #U #HY #_ -n -p -G -V -U -i + elim (drops_inv_atom1 … HLK) -HLK #H #_ destruct -b -f + elim (drops_inv_atom1 … HY) -HY #H #_ destruct + ] +| #G #K #I #HI #b #f #L #HLK #X #HX + elim (lifts_inv_lref2 … HX) -HX #j #Hf #H destruct + @(ex2_intro … (#j)) + [ /2 width=1 by lifts_lref/ + | elim (at_inv_xxp … Hf) -Hf [| // ] #g #H1 #H2 destruct + elim (drops_inv_skip1 … HLK) -HLK #J #Y #HKY #HIJ #H destruct + @cpce_zero #n #p #W #V #U #H #HWU destruct + elim (liftsb_inv_pair_sn … HIJ) -HIJ #X #HXW #H destruct + elim (cpms_lifts_sn … HWU … HKY … HXW) -b -Y -W #X0 #H #HXU + elim (lifts_inv_bind1 … H) -H #V0 #U0 #_ #_ #H destruct -V -U + /2 width=7 by/ + ] +| #n #p #G #K #W #V1 #V2 #W2 #U #HWU #_ #HVW2 #IH #b #f #L #HLK #X #HX + elim (lifts_inv_lref2 … HX) -HX #j #Hf #H destruct + elim (at_inv_xxp … Hf) -Hf [| // ] #g #H1 #H2 destruct + elim (drops_inv_skip1 … HLK) -HLK #J #Y #HKY #HIJ #H destruct + elim (liftsb_inv_pair_dx … HIJ) -HIJ #W0 #HW0 #H destruct + elim (cpms_inv_lifts_sn … HWU … HKY … HW0) -HWU -HW0 #X #H #HWU0 + elim (lifts_inv_bind2 … H) -H #V0 #U0 #HV10 #HU0 #H destruct + elim (IH … HKY … HV10) -IH -HKY -HV10 #VX #HV2X #HV0X + lapply (lifts_trans … HV2X … HVW2 (↑g) ?) + [ /3 width=5 by after_isid_sn, after_next/ ] -V2 #H + elim (lifts_split_trans … H 𝐔❴1❵ (⫯g) ?) + [| /3 width=7 by after_isid_dx, after_push/ ] #VX2 #HVX2 #HVW2 + /5 width=10 by cpce_eta, lifts_flat, lifts_bind, lifts_lref, ex2_intro/ +| #I #G #K #T #U #i #_ #HTU #IH #b #f #L #HLK #X #HX + elim (lifts_inv_lref2 … HX) -HX #x #Hf #H destruct +(**) (* this part should be a lemma *) + elim (at_inv_xxn … Hf) -Hf [2,4: // ] * + [ #g #j #Hij #H1 #H2 destruct + elim (drops_inv_skip1 … HLK) -HLK #J #Y #HLK #_ #H destruct -I + | #g #Hij #H destruct + lapply (drops_inv_drop1 … HLK) -HLK #HLK + ] +(**) + elim (IH … HLK) -IH -HLK [1,4:|*: /2 width=2 by lifts_lref/ ] -i #T0 #HT0 #Hj + lapply (lifts_trans … HT0 … HTU (↑g) ?) + [1,3: /3 width=5 by after_isid_sn, after_next/ ] -T #H + elim (lifts_split_trans … H 𝐔❴1❵ (⫯g) ?) + [2,4: /3 width=7 by after_isid_dx, after_push/ ] #U0 #HTU0 #HU0 + /3 width=5 by cpce_lref, ex2_intro/ +| #G #K #l #b #f #L #HLK #X #HX + lapply (lifts_inv_gref2 … HX) -HX #H destruct + /2 width=3 by cpce_gref, lifts_gref, ex2_intro/ +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX + elim (lifts_inv_bind2 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HLK … HVW1) -IHV #W2 #HVW2 #HW12 + elim (IHT … HTU1) -IHT -HTU1 [|*: /3 width=3 by drops_skip, ext2_pair/ ] -HVW1 #U2 #HTU2 #HU12 + /3 width=5 by cpce_bind, lifts_bind, ex2_intro/ +| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX + elim (lifts_inv_flat2 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HLK … HVW1) -IHV -HVW1 #W2 #HVW2 #HW12 + elim (IHT … HLK … HTU1) -IHT -HTU1 -HLK #U2 #HTU2 #HU12 + /3 width=5 by cpce_flat, lifts_flat, ex2_intro/ +] +qed-. +*) +lemma cpce_inv_lifts_bi (h) (G): + d_deliftable2_bi … lifts (cpce h G). +/3 width=12 by cpce_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_ext.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_ext.etc new file mode 100644 index 000000000..5596e40a5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_ext.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/cext2.ma". +include "basic_2/rt_conversion/cpce.ma". + +(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR BINDERS ********************) + +definition cpce_ext (h) (G): relation3 lenv bind bind ≝ cext2 (cpce h G). + +interpretation + "context-sensitive parallel eta-conversion (binder)" + 'PConvEta h G L I1 I2 = (cpce_ext h G L I1 I2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce.etc new file mode 100644 index 000000000..8da6c1af4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce.etc @@ -0,0 +1,86 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/lex.ma". +include "basic_2/notation/relations/pconveta_4.ma". +include "basic_2/rt_conversion/cpce_ext.ma". + +(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************) + +definition lpce (h) (G): relation lenv ≝ lex (cpce h G). + +interpretation + "parallel eta-conversion on all entries (local environment)" + 'PConvEta h G L1 L2 = (lpce h G L1 L2). + +(* Basic properties *********************************************************) + +lemma lpce_bind (h) (G): + ∀K1,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 → + ∀I1,I2. ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 → ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] K2.ⓘ{I2}. +/2 width=1 by lex_bind/ qed. + +(* Advanced properties ******************************************************) + +lemma lpce_pair (h) (G): + ∀K1,K2,V1,V2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 → ⦃G,K1⦄ ⊢ V1 ⬌η[h] V2 → + ∀I. ⦃G,K1.ⓑ{I}V1⦄ ⊢ ⬌η[h] K2.ⓑ{I}V2. +/2 width=1 by lex_pair/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lpce_inv_atom_sn (h) (G): + ∀L2. ⦃G,⋆⦄ ⊢ ⬌η[h] L2 → L2 = ⋆. +/2 width=2 by lex_inv_atom_sn/ qed-. + +lemma lpce_inv_bind_sn (h) (G): + ∀I1,L2,K1. ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] L2 → + ∃∃I2,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L2 = K2.ⓘ{I2}. +/2 width=1 by lex_inv_bind_sn/ qed-. + +lemma lpce_inv_atom_dx (h) (G): + ∀L1. ⦃G,L1⦄ ⊢ ⬌η[h] ⋆ → L1 = ⋆. +/2 width=2 by lex_inv_atom_dx/ qed-. + +lemma lpce_inv_bind_dx (h) (G): + ∀I2,L1,K2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓘ{I2} → + ∃∃I1,K1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L1 = K1.ⓘ{I1}. +/2 width=1 by lex_inv_bind_dx/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lpce_inv_unit_sn (h) (G): + ∀I,L2,K1. ⦃G,K1.ⓤ{I}⦄ ⊢ ⬌η[h] L2 → + ∃∃K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & L2 = K2.ⓤ{I}. +/2 width=1 by lex_inv_unit_sn/ qed-. + +lemma lpce_inv_pair_sn (h) (G): + ∀I,L2,K1,V1. ⦃G,K1.ⓑ{I}V1⦄ ⊢ ⬌η[h] L2 → + ∃∃K2,V2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ V1 ⬌η[h] V2 & L2 = K2.ⓑ{I}V2. +/2 width=1 by lex_inv_pair_sn/ qed-. + +lemma lpce_inv_unit_dx (h) (G): + ∀I,L1,K2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓤ{I} → + ∃∃K1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & L1 = K1.ⓤ{I}. +/2 width=1 by lex_inv_unit_dx/ qed-. + +lemma lpce_inv_pair_dx (h) (G): + ∀I,L1,K2,V2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ V1 ⬌η[h] V2 & L1 = K1.ⓑ{I}V1. +/2 width=1 by lex_inv_pair_dx/ qed-. + +lemma lpce_inv_pair (h) (G): + ∀I1,I2,L1,L2,V1,V2. ⦃G,L1.ⓑ{I1}V1⦄ ⊢ ⬌η[h] L2.ⓑ{I2}V2 → + ∧∧ ⦃G,L1⦄ ⊢ ⬌η[h] L2 & ⦃G,L1⦄ ⊢ V1 ⬌η[h] V2 & I1 = I2. +/2 width=1 by lex_inv_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce_drops.etc new file mode 100644 index 000000000..2d683d06f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lpce_drops.etc @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/drops_lex.ma". +include "basic_2/rt_conversion/lpce.ma". + +(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************) + +(* Inversion lemmas with generic slicing for local environments *************) + +lemma lpce_drops_conf (h) (G): dropable_sn (cpce h G). +/2 width=3 by lex_dropable_sn/ qed-. + +lemma lpce_drops_trans (h) (G): dropable_dx (cpce h G). +/2 width=3 by lex_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.etc new file mode 100644 index 000000000..4c8e38a03 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_1.etc @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_conversion/cpce.ma". +include "basic_2/rt_equivalence/cpcs.ma". +include "basic_2/dynamic/lsubv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +lemma lsubv_inv_unit_dx (h) (a) (G): + ∀I,L1,K2. G ⊢ L1 ⫃![h,a] K2.ⓤ{I} → + ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & L1 = K1.ⓤ{I}. +#h #a #G #I #L1 #K2 #H +elim (lsubv_inv_bind_dx … H) -H // * +#K1 #XW #XV #_ #_ #H1 #H2 destruct +qed-. + +lemma lsubv_inv_abbr_dx (h) (a) (G): + ∀L1,K2,V. G ⊢ L1 ⫃![h,a] K2.ⓓV → + ∃∃K1. G ⊢ K1 ⫃![h,a] K2 & L1 = K1.ⓓV. +#h #a #G #L1 #K2 #V #H +elim (lsubv_inv_bind_dx … H) -H // * +#K1 #XW #XV #_ #_ #H1 #H2 destruct +qed-. + +lemma lsubv_cpce_trans_cpcs (h) (a) (G) (T0): + ∀L2,T2. ⦃G,L2⦄ ⊢ T0 ⬌η[h] T2 → ∀L1. G ⊢ L1 ⫃![h,a] L2 → + ∃∃T1. ⦃G,L1⦄ ⊢ T0 ⬌η[h] T1 & ⦃G,L1⦄ ⊢ T1 ⬌*[h] T2. +#h #a #G #T0 #L2 #T2 #H elim H -G -L2 -T0 -T2 +[ #G #L2 #s #L1 #HL12 + /2 width=3 by cpce_sort, ex2_intro/ +| #G #i #Y1 #HY1 + lapply (lsubv_inv_atom2 … HY1) -HY1 #H destruct + /2 width=3 by cpce_atom, ex2_intro/ +| #I #G #K2 #Y1 #HY1 + elim (lsubv_inv_unit_dx … HY1) -HY1 #K2 #_ #H destruct + /2 width=3 by cpce_unit, ex2_intro/ +| #G #K2 #V2 #Y1 #HY1 + elim (lsubv_inv_abbr_dx … HY1) -HY1 #K2 #_ #H destruct + /2 width=3 by cpce_ldef, ex2_intro/ +| #G #K2 #W2 #HW2 #Y1 #HY1 + elim (lsubv_inv_bind_dx … HY1) -HY1 * + [ #K1 #HK12 #H destruct + @(ex2_intro … (#0)) [| // ] + @cpce_ldec #n #p #V2 #U2 #HWU2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc new file mode 100644 index 000000000..4b5ac0061 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/lsubv_cpce_2.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_equivalence/cpes.ma". *) +include "basic_2/dynamic/cnv_cpmuwe.ma". +(* include "basic_2/dynamic/lsubv.ma". *) + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************) + +(* Properties with restricted refinement for local environments *************) + +lemma lsubr_cnuw_trans (h) (G): + ∀L2,T. ⦃G,L2⦄ ⊢ ➡𝐍𝐖*[h] T → ∀L1. L1 ⫃ L2 → ⦃G,L1⦄ ⊢ ➡𝐍𝐖*[h] T. +#h #G #L2 #T1 #HT1 #L1 #HL12 #n #T2 #HT12 + +lemma lsubv_cpmuwe_trans (h) (a) (n) (G): + lsub_trans … (cpmuwe h n G) (lsubv h a G). +#h #a #n #G #L2 #T1 #T2 * #HT12 #HT2 #L1 #HL12 +lapply (lsubv_cpms_trans … HT12 … HL12) -HT12 #HT12 +@(cpmuwe_intro … HT12) -HT12 + +lemma cnv_cpmuwe_cpms_conf (h) (a) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀n1,T1. ⦃G,L⦄ ⊢ T ➡*[n1,h] T1 → + ∀n2,T2. ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n2] T2 → + ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡*[n2-n1,h] T0 & T0 ≅ T2 & ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2. +#h #a #G #L #T0 #HT0 #n1 #T1 #HT01 #n2 #T2 * #HT02 #HT2 +elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20 +lapply (HT2 … HT20) -HT20 #HT20 +/3 width=3 by tweq_sym, ex3_intro/ +qed-. + +lemma lsubv_cpms_abst_conf_cnv (h) (a) (G) (L1) (T0): + ∀n1,p1,W1,T1. ⦃G,L1⦄ ⊢ T0 ➡*[n1,h] ⓛ{p1}W1.T1 → + ∀L2. ⦃G,L2⦄ ⊢ T0 ![h,a] → G ⊢ L1 ⫃![h,a] L2 → + ∃∃n2,p2,W2,T2. ⦃G,L2⦄ ⊢ T0 ➡*[n2,h] ⓛ{p2}W2.T2. +#h #a #G #L1 #T0 #n1 #p1 #W1 #T1 #HT01 #L2 #HT0 #HL12 +elim (cnv_R_cpmuwe_total … HT0) #n2 * #X2 #HT02 +elim (abst_dec X2) [ * | #HnX2 ] +[ #p2 #W2 #T2 #H destruct + /3 width=5 by cpmuwe_fwd_cpms, ex1_4_intro/ +| lapply (lsubv_cnv_trans … HT0 … HL12) -HT0 #HT0 + lapply (lsubv_cpmuwe_trans … HT02 … HL12) -HT02 -HL12 #HT02 + elim (cnv_cpmuwe_cpms_conf … HT0 … HT01 … HT02) -HT0 -HT01 -HT02 #U2 #H1 #H2 #_ + elim (cpms_inv_abst_sn … H1) -H1 #W2 #T2 #_ #_ #H destruct + elim (tweq_inv_abst_sn … H2) -W2 -T2 #W2 #T2 #H destruct + elim (HnX2 p1 W2 T2) -HnX2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma deleted file mode 100644 index 5ba7d4f3e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma +++ /dev/null @@ -1,219 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/notation/relations/pconveta_5.ma". -include "basic_2/rt_computation/cpms.ma". - -(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************) - -(* avtivate genv *) -inductive cpce (h): relation4 genv lenv term term ≝ -| cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s) -| cpce_atom: ∀G,i. cpce h G (⋆) (#i) (#i) -| cpce_unit: ∀I,G,K. cpce h G (K.ⓤ{I}) (#0) (#0) -| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0) -| cpce_ldec: ∀G,K,W. (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → - cpce h G (K.ⓛW) (#0) (#0) -| cpce_eta : ∀n,p,G,K,W,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → - cpce h G K W W1 → ⇧*[1] W1 ≘ W2 → - cpce h G K V V1 → ⇧*[1] V1 ≘ V2 → - cpce h G (K.ⓛW) (#0) (ⓝW2.+ⓛV2.ⓐ#0.#1) -| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T → - ⇧*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U -| cpce_gref: ∀G,L,l. cpce h G L (§l) (§l) -| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2. - cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 → - cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) -| cpce_flat: ∀I,G,L,V1,V2,T1,T2. - cpce h G L V1 V2 → cpce h G L T1 T2 → - cpce h G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) -. - -interpretation - "context-sensitive parallel eta-conversion (term)" - 'PConvEta h G L T1 T2 = (cpce h G L T1 T2). - -(* Basic inversion lemmas ***************************************************) - -lemma cpce_inv_sort_sn (h) (G) (L) (s): - ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2. -#h #G #Y #s0 #X2 -@(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2 -[ #G #L #s #_ // -| #G #i #_ // -| #I #G #K #_ // -| #G #K #V #_ // -| #G #K #W #_ #_ // -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H destruct -| #G #L #l #_ // -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct -] -qed-. - -lemma cpce_inv_atom_sn (h) (G) (i): - ∀X2. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2. -#h #G #i0 #X2 -@(insert_eq_0 … LAtom) #Y -@(insert_eq_0 … (#i0)) #X1 -* -G -Y -X1 -X2 -[ #G #L #s #_ #_ // -| #G #i #_ #_ // -| #I #G #K #_ #_ // -| #G #K #V #_ #_ // -| #G #K #W #_ #_ #_ // -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #_ #H destruct -| #G #L #l #_ #_ // -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -] -qed-. - -lemma cpce_inv_unit_sn (h) (I) (G) (K): - ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2. -#h #I0 #G #K0 #X2 -@(insert_eq_0 … (K0.ⓤ{I0})) #Y -@(insert_eq_0 … (#0)) #X1 -* -G -Y -X1 -X2 -[ #G #L #s #_ #_ // -| #G #i #_ #_ // -| #I #G #K #_ #_ // -| #G #K #V #_ #_ // -| #G #K #W #_ #_ #_ // -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H #_ destruct -| #G #L #l #_ #_ // -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -] -qed-. - -lemma cpce_inv_ldef_sn (h) (G) (K) (V): - ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2. -#h #G #K0 #V0 #X2 -@(insert_eq_0 … (K0.ⓓV0)) #Y -@(insert_eq_0 … (#0)) #X1 -* -G -Y -X1 -X2 -[ #G #L #s #_ #_ // -| #G #i #_ #_ // -| #I #G #K #_ #_ // -| #G #K #V #_ #_ // -| #G #K #W #_ #_ #_ // -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H #_ destruct -| #G #L #l #_ #_ // -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -] -qed-. - -lemma cpce_inv_ldec_sn (h) (G) (K) (W): - ∀X2. ⦃G,K.ⓛW⦄ ⊢ #0 ⬌η[h] X2 → - ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2 - | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U - & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[1] W1 ≘ W2 - & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[1] V1 ≘ V2 - & ⓝW2.+ⓛV2.ⓐ#0.#1 = X2. -#h #G #K0 #W0 #X2 -@(insert_eq_0 … (K0.ⓛW0)) #Y -@(insert_eq_0 … (#0)) #X1 -* -G -Y -X1 -X2 -[ #G #L #s #H #_ destruct -| #G #i #_ #H destruct -| #I #G #K #_ #H destruct -| #G #K #V #_ #H destruct -| #G #K #W #HW #_ #H destruct /4 width=5 by or_introl, conj/ -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #HWU #HW1 #HW12 #HV1 #HV12 #_ #H destruct - /3 width=14 by or_intror, ex6_8_intro/ -| #I #G #K #T #U #i #_ #_ #H #_ destruct -| #G #L #l #H #_ destruct -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -] -qed-. - -lemma cpce_inv_lref_sn (h) (I) (G) (K) (i): - ∀X2. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 → - ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⇧*[1] T2 ≘ X2. -#h #I0 #G #K0 #i0 #X2 -@(insert_eq_0 … (K0.ⓘ{I0})) #Y -@(insert_eq_0 … (#↑i0)) #X1 -* -G -Y -X1 -X2 -[ #G #L #s #H #_ destruct -| #G #i #_ #H destruct -| #I #G #K #H #_ destruct -| #G #K #V #H #_ destruct -| #G #K #W #_ #H #_ destruct -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H #_ destruct -| #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/ -| #G #L #l #H #_ destruct -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct -] -qed-. - -lemma cpce_inv_gref_sn (h) (G) (L) (l): - ∀X2. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2. -#h #G #Y #l0 #X2 -@(insert_eq_0 … (§l0)) #X1 * -G -Y -X1 -X2 -[ #G #L #s #_ // -| #G #i #_ // -| #I #G #K #_ // -| #G #K #V #_ // -| #G #K #W #_ #_ // -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H destruct -| #G #L #l #_ // -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct -] -qed-. - -lemma cpce_inv_bind_sn (h) (p) (I) (G) (K) (V1) (T1): - ∀X2. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 → - ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2. -#h #p0 #I0 #G #Y #V0 #T0 #X2 -@(insert_eq_0 … (ⓑ{p0,I0}V0.T0)) #X1 * -G -Y -X1 -X2 -[ #G #L #s #H destruct -| #G #i #H destruct -| #I #G #K #H destruct -| #G #K #V #H destruct -| #G #K #W #_ #H destruct -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H destruct -| #G #L #l #H destruct -| #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct -] -qed-. - -lemma cpce_inv_flat_sn (h) (I) (G) (L) (V1) (T1): - ∀X2. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 → - ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2. -#h #I0 #G #Y #V0 #T0 #X2 -@(insert_eq_0 … (ⓕ{I0}V0.T0)) #X1 * -G -Y -X1 -X2 -[ #G #L #s #H destruct -| #G #i #H destruct -| #I #G #K #H destruct -| #G #K #V #H destruct -| #G #K #W #_ #H destruct -| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H destruct -| #G #L #l #H destruct -| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct -| #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma deleted file mode 100644 index fbf7b3002..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma +++ /dev/null @@ -1,291 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "ground_2/xoa/ex_7_8.ma". -include "basic_2/rt_computation/cpms_drops.ma". -include "basic_2/rt_conversion/cpce.ma". - -(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************) - -(* Advanced properties ******************************************************) - -lemma cpce_ldef_drops (h) (G) (K) (V): - ∀i,L. ⇩*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i ⬌η[h] #i. -#h #G #K #V #i elim i -i -[ #L #HLK - lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct - /2 width=1 by cpce_ldef/ -| #i #IH #L #HLK - elim (drops_inv_succ … HLK) -HLK #Z #Y #HYK #H destruct - /3 width=3 by cpce_lref/ -] -qed. - -lemma cpce_ldec_drops (h) (G) (K) (W): - (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → - ∀i,L. ⇩*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i ⬌η[h] #i. -#h #G #K #W #HW #i elim i -i -[ #L #HLK - lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct - /3 width=5 by cpce_ldec/ -| #i #IH #L #HLK - elim (drops_inv_succ … HLK) -HLK #Z #Y #HYK #H destruct - /3 width=3 by cpce_lref/ -] -qed. - -lemma cpce_eta_drops (h) (G) (K) (W): - ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → - ∀W1. ⦃G,K⦄ ⊢ W ⬌η[h] W1 → ∀V1. ⦃G,K⦄ ⊢ V ⬌η[h] V1 → - ∀i,L. ⇩*[i] L ≘ K.ⓛW → ∀W2. ⇧*[↑i] W1 ≘ W2 → - ∀V2. ⇧*[↑i] V1 ≘ V2 → ⦃G,L⦄ ⊢ #i ⬌η[h] ⓝW2.+ⓛV2.ⓐ#0.#↑i. -#h #G #K #W #n #p #V #U #HWU #W1 #HW1 #V1 #HV1 #i elim i -i -[ #L #HLK #W2 #HW12 #V2 #HV12 - lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct - /2 width=8 by cpce_eta/ -| #i #IH #L #HLK #W2 #HW12 #V2 #HV12 - elim (drops_inv_succ … HLK) -HLK #I #Y #HYK #H destruct - elim (lifts_split_trans … HW12 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #XW #HXW1 #HXW2 - elim (lifts_split_trans … HV12 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #XV #HXV1 #HXV2 - /6 width=9 by cpce_lref, lifts_push_lref, lifts_bind, lifts_flat/ -] -qed. - -lemma cpce_lref_drops (h) (G) (K) (i): - ∀T. ⦃G,K⦄ ⊢ #i ⬌η[h] T → ∀j,L. ⇩*[j] L ≘ K → - ∀U. ⇧*[j] T ≘ U → ⦃G,L⦄ ⊢ #(j+i) ⬌η[h] U. -#h #G #K #i #T #Hi #j elim j -j -[ #L #HLK #U #HTU - lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct - lapply (lifts_fwd_isid … HTU ?) -HTU [ // ] #H destruct // -| #j #IH #Y #HYK #X #HTX -Hi - elim (drops_inv_succ … HYK) -HYK #I #L #HLK #H destruct - elim (lifts_split_trans … HTX (𝐔❴j❵) (𝐔❴1❵)) [| // ] #U #HTU #HUX - /3 width=3 by cpce_lref/ -] -qed-. - -(* Advanced inversion lemmas ************************************************) - -axiom cpce_inv_lref_sn_drops_pair (h) (G) (i) (L): - ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → - ∀I,K,W. ⇩*[i] L ≘ K.ⓑ{I}W → - ∨∨ ∧∧ Abbr = I & #i = X2 - | ∧∧ Abst = I & ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2 - | ∃∃n,p,W1,W2,V,V1,V2,U. Abst = I & ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U - & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[↑i] W1 ≘ W2 - & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[↑i] V1 ≘ V2 - & ⓝW2.+ⓛV2.ⓐ#0.#(↑i) = X2. - -axiom cpce_inv_lref_sn_drops_ldef (h) (G) (i) (L): - ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → - ∀K,V. ⇩*[i] L ≘ K.ⓓV → #i = X2. - -axiom cpce_inv_lref_sn_drops_ldec (h) (G) (i) (L): - ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → - ∀K,W. ⇩*[i] L ≘ K.ⓛW → - ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2 - | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U - & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[↑i] W1 ≘ W2 - & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[↑i] V1 ≘ V2 - & ⓝW2.+ⓛV2.ⓐ#0.#(↑i) = X2. -(* -#h #G #i elim i -i -[ #L #X2 #HX2 #I #K #HLK - lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct - /2 width=1 by cpce_inv_zero_sn/ -| #i #IH #L0 #X0 #HX0 #J #K #H0 - elim (drops_inv_succ … H0) -H0 #I #L #HLK #H destruct - elim (cpce_inv_lref_sn … HX0) -HX0 #X2 #HX2 #HX20 - elim (IH … HX2 … HLK) -IH -I -L * - [ #HJ #H destruct - lapply (lifts_inv_lref1_uni … HX20) -HX20 #H destruct - /4 width=7 by or_introl, conj/ - | #n #p #W #V1 #V2 #W2 #U #HWU #HV12 #HVW2 #H1 #H2 destruct - elim (lifts_inv_bind1 … HX20) -HX20 #X2 #X #HWX2 #HX #H destruct - elim (lifts_inv_flat1 … HX) -HX #X0 #X1 #H0 #H1 #H destruct - lapply (lifts_inv_push_zero_sn … H0) -H0 #H destruct - elim (lifts_inv_push_succ_sn … H1) -H1 #j #Hj #H destruct - lapply (lifts_inv_lref1_uni … Hj) -Hj #H destruct - /4 width=12 by lifts_trans_uni, ex5_7_intro, or_intror/ - ] -] -qed-. - -lemma cpce_inv_zero_sn_drops (h) (G) (i) (L): - ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → - ∀I,K. ⇩*[i] L ≘ K.ⓘ{I} → - (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → - #i = X2. -#h #G #i #L #X2 #HX2 #I #K #HLK #HI -elim (cpce_inv_lref_sn_drops_bind … HX2 … HLK) -L * -[ #_ #H // -| #n #p #W #V1 #V2 #W2 #U #HWU #_ #_ #H destruct - elim (HI … HWU) -n -p -K -X2 -V1 -V2 -W2 -U -i // -] -qed-. -*) -(* Properties with uniform slicing for local environments *******************) - -axiom cpce_lifts_sn (h) (G): - d_liftable2_sn … lifts (cpce h G). -(* -#h #G #K #T1 #T2 #H elim H -G -K -T1 -T2 -[ #G #K #s #b #f #L #HLK #X #HX - lapply (lifts_inv_sort1 … HX) -HX #H destruct - /2 width=3 by cpce_sort, lifts_sort, ex2_intro/ -| #G #i #b #f #L #HLK #X #HX - elim (lifts_inv_lref1 … HX) -HX #j #Hf #H destruct - @(ex2_intro … (#j)) - [ /2 width=1 by lifts_lref/ - | @cpce_zero_drops #n #p #Y #W #V #U #HY #_ - elim (drops_inv_atom2 … HLK) -HLK #j1 #g #HLK #Hg - elim (after_at_fwd … Hf … Hg) -f #j2 #_ #Hj -g -i - lapply (at_inv_uni … Hj) -Hj #H destruct - lapply (drops_conf … HLK … HY ??) -L [3:|*: // ] #H - elim (drops_inv_atom1 … H) -H #H #_ destruct - ] -| #G #K #I #HI #b #f #L #HLK #X #HX - elim (lifts_inv_lref1 … HX) -HX #j #Hf #H destruct - @(ex2_intro … (#j)) - [ /2 width=1 by lifts_lref/ - | elim (drops_split_trans_bind2 … HLK … Hf) -HLK -Hf #J #Y1 #HY1 #HK #HIJ - @cpce_zero_drops #n #p #Y2 #W #V #U #HY2 #HWU - lapply (drops_mono … HY2 … HY1) -L #H destruct - elim (liftsb_inv_pair_dx … HIJ) -HIJ #X #HXW #H destruct - elim (cpms_inv_lifts_sn … HWU … HK … HXW) -b -Y1 -W #X0 #H #HXU - elim (lifts_inv_bind2 … H) -H #V0 #U0 #_ #_ #H destruct -f -j -V -U - /2 width=7 by/ - ] -| #n #p #G #K #W #V1 #V2 #W2 #U #HWU #_ #HVW2 #IH #b #f #L #HLK #X #HX - elim (lifts_inv_lref1 … HX) -HX #j #Hf #H destruct - elim (drops_split_trans_bind2 … HLK … Hf) -HLK #J #Y #HY #HK #HIJ - elim (liftsb_inv_pair_sn … HIJ) -HIJ #W0 #HW0 #H destruct - elim (cpms_lifts_sn … HWU … HK … HW0) -HWU -HW0 #X #H #HWU0 - elim (lifts_inv_bind1 … H) -H #V0 #U0 #HV10 #HU0 #H destruct - elim (IH … HK … HV10) -IH -HK -HV10 #VX #HV2X #HV0X - elim (lifts_total W2 f) #WX2 #HWX2 - lapply (lifts_trans … HVW2 … HWX2 ??) [3:|*: // ] -HVW2 #HVX2 - @(ex2_intro … (+ⓛWX2.ⓐ#O.#(↑j))) - [ /5 width=1 by lifts_lref, lifts_bind, lifts_flat, at_S1/ - | /4 width=18 by cpce_eta_drops, lifts_conf, after_uni_succ_dx/ - ] -| #I #G #K #T #U #i #_ #HTU #IH #b #f #L #HLK #X #HX - elim (lifts_inv_lref1 … HX) -HX #x #Hf #H destruct - elim (at_inv_nxx … Hf) -Hf [|*: // ] #j #Hf #H destruct - elim (drops_split_trans_bind2 … HLK) -HLK [|*: // ] #Z #Y #HLY #HYK #_ -I - lapply (drops_isuni_fwd_drop2 … HLY) -HLY [ // ] #HLY - elim (IH … HYK) -IH -HYK [|*: /2 width=2 by lifts_lref/ ] -i #T0 #HT0 #Hj - elim (lifts_total U f) #U0 #HU0 - lapply (lifts_trans … HTU … HU0 ??) [3:|*: // ] -HTU #HTU0 - lapply (lifts_conf … HT0 … HTU0 ??) -T - [3:|*: /2 width=3 by after_uni_succ_dx/ ] #HTU0 >plus_S1 - /3 width=7 by cpce_lref_drops, ex2_intro/ -| #G #K #l #b #f #L #HLK #X #HX - lapply (lifts_inv_gref1 … HX) -HX #H destruct - /2 width=3 by cpce_gref, lifts_gref, ex2_intro/ -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX - elim (lifts_inv_bind1 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct - elim (IHV … HLK … HVW1) -IHV #W2 #HVW2 #HW12 - elim (IHT … HTU1) -IHT -HTU1 [|*: /3 width=3 by drops_skip, ext2_pair/ ] -HVW1 #U2 #HTU2 #HU12 - /3 width=5 by cpce_bind, lifts_bind, ex2_intro/ -| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX - elim (lifts_inv_flat1 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct - elim (IHV … HLK … HVW1) -IHV -HVW1 #W2 #HVW2 #HW12 - elim (IHT … HLK … HTU1) -IHT -HTU1 -HLK #U2 #HTU2 #HU12 - /3 width=5 by cpce_flat, lifts_flat, ex2_intro/ -] -qed-. -*) -lemma cpce_lifts_bi (h) (G): - d_liftable2_bi … lifts (cpce h G). -/3 width=12 by cpce_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-. - -(* Inversion lemmas with uniform slicing for local environments *************) - -axiom cpce_inv_lifts_sn (h) (G): - d_deliftable2_sn … lifts (cpce h G). -(* -#h #G #K #T1 #T2 #H elim H -G -K -T1 -T2 -[ #G #K #s #b #f #L #HLK #X #HX - lapply (lifts_inv_sort2 … HX) -HX #H destruct - /2 width=3 by cpce_sort, lifts_sort, ex2_intro/ -| #G #i #b #f #L #HLK #X #HX - elim (lifts_inv_lref2 … HX) -HX #j #Hf #H destruct - @(ex2_intro … (#j)) - [ /2 width=1 by lifts_lref/ - | @cpce_zero_drops #n #p #Y #W #V #U #HY #_ -n -p -G -V -U -i - elim (drops_inv_atom1 … HLK) -HLK #H #_ destruct -b -f - elim (drops_inv_atom1 … HY) -HY #H #_ destruct - ] -| #G #K #I #HI #b #f #L #HLK #X #HX - elim (lifts_inv_lref2 … HX) -HX #j #Hf #H destruct - @(ex2_intro … (#j)) - [ /2 width=1 by lifts_lref/ - | elim (at_inv_xxp … Hf) -Hf [| // ] #g #H1 #H2 destruct - elim (drops_inv_skip1 … HLK) -HLK #J #Y #HKY #HIJ #H destruct - @cpce_zero #n #p #W #V #U #H #HWU destruct - elim (liftsb_inv_pair_sn … HIJ) -HIJ #X #HXW #H destruct - elim (cpms_lifts_sn … HWU … HKY … HXW) -b -Y -W #X0 #H #HXU - elim (lifts_inv_bind1 … H) -H #V0 #U0 #_ #_ #H destruct -V -U - /2 width=7 by/ - ] -| #n #p #G #K #W #V1 #V2 #W2 #U #HWU #_ #HVW2 #IH #b #f #L #HLK #X #HX - elim (lifts_inv_lref2 … HX) -HX #j #Hf #H destruct - elim (at_inv_xxp … Hf) -Hf [| // ] #g #H1 #H2 destruct - elim (drops_inv_skip1 … HLK) -HLK #J #Y #HKY #HIJ #H destruct - elim (liftsb_inv_pair_dx … HIJ) -HIJ #W0 #HW0 #H destruct - elim (cpms_inv_lifts_sn … HWU … HKY … HW0) -HWU -HW0 #X #H #HWU0 - elim (lifts_inv_bind2 … H) -H #V0 #U0 #HV10 #HU0 #H destruct - elim (IH … HKY … HV10) -IH -HKY -HV10 #VX #HV2X #HV0X - lapply (lifts_trans … HV2X … HVW2 (↑g) ?) - [ /3 width=5 by after_isid_sn, after_next/ ] -V2 #H - elim (lifts_split_trans … H 𝐔❴1❵ (⫯g) ?) - [| /3 width=7 by after_isid_dx, after_push/ ] #VX2 #HVX2 #HVW2 - /5 width=10 by cpce_eta, lifts_flat, lifts_bind, lifts_lref, ex2_intro/ -| #I #G #K #T #U #i #_ #HTU #IH #b #f #L #HLK #X #HX - elim (lifts_inv_lref2 … HX) -HX #x #Hf #H destruct -(**) (* this part should be a lemma *) - elim (at_inv_xxn … Hf) -Hf [2,4: // ] * - [ #g #j #Hij #H1 #H2 destruct - elim (drops_inv_skip1 … HLK) -HLK #J #Y #HLK #_ #H destruct -I - | #g #Hij #H destruct - lapply (drops_inv_drop1 … HLK) -HLK #HLK - ] -(**) - elim (IH … HLK) -IH -HLK [1,4:|*: /2 width=2 by lifts_lref/ ] -i #T0 #HT0 #Hj - lapply (lifts_trans … HT0 … HTU (↑g) ?) - [1,3: /3 width=5 by after_isid_sn, after_next/ ] -T #H - elim (lifts_split_trans … H 𝐔❴1❵ (⫯g) ?) - [2,4: /3 width=7 by after_isid_dx, after_push/ ] #U0 #HTU0 #HU0 - /3 width=5 by cpce_lref, ex2_intro/ -| #G #K #l #b #f #L #HLK #X #HX - lapply (lifts_inv_gref2 … HX) -HX #H destruct - /2 width=3 by cpce_gref, lifts_gref, ex2_intro/ -| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX - elim (lifts_inv_bind2 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct - elim (IHV … HLK … HVW1) -IHV #W2 #HVW2 #HW12 - elim (IHT … HTU1) -IHT -HTU1 [|*: /3 width=3 by drops_skip, ext2_pair/ ] -HVW1 #U2 #HTU2 #HU12 - /3 width=5 by cpce_bind, lifts_bind, ex2_intro/ -| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #b #f #L #HLK #X #HX - elim (lifts_inv_flat2 … HX) -HX #W1 #U1 #HVW1 #HTU1 #H destruct - elim (IHV … HLK … HVW1) -IHV -HVW1 #W2 #HVW2 #HW12 - elim (IHT … HLK … HTU1) -IHT -HTU1 -HLK #U2 #HTU2 #HU12 - /3 width=5 by cpce_flat, lifts_flat, ex2_intro/ -] -qed-. -*) -lemma cpce_inv_lifts_bi (h) (G): - d_deliftable2_bi … lifts (cpce h G). -/3 width=12 by cpce_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma deleted file mode 100644 index 5596e40a5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_ext.ma +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "static_2/syntax/cext2.ma". -include "basic_2/rt_conversion/cpce.ma". - -(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR BINDERS ********************) - -definition cpce_ext (h) (G): relation3 lenv bind bind ≝ cext2 (cpce h G). - -interpretation - "context-sensitive parallel eta-conversion (binder)" - 'PConvEta h G L I1 I2 = (cpce_ext h G L I1 I2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma deleted file mode 100644 index 8da6c1af4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce.ma +++ /dev/null @@ -1,86 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "static_2/relocation/lex.ma". -include "basic_2/notation/relations/pconveta_4.ma". -include "basic_2/rt_conversion/cpce_ext.ma". - -(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************) - -definition lpce (h) (G): relation lenv ≝ lex (cpce h G). - -interpretation - "parallel eta-conversion on all entries (local environment)" - 'PConvEta h G L1 L2 = (lpce h G L1 L2). - -(* Basic properties *********************************************************) - -lemma lpce_bind (h) (G): - ∀K1,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 → - ∀I1,I2. ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 → ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] K2.ⓘ{I2}. -/2 width=1 by lex_bind/ qed. - -(* Advanced properties ******************************************************) - -lemma lpce_pair (h) (G): - ∀K1,K2,V1,V2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 → ⦃G,K1⦄ ⊢ V1 ⬌η[h] V2 → - ∀I. ⦃G,K1.ⓑ{I}V1⦄ ⊢ ⬌η[h] K2.ⓑ{I}V2. -/2 width=1 by lex_pair/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma lpce_inv_atom_sn (h) (G): - ∀L2. ⦃G,⋆⦄ ⊢ ⬌η[h] L2 → L2 = ⋆. -/2 width=2 by lex_inv_atom_sn/ qed-. - -lemma lpce_inv_bind_sn (h) (G): - ∀I1,L2,K1. ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] L2 → - ∃∃I2,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L2 = K2.ⓘ{I2}. -/2 width=1 by lex_inv_bind_sn/ qed-. - -lemma lpce_inv_atom_dx (h) (G): - ∀L1. ⦃G,L1⦄ ⊢ ⬌η[h] ⋆ → L1 = ⋆. -/2 width=2 by lex_inv_atom_dx/ qed-. - -lemma lpce_inv_bind_dx (h) (G): - ∀I2,L1,K2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓘ{I2} → - ∃∃I1,K1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L1 = K1.ⓘ{I1}. -/2 width=1 by lex_inv_bind_dx/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma lpce_inv_unit_sn (h) (G): - ∀I,L2,K1. ⦃G,K1.ⓤ{I}⦄ ⊢ ⬌η[h] L2 → - ∃∃K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & L2 = K2.ⓤ{I}. -/2 width=1 by lex_inv_unit_sn/ qed-. - -lemma lpce_inv_pair_sn (h) (G): - ∀I,L2,K1,V1. ⦃G,K1.ⓑ{I}V1⦄ ⊢ ⬌η[h] L2 → - ∃∃K2,V2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ V1 ⬌η[h] V2 & L2 = K2.ⓑ{I}V2. -/2 width=1 by lex_inv_pair_sn/ qed-. - -lemma lpce_inv_unit_dx (h) (G): - ∀I,L1,K2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓤ{I} → - ∃∃K1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & L1 = K1.ⓤ{I}. -/2 width=1 by lex_inv_unit_dx/ qed-. - -lemma lpce_inv_pair_dx (h) (G): - ∀I,L1,K2,V2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ V1 ⬌η[h] V2 & L1 = K1.ⓑ{I}V1. -/2 width=1 by lex_inv_pair_dx/ qed-. - -lemma lpce_inv_pair (h) (G): - ∀I1,I2,L1,L2,V1,V2. ⦃G,L1.ⓑ{I1}V1⦄ ⊢ ⬌η[h] L2.ⓑ{I2}V2 → - ∧∧ ⦃G,L1⦄ ⊢ ⬌η[h] L2 & ⦃G,L1⦄ ⊢ V1 ⬌η[h] V2 & I1 = I2. -/2 width=1 by lex_inv_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma deleted file mode 100644 index 2d683d06f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "static_2/relocation/drops_lex.ma". -include "basic_2/rt_conversion/lpce.ma". - -(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************) - -(* Inversion lemmas with generic slicing for local environments *************) - -lemma lpce_drops_conf (h) (G): dropable_sn (cpce h G). -/2 width=3 by lex_dropable_sn/ qed-. - -lemma lpce_drops_trans (h) (G): dropable_dx (cpce h G). -/2 width=3 by lex_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 3422c89b3..6bf92c3c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -25,7 +25,7 @@ table { ] [ { "context-sensitive native validity" * } { [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ] - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_lpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] } ] } @@ -44,12 +44,14 @@ table { ] class "blue" [ { "rt-conversion" * } { +(* [ { "context-sensitive parallel eta-conversion" * } { [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" "lpce_drops" * ] [ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ] [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" "cpce_drops" * ] } ] +*) [ { "context-sensitive parallel r-conversion" * } { [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] }