From: Ferruccio Guidi Date: Fri, 27 Jul 2018 18:50:11 +0000 (+0200) Subject: update in basic_2 X-Git-Tag: make_still_working~293 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;p=helm.git update in basic_2 + refinement for native validity (lsubv) allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity) --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma new file mode 100644 index 000000000..2d9f53b9c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -0,0 +1,129 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpms_fpbg.ma". +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". +include "basic_2/dynamic/cnv_drops.ma". +include "basic_2/dynamic/cnv_etc.ma". +include "basic_2/dynamic/lsubv_cnv.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with context-free parallel reduction for local environments *****) + +fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ → + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1. +#a #h #o #Ha #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ] +[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1 + elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct // +| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 + elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1 + elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2 + elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL + elim (cpm_inv_lref1_drops … H2) -H2 * + [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/ + | #K0 #V0 #W0 #H #HVW0 #W0 -HV12 + lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct + lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/ + | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12 + lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct + lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/ + ] +| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 -IH1 + elim (cnv_inv_gref … H1) +| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 + elim (cnv_inv_bind … H1) -H1 #HV1 #HT1 + elim (cpm_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/ + | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 + /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/ + ] +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct + elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1 + elim (cpm_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 + lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 + elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12 + eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1 + lapply (cprs_trans … HXW21 … H1) -XW1 #H1 + lapply (cpms_trans … HXT21 … H2) -XT1 [h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1. +lemma cnv_cpms_trans_lpr_far (a) (h) (o): + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → + ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1. #a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H @(cpms_ind_dx … H) -n -T2 /4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/ qed-. + +lemma cnv_cpms_strip_lpr_far (a) (h) (o): + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → + ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1. +/3 width=8 by cpm_cpms/ qed-. + (* fact cnv_cpms_strip_lpr_aux (a) (h) (o): ∀G0,L0,T0. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma deleted file mode 100644 index 4a87a4c3d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma +++ /dev/null @@ -1,142 +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/cpms_fpbg.ma". -include "basic_2/rt_computation/cprs_cprs.ma". -include "basic_2/rt_computation/lprs_cpms.ma". -include "basic_2/dynamic/cnv_drops.ma". -(* -include "basic_2/dynamic/snv_aaa.ma". -*) -include "basic_2/dynamic/cnv_etc.ma". -(* -include "basic_2/dynamic/lsubsv_snv.ma". -*) -(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) - -(* Properties with context-free parallel reduction for local environments *****) - -fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ → - ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1. -#a #h #o #Ha #G0 #L0 #T0 (* #IH4 #IH3 *) #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct (* -IH4 -IH3 *) -IH2 -IH1 -H1 - elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct // -| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2 - elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1 - elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2 - elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL - elim (cpm_inv_lref1_drops … H2) -H2 * - [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/ - | #K0 #V0 #W0 #H #HVW0 #W0 -HV12 - lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct - lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/ - | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12 - lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct - lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/ - ] -| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2 -IH1 - elim (cnv_inv_gref … H1) -| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2 - elim (cnv_inv_bind … H1) -H1 #HV1 #HT1 - elim (cpm_inv_bind1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/ - | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 - /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct - elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1 - elim (cpm_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct (* -IH4 *) - lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 - lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 - elim (IH2 … HVW1 … V2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12 - eq_minus_O // #W0 #H1 #H2 - lapply (cprs_trans … HXW21 … H1) -XW1 #H1 - lapply (cpms_trans … HXT21 … H2) -XT1