From: Ferruccio Guidi Date: Mon, 5 Nov 2018 19:38:52 +0000 (+0100) Subject: update in basic_2, static_2, web site X-Git-Tag: make_still_working~270 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8;p=helm.git update in basic_2, static_2, web site + bug fix and first results on cpce + crux favicon for web site is now 32x32 + some auxiliary files for web site committed/rearranged --- diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 938529c63..e9008a950 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -1,6 +1,6 @@ H=@ -TAGS = www up-html \ +TAGS = www up-html up-css up-images up-download \ lint-xml index lddl install-xml \ test-html html install-html \ install-jed install-bib install-2 install-1 install-coq \ @@ -162,11 +162,19 @@ install-v: $(HELENADIR)/$(COQ) $(H)scp $< $(DOWNDIR) up-html: - @echo " UPDATE $(RHOMEDIR)/html" + @echo " UPDATE $(RHOMEDIR)/html/" $(H)scp -q -r html $(RHOMEDIR) +up-css: + @echo " UPDATE $(RHOMEDIR)/css/" + $(H)scp -q -r css $(RHOMEDIR) + +up-images: + @echo " UPDATE $(RHOMEDIR)/images/" + $(H)scp -q -r images $(RHOMEDIR) + up-download: - @echo " UPDATE $(RHOMEDIR)/download" + @echo " UPDATE $(RHOMEDIR)/download/" $(H)scp -q -r download $(RHOMEDIR) %.ld: diff --git a/helm/www/lambdadelta/css/wanda.css b/helm/www/lambdadelta/css/wanda.css new file mode 100644 index 000000000..5ea84ad82 --- /dev/null +++ b/helm/www/lambdadelta/css/wanda.css @@ -0,0 +1,211 @@ +@charset "UTF-8"; + +/* menus ********************************************************************/ + +.text { + display: inline-block; + list-style: none; + margin: 0; + padding: 0; + white-space: nowrap; +} + +.menu { + display: none; + border-style: solid; + border-width: thin; + position: absolute; +} + +.menu:target { + display: inline-block; +} + +/* buttons ******************************************************************/ + +.button { + color: inherit; + background-color: inherit; + border-style: none; + margin: initial; + padding: initial; +} + +.button:hover { + text-decoration: underline; +} + +/* anchors ******************************************************************/ + +a:link { + text-decoration: initial; + color: inherit; +} + +/* visited link */ +a:visited { + text-decoration: initial; + color: inherit; +} + +/* mouse over link */ +a:hover { + text-decoration: underline; + color: inherit; +} + +/* selected link */ +a:active { + text-decoration: underline; + color: inherit; +} + +/* displays *****************************************************************/ + +.block { + display: block; +} + +.inline { + display: inline; +} + +/* font families ************************************************************/ + +.monospace { + font-family:monospace; +} + +/* line heights *************************************************************/ + +.l_150 { + line-height:150%; +} + +/* font sizes ***************************************************************/ + +.t_130 { + font-size: 130%; +} + +/* foreground colors (equalized to gray 8F) *********************************/ + +.f_gray { + color:#8F8F8F; +} + +.f_wine { + color:#FF52A0; +} + +.f_magenta { + color:#FF41FF; +} + +.f_prune { + color:#C65DFF; +} + +.f_blue { + color:#8181FF; +} + +.f_sky { + color:#04C0FF; +} + +.f_cyan { + color:#00CCCC; +} + +.f_water { + color:#00D88C; +} + +.f_green { + color:#00F200; +} + +.f_grass { + color:#83AF00; +} + +.f_yellow { + color:#A0A000; +} + +.f_orange { + color:#C09000; +} + +.f_red { + color:#FF5F5F; +} + +.f_black { + color:#000000; +} + +/* background colors (equalized to gray D3) *********************************/ + +.b_white { + background-color:#FFFFFF; +} + +.b_gray { + background-color:#D3D3D3; +} + +.b_wine { + background-color:#FFBBD9; +} + +.b_magenta { + background-color:#FFB4FF; +} + +.b_prune { + background-color:#E8BFFF; +} + +.b_blue { + background-color:#CDCDFF; +} + +.b_sky { + background-color:#9CE6FF; +} + +.b_cyan { + background-color:#6CFFFF; +} + +.b_water { + background-color:#7DFFD1; +} + +.b_green { + background-color:#93FF93; +} + +.b_grass { + background-color:#C3FF11; +} + +.b_yellow { + background-color:#EDED00; +} + +.b_orange { + background-color:#FFD454; +} + +.b_red { + background-color:#FFC0C0; +} + +/* background colors (equalized to gray EB) *********************************/ + +.b_gray_EB { + background-color:#EBEBEB; +} diff --git a/helm/www/lambdadelta/images/crux_177.xcf b/helm/www/lambdadelta/images/crux_177.xcf deleted file mode 100644 index 685256637..000000000 Binary files a/helm/www/lambdadelta/images/crux_177.xcf and /dev/null differ diff --git a/helm/www/lambdadelta/images/crux_32.ico b/helm/www/lambdadelta/images/crux_32.ico new file mode 100644 index 000000000..1ce111150 Binary files /dev/null and b/helm/www/lambdadelta/images/crux_32.ico differ diff --git a/helm/www/lambdadelta/images/osn_32.xcf b/helm/www/lambdadelta/images/osn_32.xcf deleted file mode 100644 index 0b46d8024..000000000 Binary files a/helm/www/lambdadelta/images/osn_32.xcf and /dev/null differ diff --git a/helm/www/lambdadelta/images/osn_label.xcf b/helm/www/lambdadelta/images/osn_label.xcf deleted file mode 100644 index daabe0987..000000000 Binary files a/helm/www/lambdadelta/images/osn_label.xcf and /dev/null differ diff --git a/helm/www/lambdadelta/images/smile.xcf b/helm/www/lambdadelta/images/smile.xcf deleted file mode 100644 index f3cc6239a..000000000 Binary files a/helm/www/lambdadelta/images/smile.xcf and /dev/null differ diff --git a/helm/www/lambdadelta/images/wanda_32.ico b/helm/www/lambdadelta/images/wanda_32.ico new file mode 100644 index 000000000..bfe28a5f6 Binary files /dev/null and b/helm/www/lambdadelta/images/wanda_32.ico differ diff --git a/helm/www/lambdadelta/xcf/crux_177.xcf b/helm/www/lambdadelta/xcf/crux_177.xcf new file mode 100644 index 000000000..685256637 Binary files /dev/null and b/helm/www/lambdadelta/xcf/crux_177.xcf differ diff --git a/helm/www/lambdadelta/xcf/helena_label.xcf b/helm/www/lambdadelta/xcf/helena_label.xcf new file mode 100644 index 000000000..0748c5eb7 Binary files /dev/null and b/helm/www/lambdadelta/xcf/helena_label.xcf differ diff --git a/helm/www/lambdadelta/xcf/osn_32.xcf b/helm/www/lambdadelta/xcf/osn_32.xcf new file mode 100644 index 000000000..0b46d8024 Binary files /dev/null and b/helm/www/lambdadelta/xcf/osn_32.xcf differ diff --git a/helm/www/lambdadelta/xcf/osn_label.xcf b/helm/www/lambdadelta/xcf/osn_label.xcf new file mode 100644 index 000000000..daabe0987 Binary files /dev/null and b/helm/www/lambdadelta/xcf/osn_label.xcf differ diff --git a/helm/www/lambdadelta/xcf/smile.xcf b/helm/www/lambdadelta/xcf/smile.xcf new file mode 100644 index 000000000..f3cc6239a Binary files /dev/null and b/helm/www/lambdadelta/xcf/smile.xcf differ diff --git a/helm/www/lambdadelta/xcf/wanda_32.xcf b/helm/www/lambdadelta/xcf/wanda_32.xcf new file mode 100644 index 000000000..4932d3495 Binary files /dev/null and b/helm/www/lambdadelta/xcf/wanda_32.xcf differ diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index b574a4125..3fbc83b45 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -226,7 +226,7 @@ href="{$baseurl}css/xhtbl.css" />
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.ma new file mode 100644 index 000000000..d8baf5703 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.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 T2 )" + non associative with precedence 45 + for @{ 'PConvEta $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma new file mode 100644 index 000000000..b9d162530 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma @@ -0,0 +1,138 @@ +(**************************************************************************) +(* ___ *) +(* ||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/xoa/ex_2_4.ma". +include "basic_2/notation/relations/pconveta_5.ma". +include "basic_2/rt_computation/cpms.ma". + +(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************) + +(* avtivate genv *) +inductive cpce (h): relation4 genv lenv term term ≝ +| cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s) +| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0) +| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s → + cpce h G (K.ⓛV) (#0) (#0) +| cpce_eta : ∀n,p,G,K,V,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T → + cpce h G (K.ⓛV) (#0) (+ⓛW.ⓐ#0.#1) +| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T → + ⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U +| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2. + cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 → + cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) +| cpce_flat: ∀I,G,L,V1,V2,T1,T2. + cpce h G L V1 V2 → cpce h G L T1 T2 → + cpce h G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) +. + +interpretation + "context-sensitive parallel eta-conversion (term)" + 'PConvEta h G L T1 T2 = (cpce h G L T1 T2). + +(* Basic inversion lemmas ***************************************************) + +lemma cpce_inv_sort_sn (h) (G) (L) (X2): + ∀s. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2. +#h #G #Y #X2 #s0 +@(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2 +[ #G #L #s #_ // +| #G #K #V #_ // +| #n #G #K #V #s #_ #_ // +| #n #p #G #K #V #W #T #_ #H destruct +| #I #G #K #T #U #i #_ #_ #H destruct +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct +] +qed-. + +lemma cpce_inv_ldef_sn (h) (G) (K) (X2): + ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2. +#h #G #Y #X2 #X +@(insert_eq_0 … (Y.ⓓX)) #Y1 +@(insert_eq_0 … (#0)) #X1 +* -G -Y1 -X1 -X2 +[ #G #L #s #_ #_ // +| #G #K #V #_ #_ // +| #n #G #K #V #s #_ #_ #_ // +| #n #p #G #K #V #W #T #_ #_ #H destruct +| #I #G #K #T #U #i #_ #_ #H #_ destruct +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct +] +qed-. + +lemma cpce_inv_ldec_sn (h) (G) (K) (X2): + ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 → + ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2 + | ∃∃n,p,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T & +ⓛW.ⓐ#0.#1 = X2. +#h #G #Y #X2 #X +@(insert_eq_0 … (Y.ⓛX)) #Y1 +@(insert_eq_0 … (#0)) #X1 +* -G -Y1 -X1 -X2 +[ #G #L #s #H #_ destruct +| #G #K #V #_ #H destruct +| #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/ +| #n #p #G #K #V #W #T #HV #_ #H destruct /3 width=6 by or_intror, ex2_4_intro/ +| #I #G #K #T #U #i #_ #_ #H #_ destruct +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct +] +qed-. + +lemma cpce_inv_lref_sn (h) (G) (K) (X2): + ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 → + ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2. +#h #G #Y #X2 #Z #j +@(insert_eq_0 … (Y.ⓘ{Z})) #Y1 +@(insert_eq_0 … (#↑j)) #X1 +* -G -Y1 -X1 -X2 +[ #G #L #s #H #_ destruct +| #G #K #V #H #_ destruct +| #n #G #K #V #s #_ #H #_ destruct +| #n #p #G #K #V #W #T #_ #H #_ destruct +| #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/ +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct +] +qed-. + +lemma cpce_inv_bind_sn (h) (G) (K) (X2): + ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 → + ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2. +#h #G #Y #X2 #q #Z #U #X +@(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2 +[ #G #L #s #H destruct +| #G #K #V #H destruct +| #n #G #K #V #s #_ #H destruct +| #n #p #G #K #V #W #T #_ #H destruct +| #I #G #K #T #U #i #_ #_ #H destruct +| #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct +] +qed-. + +lemma cpce_inv_flat_sn (h) (G) (L) (X2): + ∀I,V1,T1. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 → + ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2. +#h #G #Y #X2 #Z #U #X +@(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2 +[ #G #L #s #H destruct +| #G #K #V #H destruct +| #n #G #K #V #s #_ #H destruct +| #n #p #G #K #V #W #T #_ #H destruct +| #I #G #K #T #U #i #_ #_ #H destruct +| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct +| #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_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 cb69bdfb9..236b4f999 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 @@ -40,6 +40,10 @@ table { ] class "blue" [ { "rt-conversion" * } { + [ { "context-sensitive parallel eta-conversion" * } { + [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ] + } + ] [ { "context-sensitive parallel r-conversion" * } { [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma new file mode 100644 index 000000000..b4f405729 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (2, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma new file mode 100644 index 000000000..af891c071 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa/ex_2_4.ma". + +(* multiple existental quantifier (2, 4) *) + +inductive ex2_4 (A0,A1,A2,A3:Type[0]) (P0,P1:A0→A1→A2→A3→Prop) : Prop ≝ + | ex2_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → ex2_4 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 4)" 'Ex4 P0 P1 = (ex2_4 ? ? ? ? P0 P1). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index d40726d02..149052483 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -5,6 +5,7 @@ ground_2/xoa ground_2/notation/xoa basics/pts.ma + 2 4 5 1 5 7 9 3 diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/relations/pconveta_4.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/pconveta_4.ma deleted file mode 100644 index 37dc822fb..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/notation/relations/pconveta_4.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 T2 )" - non associative with precedence 45 - for @{ 'PConvEta $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/cpce.ma b/matita/matita/contribs/lambdadelta/static_2/static/cpce.ma deleted file mode 100644 index c24dc49ab..000000000 --- a/matita/matita/contribs/lambdadelta/static_2/static/cpce.ma +++ /dev/null @@ -1,39 +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/pconveta_4.ma". -include "static_2/relocation/lifts.ma". -include "static_2/static/aaa.ma". - -(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************) - -(* avtivate genv *) -inductive cpce: relation4 genv lenv term term ≝ -| cpce_sort: ∀G,L,s. cpce G L (⋆s) (⋆s) -| cpce_abbr: ∀G,K,V. cpce G (K.ⓓV) (#0) (#0) -| cpce_abst: ∀G,K,W,B,A. ⦃G,K⦄ ⊢ W ⁝ ②B.A → - cpce G (K.ⓛW) (#0) (+ⓛW.ⓐ#0.#1) -| cpce_lref: ∀I,G,K,T,U,i. cpce G K (#i) T → - ⬆*[1] T ≘ U → cpce G (K.ⓘ{I}) (#↑i) U -| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2. - cpce G K V1 V2 → cpce G (K.ⓑ{I}V1) T1 T2 → - cpce G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) -| cpce_flat: ∀I,G,L,V1,V2,T1,T2. - cpce G L V1 V2 → cpce G L T1 T2 → - cpce G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) -. - -interpretation - "context-sensitive parallel eta-conversion (term)" - 'PConvEta G L T1 T2 = (cpce G L T1 T2). 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 01e178fbb..4dcb17989 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 @@ -19,10 +19,6 @@ table { ] class "green" [ { "static typing" * } { - [ { "context-sensitive parallel eta-conversion" * } { - [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η ? )" * ] - } - ] [ { "generic reducibility" * } { [ [ "restricted refinement for lenvs" ] "lsubc" + "( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] [ [ "candidates" ] "gcp_cr" + "( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]