From 0fea4ed429678c3293027cfe76fdbe15cfa331cb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 31 Aug 2019 22:01:18 +0200 Subject: [PATCH] update in static_2 and basic_2 + a weaker version of tueq reintroduced + some renaming + one conjecture to prove --- .../lambdadelta/basic_2/dynamic/cnv_cpce.ma | 13 +- .../dynamic/{cnv_cpmhe.ma => cnv_cpmuwe.ma} | 29 +- .../lambdadelta/basic_2/dynamic/cnv_eval.ma | 25 +- .../lambdadelta/basic_2/dynamic/nta_cpms.ma | 1 - .../{predevalstar_6.ma => predevalwstar_6.ma} | 4 +- .../notation/relations/preditnormal_4.ma | 2 +- .../basic_2/rt_computation/cnuw.ma | 131 ++++++++ .../basic_2/rt_computation/cnuw_cnuw.ma | 51 ++++ .../cnuw_drops.ma} | 64 ++-- .../basic_2/rt_computation/cnuw_simple.ma | 45 +++ .../cnuw_tdeq.ma} | 36 ++- .../rt_computation/{cpmhe.ma => cpmuwe.ma} | 59 ++-- .../cpmuwe_cpmuwe.ma} | 20 +- .../{cpmhe_csx.ma => cpmuwe_csx.ma} | 22 +- .../{cpms_cnh.ma => cprs_tweq.ma} | 25 +- .../{cpxs_theq.ma => cpxs_toeq.ma} | 46 +-- ...pxs_theq_vector.ma => cpxs_toeq_vector.ma} | 80 ++--- .../basic_2/rt_computation/csx_cnx_vector.ma | 14 +- .../basic_2/rt_computation/csx_csx_vector.ma | 12 +- ...{csx_simple_theq.ma => csx_simple_toeq.ma} | 17 +- .../lambdadelta/basic_2/rt_transition/cnh.ma | 75 ----- .../basic_2/rt_transition/cnh_lifts.ma | 32 -- .../basic_2/rt_transition/cpr_tdeq.ma | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 22 +- .../relations/approxeq_2.ma} | 0 .../{lifts_theq.ma => lifts_toeq.ma} | 72 +++-- .../static_2/relocation/lifts_tweq.ma | 105 +++++++ .../static_2/syntax/{theq.ma => toeq.ma} | 78 ++--- .../syntax/{theq_simple.ma => toeq_simple.ma} | 10 +- ...simple_vector.ma => toeq_simple_vector.ma} | 8 +- .../syntax/{theq_tdeq.ma => toeq_tdeq.ma} | 8 +- .../syntax/{theq_theq.ma => toeq_toeq.ma} | 22 +- .../lambdadelta/static_2/syntax/tweq.ma | 288 ++++++++++++++++++ .../syntax/tweq_simple.ma} | 21 +- .../lambdadelta/static_2/syntax/tweq_tweq.ma | 51 ++++ .../lambdadelta/static_2/web/static_2_src.tbl | 10 +- 36 files changed, 1054 insertions(+), 448 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{cnv_cpmhe.ma => cnv_cpmuwe.ma} (65%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predevalstar_6.ma => predevalwstar_6.ma} (89%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition/cnh_drops.ma => rt_computation/cnuw_drops.ma} (54%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition/cnh_tdeq.ma => rt_computation/cnuw_tdeq.ma} (75%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpmhe.ma => cpmuwe.ma} (51%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition/cnh_simple.ma => rt_computation/cpmuwe_cpmuwe.ma} (63%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpmhe_csx.ma => cpmuwe_csx.ma} (72%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpms_cnh.ma => cprs_tweq.ma} (56%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_theq.ma => cpxs_toeq.ma} (70%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_theq_vector.ma => cpxs_toeq_vector.ma} (71%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{csx_simple_theq.ma => csx_simple_toeq.ma} (74%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_lifts.ma rename matita/matita/contribs/lambdadelta/static_2/{etc/tueq/approxeq_2.etc => notation/relations/approxeq_2.ma} (100%) rename matita/matita/contribs/lambdadelta/static_2/relocation/{lifts_theq.ma => lifts_toeq.ma} (50%) create mode 100644 matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma rename matita/matita/contribs/lambdadelta/static_2/syntax/{theq.ma => toeq.ma} (64%) rename matita/matita/contribs/lambdadelta/static_2/syntax/{theq_simple.ma => toeq_simple.ma} (83%) rename matita/matita/contribs/lambdadelta/static_2/syntax/{theq_simple_vector.ma => toeq_simple_vector.ma} (87%) rename matita/matita/contribs/lambdadelta/static_2/syntax/{theq_tdeq.ma => toeq_tdeq.ma} (84%) rename matita/matita/contribs/lambdadelta/static_2/syntax/{theq_theq.ma => toeq_toeq.ma} (71%) create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma rename matita/matita/contribs/lambdadelta/{basic_2/rt_transition/cnh_cnh.ma => static_2/syntax/tweq_simple.ma} (70%) create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tweq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma index 4b6cb48d3..792c48f05 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) +include "basic_2/rt_computation/cpmuwe_cpmuwe.ma". include "basic_2/rt_conversion/cpce_drops.ma". -include "basic_2/dynamic/cnv_cpmhe.ma". +include "basic_2/dynamic/cnv_cpmuwe.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -31,10 +32,10 @@ generalize in match HT1; -HT1 elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ] [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W - elim (cpmhe_total_csx … H1W) -H1W #X #n #HWX + elim (cpmuwe_total_csx … H1W) -H1W #X #n #HWX elim (abst_dec X) [ * | -IH ] [ #p #V1 #U #H destruct - lapply (cpmhe_fwd_cpms … HWX) -HWX #HWX + lapply (cpmuwe_fwd_cpms … HWX) -HWX #HWX elim (IH G K V1) -IH [ #V2 #HV12 elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2 @@ -46,9 +47,9 @@ generalize in match HT1; -HT1 @(ex_intro … (#i)) @cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0 lapply (drops_mono … HLK0 … HLK) -i -L #H destruct - lapply (cpmhe_abst … HWU0) -HWU0 #HWU0 - elim (cnv_cpmhe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W - elim (theq_inv_pair1 … H) -V0 -U0 #V0 #U0 #H destruct + lapply (cpmuwe_abst … HWU0) -HWU0 #HWU0 + elim (cnv_cpmuwe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W + elim (tweq_inv_abst_sn … H) -V0 -U0 #V0 #U0 #H destruct /2 width=4 by/ ] | /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmhe.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma similarity index 65% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmhe.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma index 3826ae653..011388942 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmhe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/cpms_cnh.ma". -include "basic_2/rt_computation/cpmhe_csx.ma". +include "basic_2/rt_computation/cpmuwe_csx.ma". include "basic_2/rt_equivalence/cpes.ma". include "basic_2/dynamic/cnv_preserve.ma". @@ -21,25 +20,25 @@ include "basic_2/dynamic/cnv_preserve.ma". (* Properties with head evaluation for t-bound rt-transition on terms *******) -lemma cnv_cpmhe_trans (a) (h) (G) (L): +lemma cnv_cpmuwe_trans (a) (h) (G) (L): ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → - ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h]. -/3 width=4 by cpmhe_fwd_cpms, cnv_cpms_trans/ qed-. + ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +/3 width=4 by cpmuwe_fwd_cpms, cnv_cpms_trans/ qed-. -lemma cnv_R_cpmhe_total (a) (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmhe h G L T1 n. -/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmhe_total_csx/ qed-. +lemma cnv_R_cpmuwe_total (a) (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmuwe h G L T1 n. +/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmuwe_total_csx/ qed-. -axiom cnv_R_cpmhe_dec (a) (h) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmhe h G L T n). +axiom cnv_R_cpmuwe_dec (a) (h) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmuwe h G L T n). (* Main inversions with head evaluation for t-bound rt-transition on terms **) -theorem cnv_cpmhe_mono (a) (h) (G) (L): - ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*[h,n1] 𝐍*⦃T1⦄ → - ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*[h,n2] 𝐍*⦃T2⦄ → - ∧∧ ⦃G,L⦄ ⊢ T1 ⬌*[h,n2-n1,n1-n2] T2 & T1 ⩳ T2. +theorem cnv_cpmuwe_mono (a) (h) (G) (L): + ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n1] T1 → + ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n2] T2 → + ∧∧ ⦃G,L⦄ ⊢ T1 ⬌*[h,n2-n1,n1-n2] T2 & T1 ≅ T2. #a #h #G #L #T0 #HT0 #T1 #n1 * #HT01 #HT1 #T2 #n2 * #HT02 #HT2 elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20 -/4 width=8 by cpms_div, cpms_inv_cnh_sn, theq_canc_dx, conj/ +/4 width=4 by cpms_div, tweq_canc_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma index e7f16039e..9d86f579d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) +include "basic_2/rt_computation/cpmuwe_cpmuwe.ma". include "basic_2/rt_equivalence/cpes_cpes.ma". -include "basic_2/dynamic/cnv_cpmhe.ma". +include "basic_2/dynamic/cnv_cpmuwe.ma". include "basic_2/dynamic/cnv_cpes.ma". include "basic_2/dynamic/cnv_preserve_cpes.ma". @@ -50,34 +51,34 @@ theorem cnv_dec (a) (h) (G) (L) (T): ac_props a → elim (IH G L V) [| -IH #HV | // ] [ elim (IH G L T) -IH [| #HT #HV | // ] [ #HT #HV - elim (cnv_R_cpmhe_total … HT) #n #Hn - elim (dec_min (R_cpmhe h G L T) … Hn) -Hn - [| /2 width=2 by cnv_R_cpmhe_dec/ ] #n0 #_ -n + elim (cnv_R_cpmuwe_total … HT) #n #Hn + elim (dec_min (R_cpmuwe h G L T) … Hn) -Hn + [| /2 width=2 by cnv_R_cpmuwe_dec/ ] #n0 #_ -n elim (ac_dec … Ha n0) -Ha [ * #n #Hn #Ha * #X0 #HX0 #_ elim (abst_dec X0) [ * #p #W #U0 #H destruct elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] - [ lapply (cpmhe_fwd_cpms … HX0) -HX0 #HTU0 + [ lapply (cpmuwe_fwd_cpms … HX0) -HX0 #HTU0 elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hn) #U #HTU #_ -U0 -n0 /3 width=7 by cnv_appl_cpes, or_introl/ (* Note: argument type mismatch *) | @or_intror #H -n elim (cnv_inv_appl_cpes … H) -H #m0 #q #WX #UX #_ #_ #_ #HVWX #HTUX - lapply (cpmhe_abst … HTUX) -HTUX #HTUX - elim (cnv_cpmhe_mono … HT … HTUX … HX0) -a -T #H #_ + lapply (cpmuwe_abst … HTUX) -HTUX #HTUX + elim (cnv_cpmuwe_mono … HT … HTUX … HX0) -a -T #H #_ elim (cpes_fwd_abst_bi … H) -H #_ #HWX -n0 -m0 -p -q -UX -U0 /3 width=3 by cpes_cpes_trans/ - | lapply (cnv_cpmhe_trans … HT … HX0) -T #H + | lapply (cnv_cpmuwe_trans … HT … HX0) -T #H elim (cnv_inv_bind … H) -H #HW #_ // ] (* Note: no expected type *) | #HnX0 @or_intror #H elim (cnv_inv_appl_cpes … H) -H #m0 #q #W0 #U0 #_ #_ #_ #_ #HTU0 - lapply (cpmhe_abst … HTU0) -HTU0 #HTU0 - elim (cnv_cpmhe_mono … HT … HTU0 … HX0) -T #_ #H - elim (theq_inv_pair1 … H) -W0 -U0 #W0 #U0 #H destruct + lapply (cpmuwe_abst … HTU0) -HTU0 #HTU0 + elim (cnv_cpmuwe_mono … HT … HTU0 … HX0) -T #_ #H + elim (tweq_inv_abst_sn … H) -W0 -U0 #W0 #U0 #H destruct /2 width=4 by/ ] (* Note: failed applicability *) @@ -85,7 +86,7 @@ theorem cnv_dec (a) (h) (G) (L) (T): ac_props a → @or_intror #H elim (cnv_inv_appl … H) -H #m0 #q #W0 #U0 #Hm0 #_ #_ #_ #HTU0 elim (lt_or_ge m0 n0) #H0 [| /3 width=3 by ex2_intro/ ] -Hm0 -Hge - /4 width=6 by cpmhe_abst, ex_intro/ + /4 width=6 by cpmuwe_abst, ex_intro/ ] ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma index af4beb4c3..afe3079de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/rt_computation/cprs_cprs.ma". -include "basic_2/rt_computation/lprs_cpms.ma". include "basic_2/dynamic/cnv_aaa.ma". include "basic_2/dynamic/nta.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalwstar_6.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalstar_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalwstar_6.ma index 0a484cd85..065aeb23d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalstar_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalwstar_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 h, break term 46 n ] 𝐍 *⦃ break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡*𝐍𝐖*[ break term 46 h, break term 46 n ] break term 46 T2 )" non associative with precedence 45 - for @{ 'PRedEvalStar $h $n $G $L $T1 $T2 }. + for @{ 'PRedEvalWStar $h $n $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma index 881d1ba1d..1defb54aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⥲[ break term 46 h ] 𝐍⦃ break term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡𝐍𝐖*[ break term 46 h ] break term 46 T )" non associative with precedence 45 for @{ 'PRedITNormal $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma new file mode 100644 index 000000000..72a8e9ac3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma @@ -0,0 +1,131 @@ +(**************************************************************************) +(* ___ *) +(* ||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/preditnormal_4.ma". +include "static_2/syntax/tweq.ma". +include "basic_2/rt_computation/cpms.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************) + +definition cnuw (h) (G) (L): predicate term ≝ + λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → T1 ≅ T2. + +interpretation + "normality for t-unbound weak head context-sensitive parallel rt-transition (term)" + 'PRedITNormal h G L T = (cnuw h G L T). + +lemma cpm_inv_lref1_ctop (n) (h) (G): + ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0. +#n #h #G #X2 * [| #i ] #H +[ elim (cpm_inv_zero1 … H) -H * + [ #H1 #H2 destruct /2 width=1 by conj/ + | #Y #X1 #X2 #_ #_ #H destruct + | #m #Y #X1 #X2 #_ #_ #H destruct + ] +| elim (cpm_inv_lref1 … H) -H * + [ #H1 #H2 destruct /2 width=1 by conj/ + | #Z #Y #X0 #_ #_ #H destruct + ] +] +qed. + +lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G): + ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0. +#n #h #I #G #K #X2 #H +elim (cpm_inv_zero1 … H) -H * +[ #H1 #H2 destruct /2 width=1 by conj/ +| #Y #X1 #X2 #_ #_ #H destruct +| #m #Y #X1 #X2 #_ #_ #H destruct +] +qed. + +lemma cpms_inv_lref1_ctop (n) (h) (G): + ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡*[n,h] X2 → ∧∧ X2 = #i & n = 0. +#n #h #G #X2 #i #H @(cpms_ind_dx … H) -X2 +[ /2 width=1 by conj/ +| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct + elim (cpm_inv_lref1_ctop … HX2) -HX2 #H1 #H2 destruct + /2 width=1 by conj/ +] +qed-. + +lemma cpms_inv_zero1_unit (n) (h) (I) (K) (G): + ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡*[n,h] X2 → ∧∧ X2 = #0 & n = 0. +#n #h #I #G #K #X2 #H @(cpms_ind_dx … H) -X2 +[ /2 width=1 by conj/ +| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct + elim (cpm_inv_zero1_unit … HX2) -HX2 #H1 #H2 destruct + /2 width=1 by conj/ +] +qed-. + +lemma cpms_inv_gref1 (n) (h) (G) (L): + ∀X2,l. ⦃G,L⦄ ⊢ §l ➡*[n,h] X2 → ∧∧ X2 = §l & n = 0. +#n #h #G #L #X2 #l #H @(cpms_ind_dx … H) -X2 +[ /2 width=1 by conj/ +| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct + elim (cpm_inv_gref1 … HX2) -HX2 #H1 #H2 destruct + /2 width=1 by conj/ +] +qed-. + +(* Basic properties *********************************************************) + +lemma cnuw_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⋆s. +#h #G #L #s1 #n #X #H +lapply (cpms_inv_sort1 … H) -H #H destruct // +qed. + +lemma cnuw_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ➡𝐍𝐖*[h] #i. +#h #G #i #n #X #H +elim (cpms_inv_lref1_ctop … H) -H #H #_ destruct // +qed. + +lemma cnuw_zero_unit (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ➡𝐍𝐖*[h] #0. +#h #G #L #I #n #X #H +elim (cpms_inv_zero1_unit … H) -H #H #_ destruct // +qed. + +lemma cnuw_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] §l. +#h #G #L #l1 #n #X #H +elim (cpms_inv_gref1 … H) -H #H #_ destruct // +qed. + +(* Basic_inversion lemmas ***************************************************) + +lemma cnuw_inv_zero_pair (h) (I) (G) (L): ∀V. ⦃G,L.ⓑ{I}V⦄ ⊢ ➡𝐍𝐖*[h] #0 → ⊥. +#h * #G #L #V #H +elim (lifts_total V (𝐔❴1❵)) #W #HVW +[ lapply (H 0 W ?) [ /3 width=3 by cpm_cpms, cpm_delta/ ] +| lapply (H 1 W ?) [ /3 width=3 by cpm_cpms, cpm_ell/ ] +] -H #HW +lapply (tweq_inv_lref_sn … HW) -HW #H destruct +/2 width=5 by lifts_inv_lref2_uni_lt/ +qed-. + +lemma cnuw_inv_cast (h) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓝV.T → ⊥. +#h #G #L #V #T #H +lapply (H 0 T ?) [ /3 width=1 by cpm_cpms, cpm_eps/ ] -H #H +/2 width=3 by tweq_inv_cast_sn_XY_Y/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma cnuw_fwd_appl (h) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T. +#h #G #L #V #T1 #HT1 #n #T2 #HT12 +lapply (HT1 n (ⓐV.T2) ?) -HT1 +/2 width=3 by cpms_appl_dx, tweq_inv_appl_bi/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma new file mode 100644 index 000000000..0249a95e0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_cnuw.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cnuw.ma". +include "basic_2/rt_computation/cprs_tweq.ma". +include "basic_2/rt_computation/lprs_cpms.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cnuw_inv_abbr_pos (h) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] +ⓓV.T → ⊥. +#h #G #L #V #T1 #H +elim (cprs_abbr_pos_twneq h G L V T1) #T2 #HT12 #HnT12 +/3 width=2 by/ +qed-. + +(* Advanced properties ******************************************************) + +lemma cnuw_abbr_neg (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] -ⓓV.T. +#h #G #L #V1 #T1 #n #X #H +elim (cpms_inv_abbr_sn_dx … H) -H * +[ #V2 #T2 #_ #_ #H destruct /1 width=1 by tweq_abbr_neg/ +| #X1 #_ #_ #H destruct +] +qed. + +lemma cnuw_abst (h) (p) (G) (L): ∀W,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓛ{p}W.T. +#h #p #G #L #W1 #T1 #n #X #H +elim (cpms_inv_abst_sn … H) -H #W2 #T2 #_ #_ #H destruct +/1 width=1 by tweq_abst/ +qed. + +lemma cnuw_cpms_trans (h) (n) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1 → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2. +#h #n1 #G #L #T1 #HT1 #T2 #HT12 #n2 #T3 #HT23 +/4 width=5 by cpms_trans, tweq_canc_sn/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_drops.ma similarity index 54% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_drops.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_drops.ma index d4927690f..374aa1284 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_drops.ma @@ -12,41 +12,53 @@ (* *) (**************************************************************************) -include "static_2/relocation/lifts_theq.ma". -include "basic_2/rt_transition/cpm_drops.ma". -include "basic_2/rt_transition/cnh.ma". +include "static_2/relocation/lifts_tweq.ma". +include "basic_2/rt_computation/cpms_drops.ma". +include "basic_2/rt_computation/cnuw.ma". -(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) +(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************) + +(* Properties with generic relocation ***************************************) + +lemma cnuw_lifts (h) (G): d_liftable1 … (cnuw h G). +#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H +elim (cpms_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 +lapply (HT … HT0) -G -K /2 width=6 by tweq_lifts_bi/ +qed-. + +(* Inversion lemmas with generic relocation *********************************) + +lemma cnuw_inv_lifts (h) (G): d_deliftable1 … (cnuw h G). +#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H +elim (cpms_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 +lapply (HU … HU0) -G -L /2 width=6 by tweq_inv_lifts_bi/ +qed-. (* Advanced properties ******************************************************) -lemma cnh_atom_drops (h) (b) (G) (L): - ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄. +lemma cnuw_lref (h) (I) (G) (L): + ∀i. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] #i → ⦃G,L.ⓘ{I}⦄ ⊢ ➡𝐍𝐖*[h] #↑i. +#h #I #G #L #i #Hi #n #X2 #H +elim (cpms_inv_lref_sn … H) -H * +[ #H #_ destruct // +| #T2 #HT2 #HTX2 + lapply (Hi … HT2) -Hi -HT2 #H + lapply (tweq_inv_lref_sn … H) -H #H destruct + lapply (lifts_inv_lref1_uni … HTX2) -HTX2 #H destruct // +] +qed. + +lemma cnuw_atom_drops (h) (b) (G) (L): + ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] #i. #h #b #G #L #i #Hi #n #X #H -elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK +elim (cpms_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK lapply (drops_gen b … HLK) -HLK #HLK lapply (drops_mono … Hi … HLK) -L #H destruct qed. -lemma cnh_unit_drops (h) (I) (G) (L): - ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄. +lemma cnuw_unit_drops (h) (I) (G) (L): + ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] #i. #h #I #G #L #K #i #HLK #n #X #H -elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY +elim (cpms_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct qed. - -(* Properties with generic relocation ***************************************) - -lemma cnh_lifts (h) (G): d_liftable1 … (cnh h G). -#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H -elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 -lapply (HT … HT0) -G -K /2 width=6 by theq_lifts_bi/ -qed-. - -(* Inversion lemmas with generic relocation *********************************) - -lemma cnh_inv_lifts (h) (G): d_deliftable1 … (cnh h G). -#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H -elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 -lapply (HU … HU0) -G -L /2 width=6 by theq_inv_lifts_bi/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.ma new file mode 100644 index 000000000..d32e1b1d6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_simple.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 "static_2/syntax/tweq_simple.ma". +include "basic_2/rt_computation/cpms_cpms.ma". +include "basic_2/rt_computation/cnuw.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************) + +(* Advanced forward lemma with with simple terms ****************************) +(* +lemma cnuw_fwd_appl_simple (h) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T → 𝐒⦃T⦄. +#h #G #L #V #T #HT +elim (simple_dec_ex T) [ // ] * #p #I #W #U #H destruct +*) +(* Advanced properties with simple terms ************************************) + +lemma cnuw_appl_simple (h) (G) (L): + ∀V,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] ⓐV.T. +#h #G #L #V1 #T1 #H1T1 #H2T1 #n #X #H +elim (cpms_inv_appl_sn … H) -H * +[ #V2 #T2 #_ #HT12 #H destruct -H1T1 + /3 width=2 by tweq_appl/ +| #n1 #n2 #p #V2 #T2 #HT12 #_ #_ -n -n2 + lapply (H2T1 … HT12) -H2T1 -n1 #H + lapply (tweq_simple_trans … H H1T1) -H -H1T1 #H + elim (simple_inv_bind … H) +| #n1 #n2 #p #V2 #W2 #W #T2 #_ #_ #HT12 #_ #_ -n -n2 -V2 -W2 + lapply (H2T1 … HT12) -H2T1 -n1 #H + lapply (tweq_simple_trans … H H1T1) -H -H1T1 #H + elim (simple_inv_bind … H) +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma similarity index 75% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma index 666474121..40ac5ddbf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma @@ -13,22 +13,23 @@ (**************************************************************************) include "basic_2/rt_transition/cpr_tdeq.ma". -include "basic_2/rt_transition/cnh_simple.ma". -include "basic_2/rt_transition/cnh_drops.ma". +include "basic_2/rt_computation/cnuw_simple.ma". +include "basic_2/rt_computation/cnuw_drops.ma". +include "basic_2/rt_computation/cnuw_cnuw.ma". -(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) +(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************) (* Properties with context-free sort-irrelevant equivalence for terms *******) -lemma cnh_dec_tdeq (h) (G) (L): - ∀T1. ∨∨ ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ +lemma cnuw_dec_tdeq (h) (G) (L): + ∀T1. ∨∨ ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T1 | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥). -#h #G #L * * -[ #s /3 width=5 by cnh_sort, or_introl/ +#h #G #L #T1 elim T1 -T1 * +[ #s /3 width=5 by cnuw_sort, or_introl/ | #i elim (drops_F_uni L i) - [ /3 width=7 by cnh_atom_drops, or_introl/ + [ /3 width=7 by cnuw_atom_drops, or_introl/ | * * [ #I | * #V ] #K #HLK - [ /3 width=8 by cnh_unit_drops, or_introl/ + [ /3 width=8 by cnuw_unit_drops, or_introl/ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H lapply (tdeq_inv_lref1 … H) -H #H destruct @@ -39,8 +40,8 @@ lemma cnh_dec_tdeq (h) (G) (L): /2 width=5 by lifts_inv_lref2_uni_lt/ ] ] -| #l /3 width=5 by cnh_gref, or_introl/ -| #p * [ cases p ] #V1 #T1 +| #l /3 width=5 by cnuw_gref, or_introl/ +| #p * [ cases p ] #V1 #T1 #_ #_ [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2 elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ] [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2 @@ -49,12 +50,17 @@ lemma cnh_dec_tdeq (h) (G) (L): | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ ] - | /3 width=5 by cnh_abbr_neg, or_introl/ - | /3 width=5 by cnh_abst, or_introl/ + | /3 width=5 by cnuw_abbr_neg, or_introl/ + | /3 width=5 by cnuw_abst, or_introl/ ] -| * #V1 #T1 +| * #V1 #T1 #_ #IH [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ] - [ /3 width=5 by cnh_appl_simple, or_introl/ + [ elim IH -IH + [ /3 width=6 by cnuw_appl_simple, or_introl/ + | * #n #T2 #HT12 #HnT12 + @or_intror @(ex2_2_intro … n (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H + elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/ + ] | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1 @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H elim (tdeq_inv_pair … H) -H #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe.ma similarity index 51% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe.ma index c08c1b101..44d91e8da 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe.ma @@ -12,56 +12,47 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predevalstar_6.ma". -include "basic_2/rt_transition/cnh.ma". -include "basic_2/rt_computation/cpms.ma". +include "basic_2/notation/relations/predevalwstar_6.ma". +include "basic_2/rt_computation/cnuw.ma". -(* HEAD T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS *************) +(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************) -definition cpmhe (h) (n) (G) (L): relation2 term term ≝ - λT1,T2. ∧∧ ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄. +definition cpmuwe (h) (n) (G) (L): relation2 term term ≝ + λT1,T2. ∧∧ ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2. -interpretation "t-unbound evaluation for t-bound context-sensitive parallel rt-transition (term)" - 'PRedEvalStar h n G L T1 T2 = (cpmhe h n G L T1 T2). +interpretation "t-unbound whd evaluation for t-bound context-sensitive parallel rt-transition (term)" + 'PRedEvalWStar h n G L T1 T2 = (cpmuwe h n G L T1 T2). -definition R_cpmhe (h) (G) (L) (T): predicate nat ≝ - λn. ∃U. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃U⦄. +definition R_cpmuwe (h) (G) (L) (T): predicate nat ≝ + λn. ∃U. ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] U. (* Basic properties *********************************************************) -lemma cpmhe_intro (h) (n) (G) (L): - ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄. +lemma cpmuwe_intro (h) (n) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ➡𝐍𝐖*[h] T2 → ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2. /2 width=1 by conj/ qed. (* Advanced properties ******************************************************) -lemma cpmhe_sort (h) (n) (G) (L) (T): - ∀s. ⦃G,L⦄ ⊢ T ➡*[n,h] ⋆s → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃⋆s⦄. -/3 width=5 by cnh_sort, cpmhe_intro/ qed. +lemma cpmuwe_sort (h) (n) (G) (L) (T): + ∀s. ⦃G,L⦄ ⊢ T ➡*[n,h] ⋆s → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] ⋆s. +/3 width=5 by cnuw_sort, cpmuwe_intro/ qed. -lemma cpmhe_ctop (h) (n) (G) (T): - ∀i. ⦃G,⋆⦄ ⊢ T ➡*[n,h] #i → ⦃G,⋆⦄ ⊢ T ➡*[h,n] 𝐍*⦃#i⦄. -/3 width=5 by cnh_ctop, cpmhe_intro/ qed. +lemma cpmuwe_ctop (h) (n) (G) (T): + ∀i. ⦃G,⋆⦄ ⊢ T ➡*[n,h] #i → ⦃G,⋆⦄ ⊢ T ➡*𝐍𝐖*[h,n] #i. +/3 width=5 by cnuw_ctop, cpmuwe_intro/ qed. -lemma cpmhe_zero (h) (n) (G) (L) (T): - ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[n,h] #0 → ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[h,n] 𝐍*⦃#0⦄. -/3 width=6 by cnh_zero, cpmhe_intro/ qed. +lemma cpmuwe_zero_unit (h) (n) (G) (L) (T): + ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[n,h] #0 → ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*𝐍𝐖*[h,n] #0. +/3 width=6 by cnuw_zero_unit, cpmuwe_intro/ qed. -lemma cpmhe_gref (h) (n) (G) (L) (T): - ∀l. ⦃G,L⦄ ⊢ T ➡*[n,h] §l → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃§l⦄. -/3 width=5 by cnh_gref, cpmhe_intro/ qed. - -lemma cpmhe_abst (h) (n) (p) (G) (L) (T): - ∀W,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃ⓛ{p}W.U⦄. -/3 width=5 by cnh_abst, cpmhe_intro/ qed. - -lemma cpmhe_abbr_neg (h) (n) (G) (L) (T): - ∀V,U. ⦃G,L⦄ ⊢ T ➡*[n,h] -ⓓV.U → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃-ⓓV.U⦄. -/3 width=5 by cnh_abbr_neg, cpmhe_intro/ qed. +lemma cpmuwe_gref (h) (n) (G) (L) (T): + ∀l. ⦃G,L⦄ ⊢ T ➡*[n,h] §l → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] §l. +/3 width=5 by cnuw_gref, cpmuwe_intro/ qed. (* Basic forward lemmas *****************************************************) -lemma cpmhe_fwd_cpms (h) (n) (G) (L): - ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2. +lemma cpmuwe_fwd_cpms (h) (n) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2. #h #n #G #L #T1 #T2 * #HT12 #_ // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_cpmuwe.ma similarity index 63% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_simple.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_cpmuwe.ma index 71951a7ee..deea7cdd4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_cpmuwe.ma @@ -12,15 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/cpm_simple.ma". -include "basic_2/rt_transition/cnh.ma". +include "basic_2/rt_computation/cnuw_cnuw.ma". +include "basic_2/rt_computation/cpmuwe.ma". -(* NORMAL TERMS HEAD FOR T-UNUNBOUND RT-TRANSITION **************************) +(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************) -(* Advanced properties with simple terms ************************************) +(* Advanced properties ******************************************************) -lemma cnh_appl_simple (h) (G) (L): ∀V,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓐV.T⦄. -#h #G #L #V1 #T1 #HT1 #n #X #H -elim (cpm_inv_appl1_simple … H HT1) -H -HT1 #V2 #T2 #_ #_ #H destruct -/1 width=1 by theq_pair/ -qed. +lemma cpmuwe_abbr_neg (h) (n) (G) (L) (T): + ∀V,U. ⦃G,L⦄ ⊢ T ➡*[n,h] -ⓓV.U → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U. +/3 width=5 by cnuw_abbr_neg, cpmuwe_intro/ qed. + +lemma cpmuwe_abst (h) (n) (p) (G) (L) (T): + ∀W,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ T ➡*𝐍𝐖*[h,n] ⓛ{p}W.U. +/3 width=5 by cnuw_abst, cpmuwe_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma similarity index 72% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma index d821c8452..911dddd5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma @@ -13,29 +13,29 @@ (**************************************************************************) include "basic_2/rt_transition/cpm_cpx.ma". -include "basic_2/rt_transition/cnh_tdeq.ma". include "basic_2/rt_computation/csx.ma". -include "basic_2/rt_computation/cpmhe.ma". +include "basic_2/rt_computation/cnuw_tdeq.ma". +include "basic_2/rt_computation/cpmuwe.ma". -(* HEAD T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS *************) +(* T-UNBOUND WHD EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS **************) (* Properties with strong normalization for unbound rt-transition for terms *) -lemma cpmhe_total_csx (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄. +lemma cpmuwe_total_csx (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*𝐍𝐖*[h,n] T2. #h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #_ #IHT1 -elim (cnh_dec_tdeq h G L T1) -[ -IHT1 #HT1 /3 width=4 by cpmhe_intro, ex1_2_intro/ +elim (cnuw_dec_tdeq h G L T1) +[ -IHT1 #HT1 /3 width=4 by cpmuwe_intro, ex1_2_intro/ | * #n1 #T0 #HT10 #HnT10 elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ] - #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmhe_intro, ex1_2_intro/ + #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmuwe_intro, ex1_2_intro/ ] qed-. -lemma R_cpmhe_total_csx (h) (G) (L): - ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmhe h G L T1 n. +lemma R_cpmuwe_total_csx (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmuwe h G L T1 n. #h #G #L #T1 #H -elim (cpmhe_total_csx … H) -H #T2 #n #HT12 +elim (cpmuwe_total_csx … H) -H #T2 #n #HT12 /3 width=3 by ex_intro (* 2x *)/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma similarity index 56% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma index 8cd6df24a..a7c2b4074 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_tweq.ma @@ -12,17 +12,24 @@ (* *) (**************************************************************************) -include "static_2/syntax/theq_theq.ma". -include "basic_2/rt_transition/cnh_cnh.ma". +include "static_2/syntax/tweq_tweq.ma". +include "static_2/relocation/lifts_tweq.ma". +include "basic_2/rt_transition/cpr_drops_basic.ma". include "basic_2/rt_computation/cpms.ma". -(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) +(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************) -(* Inversion lemmas with normal terms for head t-unbound rt-transition ******) +(* Properties with sort-irrelevant whd equivalence on terms *****************) -lemma cpms_inv_cnh_sn (h) (n) (G) (L): - ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → T1 ⩳ T2. -#h #n #G #L #T1 #T2 #H @(cpms_ind_sn … H) -T1 // -#n1 #n2 #T1 #T0 #HT10 #_ #IH #HT1 -/4 width=9 by cnh_cpm_trans, theq_trans/ +lemma cprs_abbr_pos_twneq (h) (G) (L) (V) (T1): + ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡*[h] T2 & (+ⓓV.T1 ≅ T2 → ⊥). +#h #G #L #V #U1 +elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2 +elim (tweq_dec U1 U2) [ #HpU12 | -HTU2 #HnU12 ] +[ @(ex2_intro … T2) (**) (* full auto not tried *) + [ /3 width=6 by cpms_zeta, cpms_step_sn, cpm_bind/ + | /4 width=6 by tweq_inv_abbr_pos_sn_X_lifts_Y_Y, tweq_canc_sn, tweq_abbr_pos/ + ] +| /4 width=3 by cpm_cpms, cpm_bind, tweq_inv_abbr_pos_bi, ex2_intro/ +] 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_toeq.ma similarity index 70% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma index 5174890e0..f0782e12c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq.ma @@ -12,26 +12,28 @@ (* *) (**************************************************************************) -include "static_2/syntax/theq_tdeq.ma". +include "static_2/syntax/toeq_tdeq.ma". include "basic_2/rt_computation/cpxs_lsubr.ma". include "basic_2/rt_computation/cpxs_cnx.ma". include "basic_2/rt_computation/lpxs_cpxs.ma". (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) -(* Forward lemmas with head equivalence for terms ***************************) +(* Forward lemmas with sort-irrelevant outer equivalence for terms **********) -lemma cpxs_fwd_sort: ∀h,G,L,X2,s1. ⦃G,L⦄ ⊢ ⋆s1 ⬈*[h] X2 → ⋆s1 ⩳ X2. +lemma cpxs_fwd_sort (h) (G) (L): + ∀X2,s1. ⦃G,L⦄ ⊢ ⋆s1 ⬈*[h] X2 → ⋆s1 ⩳ X2. #h #G #L #X2 #s1 #H elim (cpxs_inv_sort1 … H) -H #s2 #H destruct // qed-. (* Note: probably this is an inversion lemma *) (* Basic_2A1: was: cpxs_fwd_delta *) -lemma cpxs_fwd_delta_drops: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → - ∀V2. ⬆*[↑i] V1 ≘ V2 → - ∀X2. ⦃G,L⦄ ⊢ #i ⬈*[h] X2 → - ∨∨ #i ⩳ X2 | ⦃G,L⦄ ⊢ V2 ⬈*[h] X2. +lemma cpxs_fwd_delta_drops (h) (I) (G) (L) (K): + ∀V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → + ∀V2. ⬆*[↑i] V1 ≘ V2 → + ∀X2. ⦃G,L⦄ ⊢ #i ⬈*[h] X2 → + ∨∨ #i ⩳ X2 | ⦃G,L⦄ ⊢ V2 ⬈*[h] X2. #h #I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/ * #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 @@ -40,10 +42,11 @@ lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct qed-. (* Basic_1: was just: pr3_iso_beta *) -lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X2 → - ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2. +lemma cpxs_fwd_beta (h) (p) (G) (L): + ∀V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X2 → + ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2. #h #p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +[ #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 @@ -53,12 +56,13 @@ lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,X2. ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] X ] qed-. -lemma cpxs_fwd_theta: ∀h,p,G,L,V1,V,T,X2. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 → - ∀V2. ⬆*[1] V1 ≘ V2 → - ∨∨ ⓐV1.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] X2. +lemma cpxs_fwd_theta (h) (p) (G) (L): + ∀V1,V,T,X2. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 → + ∀V2. ⬆*[1] V1 ≘ V2 → + ∨∨ ⓐV1.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] X2. #h #p #G #L #V1 #V #T #X2 #H #V2 #HV12 elim (cpxs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/ | #q #W #T0 #HT0 #HU elim (cpxs_inv_abbr1_dx … HT0) -HT0 * [ #V3 #T3 #_ #_ #H destruct @@ -84,13 +88,15 @@ elim (cpxs_inv_appl1 … H) -H * ] qed-. -lemma cpxs_fwd_cast: ∀h,G,L,W,T,X2. ⦃G,L⦄ ⊢ ⓝW.T ⬈*[h] X2 → - ∨∨ ⓝW. T ⩳ X2 | ⦃G,L⦄ ⊢ T ⬈*[h] X2 | ⦃G,L⦄ ⊢ W ⬈*[h] X2. +lemma cpxs_fwd_cast (h) (G) (L): + ∀W,T,X2. ⦃G,L⦄ ⊢ ⓝW.T ⬈*[h] X2 → + ∨∨ ⓝW. T ⩳ X2 | ⦃G,L⦄ ⊢ T ⬈*[h] X2 | ⦃G,L⦄ ⊢ W ⬈*[h] X2. #h #G #L #W #T #X2 #H elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * -#W0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/ +#W0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or3_intro0/ qed-. -lemma cpxs_fwd_cnx: ∀h,G,L,T1. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ → - ∀X2. ⦃G,L⦄ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2. -/3 width=5 by cpxs_inv_cnx1, tdeq_theq/ qed-. +lemma cpxs_fwd_cnx (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ → + ∀X2. ⦃G,L⦄ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2. +/3 width=5 by cpxs_inv_cnx1, tdeq_toeq/ qed-. 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_toeq_vector.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma index 40c508756..bbd7c5c9d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma @@ -12,48 +12,50 @@ (* *) (**************************************************************************) -include "static_2/syntax/theq_simple_vector.ma". +include "static_2/syntax/toeq_simple_vector.ma". include "static_2/relocation/lifts_vector.ma". -include "basic_2/rt_computation/cpxs_theq.ma". +include "basic_2/rt_computation/cpxs_toeq.ma". (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) -(* Vector form of forward lemmas with head equivalence for terms ************) +(* Vector form of forward lemmas with outer equivalence for terms ***********) -lemma cpxs_fwd_sort_vector: ∀h,G,L,s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2. +lemma cpxs_fwd_sort_vector (h) (G) (L): + ∀s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2. #h #G #L #s #Vs elim Vs -Vs /2 width=4 by cpxs_fwd_sort/ #V #Vs #IHVs #X2 #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by toeq_pair/ | #p #W1 #T1 #HT1 #HU lapply (IHVs … HT1) -IHVs -HT1 #HT1 - elim (theq_inv_applv_bind_simple … HT1) // + elim (toeq_inv_applv_bind_simple … HT1) // | #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU lapply (IHVs … HT1) -IHVs -HT1 #HT1 - elim (theq_inv_applv_bind_simple … HT1) // + elim (toeq_inv_applv_bind_simple … HT1) // ] qed-. (* Basic_2A1: was: cpxs_fwd_delta_vector *) -lemma cpxs_fwd_delta_drops_vector: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → - ∀V2. ⬆*[↑i] V1 ≘ V2 → - ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 → - ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2. +lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K): + ∀V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → + ∀V2. ⬆*[↑i] V1 ≘ V2 → + ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 → + ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2. #h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/ #V #Vs #IHVs #X2 #H -K -V1 elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/ | #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (theq_inv_applv_bind_simple … HT0) // + [ elim (toeq_inv_applv_bind_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/ ] | #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (theq_inv_applv_bind_simple … HT0) // + [ elim (toeq_inv_applv_bind_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/ @@ -62,22 +64,23 @@ elim (cpxs_inv_appl1 … H) -H * qed-. (* Basic_1: was just: pr3_iso_appls_beta *) -lemma cpxs_fwd_beta_vector: ∀h,p,G,L,Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 → - ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2. +lemma cpxs_fwd_beta_vector (h) (p) (G) (L): + ∀Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 → + ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2. #h #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ #V0 #Vs #IHVs #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/ | #q #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (theq_inv_applv_bind_simple … HT1) // + [ elim (toeq_inv_applv_bind_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ ] | #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (theq_inv_applv_bind_simple … HT1) // + [ elim (toeq_inv_applv_bind_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ @@ -86,9 +89,10 @@ elim (cpxs_inv_appl1 … H) -H * qed-. (* Basic_1: was just: pr3_iso_appls_abbr *) -lemma cpxs_fwd_theta_vector: ∀h,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b → - ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 → - ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2. +lemma cpxs_fwd_theta_vector (h) (G) (L): + ∀V1b,V2b. ⬆*[1] V1b ≘ V2b → + ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 → + ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2. #h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/ #V1b #V2b #V1a #V2a #HV12a #HV12b #p generalize in match HV12a; -HV12a @@ -97,11 +101,11 @@ generalize in match V1a; -V1a elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/ #V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #X2 #H elim (cpxs_inv_appl1 … H) -H * -[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ +[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or_introl/ | #q #W0 #T0 #HT0 #HU elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0 [ -HV12a -HV12b -HU - elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct + elim (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1b (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 elim (cpxs_inv_abbr1_dx … HT0) -HT0 * @@ -116,7 +120,7 @@ elim (cpxs_inv_appl1 … H) -H * | #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0 [ -HV12a -HV10a -HV0a -HU - elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct + elim (toeq_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1b -V1b (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 elim (cpxs_inv_abbr1_dx … HT0) -HT0 * @@ -135,16 +139,17 @@ elim (cpxs_inv_appl1 … H) -H * qed-. (* Basic_1: was just: pr3_iso_appls_cast *) -lemma cpxs_fwd_cast_vector: ∀h,G,L,Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 → - ∨∨ ⒶVs. ⓝW. T ⩳ X2 - | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 - | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2. +lemma cpxs_fwd_cast_vector (h) (G) (L): + ∀Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 → + ∨∨ ⒶVs. ⓝW. T ⩳ X2 + | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 + | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2. #h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ #V #Vs #IHVs #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair, or3_intro0/ | #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (theq_inv_applv_bind_simple … HT0) // + [ elim (toeq_inv_applv_bind_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ @@ -154,7 +159,7 @@ elim (cpxs_inv_appl1 … H) -H * ] | #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (theq_inv_applv_bind_simple … HT0) // + [ elim (toeq_inv_applv_bind_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -X2 @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ @@ -166,17 +171,18 @@ elim (cpxs_inv_appl1 … H) -H * qed-. (* Basic_1: was just: nf2_iso_appls_lref *) -lemma cpxs_fwd_cnx_vector: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → - ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2. +lemma cpxs_fwd_cnx_vector (h) (G) (L): + ∀T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → + ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2. #h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) #V #Vs #IHVs #X2 #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by toeq_pair/ | #p #W0 #T0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (theq_inv_applv_bind_simple … HT0) // + elim (toeq_inv_applv_bind_simple … HT0) // | #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (theq_inv_applv_bind_simple … HT0) // + elim (toeq_inv_applv_bind_simple … HT0) // ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma index fbaee7c73..6d75480ff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma @@ -14,8 +14,8 @@ (* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****) -include "basic_2/rt_computation/cpxs_theq_vector.ma". -include "basic_2/rt_computation/csx_simple_theq.ma". +include "basic_2/rt_computation/cpxs_toeq_vector.ma". +include "basic_2/rt_computation/csx_simple_toeq.ma". include "basic_2/rt_computation/csx_cnx.ma". include "basic_2/rt_computation/csx_cpxs.ma". include "basic_2/rt_computation/csx_vector.ma". @@ -23,13 +23,14 @@ include "basic_2/rt_computation/csx_vector.ma". (* Properties with normal terms for unbound parallel rt-transition **********) (* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → - ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄. +lemma csx_applv_cnx (h) (G) (L): + ∀T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → + ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄. #h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/ | #V #Vs #IHV #H elim (csxv_inv_cons … H) -H #HV #HVs - @csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs + @csx_appl_simple_toeq /2 width=1 by applv_simple/ -IHV -HV -HVs #X #H #H0 lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H elim (H0) -H0 // @@ -39,5 +40,6 @@ qed. (* Advanced properties ******************************************************) (* Note: strong normalization does not depend on this any more *) -lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄. +lemma csx_applv_sort (h) (G) (L): + ∀s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄. /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index 054fb100b..571a81546 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/cpxs_theq_vector.ma". -include "basic_2/rt_computation/csx_simple_theq.ma". +include "basic_2/rt_computation/cpxs_toeq_vector.ma". +include "basic_2/rt_computation/csx_simple_toeq.ma". include "basic_2/rt_computation/csx_lsubr.ma". include "basic_2/rt_computation/csx_lpx.ma". include "basic_2/rt_computation/csx_vector.ma". @@ -30,7 +30,7 @@ lemma csx_applv_beta (h) (G): #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T +@csx_appl_simple_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T #X #H #H0 elim (cpxs_fwd_beta_vector … H) -H #H [ -H1T elim H0 -H0 // @@ -47,7 +47,7 @@ lemma csx_applv_delta_drops (h) (G): | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T + @csx_appl_simple_toeq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T #X #H #H0 elim (cpxs_fwd_delta_drops_vector … HLK … HV12 … H) -HLK -HV12 -H #H [ -H1T elim H0 -H0 // @@ -68,7 +68,7 @@ elim H -V1b -V2b /2 width=3 by csx_appl_theta/ lapply (csx_appl_theta … H … HW12) -H -HW12 #H lapply (csx_fwd_pair_sn … H) #HW1 lapply (csx_fwd_flat_dx … H) #H1 -@csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2 +@csx_appl_simple_toeq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2 elim (cpxs_fwd_theta_vector … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12 [ -H #H elim H2 -H2 // | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ @@ -84,7 +84,7 @@ lemma csx_applv_cast (h) (G): lapply (csx_fwd_pair_sn … H1U) #HV lapply (csx_fwd_flat_dx … H1U) #H2U lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T +@csx_appl_simple_toeq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2U -H2T #X #H #H0 elim (cpxs_fwd_cast_vector … H) -H #H [ -H1U -H1T elim H0 -H0 // diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma similarity index 74% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma index bb3b10b01..8fb338684 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_toeq.ma @@ -12,21 +12,22 @@ (* *) (**************************************************************************) -include "static_2/syntax/theq_simple.ma". -include "static_2/syntax/theq_theq.ma". +include "static_2/syntax/toeq_simple.ma". +include "static_2/syntax/toeq_toeq.ma". include "basic_2/rt_transition/cpx_simple.ma". include "basic_2/rt_computation/cpxs.ma". include "basic_2/rt_computation/csx_csx.ma". (* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************) -(* Properties with head equivalence for terms *******************************) +(* Properties with outer equivalence for terms ******************************) (* Basic_1: was just: sn3_appl_appl *) (* Basic_2A1: was: csx_appl_simple_tsts *) -lemma csx_appl_simple_theq: ∀h,G,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → - (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) → - 𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄. +lemma csx_appl_simple_toeq (h) (G) (L): + ∀V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → + (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) → + 𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄. #h #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @@ -40,8 +41,8 @@ elim (tdneq_inv_pair … H) -H @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ | -IHV -H1T1 #H1T10 @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0 - elim (theq_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/ + elim (toeq_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, toeq_canc_sn, simple_toeq_repl_dx/ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma deleted file mode 100644 index 9e549a93d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma +++ /dev/null @@ -1,75 +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/preditnormal_4.ma". -include "static_2/syntax/theq.ma". -include "basic_2/rt_transition/cpm.ma". - -(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) - -definition cnh (h) (G) (L): predicate term ≝ - λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ⩳ T2. - -interpretation - "normality for head t-unbound context-sensitive parallel rt-transition (term)" - 'PRedITNormal h G L T = (cnh h G L T). - -(* Basic properties *********************************************************) - -lemma cnh_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃⋆s⦄. -#h #G #L #s1 #n #X #H -elim (cpm_inv_sort1 … H) -H #H #_ destruct // -qed. - -lemma cnh_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ⥲[h] 𝐍⦃#i⦄. -#h #G * [| #i ] #n #X #H -[ elim (cpm_inv_zero1 … H) -H * - [ #H #_ destruct // - | #Y #X1 #X2 #_ #_ #H destruct - | #m #Y #X1 #X2 #_ #_ #H destruct - ] -| elim (cpm_inv_lref1 … H) -H * - [ #H #_ destruct // - | #Z #Y #X0 #_ #_ #H destruct - ] -] -qed. - -lemma cnh_zero (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ⥲[h] 𝐍⦃#0⦄. -#h #G #L #I #n #X #H -elim (cpm_inv_zero1 … H) -H * -[ #H #_ destruct // -| #Y #X1 #X2 #_ #_ #H destruct -| #m #Y #X1 #X2 #_ #_ #H destruct -] -qed. - -lemma cnh_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃§l⦄. -#h #G #L #l1 #n #X #H -elim (cpm_inv_gref1 … H) -H #H #_ destruct // -qed. - -lemma cnh_abst (h) (p) (G) (L): ∀W,T. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓛ{p}W.T⦄. -#h #p #G #L #W1 #T1 #n #X #H -elim (cpm_inv_abst1 … H) -H #W2 #T2 #_ #_ #H destruct -/1 width=1 by theq_pair/ -qed. - -lemma cnh_abbr_neg (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃-ⓓV.T⦄. -#h #G #L #V1 #T1 #n #X #H -elim (cpm_inv_abbr1 … H) -H * -[ #W2 #T2 #_ #_ #H destruct /1 width=1 by theq_pair/ -| #X1 #_ #_ #H destruct -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_lifts.ma deleted file mode 100644 index 3bbfeee85..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_lifts.ma +++ /dev/null @@ -1,32 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "static_2/relocation/lifts.ma". -include "basic_2/rt_transition/cnh.ma". - -(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) - -(* Advanced properties with uniform relocation for terms ********************) - -lemma cnh_lref (h) (I) (G) (L): - ∀i. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄ → ⦃G,L.ⓘ{I}⦄ ⊢ ⥲[h] 𝐍⦃#↑i⦄. -#h #I #G #L #i #Hi #n #X #H -elim (cpm_inv_lref1 … H) -H * -[ #H #_ destruct // -| #J #K #V #HV #HVX #H destruct - lapply (Hi … HV) -Hi -HV #HV - lapply (theq_inv_lref1 … HV) -HV #H destruct - lapply (lifts_inv_lref1_uni … HVX) -HVX #H destruct // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma index cca5dac39..910c7abe1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma @@ -19,8 +19,8 @@ include "basic_2/rt_transition/cpr_drops_basic.ma". (* Properties with context-free sort-irrelevant equivalence *****************) -lemma cpr_abbr_pos (h) (G) (L) (V) (T1): - ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛ T2 → ⊥). +lemma cpr_abbr_pos_tdneq (h) (G) (L) (V) (T1): + ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛ T2 → ⊥). #h #G #L #V #U1 elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2 elim (tdeq_dec U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ] 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 ef3ff958c..daa511a89 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -25,7 +25,7 @@ table { ] [ { "context-sensitive native validity" * } { [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ] - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmhe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] } ] } @@ -62,13 +62,15 @@ table { [ [ "evaluation for terms" ] "cpre ( ⦃?,?⦄ ⊢ ? ➡*[?] 𝐍⦃?⦄ )" "cpre_csx" + "cpre_cpms" + "cpre_cpre" * ] [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ] [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ] - [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ] + [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_tweq" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ] } ] [ { "t-bound context-sensitive parallel rt-computation" * } { - [ [ "t-unbound head evaluation for terms" ] "cpmhe ( ⦃?,?⦄ ⊢ ? ⬌*[?] 𝐍*⦃?⦄ )" "cpmhe_csx" * ] + [ [ "t-unbound whd evaluation for terms" ] "cpmuwe ( ⦃?,?⦄ ⊢ ? ⬌*𝐍𝐖*[?,?] ? )" "cpmuwe_csx" + "cpmuwe_cpmuwe" * ] + [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_tdeq" + "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ] + [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ] - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnh" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { @@ -81,20 +83,16 @@ table { [ [ "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_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "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_toeq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ] [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_rdeq" + "lpxs_fdeq" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] - [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_toeq" + "cpxs_toeq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_rdeq" + "cpxs_fdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } ] class "cyan" [ { "rt-transition" * } { - [ { "t-unbound context-sensitive parallel rt-transition" * } { - [ [ "head normal form for terms" ] "cnh ( ⦃?,?⦄ ⊢ ⥲[?] 𝐍⦃?⦄ )" "cnh_tdeq" + "cnh_lifts" + "cnh_drops" + "cnh_cnr" + "cnh_cnr_simple" + "cnh_cnh" * ] - } - ] [ { "context-sensitive parallel r-transition" * } { [ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ] [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ] @@ -206,8 +204,4 @@ class "italic" { 2 } [ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ] } ] - [ { "tail sort-irrelevant equivalence" * } { - [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ] - } - ] *) diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/tueq/approxeq_2.etc b/matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/static_2/etc/tueq/approxeq_2.etc rename to matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_theq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma similarity index 50% rename from matita/matita/contribs/lambdadelta/static_2/relocation/lifts_theq.ma rename to matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma index 29abf85ba..ffbddcbe4 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_theq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_toeq.ma @@ -12,59 +12,65 @@ (* *) (**************************************************************************) -include "static_2/syntax/theq.ma". +include "static_2/syntax/toeq.ma". include "static_2/relocation/lifts_lifts.ma". (* GENERIC RELOCATION FOR TERMS *********************************************) -(* Properties with tail sort-irrelevant head equivalence for terms **********) +(* Properties with sort-irrelevant outer equivalence for terms **************) -lemma theq_lifts_bi: liftable2_bi theq. +lemma toeq_lifts_sn: liftable2_sn toeq. #T1 #T2 #H elim H -T1 -T2 [||| * ] -[ #s1 #s2 #f #X1 #H1 #X2 #H2 - >(lifts_inv_sort1 … H1) -H1 >(lifts_inv_sort1 … H2) -H2 - /1 width=1 by theq_sort/ -| #i #f #X1 #H1 #X2 #H2 - elim (lifts_inv_lref1 … H1) -H1 #j1 #Hj1 #H destruct - elim (lifts_inv_lref1 … H2) -H2 #j2 #Hj2 #H destruct - <(at_mono … Hj2 … Hj1) -i -f -j2 - /1 width=1 by theq_lref/ -| #l #f #X1 #H1 #X2 #H2 - >(lifts_inv_gref1 … H1) -H1 >(lifts_inv_gref1 … H2) -H2 - /1 width=1 by theq_gref/ -| #p #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2 - elim (lifts_inv_bind1 … H1) -H1 #W1 #U1 #_ #_ #H destruct - elim (lifts_inv_bind1 … H2) -H2 #W2 #U2 #_ #_ #H destruct - /1 width=1 by theq_pair/ -| #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2 - elim (lifts_inv_flat1 … H1) -H1 #W1 #U1 #_ #_ #H destruct - elim (lifts_inv_flat1 … H2) -H2 #W2 #U2 #_ #_ #H destruct - /1 width=1 by theq_pair/ +[ #s1 #s2 #f #X #H + >(lifts_inv_sort1 … H) -H + /2 width=3 by toeq_sort, ex2_intro/ +| #i #f #X #H + elim (lifts_inv_lref1 … H) -H #j #Hj #H destruct + /3 width=3 by toeq_lref, lifts_lref, ex2_intro/ +| #l #f #X #H + >(lifts_inv_gref1 … H) -H + /2 width=3 by toeq_gref, ex2_intro/ +| #p #I #V1 #V2 #T1 #T2 #f #X #H + elim (lifts_inv_bind1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1 + elim (lifts_total V2 f) #W2 #HVW2 + elim (lifts_total T2 (⫯f)) #U2 #HTU2 + /3 width=3 by toeq_pair, lifts_bind, ex2_intro/ +| #I #V1 #V2 #T1 #T2 #f #X #H + elim (lifts_inv_flat1 … H) -H #W1 #U1 #_ #_ #H destruct -V1 -T1 + elim (lifts_total V2 f) #W2 #HVW2 + elim (lifts_total T2 f) #U2 #HTU2 + /3 width=3 by toeq_pair, lifts_flat, ex2_intro/ ] qed-. -(* Inversion lemmas with tail sort-irrelevant head equivalence for terms ****) +lemma toeq_lifts_dx: liftable2_dx toeq. +/3 width=3 by toeq_lifts_sn, liftable2_sn_dx, toeq_sym/ qed-. + +lemma toeq_lifts_bi: liftable2_bi toeq. +/3 width=6 by toeq_lifts_sn, liftable2_sn_bi/ qed-. + +(* Inversion lemmas with sort-irrelevant outer equivalence for terms ********) -lemma theq_inv_lifts_bi: deliftable2_bi theq. +lemma toeq_inv_lifts_bi: deliftable2_bi toeq. #U1 #U2 #H elim H -U1 -U2 [||| * ] [ #s1 #s2 #f #X1 #H1 #X2 #H2 >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2 - /1 width=1 by theq_sort/ + /1 width=1 by toeq_sort/ | #j #f #X1 #H1 #X2 #H2 elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct <(at_inj … Hj2 … Hj1) -j -f -i1 - /1 width=1 by theq_lref/ + /1 width=1 by toeq_lref/ | #l #f #X1 #H1 #X2 #H2 >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2 - /1 width=1 by theq_gref/ + /1 width=1 by toeq_gref/ | #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2 - elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct - elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct - /1 width=1 by theq_pair/ + elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1 + elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2 + /1 width=1 by toeq_pair/ | #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2 - elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct - elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct - /1 width=1 by theq_pair/ + elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1 + elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2 + /1 width=1 by toeq_pair/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma new file mode 100644 index 000000000..3802cb1d4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/syntax/tweq.ma". +include "static_2/relocation/lifts_lifts.ma". + +(* GENERIC RELOCATION FOR TERMS *********************************************) + +(* Properties with sort-irrelevant whd equivalence for terms ****************) + +lemma tweq_lifts_sn: liftable2_sn tweq. +#T1 #T2 #H elim H -T1 -T2 +[ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H + /3 width=3 by lifts_sort, tweq_sort, ex2_intro/ +| #i #f #X #H elim (lifts_inv_lref1 … H) -H + /3 width=3 by lifts_lref, tweq_lref, ex2_intro/ +| #l #f #X #H >(lifts_inv_gref1 … H) -H + /2 width=3 by lifts_gref, tweq_gref, ex2_intro/ +| #p #V1 #V2 #T1 #T2 #_ #IHT #f #X #H + elim (lifts_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (lifts_total V2 f) #W2 #HVW2 + elim (true_or_false p) #H destruct + [ elim (IHT … HTU1) -T1 [| // ] #U2 #HTU2 #HU12 + | elim (lifts_total T2 (⫯f)) #U2 #HTU2 + ] + /3 width=4 by tweq_abbr_pos, lifts_bind, ex2_intro/ +| #p #V1 #V2 #T1 #T2 #f #X #H + elim (lifts_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (lifts_total V2 f) #W2 #HVW2 + elim (lifts_total T2 (⫯f)) #U2 #HTU2 + /3 width=3 by lifts_bind, ex2_intro/ +| #V1 #V2 #T1 #T2 #_ #IHT #f #X #H + elim (lifts_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (lifts_total V2 f) #W2 #HVW2 + elim (IHT … HTU1) -T1 #U2 #HTU2 #HU12 + /3 width=4 by lifts_flat, tweq_appl, ex2_intro/ +| #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H + elim (lifts_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HVW1) -V1 #W2 #HVW2 #HW12 + elim (IHT … HTU1) -T1 #U2 #HTU2 #HU12 + /3 width=5 by lifts_flat, tweq_cast, ex2_intro/ +] +qed-. + +lemma tweq_lifts_dx: liftable2_dx tweq. +/3 width=3 by tweq_lifts_sn, liftable2_sn_dx, tweq_sym/ qed-. + +lemma tweq_lifts_bi: liftable2_bi tweq. +/3 width=6 by tweq_lifts_sn, liftable2_sn_bi/ qed-. + +(* Inversion lemmas with sort-irrelevant whd equivalence for terms **********) + +lemma tweq_inv_lifts_bi: deliftable2_bi tweq. +#U1 #U2 #H elim H -U1 -U2 +[ #s1 #s2 #f #X1 #H1 #X2 #H2 + >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2 + /1 width=1 by tweq_sort/ +| #j #f #X1 #H1 #X2 #H2 + elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct + elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct + <(at_inj … Hj2 … Hj1) -j -f -i1 + /1 width=1 by tweq_lref/ +| #l #f #X1 #H1 #X2 #H2 + >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2 + /1 width=1 by tweq_gref/ +| #p #W1 #W2 #U1 #U2 #_ #IH #f #X1 #H1 #X2 #H2 + elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #HTU1 #H destruct -W1 + elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #HTU2 #H destruct -W2 + elim (true_or_false p) #H destruct + [ /3 width=3 by tweq_abbr_pos/ + | /1 width=1 by tweq_abbr_neg/ + ] +| #p #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2 + elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1 + elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2 + /1 width=1 by tweq_abst/ +| #W1 #W2 #U1 #U2 #_ #IH #f #X1 #H1 #X2 #H2 + elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #HTU1 #H destruct -W1 + elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #HTU2 #H destruct -W2 + /3 width=3 by tweq_appl/ +| #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X1 #H1 #X2 #H2 + elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct + elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #HVW2 #HTU2 #H destruct + /3 width=3 by tweq_cast/ +] +qed-. + +lemma tweq_inv_abbr_pos_sn_X_lifts_Y_Y (T) (f:rtmap): + ∀V,U. +ⓓV.U ≅ T → ⬆*[f]T ≘ U → ⊥. +@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct +elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V +elim (lifts_inv_bind1 … H2) -H2 #Y1 #Y2 #_ #HXY2 #H destruct +/2 width=7 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/theq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma similarity index 64% rename from matita/matita/contribs/lambdadelta/static_2/syntax/theq.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma index 052f9f775..7206a1d62 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/theq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq.ma @@ -15,21 +15,23 @@ include "static_2/notation/relations/topiso_2.ma". include "static_2/syntax/term.ma". -(* HEAD EQUIVALENCE FOR TERMS ***********************************************) +(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************) (* Basic_2A1: includes: tsts_atom tsts_pair *) -inductive theq: relation term ≝ -| theq_sort: ∀s1,s2. theq (⋆s1) (⋆s2) -| theq_lref: ∀i. theq (#i) (#i) -| theq_gref: ∀l. theq (§l) (§l) -| theq_pair: ∀I,V1,V2,T1,T2. theq (②{I}V1.T1) (②{I}V2.T2) +inductive toeq: relation term ≝ +| toeq_sort: ∀s1,s2. toeq (⋆s1) (⋆s2) +| toeq_lref: ∀i. toeq (#i) (#i) +| toeq_gref: ∀l. toeq (§l) (§l) +| toeq_pair: ∀I,V1,V2,T1,T2. toeq (②{I}V1.T1) (②{I}V2.T2) . -interpretation "head equivalence (term)" 'TopIso T1 T2 = (theq T1 T2). +interpretation + "sort-irrelevant outer equivalence (term)" + 'TopIso T1 T2 = (toeq T1 T2). (* Basic inversion lemmas ***************************************************) -fact theq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 → +fact toeq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 → ∃s2. Y = ⋆s2. #X #Y * -X -Y [ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/ @@ -40,11 +42,11 @@ fact theq_inv_sort1_aux: ∀X,Y. X ⩳ Y → ∀s1. X = ⋆s1 → qed-. (* Basic_1: was just: iso_gen_sort *) -lemma theq_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y → +lemma toeq_inv_sort1: ∀Y,s1. ⋆s1 ⩳ Y → ∃s2. Y = ⋆s2. -/2 width=4 by theq_inv_sort1_aux/ qed-. +/2 width=4 by toeq_inv_sort1_aux/ qed-. -fact theq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i. +fact toeq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i. #X #Y * -X -Y // [ #s1 #s2 #j #H destruct | #I #V1 #V2 #T1 #T2 #j #H destruct @@ -52,20 +54,20 @@ fact theq_inv_lref1_aux: ∀X,Y. X ⩳ Y → ∀i. X = #i → Y = #i. qed-. (* Basic_1: was: iso_gen_lref *) -lemma theq_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i. -/2 width=5 by theq_inv_lref1_aux/ qed-. +lemma toeq_inv_lref1: ∀Y,i. #i ⩳ Y → Y = #i. +/2 width=5 by toeq_inv_lref1_aux/ qed-. -fact theq_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l. +fact toeq_inv_gref1_aux: ∀X,Y. X ⩳ Y → ∀l. X = §l → Y = §l. #X #Y * -X -Y // [ #s1 #s2 #k #H destruct | #I #V1 #V2 #T1 #T2 #k #H destruct ] qed-. -lemma theq_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l. -/2 width=5 by theq_inv_gref1_aux/ qed-. +lemma toeq_inv_gref1: ∀Y,l. §l ⩳ Y → Y = §l. +/2 width=5 by toeq_inv_gref1_aux/ qed-. -fact theq_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 → +fact toeq_inv_pair1_aux: ∀T1,T2. T1 ⩳ T2 → ∀J,W1,U1. T1 = ②{J}W1.U1 → ∃∃W2,U2. T2 = ②{J}W2.U2. #T1 #T2 * -T1 -T2 @@ -78,11 +80,11 @@ qed-. (* Basic_1: was: iso_gen_head *) (* Basic_2A1: was: tsts_inv_pair1 *) -lemma theq_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 → +lemma toeq_inv_pair1: ∀J,W1,U1,T2. ②{J}W1.U1 ⩳ T2 → ∃∃W2,U2. T2 = ②{J}W2. U2. -/2 width=7 by theq_inv_pair1_aux/ qed-. +/2 width=7 by toeq_inv_pair1_aux/ qed-. -fact theq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 → +fact toeq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 → ∀J,W2,U2. T2 = ②{J}W2.U2 → ∃∃W1,U1. T1 = ②{J}W1.U1. #T1 #T2 * -T1 -T2 @@ -94,15 +96,15 @@ fact theq_inv_pair2_aux: ∀T1,T2. T1 ⩳ T2 → qed-. (* Basic_2A1: was: tsts_inv_pair2 *) -lemma theq_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 → +lemma toeq_inv_pair2: ∀J,T1,W2,U2. T1 ⩳ ②{J}W2.U2 → ∃∃W1,U1. T1 = ②{J}W1.U1. -/2 width=7 by theq_inv_pair2_aux/ qed-. +/2 width=7 by toeq_inv_pair2_aux/ qed-. (* Advanced inversion lemmas ************************************************) -lemma theq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 → +lemma toeq_inv_pair: ∀I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳ ②{I2}V2.T2 → I1 = I2. -#I1 #I2 #V1 #V2 #T1 #T2 #H elim (theq_inv_pair1 … H) -H +#I1 #I2 #V1 #V2 #T1 #T2 #H elim (toeq_inv_pair1 … H) -H #V0 #T0 #H destruct // qed-. @@ -110,45 +112,45 @@ qed-. (* Basic_1: was: iso_refl *) (* Basic_2A1: was: tsts_refl *) -lemma theq_refl: reflexive … theq. +lemma toeq_refl: reflexive … toeq. * // -* /2 width=1 by theq_lref, theq_gref/ +* /2 width=1 by toeq_lref, toeq_gref/ qed. (* Basic_2A1: was: tsts_sym *) -lemma theq_sym: symmetric … theq. -#T1 #T2 * -T1 -T2 /2 width=3 by theq_sort/ +lemma toeq_sym: symmetric … toeq. +#T1 #T2 * -T1 -T2 /2 width=3 by toeq_sort/ qed-. (* Basic_2A1: was: tsts_dec *) -lemma theq_dec: ∀T1,T2. Decidable (T1 ⩳ T2). +lemma toeq_dec: ∀T1,T2. Decidable (T1 ⩳ T2). * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] -[ /3 width=1 by theq_sort, or_introl/ +[ /3 width=1 by toeq_sort, or_introl/ |2,3,13: @or_intror #H - elim (theq_inv_sort1 … H) -H #x #H destruct + elim (toeq_inv_sort1 … H) -H #x #H destruct |4,6,14: @or_intror #H - lapply (theq_inv_lref1 … H) -H #H destruct + lapply (toeq_inv_lref1 … H) -H #H destruct |5: elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ @or_intror #H - lapply (theq_inv_lref1 … H) -H #H destruct /2 width=1 by/ + lapply (toeq_inv_lref1 … H) -H #H destruct /2 width=1 by/ |7,8,15: @or_intror #H - lapply (theq_inv_gref1 … H) -H #H destruct + lapply (toeq_inv_gref1 … H) -H #H destruct |9: elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ @or_intror #H - lapply (theq_inv_gref1 … H) -H #H destruct /2 width=1 by/ + lapply (toeq_inv_gref1 … H) -H #H destruct /2 width=1 by/ |10,11,12: @or_intror #H - elim (theq_inv_pair1 … H) -H #X1 #X2 #H destruct + elim (toeq_inv_pair1 … H) -H #X1 #X2 #H destruct |16: elim (eq_item2_dec I1 I2) #HI12 destruct - [ /3 width=1 by theq_pair, or_introl/ ] + [ /3 width=1 by toeq_pair, or_introl/ ] @or_intror #H - lapply (theq_inv_pair … H) -H /2 width=1 by/ + lapply (toeq_inv_pair … H) -H /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma similarity index 83% rename from matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma index d9f59e4a5..00d96949c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple.ma @@ -13,19 +13,19 @@ (**************************************************************************) include "static_2/syntax/term_simple.ma". -include "static_2/syntax/theq.ma". +include "static_2/syntax/toeq.ma". -(* HEAD EQUIVALENCE FOR TERMS ***********************************************) +(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************) (* Properies with simple (neutral) terms ************************************) (* Basic_2A1: was: simple_tsts_repl_dx *) -lemma simple_theq_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +lemma simple_toeq_repl_dx: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #T1 #T2 * -T1 -T2 // #I #V1 #V2 #T1 #T2 #H elim (simple_inv_pair … H) -H #J #H destruct // qed-. (* Basic_2A1: was: simple_tsts_repl_sn *) -lemma simple_theq_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=3 by simple_theq_repl_dx, theq_sym/ qed-. +lemma simple_toeq_repl_sn: ∀T1,T2. T1 ⩳ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=3 by simple_toeq_repl_dx, toeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple_vector.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma index 471389125..92e28c878 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_simple_vector.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_simple_vector.ma @@ -13,17 +13,17 @@ (**************************************************************************) include "static_2/syntax/term_vector.ma". -include "static_2/syntax/theq_simple.ma". +include "static_2/syntax/toeq_simple.ma". -(* HEAD EQUIVALENCE FOR TERMS ***********************************************) +(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************) (* Advanced inversion lemmas with simple (neutral) terms ********************) (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) (* Basic_2A1: was: tsts_inv_bind_applv_simple *) -lemma theq_inv_applv_bind_simple (p) (I): +lemma toeq_inv_applv_bind_simple (p) (I): ∀Vs,V2,T1,T2. ⒶVs.T1 ⩳ ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥. -#p #I #Vs #V2 #T1 #T2 #H elim (theq_inv_pair2 … H) -H +#p #I #Vs #V2 #T1 #T2 #H elim (toeq_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize [ #H destruct #H /2 width=5 by simple_inv_bind/ | #V #Vs #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma similarity index 84% rename from matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma index b70559d87..73be8f600 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_tdeq.ma @@ -13,12 +13,12 @@ (**************************************************************************) include "static_2/syntax/tdeq.ma". -include "static_2/syntax/theq.ma". +include "static_2/syntax/toeq.ma". -(* HEAD EQUIVALENCE FOR TERMS ***********************************************) +(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************) (* Properties with sort-irrelevant equivalence for terms ********************) -lemma tdeq_theq: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2. -#T1 #T2 * -T1 -T2 /2 width=1 by theq_sort, theq_pair/ +lemma tdeq_toeq: ∀T1,T2. T1 ≛ T2 → T1 ⩳ T2. +#T1 #T2 * -T1 -T2 /2 width=1 by toeq_sort, toeq_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_theq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/static_2/syntax/theq_theq.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma index 6b33049ee..9b7af0a51 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/theq_theq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/toeq_toeq.ma @@ -12,29 +12,29 @@ (* *) (**************************************************************************) -include "static_2/syntax/theq.ma". +include "static_2/syntax/toeq.ma". -(* HEAD EQUIVALENCE FOR TERMS ***********************************************) +(* SORT-IRRELEVANT OUTER EQUIVALENCE FOR TERMS ******************************) (* Main properties **********************************************************) (* Basic_1: was: iso_trans *) (* Basic_2A1: was: tsts_trans *) -theorem theq_trans: Transitive … theq. +theorem toeq_trans: Transitive … toeq. #T1 #T * -T1 -T [ #s1 #s #X #H - elim (theq_inv_sort1 … H) -s /2 width=1 by theq_sort/ -| #i1 #i #H <(theq_inv_lref1 … H) -H // -| #l1 #l #H <(theq_inv_gref1 … H) -H // + elim (toeq_inv_sort1 … H) -s /2 width=1 by toeq_sort/ +| #i1 #i #H <(toeq_inv_lref1 … H) -H // +| #l1 #l #H <(toeq_inv_gref1 … H) -H // | #I #V1 #V #T1 #T #X #H - elim (theq_inv_pair1 … H) -H #V2 #T2 #H destruct // + elim (toeq_inv_pair1 … H) -H #V2 #T2 #H destruct // ] qed-. (* Basic_2A1: was: tsts_canc_sn *) -theorem theq_canc_sn: left_cancellable … theq. -/3 width=3 by theq_trans, theq_sym/ qed-. +theorem toeq_canc_sn: left_cancellable … toeq. +/3 width=3 by toeq_trans, toeq_sym/ qed-. (* Basic_2A1: was: tsts_canc_dx *) -theorem theq_canc_dx: right_cancellable … theq. -/3 width=3 by theq_trans, theq_sym/ qed-. +theorem toeq_canc_dx: right_cancellable … toeq. +/3 width=3 by toeq_trans, toeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma new file mode 100644 index 000000000..fd31eb05e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma @@ -0,0 +1,288 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/approxeq_2.ma". +include "static_2/syntax/term_weight.ma". + +lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}. +#I #V #T /2 width=1 by le_S_S/ +qed. + +(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************) + +inductive tweq: relation term ≝ +| tweq_sort: ∀s1,s2. tweq (⋆s1) (⋆s2) +| tweq_lref: ∀i. tweq (#i) (#i) +| tweq_gref: ∀l. tweq (§l) (§l) +| tweq_abbr: ∀p,V1,V2,T1,T2. (p=Ⓣ→tweq T1 T2) → tweq (ⓓ{p}V1.T1) (ⓓ{p}V2.T2) +| tweq_abst: ∀p,V1,V2,T1,T2. tweq (ⓛ{p}V1.T1) (ⓛ{p}V2.T2) +| tweq_appl: ∀V1,V2,T1,T2. tweq T1 T2 → tweq (ⓐV1.T1) (ⓐV2.T2) +| tweq_cast: ∀V1,V2,T1,T2. tweq V1 V2 → tweq T1 T2 → tweq (ⓝV1.T1) (ⓝV2.T2) +. + +interpretation + "context-free tail sort-irrelevant equivalence (term)" + 'ApproxEq T1 T2 = (tweq T1 T2). + +(* Basic properties *********************************************************) + +lemma tweq_abbr_pos: ∀V1,V2,T1,T2. T1 ≅ T2 → +ⓓV1.T1 ≅ +ⓓV2.T2. +/3 width=1 by tweq_abbr/ qed. + +lemma tweq_abbr_neg: ∀V1,V2,T1,T2. -ⓓV1.T1 ≅ -ⓓV2.T2. +#V1 #V2 #T1 #T2 +@tweq_abbr #H destruct +qed. + +lemma tweq_refl: reflexive … tweq. +#T elim T -T * [||| #p * | * ] +/2 width=1 by tweq_sort, tweq_lref, tweq_gref, tweq_abbr, tweq_abst, tweq_appl, tweq_cast/ +qed. + +lemma tweq_sym: symmetric … tweq. +#T1 #T2 #H elim H -T1 -T2 +/3 width=3 by tweq_sort, tweq_lref, tweq_gref, tweq_abbr, tweq_abst, tweq_appl, tweq_cast/ +qed-. + +(* Left basic inversion lemmas **********************************************) + +fact tweq_inv_sort_sn_aux: + ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 → ∃s2. Y = ⋆s2. +#X #Y * -X -Y +[1 : #s1 #s2 #s #H destruct /2 width=2 by ex_intro/ +|2,3: #i #s #H destruct +|4 : #p #V1 #V2 #T1 #T2 #_ #s #H destruct +|5 : #p #V1 #V2 #T1 #T2 #s #H destruct +|6 : #V1 #V2 #T1 #T2 #_ #s #H destruct +|7 : #V1 #V2 #T1 #T2 #_ #_ #s #H destruct +] +qed-. + +lemma tweq_inv_sort_sn: + ∀Y,s1. ⋆s1 ≅ Y → ∃s2. Y = ⋆s2. +/2 width=4 by tweq_inv_sort_sn_aux/ qed-. + +fact tweq_inv_lref_sn_aux: + ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i. +#X #Y * -X -Y +[1 : #s1 #s2 #j #H destruct +|2,3: // +|4 : #p #V1 #V2 #T1 #T2 #_ #j #H destruct +|5 : #p #V1 #V2 #T1 #T2 #j #H destruct +|6 : #V1 #V2 #T1 #T2 #_ #j #H destruct +|7 : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct +] +qed-. + +lemma tweq_inv_lref_sn: ∀Y,i. #i ≅ Y → Y = #i. +/2 width=5 by tweq_inv_lref_sn_aux/ qed-. + +fact tweq_inv_gref_sn_aux: + ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l. +#X #Y * -X -Y +[1 : #s1 #s2 #k #H destruct +|2,3: // +|4 : #p #V1 #V2 #T1 #T2 #_ #k #H destruct +|5 : #p #V1 #V2 #T1 #T2 #k #H destruct +|6 : #V1 #V2 #T1 #T2 #_ #k #H destruct +|7 : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct +] +qed-. + +lemma tweq_inv_gref_sn: + ∀Y,l. §l ≅ Y → Y = §l. +/2 width=5 by tweq_inv_gref_sn_aux/ qed-. + +fact tweq_inv_abbr_sn_aux: + ∀X,Y. X ≅ Y → ∀p,V1,T1. X = ⓓ{p}V1.T1 → + ∃∃V2,T2. p = Ⓣ → T1 ≅ T2 & Y = ⓓ{p}V2.T2. +#X #Y * -X -Y +[1 : #s1 #s2 #q #W1 #U1 #H destruct +|2,3: #i #q #W1 #U1 #H destruct +|4 : #p #V1 #V2 #T1 #T2 #HT #q #W1 #U1 #H destruct /3 width=4 by ex2_2_intro/ +|5 : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct +|6 : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct +|7 : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct +] +qed-. + +lemma tweq_inv_abbr_sn: + ∀p,V1,T1,Y. ⓓ{p}V1.T1 ≅ Y → + ∃∃V2,T2. p = Ⓣ → T1 ≅ T2 & Y = ⓓ{p}V2.T2. +/2 width=4 by tweq_inv_abbr_sn_aux/ qed-. + +fact tweq_inv_abst_sn_aux: + ∀X,Y. X ≅ Y → ∀p,V1,T1. X = ⓛ{p}V1.T1 → + ∃∃V2,T2. Y = ⓛ{p}V2.T2. +#X #Y * -X -Y +[1 : #s1 #s2 #q #W1 #U1 #H destruct +|2,3: #i #q #W1 #U1 #H destruct +|4 : #p #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct +|5 : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/ +|6 : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct +|7 : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct +] +qed-. + +lemma tweq_inv_abst_sn: + ∀p,V1,T1,Y. ⓛ{p}V1.T1 ≅ Y → + ∃∃V2,T2. Y = ⓛ{p}V2.T2. +/2 width=5 by tweq_inv_abst_sn_aux/ qed-. + +fact tweq_inv_appl_sn_aux: + ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓐV1.T1 → + ∃∃V2,T2. T1 ≅ T2 & Y = ⓐV2.T2. +#X #Y * -X -Y +[1 : #s1 #s2 #W1 #U1 #H destruct +|2,3: #i #W1 #U1 #H destruct +|4 : #p #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct +|5 : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct +|6 : #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct /2 width=4 by ex2_2_intro/ +|7 : #V1 #V2 #T1 #T2 #_ #_ #W1 #U1 #H destruct +] +qed-. + +lemma tweq_inv_appl_sn: + ∀V1,T1,Y. ⓐV1.T1 ≅ Y → + ∃∃V2,T2. T1 ≅ T2 & Y = ⓐV2.T2. +/2 width=4 by tweq_inv_appl_sn_aux/ qed-. + +fact tweq_inv_cast_sn_aux: + ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 → + ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2. +#X #Y * -X -Y +[1 : #s1 #s2 #W1 #U1 #H destruct +|2,3: #i #W1 #U1 #H destruct +|4 : #p #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct +|5 : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct +|6 : #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct +|7 : #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma tweq_inv_cast_sn: + ∀V1,T1,Y. ⓝV1.T1 ≅ Y → + ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2. +/2 width=3 by tweq_inv_cast_sn_aux/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma tweq_inv_abbr_pos_sn: + ∀V1,T1,Y. +ⓓV1.T1 ≅ Y → ∃∃V2,T2. T1 ≅ T2 & Y = +ⓓV2.T2. +#V1 #V2 #Y #H +elim (tweq_inv_abbr_sn … H) -H #V2 #T2 +/3 width=4 by ex2_2_intro/ +qed-. + +lemma tweq_inv_abbr_neg_sn: + ∀V1,T1,Y. -ⓓV1.T1 ≅ Y → ∃∃V2,T2. Y = -ⓓV2.T2. +#V1 #V2 #Y #H +elim (tweq_inv_abbr_sn … H) -H #V2 #T2 #_ +/2 width=3 by ex1_2_intro/ +qed-. + +lemma tweq_inv_abbr_pos_bi: + ∀V1,V2,T1,T2. +ⓓV1.T1 ≅ +ⓓV2.T2 → T1 ≅ T2. +#V1 #V2 #T1 #T2 #H +elim (tweq_inv_abbr_pos_sn … H) -H #W2 #U2 #HTU #H destruct // +qed-. + +lemma tweq_inv_appl_bi: + ∀V1,V2,T1,T2. ⓐV1.T1 ≅ ⓐV2.T2 → T1 ≅ T2. +#V1 #V2 #T1 #T2 #H +elim (tweq_inv_appl_sn … H) -H #W2 #U2 #HTU #H destruct // +qed-. + +lemma tweq_inv_cast_bi: + ∀V1,V2,T1,T2. ⓝV1.T1 ≅ ⓝV2.T2 → ∧∧ V1 ≅ V2 & T1 ≅ T2. +#V1 #V2 #T1 #T2 #H +elim (tweq_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct +/2 width=1 by conj/ +qed-. + +lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥. +@(f_ind … tw) #n #IH #T #Hn #V #H destruct +elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V +/2 width=4 by/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma tweq_fwd_pair_sn (I): + ∀V1,T1,X2. ②{I}V1.T1 ≅ X2 → ∃∃V2,T2. X2 = ②{I}V2.T2. +* [ #p ] * [ cases p -p ] #V1 #T1 #X2 #H +[ elim (tweq_inv_abbr_pos_sn … H) -H #V2 #T2 #_ #H +| elim (tweq_inv_abbr_neg_sn … H) -H #V2 #T2 #H +| elim (tweq_inv_abst_sn … H) -H #V2 #T2 #H +| elim (tweq_inv_appl_sn … H) -H #V2 #T2 #_ #H +| elim (tweq_inv_cast_sn … H) -H #V2 #T2 #_ #_ #H +] /2 width=3 by ex1_2_intro/ +qed-. + +lemma tweq_fwd_pair_bi (I1) (I2): + ∀V1,V2,T1,T2. ②{I1}V1.T1 ≅ ②{I2}V2.T2 → I1 = I2. +#I1 #I2 #V1 #V2 #T1 #T2 #H +elim (tweq_fwd_pair_sn … H) -H #W2 #U2 #H destruct // +qed-. + +(* Advanced properties ******************************************************) + +lemma tweq_dec: ∀T1,T2. Decidable (T1 ≅ T2). +#T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] +[ /3 width=1 by tweq_sort, or_introl/ +|2,3,13: + @or_intror #H + elim (tweq_inv_sort_sn … H) -H #x #H destruct +|4,6,14: + @or_intror #H + lapply (tweq_inv_lref_sn … H) -H #H destruct +|5: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (tweq_inv_lref_sn … H) -H #H destruct /2 width=1 by/ +|7,8,15: + @or_intror #H + lapply (tweq_inv_gref_sn … H) -H #H destruct +|9: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (tweq_inv_gref_sn … H) -H #H destruct /2 width=1 by/ +|10,11,12: + @or_intror #H + elim (tweq_fwd_pair_sn … H) -H #X1 #X2 #H destruct +|16: + elim (eq_item2_dec I1 I2) #HI12 destruct + [ cases I2 -I2 [ #p ] * [ cases p -p ] + [ elim (IHT T2) -IHT #HT12 + [ /3 width=1 by tweq_abbr_pos, or_introl/ + | /4 width=3 by tweq_inv_abbr_pos_bi, or_intror/ + ] + | /3 width=1 by tweq_abbr_neg, or_introl/ + | /3 width=1 by tweq_abst, or_introl/ + | elim (IHT T2) -IHT #HT12 + [ /3 width=1 by tweq_appl, or_introl/ + | /4 width=3 by tweq_inv_appl_bi, or_intror/ + ] + | elim (IHV V2) -IHV #HV12 + elim (IHT T2) -IHT #HT12 + [1: /3 width=1 by tweq_cast, or_introl/ + |*: @or_intror #H + elim (tweq_inv_cast_bi … H) -H #HV12 #HT12 + /2 width=1 by/ + ] + ] + | /4 width=5 by tweq_fwd_pair_bi, or_intror/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_cnh.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_simple.ma similarity index 70% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_cnh.ma rename to matita/matita/contribs/lambdadelta/static_2/syntax/tweq_simple.ma index 7a65df8d3..4077d0568 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_cnh.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_simple.ma @@ -12,15 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/cpm.ma". -include "basic_2/rt_transition/cnh.ma". +include "static_2/syntax/term_simple.ma". +include "static_2/syntax/tweq.ma". -(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) +(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************) -(* Advanced properties ******************************************************) +(* Properties with simple terms *********************************************) -axiom cnh_cpm_trans (h) (n) (G) (L): - ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄. -(* -#h #n #G #L #T1 #T2 #HT1 #n #T2 #HT12 #k #X #HX -*) +lemma tweq_simple_trans: + ∀T1,T2. T1 ≅ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +#T1 #T2 * -T1 -T2 +[4,5: #p #V1 #V2 #T1 #T2 [ #_ ] #H + elim (simple_inv_bind … H) +|* : /1 width=1 by simple_atom, simple_flat/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tweq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tweq.ma new file mode 100644 index 000000000..afa33ccfb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tweq.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/syntax/tweq.ma". + +(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************) + +(* Main properties **********************************************************) + +theorem tweq_trans: Transitive … tweq. +#T1 #T #H elim H -T1 -T +[ #s1 #s #X #H + elim (tweq_inv_sort_sn … H) -s #s2 destruct + /2 width=1 by tweq_sort/ +| #i1 #i #H // +| #l1 #l #H // +| #p #V1 #V #T1 #T #_ #IHT #X #H + elim (tweq_inv_abbr_sn … H) -H #V2 #T2 #HT #H destruct + /4 width=1 by tweq_abbr/ +| #p #V1 #V #T1 #T #X #H + elim (tweq_inv_abst_sn … H) -H #V2 #T2 #H destruct + /2 width=1 by tweq_abst/ +| #V1 #V #T1 #T #_ #IHT #X #H + elim (tweq_inv_appl_sn … H) -H #V2 #T2 #HT #H destruct + /3 width=1 by tweq_appl/ +| #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H + elim (tweq_inv_cast_sn … H) -H #V2 #T2 #HV #HT #H destruct + /3 width=1 by tweq_cast/ +] +qed-. + +theorem tweq_canc_sn: left_cancellable … tweq. +/3 width=3 by tweq_trans, tweq_sym/ qed-. + +theorem tweq_canc_dx: right_cancellable … tweq. +/3 width=3 by tweq_trans, tweq_sym/ qed-. + +theorem tweq_repl: + ∀T1,T2. T1 ≅ T2 → ∀U1. T1 ≅ U1 → ∀U2. T2 ≅ U2 → U1 ≅ U2. +/3 width=3 by tweq_canc_sn, tweq_trans/ qed-. 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 07bc1856a..5fb750e3f 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 @@ -86,7 +86,7 @@ table { [ { "generic and uniform relocation" * } { [ [ "for binders" ] "lifts_bind" + "( ⬆*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] [ [ "for term vectors" ] "lifts_vector" + "( ⬆*[?] ? ≘ ? )" "lifts_lifts_vector" * ] - [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tueq" + "lifts_lifts" * ] + [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_toeq" + "lifts_lifts" * ] } ] [ { "syntactic equivalence" * } { @@ -115,8 +115,12 @@ table { [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ] } ] - [ { "sort-irrelevant head equivalence" * } { - [ [ "for terms" ] "theq" + "( ? ⩳ ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] + [ { "sort-irrelevant outer equivalence" * } { + [ [ "for terms" ] "toeq" + "( ? ⩳ ? )" "toeq_simple" + "toeq_tdeq" + "toeq_toeq" + "toeq_simple_vector" * ] + } + ] + [ { "sort-irrelevant whd equivalence" * } { + [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tueq" * ] } ] [ { "sort-irrelevant equivalence" * } { -- 2.39.2