From: Ferruccio Guidi Date: Fri, 25 Sep 2020 21:54:50 +0000 (+0200) Subject: milestone update in basic_2 X-Git-Tag: make_still_working~177 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e23331eef5817eaa6c5e1c442d1d6bbb18650573;p=helm.git milestone update in basic_2 + improved rst-transition and related theory + minor improvements --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma index fea399443..0cd18e341 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_computation/fpbg_fqus.ma". include "basic_2/rt_computation/fpbs_cpxs.ma". include "basic_2/rt_computation/fpbg_fpbs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma index 51d06a1bd..e37493a83 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma @@ -16,7 +16,7 @@ include "ground/xoa/ex_5_1.ma". include "ground/xoa/ex_8_5.ma". include "ground/xoa/ex_9_3.ma". include "basic_2/rt_transition/cpm_teqx.ma". -include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_computation/fpbg_cpm.ma". include "basic_2/dynamic/cnv_fsb.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -41,11 +41,11 @@ lemma cnv_cpr_teqx_fwd_refl (h) (a) (G) (L): /3 width=3 by eq_f2/ | #G #K #V #T1 #X1 #X2 #HXT1 #HX12 #_ #H1 #H2 elim (cnv_fpbg_refl_false … H2) -a - @(fpbg_teqx_div … H1) -H1 - /3 width=9 by cpm_tneqx_cpm_fpbg, cpm_zeta, teqx_lifts_inv_pair_sn/ + @(fpbg_teqg_div … H1) -H1 + /3 width=9 by cpm_tneqx_cpm_fpbg, cpm_zeta, teqg_lifts_inv_pair_sn/ | #G #L #U #T1 #T2 #HT12 #_ #H1 #H2 elim (cnv_fpbg_refl_false … H2) -a - @(fpbg_teqx_div … H1) -H1 + @(fpbg_teqg_div … H1) -H1 /3 width=7 by cpm_tneqx_cpm_fpbg, cpm_eps, teqg_inv_pair_xy_y/ | #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H1 #_ elim (teqx_inv_pair … H1) -H1 #H #_ #_ destruct @@ -67,7 +67,7 @@ elim (cpm_inv_bind1 … H1) -H1 * /2 width=4 by ex5_intro/ | #X1 #HXT1 #HX1 #H1 #H destruct elim (cnv_fpbg_refl_false … H0) -a - @(fpbg_teqx_div … H2) -H2 + @(fpbg_teqg_div … H2) -H2 /3 width=9 by cpm_tneqx_cpm_fpbg, cpm_zeta, teqx_lifts_inv_pair_sn/ ] qed-. @@ -105,11 +105,11 @@ elim (cpm_inv_cast1 … H1) -H1 [ * || * ] /2 width=7 by ex9_3_intro/ | #HT1X elim (cnv_fpbg_refl_false … H0) -a - @(fpbg_teqx_div … H2) -H2 + @(fpbg_teqg_div … H2) -H2 /3 width=7 by cpm_tneqx_cpm_fpbg, cpm_eps, teqg_inv_pair_xy_y/ | #m #HU1X #H destruct elim (cnv_fpbg_refl_false … H0) -a - @(fpbg_teqx_div … H2) -H2 + @(fpbg_teqg_div … H2) -H2 /3 width=7 by cpm_tneqx_cpm_fpbg, cpm_ee, teqg_inv_pair_xy_x/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma index aad1acf18..546223ed6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_conf.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground/xoa/ex_4_1_props.ma". +include "basic_2/rt_computation/fpbg_fqus.ma". include "basic_2/dynamic/cnv_cpm_teqx.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma index 691ffde90..d20e116b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma @@ -47,9 +47,9 @@ fact cnv_cpms_conf_lpr_refl_tneqx_sub (h) (a) (G0) (L0) (T0) (m21) (m22): lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) // ❪G0, L0, X2❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) -lapply (fpbg_fpbs_trans ? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg +cut (❪G0, L0, T0❫ > ❪G0, L0, X2❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fwd_fpbc, fpbc_fpbs_fpbg/ ] #H1fpbg (**) (* cut *) +lapply (fpbg_fpbs_trans … H1fpbg G0 L0 Z0 ?) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ20 … L0 ?) // #HZ0 -elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 +elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 elim (teqx_dec X1 Z0) #H2XZ [ -IH - elim (cnv_cpms_conf_lpr_teqx_teqx_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] + elim (cnv_cpms_conf_lpr_teqx_teqx_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0) + [2,3: // |4,5: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ] | -H1XT1 -H2XT1 - elim (cpms_tneqx_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] + elim (cpms_tneqx_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ] -HXZ10 -H2XZ #n1 #n2 #X0 #H1X10 #H2X10 #HXZ0 #Hn - elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] + elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ] >Hn -n1 -n2 -X0 -IH ] #Z1 #HTZ1 #HZ01 @@ -135,11 +136,11 @@ fact cnv_cpms_conf_lpr_tneqx_tneqx_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20 -cut (❪G0, L0, T0❫ > ❪G0, L0, X1❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) -lapply (fpbg_fpbs_trans ? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg +cut (❪G0, L0, T0❫ > ❪G0, L0, X1❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fwd_fpbc, fpbc_fpbs_fpbg/ ] #H1fpbg (**) (* cut *) +lapply (fpbg_fpbs_trans … H1fpbg G0 L0 Z0 ?) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0 -elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01 -elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=3 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 +elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01 +elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02 lapply (cpms_trans … HTZ1 … HZ01) -Z1 arith_l3 /3 width=7 by cpms_step_sn, teqx_trans, ex4_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma index 6239b4798..76ff1a2a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/rt_transition/lpr.ma". include "basic_2/rt_computation/cpms_fpbg.ma". include "basic_2/dynamic/cnv.ma". @@ -20,32 +21,32 @@ include "basic_2/dynamic/cnv.ma". (* Inductive premises for the preservation results **************************) definition IH_cnv_cpm_trans_lpr (h) (a): relation3 genv lenv term ≝ - λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → - ∀n,T2. ❪G,L1❫ ⊢ T1 ➡[h,n] T2 → - ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. + λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → + ∀n,T2. ❪G,L1❫ ⊢ T1 ➡[h,n] T2 → + ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. definition IH_cnv_cpms_trans_lpr (h) (a): relation3 genv lenv term ≝ - λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → - ∀n,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 → - ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. + λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → + ∀n,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 → + ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. definition IH_cnv_cpm_conf_lpr (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → - ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → - ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. + λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → + ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → + ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → + ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. definition IH_cnv_cpms_strip_lpr (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → - ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → - ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. + λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → + ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → + ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → + ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. definition IH_cnv_cpms_conf_lpr (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡*[h,n2] T2 → - ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → - ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. + λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → + ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡*[h,n2] T2 → + ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → + ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. (* Auxiliary properties for preservation ************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpbc_reqg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpbc_reqg.etc new file mode 100644 index 000000000..551d85545 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpbc_reqg.etc @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reqg_fqus.ma". +include "basic_2/rt_transition/cpx_reqg.ma". +include "basic_2/rt_transition/lpx_reqg.ma". +include "basic_2/rt_transition/fpbc.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Properties with generic equivalence for local environments ***************) + +(* Basic_2A1: was: teqg_fpb_trans *) +lemma teqg_fpbc_trans (S): + reflexive … S → symmetric … S → + ∀U2,U1. U2 ≛[S] U1 → + ∀G1,G2,L1,L2,T1. ❪G1,L1,U1❫ ≻ ❪G2,L2,T1❫ → + ∃∃L,T2. ❪G1,L1,U2❫ ≻ ❪G2,L,T2❫ & T2 ≛[S] T1 & L ≛[S,T1] L2. +#S #H1S #H2S #U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 #H +elim (fpbc_inv_gen S … H) -H #H12 #Hn12 + +(* Basic_2A1: was just: lleq_fpb_trans *) +lemma reqg_fpb_trans (S): + reflexive … S → symmetric … S → + ∀F,K1,K2,T. K1 ≛[S,T] K2 → + ∀G,L2,U. ❪F,K2,T❫ ≻ ❪G,L2,U❫ → + ∃∃L1,U0. ❪F,K1,T❫ ≻ ❪G,L1,U0❫ & U0 ≛[S] U & L1 ≛[S,U] L2. +#S #H1S #H2S #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U +[ #G #L2 #U #H2 elim (reqg_fqu_trans … H2 … HT) -K2 + /3 width=5 by fpb_fqu, ex3_2_intro/ +| #U #HTU #HnTU lapply (reqg_cpx_trans … HT … HTU) -HTU // + /4 width=8 by fpb_cpx, cpx_reqg_conf_sn, teqg_refl, ex3_2_intro/ +| #L2 #HKL2 #HnKL2 elim (reqg_lpx_trans … HKL2 … HT) -HKL2 // + /6 width=9 by fpb_lpx, reqg_reqx, reqg_repl, teqg_refl, ex3_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_etc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_etc.etc new file mode 100644 index 000000000..10891d697 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_etc.etc @@ -0,0 +1,13 @@ +lemma fpbg_fqu_trans: + ∀G1,G,G2,L1,L,L2,T1,T,T2. + ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G,L,T❫ ⬂ ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 +/4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/ +qed-. + +lemma fpbq_fpbg_trans: + ∀G1,G,G2,L1,L,L2,T1,T,T2. + ❪G1,L1,T1❫ ≻ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc new file mode 100644 index 000000000..f5d330427 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/teqx/fpbq_feqx.etc @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/feqx.ma". +include "basic_2/rt_transition/rpx_reqx.ma". +include "basic_2/rt_transition/fpbq.ma". + +(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) + +(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *) +lemma fpbq_feqx (G1) (G2): + ∀L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H +elim (feqx_inv_gen_sn … H) #H #HL12 #HT12 destruct +/3 width=3 by fpbq_rcpx, reqx_rpx_trans, teqx_cpx_trans/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma index 1dc14f5db..d63c89909 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_transition/cpm_fpbc.ma". +include "basic_2/rt_computation/fpbg_fqus.ma". include "basic_2/rt_computation/fpbg_cpxs.ma". include "basic_2/rt_computation/cpms_fpbs.ma". @@ -44,5 +45,5 @@ lemma cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg (h) (G) (L) (T1): ∀n1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) → ∀n2,T2. ❪G,L❫⊢ T ➡*[h,n2] T2 → T1 ≅ T2 → ❪G,L,T1❫ > ❪G,L,T1❫. #h #G #L #T1 #n1 #T #H1T1 #H2T1 #n2 #T2 #H1T2 #H2T12 -/4 width=7 by cpms_fwd_fpbs, cpm_fpb, fpbs_teqx_trans, teqx_sym, ex2_3_intro/ +/4 width=10 by fpbc_fpbs_fpbg, cpms_fwd_fpbs, fpbs_teqg_trans, cpm_fwd_fpbc, teqx_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqg.ma index 3c8f4902a..f82f0bfdd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqg.ma @@ -19,7 +19,7 @@ include "basic_2/rt_computation/cpxs_reqg.ma". (* Properties with generic equivalence for closures *************************) -(* to be updated *) +(* to update *) lemma feqg_cpxs_trans (S): reflexive … S → symmetric … S → ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma index d4b4d6520..a0e20355f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -59,11 +59,11 @@ qed-. (* Note: a proof based on fqu_cpx_trans_tneqx might exist *) (* Basic_2A1: uses: fqu_cpxs_trans_neq *) -lemma fqu_cpxs_trans_tneqx (b): +lemma fqu_cpxs_trans_tneqg (S) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → - ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≅ U2 → ⊥) → - ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≅ U1 → ⊥ & ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,U2❫. -#b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 + ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≛[S] U2 → ⊥) → + ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,U2❫. +#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❨1❩) #U2 #HVU2 @(ex3_intro … U2) [1,3: /3 width=7 by cpxs_delta, fqu_drop/ @@ -72,59 +72,59 @@ lemma fqu_cpxs_trans_tneqx (b): ] | #I #G #L #V1 #T #V2 #HV12 #H0 @(ex3_intro … (②[I]V2.T)) [1,3: /2 width=4 by fqu_pair_sn, cpxs_pair_sn/ - | #H elim (teqx_inv_pair … H) -H /2 width=1 by/ + | #H elim (teqg_inv_pair … H) -H /2 width=1 by/ ] | #p #I #G #L #V #T1 #Hb #T2 #HT12 #H0 @(ex3_intro … (ⓑ[p,I]V.T2)) [1,3: /2 width=4 by fqu_bind_dx, cpxs_bind/ - | #H elim (teqx_inv_pair … H) -H /2 width=1 by/ + | #H elim (teqg_inv_pair … H) -H /2 width=1 by/ ] | #p #I #G #L #V #T1 #Hb #T2 #HT12 #H0 @(ex3_intro … (ⓑ[p,I]V.T2)) [1,3: /4 width=4 by lsubr_cpxs_trans, cpxs_bind, lsubr_unit, fqu_clear/ - | #H elim (teqx_inv_pair … H) -H /2 width=1 by/ + | #H elim (teqg_inv_pair … H) -H /2 width=1 by/ ] | #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓕ[I]V.T2)) [1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/ - | #H elim (teqx_inv_pair … H) -H /2 width=1 by/ + | #H elim (teqg_inv_pair … H) -H /2 width=1 by/ ] | #I #G #L #T1 #U1 #HTU1 #T2 #HT12 #H0 elim (cpxs_lifts_sn … HT12 (Ⓣ) … (L.ⓘ[I]) … HTU1) -HT12 - /4 width=6 by fqu_drop, drops_refl, drops_drop, teqx_inv_lifts_bi, ex3_intro/ + /4 width=6 by fqu_drop, drops_refl, drops_drop, teqg_inv_lifts_bi, ex3_intro/ ] qed-. (* Basic_2A1: uses: fquq_cpxs_trans_neq *) -lemma fquq_cpxs_trans_tneqx (b): +lemma fquq_cpxs_trans_tneqg (S) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ → - ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≅ U2 → ⊥) → - ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≅ U1 → ⊥ & ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,U2❫. -#b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 -[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqx … H12 … HTU2 H) -T2 + ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≛[S] U2 → ⊥) → + ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,U2❫. +#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 +[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqg … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] qed-. (* Basic_2A1: uses: fqup_cpxs_trans_neq *) -lemma fqup_cpxs_trans_tneqx (b): +lemma fqup_cpxs_trans_tneqg (S) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → - ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≅ U2 → ⊥) → - ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≅ U1 → ⊥ & ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,U2❫. -#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 -[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqx … H12 … HTU2 H) -T2 + ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≛[S] U2 → ⊥) → + ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,U2❫. +#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tneqg … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ | #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 - #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_tneqx … H1 … HTU1 H) -T1 + #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_tneqg … H1 … HTU1 H) -T1 /3 width=8 by fqup_strap2, ex3_intro/ ] qed-. (* Basic_2A1: uses: fqus_cpxs_trans_neq *) -lemma fqus_cpxs_trans_tneqx (b): +lemma fqus_cpxs_trans_tneqg (S) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ → - ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≅ U2 → ⊥) → - ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≅ U1 → ⊥ & ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,U2❫. -#b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 -[ #H12 elim (fqup_cpxs_trans_tneqx … H12 … HTU2 H) -T2 + ∀U2. ❪G2,L2❫ ⊢ T2 ⬈* U2 → (T2 ≛[S] U2 → ⊥) → + ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈* U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,U2❫. +#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 +[ #H12 elim (fqup_cpxs_trans_tneqg … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma index aa5e0e2fc..07782a8dc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma @@ -37,22 +37,22 @@ qed-. (* Eliminators with extended context-sensitive rt-computation for terms *****) fact csx_ind_cpxs_aux (G) (L): - ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 → - (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≅ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 → - ∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → Q T2. + ∀Q:predicate term. + (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 → + (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≅ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 → + ∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → Q T2. #G #L #Q #IH #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IH1 #T2 #HT12 @IH -IH /2 width=3 by csx_cpxs_trans/ -HT1 #V2 #HTV2 #HnTV2 elim (teqx_dec T1 T2) #H [ lapply (teqg_tneqg_trans … H … HnTV2) // -H -HnTV2 #Hn12 lapply (cpxs_trans … HT12 … HTV2) -T2 #H12 - elim (cpxs_tneqg_fwd_step_sn … H12 … Hn12) // -H12 -Hn12 + elim (cpxs_tneqg_fwd_step_sn … H12 … Hn12) /2 width=1 by sfull_dec/ -H12 -Hn12 /3 width=4 by/ | elim (cpxs_tneqg_fwd_step_sn … HT12 … H) -HT12 -H - /3 width=6 by cpxs_trans/ + /3 width=6 by cpxs_trans, sfull_dec/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma new file mode 100644 index 000000000..5c69219b2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpb_lpx.ma". +include "basic_2/rt_computation/csx_fqus.ma". +include "basic_2/rt_computation/csx_reqg.ma". +include "basic_2/rt_computation/csx_lpx.ma". + +(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********) + +(* Properties with parallel rst-transition for closures *********************) + +(* Basic_2A1: was: csx_fpb_conf *) +lemma csx_fpb_conf: + ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2. +#G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H +elim (fpb_inv_req … H) -H #L0 #L #T #H1 #HT2 #HL0 #HL02 +lapply (cpx_reqg_conf … HL0 … HT2) -HT2 // #HT2 +/5 width=8 by csx_fquq_conf, csx_cpx_trans, csx_lpx_conf, csx_reqg_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma deleted file mode 100644 index 791c5f521..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma +++ /dev/null @@ -1,30 +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/fpbq.ma". -include "basic_2/rt_computation/csx_fqus.ma". -include "basic_2/rt_computation/csx_feqg.ma". -include "basic_2/rt_computation/csx_lpx.ma". - -(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********) - -(* Properties with parallel rst-transition for closures *********************) - -(* Basic_2A1: was: csx_fpb_conf *) -lemma csx_fpbq_conf: - ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2. -#G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -/2 width=8 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_feqg_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma index c052a3a3c..5c6176697 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -12,59 +12,52 @@ (* *) (**************************************************************************) -include "ground/xoa/ex_2_3.ma". +include "ground/xoa/ex_3_6.ma". include "basic_2/notation/relations/predsubtystarproper_6.ma". -include "basic_2/rt_transition/fpb.ma". +include "basic_2/rt_transition/fpbc.ma". include "basic_2/rt_computation/fpbs.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) definition fpbg: tri_relation genv lenv term ≝ λG1,L1,T1,G2,L2,T2. - ∃∃G,L,T. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ & ❪G,L,T❫ ≥ ❪G2,L2,T2❫. + ∃∃G3,L3,T3,G4,L4,T4. ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ & ❪G3,L3,T3❫ ≻ ❪G4,L4,T4❫ & ❪G4,L4,T4❫ ≥ ❪G2,L2,T2❫. -interpretation "proper parallel rst-computation (closure)" - 'PRedSubTyStarProper G1 L1 T1 G2 L2 T2 = (fpbg G1 L1 T1 G2 L2 T2). +interpretation + "proper parallel rst-computation (closure)" + 'PRedSubTyStarProper G1 L1 T1 G2 L2 T2 = (fpbg G1 L1 T1 G2 L2 T2). + +(* Basic inversion lemmas ***************************************************) + +lemma fpbg_inv_gen (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → + ∃∃G3,L3,T3,G4,L4,T4. ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ & ❪G3,L3,T3❫ ≻ ❪G4,L4,T4❫ & ❪G4,L4,T4❫ ≥ ❪G2,L2,T2❫. +// qed-. (* Basic properties *********************************************************) -lemma fpb_fpbg: - ∀G1,G2,L1,L2,T1,T2. - ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -/2 width=5 by ex2_3_intro/ qed. +lemma fpbg_intro (G3) (G4) (L3) (L4) (T3) (T4): + ∀G1,L1,T1,G2,L2,T2. + ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ → ❪G3,L3,T3❫ ≻ ❪G4,L4,T4❫ → + ❪G4,L4,T4❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/2 width=9 by ex3_6_intro/ qed. -lemma fpbg_fpbq_trans: +(* Basic_2A1: was: fpbg_fpbq_trans *) +lemma fpbg_fpb_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * -/3 width=9 by fpbs_strap1, ex2_3_intro/ +#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 +elim (fpbg_inv_gen … H1) -H1 +/3 width=13 by fpbs_strap1, fpbg_intro/ qed-. -lemma fpbg_fqu_trans: +(* Basic_2A1: was: fpbq_fpbg_trans *) +lemma fpb_fpbg_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. - ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G,L,T❫ ⬂ ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 -/4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/ -qed-. - -(* Note: this is used in the closure proof *) -lemma fpbg_fpbs_trans: - ∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → - ∀G1,L1,T1. ❪G1,L1,T1❫ > ❪G,L,T❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/ +elim (fpbg_inv_gen … H2) -H2 +/3 width=13 by fpbs_strap2, fpbg_intro/ qed-. - -(* Basic_2A1: uses: fpbg_fleq_trans *) -lemma fpbg_feqx_trans: - ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ > ❪G,L,T❫ → - ∀G2,L2,T2. ❪G,L,T❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -/3 width=5 by fpbg_fpbq_trans, fpbq_feqx/ qed-. - -(* Properties with t-bound rt-transition for terms **************************) - -lemma cpm_tneqx_cpm_fpbg (h) (G) (L): - ∀n1,T1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) → - ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 → ❪G,L,T1❫ > ❪G,L,T2❫. -/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma new file mode 100644 index 000000000..82c1b2f63 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpm_fpb.ma". +include "basic_2/rt_transition/cpm_fpbc.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". + +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) + +(* Properties with t-bound rt-transition for terms **************************) + +lemma cpm_tneqx_cpm_fpbg (h) (G) (L): + ∀n1,T1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) → + ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 → ❪G,L,T1❫ > ❪G,L,T2❫. +/4 width=5 by fpbc_fpbs_fpbg, fpb_fpbs, cpm_fwd_fpbc, cpm_fwd_fpb/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma index 570c4490f..484500f64 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma @@ -12,8 +12,10 @@ (* *) (**************************************************************************) +include "basic_2/rt_transition/fpbc_fqup.ma". include "basic_2/rt_computation/cpxs_teqg.ma". include "basic_2/rt_computation/fpbs_cpxs.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". include "basic_2/rt_computation/fpbg_fpbs.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) @@ -26,7 +28,7 @@ lemma cpxs_tneqx_fpbg: (T1 ≅ T2 → ⊥) → ❪G,L,T1❫ > ❪G,L,T2❫. #G #L #T1 #T2 #H #H0 elim (cpxs_tneqg_fwd_step_sn … H … H0) -H -H0 -/4 width=5 by cpxs_teqx_fpbs, fpb_cpx, ex2_3_intro/ +/4 width=5 by fpbc_fpbs_fpbg, cpxs_fpbs, cpx_fpbc, sfull_dec/ qed. lemma cpxs_fpbg_trans: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma new file mode 100644 index 000000000..fca623b64 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma @@ -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 "basic_2/rt_computation/fpbs_fpbc.ma". +include "basic_2/rt_computation/fpbg_fpbs.ma". + +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) + +(* Properties with generic equivalence for closures *************************) + +(* Basic_2A1: uses: fpbg_fleq_trans *) +lemma fpbg_feqg_trans (S) (G) (L) (T): + reflexive … S → symmetric … S → + ∀G1,L1,T1. ❪G1,L1,T1❫ > ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/3 width=8 by fpbg_fpb_trans, feqg_fpb/ qed-. + +(* Basic_2A1: uses: fleq_fpbg_trans *) +lemma feqg_fpbg_trans (S) (G) (L) (T): + reflexive … S → symmetric … S → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/3 width=8 by fpb_fpbg_trans, feqg_fpb/ qed-. + +(* Properties with generic equivalence for terms ****************************) + +lemma fpbg_teqg_div (S): + reflexive … S → symmetric … S → + ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ → + ∀T2. T2 ≛[S] T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/4 width=8 by fpbg_feqg_trans, teqg_feqg, teqg_sym/ qed-. + +(* Advanced inversion lemmas of parallel rst-computation on closures ********) + +(* Basic_2A1: was: fpbs_fpbg *) +lemma fpbs_inv_fpbg: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → + ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ + | ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H +elim (fpbs_inv_fpbc_sn … H) -H +[ /2 width=1 by or_introl/ +| * #G #L #T #H1 #H2 + /3 width=9 by fpbg_intro, or_intror/ +] +qed-. + +(* Basic_2A1: this was the definition of fpbg *) +lemma fpbg_inv_fpbc_fpbs (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → + ∃∃G,L,T. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ & ❪G,L,T❫ ≥ ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H +elim (fpbg_inv_gen … H) -H #G3 #L3 #T3 #G4 #L4 #T4 #H13 #H34 #H42 +elim (fpbs_inv_fpbc_sn … H13) -H13 +[ /3 width=9 by feqg_fpbc_trans, ex2_3_intro/ +| * #G #L #T #H1 #H3 + /4 width=13 by fpbg_fwd_fpbs,fpbg_intro, ex2_3_intro/ +] +qed-. + +(* Advanced properties of parallel rst-computation on closures **************) + +lemma fpbs_fpb_trans: + ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≥ ❪F2,K2,T2❫ → + ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ → + ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫. +#F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H +[ #H12 #G2 #L2 #U2 #H22 + lapply (feqg_fpbc_trans … H12 … H22) -F2 -K2 -T2 + /3 width=5 by feqg_fpbs, ex2_3_intro/ +| #H12 #G2 #L2 #U2 #H22 + elim (fpbg_inv_fpbc_fpbs … H12) -H12 #F #K #T #H1 #H2 + /4 width=9 by fpbs_strap1, fpbc_fwd_fpb, ex2_3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma index ebc9164a7..a1ac69182 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma @@ -12,98 +12,35 @@ (* *) (**************************************************************************) -include "static_2/static/feqg_fqup.ma". -include "static_2/static/feqg_feqg.ma". -include "basic_2/rt_transition/fpbq_fpb.ma". -include "basic_2/rt_computation/fpbs_fqup.ma". +include "basic_2/rt_computation/fpbs_fpbs.ma". include "basic_2/rt_computation/fpbg.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) (* Advanced forward lemmas **************************************************) -lemma fpbg_fwd_fpbs: - ∀G1,G2,L1,L2,T1,T2. +lemma fpbg_fwd_fpbs (G1) (G2) (L1) (L2) (T1) (T2): ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 * -/3 width=5 by fpbs_strap2, fpb_fpbq/ +#G1 #G2 #L1 #L2 #T1 #T2 #H +elim (fpbg_inv_gen … H) -H +/4 width=9 by fpbs_trans, fpbs_strap2, fpbc_fwd_fpb/ qed-. -(* Advanced properties with sort-irrelevant equivalence on closures *********) +(* Advanced properties ******************************************************) -(* Basic_2A1: uses: fleq_fpbg_trans *) -lemma feqx_fpbg_trans: - ∀G,G2,L,L2,T,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → - ∀G1,L1,T1. ❪G1,L1,T1❫ ≅ ❪G,L,T❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1 -elim (feqg_fpb_trans … H1 … H0) -G -L -T -/4 width=9 by fpbs_strap2, fpbq_feqx, ex2_3_intro/ -qed-. - -(* Properties with parallel proper rst-reduction on closures ****************) - -lemma fpb_fpbg_trans: - ∀G1,G,G2,L1,L,L2,T1,T,T2. - ❪G1,L1,T1❫ ≻ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ → - ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-. - -(* Properties with parallel rst-reduction on closures ***********************) - -lemma fpbq_fpbg_trans: - ∀G1,G,G2,L1,L,L2,T1,T,T2. - ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ > ❪G2,L2,T2❫ → - ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 -elim (fpbq_inv_fpb … H1) -H1 -/2 width=5 by feqx_fpbg_trans, fpb_fpbg_trans/ -qed-. - -(* Properties with parallel rst-compuutation on closures ********************) - -lemma fpbs_fpbg_trans: - ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → +lemma fpbs_fpbg_trans (G) (L) (T): + ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/ +#G #L #T #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2 +elim (fpbg_inv_gen … H2) -H2 +/3 width=13 by fpbg_intro, fpbs_trans/ qed-. -(* Advanced properties with plus-iterated structural successor for closures *) - -lemma fqup_fpbg_trans: - ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ⬂+ ❪G,L,T❫ → - ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-. - -(* Advanced inversion lemmas of parallel rst-computation on closures ********) - -(* Basic_2A1: was: fpbs_fpbg *) -lemma fpbs_inv_fpbg: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → - ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ - | ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 -[ /3 width=1 by feqg_refl, or_introl/ -| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 - elim (fpbq_inv_fpb … H2) -H2 #H2 - [ /3 width=5 by feqg_trans, or_introl/ - | elim (feqg_fpb_trans … H1 … H2) -G -L -T - /4 width=5 by ex2_3_intro, or_intror, feqx_fpbs/ - | /3 width=5 by fpbg_feqx_trans, or_intror/ - | /4 width=5 by fpbg_fpbq_trans, fpb_fpbq, or_intror/ - ] -] -qed-. - -(* Advanced properties of parallel rst-computation on closures **************) - -lemma fpbs_fpb_trans: - ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≥ ❪F2,K2,T2❫ → - ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ → - ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫. -#F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H -[ #H12 #G2 #L2 #U2 #H2 elim (feqg_fpb_trans … H12 … H2) -F2 -K2 -T2 - /3 width=5 by feqx_fpbs, ex2_3_intro/ -| * #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 - @(ex2_3_intro … H4) -H4 /3 width=5 by fpbs_strap1, fpb_fpbq/ -] +(* Note: this is used in the closure proof *) +lemma fpbg_fpbs_trans (G) (L) (T): + ∀G1,L1,T1. ❪G1,L1,T1❫ > ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +#G #L #T #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2 +elim (fpbg_inv_gen … H1) -H1 +/3 width=13 by fpbg_intro, fpbs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma index 7acceab10..37681f1fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma @@ -17,18 +17,13 @@ include "basic_2/rt_computation/fpbg.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) -(* Advanced properties with sort-irrelevant equivalence for terms ***********) +(* Advanced properties ******************************************************) -lemma fpbg_teqx_div: - ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ → - ∀T2. T2 ≅ T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -/4 width=5 by fpbg_feqx_trans, teqg_feqg, teqx_sym/ qed-. +lemma fpbc_fpbg (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/3 width=13 by fpbg_intro, fpb_fpbs/ qed. -(* Properties with plus-iterated structural successor for closures **********) - -(* Note: this is used in the closure proof *) -lemma fqup_fpbg: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H -/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/ -qed. +lemma fpbc_fpbs_fpbg (G) (L) (T): + ∀G1,L1,T1. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/2 width=9 by fpbg_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma new file mode 100644 index 000000000..1c64f5eb2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqus.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/s_computation/fqus_fqup.ma". +include "basic_2/rt_transition/fpbc_fqup.ma". +include "basic_2/rt_computation/fpbs_fqus.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_computation/fpbg_fpbs.ma". + +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) + +(* Properties with plus-iterated structural successor for closures **********) + +(* Note: this is used in the closure proof *) +lemma fqup_fpbg: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H +/3 width=5 by fpbc_fpbs_fpbg, fqus_fpbs, fqu_fpbc/ +qed. + +(* Note: this is used in the closure proof *) +lemma fqup_fpbg_trans (G) (L) (T): + ∀G1,L1,T1. ❪G1,L1,T1❫ ⬂+ ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ > ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma index 397c2c4f6..b40bf450a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) +include "basic_2/rt_transition/fpbc_lpx.ma". include "basic_2/rt_computation/fpbs_lpxs.ma". -include "basic_2/rt_computation/fpbg.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) @@ -25,5 +26,5 @@ lemma lpxs_rneqx_fpbg: (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ > ❪G,L2,T❫. #G #L1 #L2 #T #H #H0 elim (lpxs_rneqg_inv_step_sn … H … H0) -H -H0 -/4 width=7 by fpb_lpx, lpxs_feqx_fpbs, feqg_intro_sn, ex2_3_intro/ +/4 width=10 by fpbc_fpbs_fpbg, lpxs_feqg_fpbs, lpx_fpbc, feqg_intro_sn, sfull_dec/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma index 8aa6dba6d..f7437d26d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma @@ -14,39 +14,22 @@ include "ground/lib/star.ma". include "basic_2/notation/relations/predsubtystar_6.ma". -include "static_2/static/reqx.ma". -include "basic_2/rt_transition/fpbq.ma". +include "basic_2/rt_transition/fpb.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) definition fpbs: tri_relation genv lenv term ≝ - tri_TC … fpbq. + tri_TC … fpb. interpretation "parallel rst-computation (closure)" 'PRedSubTyStar G1 L1 T1 G2 L2 T2 = (fpbs G1 L1 T1 G2 L2 T2). -(* Basic eliminators ********************************************************) - -lemma fpbs_ind: - ∀G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 → - (∀G,G2,L,L2,T,T2. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → Q G L T → Q G2 L2 T2) → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2. -/3 width=8 by tri_TC_star_ind/ qed-. - -lemma fpbs_ind_dx: - ∀G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 → - (∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → Q G L T → Q G1 L1 T1) → - ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G1 L1 T1. -/3 width=8 by tri_TC_star_ind_dx/ qed-. (* Basic properties *********************************************************) -lemma fpbs_refl: - tri_reflexive … fpbs. -/2 width=1 by tri_inj/ qed. - -lemma fpbq_fpbs: +(* Basic_2A1: uses: fpbq_fpbs *) +lemma fpb_fpbs: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. /2 width=1 by tri_inj/ qed. @@ -61,28 +44,6 @@ lemma fpbs_strap2: ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. /2 width=5 by tri_TC_strap/ qed-. -(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *) -lemma feqx_fpbs: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=1 by fpbq_fpbs, fpbq_feqx/ qed. - -(* Basic_2A1: uses: fpbs_lleq_trans *) -lemma fpbs_feqx_trans: - ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → - ∀G2,L2,T2. ❪G,L,T❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=9 by fpbs_strap1, fpbq_feqx/ qed-. - -(* Basic_2A1: uses: lleq_fpbs_trans *) -lemma feqx_fpbs_trans: - ∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → - ∀G1,L1,T1. ❪G1,L1,T1❫ ≅ ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=5 by fpbs_strap2, fpbq_feqx/ qed-. - -lemma teqx_reqx_lpx_fpbs: - ∀T1,T2. T1 ≅ T2 → ∀L1,L0. L1 ≅[T2] L0 → - ∀G,L2. ❪G,L0❫ ⊢ ⬈ L2 → ❪G,L1,T1❫ ≥ ❪G,L2,T2❫. -/4 width=5 by feqx_fpbs, fpbs_strap1, fpbq_lpx, feqg_intro_dx/ qed. - (* Basic_2A1: removed theorems 3: fpb_fpbsa_trans fpbs_fpbsa fpbsa_inv_fpbs *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma index 94a822999..ba67c5425 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/fpbq_aaa.ma". -include "basic_2/rt_computation/fpbs.ma". +include "basic_2/rt_transition/fpb_aaa.ma". +include "basic_2/rt_computation/fpbs_fqup.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) @@ -22,7 +22,9 @@ include "basic_2/rt_computation/fpbs.ma". lemma fpbs_aaa_conf: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2. -#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=2 by ex_intro/ -#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A -/2 width=8 by fpbq_aaa_conf/ +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +[ /2 width=2 by ex_intro/ +| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A + /2 width=8 by fpb_aaa_conf/ +] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma index a0d045611..4225caf0e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/cpx_feqg.ma". include "basic_2/rt_computation/lpxs_cpxs.ma". include "basic_2/rt_computation/fpbs_lpxs.ma". @@ -21,21 +20,25 @@ include "basic_2/rt_computation/fpbs_lpxs.ma". (* Properties with extended context-sensitive parallel rt-transition ********) (* Basic_2A1: uses: fpbs_cpx_trans_neq *) -lemma fpbs_cpx_tneqx_trans: +lemma fpbs_cpx_tneqg_trans (S): + reflexive … S → symmetric … S → Transitive … S → + (∀s1,s2. Decidable (S s1 s2)) → ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → - ∀U2. ❪G2,L2❫ ⊢ T2 ⬈ U2 → (T2 ≅ U2 → ⊥) → - ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈ U1 & T1 ≅ U1 → ⊥ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫. -#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 -elim (fpbs_inv_star … H) -H #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32 -elim (feqg_cpx_trans … H32 … HTU2) -HTU2 // #T4 #HT34 #H42 -lapply (feqg_tneqg_repl_dx … H32 … H42 … HnTU2) -T2 // #HnT34 -lapply (lpxs_cpx_trans … HT34 … HL03) -HT34 #HT34 -elim (fqus_cpxs_trans_tneqx … H10 … HT34 HnT34) -T3 #T2 #HT02 #HnT02 #H24 -elim (teqx_dec T1 T0) [ #H10 | -HnT02 #HnT10 ] + ∀U2. ❪G2,L2❫ ⊢ T2 ⬈ U2 → (T2 ≛[S] U2 → ⊥) → + ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈ U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫. +#S #H1S #H2S #H3S #H4S #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 +elim (fpbs_inv_star S … H) -H // #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32 +lapply (feqg_cpx_trans_cpx … H32 … HTU2) // #HTU32 +lapply (feqg_tneqg_trans … H32 … HnTU2) -HnTU2 // #HnTU34 +lapply (feqg_cpx_trans_feqg … H32 … HTU2) // -T2 #H32 +lapply (lpxs_cpx_trans … HTU32 … HL03) -HTU32 #HTU32 +elim (fqus_cpxs_trans_tneqg … H10 … HTU32 HnTU34) -T3 #T2 #HT02 #HnT02 #H2 +elim (teqg_dec S … T1 T0) [ #H10 | -HnT02 #HnT10 | // ] [ lapply (cpxs_trans … HT10 … HT02) -HT10 -HT02 #HT12 elim (cpxs_tneqg_fwd_step_sn … HT12) - [2,7: /3 width=3 by teqg_canc_sn/ ] -T0 -HT12 // -| elim (cpxs_tneqg_fwd_step_sn … HT10 … HnT10) -HT10 -HnT10 // + [2,7: /3 width=3 by teqg_canc_sn/ ] -T0 -HT12 /2 width=1 by sfull_dec/ + /3 width=15 by fpbs_intro_star, ex3_intro/ +| elim (cpxs_tneqg_fwd_step_sn … HT10 … HnT10) -HT10 -HnT10 /2 width=1 by sfull_dec/ + /4 width=15 by fpbs_intro_star, cpxs_trans, ex3_intro/ ] -/4 width=16 by fpbs_intro_star, cpxs_teqx_fpbs_trans, ex3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma index f9d110dd1..4461f2f18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/rt_computation/cpxs.ma". -include "basic_2/rt_computation/fpbs_fqup.ma". +include "basic_2/rt_computation/fpbs_feqg.ma". +include "basic_2/rt_computation/fpbs_fqus.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) @@ -22,39 +23,34 @@ include "basic_2/rt_computation/fpbs_fqup.ma". lemma cpxs_fpbs: ∀G,L,T1,T2. ❪G,L❫ ⊢ T1 ⬈* T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫. #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 -/3 width=5 by fpbq_cpx, fpbs_strap1/ +/3 width=5 by cpx_fpb, fpbs_strap1/ qed. lemma fpbs_cpxs_trans: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ∀T2. ❪G,L❫ ⊢ T ⬈* T2 → ❪G1,L1,T1❫ ≥ ❪G,L,T2❫. #G1 #G #L1 #L #T1 #T #H1 #T2 #H @(cpxs_ind … H) -T2 -/3 width=5 by fpbs_strap1, fpbq_cpx/ +/3 width=5 by fpbs_strap1, cpx_fpb/ qed-. lemma cpxs_fpbs_trans: ∀G1,G2,L1,L2,T,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ → ∀T1. ❪G1,L1❫ ⊢ T1 ⬈* T → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G1 #G2 #L1 #L2 #T #T2 #H1 #T1 #H @(cpxs_ind_dx … H) -T1 -/3 width=5 by fpbs_strap2, fpbq_cpx/ +/3 width=5 by fpbs_strap2, cpx_fpb/ qed-. -lemma cpxs_teqx_fpbs_trans: - ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → ∀T0. T ≅ T0 → +lemma cpxs_teqg_fpbs_trans (S): + reflexive … S → symmetric … S → + ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → ∀T0. T ≛[S] T0 → ∀G2,L2,T2. ❪G1,L1,T0❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=3 by cpxs_fpbs_trans, teqx_fpbs_trans/ qed-. +/3 width=6 by cpxs_fpbs_trans, teqg_fpbs_trans/ qed-. -lemma cpxs_teqx_fpbs: +lemma cpxs_teqg_fpbs (S): + reflexive … S → symmetric … S → ∀G,L,T1,T. ❪G,L❫ ⊢ T1 ⬈* T → - ∀T2. T ≅ T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫. -/4 width=3 by cpxs_fpbs_trans, feqx_fpbs, teqg_feqg/ qed. - -(* Properties with star-iterated structural successor for closures **********) - -lemma cpxs_fqus_fpbs: - ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → - ∀G2,L2,T2. ❪G1,L1,T❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed. + ∀T2. T ≛[S] T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫. +/4 width=5 by cpxs_fpbs_trans, feqg_fpbs, teqg_feqg/ qed. (* Properties with plus-iterated structural successor for closures **********) @@ -62,3 +58,10 @@ lemma cpxs_fqup_fpbs: ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → ∀G2,L2,T2. ❪G1,L1,T❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. /3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed. + +(* Properties with star-iterated structural successor for closures **********) + +lemma cpxs_fqus_fpbs: + ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → + ∀G2,L2,T2. ❪G1,L1,T❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma index c68d3a661..159b57bcb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/csx_fpbq.ma". -include "basic_2/rt_computation/fpbs.ma". +include "basic_2/rt_computation/csx_fpb.ma". +include "basic_2/rt_computation/fpbs_fqup.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) @@ -24,5 +24,5 @@ lemma fpbs_csx_conf: ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 → ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2. #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 -/2 width=5 by csx_fpbq_conf/ +/2 width=5 by csx_fpb_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_feqg.ma new file mode 100644 index 000000000..6c92352e4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_feqg.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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/feqg_fqup.ma". +include "basic_2/rt_transition/fpb_feqg.ma". +include "basic_2/rt_computation/fpbs_fqup.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Propreties with generic equivalence on referred closures *****************) + +(* Basic_2A1: uses: lleq_fpbs fleq_fpbs *) +lemma feqg_fpbs (S) (G1) (G2) (L1) (L2) (T1) (T2): + reflexive … S → symmetric … S → + ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=5 by fpb_fpbs, feqg_fpb/ qed. + +(* Basic_2A1: uses: fpbs_lleq_trans *) +lemma fpbs_feqg_trans (S) (G) (L) (T): + reflexive … S → symmetric … S → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=9 by fpbs_strap1, feqg_fpb/ qed-. + +(* Basic_2A1: uses: lleq_fpbs_trans *) +lemma feqg_fpbs_trans (S) (G) (L) (T): + reflexive … S → symmetric … S → + ∀G2,L2,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=5 by fpbs_strap2, feqg_fpb/ qed-. + +lemma teqg_fpbs_trans (S) (T): + reflexive … S → symmetric … S → + ∀T1. T1 ≛[S] T → + ∀G1,G2,L1,L2,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=8 by feqg_fpbs_trans, teqg_feqg/ qed-. + +lemma fpbs_teqg_trans (S) (T): + reflexive … S → symmetric … S → + ∀G1,G2,L1,L2,T1. ❪G1,L1,T1❫ ≥ ❪G2,L2,T❫ → + ∀T2. T ≛[S] T2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=8 by fpbs_feqg_trans, teqg_feqg/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma deleted file mode 100644 index 73715fc3a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma +++ /dev/null @@ -1,25 +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/fpbq_fpb.ma". -include "basic_2/rt_computation/fpbs.ma". - -(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) - -(* Properties with proper parallel rst-reduction on closures ****************) - -lemma fpb_fpbs: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → - ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=1 by fpbq_fpbs, fpb_fpbq/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbc.ma new file mode 100644 index 000000000..e8bd0ebc4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbc.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbc_feqg.ma". +include "basic_2/rt_transition/fpbc_fpb.ma". +include "basic_2/rt_computation/fpbs_feqg.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with proper parallel rst-reduction on closures ****************) + +lemma fpbc_fpbs: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=1 by fpb_fpbs, fpbc_fwd_fpb/ qed. + +(* Inversion lemmas with proper parallel rst-reduction on closures **********) + +lemma fpbs_inv_fpbc_sn: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → + ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ + | ∃∃G,L,T. ❪G1,L1,T1❫ ≻ ❪G,L,T❫ & ❪G,L,T❫ ≥ ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +[ /3 width=1 by feqg_refl, or_introl/ +| #G #G2 #L #L2 #T #T2 #_ #H2 * [ #H1 | * #G0 #L0 #T0 #H10 #H0 ] + elim (fpb_inv_fpbc … H2) -H2 #H2 + [ /3 width=5 by feqg_trans, or_introl/ + | lapply (feqg_fpbc_trans … H1 … H2) -G -L -T // + /3 width=5 by fpb_fpbs, ex2_3_intro, or_intror/ + | /4 width=12 by fpbs_feqg_trans, ex2_3_intro, or_intror/ + | /5 width=9 by fpbs_strap1, fpbc_fwd_fpb, ex2_3_intro, or_intror/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma index e4c5ac28a..1ce4ac358 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma @@ -12,38 +12,49 @@ (* *) (**************************************************************************) -include "static_2/s_computation/fqus_fqup.ma". -include "static_2/static/feqg_fqup.ma". -include "basic_2/rt_computation/fpbs_fqus.ma". +include "basic_2/rt_transition/fpb_fqup.ma". +include "basic_2/rt_computation/fpbs.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) -(* Advanced properties ******************************************************) +(* Advanced eliminators *****************************************************) + +lemma fpbs_ind: + ∀G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 → + (∀G,G2,L,L2,T,T2. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → Q G L T → Q G2 L2 T2) → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2. +/3 width=8 by tri_TC_star_ind/ qed-. -lemma teqx_fpbs_trans: - ∀T1,T. T1 ≅ T → - ∀G1,G2,L1,L2,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=5 by feqx_fpbs_trans, teqg_feqg/ qed-. +lemma fpbs_ind_dx: + ∀G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≽ ❪G,L,T❫ → ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → Q G L T → Q G1 L1 T1) → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G1 L1 T1. +/3 width=8 by tri_TC_star_ind_dx/ qed-. + +(* Advanced properties ******************************************************) -lemma fpbs_teqx_trans: - ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≥ ❪G2,L2,T❫ → - ∀T2. T ≅ T2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=5 by fpbs_feqx_trans, teqg_feqg/ qed-. +lemma fpbs_refl: + tri_reflexive … fpbs. +/2 width=1 by tri_inj/ qed. (* Properties with plus-iterated structural successor for closures **********) lemma fqup_fpbs: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/4 width=5 by fqu_fquq, fpbq_fquq, tri_step/ +/4 width=5 by fqu_fquq, fquq_fpb, tri_step/ qed. lemma fpbs_fqup_trans: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ∀G2,L2,T2. ❪G,L,T❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=5 by fpbs_fqus_trans, fqup_fqus/ qed-. +#G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by fpbs_strap1, fqu_fpb/ +qed-. lemma fqup_fpbs_trans: ∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ∀G1,L1,T1. ❪G1,L1,T1❫ ⬂+ ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=5 by fqus_fpbs_trans, fqup_fqus/ qed-. +#G #G2 #L #L2 #T #T2 #H1 #G1 #L1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -T1 +/3 width=9 by fpbs_strap2, fqu_fpb/ +qed-. \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma index 3476c11d5..c6544a135 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "static_2/s_computation/fqus.ma". -include "basic_2/rt_computation/fpbs.ma". +include "basic_2/rt_computation/fpbs_fqup.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) @@ -23,19 +23,19 @@ lemma fqus_fpbs: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 -/3 width=5 by fpbq_fquq, tri_step/ +/3 width=5 by fquq_fpb, fpbs_strap1/ qed. lemma fpbs_fqus_trans: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥ ❪G,L,T❫ → ∀G2,L2,T2. ❪G,L,T❫ ⬂* ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 -/3 width=5 by fpbs_strap1, fpbq_fquq/ +/3 width=5 by fpbs_strap1, fquq_fpb/ qed-. lemma fqus_fpbs_trans: ∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ → ∀G1,L1,T1. ❪G1,L1,T1❫ ⬂* ❪G,L,T❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G #G2 #L #L2 #T #T2 #H1 #G1 #L1 #T1 #H @(fqus_ind_dx … H) -G1 -L1 -T1 -/3 width=5 by fpbs_strap2, fpbq_fquq/ +/3 width=5 by fpbs_strap2, fquq_fpb/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpx.ma new file mode 100644 index 000000000..e9420b5e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpx.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpb_lpx.ma". +include "basic_2/rt_computation/fpbs_feqg.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with extended rt-transition on full local environments *******) + +lemma fpbs_lpx_trans (L): + ∀G1,G2,L1,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L,T2❫ → + ∀L2. ❪G2,L❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=5 by fpbs_strap1, lpx_fpb/ qed-. + +lemma teqg_reqg_lpx_fpbs (S): + reflexive … S → symmetric … S → + ∀T1,T2. T1 ≛[S] T2 → ∀L1,L0. L1 ≛[S,T2] L0 → + ∀G,L2. ❪G,L0❫ ⊢ ⬈ L2 → ❪G,L1,T1❫ ≥ ❪G,L2,T2❫. +/4 width=7 by feqg_fpbs, fpbs_strap1, lpx_fpb, feqg_intro_dx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma index b815ae960..6f3e97a95 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma @@ -12,11 +12,10 @@ (* *) (**************************************************************************) -include "static_2/static/feqg_fqus.ma". -include "static_2/static/feqg_feqg.ma". include "basic_2/rt_computation/cpxs_fqus.ma". -include "basic_2/rt_computation/cpxs_feqg.ma". +include "basic_2/rt_computation/cpxs_reqg.ma". include "basic_2/rt_computation/lpxs_feqg.ma". +include "basic_2/rt_computation/fpbs_lpx.ma". include "basic_2/rt_computation/fpbs_cpxs.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) @@ -26,33 +25,29 @@ include "basic_2/rt_computation/fpbs_cpxs.ma". lemma lpxs_fpbs: ∀G,L1,L2,T. ❪G,L1❫ ⊢ ⬈* L2 → ❪G,L1,T❫ ≥ ❪G,L2,T❫. #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2 -/3 width=5 by fpbq_lpx, fpbs_strap1/ +/3 width=5 by lpx_fpb, fpbs_strap1/ qed. lemma fpbs_lpxs_trans: ∀G1,G2,L1,L,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L,T2❫ → ∀L2. ❪G2,L❫ ⊢ ⬈* L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G1 #G2 #L1 #L #T1 #T2 #H1 #L2 #H @(lpxs_ind_dx … H) -L2 -/3 width=5 by fpbs_strap1, fpbq_lpx/ +/3 width=5 by fpbs_strap1, lpx_fpb/ qed-. lemma lpxs_fpbs_trans: ∀G1,G2,L,L2,T1,T2. ❪G1,L,T1❫ ≥ ❪G2,L2,T2❫ → ∀L1. ❪G1,L1❫ ⊢ ⬈* L → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. #G1 #G2 #L #L2 #T1 #T2 #H1 #L1 #H @(lpxs_ind_sn … H) -L1 -/3 width=5 by fpbs_strap2, fpbq_lpx/ +/3 width=5 by fpbs_strap2, lpx_fpb/ qed-. (* Basic_2A1: uses: lpxs_lleq_fpbs *) -lemma lpxs_feqx_fpbs: - ∀G1,L1,L,T1. ❪G1,L1❫ ⊢ ⬈* L → - ∀G2,L2,T2. ❪G1,L,T1❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=3 by lpxs_fpbs_trans, feqx_fpbs/ qed. - -lemma fpbs_lpx_trans: - ∀G1,G2,L1,L,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L,T2❫ → - ∀L2. ❪G2,L❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -/3 width=3 by fpbs_lpxs_trans, lpx_lpxs/ qed-. +lemma lpxs_feqg_fpbs (S) (L): + reflexive … S → symmetric … S → + ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈* L → + ∀G2,L2,T2. ❪G1,L,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=4 by lpxs_fpbs_trans, feqg_fpbs/ qed. (* Properties with star-iterated structural successor for closures **********) @@ -69,50 +64,57 @@ lemma cpxs_fqus_lpxs_fpbs: ∀L2.❪G2,L❫ ⊢ ⬈* L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. /3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed. -lemma fpbs_cpxs_teqx_fqup_lpx_trans: +lemma fpbs_cpxs_teqg_fqup_lpx_trans (S): + reflexive … S → symmetric … S → ∀G1,G3,L1,L3,T1,T3. ❪G1,L1,T1❫ ≥ ❪G3,L3,T3❫ → - ∀T4. ❪G3,L3❫ ⊢ T3 ⬈* T4 → ∀T5. T4 ≅ T5 → + ∀T4. ❪G3,L3❫ ⊢ T3 ⬈* T4 → ∀T5. T4 ≛[S] T5 → ∀G2,L4,T2. ❪G3,L3,T5❫ ⬂+ ❪G2,L4,T2❫ → ∀L2. ❪G2,L4❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. -#G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42 +#S #H1S #H2S #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42 @(fpbs_lpx_trans … HL42) -L2 (**) (* full auto too slow *) @(fpbs_fqup_trans … H34) -G2 -L4 -T2 -/3 width=3 by fpbs_cpxs_trans, fpbs_teqx_trans/ +/3 width=6 by fpbs_cpxs_trans, fpbs_teqg_trans/ qed-. (* Advanced properties ******************************************************) (* Basic_2A1: uses: fpbs_intro_alt *) -lemma fpbs_intro_star: - ∀G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈* T → - ∀G,L,T0. ❪G1,L1,T❫ ⬂* ❪G,L,T0❫ → - ∀L0. ❪G,L❫ ⊢ ⬈* L0 → - ∀G2,L2,T2. ❪G,L0,T0❫ ≅ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ . -/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_feqx/ qed. +lemma fpbs_intro_star (S) (G) (T) (T0) (L) (L0): + reflexive … S → symmetric … S → + ∀G1,L1,T1. ❪G1,L1❫ ⊢ T1 ⬈* T → + ❪G1,L1,T❫ ⬂* ❪G,L,T0❫ → ❪G,L❫ ⊢ ⬈* L0 → + ∀G2,L2,T2. ❪G,L0,T0❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫. +/3 width=8 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, feqg_fpb/ qed. (* Advanced inversion lemmas *************************************************) (* Basic_2A1: uses: fpbs_inv_alt *) -lemma fpbs_inv_star: +lemma fpbs_inv_star (S): + reflexive … S → symmetric … S → Transitive … S → ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → - ∃∃G,L,L0,T,T0. ❪G1,L1❫ ⊢ T1 ⬈* T & ❪G1,L1,T❫ ⬂* ❪G,L,T0❫ & ❪G,L❫ ⊢ ⬈* L0 & ❪G,L0,T0❫ ≅ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 + ∃∃G,L,L0,T,T0. ❪G1,L1❫ ⊢ T1 ⬈* T & ❪G1,L1,T❫ ⬂* ❪G,L,T0❫ & ❪G,L❫ ⊢ ⬈* L0 & ❪G,L0,T0❫ ≛[S] ❪G2,L2,T2❫. +#S #H1S #H2S #H3S #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 [ /3 width=9 by feqg_refl, ex4_5_intro/ -| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0 - [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42 - elim (fquq_cpxs_trans … HT03 … H10) -T0 - /3 width=9 by fqus_strap2, ex4_5_intro/ - | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42 - /3 width=9 by cpxs_strap2, ex4_5_intro/ - | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42 - lapply (lpx_cpxs_trans … HT13 … HL10) -HT13 #HT13 - elim (lpx_fqus_trans … H34 … HL10) -L0 - /3 width=9 by lpxs_step_sn, cpxs_trans, ex4_5_intro/ - | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42 - elim (feqg_cpxs_trans … H10 … HT03) -T0 // #T0 #HT10 #H03 - elim (feqg_fqus_trans … H03 … H34) -G0 -L0 -T3 // #G0 #L0 #T3 #H03 #H34 - elim (feqg_lpxs_trans … H34 … HL34) -L3 // #L3 #HL03 #H34 - /3 width=13 by feqg_trans, ex4_5_intro/ - ] +| #G1 #G0 #L1 #L0 #T1 #T0 * + #L3 #T3 #H13 #HT30 #HL30 #_ * + #G4 #L4 #L5 #T4 #T5 #HT04 #H45 #HL45 #H52 + lapply (rpx_cpx_conf_sn … HT30 … HL30) -HL30 #HL30 + elim (fquq_cpx_trans … H13 … HT30) -T3 #T3 #HT13 #H30 + elim (rpx_fwd_lpx_reqg S … HL30) -HL30 // #L #HL3 #HL0 + lapply (reqg_cpxs_trans … HT04 … HL0) -HT04 // #HT04 + lapply (cpxs_reqg_conf_sn … HT04 … HL0) -HL0 #HL0 + lapply (lpx_cpxs_trans … HT04 … HL3) -HT04 #HT04 + elim (fquq_cpxs_trans … HT04 … H30) -T0 #T0 #HT30 #H04 + lapply (cpxs_strap2 … HT13 … HT30) -T3 #HT10 + elim (reqg_fqus_trans … H45 … HL0) -L0 // #L0 #T3 #H43 #HT35 #HL04 + lapply (feqg_intro_dx … G4 … HL04 … HT35) -HL04 -HT35 // #H35 + elim (lpx_fqus_trans … H43 … HL3) -L #L #T #HT4 #H3 #HL0 + elim (fquq_cpxs_trans … HT4 … H04) -T4 #T4 #HT04 #H4 + lapply (cpxs_trans … HT10 … HT04) -T0 #HT14 + lapply (fqus_strap2 … H4 … H3) -G0 -L3 -T #H43 + elim (feqg_lpxs_trans … H35 … HL45) -L4 // #L4 #HL04 #H35 + lapply (lpxs_step_sn … HL0 … HL04) -L0 #HL4 + lapply (feqg_trans … H35 … H52) -L5 -T5 // #H32 + /2 width=9 by ex4_5_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma index dc6cd6694..30864de70 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/predsubtystrong_3.ma". -include "basic_2/rt_transition/fpb.ma". +include "basic_2/rt_transition/fpbc.ma". (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma index b03c6a615..4da3d3d9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma @@ -14,40 +14,39 @@ include "basic_2/rt_computation/csx_aaa.ma". include "basic_2/rt_computation/fpbs_aaa.ma". -include "basic_2/rt_computation/fpbs_fpb.ma". include "basic_2/rt_computation/fsb_csx.ma". (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) (* Main properties with atomic arity assignment for terms *******************) -theorem aaa_fsb: - ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ≥𝐒 ❪G,L,T❫. +theorem aaa_fsb (G) (L) (T) (A): + ❪G,L❫ ⊢ T ⁝ A → ≥𝐒 ❪G,L,T❫. /3 width=2 by aaa_csx, csx_fsb/ qed. (* Advanced eliminators with atomic arity assignment for terms **************) -fact aaa_ind_fpb_aux (Q:relation3 …): +fact aaa_ind_fpbc_aux (Q:relation3 …): (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A → (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. -#R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T +#R #IH #G #L #T #H @(csx_ind_fpbc … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf … G2 … L2 … T2 … HTA1) -A1 -/2 width=2 by fpb_fpbs/ +/2 width=2 by fpbc_fpbs/ qed-. -lemma aaa_ind_fpb (Q:relation3 …): +lemma aaa_ind_fpbc (Q:relation3 …): (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A → (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. -/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-. +/4 width=4 by aaa_ind_fpbc_aux, aaa_csx/ qed-. fact aaa_ind_fpbg_aux (Q:relation3 …): (∀G1,L1,T1,A. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma index e8aebb213..628b3b9df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/rt_transition/fpbc_fqup.ma". +include "basic_2/rt_transition/fpbc_lpx.ma". include "basic_2/rt_computation/rsx_csx.ma". include "basic_2/rt_computation/fpbs_cpx.ma". include "basic_2/rt_computation/fpbs_csx.ma". @@ -23,7 +25,8 @@ include "basic_2/rt_computation/fsb_fpbg.ma". lemma fsb_inv_csx: ∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T. -#G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/ +#G #L #T #H @(fsb_ind_alt … H) -G -L -T +/5 width=1 by csx_intro, cpx_fpbc/ qed-. (* Propreties with context-sensitive stringly rt-normalizing terms **********) @@ -36,35 +39,37 @@ lemma csx_fsb_fpbs: #G0 #L0 #T0 #IHu #H10 lapply (fpbs_csx_conf … H10) // -HT1 #HT0 generalize in match IHu; -IHu generalize in match H10; -H10 -@(rsx_ind … (csx_rsx … HT0)) -L0 -#L0 #_ #IHd #H10 #IHu @fsb_intro -#G2 #L2 #T2 * -G2 -L2 -T2 [ -IHd -IHc | -IHu -IHd | ] -[ /4 width=5 by fpbs_fqup_trans, fqu_fqup/ -| #T2 #HT02 #HnT02 - elim (fpbs_cpx_tneqx_trans … H10 … HT02 HnT02) -T0 - /3 width=4 by/ -| #L2 #HL02 #HnL02 @(IHd … HL02 HnL02) -IHd -HnL02 [ -IHu -IHc | ] +@(rsx_ind … (csx_rsx … HT0)) -L0 #L0 #_ #IHd #H10 #IHu +@fsb_intro #G2 #L2 #T2 #H +elim (fpbc_fwd_lpx … H) -H * [ -IHd -IHc | -IHu -IHd |] +[ /5 width=5 by fsb_fpb_trans, fpbs_fqup_trans, fqu_fqup/ +| #T3 #HT03 #HnT03 #H32 + elim (fpbs_cpx_tneqg_trans … H10 … HT03 HnT03) -T0 + /4 width=5 by fsb_fpb_trans, sfull_dec/ +| #L3 #HL03 #HnL03 #HL32 + @(fsb_fpb_trans … HL32) -L2 + @(IHd … HL03 HnL03) -IHd -HnL03 [ -IHu -IHc |] [ /3 width=3 by fpbs_lpxs_trans, lpx_lpxs/ - | #G3 #L3 #T3 #H03 #_ - elim (lpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 #HT04 #H43 #HL43 - elim (teqx_dec T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ] - [ elim (teqg_fqup_trans … H43 … HT04) -T4 // #L2 #T4 #H04 #HT43 #HL24 - /4 width=7 by fsb_fpbs_trans, teqx_reqx_lpx_fpbs, fpbs_fqup_trans/ - | elim (cpxs_tneqg_fwd_step_sn … HT04 HnT04) -HT04 -HnT04 // #T2 #HT02 #HnT02 #HT24 - elim (fpbs_cpx_tneqx_trans … H10 … HT02 HnT02) -T0 #T0 #HT10 #HnT10 #H02 - /3 width=14 by fpbs_cpxs_teqx_fqup_lpx_trans/ + | #G4 #L4 #T4 #H04 #_ + elim (lpx_fqup_trans … H04 … HL03) -L3 #L3 #T3 #HT03 #H34 #HL34 + elim (teqx_dec T0 T3) [ -IHc -HT03 #HT03 | -IHu #HnT03 ] + [ elim (teqg_fqup_trans … H34 … HT03) -T3 // #L2 #T3 #H03 #HT34 #HL23 + /4 width=10 by fsb_fpbs_trans, teqg_reqg_lpx_fpbs, fpbs_fqup_trans/ + | elim (cpxs_tneqg_fwd_step_sn … HT03 HnT03) -HT03 -HnT03 /2 width=1 by sfull_dec/ #T2 #HT02 #HnT02 #HT23 + elim (fpbs_cpx_tneqg_trans … H10 … HT02 HnT02) -T0 /2 width=1 by sfull_dec/ #T0 #HT10 #HnT10 #H02 + /3 width=17 by fpbs_cpxs_teqg_fqup_lpx_trans/ ] ] ] qed. -lemma csx_fsb: - ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → ≥𝐒 ❪G,L,T❫. +lemma csx_fsb (G) (L) (T): + ❪G,L❫ ⊢ ⬈*𝐒 T → ≥𝐒 ❪G,L,T❫. /2 width=5 by csx_fsb_fpbs/ qed. (* Advanced eliminators *****************************************************) -lemma csx_ind_fpb (Q:relation3 …): +lemma csx_ind_fpbc (Q:relation3 …): (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 → (∀G2,L2,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → Q G2 L2 T2) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma index b18057900..f2a7640d1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqg.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/fpb_feqg.ma". +include "static_2/static/feqg_fqup.ma". +include "basic_2/rt_transition/fpbc_feqg.ma". include "basic_2/rt_computation/fsb.ma". (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) @@ -26,6 +27,6 @@ lemma fsb_feqg_trans (S): #S #H1S #H2S #H3S #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12 @fsb_intro #G #L #T #H2 -elim (feqg_fpb_trans … H12 … H2) -G2 -L2 -T2 -/2 width=5 by/ +elim (feqg_fpbc_trans … H12 … H2) -G2 -L2 -T2 +/4 width=5 by fpbc_intro, feqg_refl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma index cdea1a396..18902f2cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/fpbg_fpbs.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_computation/fpbg_feqg.ma". include "basic_2/rt_computation/fsb_feqg.ma". (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) @@ -26,17 +27,25 @@ lemma fsb_fpbs_trans: #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 elim (fpbs_inv_fpbg … H12) -H12 [ -IH /2 width=9 by fsb_feqg_trans/ -| -H1 * /2 width=5 by/ +| -H1 #H elim (fpbg_inv_fpbc_fpbs … H) + /2 width=5 by/ ] qed-. +(* Properties with parallel rst-transition for closures *********************) + +lemma fsb_fpb_trans: + ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫. +/3 width=5 by fsb_fpbs_trans, fpb_fpbs/ qed-. + (* Properties with proper parallel rst-computation for closures *************) lemma fsb_intro_fpbg: ∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫) → ≥𝐒 ❪G1,L1,T1❫. -/4 width=1 by fsb_intro, fpb_fpbg/ qed. +/4 width=1 by fsb_intro, fpbc_fpbg/ qed. (* Eliminators with proper parallel rst-computation for closures ************) @@ -52,7 +61,8 @@ lemma fsb_ind_fpbg_fpbs (Q:relation3 …): @IH1 -IH1 [ -IH /2 width=5 by fsb_fpbs_trans/ | -H1 #G0 #L0 #T0 #H10 - elim (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2 + lapply (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2 #H + elim (fpbg_inv_fpbc_fpbs … H) -H #G #L #T #H1 #H0 /2 width=5 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma index 9490ef8b7..7882409b5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma @@ -53,8 +53,8 @@ elim (reqx_dec L1 L0 T) #H [ lapply (reqg_rneqg_trans … H … HnLK0) -H -HnLK0 // #Hn10 lapply (lpxs_trans … HL10 … HLK0) -L0 #H10 elim (lpxs_rneqg_inv_step_sn … H10 … Hn10) -H10 -Hn10 - /3 width=8 by reqg_trans/ -| elim (lpxs_rneqg_inv_step_sn … HL10 … H) -HL10 -H // #L #K #HL1 #HnL1 #HLK #HKL0 + /3 width=8 by reqg_trans, sfull_dec/ +| elim (lpxs_rneqg_inv_step_sn … HL10 … H) -HL10 -H /2 width=1 by sfull_dec/ #L #K #HL1 #HnL1 #HLK #HKL0 elim (reqg_lpxs_trans … HLK0 … HKL0) -L0 /3 width=8 by lpxs_trans, reqg_trans/ ] @@ -84,7 +84,7 @@ fact rsx_bind_lpxs_aux (G): #Y #HY #IHY #L2 #H #HL12 destruct @rsx_intro_lpxs #L0 #HL20 lapply (lpxs_trans … HL12 … HL20) #HL10 #H -elim (rneqg_inv_bind … H) -H // [ -IHY | -HY -IHL1 -HL12 ] +elim (rneqg_inv_bind … H) -H /2 width=1 by sfull_dec/ [ -IHY | -HY -IHL1 -HL12 ] [ #HnV elim (reqx_dec L1 L2 V) [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10 /3 width=4 by rsx_lpxs_trans, lpxs_bind_refl_dx, reqg_canc_sn/ (**) (* full auto too slow *) @@ -110,7 +110,7 @@ lemma rsx_flat_lpxs (G): #L1 #HL1 #IHL1 #L2 #T #H @(rsx_ind_lpxs … H) -L2 #L2 #HL2 #IHL2 #HL12 @rsx_intro_lpxs #L0 #HL20 lapply (lpxs_trans … HL12 … HL20) -#HL10 #H elim (rneqg_inv_flat … H) -H // [ -HL1 -IHL2 | -HL2 -IHL1 ] +#HL10 #H elim (rneqg_inv_flat … H) -H /2 width=1 by sfull_dec/ [ -HL1 -IHL2 | -HL2 -IHL1 ] [ #HnV elim (reqx_dec L1 L2 V) [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10 /3 width=5 by rsx_lpxs_trans, reqg_canc_sn/ (**) (* full auto too slow: 47s *) @@ -136,7 +136,7 @@ fact rsx_bind_lpxs_void_aux (G): #Y #HY #IHY #L2 #H #HL12 destruct @rsx_intro_lpxs #L0 #HL20 lapply (lpxs_trans … HL12 … HL20) #HL10 #H -elim (rneqg_inv_bind_void … H) -H // [ -IHY | -HY -IHL1 -HL12 ] +elim (rneqg_inv_bind_void … H) -H /2 width=1 by sfull_dec/ [ -IHY | -HY -IHL1 -HL12 ] [ #HnV elim (reqx_dec L1 L2 V) [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10 /3 width=6 by rsx_lpxs_trans, lpxs_bind_refl_dx, reqg_canc_sn/ (**) (* full auto too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma index f516a4ef1..9310bcf6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_teqx.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "static_2/syntax/teqx.ma". -include "basic_2/rt_transition/cnr_teqg.ma". +include "basic_2/rt_transition/cnr_teqg.ma". (**) (* one dependence *) (* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma new file mode 100644 index 000000000..0cbf9b071 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma @@ -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 "basic_2/rt_transition/fpb_fqup.ma". +include "basic_2/rt_transition/cpm_cpx.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Forward lemmas with rst-transition for closures **************************) + +(* Basic_2A1: includes: cpr_fpbq *) +(* Basic_2A1: uses: cpm_fpbq *) +lemma cpm_fwd_fpb (h) (n) (G) (L): + ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫. +/3 width=3 by cpx_fpb, cpm_fwd_cpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpbc.ma new file mode 100644 index 000000000..5b30d4b0a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpbc.ma @@ -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 "basic_2/rt_transition/fpbc_fqup.ma". +include "basic_2/rt_transition/cpm_cpx.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Forward lemmas with proper rst-transition for closures *******************) + +(* Basic_2A1: includes: cpr_fpb *) +(* Basic_2A1: uses: cpm_fpb *) +lemma cpm_fwd_fpbc (h) (n) (G) (L): + ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → (T1 ≅ T2 → ⊥) → ❪G,L,T1❫ ≻ ❪G,L,T2❫. +/3 width=3 by cpx_fpbc, cpm_fwd_cpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index 13e3a4230..9e9dcf7b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -24,10 +24,8 @@ include "basic_2/rt_transition/cpg.ma". (* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************) -definition sort_eq_f: relation nat ≝ λs1,s2. ⊤. - definition cpx (G) (L): relation2 term term ≝ - λT1,T2. ∃c. ❪G,L❫ ⊢ T1 ⬈[sort_eq_f,rtc_eq_f,c] T2. + λT1,T2. ∃c. ❪G,L❫ ⊢ T1 ⬈[sfull,rtc_eq_f,c] T2. interpretation "extended context-sensitive parallel rt-transition (term)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqg.ma index 518ece0be..fa73e6fa3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqg.ma @@ -20,16 +20,22 @@ include "basic_2/rt_transition/rpx_reqg.ma". (* Properties with generic equivalence for closures *************************) -(**) (* to update *) -lemma feqg_cpx_trans (S): +lemma feqg_cpx_trans_cpx (S): reflexive … S → symmetric … S → ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ → - ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → - ∃∃T0. ❪G1,L1❫ ⊢ T1 ⬈ T0 & ❪G1,L1,T0❫ ≛[S] ❪G2,L2,T2❫. + ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → ❪G1,L1❫ ⊢ T1 ⬈ T2. #S #H1S #H2S #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2 elim (feqg_inv_gen_dx … H) -H // #H #HL12 #HT1 destruct -lapply (reqg_cpx_trans … HL12 … HT2) // #H +@(cpx_teqg_repl_reqg … HT2) +/2 width=7 by reqg_sym, teqg_sym, teqg_refl/ +qed-. + +lemma feqg_cpx_trans_feqg (S): + reflexive … S → symmetric … S → + ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ → + ∀T2. ❪G2,L2❫ ⊢ T ⬈ T2 → ❪G1,L1,T2❫ ≛[S] ❪G2,L2,T2❫. +#S #H1S #H2S #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2 +elim (feqg_inv_gen_dx … H) -H // #H #HL12 #_ destruct lapply (cpx_reqg_conf_dx … HT2 … HL12) -HT2 -HL12 // #HL12 -lapply (teqg_cpx_trans … HT1 … H) -T // #HT12 -/4 width=4 by feqg_intro_sn, teqg_refl, ex2_intro/ +/3 width=1 by feqg_intro_sn, teqg_refl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma index f210e63a1..9d9af6c96 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma @@ -12,30 +12,38 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predsubtyproper_6.ma". -include "static_2/s_transition/fqu.ma". -include "static_2/static/reqx.ma". -include "basic_2/rt_transition/lpr_lpx.ma". +include "basic_2/notation/relations/predsubty_6.ma". +include "static_2/s_transition/fquq.ma". +include "basic_2/rt_transition/rpx.ma". -(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) +(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) -inductive fpb (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpb_fqu: ∀G2,L2,T2. ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → fpb G1 L1 T1 G2 L2 T2 -| fpb_cpx: ∀T2. ❪G1,L1❫ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → fpb G1 L1 T1 G1 L1 T2 -| fpb_lpx: ∀L2. ❪G1,L1❫ ⊢ ⬈ L2 → (L1 ≅[T1] L2 → ⊥) → fpb G1 L1 T1 G1 L2 T1 -. +(* Basic_2A1: uses: fpbq *) +definition fpb (G1) (L1) (T1) (G2) (L2) (T2): Prop ≝ + ∃∃L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈[T] L2. interpretation - "proper parallel rst-transition (closure)" - 'PRedSubTyProper G1 L1 T1 G2 L2 T2 = (fpb G1 L1 T1 G2 L2 T2). + "parallel rst-transition (closure)" + 'PRedSubTy G1 L1 T1 G2 L2 T2 = (fpb G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -(* Basic_2A1: includes: cpr_fpb *) -lemma cpm_fpb (h) (n) (G) (L): - ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → (T1 ≅ T2 → ⊥) → ❪G,L,T1❫ ≻ ❪G,L,T2❫. -/3 width=3 by fpb_cpx, cpm_fwd_cpx/ qed. +lemma fpb_intro (G1) (L1) (T1) (G2) (L2) (T2): + ∀L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ → ❪G2,L❫ ⊢ T ⬈ T2 → + ❪G2,L❫ ⊢ ⬈[T] L2 → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +/2 width=5 by ex3_2_intro/ qed. -lemma lpr_fpb (h) (G) (T): - ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫. -/3 width=2 by fpb_lpx, lpr_fwd_lpx/ qed. +lemma rpx_fpb (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫. +/2 width=5 by fpb_intro/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma fpb_inv_gen (G1) (L1) (T1) (G2) (L2) (T2): + ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → + ∃∃L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈[T] L2. +// qed-. + +(* Basic_2A1: removed theorems 2: + fpbq_fpbqa fpbqa_inv_fpbq +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.ma new file mode 100644 index 000000000..533718941 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.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 "static_2/static/aaa_fqus.ma". +include "static_2/static/aaa_reqg.ma". +include "basic_2/rt_transition/lpx_aaa.ma". +include "basic_2/rt_transition/fpb_lpx.ma". + +(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) + +(* Properties with atomic arity assignment for terms ************************) + +(* Basic_2A1: uses: fpbq_aaa_conf *) +lemma fpb_aaa_conf: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → + ∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2. +#G1 #G2 #L1 #L2 #T1 #T2 #H #A1 #HA1 +elim (fpb_inv_req … H) -H #L0 #L #T #H1 #HT2 #HL0 #HL02 +elim (aaa_fquq_conf … H1 … HA1) -G1 -L1 -T1 -A1 #A2 #HA2 +lapply (cpx_reqg_conf … HL0 … HT2) -HT2 // #HT2 +/4 width=6 by cpx_aaa_conf_lpx, aaa_reqg_conf, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma index 27f3df4e3..22219566d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqg.ma @@ -12,38 +12,36 @@ (* *) (**************************************************************************) -include "static_2/s_transition/fqu_teqg.ma". -include "static_2/static/feqg.ma". -include "basic_2/rt_transition/fpb_reqg.ma". +include "static_2/static/feqg_fqus.ma". +include "static_2/static/feqg_feqg.ma". +include "basic_2/rt_transition/cpx_feqg.ma". +include "basic_2/rt_transition/lpx_reqg.ma". +include "basic_2/rt_transition/fpb.ma". -(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) +(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) -(* Properties with generic equivalence for closures *************************) +(* Propreties with generic equivalence on referred closures *****************) -(* Basic_2A1: uses: fleq_fpb_trans *) -lemma feqg_fpb_trans (S): - reflexive … S → symmetric … S → Transitive … S → - ∀F1,F2,K1,K2,T1,T2. ❪F1,K1,T1❫ ≛[S] ❪F2,K2,T2❫ → - ∀G2,L2,U2. ❪F2,K2,T2❫ ≻ ❪G2,L2,U2❫ → - ∃∃G1,L1,U1. ❪F1,K1,T1❫ ≻ ❪G1,L1,U1❫ & ❪G1,L1,U1❫ ≛[S] ❪G2,L2,U2❫. -#S #H1S #H2S #H3S #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 -#K2 #T2 #HK12 #HT12 #G2 #L2 #U2 #H12 -elim (teqg_fpb_trans … HT12 … H12) -T2 // #K0 #T0 #H #HT0 #HK0 -elim (reqg_fpb_trans … HK12 … H) -K2 // #L0 #U0 #H #HUT0 #HLK0 -@(ex2_3_intro … H) -H (**) (* full auto too slow *) -/4 width=5 by feqg_intro_dx, reqg_trans, teqg_reqg_conf_sn, teqg_trans/ -qed-. +(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *) +(* Basic_2A1: uses: fpbq_feqx *) +lemma feqg_fpb (S) (G1) (G2) (L1) (L2) (T1) (T2): + reflexive … S → symmetric … S → + ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +#S #G1 #G2 #L1 #L2 #T1 #T2 #HS1 #HS2 #H +elim (feqg_inv_gen_sn … H) -H #H #HL12 #HT12 destruct +/4 width=8 by reqg_rpx, teqg_cpx, fpb_intro/ +qed. -(* Inversion lemmas with generic equivalence for closures *******************) - -(* Basic_2A1: uses: fpb_inv_fleq *) -lemma fpb_inv_feqg (S): - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → - ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥. -#S #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -[ #G2 #L2 #T2 #H12 #H elim (feqg_inv_gen_sn … H) -H - /3 width=11 by reqg_fwd_length, fqu_inv_teqg/ -| #T2 #_ #HnT #H elim (feqg_inv_gen_sn … H) -H /3 width=2 by teqg_teqx/ -| #L2 #_ #HnL #H elim (feqg_inv_gen_sn … H) -H /3 width=2 by reqg_reqx/ -] +lemma feqg_fpb_trans (S) (G) (L) (T): + reflexive … S → symmetric … S → Transitive … S → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≽ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +#S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2 +elim (fpb_inv_gen … H2) -H2 #L0 #T0 #H0 #HT02 #H +elim (rpx_inv_reqg_lpx S … H) -H // #L3 #HL03 #HL32 +elim (feqg_fquq_trans … H1 … H0) -G -L -T // #G #L #T #H1 #H0 +lapply (feqg_cpx_trans_cpx … H0 … HT02) // -HT02 #HT2 +lapply (feqg_reqg_trans … H0 … HL03) -H0 -HL03 // #H +elim (feqg_inv_gen_sn … H) -H #H #HL3 #_ destruct -T0 +/3 width=10 by fpb_intro, reqg_lpx_trans_rpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fqup.ma new file mode 100644 index 000000000..71f214c34 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fqup.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rpx_fqup.ma". +include "basic_2/rt_transition/fpb.ma". + +(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was: fpbq_refl *) +lemma fpb_refl: tri_reflexive … fpb. +/2 width=5 by fpb_intro/ qed. + +(* Basic_2A1: uses: fpbq_cpx *) +lemma cpx_fpb (G) (L): + ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈ T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫. +/2 width=5 by fpb_intro/ qed. + +(* Basic_2A1: uses: fpbq_fquq *) +lemma fquq_fpb (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ⬂⸮ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +/2 width=5 by fpb_intro/ qed. + +lemma fqu_fpb (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +/3 width=5 by fquq_fpb, fqu_fquq/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma new file mode 100644 index 000000000..2aa0f0d4d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lpx.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rpx_lpx.ma". +include "basic_2/rt_transition/fpb.ma". + +(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) + +(* Properties with extended rt-transition for full local envs ***************) + +(* Basic_2A1: uses: fpbq_lpx *) +lemma lpx_fpb (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫. +/3 width=1 by rpx_fpb, lpx_rpx/ qed. + +lemma fpb_intro_req (G1) (G2) (L1) (L2) (T1) (T2): + ∀L0,L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ → ❪G2,L❫ ⊢ T ⬈ T2 → + L ≡[T] L0 → ❪G2,L0❫ ⊢ ⬈ L2 → ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +/4 width=10 by fpb_intro, lpx_rpx, reqg_rpx_trans/ qed. + +(* Inversion lemmas with extended rt-transition for full local envs *********) + +lemma fpb_inv_req (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → + ∃∃L0,L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & L ≡[T] L0 & ❪G2,L0❫ ⊢ ⬈ L2. +#G1 #G2 #L1 #L2 #T1 #T2 * #L #T #H1 #HT2 #HL2 +elim (rpx_inv_req_lpx … HL2) -HL2 #L0 #HL0 #HL02 +/2 width=7 by ex4_3_intro/ +qed-. + +(* Forward lemmas with extended rt-transition for full local envs ***********) + +lemma fpb_fwd_req (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → + ∃∃L0,L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈ L0 & L0 ≡[T] L2. +#G1 #G2 #L1 #L2 #T1 #T2 * #L #T #H1 #HT2 #HL2 +elim (rpx_fwd_lpx_req … HL2) -HL2 #L0 #HL0 #HL02 +/2 width=7 by ex4_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqg.ma deleted file mode 100644 index 6ab2c4da6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqg.ma +++ /dev/null @@ -1,54 +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/static/reqg_fqus.ma". -include "basic_2/rt_transition/cpx_reqg.ma". -include "basic_2/rt_transition/lpx_reqg.ma". -include "basic_2/rt_transition/fpb.ma". - -(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) - -(* Properties with generic equivalence for local environments ***************) - -lemma teqg_fpb_trans (S): - reflexive … S → symmetric … S → - ∀U2,U1. U2 ≛[S] U1 → - ∀G1,G2,L1,L2,T1. ❪G1,L1,U1❫ ≻ ❪G2,L2,T1❫ → - ∃∃L,T2. ❪G1,L1,U2❫ ≻ ❪G2,L,T2❫ & T2 ≛[S] T1 & L ≛[S,T1] L2. -#S #H1S #H2S #U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 * -G2 -L2 -T1 -[ #G2 #L2 #T1 #H - elim (teqg_fqu_trans … H … HU21) -H - /3 width=5 by fpb_fqu, ex3_2_intro/ -| #T1 #HUT1 #HnUT1 - lapply (teqg_cpx_trans … HU21 … HUT1) -HUT1 - /6 width=5 by fpb_cpx, reqg_refl, teqg_teqx, teqg_canc_sn, teqg_refl, ex3_2_intro/ -| /5 width=5 by fpb_lpx, teqg_reqg_conf_sn, reqg_refl, ex3_2_intro/ -] -qed-. - -(* Basic_2A1: was just: lleq_fpb_trans *) -lemma reqg_fpb_trans (S): - reflexive … S → symmetric … S → - ∀F,K1,K2,T. K1 ≛[S,T] K2 → - ∀G,L2,U. ❪F,K2,T❫ ≻ ❪G,L2,U❫ → - ∃∃L1,U0. ❪F,K1,T❫ ≻ ❪G,L1,U0❫ & U0 ≛[S] U & L1 ≛[S,U] L2. -#S #H1S #H2S #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U -[ #G #L2 #U #H2 elim (reqg_fqu_trans … H2 … HT) -K2 - /3 width=5 by fpb_fqu, ex3_2_intro/ -| #U #HTU #HnTU lapply (reqg_cpx_trans … HT … HTU) -HTU // - /4 width=8 by fpb_cpx, cpx_reqg_conf_sn, teqg_refl, ex3_2_intro/ -| #L2 #HKL2 #HnKL2 elim (reqg_lpx_trans … HKL2 … HT) -HKL2 // - /6 width=9 by fpb_lpx, reqg_reqx, reqg_repl, teqg_refl, ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma new file mode 100644 index 000000000..1944ee29b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma @@ -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/notation/relations/predsubtyproper_6.ma". +include "static_2/static/feqx.ma". +include "basic_2/rt_transition/fpb.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Basic_2A1: uses: fpb *) +definition fpbc (G1) (L1) (T1) (G2) (L2) (T2): Prop ≝ + ∧∧ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ + & (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ⊥). + +interpretation + "proper parallel rst-transition (closure)" + 'PRedSubTyProper G1 L1 T1 G2 L2 T2 = (fpbc G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +(* Basic_2A1: fpbq_inv_fpb_alt *) +lemma fpbc_intro (G1) (L1) (T1) (G2) (L2) (T2): + ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ⊥) → + ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫. +/3 width=1 by conj/ qed. + +lemma rpx_fpbc (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫. +/4 width=4 by fpbc_intro, rpx_fpb, feqg_fwd_reqg_sn/ qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: uses: fpb_fpbq_alt *) +lemma fpbc_inv_gen (S): + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → + ∧∧ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ & (❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥). +#S #G1 #G2 #L1 #L2 #T1 #T2 * +/4 width=2 by feqg_feqx, conj/ +qed-. + +(* Basic forward lemmas *****************************************************) + +(* Basic_2A1: uses: fpb_fpbq *) +lemma fpbc_fwd_fpb: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 * // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_feqg.ma new file mode 100644 index 000000000..78ada2f83 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_feqg.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpb_feqg.ma". +include "basic_2/rt_transition/fpbc.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Properties with generic equivalence for closures *************************) + +(* Basic_2A1: uses: teqg_fpb_trans lleq_fpb_trans fleq_fpb_trans *) +lemma feqg_fpbc_trans (S) (G) (L) (T): + reflexive … S → symmetric … S → Transitive … S → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≻ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫. +#S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2 +elim (fpbc_inv_gen sfull … H2) -H2 #H2 #Hn2 +/6 width=9 by fpbc_intro, feqg_fpb_trans, feqg_canc_sn, feqg_feqx/ +qed-. + +(* Inversion lemmas with generic equivalence for closures *******************) + +(* Basic_2A1: uses: fpb_inv_fleq *) +lemma fpbc_inv_feqg (S): + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥. +#S #G1 #G2 #L1 #L2 #T1 #T2 #H #H12 +elim (fpbc_inv_gen S … H) -H #_ #Hn2 +/2 width=1 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma new file mode 100644 index 000000000..35654e6da --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/feqx_feqx.ma". +include "basic_2/rt_transition/fpbc.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Inversrion lemmas with parallel rst-transition for closures **************) + +(* Basic_2A1: uses: fpbq_ind_alt *) +lemma fpb_inv_fpbc: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → + ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ + | ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H +elim (feqx_dec G1 G2 L1 L2 T1 T2) +/4 width=1 by fpbc_intro, or_intror, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fqup.ma new file mode 100644 index 000000000..23806bc82 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fqup.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/feqg_fqu.ma". +include "basic_2/rt_transition/fpb_fqup.ma". +include "basic_2/rt_transition/fpbc.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: fpb_cpx *) +lemma cpx_fpbc (G) (L): + ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → ❪G,L,T1❫ ≻ ❪G,L,T2❫. +/4 width=5 by fpbc_intro, cpx_fpb, feqg_fwd_teqg/ qed. + +(* Basic_2A1: uses: fpb_fqu *) +lemma fqu_fpbc (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫. +/4 width=10 by fpbc_intro, fquq_fpb, fqu_fquq, fqu_fneqg/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma new file mode 100644 index 000000000..5db9f7e13 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpx_reqg.ma". +include "basic_2/rt_transition/fpbc.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Properties with extended rt-transition for full local envs ***************) + +(* Basic_2A1: uses: fpb_lpx *) +lemma lpx_fpbc (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫. +/3 width=1 by rpx_fpbc, lpx_rpx/ qed. + +(* Forward lemmas with extended rt-transition for full local envs ***********) + +lemma fpbc_fwd_lpx (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → + ∨∨ ∃∃G,L,T. ❪G1,L1,T1❫ ⬂ ❪G,L,T❫ & ❪G,L,T❫ ≽ ❪G2,L2,T2❫ + | ∃∃T. ❪G1,L1❫ ⊢ T1 ⬈ T & T1 ≅ T → ⊥ & ❪G1,L1,T❫ ≽ ❪G2,L2,T2❫ + | ∃∃L. ❪G1,L1❫ ⊢ ⬈ L & (L1 ≅[T1] L → ⊥) & ❪G1,L,T1❫ ≽ ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H +elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12 +elim (fpb_inv_gen … H12) -H12 #L #T #H1 #HT2 #HL2 +elim H1 -H1 [ /4 width=9 by fpb_intro, ex2_3_intro, or3_intro0/ ] +* #H1 #H2 #H3 destruct +elim (teqg_dec sfull … T T2) +[ -HT2 #HT2 |*: /5 width=11 by fpb_intro, cpx_rex_conf_sn, ex3_intro, or3_intro1, sfull_dec/ ] +elim (rpx_fwd_lpx_reqg sfull … HL2) -HL2 // #L0 #HL0 #HL02 +elim (reqg_dec sfull … L L0 T) +[ -HL0 #HL0 |*: /5 width=11 by fpb_intro, reqg_rpx, teqg_cpx, ex3_intro, or3_intro2, sfull_dec/ ] +elim Hn12 -Hn12 /3 width=3 by feqg_intro_sn, reqg_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma deleted file mode 100644 index 2a12bf05f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma +++ /dev/null @@ -1,50 +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/predsubty_6.ma". -include "static_2/static/feqx.ma". -include "static_2/s_transition/fquq.ma". -include "basic_2/rt_transition/lpr_lpx.ma". - -(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) - -(* Basic_2A1: includes: fleq_fpbq fpbq_lleq *) -inductive fpbq (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbq_fquq: ∀G2,L2,T2. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L2,T2❫ → fpbq G1 L1 T1 G2 L2 T2 -| fpbq_cpx : ∀T2. ❪G1,L1❫ ⊢ T1 ⬈ T2 → fpbq G1 L1 T1 G1 L1 T2 -| fpbq_lpx : ∀L2. ❪G1,L1❫ ⊢ ⬈ L2 → fpbq G1 L1 T1 G1 L2 T1 -| fpbq_feqx: ∀G2,L2,T2. ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → fpbq G1 L1 T1 G2 L2 T2 -. - -interpretation - "parallel rst-transition (closure)" - 'PRedSubTy G1 L1 T1 G2 L2 T2 = (fpbq G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fpbq_refl: tri_reflexive … fpbq. -/2 width=1 by fpbq_cpx/ qed. - -(* Basic_2A1: includes: cpr_fpbq *) -lemma cpm_fpbq (h) (n) (G) (L): - ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫. -/3 width=3 by fpbq_cpx, cpm_fwd_cpx/ qed. - -lemma lpr_fpbq (h) (G) (T): - ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫. -/3 width=2 by fpbq_lpx, lpr_fwd_lpx/ qed. - -(* Basic_2A1: removed theorems 2: - fpbq_fpbqa fpbqa_inv_fpbq -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma deleted file mode 100644 index 452145541..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma +++ /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 "static_2/static/aaa_fqus.ma". -include "static_2/static/aaa_feqg.ma". -include "basic_2/rt_transition/lpx_aaa.ma". -include "basic_2/rt_transition/fpbq.ma". - -(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) - -(* Properties with atomic arity assignment for terms ************************) - -lemma fpbq_aaa_conf: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → - ∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=8 by lpx_aaa_conf, cpx_aaa_conf, aaa_feqg_conf, aaa_fquq_conf, ex_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma deleted file mode 100644 index 7f0fa2577..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma +++ /dev/null @@ -1,65 +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/static/feqg_fqup.ma". -include "static_2/static/feqg_feqg.ma". -include "basic_2/rt_transition/fpb_feqg.ma". -include "basic_2/rt_transition/fpbq.ma". - -(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) - -(* Properties with proper parallel rst-transition for closures **************) - -lemma fpb_fpbq: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → - ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=1 by fpbq_fquq, fpbq_cpx, fpbq_lpx, fqu_fquq/ -qed. - -(* Basic_2A1: fpb_fpbq_alt *) -lemma fpb_fpbq_fneqx (S): - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ → - ∧∧ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ & (❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥). -/3 width=10 by fpb_fpbq, fpb_inv_feqg, conj/ qed-. - -(* Inversrion lemmas with proper parallel rst-transition for closures *******) - -(* Basic_2A1: fpbq_inv_fpb_alt *) -lemma fpbq_fneqx_inv_fpb: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → - (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ → ⊥) → ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -[ #G2 #L2 #T2 * [2: * #H1 #H2 #H3 destruct ] - [ #H elim H -H /2 width=1 by feqg_refl/ - | /2 width=1 by fpb_fqu/ - ] -| /4 width=1 by fpb_cpx, teqg_feqg/ -| /4 width=1 by fpb_lpx, feqg_intro_sn/ -| #G2 #L2 #T2 #H12 #Hn12 - elim Hn12 -Hn12 // -] -qed-. - -(* Basic_2A1: uses: fpbq_ind_alt *) -lemma fpbq_inv_fpb: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → - ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫ - | ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫. -#G1 #G2 #L1 #L2 #T1 #T2 #H -elim (feqg_dec sfull … G1 G2 L1 L2 T1 T2) // -[ /2 width=1 by or_introl/ -| /4 width=1 by fpbq_fneqx_inv_fpb, or_intror/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpb.ma new file mode 100644 index 000000000..866a03b98 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpb.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_transition/fpb_lpx.ma". +include "basic_2/rt_transition/lpr_lpx.ma". + +(* PARALLEL R-TRANSITION FOR FULL LOCAL ENVIRONMENTS ************************) + +(* Forward lemmas with rst-transition for closures **************************) + +(* Basic_2A1: uses: lpr_fpbq *) +lemma lpr_fwd_fpb (h) (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫. +/3 width=2 by lpx_fpb, lpr_fwd_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpbc.ma new file mode 100644 index 000000000..542e4bf3f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fpbc.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_transition/fpbc_lpx.ma". +include "basic_2/rt_transition/lpr_lpx.ma". + +(* PARALLEL R-TRANSITION FOR FULL LOCAL ENVIRONMENTS ************************) + +(* Forward lemmas with proper rst-transition for closures *******************) + +(* Basic_2A1: uses: lpr_fpb *) +lemma lpr_fwd_fpbc (h) (G) (T): + ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫. +/3 width=2 by lpx_fpbc, lpr_fwd_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqg.ma index 4041da979..2b9dbd29c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqg.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -include "static_2/static/req.ma". -include "basic_2/rt_transition/rpx_lpx.ma". +include "basic_2/rt_transition/rpx_lpx.ma". (**) (* one dependence *) (* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************) (* Properties with generic equivalence for local environments ***************) lemma reqg_lpx_trans_rpx (S) (G) (L) (T:term): - ∀L1. L1 ≛[S,T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2. -/3 width=1 by lpx_rpx, reqg_rpx_trans/ qed. + reflexive … S → symmetric … S → + ∀L1. L1 ≛[S,T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L1❫ ⊢ ⬈[T] L2. +/3 width=6 by lpx_rpx, reqg_rpx_trans/ qed. (* Basic_2A1: uses: lleq_lpx_trans *) lemma reqg_lpx_trans (S) (G) (T:term): @@ -35,7 +35,7 @@ elim (rpx_fwd_lpx_req … H) -H #K1 #HLK1 #HK12 /3 width=3 by req_fwd_reqg, ex2_intro/ qed-. -(* Inversion lemmas with sort-irrelevant equivalence for local environments *) +(* Inversion lemmas with generic equivalence for local environments *********) lemma rpx_inv_reqg_lpx (S) (G) (T): reflexive … S → @@ -46,7 +46,7 @@ elim (rpx_inv_req_lpx … H) -H #L #HL1 #HL2 /3 width=3 by req_fwd_reqg, ex2_intro/ qed-. -(* Forward lemmas with sort-irrelevant equivalence for local environments ***) +(* Forward lemmas with generic equivalence for local environments ***********) lemma rpx_fwd_lpx_reqg (S) (G) (T): reflexive … S → diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index fcabdb760..befee2607 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -26,6 +26,9 @@ + + Improved rst-transition and related theory. + Sort hierarchy parameter removed from unbound rt-transition (anniversary milestone). 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 6439d77b9..5df024fb6 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 @@ -80,15 +80,15 @@ table { ] [ { "extended context-sensitive parallel rst-computation" * } { [ [ "strongly normalizing for closures" ] "fsb" + "( ≥𝐒 ❪?,?,?❫ )" "fsb_feqg" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ] - [ [ "proper for closures" ] "fpbg" + "( ❪?,?,?❫ > ❪?,?,?❫ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ] - [ [ "for closures" ] "fpbs" + "( ❪?,?,?❫ ≥ ❪?,?,?❫ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ] + [ [ "proper for closures" ] "fpbg" + "( ❪?,?,?❫ > ❪?,?,?❫ )" "fpbg_fqup" + "fpbg_fqus" + "fpbg_feqg" + "fpbg_cpm" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ] + [ [ "for closures" ] "fpbs" + "( ❪?,?,?❫ ≥ ❪?,?,?❫ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_feqg" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpbc" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ] } ] [ { "extended context-sensitive parallel rt-computation" * } { [ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒ ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ] [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*𝐒[?] ? )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ] [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ❪?,?❫ ⊢ ⬈*𝐒 ? )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*𝐒 ? )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqg" + "csx_feqg" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ] + [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*𝐒 ? )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqg" + "csx_feqg" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpb" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ] [ [ "for lenvs on all entries" ] "lpxs" + "( ❪?,?❫ ⊢ ⬈* ? )" "lpxs_length" + "lpxs_drops" + "lpxs_reqg" + "lpxs_feqg" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ [ "for binders" ] "cpxs_ext" + "( ❪?,?❫ ⊢ ? ⬈* ? )" * ] [ [ "for terms" ] "cpxs" + "( ❪?,?❫ ⊢ ? ⬈* ? )" "cpxs_teqg" + "cpxs_teqo" + "cpxs_teqo_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_reqg" + "cpxs_feqg" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ] @@ -104,18 +104,18 @@ table { ] [ { "context-sensitive parallel r-transition" * } { [ [ "normal form for terms" ] "cnr ( ❪?,?❫ ⊢ ➡𝐍[?,?] ? )" "cnr_simple" + "cnr_teqg" + "cnr_teqx" + "cnr_drops" * ] - [ [ "for lenvs on all entries" ] "lpr" + "( ❪?,?❫ ⊢ ➡[?,?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ] + [ [ "for lenvs on all entries" ] "lpr" + "( ❪?,?❫ ⊢ ➡[?,?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_fpb" + "lpr_fpbc" + "lpr_lpr" * ] [ [ "for binders" ] "cpr_ext" * ] [ [ "for terms" ] "cpr" "cpr_drops" + "cpr_drops_basic" + "cpr_teqg" + "cpr_cpr" * ] } ] [ { "t-bound context-sensitive parallel rt-transition" * } { - [ [ "for terms" ] "cpm" + "( ❪?,?❫ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_teqx" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] + [ [ "for terms" ] "cpm" + "( ❪?,?❫ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_teqx" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" + "cpm_fpb" + "cpm_fpbc" * ] } ] [ { "extended parallel rst-transition" * } { - [ [ "for closures" ] "fpbq" + "( ❪?,?,?❫ ≽ ❪?,?,?❫ )" "fpbq_aaa" + "fpbq_fpb" * ] - [ [ "proper for closures" ] "fpb" + "( ❪?,?,?❫ ≻ ❪?,?,?❫ )" "fpb_reqg" + "fpb_feqg" * ] + [ [ "proper for closures" ] "fpbc" + "( ❪?,?,?❫ ≻ ❪?,?,?❫ )" "fpbc_fqup" + "fpbc_feqg" + "fpbc_lpx" + "fpbc_fpb" * ] + [ [ "for closures" ] "fpb" + "( ❪?,?,?❫ ≽ ❪?,?,?❫ )" "fpb_fqup" + "fpb_feqg" + "fpb_aaa" + "fpb_lpx" * ] } ] [ { "extended context-sensitive parallel rt-transition" * } { diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma new file mode 100644 index 000000000..1dd1986dc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma @@ -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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (3, 6) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex6 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex6 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) }. + diff --git a/matita/matita/contribs/lambdadelta/ground/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground/xoa.conf.xml index 73adf22c3..9ef6d4f38 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground/xoa.conf.xml @@ -17,6 +17,7 @@ 3 3 3 4 3 5 + 3 6 4 1 4 2 4 3 diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma new file mode 100644 index 000000000..ccef1fd88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground/notation/xoa/ex_3_6.ma". + +(* multiple existental quantifier (3, 6) *) + +inductive ex3_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ + | ex3_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → ex3_6 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 6)" 'Ex6 P0 P1 P2 = (ex3_6 ? ? ? ? ? ? P0 P1 P2). + diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_feqx.etc b/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_feqx.etc deleted file mode 100644 index 62ed7e48c..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/etc/teqx/feqx_feqx.etc +++ /dev/null @@ -1,52 +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/static/reqx_reqx.ma". -include "static_2/static/feqx.ma". - -(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) - -(* Advanced properties ******************************************************) - -lemma feqx_sym: tri_symmetric … feqx. -#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 -/3 width=1 by feqx_intro_dx, reqx_sym, teqx_sym/ -qed-. - -(* Main properties **********************************************************) - -theorem feqx_trans: tri_transitive … feqx. -#G1 #G #L1 #L #T1 #T * -G -L -T -#L #T #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 -/4 width=5 by feqx_intro_sn, reqx_trans, teqx_reqx_div, teqx_trans/ -qed-. - -theorem feqx_canc_sn: ∀G,G1,L,L1,T,T1. ❪G,L,T❫ ≛ ❪G1,L1,T1❫→ - ∀G2,L2,T2. ❪G,L,T❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫. -/3 width=5 by feqx_trans, feqx_sym/ qed-. - -theorem feqx_canc_dx: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ → - ∀G2,L2,T2. ❪G2,L2,T2❫ ≛ ❪G,L,T❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫. -/3 width=5 by feqx_trans, feqx_sym/ qed-. - -(* Main inversion lemmas with degree-based equivalence on terms *************) - -theorem feqx_tneqx_repl_dx: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → - ∀U1,U2. ❪G1,L1,U1❫ ≛ ❪G2,L2,U2❫ → - (T2 ≛ U2 → ⊥) → (T1 ≛ U1 → ⊥). -#G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1 -elim (feqx_inv_gen_sn … HT) -HT #_ #_ #HT -elim (feqx_inv_gen_sn … HU) -HU #_ #_ #HU -/3 width=5 by teqx_repl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqg.ma index e2d735487..f2b4fb056 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_reqg.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "static_2/static/reqg.ma". +include "static_2/static/reqg_fqup.ma". include "static_2/static/aaa.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) @@ -45,3 +45,13 @@ lemma aaa_teqg_conf_reqg (S) (G): /3 width=1 by aaa_cast/ ] qed-. + +lemma aaa_teqg_conf (S) (G) (L) (A): + reflexive … S → + ∀T1. ❪G,L❫ ⊢ T1 ⁝ A → ∀T2. T1 ≛[S] T2 → ❪G,L❫ ⊢ T2 ⁝ A. +/3 width=7 by aaa_teqg_conf_reqg, reqg_refl/ qed-. + +lemma aaa_reqg_conf (S) (G) (T) (A): + reflexive … S → + ∀L1. ❪G,L1❫ ⊢ T ⁝ A → ∀L2. L1 ≛[S,T] L2 → ❪G,L2❫ ⊢ T ⁝ A. +/3 width=7 by aaa_teqg_conf_reqg, teqg_refl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma index 39cba31e9..378e52d91 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma @@ -51,6 +51,27 @@ lemma feqg_inv_gen_dx (S): /3 width=6 by teqg_reqg_conf_sn, and3_intro/ qed-. +(* Basic forward lemmas *****************************************************) + +lemma feqg_fwd_teqg (S): + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → T1 ≛[S] T2. +#S #G1 #G2 #L1 #L2 #T1 #T2 #H +elim (feqg_inv_gen_sn … H) -H // +qed-. + +lemma feqg_fwd_reqg_sn (S): + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → L1 ≛[S,T1] L2. +#S #G1 #G2 #L1 #L2 #T1 #T2 #H +elim (feqg_inv_gen_sn … H) -H // +qed-. + +lemma feqg_fwd_reqg_dx (S): + reflexive … S → + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → L1 ≛[S,T2] L2. +#S #HS #G1 #G2 #L1 #L2 #T1 #T2 #H +elim (feqg_inv_gen_dx … H) -H // +qed-. + (* Basic_2A1: removed theorems 6: fleq_refl fleq_sym fleq_inv_gen fleq_trans fleq_canc_sn fleq_canc_dx diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma index cb2b11ddd..7a3339a88 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma @@ -63,15 +63,22 @@ theorem feqg_canc_dx (S): ∀G2,L2,T2. ❪G2,L2,T2❫ ≛[S] ❪G,L,T❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫. /3 width=5 by feqg_trans, feqg_sym/ qed-. -(* Main inversion lemmas with generic equivalence on terms ******************) +lemma feqg_reqg_trans (S) (G2) (L) (T2): + reflexive … S → symmetric … S → Transitive … S → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L,T2❫ → + ∀L2. L ≛[S,T2] L2 → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫. +#S #G2 #L #T2 #H1S #H2S #H3S #G1 #L1 #T1 #H1 #L2 #HL2 +/4 width=5 by feqg_trans, feqg_intro_sn, teqg_refl/ +qed-. -theorem feqg_tneqg_repl_dx (S): - reflexive … S → symmetric … S → Transitive … S → - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → - ∀U1,U2. ❪G1,L1,U1❫ ≛[S] ❪G2,L2,U2❫ → - (T2 ≛[S] U2 → ⊥) → (T1 ≛[S] U1 → ⊥). -#S #H1S #H2S #H3S #G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1 -elim (feqg_inv_gen_sn … HT) -HT #_ #_ #HT -elim (feqg_inv_gen_sn … HU) -HU #_ #_ #HU -/3 width=5 by teqg_repl/ +(* Inversion lemmas with generic equivalence on terms ***********************) + +(* Basic_2A1: uses: feqg_tneqg_repl_dx *) +lemma feqg_tneqg_trans (S) (G1) (G2) (L1) (L2) (T): + reflexive … S → symmetric … S → Transitive … S → + ∀T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ → + ∀T2. (T ≛[S] T2 → ⊥) → (T1 ≛[S] T2 → ⊥). +#S #G1 #G2 #L1 #L2 #T #H1S #H2S #H3S #T1 #H1 #T2 #HnT2 #HT12 +elim (feqg_inv_gen_sn … H1) -H1 #_ #_ #HnT1 -G1 -G2 -L1 -L2 +/3 width=3 by teqg_canc_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqu.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqu.ma new file mode 100644 index 000000000..3e7ddc638 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqu.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/feqg_length.ma". + +(* GENERIC EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *********************) + +(* Properties with structural successor for closures ************************) + +lemma fqu_fneqg (S) (b) (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥. +#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ /3 width=8 by feqg_fwd_length, succ_inv_refl_sn/ +| /3 width=9 by teqg_inv_pair_xy_x, feqg_fwd_teqg/ +| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/ +| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/ +| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/ +| /3 width=8 by feqg_fwd_length, succ_inv_refl_sn/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqus.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqus.ma index b2db044de..33663faa0 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqus.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_fqus.ma @@ -19,6 +19,19 @@ include "static_2/static/feqg.ma". (* Properties with star-iterated structural successor for closures **********) +lemma feqg_fquq_trans (S) (b): + reflexive … S → symmetric … S → Transitive … S → + ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ⬂⸮[b] ❪G2,L2,T2❫ → + ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂⸮[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛[S] ❪G2,L2,T2❫. +#S #b #H1S #H2S #H3S #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2 +elim(feqg_inv_gen_dx … H1) -H1 // #HG #HL1 #HT1 destruct +elim (reqg_fquq_trans … H2 … HL1) -L // #L #T0 #H2 #HT02 #HL2 +elim (teqg_fquq_trans … H2 … HT1) -T // #L0 #T #H2 #HT0 #HL0 +lapply (teqg_reqg_conf_sn … HT02 … HL0) -HL0 // #HL0 +/4 width=7 by feqg_intro_dx, reqg_trans, teqg_trans, ex2_3_intro/ +qed-. + lemma feqg_fqus_trans (S) (b): reflexive … S → symmetric … S → Transitive … S → ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ → diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_length.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_length.ma new file mode 100644 index 000000000..fd4119f87 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_length.ma @@ -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/static/reqg_length.ma". +include "static_2/static/feqg.ma". + +(* GENERIC EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *********************) + +(* Forward lemmas with length for local environments ************************) + +lemma feqg_fwd_length (S) (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → |L1| = |L2|. +/3 width=6 by feqg_fwd_reqg_sn, reqg_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma index e4c8a22d1..9804e73c2 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx.ma @@ -13,41 +13,23 @@ (**************************************************************************) include "static_2/notation/relations/approxeqsn_6.ma". -include "static_2/syntax/teqx.ma". +include "static_2/static/reqx.ma". include "static_2/static/feqg.ma". (* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) - +(* definition feqx: relation6 genv lenv term genv lenv term ≝ feqg sfull. - +*) interpretation "sort-irrelevant equivalence on referred entries (closure)" - 'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqx G1 L1 T1 G2 L2 T2). + 'ApproxEqSn G1 L1 T1 G2 L2 T2 = (feqg sfull G1 L1 T1 G2 L2 T2). (* Basic_properties *********************************************************) -(* -lemma feqx_intro_dx (G): - ∀L1,L2,T2. L1 ≛[T2] L2 → - ∀T1. T1 ≛ T2 → ❪G,L1,T1❫ ≛ ❪G,L2,T2❫. -/3 width=3 by feqx_intro_sn, teqx_reqx_div/ qed. -(* Basic inversion lemmas ***************************************************) - -lemma feqx_inv_gen_sn: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → - ∧∧ G1 = G2 & L1 ≛[T1] L2 & T1 ≛ T2. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ -qed-. - -lemma feqx_inv_gen_dx: - ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → - ∧∧ G1 = G2 & L1 ≛[T2] L2 & T1 ≛ T2. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=3 by teqx_reqx_conf_sn, and3_intro/ -qed-. -*) -(* Basic_2A1: removed theorems 6: - fleq_refl fleq_sym fleq_inv_gen - fleq_trans fleq_canc_sn fleq_canc_dx -*) +lemma feqg_feqx (S) (G1) (G2) (L1) (L2) (T1) (T2): + ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫. +#S #G1 #G2 #L1 #L2 #T1 #T2 #H +elim (feqg_inv_gen_sn … H) -H +/3 width=2 by feqg_intro_sn, reqg_reqx, teqg_teqx/ +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqx_feqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqx_feqx.ma new file mode 100644 index 000000000..dddcb113b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/static/feqx_feqx.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/feqg_feqg.ma". +include "static_2/static/feqx.ma". + +(* SORT-IRRELEVANT EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *************) + +(* Advanced properties ******************************************************) + +lemma feqx_dec (G1) (G2) (L1) (L2) (T1) (T2): + Decidable (❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫). +/3 width=1 by feqg_dec, sfull_dec/ qed-. +(* +lemma feqx_sym: tri_symmetric … feqx. +#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 +/3 width=1 by feqx_intro_dx, reqx_sym, teqx_sym/ +qed-. + +(* Main properties **********************************************************) + +theorem feqx_trans: tri_transitive … feqx. +#G1 #G #L1 #L #T1 #T * -G -L -T +#L #T #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 +/4 width=5 by feqx_intro_sn, reqx_trans, teqx_reqx_div, teqx_trans/ +qed-. + +theorem feqx_canc_sn: ∀G,G1,L,L1,T,T1. ❪G,L,T❫ ≛ ❪G1,L1,T1❫→ + ∀G2,L2,T2. ❪G,L,T❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫. +/3 width=5 by feqx_trans, feqx_sym/ qed-. + +theorem feqx_canc_dx: ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ → + ∀G2,L2,T2. ❪G2,L2,T2❫ ≛ ❪G,L,T❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫. +/3 width=5 by feqx_trans, feqx_sym/ qed-. + +(* Main inversion lemmas with degree-based equivalence on terms *************) + +theorem feqx_tneqx_repl_dx: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → + ∀U1,U2. ❪G1,L1,U1❫ ≛ ❪G2,L2,U2❫ → + (T2 ≛ U2 → ⊥) → (T1 ≛ U1 → ⊥). +#G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1 +elim (feqx_inv_gen_sn … HT) -HT #_ #_ #HT +elim (feqx_inv_gen_sn … HU) -HU #_ #_ #HU +/3 width=5 by teqx_repl/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma index 41f0fee26..cb01ec662 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqg_reqg.ma @@ -14,7 +14,6 @@ include "static_2/syntax/ext2_ext2.ma". include "static_2/syntax/teqg_teqg.ma". -include "static_2/static/rex_rex.ma". include "static_2/static/reqg_length.ma". (* GENERIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***********) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma index b6dc3d196..8f9999e64 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma @@ -24,7 +24,7 @@ lemma reqx_sym: ∀T. symmetric … (reqx T). *) (* Basic_2A1: uses: lleq_dec *) lemma reqx_dec: ∀L1,L2. ∀T:term. Decidable (L1 ≅[T] L2). -/2 width=1 by reqg_dec/ qed-. +/3 width=1 by reqg_dec, sfull_dec/ qed-. (* (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma index 1db29eabb..bcaff1f89 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/item.ma @@ -17,34 +17,37 @@ include "ground/lib/arith.ma". (* ITEMS ********************************************************************) +definition sfull: relation2 nat nat ≝ + λs1,s2. ⊤. + (* atomic items *) inductive item0: Type[0] ≝ - | Sort: nat → item0 (* sort: starting at 0 *) - | LRef: nat → item0 (* reference by index: starting at 0 *) - | GRef: nat → item0 (* reference by position: starting at 0 *) +| Sort: nat → item0 (* sort: starting at 0 *) +| LRef: nat → item0 (* reference by index: starting at 0 *) +| GRef: nat → item0 (* reference by position: starting at 0 *) . (* unary binding items *) inductive bind1: Type[0] ≝ - | Void: bind1 (* exclusion *) +| Void: bind1 (* exclusion *) . (* binary binding items *) inductive bind2: Type[0] ≝ - | Abbr: bind2 (* abbreviation *) - | Abst: bind2 (* abstraction *) +| Abbr: bind2 (* abbreviation *) +| Abst: bind2 (* abstraction *) . (* binary non-binding items *) inductive flat2: Type[0] ≝ - | Appl: flat2 (* application *) - | Cast: flat2 (* explicit type annotation *) +| Appl: flat2 (* application *) +| Cast: flat2 (* explicit type annotation *) . (* binary items *) inductive item2: Type[0] ≝ - | Bind2: bool → bind2 → item2 (* polarized binding item *) - | Flat2: flat2 → item2 (* non-binding item *) +| Bind2: bool → bind2 → item2 (* polarized binding item *) +| Flat2: flat2 → item2 (* non-binding item *) . (* Basic inversion lemmas ***************************************************) @@ -55,30 +58,39 @@ qed-. (* Basic properties *********************************************************) -lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2). +lemma sfull_dec: + ∀s1,s2. Decidable (sfull s1 s2). +/2 width=1 by or_introl/ qed-. + +lemma eq_item0_dec: + ∀I1,I2:item0. Decidable (I1 = I2). * #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ] [2: elim (eq_nat_dec i1 i2) |1,3: elim (eq_nat_dec i1 i2) ] /2 width=1 by or_introl/ #Hni12 @or_intror #H destruct /2 width=1 by/ qed-. -lemma eq_bind1_dec: ∀I1,I2:bind1. Decidable (I1 = I2). +lemma eq_bind1_dec: + ∀I1,I2:bind1. Decidable (I1 = I2). * * /2 width=1 by or_introl/ qed-. (* Basic_1: was: bind_dec *) -lemma eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2). +lemma eq_bind2_dec: + ∀I1,I2:bind2. Decidable (I1 = I2). * * /2 width=1 by or_introl/ @or_intror #H destruct qed-. (* Basic_1: was: flat_dec *) -lemma eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2). +lemma eq_flat2_dec: + ∀I1,I2:flat2. Decidable (I1 = I2). * * /2 width=1 by or_introl/ @or_intror #H destruct qed-. (* Basic_1: was: kind_dec *) -lemma eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2). +lemma eq_item2_dec: + ∀I1,I2:item2. Decidable (I1 = I2). * [ #p1 ] #I1 * [1,3: #p2 ] #I2 [2,3: @or_intror #H destruct | elim (eq_bool_dec p1 p2) #Hp diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma index ed581c5be..f44d4c438 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma @@ -17,9 +17,6 @@ include "static_2/syntax/teqg.ma". (* SORT-IRRELEVANT EQUIVALENCE ON TERMS *************************************) -definition sfull: relation2 nat nat ≝ - λs1,s2. ⊤. - definition teqx: relation term ≝ teqg sfull. @@ -29,10 +26,6 @@ interpretation (* Basic properties *********************************************************) -lemma sfull_dec: - ∀s1,s2. Decidable (sfull s1 s2). -/2 width=1 by or_introl/ qed. - lemma teqx_pair: ∀V1,V2. V1 ≅ V2 → ∀T1,T2. T1 ≅ T2 → ∀I. ②[I]V1.T1 ≅ ②[I]V2.T2. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx_ext.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx_ext.ma index efbf86075..68a91196f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/teqx_ext.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teqx_ext.ma @@ -13,7 +13,7 @@ (**************************************************************************) (* -include "static_2/notation/relations/stareq_3.ma". +include "static_2/notation/relations/approxeq_3.ma". *) include "static_2/syntax/teqg_ext.ma". include "static_2/syntax/teqx.ma". diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma index 83937e544..0a6f97872 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma @@ -36,72 +36,91 @@ include "static_2/syntax/item.ma". (* terms *) inductive term: Type[0] ≝ - | TAtom: item0 → term (* atomic item construction *) - | TPair: item2 → term → term → term (* binary item construction *) +| TAtom: item0 → term (* atomic item construction *) +| TPair: item2 → term → term → term (* binary item construction *) . -interpretation "term construction (atomic)" - 'Item0 I = (TAtom I). +interpretation + "term construction (atomic)" + 'Item0 I = (TAtom I). -interpretation "term construction (binary)" - 'SnItem2 I T1 T2 = (TPair I T1 T2). +interpretation + "term construction (binary)" + 'SnItem2 I T1 T2 = (TPair I T1 T2). -interpretation "term binding construction (binary)" - 'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2). +interpretation + "term binding construction (binary)" + 'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2). -interpretation "term positive binding construction (binary)" - 'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2). +interpretation + "term positive binding construction (binary)" + 'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2). -interpretation "term negative binding construction (binary)" - 'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2). +interpretation + "term negative binding construction (binary)" + 'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2). -interpretation "term flat construction (binary)" - 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2). +interpretation + "term flat construction (binary)" + 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2). -interpretation "sort (term)" - 'Star s = (TAtom (Sort s)). +interpretation + "sort (term)" + 'Star s = (TAtom (Sort s)). -interpretation "local reference (term)" - 'LRef i = (TAtom (LRef i)). +interpretation + "local reference (term)" + 'LRef i = (TAtom (LRef i)). -interpretation "global reference (term)" - 'GRef l = (TAtom (GRef l)). +interpretation + "global reference (term)" + 'GRef l = (TAtom (GRef l)). -interpretation "abbreviation (term)" - 'SnAbbr p T1 T2 = (TPair (Bind2 p Abbr) T1 T2). +interpretation + "abbreviation (term)" + 'SnAbbr p T1 T2 = (TPair (Bind2 p Abbr) T1 T2). -interpretation "positive abbreviation (term)" - 'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2). +interpretation + "positive abbreviation (term)" + 'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2). -interpretation "negative abbreviation (term)" - 'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2). +interpretation + "negative abbreviation (term)" + 'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2). -interpretation "abstraction (term)" - 'SnAbst p T1 T2 = (TPair (Bind2 p Abst) T1 T2). +interpretation + "abstraction (term)" + 'SnAbst p T1 T2 = (TPair (Bind2 p Abst) T1 T2). -interpretation "positive abstraction (term)" - 'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2). +interpretation + "positive abstraction (term)" + 'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2). -interpretation "negative abstraction (term)" - 'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2). +interpretation + "negative abstraction (term)" + 'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2). -interpretation "application (term)" - 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2). +interpretation + "application (term)" + 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2). -interpretation "native type annotation (term)" - 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2). +interpretation + "native type annotation (term)" + 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2). (* Basic properties *********************************************************) -lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ[p]W.T - | (∀p,W,T. X = ⓛ[p]W.T → ⊥). +lemma abst_dec (X): + ∨∨ ∃∃p,W,T. X = ⓛ[p]W.T + | (∀p,W,T. X = ⓛ[p]W.T → ⊥). * [ #I | * [ #p * | #I ] #V #T ] [3: /3 width=4 by ex1_3_intro, or_introl/ ] @or_intror #q #W #U #H destruct qed-. (* Basic_1: was: term_dec *) -lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2). +lemma eq_term_dec: + ∀T1,T2:term. Decidable (T1 = T2). #T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ] [1,4: @or_intror #H destruct | elim (eq_item2_dec I1 I2) #HI @@ -116,16 +135,19 @@ qed-. (* Basic inversion lemmas ***************************************************) -fact destruct_tatom_tatom_aux: ∀I1,I2. ⓪[I1] = ⓪[I2] → I1 = I2. +fact destruct_tatom_tatom_aux: + ∀I1,I2. ⓪[I1] = ⓪[I2] → I1 = I2. #I1 #I2 #H destruct // qed-. -fact destruct_tpair_tpair_aux: ∀I1,I2,T1,T2,V1,V2. ②[I1]T1.V1 = ②[I2]T2.V2 → - ∧∧T1 = T2 & I1 = I2 & V1 = V2. +fact destruct_tpair_tpair_aux: + ∀I1,I2,T1,T2,V1,V2. ②[I1]T1.V1 = ②[I2]T2.V2 → + ∧∧ T1 = T2 & I1 = I2 & V1 = V2. #I1 #I2 #T1 #T2 #V1 #V2 #H destruct /2 width=1 by and3_intro/ qed-. -lemma discr_tpair_xy_x: ∀I,T,V. ②[I]V.T = V → ⊥. +lemma discr_tpair_xy_x: + ∀I,T,V. ②[I]V.T = V → ⊥. #I #T #V elim V -V [ #J #H destruct | #J #W #U #IHW #_ #H elim (destruct_tpair_tpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *) @@ -133,24 +155,27 @@ lemma discr_tpair_xy_x: ∀I,T,V. ②[I]V.T = V → ⊥. qed-. (* Basic_1: was: thead_x_y_y *) -lemma discr_tpair_xy_y: ∀I,V,T. ②[I]V.T = T → ⊥. +lemma discr_tpair_xy_y: + ∀I,V,T. ②[I]V.T = T → ⊥. #I #V #T elim T -T [ #J #H destruct | #J #W #U #_ #IHU #H elim (destruct_tpair_tpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *) ] qed-. -lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2. - (②[I]V1.T1 = ②[I]V2.T2 → ⊥) → - (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)). +lemma eq_false_inv_tpair_sn: + ∀I,V1,T1,V2,T2. + (②[I]V1.T1 = ②[I]V2.T2 → ⊥) → + (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)). #I #V1 #T1 #V2 #T2 #H elim (eq_term_dec V1 V2) /3 width=1 by or_introl/ #HV12 destruct @or_intror @conj // #HT12 destruct /2 width=1 by/ qed-. -lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2. - (②[I] V1. T1 = ②[I]V2.T2 → ⊥) → - (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)). +lemma eq_false_inv_tpair_dx: + ∀I,V1,T1,V2,T2. + (②[I] V1. T1 = ②[I]V2.T2 → ⊥) → + (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)). #I #V1 #T1 #V2 #T2 #H elim (eq_term_dec T1 T2) /3 width=1 by or_introl/ #HT12 destruct @or_intror @conj // #HT12 destruct /2 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 329c596ec..74f0e6f20 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -31,7 +31,7 @@ table { } ] [ { "sort-irrelevant equivalence" * } { - [ [ "for closures on referred entries" ] "feqx" + "( ❪?,?,?❫ ≅ ❪?,?,?❫ )" * ] + [ [ "for closures on referred entries" ] "feqx" + "( ❪?,?,?❫ ≅ ❪?,?,?❫ )" "feqx_feqx" * ] [ [ "for lenvs on referred entries" ] "reqx" + "( ? ≅[?] ? )" "reqx_reqx" * ] } ] @@ -40,7 +40,7 @@ table { } ] [ { "generic equivalence" * } { - [ [ "for closures on referred entries" ] "feqg" + "( ❪?,?,?❫ ≛[?] ❪?,?,?❫ )" "feqg_fqup" + "feqg_fqus" + "feqg_feqg" * ] + [ [ "for closures on referred entries" ] "feqg" + "( ❪?,?,?❫ ≛[?] ❪?,?,?❫ )" "feqg_length" + "feqg_fqu" + "feqg_fqup" + "feqg_fqus" + "feqg_feqg" * ] [ [ "for lenvs on referred entries" ] "reqg" + "( ? ≛[?,?] ? )" "reqg_length" + "reqg_drops" + "reqg_fqup" + "reqg_fqus" + "reqg_reqg" * ] } ]