From 93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 27 Jul 2018 20:50:11 +0200 Subject: [PATCH] update in basic_2 + refinement for native validity (lsubv) allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity) --- .../dynamic/{cnv_lpr.ma => cnv_cpm_trans.ma} | 65 +++++------ .../lambdadelta/basic_2/dynamic/cnv_etc.ma | 17 ++- .../lambdadelta/basic_2/dynamic/lsubv.ma | 103 ++++++++++++++++++ .../lambdadelta/basic_2/dynamic/lsubv_cnv.ma | 37 +++++++ .../lambdadelta/basic_2/dynamic/lsubv_cpcs.ma | 25 +++++ .../lambdadelta/basic_2/dynamic/lsubv_cpms.ma | 25 +++++ .../basic_2/dynamic/lsubv_drops.ma | 70 ++++++++++++ .../basic_2/dynamic/lsubv_lsuba.ma | 33 ++++++ .../basic_2/dynamic/lsubv_lsubr.ma | 25 +++++ .../lambdadelta/basic_2/dynamic/partial.txt | 3 +- .../lsubsv.ma => etc/lsubsv/lsubsv.etc} | 0 .../lsubsv/lsubsv_cpcs.etc} | 0 .../lsubsv/lsubsv_lstas.etc} | 0 .../lsubsv/lsubsv_lsuba.etc} | 0 .../lsubsv/lsubsv_lsubd.etc} | 0 .../lsubsv/lsubsv_scpds.etc} | 0 .../lsubsv/lsubsv_snv.etc} | 0 .../shnv/nativevalid_6.etc} | 0 .../{dynamic/shnv.ma => etc/shnv/shnv.etc} | 0 .../basic_2/notation/relations/lrsubeqv_5.ma | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 13 +-- 21 files changed, 364 insertions(+), 56 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{cnv_lpr.ma => cnv_cpm_trans.ma} (75%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv.ma => etc/lsubsv/lsubsv.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_cpcs.ma => etc/lsubsv/lsubsv_cpcs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lstas.ma => etc/lsubsv/lsubsv_lstas.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lsuba.ma => etc/lsubsv/lsubsv_lsuba.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lsubd.ma => etc/lsubsv/lsubsv_lsubd.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_scpds.ma => etc/lsubsv/lsubsv_scpds.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_snv.ma => etc/lsubsv/lsubsv_snv.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/nativevalid_6.ma => etc/shnv/nativevalid_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/shnv.ma => etc/shnv/shnv.etc} (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma similarity index 75% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma index 4a87a4c3d..2d9f53b9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -16,13 +16,9 @@ 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". -*) +include "basic_2/dynamic/lsubv_cnv.ma". + (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Properties with context-free parallel reduction for local environments *****) @@ -32,10 +28,10 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ → (∀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 +#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 (* -IH4 -IH3 *) -IH2 +| #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 @@ -49,9 +45,9 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ → 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 +| #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 (* -IH4 -IH3 *) -IH2 +| #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/ @@ -61,13 +57,13 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ → | #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 *) + [ #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 (IH2 … HVW1 … V2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12 + 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 + >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/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma new file mode 100644 index 000000000..bba857ac8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lrsubeqv_5.ma". +include "basic_2/dynamic/cnv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Note: this is not transitive *) +inductive lsubv (a) (h) (G): relation lenv ≝ +| lsubv_atom: lsubv a h G (⋆) (⋆) +| lsubv_bind: ∀I,L1,L2. lsubv a h G L1 L2 → lsubv a h G (L1.ⓘ{I}) (L2.ⓘ{I}) +| lsubv_beta: ∀L1,L2,W,V. ⦃G, L1⦄ ⊢ ⓝW.V ![a,h] → ⦃G, L2⦄ ⊢ W ![a,h] → + lsubv a h G L1 L2 → lsubv a h G (L1.ⓓⓝW.V) (L2.ⓛW) +. + +interpretation + "local environment refinement (native validity)" + 'LRSubEqV a h G L1 L2 = (lsubv a h G L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆. +#a #h #G #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #_ #H destruct +| #L1 #L2 #W #V #_ #_ #_ #H destruct +] +qed-. + +(* Basic_2A1: uses: lsubsv_inv_atom1 *) +lemma lsubv_inv_atom_sn (a) (h) (G): ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆. +/2 width=6 by lsubv_inv_atom_sn_aux/ qed-. + +fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → + ∀I,K1. L1 = K1.ⓘ{I} → + ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I} + | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] & + G ⊢ K1 ⫃![a,h] K2 & + I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. +#a #h #G #L1 #L2 * -L1 -L2 +[ #J #K1 #H destruct +| #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/ +| #L1 #L2 #W #V #HWV #HW #HL12 #J #K1 #H destruct /3 width=8 by ex5_3_intro, or_intror/ +] +qed-. + +(* Basic_2A1: uses: lsubsv_inv_pair1 *) +lemma lsubv_inv_bind_sn (a) (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 → + ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I} + | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] & + G ⊢ K1 ⫃![a,h] K2 & + I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW. +/2 width=3 by lsubv_inv_bind_sn_aux/ qed-. + +fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = ⋆ → L1 = ⋆. +#a #h #G #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #_ #H destruct +| #L1 #L2 #W #V #_ #_ #_ #H destruct +] +qed-. + +(* Basic_2A1: uses: lsubsv_inv_atom2 *) +lemma lsubv_inv_atom2 (a) (h) (G): ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆. +/2 width=6 by lsubv_inv_atom_dx_aux/ qed-. + +fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → + ∀I,K2. L2 = K2.ⓘ{I} → + ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I} + | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] & + G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V. +#a #h #G #L1 #L2 * -L1 -L2 +[ #J #K2 #H destruct +| #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/ +| #L1 #L2 #W #V #HWV #HW #HL12 #J #K2 #H destruct /3 width=8 by ex5_3_intro, or_intror/ +] +qed-. + +(* Basic_2A1: uses: lsubsv_inv_pair2 *) +lemma lsubv_inv_bind_dx (a) (h) (G): ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} → + ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I} + | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] & + G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V. +/2 width=3 by lsubv_inv_bind_dx_aux/ qed-. + +(* Basic properties *********************************************************) + +(* Basic_2A1: uses: lsubsv_refl *) +lemma lsubv_refl (a) (h) (G): reflexive … (lsubv a h G). +#a #h #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma new file mode 100644 index 000000000..b1782a021 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/lsubv_cpms.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Forward lemmas with native validity **************************************) + +(* Basic_2A1: uses: lsubsv_snv_trans *) +lemma lsubv_cnv_trans (a) (h) (G): + ∀L2,T. ⦃G, L2⦄ ⊢ T ![a,h] → + ∀L1. G ⊢ L1 ⫃![a,h] L2 → ⦃G, L1⦄ ⊢ T ![a,h]. +#a #h #G #L2 #T #H elim H -G -L2 -T // +[ #I #G #K2 #V #HV #IH #L1 #H + elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_zero/ +| #I #G #K2 #i #_ #IH #L1 #H + elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_lref/ +| #p #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 + /4 width=1 by cnv_bind, lsubv_bind/ +| #n #p #G #L2 #V #W #T #U #Ha #_ #_ #HVW #HTU #IHV #IHT #L1 #HL + /4 width=10 by lsubv_cpms_trans, cnv_appl/ +| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12 + /4 width=6 by lsubv_cpms_trans, cnv_cast/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma new file mode 100644 index 000000000..c02ec80b0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpcs_lsubr.ma". +include "basic_2/dynamic/lsubv_lsubr.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Forward lemmas with context-sensitive r-equivalence for terms ************) + +(* Basic_2A1: uses: lsubsv_cprs_trans *) +lemma lsubv_cpcs_trans (a) (h) (G): lsub_trans … (cpcs h G) (lsubv a h G). +/3 width=6 by lsubv_fwd_lsubr, lsubr_cpcs_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma new file mode 100644 index 000000000..81d385add --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lsubr.ma". +include "basic_2/dynamic/lsubv_lsubr.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Forward lemmas with t-bound contex-sensitive rt-computation for terms ****) + +(* Basic_2A1: uses: lsubsv_cprs_trans lsubsv_scpds_trans *) +lemma lsubv_cpms_trans (a) (n) (h) (G): lsub_trans … (λL. cpms h G L n) (lsubv a h G). +/3 width=6 by lsubv_fwd_lsubr, lsubr_cpms_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma new file mode 100644 index 000000000..90b59cba0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "basic_2/dynamic/lsubv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Properties with generic slicing for local environments *******************) + +(* Note: the premise 𝐔⦃f⦄ cannot be removed *) +(* Basic_2A1: includes: lsubsv_drop_O1_conf *) +lemma lsubv_drops_conf_isuni (a) (h) (G): + ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → + ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b,f] L1 ≘ K1 → + ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L2 ≘ K2. +#a #h #G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H + elim (drops_inv_bind1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by lsubv_bind, drops_refl, ex2_intro/ + | #g #Hg #HLK1 #H destruct -HL12 + elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/ + ] +| #L1 #L2 #W #V #HVW #HW #HL12 #IH #b #f #K1 #Hf #H + elim (drops_inv_bind1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by drops_refl, lsubv_beta, ex2_intro/ + | #g #Hg #HLK1 #H destruct -HL12 + elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/ + ] +] +qed-. + +(* Note: the premise 𝐔⦃f⦄ cannot be removed *) +(* Basic_2A1: includes: lsubsv_drop_O1_trans *) +lemma lsubv_drops_trans_isuni (a) (h) (G): + ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → + ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2 → + ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L1 ≘ K1. +#a #h #G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H + elim (drops_inv_bind1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by lsubv_bind, drops_refl, ex2_intro/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ + ] +| #L1 #L2 #W #V #HWV #HW #HL12 #IH #b #f #K2 #Hf #H + elim (drops_inv_bind1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by drops_refl, lsubv_beta, ex2_intro/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma new file mode 100644 index 000000000..ac03aa297 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/cnv_aaa.ma". +include "basic_2/dynamic/lsubv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Forward lemmas with lenv refinement for atomic arity assignment **********) + +(* Basic_2A1: uses: lsubsv_fwd_lsuba *) +lemma lsubsv_fwd_lsuba (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → G ⊢ L1 ⫃⁝ L2. +#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/ +#L1 #L2 #W #V #H #_ #_ #IH +elim (cnv_inv_cast … H) -H #W0 #HW #HV #HW0 #HVW0 +elim (cnv_fwd_aaa … HW) -HW #B #HW +elim (cnv_fwd_aaa … HV) -HV #A #HV +lapply (cpms_aaa_conf … HW … HW0) -HW0 #H +lapply (cpms_aaa_conf … HV … HVW0) -HVW0 #HW0 +lapply (aaa_mono … H … HW0) -W0 #H destruct +/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma new file mode 100644 index 000000000..938c116c5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lsubr.ma". +include "basic_2/dynamic/lsubv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************) + +(* Forward lemmas with restricted refinement for local environments *********) + +(* Basic_2A1: uses: lsubsv_fwd_lsubr *) +lemma lsubv_fwd_lsubr (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 ⫃ L2. +#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_beta/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt index 87d2cd592..ad9b95be0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt @@ -1,2 +1,3 @@ cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma -cnv_etc.ma cnv_lpr.ma +cnv_etc.ma cnv_cpm_trans.ma +lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma index 78eeb36a2..ff9313322 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ [ break term 46 h, break term 46 o ] break term 46 L2 )" +notation "hvbox( G ⊢ break term 46 L1 ⫃![ break term 46 a, break term 46 h ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LRSubEqV $h $o $G $L1 $L2 }. + for @{ 'LRSubEqV $a $h $G $L1 $L2 }. 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 e6a1ea5d3..1c19f4e3a 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 @@ -28,16 +28,10 @@ table { [ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ] } ] - [ { "local env. ref. for stratified native validity" * } { - [ [ "" ] "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] - } - ] -*) - [ { "context-sensitive native validity" * } { -(* - [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] *) - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ] + [ { "context-sensitive native validity" * } { + [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "snv_cpm_trans" (* + "snv_scpes" + "snv_preserve" *) * ] } ] } @@ -127,6 +121,7 @@ class "capitalize italic" { 0 1 } class "italic" { 2 } (* + [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] [ { "decomposed rt-equivalence" * } { [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] } -- 2.39.2