From 31be09cc0d040577917783e050e1d38c0daa8f01 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 16 Apr 2019 23:11:59 +0200 Subject: [PATCH] milestone in basic_2 with additions in static_2 + validity is decidable + some renaming + batch compilation handles each specification separately otherwise matitac opens too many files --- .../basic_2/dynamic/cnv_cpm_conf.ma | 6 +- .../lambdadelta/basic_2/dynamic/cnv_cpme.ma | 7 + .../lambdadelta/basic_2/dynamic/cnv_cpue.ma | 48 ++++++ .../lambdadelta/basic_2/dynamic/cnv_drops.ma | 29 +++- .../lambdadelta/basic_2/dynamic/cnv_eval.ma | 124 +++++++++++++++ .../basic_2/dynamic/cnv_preserve.ma | 21 +++ .../{cnv_cpes_dec.ma => cnv_preserve_cpes.ma} | 11 ++ .../lambdadelta/basic_2/dynamic/nta_cpms.ma | 2 +- .../notation/relations/prediteval_5.ma | 16 ++ .../{predtywhead_4.ma => preditnormal_4.ma} | 4 +- .../basic_2/rt_computation/cpms_cnu.ma | 27 ++++ .../basic_2/rt_computation/cpms_cwhx.ma | 75 --------- .../basic_2/rt_computation/cpue.ma | 25 +++ .../basic_2/rt_computation/cpue_csx.ma | 32 ++++ .../basic_2/rt_computation/lprs_cpms.ma | 10 +- .../basic_2/rt_equivalence/cpcs_csx.ma | 40 +++++ .../basic_2/rt_equivalence/cpes_cprs.ma | 28 ++++ .../basic_2/rt_transition/cnr_tdeq.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cnu.ma | 61 ++++++++ .../basic_2/rt_transition/cnu_cnr.ma | 37 +++++ .../basic_2/rt_transition/cnu_cnr_simple.ma | 29 ++++ .../basic_2/rt_transition/cnu_cnu.ma | 29 ++++ .../basic_2/rt_transition/cnu_drops.ma | 52 +++++++ .../basic_2/rt_transition/cnu_lifts.ma | 32 ++++ .../basic_2/rt_transition/cnu_tdeq.ma | 98 ++++++++++++ .../basic_2/rt_transition/cpm_tueq.ma | 90 +++++++++++ .../lambdadelta/basic_2/rt_transition/cwhx.ma | 116 -------------- .../basic_2/rt_transition/cwhx_drops.ma | 46 ------ .../basic_2/rt_transition/cwhx_rdeq.ma | 41 ----- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 4 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 25 +-- .../contribs/lambdadelta/compile_partial.sh | 5 +- .../matita/contribs/lambdadelta/partial.txt | 4 - .../static_2/notation/relations/approxeq_2.ma | 19 +++ .../lambdadelta/static_2/relocation/lifts.ma | 11 +- .../static_2/relocation/lifts_tdeq.ma | 3 + .../static_2/relocation/lifts_tueq.ma | 80 ++++++++++ .../lambdadelta/static_2/syntax/tueq.ma | 143 ++++++++++++++++++ .../lambdadelta/static_2/syntax/tueq_tueq.ma | 44 ++++++ .../lambdadelta/static_2/web/static_2_src.tbl | 8 +- matita/matita/predefined_virtuals.ml | 2 +- 41 files changed, 1171 insertions(+), 315 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpue.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{cnv_cpes_dec.ma => cnv_preserve_cpes.ma} (80%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/prediteval_5.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predtywhead_4.ma => preditnormal_4.ma} (87%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnu.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue_csx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cprs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr_simple.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnu.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_lifts.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_tdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tueq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma delete mode 100644 matita/matita/contribs/lambdadelta/partial.txt create mode 100644 matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tueq.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tueq_tueq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma index 3e6527a02..f0eb6355b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma @@ -40,7 +40,7 @@ fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i): ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T. #a #h #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2 -lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV +lapply (cnv_inv_lref_pair … HT … HLK) -HT #HV elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #HV1 #H destruct elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2 @@ -62,7 +62,7 @@ fact cnv_cpm_conf_lpr_atom_ell_aux (a) (h) (G) (L) (i): ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T. #a #h #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2 -lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW +lapply (cnv_inv_lref_pair … HT … HLK) -HT #HW elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK1 #HW1 #H destruct elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2 @@ -87,7 +87,7 @@ fact cnv_cpm_conf_lpr_delta_delta_aux (a) (h) (I) (G) (L) (i): #K #V #HLK #Y #X #HLY #n1 #XV1 #HVX1 #n2 #XV2 #HVX2 #X1 #HXV1 #X2 #HXV2 #L1 #HL1 #L2 #HL2 lapply (drops_mono … HLY … HLK) -HLY #H destruct -lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV +lapply (cnv_inv_lref_pair … HT … HLK) -HT #HV elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #_ #H destruct lapply (drops_isuni_fwd_drop2 … HLK1) -V1 // #HLK1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma index dd3d99a30..be0443bca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma @@ -20,6 +20,13 @@ include "basic_2/dynamic/cnv_preserve.ma". (* Properties with evaluation for t-bound rt-transition on terms ************) +lemma cnv_cpme_trans (a) (h) (n) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h]. +#a #h #n #G #L #T1 #HT1 #T2 * #HT12 #_ +/2 width=4 by cnv_cpms_trans/ +qed-. + lemma cnv_cpme_cpms_conf (a) (h) (n) (G) (L): ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpue.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpue.ma new file mode 100644 index 000000000..a84fd5cd2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpue.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cpms_cnu.ma". +include "basic_2/rt_computation/cpue.ma". +include "basic_2/dynamic/cnv_preserve.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with evaluation for t-unbound rt-transition on terms **********) + +lemma cnv_cpue_trans (a) (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀T2. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h]. +#a #h #G #L #T1 #HT1 #T2 * #n #HT12 #_ +/2 width=4 by cnv_cpms_trans/ +qed-. + +lemma cnv_cpue_cpms_conf (a) (h) (n) (G) (L): + ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T0 ➡*[n,h] T1 → + ∀T2. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T2⦄ → + ∃∃T. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T⦄ & T2 ≅ T. +#a #h #n1 #G #L #T0 #HT0 #T1 #HT01 #T2 * #n2 #HT02 #HT2 +elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20 +lapply (cpms_inv_cnu_sn … HT20 HT2) -HT20 #HT20 +/4 width=8 by cnu_tueq_trans, ex2_intro/ +qed-. + +(* Main properties with evaluation for t-unbound rt-transition on terms *****) + +theorem cnv_cpue_mono (a) (h) (G) (L): + ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T1⦄ → + ∀T2. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃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 +/3 width=8 by cpms_inv_cnu_sn, tueq_canc_dx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma index 8c95ffcf6..7bcc3f1fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma @@ -49,15 +49,30 @@ lemma cnv_inv_lref_drops (a) (h) (G): ] qed-. -(* Advanced forward lemmas **************************************************) - -lemma cnv_lref_fwd_drops (a) (h) (G): - ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] → - ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ![a, h]. -#a #h #o #i #L #H #I #K #V #HLK +lemma cnv_inv_lref_pair (a) (h) (G): + ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] → + ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ![a, h]. +#a #h #G #i #L #H #I #K #V #HLK elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #HX lapply (drops_mono … HLY … HLK) -L #H destruct // -qed-. +qed-. + +lemma cnv_inv_lref_atom (a) (h) (b) (G): + ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] → + ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⊥. +#a #h #b #G #i #L #H #Hi +elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_ +lapply (drops_gen b … HLY) -HLY #HLY +lapply (drops_mono … HLY … Hi) -L #H destruct +qed-. + +lemma cnv_inv_lref_unit (a) (h) (G): + ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] → + ∀I,K. ⬇*[i] L ≘ K.ⓤ{I} → ⊥. +#a #h #G #i #L #H #I #K #HLK +elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #_ +lapply (drops_mono … HLY … HLK) -L #H destruct +qed-. (* Properties with generic slicing for local environments *******************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma new file mode 100644 index 000000000..0052d7cb4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma @@ -0,0 +1,124 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpue_csx.ma". +include "basic_2/rt_equivalence/cpes_cprs.ma". +include "basic_2/dynamic/cnv_cpue.ma". +include "basic_2/dynamic/cnv_cpes.ma". +include "basic_2/dynamic/cnv_preserve_cpes.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ{p}W.T + | (∀p,W,T. X = ⓛ{p}W.T → ⊥). +* [ #I | * [ #p * | #I ] #V #T ] +[3: /3 width=4 by ex1_3_intro, or_introl/ ] +@or_intror #q #W #U #H destruct +qed-. + +(* main properties with evaluations for rt-transition on terms **************) + +theorem cnv_dec (a) (h) (G) (L) (T): + Decidable (⦃G,L⦄ ⊢ T ![a,h]). +#a #h #G #L #T +@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ] +[ #s #HG #HL #HT destruct -IH + /2 width=1 by cnv_sort, or_introl/ +| #i #HG #HL #HT destruct + elim (drops_F_uni L i) [| * * ] + [ /3 width=8 by cnv_inv_lref_atom, or_intror/ + | /3 width=9 by cnv_inv_lref_unit, or_intror/ + | #I #V #K #HLK + elim (IH G K V) -IH [3: /2 width=2 by fqup_lref/ ] + [ /3 width=5 by cnv_lref_drops, or_introl/ + | /4 width=5 by cnv_inv_lref_pair, or_intror/ + ] + ] +| #l #HG #HL #HT destruct -IH + /3 width=6 by cnv_inv_gref, or_intror/ +| #p #I #V #T #HG #HL #HT destruct + elim (IH G L V) [| -IH | // ] #HV + [ elim (IH G (L.ⓑ{I}V) T) -IH [3: // ] #HT + [ /3 width=1 by cnv_bind, or_introl/ ] + ] + @or_intror #H + elim (cnv_inv_bind … H) -H /2 width=1 by/ +| #V #T #HG #HL #HT destruct + elim (IH G L V) [| -IH #HV | // ] + [ elim (IH G L T) -IH [| #HT #HV | // ] + [ cases a #HT #HV + [ elim (cnv_fwd_aaa … HT) #A #HA + elim (cpme_total_aaa h 1 … HA) #X + elim (abst_dec X) [ * ] + [ #p #W #U #H #HTU destruct + elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] + [ elim HTU -HTU #HTU #_ + /3 width=7 by cnv_appl_cpes, or_introl/ + | @or_intror #H + elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #HVW0 + >Hm1 -m1 [| // ] #HTU0 + elim (cnv_cpme_cpms_conf … HT … HTU0 … HTU) -T #HU0 #_ + elim (cpms_inv_abst_bi … HU0) -HU0 #_ #HW0 #_ -p -q -U0 + /3 width=3 by cpes_cprs_trans/ + | lapply (cnv_cpme_trans … HT … HTU) -T #H + elim (cnv_inv_bind … H) -H #HW #_ // + ] + | #HnTU #HTX + @or_intror #H + elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #_ + >Hm1 -m1 [| // ] #HTU0 + elim (cnv_cpme_cpms_conf … HT … HTU0 … HTX) -T #HX #_ + elim (cpms_inv_abst_sn … HX) -HX #V0 #T0 #_ #_ #H destruct -W0 -U0 + /2 width=4 by/ + ] + | elim (cpue_total_csx h G L T) + [| /3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ ] #X + elim (abst_dec X) [ * ] + [ #p #W #U #H #HTU destruct + elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] + [ elim HTU -HTU #n #HTU #_ + @or_introl @(cnv_appl_cpes … HV … HT … HVW … HTU) #H destruct + | @or_intror #H + elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0 + elim (cnv_cpue_cpms_conf … HT … HTU0 … HTU) -m1 -T #X * #m2 #HU0X #_ #HUX + elim (tueq_inv_bind1 … HUX) -HUX #X0 #_ #H destruct -U + elim (cpms_inv_abst_bi … HU0X) -HU0X #_ #HW0 #_ -p -q -m2 -U0 -X0 + /3 width=3 by cpes_cprs_trans/ + | lapply (cnv_cpue_trans … HT … HTU) -T #H + elim (cnv_inv_bind … H) -H #HW #_ // + ] + | #HnTU #HTX + @or_intror #H + elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0 + elim (cnv_cpue_cpms_conf … HT … HTU0 … HTX) -m1 -T #X0 * #m2 #HUX0 #_ #HX0 + elim (cpms_inv_abst_sn … HUX0) -HUX0 #V0 #T0 #_ #_ #H destruct -m2 -W0 -U0 + elim (tueq_inv_bind2 … HX0) -HX0 #X0 #_ #H destruct + /2 width=4 by/ + ] + ] + ] + ] + @or_intror #H + elim (cnv_inv_appl_SO … H) -H /2 width=1 by/ +| #U #T #HG #HL #HT destruct + elim (IH G L U) [| -IH | // ] #HU + [ elim (IH G L T) -IH [3: // ] #HT + [ elim (cnv_cpes_dec … 0 1 … HU … HT) #HUT + [ /3 width=1 by cnv_cast_cpes, or_introl/ ] + ] + ] + @or_intror #H + elim (cnv_inv_cast_cpes … H) -H /2 width=1 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma index 483ea690e..297a86498 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -73,3 +73,24 @@ lemma cnv_lprs_trans (a) (h) (G): #a #h #G #L1 #T #HT #L2 #H @(lprs_ind_dx … H) -L2 /2 width=3 by cnv_lpr_trans/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma cnv_inv_appl_SO (a) (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → + ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0. +* #h #G #L #V #T #H +elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU +[ elim (cnv_fwd_cpm_SO … (ⓛ{p}W.U)) + [|*: /2 width=8 by cnv_cpms_trans/ ] #X #HU0 + elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct + lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0 + lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0 + /2 width=7 by ex5_4_intro/ +| lapply (Ha ?) -Ha [ // ] #Ha + lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct + /2 width=7 by ex5_4_intro/ +| @(ex5_4_intro … HV HT HVW HTU) #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes_dec.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma similarity index 80% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes_dec.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma index 60fc0d0da..f266bb581 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes_dec.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma @@ -39,3 +39,14 @@ elim (eq_term_dec U1 U2) [ #H destruct | #HnU12 ] /3 width=6 by cpre_mono/ ] qed-. + +(* Advanced inversion lemmas with t-bound rt-equivalence for terms **********) + +lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → + ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U. +#a #h #G #L #V #T #H +elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU +/3 width=7 by cpms_div, ex5_4_intro/ +qed-. 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 8dbb60c79..b0530a3bb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma @@ -58,6 +58,6 @@ elim (cnv_inv_cast … H) -H #X #HWU #HWT #HUX #HTX elim (cnv_inv_bind … HWU) -HWU #HW #HU elim (cnv_inv_bind … HWT) -HWT #_ #HT elim (cpms_inv_abst_sn … HUX) -HUX #W0 #X0 #_ #HUX0 #H destruct -elim (cpms_inv_abst_bi … HTX) -HTX #_ #HTX0 -W0 +elim (cpms_inv_abst_bi … HTX) -HTX #_ #_ #HTX0 -W0 /3 width=3 by cnv_cast, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prediteval_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prediteval_5.ma new file mode 100644 index 000000000..db0a4aa6d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prediteval_5.ma @@ -0,0 +1,16 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* 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 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PRedITEval $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/preditnormal_4.ma index 05f4ee9c6..881d1ba1d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_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 @{ 'PRedTyWHead $h $G $L $T }. + for @{ 'PRedITNormal $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnu.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnu.ma new file mode 100644 index 000000000..5e7790683 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnu.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cnu_cnu.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Inversion lemmas with normal terms for t-unbound rt-transition ***********) + +lemma cpms_inv_cnu_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 +/5 width=8 by cnu_tueq_trans, tueq_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma deleted file mode 100644 index bfb52bc35..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.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/rt_transition/cpr_tdeq.ma". -include "basic_2/rt_transition/cwhx_drops.ma". -include "basic_2/rt_transition/cwhx_rdeq.ma". -include "basic_2/rt_computation/fsb_aaa.ma". -include "basic_2/rt_computation/cpms_cpms.ma". -include "basic_2/rt_computation/cpms_fpbg.ma". - -(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) - -(* Properties with whd normality for unbound rt-transition ******************) - -lemma aaa_cpms_cwhx (h) (G) (L): - ∀T1,A. ⦃G,L⦄ ⊢ T1 ⁝ A → - ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄. -#h #G #L #T1 #A #H -@(aaa_ind_fpbg h … H) -G -L -T1 -A -#G #L #T1 #A * -G -L -T1 -A -[ #G #L #s #_ /2 width=4 by cwhx_sort, ex2_2_intro/ -| * #G #K #V1 #A #_ #IH -A - elim (IH … G K V1) [2,4: /3 width=1 by fpb_fpbg, fpb_fqu, fqu_lref_O/ ] -IH #n #V2 #HV12 #HV2 - elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2 - /5 width=10 by cpms_ell, cpms_delta, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/ -| #I #G #K #A #i #_ #IH -A - elim (IH … G K (#i)) [| /3 width=1 by fpb_fpbg, fpb_fqu/ ] -IH #n #V2 #HV12 #HV2 - elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2 - /5 width=10 by cpms_lref, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/ -| * #G #L #V #T1 #B #A #_ #_ #IH -B -A - [ elim (cpr_abbr_pos h G L V T1) #T0 #HT10 #HnT10 - elim (IH G L T0) -IH [| /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HnT10 #n #T2 #HT02 #HT2 - /3 width=5 by cpms_step_sn, ex2_2_intro/ - | elim (IH … G (L.ⓓV) T1) -IH [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #n #T2 #HT12 #HT2 - /3 width=5 by cwhx_ldef, cpms_bind_dx, ex2_2_intro/ - ] -| #p #G #L #W #T1 #B #A #_ #_ #_ -B -A - /2 width=5 by cwhx_abst, ex2_2_intro/ -| #G #L #V #T1 #B #A #_ #HT1 #IH - elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n1 #T2 #HT12 #HT2 - elim (tdeq_dec T1 T2) [ -n1 #HT12 | -HT2 #HnT12 ] - [ lapply (tdeq_cwhx_trans … HT2 … HT12) -T2 - @(insert_eq_0 … L) #Y @(insert_eq_0 … T1) #X * -Y -X - [ #L0 #s0 #H1 #H2 destruct -IH - lapply (aaa_inv_sort … HT1) -HT1 #H destruct - | #p #L0 #W0 #T0 #H1 #H2 destruct -HT1 - elim (IH G L0 (ⓓ{p}ⓝW0.V.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_beta, ex2_2_intro/ ] - @fpb_fpbg @fpb_cpx [ /2 width=1 by cpx_beta/ ] #H - elim (tdeq_inv_pair … H) -H #H #_ #_ destruct - | #L0 #V0 #T0 #_ #H1 #H2 destruct -HT1 - elim (lifts_total V (𝐔❴1❵)) #W #HVW - elim (IH G L0 (-ⓓV0.ⓐW.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_theta, ex2_2_intro/ ] - @fpb_fpbg @fpb_cpx [ /2 width=3 by cpx_theta/ ] #H - elim (tdeq_inv_pair … H) -H #H #_ #_ destruct - ] - | elim (IH G L (ⓐV.T2)) -IH [ /4 width=5 by cpms_trans, cpms_appl_dx, ex2_2_intro/ ] - @(cpms_tdneq_fwd_fpbg … n1) [ /2 width=3 by cpms_appl_dx/ ] #H - elim (tdeq_inv_pair … H) -H #_ #_ #H /2 width=1 by/ - ] -| #G #L #U #T1 #A #_ #_ #IH -A - elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n #T2 #HT12 #HT2 - /3 width=4 by cpms_eps, ex2_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma new file mode 100644 index 000000000..95c2b56ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/prediteval_5.ma". +include "basic_2/rt_transition/cnu.ma". +include "basic_2/rt_computation/cpms.ma". + +(* EVALUATION FOR T-UNBOUND RT-TRANSITION ON TERMS **************************) + +definition cpue (h) (G) (L): relation2 term term ≝ + λT1,T2. ∃∃n. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G, L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄. + +interpretation "evaluation for t-unbound context-sensitive parallel rt-transition (term)" + 'PRedITEval h G L T1 T2 = (cpue h G L T1 T2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue_csx.ma new file mode 100644 index 000000000..9c1fb3707 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue_csx.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpm_cpx.ma". +include "basic_2/rt_transition/cnu_tdeq.ma". +include "basic_2/rt_computation/csx.ma". +include "basic_2/rt_computation/cpue.ma". + +(* EVALUATION FOR T-UNBOUND RT-TRANSITION ON TERMS **************************) + +(* Properties with strong normalization for unbound rt-transition for terms *) + +lemma cpue_total_csx (h) (G) (L): + ∀T1. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G, L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T2⦄. +#h #G #L #T1 #H +@(csx_ind … H) -T1 #T1 #_ #IHT1 +elim (cnu_dec_tdeq h G L T1) [ /3 width=4 by ex2_intro, ex_intro/ ] * +#n1 #T0 #HT10 #HnT10 +elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ] +#T2 * #n2 #HT02 #HT2 /4 width=7 by cpms_step_sn, ex2_intro, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma index 0c625a2da..ad24e5876 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma @@ -62,12 +62,12 @@ elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct qed-. (* Basic_2A1: includes: cprs_inv_abst *) -lemma cpms_inv_abst_bi (n) (h) (G) (L): - ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 → - ∧∧ ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2. -#n #h #G #L #p #W1 #W2 #T1 #T2 #H +lemma cpms_inv_abst_bi (n) (h) (p1) (p2) (G) (L): + ∀W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ➡*[n, h] ⓛ{p2}W2.T2 → + ∧∧ p1 = p2 & ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2. +#n #h #p1 #p2 #G #L #W1 #W2 #T1 #T2 #H elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct -/2 width=1 by conj/ +/2 width=1 by and3_intro/ qed-. (* Basic_1: was pr3_gen_abbr *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma new file mode 100644 index 000000000..f37dc4184 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpre_csx.ma". +include "basic_2/rt_computation/cpre_cpre.ma". +include "basic_2/rt_equivalence/cpcs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +(* Properties with strongly normalizing terms for unbound rt-transition *****) + +(* Basic_1: was: cpcs_dec *) +lemma csx_cpcs_dec (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∀T2. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄ → + Decidable … (⦃G,L⦄ ⊢ T1 ⬌*[h] T2). +#h #G #L #T1 #HT1 #T2 #HT2 +elim (cpre_total_csx … HT1) -HT1 #U1 #HTU1 +elim (cpre_total_csx … HT2) -HT2 #U2 #HTU2 +elim (eq_term_dec U1 U2) [ #H destruct | #HnU12 ] +[ cases HTU1 -HTU1 #HTU1 #_ + cases HTU2 -HTU2 #HTU2 #_ + /3 width=3 by cprs_div, or_introl/ +| @or_intror #H + elim (cpcs_inv_cprs … H) -H #T0 #HT10 #HT20 + lapply (cpre_cprs_conf … HT10 … HTU1) -T1 #H1 + lapply (cpre_cprs_conf … HT20 … HTU2) -T2 #H2 + /3 width=6 by cpre_mono/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cprs.ma new file mode 100644 index 000000000..53967448e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cprs.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_equivalence/cpes.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************) + +(* Properties with context-sensitive parallel r-computation on terms ********) + +lemma cpes_cprs_trans (h) (n) (G) (L) (T0): + ∀T1. ⦃G,L⦄ ⊢ T1 ⬌*[h,n,0] T0 → + ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h,n,0] T2. +#h #n #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT02 +elim (cprs_conf … HT0 … HT02) -T0 #T0 #HT0 #HT20 +/3 width=3 by cpms_div, cpms_cprs_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma index 3efc47bba..80e4d8ff0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma @@ -82,7 +82,7 @@ lemma cnr_dec_tdeq (h) (G) (L): elim (tdeq_inv_pair … H) -H #H destruct | @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H elim (tdeq_inv_pair … H) -H #H destruct - ] + ] | #T2 #HT12 #HnT12 #_ @or_intror @(ex2_intro … (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma new file mode 100644 index 000000000..19b1eaf8c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tueq.ma". +include "basic_2/rt_transition/cpm.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +definition cnu (h) (G) (L): predicate term ≝ + λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≅ T2. + +interpretation + "normality for t-unbound context-sensitive parallel rt-transition (term)" + 'PRedITNormal h G L T = (cnu h G L T). + +(* Basic properties *********************************************************) + +lemma cnu_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 cnu_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 cnu_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 cnu_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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr.ma new file mode 100644 index 000000000..ce295d3ed --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cnr.ma". +include "basic_2/rt_transition/cnu.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +(* Advanced properties with normal terms for r-transition *******************) + +lemma cnu_abst (h) (p) (G) (L): + ∀W. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃W⦄ → ∀T.⦃G,L.ⓛW⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓛ{p}W.T⦄. +#h #p #G #L #W1 #HW1 #T1 #HT1 #n #X #H +elim (cpm_inv_abst1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct +<(HW1 … HW12) -W2 /3 width=2 by tueq_bind/ +qed. + +lemma cnu_abbr_neg (h) (G) (L): + ∀V. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ∀T.⦃G,L.ⓓV⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃-ⓓV.T⦄. +#h #G #L #V1 #HV1 #T1 #HT1 #n #X #H +elim (cpm_inv_abbr1 … H) -H * +[ #V2 #T2 #HV12 #HT12 #H destruct + <(HV1 … HV12) -V2 /3 width=2 by tueq_bind/ +| #X1 #_ #_ #H destruct +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr_simple.ma new file mode 100644 index 000000000..056c8e250 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr_simple.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpm_simple.ma". +include "basic_2/rt_transition/cnr.ma". +include "basic_2/rt_transition/cnu.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +(* Advanced properties with simple terms and normal terms for r-transition **) + +lemma cnu_appl_simple (h) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓐV.T⦄. +#h #G #L #V1 #T1 #HV1 #HT1 #HS #n #X #H +elim (cpm_inv_appl1_simple … H HS) -H -HS #V2 #T2 #HV12 #HT12 #H destruct +lapply (HV1 … HV12) -HV1 -HV12 #H destruct +/3 width=2 by tueq_appl/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnu.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnu.ma new file mode 100644 index 000000000..2bc4d3c2d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnu.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tueq_tueq.ma". +include "basic_2/rt_transition/cpm_tueq.ma". +include "basic_2/rt_transition/cnu.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +(* Advanced properties ******************************************************) + +lemma cnu_tueq_trans (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → ∀T2.T1 ≅ T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄. +#h #G #L #T1 #HT1 #T2 #HT12 #n #T0 #HT20 +@(tueq_canc_sn … HT12) +elim (tueq_cpm_trans … HT12 … HT20) -T2 #T2 #HT13 #HT30 +/3 width=3 by tueq_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_drops.ma new file mode 100644 index 000000000..6b6aa0962 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_drops.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tueq.ma". +include "basic_2/rt_transition/cpm_drops.ma". +include "basic_2/rt_transition/cnu.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +(* Advanced properties ******************************************************) + +lemma cnu_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 +lapply (drops_gen b … HLK) -HLK #HLK +lapply (drops_mono … Hi … HLK) -L #H destruct +qed. + +lemma cnu_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 +lapply (drops_mono … HLK … HLY) -L #H destruct +qed. + +(* Properties with generic relocation ***************************************) + +lemma cnu_lifts (h) (G): d_liftable1 … (cnu 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 tueq_lifts_bi/ +qed-. + +(* Inversion lemmas with generic relocation *********************************) + +lemma cnu_inv_lifts (h) (G): d_deliftable1 … (cnu 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 tueq_inv_lifts_bi/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_lifts.ma new file mode 100644 index 000000000..051da519a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_lifts.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/relocation/lifts_tueq.ma". +include "basic_2/rt_transition/cnu.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +(* Advanced properties with uniform relocation for terms ********************) + +lemma cnu_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 + elim (tueq_lifts_dx … HV … HVX) -V #Xi #Hi #HX + lapply (lifts_inv_lref1_uni … Hi) -Hi #H destruct // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_tdeq.ma new file mode 100644 index 000000000..91676f500 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_tdeq.ma @@ -0,0 +1,98 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cnr_tdeq.ma". +include "basic_2/rt_transition/cnu_drops.ma". +include "basic_2/rt_transition/cnu_cnr.ma". +include "basic_2/rt_transition/cnu_cnr_simple.ma". + +(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************) + +(* Properties with context-free sort-irrelevant equivalence for terms *******) + +lemma cnu_dec_tdeq (h) (G) (L): + ∀T1. ∨∨ ⦃G, L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ + | ∃∃n,T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥). +#h #G #L #T1 +@(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 #T0 #IH #G #L * * +[ #s #HG #HL #HT destruct -IH + /3 width=5 by cnu_sort, or_introl/ +| #i #HG #HL #HT destruct -IH + elim (drops_F_uni L i) + [ /3 width=7 by cnu_atom_drops, or_introl/ + | * * [ #I | * #V ] #K #HLK + [ /3 width=8 by cnu_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 + /2 width=5 by lifts_inv_lref2_uni_lt/ + | elim (lifts_total V 𝐔❴↑i❵) #W #HVW + @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H + lapply (tdeq_inv_lref1 … H) -H #H destruct + /2 width=5 by lifts_inv_lref2_uni_lt/ + ] + ] +| #l #HG #HL #HT destruct -IH + /3 width=5 by cnu_gref, or_introl/ +| #p * [ cases p ] #V1 #T1 #HG #HL #HT destruct + [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2 -IH + elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ] + [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2 + @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H + /2 width=7 by tdeq_lifts_inv_pair_sn/ + | @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/ + ] + | elim (cnr_dec_tdeq h G L V1) [ elim (IH G (L.ⓓV1) T1) [| * | // ] | * ] -IH + [ #HT1 #HV1 /3 width=7 by cnu_abbr_neg, or_introl/ + | #n #T2 #HT12 #HnT12 #_ + @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/ + | #V2 #HV12 #HnV12 + @or_intror @(ex2_2_intro … (-ⓓV2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + | elim (cnr_dec_tdeq h G L V1) [ elim (IH G (L.ⓛV1) T1) [| * | // ] | * ] -IH + [ #HT1 #HV1 /3 width=7 by cnu_abst, or_introl/ + | #n #T2 #HT12 #HnT12 #_ + @or_intror @(ex2_2_intro … (ⓛ{p}V1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + | #V2 #HV12 #HnV12 + @or_intror @(ex2_2_intro … (ⓛ{p}V2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + ] +| * #V1 #T1 #HG #HL #HT destruct [| -IH ] + [ elim (cnr_dec_tdeq h G L V1) [ elim (IH G L T1) [| * | // ] | * ] -IH + [ #HT1 #HV1 + elim (simple_dec_ex T1) [| * #p * #W1 #U1 #H destruct ] + [ /3 width=7 by cnu_appl_simple, or_introl/ + | 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 + | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H + elim (tdeq_inv_pair … H) -H #H destruct + ] + | #n #T2 #HT12 #HnT12 #_ + @or_intror @(ex2_2_intro … (ⓐV1.T2)) [1,2: /2 width=2 by cpm_appl/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + | #V2 #HV12 #HnV12 + @or_intror @(ex2_2_intro … (ⓐV2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H + /2 width=4 by tdeq_inv_pair_xy_y/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tueq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tueq.ma new file mode 100644 index 000000000..2baeeefae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tueq.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tueq.ma". +include "basic_2/rt_transition/cpm.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Properties with tail sort-irrelevant equivalence on terms ****************) + +lemma cpm_tueq_conf (h) (n) (G) (L) (T0): + ∀T1. ⦃G,L⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. T0 ≅ T2 → + ∃∃T. ⦃G,L⦄ ⊢ T2 ➡[n,h] T & T1 ≅ T. +#h #n #G #L #T0 #T1 #H @(cpm_ind … H) -G -L -T0 -T1 -n +[ /2 width=3 by ex2_intro/ +| #G #L #s0 #X2 #H2 + elim (tueq_inv_sort1 … H2) -H2 #s2 #H destruct + /3 width=3 by tueq_sort, ex2_intro/ +| #n #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #X2 #H2 + >(tueq_inv_lref1 … H2) -X2 + elim (IH V0) [| // ] -IH #V #HV0 #HV1 + elim (tueq_lifts_sn … HV1 … HVW1) -V1 + /3 width=3 by cpm_delta, ex2_intro/ +| #n #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #X2 #H2 + >(tueq_inv_lref1 … H2) -X2 + elim (IH V0) [| // ] -IH #V #HV0 #HV1 + elim (tueq_lifts_sn … HV1 … HVW1) -V1 + /3 width=3 by cpm_ell, ex2_intro/ +| #n #I #G #K0 #V1 #W1 #i #_ #IH #HVW1 #X2 #H2 + >(tueq_inv_lref1 … H2) -X2 + elim (IH (#i)) [| // ] -IH #V #HV0 #HV1 + elim (tueq_lifts_sn … HV1 … HVW1) -V1 + /3 width=3 by cpm_lref, ex2_intro/ +| #n #p #I #G #L #V0 #V1 #T0 #T1 #HV01 #_ #_ #IHT #X2 #H2 + elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct + elim (IHT … HT02) -T0 #T #HT2 #HT1 + /3 width=3 by cpm_bind, tueq_bind, ex2_intro/ +| #n #G #L #V0 #V1 #T0 #T1 #HV10 #_ #_ #IHT #X2 #H2 + elim (tueq_inv_appl1 … H2) -H2 #T2 #HT02 #H destruct + elim (IHT … HT02) -T0 #T #HT2 #HT1 + /3 width=3 by cpm_appl, tueq_appl, ex2_intro/ +| #n #G #L #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X2 #H2 + elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct + elim (IHV … HV02) -V0 #V #HV2 #HV1 + elim (IHT … HT02) -T0 #T #HT2 #HT1 + /3 width=5 by cpm_cast, tueq_cast, ex2_intro/ +| #n #G #L #V0 #U0 #T0 #T1 #HTU0 #_ #IH #X2 #H2 + elim (tueq_inv_bind1 … H2) -H2 #U2 #HU02 #H destruct + elim (tueq_inv_lifts_sn … HU02 … HTU0) -U0 #T2 #HTU2 #HT02 + elim (IH … HT02) -T0 #T #HT2 #HT1 + /3 width=3 by cpm_zeta, ex2_intro/ +| #n #G #L #V0 #T0 #T1 #_ #IH #X2 #H2 + elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #_ #HT02 #H destruct + elim (IH … HT02) -V0 -T0 + /3 width=3 by cpm_eps, ex2_intro/ +| #n #G #L #V0 #T0 #T1 #_ #IH #X2 #H2 + elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #HV02 #_ #H destruct + elim (IH … HV02) -V0 -T1 + /3 width=3 by cpm_ee, ex2_intro/ +| #n #p #G #L #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #_ #_ #_ #IHT #X2 #H2 + elim (tueq_inv_appl1 … H2) -H2 #X #H2 #H destruct + elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct + elim (IHT … HT02) -T0 + /4 width=3 by cpm_beta, tueq_cast, tueq_bind, ex2_intro/ +| #n #p #G #L #V0 #V1 #U1 #W0 #W1 #T0 #T1 #HV01 #HW01 #_ #_ #_ #IHT #HVU1 #X2 #H2 + elim (tueq_inv_appl1 … H2) -H2 #X #H2 #H destruct + elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct + elim (IHT … HT02) -T0 #T #HT2 #HT1 + /4 width=3 by cpm_theta, tueq_appl, tueq_bind, ex2_intro/ +] +qed-. + +lemma tueq_cpm_trans (h) (n) (G) (L) (T0): + ∀T1. T1 ≅ T0 → ∀T2. ⦃G,L⦄ ⊢ T0 ➡[n,h] T2 → + ∃∃T. ⦃G,L⦄ ⊢ T1 ➡[n,h] T & T ≅ T2. +#h #n #G #L #T0 #T1 #HT10 #T2 #HT02 +elim (cpm_tueq_conf … HT02 T1) +/3 width=3 by tueq_sym, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma deleted file mode 100644 index 0317cc097..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma +++ /dev/null @@ -1,116 +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/predtywhead_4.ma". -include "static_2/syntax/item_sh.ma". -include "static_2/syntax/lenv.ma". -include "static_2/syntax/genv.ma". - -(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****) - -inductive cwhx (h:sh) (G:genv): relation2 lenv term ≝ -| cwhx_sort: ∀L,s. cwhx h G L (⋆s) -| cwhx_abst: ∀p,L,W,T. cwhx h G L (ⓛ{p}W.T) -| cwhx_ldef: ∀L,V,T. cwhx h G (L.ⓓV) T → cwhx h G L (-ⓓV.T) -. - -interpretation - "whd normality for unbound context-sensitive parallel rt-transition (term)" - 'PRedTyWHead h G L T = (cwhx h G L T). - -(* Basic inversion lemmas ***************************************************) - -fact cwhx_inv_lref_aux (h) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → - ∀i. X = #i → ⊥. -#h #G #Y #X * - X -Y -[ #L #s #i #H destruct -| #p #L #W #T #i #H destruct -| #L #V #T #_ #i #H destruct -] -qed-. - -lemma cwhx_inv_lref (h) (G): - ∀L,i. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃#i⦄ → ⊥. -/2 width=7 by cwhx_inv_lref_aux/ qed-. - -fact cwhx_inv_gref_aux (h) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → - ∀l. X = §l → ⊥. -#h #G #Y #X * - X -Y -[ #L #s #l #H destruct -| #p #L #W #T #l #H destruct -| #L #V #T #_ #l #H destruct -] -qed-. - -lemma cwhx_inv_gref (h) (G): - ∀L,l. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃§l⦄ → ⊥. -/2 width=7 by cwhx_inv_gref_aux/ qed-. - -fact cwhx_inv_abbr_aux (h) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → - ∀V,T. X = +ⓓV.T → ⊥. -#h #G #Y #X * - X -Y -[ #L #s #X1 #X2 #H destruct -| #p #L #W #T #X1 #X2 #H destruct -| #L #V #T #_ #X1 #X2 #H destruct -] -qed-. - -lemma cwhx_inv_abbr (h) (G): - ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥. -/2 width=8 by cwhx_inv_abbr_aux/ qed-. - -fact cwhx_inv_ldef_aux (h) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → - ∀V,T. X = -ⓓV.T → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄. -#h #G #Y #X * - X -Y -[ #L #s #X1 #X2 #H destruct -| #p #L #W #T #X1 #X2 #H destruct -| #L #V #T #HT #X1 #X2 #H destruct // -] -qed-. - -lemma cwhx_inv_ldef (h) (G): - ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃-ⓓV.T⦄ → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄. -/2 width=3 by cwhx_inv_ldef_aux/ qed-. - -fact cwhx_inv_appl_aux (h) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → - ∀V,T. X = ⓐV.T → ⊥. -#h #G #Y #X * - X -Y -[ #L #s #X1 #X2 #H destruct -| #p #L #W #T #X1 #X2 #H destruct -| #L #V #T #_ #X1 #X2 #H destruct -] -qed-. - -lemma cwhx_inv_appl (h) (G): - ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓐV.T⦄ → ⊥. -/2 width=8 by cwhx_inv_appl_aux/ qed-. - -fact cwhx_inv_cast_aux (h) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → - ∀U,T. X = ⓝU.T → ⊥. -#h #G #Y #X * - X -Y -[ #L #s #X1 #X2 #H destruct -| #p #L #W #T #X1 #X2 #H destruct -| #L #V #T #_ #X1 #X2 #H destruct -] -qed-. - -lemma cwhx_inv_cast (h) (G): - ∀Y,U,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓝU.T⦄ → ⊥. -/2 width=8 by cwhx_inv_cast_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma deleted file mode 100644 index 8ef7b522b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma +++ /dev/null @@ -1,46 +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/drops.ma". -include "basic_2/rt_transition/cwhx.ma". - -(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****) - -(* Properties with generic slicing ******************************************) - -lemma cwhx_lifts (h) (G): d_liftable1 … (cwhx h G). -#h #G #K #T #H elim H -K -T -[ #K #s #b #f #L #HLK #X #H - lapply (lifts_inv_sort1 … H) -H #H destruct // -| #p #K #V #T #b #f #L #HLK #X #H - elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct // -| #K #V #T #_ #IH #b #f #L #HLK #X #H - elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct - /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/ -] -qed-. - -(* Inversion lemmas with generic slicing ************************************) - -lemma cwhx_inv_lifts (h) (G): d_deliftable1 … (cwhx h G). -#h #G #L #U #H elim H -L -U -[ #L #s #b #f #K #HLK #X #H - lapply (lifts_inv_sort2 … H) -H #H destruct // -| #p #L #W #U #b #f #K #HLK #X #H - elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct // -| #L #W #U #_ #IH #b #f #K #HLK #X #H - elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct - /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma deleted file mode 100644 index df1a77e38..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma +++ /dev/null @@ -1,41 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "static_2/static/rdeq_fqup.ma". -include "basic_2/rt_transition/cwhx.ma". - -(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****) - -(* Properties with sort-irrelevant equivalence ******************************) - -lemma rdeq_tdeq_cwhx_trans (h) (G): - ∀L2,T2. ⦃G,L2⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ → - ∀T1. T1 ≛ T2 → - ∀L1. L1 ≛[T1] L2 → ⦃G,L1⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄. -#h #G #L2 #T2 #H elim H -L2 -T2 -[ #L2 #s2 #X1 #HX #L1 #HL - elim (tdeq_inv_sort2 … HX) -HX #s1 #H destruct -s2 // -| #p #L2 #W2 #T2 #X1 #HX #L1 #HL - elim (tdeq_inv_pair2 … HX) -HX #W1 #T1 #_ #_ #H destruct -W2 -T2 // -| #L2 #V2 #T2 #_ #IH #X1 #HX #L1 #HL - elim (tdeq_inv_pair2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct - elim (rdeq_inv_bind … HL) -HL #HV1 #HT1 - /5 width=2 by cwhx_ldef, rdeq_bind_repl_dx, ext2_pair/ -] -qed-. - -lemma tdeq_cwhx_trans (h) (G) (L): - ∀T2. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ → - ∀T1. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄. -/3 width=5 by rdeq_tdeq_cwhx_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index e1457f0b7..a5c53bf3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -27,6 +27,10 @@ Stage "B" + + Extended (λδ-2) and restricted (λδ-1) validity is decidable + (anniversary milestone). + Preservation of validity for rt-computation does not need the sort degree parameter 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 76da17d40..efbca8468 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_cpes" + "cnv_cpes_dec" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ] + [ [ "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_cpue" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" * ] } ] } @@ -33,11 +33,11 @@ table { class "prune" [ { "rt-equivalence" * } { [ { "context-sensitive parallel r-equivalence" * } { - [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ] + [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_csx" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ] } ] [ { "t-bound context-sensitive parallel rt-equivalence" * } { - [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" * ] + [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" + "cpes_cprs" * ] } ] } @@ -58,6 +58,10 @@ table { ] class "sky" [ { "rt-computation" * } { + [ { "t-unbound context-sensitive parallel rt-computation" * } { + [ [ "evaluation for terms" ] "cpue ( ⦃?,?⦄ ⊢ ? ⥲*[?] 𝐍⦃?⦄ )" "cpue_csx" * ] + } + ] [ { "context-sensitive parallel r-computation" * } { [ [ "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" * ] @@ -67,7 +71,7 @@ table { ] [ { "t-bound context-sensitive parallel rt-computation" * } { [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ] - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_cwhx" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnu" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { @@ -90,9 +94,8 @@ table { ] class "cyan" [ { "rt-transition" * } { - [ { "unbound parallel rst-transition" * } { - [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" + "fpbq_fpb" * ] - [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_rdeq" + "fpb_fdeq" * ] + [ { "t-unbound context-sensitive parallel rt-transition" * } { + [ [ "normal form for terms" ] "cnu ( ⦃?,?⦄ ⊢ ⥲[?] 𝐍⦃?⦄ )" "cnu_tdeq" + "cnu_lifts" + "cnu_drops" + "cnu_cnr" + "cnu_cnr_simple" + "cnu_cnu" * ] } ] [ { "context-sensitive parallel r-transition" * } { @@ -103,11 +106,15 @@ table { } ] [ { "t-bound context-sensitive parallel rt-transition" * } { - [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] + [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_tueq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] + } + ] + [ { "unbound parallel rst-transition" * } { + [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" + "fpbq_fpb" * ] + [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_rdeq" + "fpb_fdeq" * ] } ] [ { "unbound context-sensitive parallel rt-transition" * } { - [ [ "whd normal form for terms" ] "cwhx" + "( ⦃?,?⦄ ⊢ ⬈[?] 𝐖𝐇⦃?⦄ )" "cwhx_drops" + "cwhx_rdeq" * ] [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ] [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ] diff --git a/matita/matita/contribs/lambdadelta/compile_partial.sh b/matita/matita/contribs/lambdadelta/compile_partial.sh index 817d68bc0..13afbaf04 100644 --- a/matita/matita/contribs/lambdadelta/compile_partial.sh +++ b/matita/matita/contribs/lambdadelta/compile_partial.sh @@ -1 +1,4 @@ -../../matitac.opt `cat partial.txt` +../../matitac.opt ground_2 +../../matitac.opt static_2 +../../matitac.opt basic_2 +../../matitac.opt apps_2 diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt deleted file mode 100644 index 11b4d4573..000000000 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ /dev/null @@ -1,4 +0,0 @@ -ground_2 -static_2 -basic_2 -apps_2 diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma new file mode 100644 index 000000000..4cb121630 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( T1 ≅ break term 46 T2 )" + non associative with precedence 45 + for @{ 'ApproxEq $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma index 060f3b805..681363f03 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma @@ -56,6 +56,10 @@ definition deliftable2_bi: predicate (relation term) ≝ λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 → ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2. +definition liftable2_dx: predicate (relation term) ≝ + λR. ∀T1,T2. R T1 T2 → ∀f,U2. ⬆*[f] T2 ≘ U2 → + ∃∃U1. ⬆*[f] T1 ≘ U1 & R U1 U2. + definition deliftable2_dx: predicate (relation term) ≝ λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 → ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2. @@ -333,6 +337,11 @@ qed-. (* Basic properties *********************************************************) +lemma liftable2_sn_dx (R): symmetric … R → liftable2_sn R → liftable2_dx R. +#R #H2R #H1R #T1 #T2 #HT12 #f #U2 #HTU2 +elim (H1R … T1 … HTU2) -H1R /3 width=3 by ex2_intro/ +qed-. + lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R. #R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2 elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/ @@ -365,7 +374,7 @@ elim (IHV1 f) -IHV1 #V2 #HV12 ] qed-. -lemma lifts_push_zero (f): ⬆*[⫯f]#O ≘ #0. +lemma lifts_push_zero (f): ⬆*[⫯f]#0 ≘ #0. /2 width=1 by lifts_lref/ qed. lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2). diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma index 5aee3ad12..c76781d11 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma @@ -38,6 +38,9 @@ lemma tdeq_lifts_sn: liftable2_sn tdeq. ] qed-. +lemma tdeq_lifts_dx: liftable2_dx tdeq. +/3 width=3 by tdeq_lifts_sn, liftable2_sn_dx, tdeq_sym/ qed-. + lemma tdeq_lifts_bi: liftable2_bi tdeq. /3 width=6 by tdeq_lifts_sn, liftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tueq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tueq.ma new file mode 100644 index 000000000..a9805a9e3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tueq.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tueq.ma". +include "static_2/relocation/lifts_lifts.ma". + +(* GENERIC RELOCATION FOR TERMS *********************************************) + +(* Properties with tail sort-irrelevant equivalence for terms ***************) + +lemma tueq_lifts_sn: liftable2_sn tueq. +#T1 #T2 #H elim H -T1 -T2 +[ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H + /3 width=3 by lifts_sort, tueq_sort, ex2_intro/ +| #i #f #X #H elim (lifts_inv_lref1 … H) -H + /3 width=3 by lifts_lref, tueq_lref, ex2_intro/ +| #l #f #X #H >(lifts_inv_gref1 … H) -H + /2 width=3 by lifts_gref, tueq_gref, ex2_intro/ +| #p #I #V #T1 #T2 #_ #IHT #f #X #H elim (lifts_inv_bind1 … H) -H + #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHT … HTU1) -T1 + /3 width=3 by lifts_bind, tueq_bind, ex2_intro/ +| #V #T1 #T2 #_ #IHT #f #X #H elim (lifts_inv_flat1 … H) -H + #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHT … HTU1) -T1 + /3 width=3 by lifts_flat, tueq_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 elim (IHT … HTU1) -T1 + /3 width=5 by lifts_flat, tueq_cast, ex2_intro/ +] +qed-. + +lemma tueq_lifts_dx: liftable2_dx tueq. +/3 width=3 by tueq_lifts_sn, liftable2_sn_dx, tueq_sym/ qed-. + +lemma tueq_lifts_bi: liftable2_bi tueq. +/3 width=6 by tueq_lifts_sn, liftable2_sn_bi/ qed-. + +(* Inversion lemmas with tail sort-irrelevant equivalence for terms *********) + +lemma tueq_inv_lifts_sn: deliftable2_sn tueq. +#U1 #U2 #H elim H -U1 -U2 +[ #s1 #s2 #f #X #H >(lifts_inv_sort2 … H) -H + /3 width=3 by lifts_sort, tueq_sort, ex2_intro/ +| #i #f #X #H elim (lifts_inv_lref2 … H) -H + /3 width=3 by lifts_lref, tueq_lref, ex2_intro/ +| #l #f #X #H >(lifts_inv_gref2 … H) -H + /2 width=3 by lifts_gref, tueq_gref, ex2_intro/ +| #p #I #W #U1 #U2 #_ #IHU #f #X #H elim (lifts_inv_bind2 … H) -H + #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHU … HTU1) -U1 + /3 width=3 by lifts_bind, tueq_bind, ex2_intro/ +| #W #U1 #U2 #_ #IHU #f #X #H elim (lifts_inv_flat2 … H) -H + #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHU … HTU1) -U1 + /3 width=3 by lifts_flat, tueq_appl, ex2_intro/ +| #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_flat2 … H) -H + #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1 + /3 width=5 by lifts_flat, tueq_cast, ex2_intro/ +] +qed-. + +lemma tueq_inv_lifts_dx: deliftable2_dx tueq. +/3 width=3 by tueq_inv_lifts_sn, deliftable2_sn_dx, tueq_sym/ qed-. + +lemma tueq_inv_lifts_bi: deliftable2_bi tueq. +/3 width=6 by tueq_inv_lifts_sn, deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma new file mode 100644 index 000000000..49a6b2fdf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma @@ -0,0 +1,143 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************) + +inductive tueq: relation term ≝ +| tueq_sort: ∀s1,s2. tueq (⋆s1) (⋆s2) +| tueq_lref: ∀i. tueq (#i) (#i) +| tueq_gref: ∀l. tueq (§l) (§l) +| tueq_bind: ∀p,I,V,T1,T2. tueq T1 T2 → tueq (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2) +| tueq_appl: ∀V,T1,T2. tueq T1 T2 → tueq (ⓐV.T1) (ⓐV.T2) +| tueq_cast: ∀V1,V2,T1,T2. tueq V1 V2 → tueq T1 T2 → tueq (ⓝV1.T1) (ⓝV2.T2) +. + +interpretation + "context-free tail sort-irrelevant equivalence (term)" + 'ApproxEq T1 T2 = (tueq T1 T2). + +(* Basic properties *********************************************************) + +lemma tueq_refl: reflexive … tueq. +#T elim T -T * [|||| * ] +/2 width=1 by tueq_sort, tueq_lref, tueq_gref, tueq_bind, tueq_appl, tueq_cast/ +qed. + +lemma tueq_sym: symmetric … tueq. +#T1 #T2 #H elim H -T1 -T2 +/2 width=3 by tueq_sort, tueq_bind, tueq_appl, tueq_cast/ +qed-. + +(* Left basic inversion lemmas **********************************************) + +fact tueq_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/ +| #i #s #H destruct +| #l #s #H destruct +| #p #I #V #T1 #T2 #_ #s #H destruct +| #V #T1 #T2 #_ #s #H destruct +| #V1 #V2 #T1 #T2 #_ #_ #s #H destruct +] +qed-. + +lemma tueq_inv_sort1: ∀Y,s1. ⋆s1 ≅ Y → + ∃s2. Y = ⋆s2. +/2 width=4 by tueq_inv_sort1_aux/ qed-. + +fact tueq_inv_lref1_aux: ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i. +#X #Y * -X -Y // +[ #s1 #s2 #j #H destruct +| #p #I #V #T1 #T2 #_ #j #H destruct +| #V #T1 #T2 #_ #j #H destruct +| #V1 #V2 #T1 #T2 #_ #_ #j #H destruct +] +qed-. + +lemma tueq_inv_lref1: ∀Y,i. #i ≅ Y → Y = #i. +/2 width=5 by tueq_inv_lref1_aux/ qed-. + +fact tueq_inv_gref1_aux: ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l. +#X #Y * -X -Y // +[ #s1 #s2 #k #H destruct +| #p #I #V #T1 #T2 #_ #k #H destruct +| #V #T1 #T2 #_ #k #H destruct +| #V1 #V2 #T1 #T2 #_ #_ #k #H destruct +] +qed-. + +lemma tueq_inv_gref1: ∀Y,l. §l ≅ Y → Y = §l. +/2 width=5 by tueq_inv_gref1_aux/ qed-. + +fact tueq_inv_bind1_aux: ∀X,Y. X ≅ Y → ∀p,I,V,T1. X = ⓑ{p,I}V.T1 → + ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2. +#X #Y * -X -Y +[ #s1 #s2 #q #J #W #U1 #H destruct +| #i #q #J #W #U1 #H destruct +| #l #q #J #W #U1 #H destruct +| #p #I #V #T1 #T2 #HT #q #J #W #U1 #H destruct /2 width=3 by ex2_intro/ +| #V #T1 #T2 #_ #q #J #W #U1 #H destruct +| #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct +] +qed-. + +lemma tueq_inv_bind1: ∀p,I,V,T1,Y. ⓑ{p,I}V.T1 ≅ Y → + ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2. +/2 width=3 by tueq_inv_bind1_aux/ qed-. + +fact tueq_inv_appl1_aux: ∀X,Y. X ≅ Y → ∀V,T1. X = ⓐV.T1 → + ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2. +#X #Y * -X -Y +[ #s1 #s2 #W #U1 #H destruct +| #i #W #U1 #H destruct +| #l #W #U1 #H destruct +| #p #I #V #T1 #T2 #_ #W #U1 #H destruct +| #V #T1 #T2 #HT #W #U1 #H destruct /2 width=3 by ex2_intro/ +| #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct +] +qed-. + +lemma tueq_inv_appl1: ∀V,T1,Y. ⓐV.T1 ≅ Y → + ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2. +/2 width=3 by tueq_inv_appl1_aux/ qed-. + +fact tueq_inv_cast1_aux: ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 → + ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2. +#X #Y * -X -Y +[ #s1 #s2 #W1 #U1 #H destruct +| #i #W1 #U1 #H destruct +| #l #W1 #U1 #H destruct +| #p #I #V #T1 #T2 #_ #W1 #U1 #H destruct +| #V #T1 #T2 #_ #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma tueq_inv_cast1: ∀V1,T1,Y. ⓝV1.T1 ≅ Y → + ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2. +/2 width=3 by tueq_inv_cast1_aux/ qed-. + +(* Right basic inversion lemmas *********************************************) + +lemma tueq_inv_bind2: ∀p,I,V,T2,X1. X1 ≅ ⓑ{p,I}V.T2 → + ∃∃T1. T1 ≅ T2 & X1 = ⓑ{p,I}V.T1. +#p #I #V #T2 #X1 #H +elim (tueq_inv_bind1 p I V T2 X1) +[ #T1 #HT #H destruct ] +/3 width=3 by tueq_sym, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq_tueq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tueq_tueq.ma new file mode 100644 index 000000000..4d8d21f6c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tueq_tueq.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tueq.ma". + +(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************) + +(* Main properties **********************************************************) + +theorem tueq_trans: Transitive … tueq. +#T1 #T #H elim H -T1 -T +[ #s1 #s #X #H + elim (tueq_inv_sort1 … H) -s /2 width=1 by tueq_sort/ +| #i1 #i #H // +| #l1 #l #H // +| #p #I #V #T1 #T #_ #IHT #X #H + elim (tueq_inv_bind1 … H) -H /3 width=1 by tueq_bind/ +| #V #T1 #T #_ #IHT #X #H + elim (tueq_inv_appl1 … H) -H /3 width=1 by tueq_appl/ +| #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H + elim (tueq_inv_cast1 … H) -H /3 width=1 by tueq_cast/ +] +qed-. + +theorem tueq_canc_sn: left_cancellable … tueq. +/3 width=3 by tueq_trans, tueq_sym/ qed-. + +theorem tueq_canc_dx: right_cancellable … tueq. +/3 width=3 by tueq_trans, tueq_sym/ qed-. + +theorem tueq_repl: ∀T1,T2. T1 ≅ T2 → + ∀U1. T1 ≅ U1 → ∀U2. T2 ≅ U2 → U1 ≅ U2. +/3 width=3 by tueq_canc_sn, tueq_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 8b9fec7bb..fed1803e1 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_lifts" * ] + [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tueq" + "lifts_lifts" * ] } ] [ { "syntactic equivalence" * } { @@ -115,7 +115,11 @@ table { [ [ "for terms" ] "theq" + "( ? ⩳ ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] - [ { "degree-based equivalence" * } { + [ { "tail sort-irrelevant equivalence" * } { + [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ] + } + ] + [ { "sort-irrelevant equivalence" * } { [ [ "" ] "tdeq_ext" + "( ? ≛ ? )" + "( ? ⊢ ? ≛ ? )" * ] [ [ "" ] "tdeq" + "( ? ≛ ? )" "tdeq_tdeq" * ] } diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 9efd9a61b..ead63683a 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1513,7 +1513,7 @@ let predefined_classes = [ ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ]; ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; - ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; "⇡"; ] ; ["⇑"; "⇧"; "⬆"; ] ; -- 2.39.2