From 6555775aa5268dec0d9ae4579412b659cacdc964 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 29 Mar 2017 10:24:25 +0000 Subject: [PATCH] - advances towards strong normalization - refactoring of properties with relocation --- .../lambdadelta/basic_2/relocation/drops.ma | 19 ++- .../basic_2/relocation/drops_ceq.ma | 6 +- .../basic_2/relocation/drops_drops.ma | 14 +++ .../basic_2/relocation/drops_lexs.ma | 12 +- .../basic_2/relocation/drops_lreq.ma | 8 +- .../basic_2/relocation/drops_lstar.ma | 4 +- .../lambdadelta/basic_2/relocation/lifts.ma | 6 +- .../basic_2/relocation/lifts_lifts.ma | 2 +- .../basic_2/relocation/lifts_tdeq.ma | 8 +- .../basic_2/rt_computation/cpxs_drops.ma | 41 +++--- .../basic_2/rt_computation/cpxs_theq.ma | 9 +- .../rt_computation/cpxs_theq_vector.ma | 6 +- .../basic_2/rt_computation/csx_cpxs.ma | 11 +- .../basic_2/rt_computation/csx_drops.ma | 4 +- .../basic_2/rt_computation/csx_lfpx.ma | 102 +++++++++++++++ .../basic_2/rt_computation/csx_lpx.ma | 117 ------------------ .../basic_2/rt_computation/csx_lsubr.ma | 46 +++++++ .../basic_2/rt_computation/lfpxs_cpxs.ma | 2 +- .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/cnx_drops.ma | 12 +- .../basic_2/rt_transition/cpg_drops.ma | 10 +- .../basic_2/rt_transition/cpm_drops.ma | 14 ++- .../basic_2/rt_transition/cpx_drops.ma | 14 ++- .../basic_2/rt_transition/cpx_fqus.ma | 10 +- .../basic_2/rt_transition/lfpr_drops.ma | 2 +- .../basic_2/rt_transition/lfpr_fquq.ma | 4 +- .../basic_2/rt_transition/lfpr_lfpr.ma | 23 ++-- .../basic_2/rt_transition/lfpx_drops.ma | 2 +- .../basic_2/rt_transition/lfpx_lfdeq.ma | 8 +- .../lambdadelta/basic_2/static/lfdeq_drops.ma | 6 +- .../lambdadelta/basic_2/static/lfdeq_fqus.ma | 2 +- .../lambdadelta/basic_2/static/lfxs_drops.ma | 8 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 33 files changed, 298 insertions(+), 238 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index 7a4ad7662..0a21cd1d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -46,22 +46,31 @@ definition d_deliftable1: predicate (relation2 lenv term) ≝ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U → R K T. -definition d_liftable2: predicate (lenv → relation term) ≝ - λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K → - ∀U1. ⬆*[f] T1 ≡ U1 → - ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2. +definition d_liftable2_sn: predicate (lenv → relation term) ≝ + λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K → + ∀U1. ⬆*[f] T1 ≡ U1 → + ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2. definition d_deliftable2_sn: predicate (lenv → relation term) ≝ λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K → ∀T1. ⬆*[f] T1 ≡ U1 → ∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2. +definition d_liftable2_bi: predicate (lenv → relation term) ≝ + λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K → + ∀U1. ⬆*[f] T1 ≡ U1 → + ∀U2. ⬆*[f] T2 ≡ U2 → R L U1 U2. + +definition d_deliftable2_bi: predicate (lenv → relation term) ≝ + λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K → + ∀T1. ⬆*[f] T1 ≡ U1 → + ∀T2. ⬆*[f] T2 ≡ U2 → R K T1 T2. + definition co_dropable_sn: predicate (rtmap → relation lenv) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → ∀f2,L2. R f2 L1 L2 → ∀f1. f ~⊚ f1 ≡ f2 → ∃∃K2. R f1 K1 K2 & ⬇*[b, f] L2 ≡ K2. - definition co_dropable_dx: predicate (rtmap → relation lenv) ≝ λR. ∀f2,L1,L2. R f2 L1 L2 → ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma index e5240d788..676c8d33f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma @@ -18,14 +18,14 @@ include "basic_2/relocation/drops.ma". (* Properties with context-sensitive equivalence for terms ******************) -lemma ceq_lift: d_liftable2 ceq. +lemma ceq_lift_sn: d_liftable2_sn ceq. /2 width=3 by ex2_intro/ qed-. -lemma ceq_inv_lift: d_deliftable2_sn ceq. +lemma ceq_inv_lift_sn: d_deliftable2_sn ceq. /2 width=3 by ex2_intro/ qed-. (* Note: d_deliftable2_sn cfull does not hold *) -lemma cfull_lift: d_liftable2 cfull. +lemma cfull_lift_sn: d_liftable2_sn cfull. #K #T1 #T2 #_ #b #f #L #_ #U1 #_ -K -T1 -b elim (lifts_total T2 f) /2 width=3 by ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma index e8dcdee40..7fae70bda 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma @@ -17,6 +17,20 @@ include "basic_2/relocation/drops_weight.ma". (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) +(* Main properties on generic relocation ************************************) + +lemma d_liftable2_sn_bi: ∀R. d_liftable2_sn R → d_liftable2_bi R. +#R #HR #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2 +elim (HR … HT12 … HLK … HTU1) -HR -K -T1 #X #HTX #HUX +<(lifts_mono … HTX … HTU2) -T2 -U2 -b -f // +qed-. + +lemma d_deliftable2_sn_bi: ∀R. d_deliftable2_sn R → d_deliftable2_bi R. +#R #HR #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2 +elim (HR … HU12 … HLK … HTU1) -HR -L -U1 #X #HUX #HTX +<(lifts_inj … HUX … HTU2) -U2 -T2 -b -f // +qed-. + (* Main properties **********************************************************) (* Basic_2A1: includes: drop_conf_ge drop_conf_be drop_conf_le *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma index a192a206e..1e22db645 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma @@ -41,8 +41,8 @@ lemma lexs_co_dropable_sn: ∀RN,RP. co_dropable_sn (lexs RN RP). qed-. (* Basic_2A1: includes: lpx_sn_liftable_dedropable *) -lemma lexs_liftable_co_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → - d_liftable2 RN → d_liftable2 RP → co_dedropable_sn (lexs RN RP). +lemma lexs_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2_sn RN → d_liftable2_sn RP → co_dedropable_sn (lexs RN RP). #RN #RP #H1RN #H1RP #H2RN #H2RP #b #f #L1 #K1 #H elim H -f -L1 -K1 [ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X /4 width=4 by drops_atom, lexs_atom, ex3_intro/ @@ -130,25 +130,25 @@ elim (lexs_co_dropable_dx … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf qed-. lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → - d_liftable2 RN → d_liftable2 RP → + d_liftable2_sn RN → d_liftable2_sn RP → ∀f1,K1,K2. K1 ⦻*[RN, RP, f1] K2 → ∀b,f,I,L1,V1. ⬇*[b,f] L1.ⓑ{I}V1 ≡ K1 → ∀f2. f ~⊚ f1 ≡ ⫯f2 → ∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RN L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2 -elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP +elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX #L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/ qed-. lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → - d_liftable2 RN → d_liftable2 RP → + d_liftable2_sn RN → d_liftable2_sn RP → ∀f1,K1,K2. K1 ⦻*[RN, RP, f1] K2 → ∀b,f,I,L1,V1. ⬇*[b,f] L1.ⓑ{I}V1 ≡ K1 → ∀f2. f ~⊚ f1 ≡ ↑f2 → ∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RP L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2 -elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP +elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX #L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index c9934f664..7059e9c43 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -19,9 +19,9 @@ include "basic_2/relocation/drops_lexs.ma". (* Properties with ranged equivalence for local environments ****************) -lemma lreq_co_dedropable: co_dedropable_sn lreq. -@lexs_liftable_co_dedropable -/2 width=6 by cfull_lift, ceq_lift/ qed-. +lemma lreq_co_dedropable_sn: co_dedropable_sn lreq. +@lexs_liftable_co_dedropable_sn +/2 width=6 by cfull_lift_sn, ceq_lift_sn/ qed-. lemma lreq_co_dropable_sn: co_dropable_sn lreq. @lexs_co_dropable_sn qed-. @@ -55,4 +55,4 @@ lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 → ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V. #f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1 -/2 width=6 by cfull_lift, ceq_lift, ex3_intro/ qed-. +/2 width=6 by cfull_lift_sn, ceq_lift_sn, ex3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma index 8badfaf9d..b3785339f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma @@ -20,7 +20,7 @@ include "basic_2/relocation/lreq_lreq.ma". (* Properties with reflexive and transitive closure *************************) (* Basic_2A1: was: d_liftable_LTC *) -lemma d2_liftable_LTC: ∀R. d_liftable2 R → d_liftable2 (LTC … R). +lemma d2_liftable_sn_LTC: ∀R. d_liftable2_sn R → d_liftable2_sn (LTC … R). #R #HR #K #T1 #T2 #H elim H -T2 [ #T2 #HT12 #b #f #L #HLK #U1 #HTU1 elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/ @@ -52,7 +52,7 @@ lemma co_dropable_sn_TC: ∀R. co_dropable_sn R → co_dropable_sn (LTC … R). qed-. (* Basic_2A1: was: d_liftable_llstar *) -lemma d2_liftable_llstar: ∀R. d_liftable2 R → ∀d. d_liftable2 (llstar … R d). +lemma d2_liftable_sn_llstar: ∀R. d_liftable2_sn R → ∀d. d_liftable2_sn (llstar … R d). #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2 [ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/ | #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma index 6f0cef9d0..31f416f12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma @@ -41,9 +41,9 @@ interpretation "uniform relocation (term)" interpretation "generic relocation (term)" 'RLiftStar f T1 T2 = (lifts f T1 T2). -definition liftable2: predicate (relation term) ≝ - λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → - ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2. +definition liftable2_sn: predicate (relation term) ≝ + λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → + ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2. definition deliftable2_sn: predicate (relation term) ≝ λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma index 381c1c96c..d3fa65354 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma @@ -117,7 +117,7 @@ lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 /3 width=6 by lifts_conf, lifts_fwd_isid/ qed-. -lemma liftable2_sn_bi: ∀R. liftable2 R → liftable2_bi R. +lemma liftable2_sn_bi: ∀R. liftable2_sn R → liftable2_bi R. #R #HR #T1 #T2 #HT12 #f #U1 #HTU1 #U2 #HTU2 elim (HR … HT12 … HTU1) -HR -T1 #X #HTX #HUX <(lifts_mono … HTX … HTU2) -T2 -U2 -f // diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma index e581cc538..828ee58a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma @@ -19,7 +19,7 @@ include "basic_2/relocation/lifts_lifts.ma". (* Properties with degree-based equivalence for terms ***********************) -lemma tdeq_lifts: ∀h,o. liftable2 (tdeq h o). +lemma tdeq_lifts_sn: ∀h,o. liftable2_sn (tdeq h o). #h #o #T1 #T2 #H elim H -T1 -T2 [||| * ] [ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort1 … H) -H /3 width=5 by lifts_sort, tdeq_sort, ex2_intro/ @@ -39,11 +39,11 @@ lemma tdeq_lifts: ∀h,o. liftable2 (tdeq h o). qed-. lemma tdeq_lifts_bi: ∀h,o. liftable2_bi (tdeq h o). -/3 width=6 by tdeq_lifts, liftable2_sn_bi/ qed-. +/3 width=6 by tdeq_lifts_sn, liftable2_sn_bi/ qed-. (* Inversion lemmas with degree-based equivalence for terms *****************) -lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o). +lemma tdeq_inv_lifts_sn: ∀h,o. deliftable2_sn (tdeq h o). #h #o #U1 #U2 #H elim H -U1 -U2 [||| * ] [ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort2 … H) -H /3 width=5 by lifts_sort, tdeq_sort, ex2_intro/ @@ -63,4 +63,4 @@ lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o). qed-. lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o). -/3 width=6 by tdeq_inv_lifts, deliftable2_sn_bi/ qed-. +/3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma index 08eed1481..99a6e3670 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -25,11 +25,8 @@ lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 → #h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2 [ /3 width=3 by cpx_cpxs, cpx_delta/ | #V #V2 #_ #HV2 #IH #W2 #HVW2 - elim (lifts_total V (𝐔❴1❵)) #W #HVW - elim (cpx_lifts … HV2 (Ⓣ) … (K.ⓑ{I}V1) … HVW) -HV2 - [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ - | /3 width=1 by drops_refl, drops_drop/ - ] + elim (lifts_total V (𝐔❴1❵)) + /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/ ] qed. @@ -38,11 +35,8 @@ lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T → #h #I #G #K #V #T #i #H @(cpxs_ind … H) -T [ /3 width=3 by cpx_cpxs, cpx_lref/ | #T0 #T #_ #HT2 #IH #U #HTU - elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 - elim (cpx_lifts … HT2 (Ⓣ) … (K.ⓑ{I}V) … HTU0) -HT2 - [ #X #HTX <(lifts_mono … HTU … HTX) -T -X /3 width=3 by cpxs_strap1/ - | /3 width=1 by drops_refl, drops_drop/ - ] + elim (lifts_total T0 (𝐔❴1❵)) + /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/ ] qed. @@ -53,11 +47,8 @@ lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i. #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/ | #V #V2 #_ #HV2 #IH #W2 #HVW2 - elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW - elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2 - [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ - | /2 width=3 by drops_isuni_fwd_drop2/ - ] + elim (lifts_total V (𝐔❴⫯i❵)) + /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/ ] qed. @@ -73,7 +64,7 @@ lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 → elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/ * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ | * #I #K #V1 #T1 #HVT1 #HT1 #H destruct - elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T + elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/ ] qed-. @@ -87,7 +78,7 @@ lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈*[h] T2 → elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ | * #I #K #V1 #T1 #Hi #HT1 #H destruct - elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T + elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/ ] qed-. @@ -104,7 +95,7 @@ lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 → * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ | * #I #K #V1 #T1 #HLK #HVT1 #HT1 lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK - elim (cpx_inv_lifts … HT2 … H0LK … HT1) -H0LK -T + elim (cpx_inv_lifts_sn … HT2 … H0LK … HT1) -H0LK -T /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ ] qed-. @@ -112,11 +103,17 @@ qed-. (* Properties with generic relocation ***************************************) (* Basic_2A1: includes: cpxs_lift *) -lemma cpxs_lifts: ∀h,G. d_liftable2 (cpxs h G). -/3 width=10 by cpx_lifts, cpxs_strap1, d2_liftable_LTC/ qed-. +lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn (cpxs h G). +/3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_LTC/ qed-. + +lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi (cpxs h G). +/3 width=9 by cpxs_lifts_sn, d_liftable2_sn_bi/ qed-. (* Inversion lemmas with generic relocation *********************************) (* Basic_2A1: includes: cpxs_inv_lift1 *) -lemma cpxs_inv_lifts: ∀h,G. d_deliftable2_sn (cpxs h G). -/3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts/ qed-. +lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpxs h G). +/3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts_sn/ qed-. + +lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpxs h G). +/3 width=9 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma index d8a6f77a3..8a52882a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma @@ -40,8 +40,7 @@ lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/ * #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct -elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_isuni_fwd_drop2/ #X #H -<(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/ +/4 width=9 by cpxs_lifts_bi, drops_isuni_fwd_drop2, or_intror/ qed-. (* Basic_1: was just: pr3_iso_beta *) @@ -78,12 +77,10 @@ elim (cpxs_inv_appl1 … H) -H * @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V5 #T5 #HV5 #HT5 #H destruct - elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV) … HV12) -V1 /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV34 … H) -V3 -X /3 width=1 by cpxs_flat, cpxs_bind/ + /6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/ | #X #HT1 #H #H0 destruct elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct - elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV0) … HV12) -HV13 /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV34 … H) -V3 -X #HV24 + lapply (cpxs_lifts_bi … HV13 (Ⓣ) … (L.ⓓV0) … HV12 … HV34) -V3 /3 width=1 by drops_refl, drops_drop/ #HV24 @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5 @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma index 4d7cf8baf..bab5c447e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma @@ -129,13 +129,11 @@ elim (cpxs_inv_appl1 … H) -H * @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V1 #T1 #HV1 #HT1 #H destruct - elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV) … HV12a) -V1a /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV0a … H) -V0a -X #HV2a + lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a @(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ | #X #HT1 #H #H0 destruct elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct - elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV0) … HV12a) /3 width=1 by drops_refl, drops_drop/ #X #H - <(lifts_mono … HV0a … H) -V0a -X #HV2a + lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV0) … HV12a … HV0a) -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b @(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1 @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ 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 1b4c9cb52..ae3d9a889 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 @@ -58,11 +58,12 @@ elim (tdeq_dec h o T1 T0) #H ] qed-. -lemma csx_ind_alt: ∀h,o,G,L. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. +(* Basic_2A1: was: csx_ind_alt *) +lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. #h #o #G #L #R #IH #T #HT @(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma index f934707bb..2a1981169 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma @@ -26,7 +26,7 @@ lemma csx_lifts: ∀h,o,G. d_liftable1 … (csx h o G). #h #o #G #K #T #H @(csx_ind … H) -T #T1 #_ #IH #b #f #L #HLK #U1 #HTU1 @csx_intro #U2 #HU12 #HnU12 -elim (cpx_inv_lifts … HU12 … HLK … HTU1) -HU12 +elim (cpx_inv_lifts_sn … HU12 … HLK … HTU1) -HU12 /4 width=7 by tdeq_lifts_bi/ qed-. @@ -38,6 +38,6 @@ lemma csx_inv_lifts: ∀h,o,G. d_deliftable1 … (csx h o G). #h #o #G #L #U #H @(csx_ind … H) -U #U1 #_ #IH #b #f #K #HLK #T1 #HTU1 @csx_intro #T2 #HT12 #HnT12 -elim (cpx_lifts … HT12 … HLK … HTU1) -HT12 +elim (cpx_lifts_sn … HT12 … HLK … HTU1) -HT12 /4 width=7 by tdeq_inv_lifts_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma new file mode 100644 index 000000000..47d066ab6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma @@ -0,0 +1,102 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpxs_lfpx.ma". +include "basic_2/rt_computation/csx_drops.ma". +include "basic_2/rt_computation/csx_cpxs.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was just: csx_lpx_conf *) +lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → + ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. +#h #o #G #L1 #T #H @(csx_ind_cpxs … H) -T +/5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_conf/ +qed-. + +lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ → + ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄. +#h #o #p #G #L #W #HW @(csx_ind … HW) -W +#W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 +elim (cpx_inv_abst1 … H1) -H1 +#W0 #T0 #HLW0 #HLT0 #H destruct +elim (tdneq_inv_pair … H2) -H2 +[ #H elim H -H // +| -IHT #H lapply (csx_cpx_trans … o … HLT0) // -HT + #HT0 lapply (csx_lfpx_conf … HT0 … (L.ⓛW0)) -HT0 /4 width=1 by lfpx_pair/ +| -IHW -HT /4 width=3 by csx_cpx_trans, cpx_pair_sn/ +] +qed. + +lemma csx_abbr: ∀h,o,p,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → + ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.T⦄. +#h #o #p #G #L #V #HV @(csx_ind … HV) -V +#V #_ #IHV #T #HT @(csx_ind_cpxs … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 +elim (cpx_inv_abbr1 … H1) -H1 * +[ #V1 #T1 #HLV1 #HLT1 #H destruct + elim (tdneq_inv_pair … H2) -H2 + [ #H elim H -H // + | /4 width=3 by csx_cpx_trans, csx_lfpx_conf, lfpx_pair/ + | -IHV /4 width=3 by csx_cpx_trans, cpx_cpxs, cpx_pair_sn/ + ] +| -IHV -IHT -H2 + /4 width=7 by csx_cpx_trans, csx_inv_lifts, drops_drop, drops_refl/ +] +qed. + +fact csx_appl_theta_aux: ∀h,o,p,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≡ V2 → + ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄. +#h #o #p #G #L #X #H @(csx_ind_cpxs … H) -X +#X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +lapply (csx_fwd_pair_sn … HVT) #HV +lapply (csx_fwd_bind_dx … HVT) -HVT #HVT +@csx_intro #X #HL #H +elim (cpx_inv_appl1 … HL) -HL * +[ -HV #V0 #Y #HLV10 #HL #H0 destruct + elim (cpx_inv_abbr1 … HL) -HL * + [ #V3 #T3 #HV3 #HLT3 #H0 destruct + elim (lift_total V0 0 1) #V4 #HV04 + elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) + [ -IHVT #H0 destruct + elim (eq_false_inv_tpair_sn … H) -H + [ -HLV10 -HV3 -HLT3 -HVT + >(lift_inj … HV12 … HV04) -V4 + #H elim H // + | * #_ #H elim H // + ] + | -H -HVT #H + lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓕ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by drop_drop/ #HV24 + @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ + ] + | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct + lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 + lapply (csx_inv_lift … L … (Ⓕ) … 1 HVT0 ? ? ?) -HVT0 + /3 width=5 by csx_cpx_trans, cpx_pair_sn, drop_drop, lift_flat/ + ] +| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct +| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct + lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by drop_drop/ #HLV23 + @csx_abbr /2 width=3 by csx_cpx_trans/ -HV + @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1 + /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/ +] +qed-. + +lemma csx_appl_theta: ∀h,o,a,V1,V2. ⬆[0, 1] V1 ≡ V2 → + ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] ⓐV1.ⓓ{a}V.T. +/2 width=5 by csx_appl_theta_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma deleted file mode 100644 index 8caea5831..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma +++ /dev/null @@ -1,117 +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/computation/cpxs_cpxs.ma". -include "basic_2/computation/csx_alt.ma". -include "basic_2/computation/csx_lift.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* Advanced properties ******************************************************) - -lemma csx_lpx_conf: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → - ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, o] T → ⦃G, L2⦄ ⊢ ⬊*[h, o] T. -#h #o #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T -/4 width=3 by csx_intro, lpx_cpx_trans/ -qed-. - -lemma csx_abst: ∀h,o,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, o] W → - ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓛ{a}W.T. -#h #o #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_abst1 … H1) -H1 -#W0 #T0 #HLW0 #HLT0 #H destruct -elim (eq_false_inv_tpair_sn … H2) -H2 -[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT - #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/ -| -IHW -HLW0 -HT * #H destruct /3 width=1 by/ -] -qed. - -lemma csx_abbr: ∀h,o,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, o] V → - ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V. T. -#h #o #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_abbr1 … H1) -H1 * -[ #V1 #T1 #HLV1 #HLT1 #H destruct - elim (eq_false_inv_tpair_sn … H2) -H2 - [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/ - | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/ - ] -| -IHV -IHT -H2 - /3 width=8 by csx_cpx_trans, csx_inv_lift, drop_drop/ -] -qed. - -fact csx_appl_beta_aux: ∀h,o,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, o] U1 → - ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV.ⓛ{a}W.T1. -#h #o #a #G #L #X #H @(csx_ind … H) -X -#X #HT1 #IHT1 #V #W #T1 #H1 destruct -@csx_intro #X #H1 #H2 -elim (cpx_inv_appl1 … H1) -H1 * -[ -HT1 #V0 #Y #HLV0 #H #H0 destruct - elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct - @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2 - lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_beta/ -| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct - lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 - /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_beta/ -| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct -] -qed-. - -(* Basic_1: was just: sn3_beta *) -lemma csx_appl_beta: ∀h,o,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV.ⓛ{a}W.T. -/2 width=3 by csx_appl_beta_aux/ qed. - -fact csx_appl_theta_aux: ∀h,o,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, o] U → ∀V1,V2. ⬆[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV1.ⓓ{a}V.T. -#h #o #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csx_fwd_pair_sn … HVT) #HV -lapply (csx_fwd_bind_dx … HVT) -HVT #HVT -@csx_intro #X #HL #H -elim (cpx_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpx_inv_abbr1 … HL) -HL * - [ #V3 #T3 #HV3 #HLT3 #H0 destruct - elim (lift_total V0 0 1) #V4 #HV04 - elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV04) -V4 - #H elim H // - | * #_ #H elim H // - ] - | -H -HVT #H - lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓕ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by drop_drop/ #HV24 - @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ - ] - | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 - lapply (csx_inv_lift … L … (Ⓕ) … 1 HVT0 ? ? ?) -HVT0 - /3 width=5 by csx_cpx_trans, cpx_pair_sn, drop_drop, lift_flat/ - ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct -| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct - lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by drop_drop/ #HLV23 - @csx_abbr /2 width=3 by csx_cpx_trans/ -HV - @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1 - /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/ -] -qed-. - -lemma csx_appl_theta: ∀h,o,a,V1,V2. ⬆[0, 1] V1 ≡ V2 → - ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV1.ⓓ{a}V.T. -/2 width=5 by csx_appl_theta_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma new file mode 100644 index 000000000..00683b0fc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx_lsubr.ma". +include "basic_2/rt_computation/csx_csx.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Advanced properties ******************************************************) + +fact csx_appl_beta_aux: ∀h,o,p,G,L,U1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U1⦄ → + ∀V,W,T1. U1 = ⓓ{p}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.ⓛ{p}W.T1⦄. +#h #o #p #G #L #X #H @(csx_ind … H) -X +#X #HT1 #IHT1 #V #W #T1 #H1 destruct +@csx_intro #X #H1 #H2 +elim (cpx_inv_appl1 … H1) -H1 * +[ -HT1 #V0 #Y #HLV0 #H #H0 destruct + elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct + @IHT1 -IHT1 [4: // | skip ] + [ lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 -H2 + /3 width=1 by cpx_bind, cpx_flat, lsubr_beta/ + | #H elim (tdeq_inv_pair … H) -H + #_ #H elim (tdeq_inv_pair … H) -H + #_ /4 width=1 by tdeq_pair/ + ] +| -IHT1 -H2 #q #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct + lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 + /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_beta/ +| -HT1 -IHT1 -H2 #q #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: was just: sn3_beta *) +lemma csx_appl_beta: ∀h,o,p,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.ⓛ{p}W.T⦄. +/2 width=3 by csx_appl_beta_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma index e565bdc67..e5e5ea562 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma @@ -72,7 +72,7 @@ lemma cpxs_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 /4 width=3 by lfpxs_pair, cpxs_trans, ex3_intro, or_intror/ ] | #U1 #HTU1 #HU01 - elim (cpx_lifts … HU02 (Ⓣ) … (L.ⓓV1) … HU01) + elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01) /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 5136af26a..4a6887490 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma -csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma index 1dcbdf2a4..21a642e5a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma @@ -28,10 +28,8 @@ qed. (* Basic_2A1: includes: cnx_lift *) lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G). #h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H -elim (cpx_inv_lifts … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 -lapply (HT … HT0) -G -K #HT0 -elim (tdeq_lifts … HT0 … HTU) -T #X #HX #HU -<(lifts_mono … HX … HTU0) -T0 // +elim (cpx_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 +lapply (HT … HT0) -G -K /2 width=6 by tdeq_lifts_bi/ qed-. (* Inversion lemmas with generic slicing ************************************) @@ -48,8 +46,6 @@ qed-. (* Basic_2A1: includes: cnx_inv_lift *) lemma cnx_inv_lifts: ∀h,o,G. d_deliftable1 … (cnx h o G). #h #o #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H -elim (cpx_lifts … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 -lapply (HU … HU0) -G -L #HU0 -elim (tdeq_inv_lifts … HU0 … HTU) -U #X #HX #HT -<(lifts_inj … HX … HTU0) -U0 // +elim (cpx_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 +lapply (HU … HU0) -G -L /2 width=6 by tdeq_inv_lifts_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index 6c9fdfd22..758a278b7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -81,7 +81,7 @@ qed-. (* Properties with generic slicing for local environments *******************) (* Note: it should use drops_split_trans_pair2 *) -lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G). +lemma cpg_lifts_sn: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2_sn (cpg Rt h c G). #Rt #HRt #c #h #G #K #T generalize in match c; -c @(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * * [ #s #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct -IH @@ -158,9 +158,12 @@ lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G ] qed-. +lemma cpg_lifts_bi: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2_bi (cpg Rt h c G). +/3 width=9 by cpg_lifts_sn, d_liftable2_sn_bi/ qed-. + (* Inversion lemmas with generic slicing for local environments *************) -lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G). +lemma cpg_inv_lifts_sn: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G). #Rt #HRt #c #h #G #L #U generalize in match c; -c @(fqup_wf_ind_eq … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * * [ #s #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct -IH @@ -232,3 +235,6 @@ lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cp ] ] qed-. + +lemma cpg_inv_lifts_bi: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_bi (cpg Rt h c G). +/3 width=9 by cpg_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma index fbcd7958d..790970db3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma @@ -78,18 +78,24 @@ qed-. (* Basic_1: includes: pr0_lift pr2_lift *) (* Basic_2A1: includes: cpr_lift *) -lemma cpm_lifts: ∀n,h,G. d_liftable2 (cpm n h G). +lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn (cpm n h G). #n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1 -elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1 +elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1 /3 width=5 by ex2_intro/ qed-. +lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi (cpm n h G). +/3 width=9 by cpm_lifts_sn, d_liftable2_sn_bi/ qed-. + (* Inversion lemmas with generic slicing for local environments *************) (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *) (* Basic_2A1: includes: cpr_inv_lift1 *) -lemma cpm_inv_lifts1: ∀n,h,G. d_deliftable2_sn (cpm n h G). +lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn (cpm n h G). #n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1 -elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1 +elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1 /3 width=5 by ex2_intro/ qed-. + +lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi (cpm n h G). +/3 width=9 by cpm_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma index fe9afa3a8..0d7a97a69 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma @@ -51,17 +51,23 @@ qed-. (* Properties with generic slicing for local environments *******************) (* Basic_2A1: includes: cpx_lift *) -lemma cpx_lifts: ∀h,G. d_liftable2 (cpx h G). +lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn (cpx h G). #h #G #K #T1 #T2 * #cT #HT12 #b #f #L #HLK #U1 #HTU1 -elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1 +elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1 /3 width=4 by ex2_intro, ex_intro/ qed-. +lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi (cpx h G). +/3 width=9 by cpx_lifts_sn, d_liftable2_sn_bi/ qed-. + (* Inversion lemmas with generic slicing for local environments *************) (* Basic_2A1: includes: cpx_inv_lift1 *) -lemma cpx_inv_lifts: ∀h,G. d_deliftable2_sn (cpx h G). +lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpx h G). #h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1 -elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1 +elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1 /3 width=4 by ex2_intro, ex_intro/ qed-. + +lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpx h G). +/3 width=9 by cpx_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 8bc29f301..453d2b5e1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -29,7 +29,7 @@ lemma fqu_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2 elim (lifts_total X2 (𝐔❴1❵)) /3 width=3 by fqu_drop, cpx_delta, ex2_intro/ | #I #G #L2 #V #T2 #X2 #HTX2 #U2 #HTU2 - elim (cpx_lifts … HTU2 (Ⓣ) … (L2.ⓑ{I}V) … HTX2) + elim (cpx_lifts_sn … HTU2 (Ⓣ) … (L2.ⓑ{I}V) … HTX2) /3 width=3 by fqu_drop, drops_refl, drops_drop, ex2_intro/ ] qed-. @@ -87,12 +87,8 @@ lemma fqu_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ ] | #I #G #L #V #T1 #U1 #HTU1 #T2 #HT12 #H0 - elim (cpx_lifts … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 /3 width=1 by drops_refl, drops_drop/ - #U2 #HTU2 #HU12 @(ex3_intro … U2) - [1,3: /3 width=1 by fqu_drop/ - | #H elim (tdeq_inv_lifts … H … HTU1) -U1 - #X2 #H <(lifts_inj … HTU2 … H) -U2 /2 width=1 by/ - ] + elim (cpx_lifts_sn … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 + /4 width=6 by fqu_drop, drops_refl, drops_drop, tdeq_inv_lifts_bi, ex3_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma index 3156e7252..7d23f3b0f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma @@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpr.ma". (* Properties with generic slicing for local environments *******************) lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G). -/3 width=6 by lfxs_liftable_dedropable, cpm_lifts/ qed-. +/3 width=6 by lfxs_liftable_dedropable_sn, cpm_lifts_sn/ qed-. (* Inversion lemmas with generic slicing for local environments *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma index 4fdd21f9e..66d9580db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma @@ -26,7 +26,7 @@ lemma fqu_cpr_trans_dx: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/ -#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts … HU2 (Ⓣ) … HUT) -U +#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U /3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ qed-. @@ -35,7 +35,7 @@ lemma fqu_cpr_trans_sn: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/ -#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts … HU2 (Ⓣ) … HUT) -U +#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U /3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index d05584ebf..7c6c22237 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -45,10 +45,11 @@ elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_ lapply (drops_isuni_fwd_drop2 … HLK2) // -W2 #HLK2 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 -elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2 +elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 /3 width=6 by cpm_delta_drops, ex2_intro/ qed-. +(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *) fact cpr_conf_lfpr_delta_delta: ∀h,G,L0,i. ( ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → @@ -71,8 +72,8 @@ elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_ lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 -elim (cpm_lifts … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1 -elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2 +elim (cpm_lifts_sn … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1 +elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2 lapply (lifts_mono … HX … HVT) #H destruct /2 width=3 by ex2_intro/ qed-. @@ -113,9 +114,10 @@ fact cpr_conf_lfpr_bind_zeta: elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0 elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -T0 #T #HT1 #HT2 -elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/ +elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/ qed-. +(* Note: we don't use cpm_inv_lifts_bi to preserve visual symmetry *) fact cpr_conf_lfpr_zeta_zeta: ∀h,G,L0,V0,T0. ( ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → @@ -132,8 +134,8 @@ fact cpr_conf_lfpr_zeta_zeta: elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -T0 #T #HT1 #HT2 -elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1 -elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2 +elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1 +elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2 lapply (lifts_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/ qed-. @@ -234,7 +236,7 @@ elim (lfpr_inv_bind … HL01) -HL01 #H1W0 #H1T0 elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02 elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 -elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2 +elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2 elim (cpm_inv_abbr1 … H) -H * [ #W1 #T1 #HW01 #HT01 #H destruct elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/ @@ -242,7 +244,7 @@ elim (cpm_inv_abbr1 … H) -H * /4 width=7 by cpm_bind, cpr_flat, cpm_theta, ex2_intro/ | #T1 #HT01 #HXT1 #H destruct elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 - elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -HXT1 + elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -HXT1 /4 width=9 by cpr_flat, cpm_zeta, drops_refl, drops_drop, lifts_flat, ex2_intro/ ] qed-. @@ -272,6 +274,7 @@ lapply (lsubr_cpm_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_bet /4 width=5 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. +(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *) fact cpr_conf_lfpr_theta_theta: ∀h,p,G,L0,V0,W0,T0. ( ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → @@ -294,8 +297,8 @@ elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 -elim (cpm_lifts … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU -elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX +elim (cpm_lifts_sn … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU +elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX lapply (lifts_mono … HX … HVU) -HX #H destruct /4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma index 086e71e87..d49e4e01d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma @@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpx.ma". (* Properties with generic slicing for local environments *******************) lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G). -/3 width=6 by lfxs_liftable_dedropable, cpx_lifts/ qed-. +/3 width=6 by lfxs_liftable_dedropable_sn, cpx_lifts_sn/ qed-. (* Inversion lemmas with generic slicing for local environments *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 47b09be86..7af823975 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -32,13 +32,13 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (lfpx_inv_zero_pair_sn … H1) -H1 #K1 #X1 #HK01 #HX1 #H destruct elim (lfdeq_inv_zero_pair_sn … H2) -H2 #K2 #X2 #HK02 #HX2 #H destruct elim (IH X2 … HK01 … HK02) // -K0 -V0 #V #HV1 #HV2 - elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/ + elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/ | #I #G #K0 #V0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2 >(tdeq_inv_lref1 … H0) -H0 elim (lfpx_inv_lref_pair_sn … H1) -H1 #K1 #X1 #HK01 #H destruct elim (lfdeq_inv_lref_pair_sn … H2) -H2 #K2 #X2 #HK02 #H destruct elim (IH … HK01 … HK02) [|*: //] -K0 -V0 #V #HV1 #HV2 - elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/ + elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/ | #p #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2 elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct elim (lfpx_inv_bind … H1) -H1 #HL01 #H1 @@ -60,7 +60,7 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2 lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 -HV02 #H2 elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1 - elim (tdeq_inv_lifts … HT1 … HUT1) -T1 + elim (tdeq_inv_lifts_sn … HT1 … HUT1) -T1 /3 width=5 by cpx_zeta, ex2_intro/ | #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2 elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #_ #HT02 #H destruct @@ -97,7 +97,7 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 #V #HV1 elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0 elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0 - elim (tdeq_lifts … HV1 … HVU1) -V1 + elim (tdeq_lifts_sn … HV1 … HVU1) -V1 /4 width=9 by cpx_theta, tdeq_pair, ex2_intro/ (* note: 2 tdeq_pair *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma index 93b9ccfa1..38463c2fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma @@ -21,13 +21,13 @@ include "basic_2/static/lfdeq_fqup.ma". (* Properties with generic slicing for local environments *******************) (* Basic_2A1: includes: lleq_lift_le lleq_lift_ge *) -lemma lfdeq_lifts: ∀h,o. dedropable_sn (cdeq h o). -/3 width=5 by lfxs_liftable_dedropable, tdeq_lifts/ qed-. +lemma lfdeq_lifts_sn: ∀h,o. dedropable_sn (cdeq h o). +/3 width=5 by lfxs_liftable_dedropable_sn, tdeq_lifts_sn/ qed-. (* Inversion lemmas with generic slicing for local environments *************) (* Basic_2A1: restricts: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) -lemma lfdeq_inv_lifts: ∀h,o. dropable_sn (cdeq h o). +lemma lfdeq_inv_lifts_sn: ∀h,o. dropable_sn (cdeq h o). /2 width=5 by lfxs_dropable_sn/ qed-. (* Note: missing in basic_2A1 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma index 280ab796a..5a6024a84 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma @@ -36,7 +36,7 @@ lemma fqu_tdeq_conf: ∀h,o,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, T elim (tdeq_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct /2 width=5 by fqu_flat_dx, ex3_2_intro/ | #I #G #L #W #T1 #U1 #HTU1 #U2 #HU12 - elim (tdeq_inv_lifts … HU12 … HTU1) -U1 #T2 #HTU2 #HT12 + elim (tdeq_inv_lifts_sn … HU12 … HTU1) -U1 #T2 #HTU2 #HT12 /3 width=5 by fqu_drop, ex3_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 9875361f7..b39c11f95 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -37,13 +37,13 @@ definition dropable_dx: predicate (relation3 lenv term term) ≝ (* Properties with generic slicing for local environments *******************) (* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *) -lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - d_liftable2 R → dedropable_sn R. +lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) → + d_liftable2_sn R → dedropable_sn R. #R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU elim (frees_total L1 U) #f2 #Hf2 lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf -elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1 -/3 width=6 by cfull_lift, ex3_intro, ex2_intro/ +elim (lexs_liftable_co_dedropable_sn … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1 +/3 width=6 by cfull_lift_sn, ex3_intro, ex2_intro/ qed-. (* Inversion lemmas with generic slicing for local environments *************) 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 efb95c8e3..05b42b27d 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 @@ -114,7 +114,7 @@ table { [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } -- 2.39.2