From: Ferruccio Guidi Date: Mon, 13 Nov 2017 17:09:16 +0000 (+0000) Subject: - lsubsx (replacement of lcosx) completed X-Git-Tag: make_still_working~409 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc40346f09bcccb9a09560963ccb7157ebfad7ad;p=helm.git - lsubsx (replacement of lcosx) completed - minor updates --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml deleted file mode 100644 index 09003e83a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml +++ /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( L1 ⨵ [ break term 46 f ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'Clear $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma deleted file mode 100644 index e69a4ac02..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_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( G ⊢ ~ ⬊ * [ break term 46 h , break term 46 o , break term 46 f ] break term 46 L )" - non associative with precedence 45 - for @{ 'CoSN $h $o $f $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_6.ma new file mode 100644 index 000000000..7f9afe8ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_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( G ⊢ break term 46 L1 ⊆ⓧ [ break term 46 h, break term 46 o, break term 46 f ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LSubEqX $h $o $f $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma deleted file mode 100644 index 8f29e1aaf..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma +++ /dev/null @@ -1,77 +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/cosn_5.ma". -include "basic_2/computation/lsx.ma". - -(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) - -inductive lcosx (h) (o) (G): relation2 ynat lenv ≝ -| lcosx_sort: ∀l. lcosx h o G l (⋆) -| lcosx_skip: ∀I,L,T. lcosx h o G 0 L → lcosx h o G 0 (L.ⓑ{I}T) -| lcosx_pair: ∀I,L,T,l. G ⊢ ⬊*[h, o, T, l] L → - lcosx h o G l L → lcosx h o G (⫯l) (L.ⓑ{I}T) -. - -interpretation - "sn extended strong conormalization (local environment)" - 'CoSN h o l G L = (lcosx h o G l L). - -(* Basic properties *********************************************************) - -lemma lcosx_O: ∀h,o,G,L. G ⊢ ~⬊*[h, o, 0] L. -#h #o #G #L elim L /2 width=1 by lcosx_skip/ -qed. - -lemma lcosx_drop_trans_lt: ∀h,o,G,L,l. G ⊢ ~⬊*[h, o, l] L → - ∀I,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → i < l → - G ⊢ ~⬊*[h, o, ⫰(l-i)] K ∧ G ⊢ ⬊*[h, o, V, ⫰(l-i)] K. -#h #o #G #L #l #H elim H -L -l -[ #l #J #K #V #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H // -| #I #L #T #l #HT #HL #IHL #J #K #V #i #H #Hil - elim (drop_inv_O1_pair1 … H) -H * #Hi #HLK destruct - [ >ypred_succ /2 width=1 by conj/ - | lapply (ylt_pred … Hil ?) -Hil /2 width=1 by ylt_inj/ >ypred_succ #Hil - elim (IHL … HLK ?) -IHL -HLK yminus_SO2 // - <(ypred_succ l) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/ - ] -] -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lcosx_inv_succ_aux: ∀h,o,G,L,x. G ⊢ ~⬊*[h, o, x] L → ∀l. x = ⫯l → - L = ⋆ ∨ - ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, o, l] K & - G ⊢ ⬊*[h, o, V, l] K. -#h #o #G #L #l * -L -l /2 width=1 by or_introl/ -[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H) -| #I #L #T #l #HT #HL #x #H <(ysucc_inv_inj … H) -x - /3 width=6 by ex3_3_intro, or_intror/ -] -qed-. - -lemma lcosx_inv_succ: ∀h,o,G,L,l. G ⊢ ~⬊*[h, o, ⫯l] L → L = ⋆ ∨ - ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, o, l] K & - G ⊢ ⬊*[h, o, V, l] K. -/2 width=3 by lcosx_inv_succ_aux/ qed-. - -lemma lcosx_inv_pair: ∀h,o,I,G,L,T,l. G ⊢ ~⬊*[h, o, ⫯l] L.ⓑ{I}T → - G ⊢ ~⬊*[h, o, l] L ∧ G ⊢ ⬊*[h, o, T, l] L. -#h #o #I #G #L #T #l #H elim (lcosx_inv_succ … H) -H -[ #H destruct -| * #Z #Y #X #H destruct /2 width=1 by conj/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma deleted file mode 100644 index 756b8a7a1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma +++ /dev/null @@ -1,67 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/lsx_drop.ma". -include "basic_2/computation/lsx_lpx.ma". -include "basic_2/computation/lsx_lpxs.ma". -include "basic_2/computation/lcosx.ma". - -(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************) - -(* Properties on extended context-sensitive parallel reduction for term *****) - -lemma lsx_cpx_trans_lcosx: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → - ∀l. G ⊢ ~⬊*[h, o, l] L → - G ⊢ ⬊*[h, o, T1, l] L → G ⊢ ⬊*[h, o, T2, l] L. -#h #o #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // -[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H - elim (ylt_split i l) #Hli [ -H | -HL ] - [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/ - elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli - lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/ - | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli - lapply (drop_fwd_drop2 … HLK) -HLK - /4 width=10 by lsx_ge, lsx_lift_le/ - ] -| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H - elim (lsx_inv_bind … H) -H #HV1 #HT1 - @lsx_bind /2 width=2 by/ (**) (* explicit constructor *) - @(lsx_lreq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lreq_succ/ -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H - elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/ -| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H - elim (lsx_inv_bind … H) -H #HV #HU1 - <(ypred_succ l) (lsubsx_inv_atom_sn … H) -L2 // +| #f #I #K1 #K2 #_ #IH #L2 #H + elim (lsubsx_inv_push_sn … H) -H /3 width=1 by eq_f2/ +| #f #I #K1 #K2 #_ #IH #L2 #H + elim (lsubsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/ +| #f #I #K1 #K2 #V #_ #_ #IH #L2 #H + elim (lsubsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/ +] +qed-. + +theorem lsubsx_trans: ∀h,o,f,G. Transitive … (lsubsx h o G f). +#h #o #f #G #L1 #L #H1 #L2 #H2 +<(lsubsx_fix … H1 … H2) -L2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 079fa87e0..acdc797e9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -3,3 +3,4 @@ lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.m csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma +lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma 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 8ff7a521f..5719d23da 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 @@ -87,7 +87,6 @@ table { } ] [ { "strongly normalizing rt-computation" * } { - [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] [ "llsx_csx" * ] [ "csx_fpbs" * ] } @@ -106,8 +105,9 @@ table { [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ] } ] -*) +*) [ { "uncounted context-sensitive rt-computation" * } { + [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]