From: Ferruccio Guidi Date: Fri, 23 Aug 2019 19:24:02 +0000 (+0200) Subject: update in ground_2 static_2 basic_2 X-Git-Tag: make_still_working~239 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bac74b5cff042d37e1abc9c961a6c41094b8a294 update in ground_2 static_2 basic_2 + the applicability parameter is now a predicate + tueq removed in favor of theq + two conjectures to prove ... --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma index c3c661085..9539ab942 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma @@ -35,12 +35,12 @@ qed. lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h]. #h #p #G #L #s @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2)) -[ /2 width=1 by ylt_inj/ +[ // | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/ | @cnv_zero @cnv_bind // @(cnv_appl … 1 p … (⋆s) … (⋆s)) - [ /2 width=1 by ylt_inj/ + [ // | /2 width=1 by cnv_sort, cnv_zero/ | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/ | /2 width=3 by cpms_ell, lifts_sort/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index 962b6d775..0bd1aa915 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_lt.ma". +include "static_2/syntax/ac.ma". include "basic_2/notation/relations/exclaim_5.ma". include "basic_2/notation/relations/exclaim_4.ma". include "basic_2/notation/relations/exclaimstar_4.ma". @@ -22,12 +22,12 @@ include "basic_2/rt_computation/cpms.ma". (* activate genv *) (* Basic_2A1: uses: snv *) -inductive cnv (a:ynat) (h): relation3 genv lenv term ≝ +inductive cnv (a) (h): relation3 genv lenv term ≝ | cnv_sort: ∀G,L,s. cnv a h G L (⋆s) | cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0) | cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i) | cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T) -| cnv_appl: ∀n,p,G,L,V,W0,T,U0. yinj n < a → cnv a h G L V → cnv a h G L T → +| cnv_appl: ∀n,p,G,L,V,W0,T,U0. appl a n → cnv a h G L V → cnv a h G L T → ⦃G,L⦄ ⊢ V ➡*[1,h] W0 → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T) | cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T → ⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[1,h] U0 → cnv a h G L (ⓝU.T) @@ -37,10 +37,10 @@ interpretation "context-sensitive native validity (term)" 'Exclaim a h G L T = (cnv a h G L T). interpretation "context-sensitive restricted native validity (term)" - 'Exclaim h G L T = (cnv (yinj (S (S O))) h G L T). + 'Exclaim h G L T = (cnv (ac_eq (S O)) h G L T). interpretation "context-sensitive extended native validity (term)" - 'ExclaimStar h G L T = (cnv Y h G L T). + 'ExclaimStar h G L T = (cnv ac_top h G L T). (* Basic inversion lemmas ***************************************************) @@ -117,7 +117,7 @@ lemma cnv_inv_bind (a) (h): fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀V,T. X = ⓐV.T → - ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & + ∃∃n,p,W0,U0. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. #a #h #G #L #X * -L -X [ #G #L #s #X1 #X2 #H destruct @@ -132,7 +132,7 @@ qed-. (* Basic_2A1: uses: snv_inv_appl *) lemma cnv_inv_appl (a) (h): ∀G,L,V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → - ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & + ∃∃n,p,W0,U0. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0. /2 width=3 by cnv_inv_appl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma index c7735d20c..5667b7870 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -12,9 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/lib/arith_2b.ma". include "basic_2/rt_computation/cpms_aaa.ma". -include "basic_2/rt_computation/lprs_cpms.ma". include "basic_2/dynamic/cnv.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -61,21 +59,23 @@ elim (cnv_fwd_aaa … H) -H #A #HA /2 width=2 by cpms_total_aaa/ qed-. -(* Advanced inversion lemmas ************************************************) - -lemma cnv_inv_appl_pred (a) (h) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] → - ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & - ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0. -#a #h #G #L #V #T #H -elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU -lapply (ylt_inv_inj … Ha) -Ha #Ha -elim (cnv_fwd_aaa … HT) #A #HA -elim (cpms_total_aaa h … (a-↑n) … (ⓛ{p}W.U)) -[|*: /2 width=8 by cpms_aaa_conf/ ] -HA #X #HU0 -elim (cpms_inv_abst_sn … HU0) #W0 #U0 #HW0 #_ #H destruct -lapply (cpms_trans … HVW … HW0) -HVW -HW0 #HVW0 -lapply (cpms_trans … HTU … HU0) -HTU -HU0 ->(arith_m2 … Ha) -Ha #HTU0 -/2 width=5 by ex4_3_intro/ +lemma cnv_fwd_cpms_abst_dx_le (a) (h) (G) (L) (W) (p): + ∀T. ⦃G,L⦄ ⊢ T ![a,h] → + ∀n1,U1. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U1 → ∀n2. n1 ≤ n2 → + ∃∃U2. ⦃G,L⦄ ⊢ T ➡*[n2,h] ⓛ{p}W.U2 & ⦃G,L.ⓛW⦄ ⊢ U1 ➡*[n2-n1,h] U2. +#a #h #G #L #W #p #T #H +elim (cnv_fwd_aaa … H) -H #A #HA +/2 width=2 by cpms_abst_dx_le_aaa/ qed-. + +(* Advanced properties ******************************************************) + +lemma cnv_appl_ge (a) (h) (n1) (p) (G) (L): + ∀n2. n1 ≤ n2 → appl a n2 → + ∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] → + ∀X. ⦃G,L⦄ ⊢ V ➡*[1,h] X → ∀W. ⦃G,L⦄ ⊢ W ➡*[h] X → + ∀U. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h]. +#a #h #n1 #p #G #L #n2 #Hn12 #Ha #V #HV #T #HT #X #HVX #W #HW #X #HTX +elim (cnv_fwd_cpms_abst_dx_le … HT … HTX … Hn12) #U #HTU #_ -n1 +/4 width=11 by cnv_appl, cpms_bind, cpms_cprs_trans/ +qed. 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 5f1bf31a8..4b6cb48d3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/cpue_csx.ma". include "basic_2/rt_conversion/cpce_drops.ma". -include "basic_2/dynamic/cnv_cpue.ma". +include "basic_2/dynamic/cnv_cpmhe.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -32,9 +31,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 (cpue_total_csx … H1W) -H1W #X + elim (cpmhe_total_csx … H1W) -H1W #X #n #HWX elim (abst_dec X) [ * | -IH ] - [ #p #V1 #U #H destruct * #n #HWU #_ + [ #p #V1 #U #H destruct + lapply (cpmhe_fwd_cpms … HWX) -HWX #HWX elim (IH G K V1) -IH [ #V2 #HV12 elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2 @@ -42,13 +42,13 @@ generalize in match HT1; -HT1 | /3 width=6 by cnv_cpms_trans, cnv_fwd_pair_sn/ | /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ ] - | #HnX #HWX + | #HnX @(ex_intro … (#i)) @cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0 lapply (drops_mono … HLK0 … HLK) -i -L #H destruct - elim (cnv_cpue_cpms_conf … H2W … HWU0 … HWX) -n0 -W #X0 * #n0 #HUX0 #_ #HX0 - elim (cpms_inv_abst_sn … HUX0) -HUX0 #V1 #U1 #_ #_ #H destruct -n0 -K -V0 -U0 - elim (tueq_inv_bind2 … HX0) -HX0 #U0 #_ #H destruct -U1 + 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 /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_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma index e0775c021..125c9649f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) +include "basic_2/rt_computation/cpms_cpms.ma". include "basic_2/rt_equivalence/cpes.ma". -include "basic_2/dynamic/cnv_aaa.ma". +include "basic_2/dynamic/cnv.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Properties with t-bound rt-equivalence for terms *************************) lemma cnv_appl_cpes (a) (h) (G) (L): - ∀n. yinj n < a → + ∀n. appl a n → ∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀W. ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W → ∀p,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h]. @@ -38,22 +39,13 @@ qed. lemma cnv_inv_appl_cpes (a) (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → - ∃∃n,p,W,U. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & + ∃∃n,p,W,U. appl a n & ⦃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 … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU /3 width=7 by cpms_div, ex5_4_intro/ qed-. -lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] → - ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & - ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W.U. -#a #h #G #L #V #T #H -elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU -/3 width=7 by cpms_div, ex4_3_intro/ -qed-. - lemma cnv_inv_cast_cpes (a) (h) (G) (L): ∀U,T. ⦃G,L⦄ ⊢ ⓝU.T ![a,h] → ∧∧ ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T. @@ -71,7 +63,7 @@ lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term): (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] → Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T) ) → - (∀n,p,G,L,V,W,T,U. yinj n < a → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] → + (∀n,p,G,L,V,W,T,U. appl a n → ⦃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 → Q G L V → Q G L T → Q G L (ⓐV.T) ) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma index e8f59293c..8fac0d847 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma @@ -74,7 +74,7 @@ qed-. lemma cpm_tdeq_inv_appl_sn (a) (h) (n) (G) (L): ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] → ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X → - ∃∃m,q,W,U1,T2. yinj m < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W & ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1 + ∃∃m,q,W,U1,T2. appl a m & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W & ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1 & ⦃G,L⦄⊢ T1 ![a,h] & ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2. #a #h #n #G #L #V #T1 #H0 #X #H1 #H2 elim (cpm_inv_appl1 … H1) -H1 * @@ -132,7 +132,7 @@ lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …): ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2) ) → - (∀m. yinj m < a → + (∀m. appl a m → ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G,L⦄ ⊢ V ➡*[1,h] W → ∀p,T1,U1. ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] → ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma index 3b4b54740..f1c856801 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -14,9 +14,9 @@ include "ground_2/lib/arith_2b.ma". include "basic_2/rt_computation/cprs_cprs.ma". -include "basic_2/rt_computation/lprs_cpms.ma". include "basic_2/dynamic/cnv_drops.ma". include "basic_2/dynamic/cnv_preserve_sub.ma". +include "basic_2/dynamic/cnv_aaa.ma". include "basic_2/dynamic/lsubv_cnv.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -63,13 +63,14 @@ fact cnv_cpm_trans_lpr_aux (a) (h): elim (cnv_cpms_strip_lpr_sub … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12 (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/etc/cpue/cpms_cnu.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpms_cnu.etc new file mode 100644 index 000000000..5e7790683 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpms_cnu.etc @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "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/etc/cpue/cpmue.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpmue.etc new file mode 100644 index 000000000..1132c8ee5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpmue.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/predevalstar_6.ma". +include "basic_2/rt_transition/cnu.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS ******************) + +definition cpmue (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 = (cpmue h n G L T1 T2). + +definition R_cpmue (h) (G) (L) (T): predicate nat ≝ + λn. ∃U. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃U⦄. + +(* Basic properties *********************************************************) + +lemma cpmue_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. + +(* Basic forward lemmas *****************************************************) + +lemma cpmue_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/etc/cpue/cpmue_csx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpmue_csx.etc new file mode 100644 index 000000000..7ad451c1b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpmue_csx.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpm_cpx.ma". +include "basic_2/rt_transition/cnu_tdeq.ma". +include "basic_2/rt_computation/csx.ma". +include "basic_2/rt_computation/cpmue.ma". + +(* T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS ******************) + +(* Properties with strong normalization for unbound rt-transition for terms *) + +lemma cpmue_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 (cnu_dec_tdeq h G L T1) +[ -IHT1 #HT1 /3 width=4 by cpmue_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, cpmue_intro, ex1_2_intro/ +] +qed-. + +lemma R_cpmue_total_csx (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmue h G L T1 n. +#h #G #L #T1 #H +elim (cpmue_total_csx … H) -H #T2 #n #HT12 +/3 width=3 by ex_intro (* 2x *)/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue.etc new file mode 100644 index 000000000..a22002aed --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue.etc @@ -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/etc/cpue/cpue_csx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue_csx.etc new file mode 100644 index 000000000..2ba2ddb02 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue_csx.etc @@ -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/etc/cpue/prediteval_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/prediteval_5.etc new file mode 100644 index 000000000..b87e86381 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpue/prediteval_5.etc @@ -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( ⦃ 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/predevalstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalstar_6.ma new file mode 100644 index 000000000..0a484cd85 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalstar_6.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( ⦃ 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 }. 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 deleted file mode 100644 index b87e86381..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prediteval_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* 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/rt_computation/cpmhe.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe.ma new file mode 100644 index 000000000..c08c1b101 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predevalstar_6.ma". +include "basic_2/rt_transition/cnh.ma". +include "basic_2/rt_computation/cpms.ma". + +(* HEAD T-UNBOUND 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⦄. + +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). + +definition R_cpmhe (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⦄. +/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 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 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 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. + +(* 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. +#h #n #G #L #T1 #T2 * #HT12 #_ // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma new file mode 100644 index 000000000..d821c8452 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/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". + +(* HEAD T-UNBOUND 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⦄. +#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/ +| * #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/ +] +qed-. + +lemma R_cpmhe_total_csx (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmhe h G L T1 n. +#h #G #L #T1 #H +elim (cpmhe_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_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma index f4cc579aa..db4eefb22 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma @@ -15,6 +15,7 @@ include "basic_2/rt_transition/cpm_aaa.ma". include "basic_2/rt_computation/cpxs_aaa.ma". include "basic_2/rt_computation/cpms_cpxs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) @@ -22,7 +23,7 @@ include "basic_2/rt_computation/cpms_cpxs.ma". (* Basic_2A1: uses: scpds_aaa_conf *) (* Basic_2A1: includes: cprs_aaa_conf *) -lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n). +lemma cpms_aaa_conf (h) (G) (L) (n): Conf3 … (aaa G L) (cpms h G L n). /3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-. lemma cpms_total_aaa (h) (G) (L) (n) (A): @@ -36,3 +37,15 @@ lemma cpms_total_aaa (h) (G) (L) (n) (A): /3 width=4 by cpms_step_dx, ex_intro/ ] qed-. + +lemma cpms_abst_dx_le_aaa (h) (G) (L) (T) (W) (p): + ∀A. ⦃G,L⦄ ⊢ T ⁝ A → + ∀n1,U1. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U1 → ∀n2. n1 ≤ n2 → + ∃∃U2. ⦃G,L⦄ ⊢ T ➡*[n2,h] ⓛ{p}W.U2 & ⦃G,L.ⓛW⦄ ⊢ U1 ➡*[n2-n1,h] U2. +#h #G #L #T #W #p #A #HA #n1 #U1 #HTU1 #n2 #Hn12 +lapply (cpms_aaa_conf … HA … HTU1) -HA #HA +elim (cpms_total_aaa h … (n2-n1) … HA) -HA #X #H +elim (cpms_inv_abst_sn … H) -H #W0 #U2 #_ #HU12 #H destruct -W0 +>(plus_minus_m_m_commutative … Hn12) in ⊢ (??%?); -Hn12 +/4 width=5 by cpms_trans, cpms_bind_dx, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.ma new file mode 100644 index 000000000..8cd6df24a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.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 "static_2/syntax/theq_theq.ma". +include "basic_2/rt_transition/cnh_cnh.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Inversion lemmas with normal terms for head t-unbound rt-transition ******) + +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/ +qed-. 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 deleted file mode 100644 index 5e7790683..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnu.ma +++ /dev/null @@ -1,27 +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/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/cpue.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma deleted file mode 100644 index a22002aed..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/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 deleted file mode 100644 index 2ba2ddb02..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue_csx.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 "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_equivalence/cpes_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpes.ma new file mode 100644 index 000000000..73dca9727 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpes.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lprs_cpms.ma". +include "basic_2/rt_equivalence/cpes_cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************) + +(* Advanced forward lemmas **************************************************) + +lemma cpes_fwd_abst_bi (h) (n1) (n2) (p1) (p2) (G) (L): + ∀W1,W2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h,n1,n2] ⓛ{p2}W2.T2 → + ∧∧ p1 = p2 & ⦃G,L⦄ ⊢ W1 ⬌*[h,0,O] W2. +#h #n1 #n2 #p1 #p2 #G #L #W1 #W2 #T1 #T2 * #X #H1 #H2 +elim (cpms_inv_abst_sn … H1) #W0 #X0 #HW10 #_ #H destruct +elim (cpms_inv_abst_bi … H2) #H #HW20 #_ destruct +/3 width=3 by cpms_div, conj/ +qed-. + +(* Main properties **********************************************************) + +theorem cpes_cpes_trans (h) (n1) (n2) (G) (L) (T): + ∀T1. ⦃G,L⦄ ⊢ T ⬌*[h,n1,0] T1 → + ∀T2. ⦃G,L⦄ ⊢ T1 ⬌*[h,0,n2] T2 → ⦃G,L⦄ ⊢ T ⬌*[h,n1,n2] T2. +#h #n1 #n2 #G #L #T #T1 #HT1 #T2 * #X #HX1 #HX2 +lapply (cpes_cprs_trans … HT1 … HX1) -T1 #HTX +lapply (cpes_cpms_div … HTX … HX2) -X // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpms.ma new file mode 100644 index 000000000..48b0ceb1c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpms.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "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 t-bound rt-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-. + +lemma cpes_cpms_div (h) (n) (n1) (n2) (G) (L) (T0): + ∀T1. ⦃G,L⦄ ⊢ T1 ⬌*[h,n,n1] T0 → + ∀T2. ⦃G,L⦄ ⊢ T2 ➡*[n2,h] T0 → ⦃G,L⦄ ⊢ T1 ⬌*[h,n,n2+n1] T2. +#h #n #n1 #n2 #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT20 +lapply (cpms_trans … HT20 … HT0) -T0 #HT2 +/2 width=3 by cpms_div/ +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 deleted file mode 100644 index 53967448e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cprs.ma +++ /dev/null @@ -1,28 +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_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/cnh.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma new file mode 100644 index 000000000..9e549a93d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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_cnh.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_cnh.ma new file mode 100644 index 000000000..7a65df8d3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_cnh.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpm.ma". +include "basic_2/rt_transition/cnh.ma". + +(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) + +(* Advanced properties ******************************************************) + +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 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_drops.ma new file mode 100644 index 000000000..d4927690f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_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_theq.ma". +include "basic_2/rt_transition/cpm_drops.ma". +include "basic_2/rt_transition/cnh.ma". + +(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) + +(* Advanced properties ******************************************************) + +lemma cnh_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 cnh_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 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_transition/cnh_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_lifts.ma new file mode 100644 index 000000000..3bbfeee85 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_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.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/cnh_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_simple.ma new file mode 100644 index 000000000..71951a7ee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_simple.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpm_simple.ma". +include "basic_2/rt_transition/cnh.ma". + +(* NORMAL TERMS HEAD FOR T-UNUNBOUND RT-TRANSITION **************************) + +(* Advanced properties with simple terms ************************************) + +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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma new file mode 100644 index 000000000..666474121 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cnh_simple.ma". +include "basic_2/rt_transition/cnh_drops.ma". + +(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************) + +(* Properties with context-free sort-irrelevant equivalence for terms *******) + +lemma cnh_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/ +| #i elim (drops_F_uni L i) + [ /3 width=7 by cnh_atom_drops, or_introl/ + | * * [ #I | * #V ] #K #HLK + [ /3 width=8 by cnh_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 /3 width=5 by cnh_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 + @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/ + ] + | /3 width=5 by cnh_abbr_neg, or_introl/ + | /3 width=5 by cnh_abst, or_introl/ + ] +| * #V1 #T1 + [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ] + [ /3 width=5 by cnh_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 + ] + | @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/cnu.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma deleted file mode 100644 index 19b1eaf8c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma +++ /dev/null @@ -1,61 +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/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 deleted file mode 100644 index ce295d3ed..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr.ma +++ /dev/null @@ -1,37 +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/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 deleted file mode 100644 index 056c8e250..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr_simple.ma +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "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 deleted file mode 100644 index 2bc4d3c2d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnu.ma +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "static_2/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 deleted file mode 100644 index 97e13d22a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_drops.ma +++ /dev/null @@ -1,52 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "static_2/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 deleted file mode 100644 index 051da519a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_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_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 deleted file mode 100644 index f6eb1a805..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_tdeq.ma +++ /dev/null @@ -1,98 +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/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 deleted file mode 100644 index 2baeeefae..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tueq.ma +++ /dev/null @@ -1,90 +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_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/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 48785b62b..ef3ff958c 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_cpue" + "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_cpmhe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] } ] } @@ -37,7 +37,7 @@ table { } ] [ { "t-bound context-sensitive parallel rt-equivalence" * } { - [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" + "cpes_cprs" * ] + [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" + "cpes_cpms" + "cpes_cpes" * ] } ] } @@ -58,10 +58,6 @@ 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" * ] @@ -70,8 +66,9 @@ table { } ] [ { "t-bound context-sensitive parallel rt-computation" * } { + [ [ "t-unbound head evaluation for terms" ] "cpmhe ( ⦃?,?⦄ ⊢ ? ⬌*[?] 𝐍*⦃?⦄ )" "cpmhe_csx" * ] [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ] - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnu" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnh" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { @@ -95,7 +92,7 @@ table { class "cyan" [ { "rt-transition" * } { [ { "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" * ] + [ [ "head normal form for terms" ] "cnh ( ⦃?,?⦄ ⊢ ⥲[?] 𝐍⦃?⦄ )" "cnh_tdeq" + "cnh_lifts" + "cnh_drops" + "cnh_cnr" + "cnh_cnr_simple" + "cnh_cnh" * ] } ] [ { "context-sensitive parallel r-transition" * } { @@ -106,7 +103,7 @@ table { } ] [ { "t-bound context-sensitive parallel rt-transition" * } { - [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_tueq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] + [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] } ] [ { "unbound parallel rst-transition" * } { @@ -209,4 +206,8 @@ class "italic" { 2 } [ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ] } ] + [ { "tail sort-irrelevant equivalence" * } { + [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ] + } + ] *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc index 1af2859d7..11ef739da 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc @@ -30,3 +30,7 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. #x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/ #Hxy elim (H Hxy) qed-. + +lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y. +#x #y #Hxy >minus_minus [|*: // ] minus_minus [|*: // ] (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/etc/tueq/tueq.etc b/matita/matita/contribs/lambdadelta/static_2/etc/tueq/tueq.etc new file mode 100644 index 000000000..49a6b2fdf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/etc/tueq/tueq.etc @@ -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/etc/tueq/tueq_tueq.etc b/matita/matita/contribs/lambdadelta/static_2/etc/tueq/tueq_tueq.etc new file mode 100644 index 000000000..4d8d21f6c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/etc/tueq/tueq_tueq.etc @@ -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/notation/relations/approxeq_2.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma deleted file mode 100644 index 4cb121630..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* 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_theq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_theq.ma new file mode 100644 index 000000000..29abf85ba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_theq.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/syntax/theq.ma". +include "static_2/relocation/lifts_lifts.ma". + +(* GENERIC RELOCATION FOR TERMS *********************************************) + +(* Properties with tail sort-irrelevant head equivalence for terms **********) + +lemma theq_lifts_bi: liftable2_bi theq. +#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/ +] +qed-. + +(* Inversion lemmas with tail sort-irrelevant head equivalence for terms ****) + +lemma theq_inv_lifts_bi: deliftable2_bi theq. +#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/ +| #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/ +| #l #f #X1 #H1 #X2 #H2 + >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2 + /1 width=1 by theq_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/ +| #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/ +] +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 deleted file mode 100644 index a9805a9e3..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tueq.ma +++ /dev/null @@ -1,80 +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/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/ac.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma new file mode 100644 index 000000000..9968544cb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/lib/arith.ma". + +(* APPLICABILITY CONDITION *************************************************) + +(* applicability condition specification *) +record ac: Type[0] ≝ { +(* degree of the sort *) + appl: predicate nat +}. + +(* applicability condition postulates *) +record ac_props (a): Prop ≝ { + ac_dec: ∀m. Decidable (∃∃n. m ≤ n & appl a n) +}. + +(* Notable specifications ***************************************************) + +definition apply_top: predicate nat ≝ λn. ⊤. + +definition ac_top: ac ≝ mk_ac apply_top. + +lemma ac_top_props: ac_props ac_top ≝ mk_ac_props …. +/3 width=3 by or_introl, ex2_intro/ +qed. + +definition ac_eq (k): ac ≝ mk_ac (eq … k). + +lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props …. +#m elim (le_dec m k) #Hm +[ /3 width=3 by or_introl, ex2_intro/ +| @or_intror * #n #Hmn #H destruct /2 width=1 by/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma deleted file mode 100644 index 49a6b2fdf..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma +++ /dev/null @@ -1,143 +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/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 deleted file mode 100644 index 4d8d21f6c..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/tueq_tueq.ma +++ /dev/null @@ -1,44 +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/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 3793e6896..07bc1856a 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 @@ -102,6 +102,10 @@ table { ] class "red" [ { "syntax" * } { + [ { "applicability condition" * } { + [ [ "properties" ] "ac" * ] + } + ] [ { "equivalence up to exclusion binders" * } { [ [ "for lenvs" ] "lveq" + "( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ] } @@ -111,14 +115,10 @@ table { [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ] } ] - [ { "head equivalence" * } { + [ { "sort-irrelevant head equivalence" * } { [ [ "for terms" ] "theq" + "( ? ⩳ ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] - [ { "tail sort-irrelevant equivalence" * } { - [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ] - } - ] [ { "sort-irrelevant equivalence" * } { [ [ "" ] "tdeq_ext" + "( ? ≛ ? )" + "( ? ⊢ ? ≛ ? )" * ] [ [ "" ] "tdeq" + "( ? ≛ ? )" "tdeq_tdeq" * ]