From 3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 5 Nov 2018 20:38:52 +0100 Subject: [PATCH] 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 --- helm/www/lambdadelta/Makefile | 14 +- helm/www/lambdadelta/css/wanda.css | 211 ++++++++++++++++++ helm/www/lambdadelta/images/crux_32.ico | Bin 0 -> 766 bytes helm/www/lambdadelta/images/wanda_32.ico | Bin 0 -> 2238 bytes .../lambdadelta/{images => xcf}/crux_177.xcf | Bin helm/www/lambdadelta/xcf/helena_label.xcf | Bin 0 -> 7794 bytes .../lambdadelta/{images => xcf}/osn_32.xcf | Bin .../lambdadelta/{images => xcf}/osn_label.xcf | Bin .../www/lambdadelta/{images => xcf}/smile.xcf | Bin helm/www/lambdadelta/xcf/wanda_32.xcf | Bin 0 -> 3026 bytes helm/www/lambdadelta/xslt/ld_web_root.xsl | 2 +- .../notation/relations/pconveta_5.ma} | 4 +- .../lambdadelta/basic_2/rt_conversion/cpce.ma | 138 ++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 + .../ground_2/notation/xoa/ex_2_4.ma | 26 +++ .../static/cpce.ma => ground_2/xoa/ex_2_4.ma} | 31 +-- .../lambdadelta/ground_2/xoa2.conf.xml | 1 + .../lambdadelta/static_2/web/static_2_src.tbl | 4 - 18 files changed, 404 insertions(+), 31 deletions(-) create mode 100644 helm/www/lambdadelta/css/wanda.css create mode 100644 helm/www/lambdadelta/images/crux_32.ico create mode 100644 helm/www/lambdadelta/images/wanda_32.ico rename helm/www/lambdadelta/{images => xcf}/crux_177.xcf (100%) create mode 100644 helm/www/lambdadelta/xcf/helena_label.xcf rename helm/www/lambdadelta/{images => xcf}/osn_32.xcf (100%) rename helm/www/lambdadelta/{images => xcf}/osn_label.xcf (100%) rename helm/www/lambdadelta/{images => xcf}/smile.xcf (100%) create mode 100644 helm/www/lambdadelta/xcf/wanda_32.xcf rename matita/matita/contribs/lambdadelta/{static_2/notation/relations/pconveta_4.ma => basic_2/notation/relations/pconveta_5.ma} (92%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_2_4.ma rename matita/matita/contribs/lambdadelta/{static_2/static/cpce.ma => ground_2/xoa/ex_2_4.ma} (50%) 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_32.ico b/helm/www/lambdadelta/images/crux_32.ico new file mode 100644 index 0000000000000000000000000000000000000000..1ce1111502a52027fec0348bcd231bc76301fb36 GIT binary patch literal 766 zcmZQzU<5)11py$*!tjELfkBLcfk6X^6@b_Qh(Y4G!2kUX4F6~TXK2_D#Q%Zp|Nn6* i#VT$L0VYmL5HQ^NE(8EHkXRfAAz*~?v8D}r2m%1H)Js1A literal 0 HcmV?d00001 diff --git a/helm/www/lambdadelta/images/wanda_32.ico b/helm/www/lambdadelta/images/wanda_32.ico new file mode 100644 index 0000000000000000000000000000000000000000..bfe28a5f6240bc18596fb8023172a1736f1ee796 GIT binary patch literal 2238 zcmeH|X;4mK6vzLF$`&cv>do3>iR=p5C2fi*y^arj@WtS>ZN@i-F=K`?!(awk#%`t= z%NR>3(o|YSmQs-vhGta9|GtafX3G1y8P7Yvd(J)o=Q;P@bDn!&pc{Yw{@~FKX>Pz^ z0D*)dL=Yq1+0fJssF`fcgl>8Y-AuM*LAPc@w~_5+$1~{89Oy2xo9uZ3-Anf6LiguE z50HcT&_m>K0rbdA=+Q#xF><^JdZHM5lAI!^OQ2`S*;44aGU$1dMlQU9UL=>uWpbq) zdX-#z4ZUvg26}_`W(D*X{o5p+e)>D;9dei4Gxz|#Pacqm zB)b>y^>>CT)gE-TsrD3J9m*o9whSF4x8{krT*2g+w7qY+LZmeo!S5!$B%nu%eO9EA zAlZ60kM25=H8hLuda|M0o;!@+*;yiqG(L9SZ0NR=nSf7!kyXF|S6fOE2Yos)qj!SD z0p5XO_5==kC@^QrM2TUV7>^G0$v}8wul3Qu5VLEdZGyx4Nx)p`6BPvvmEe$edP?|O zksx5cg!(Q6hD(gQ?V+se#~3vj$Nv&Z>>dvIirF>Vn!u`iB1vQvut21*2jC|%ex#!w zgykZBz(SF!T;VSgYpbz!eNs(p&n+HGwITlY3%B|%LUn>J)+Vzg6Pi@K^U-Bc=3)v;eYFF1Cv z9h&f=Ab}=C{}dPn@dItsREmV4KL$h$G5%1YRhy^~jIyy6hPG~es7=2TJI>*G-jCSX z5-IzUp^jYXxgY1AbMLw5i5w|tf9ZGp})ML z-_p?MHe72R;BMD27eoa2Wfbg2>$$dU50yJ}$zi()lIz+;J84#%r)?W-k}2dd-tY9= zC2O~R#M)QrPv$pR+X}gKFx^>lzF=GN4+Vbpgj}j;xB+L#&e7(5PQFZ+4Z9vlVvx)^ z$&x?LCG*)q1e?|7lsla=m+wuM?9Q}Pv{PlLkhgN>B8YE}Hn^}m5l6VWovzJyC+bcG z`)3AAWhXOiIy;pOm|nY8c=9FK%|{J@8d$Z?r!LZF0oN;JeOq6VWTS%P-rJE}(!EJi~z zxqsqT2@AU(suDSmEj#6sedrZ~F%(HaCFIV|$99+@FnT^U*bZI@DAx#El` z8PFgalCg(XK0bcCNQeHr!#BNa|0bOrh5hJ;h}U(kA9==t8)~;Sqn;Xv<4)3-yos4& zOuNW)Pd)b}S}g9Bh0Jy4dj#N>!~29K$o19eGuL;aoh#S7{9LEbK`PHL(|hXq!0X{1 z%=EWD3DcMV+sgF#hwDdZ$n?bYYTmUlSEffFqp?u}=fnQdpLwK!7X2;9BWAz)kO!r@ z>6KSM0%u+6eSPBGfXGv-f57naSls&g%OYd)aP-0`Y4iI&&dJRhqTfI{dy$!?B!319C~r$ znR_L{Gj#*403$v&P%NbEQmNoRAqyGq>#!T2zuCf_wE2enw8C@8d@$obY@6z_@(zc4 z5RTLD*>s0rKyTw=YdAtfxX0i0-pv*6G4Io|?s0C>fNWJq9W&8IeG;*_}EqX zQx*qtt2%Gk+r=XQ-Y9PV464|lvM$4jw}QPBrKS@A0GN2KTd6VRHt&ot(Rk}vv64E%m7yMH&m!qZ64JM23uf{?qGPh-!Es@uF zQ>O3_Uo@7WD7I**5+koNxqRHFZB4*ulUC26i#9hk>08 z>|>ZOu$O@y4eV!NSK7zG&Ia~1u)Bf14g6qWe*?c5_`|?Y2L3Vdn}NTK-Ue8}`+z(B zmSfU6Pd@Tfj`CcG>v3JK&waQb_vQZ7gZfY}>PJ1PFZHJWJO|IibJhJif~%tu2<8m{ zA6b?l1K3}-Et&dkwpbX)q$C`P?n@;aQB0cVBEQ`gGB!3;i86pSxu~Jd3fq7^@2%tBWz_#Tb4yH2{9c Irhhg63m|?kQUCw| literal 0 HcmV?d00001 diff --git a/helm/www/lambdadelta/images/osn_32.xcf b/helm/www/lambdadelta/xcf/osn_32.xcf similarity index 100% rename from helm/www/lambdadelta/images/osn_32.xcf rename to helm/www/lambdadelta/xcf/osn_32.xcf diff --git a/helm/www/lambdadelta/images/osn_label.xcf b/helm/www/lambdadelta/xcf/osn_label.xcf similarity index 100% rename from helm/www/lambdadelta/images/osn_label.xcf rename to helm/www/lambdadelta/xcf/osn_label.xcf diff --git a/helm/www/lambdadelta/images/smile.xcf b/helm/www/lambdadelta/xcf/smile.xcf similarity index 100% rename from helm/www/lambdadelta/images/smile.xcf rename to helm/www/lambdadelta/xcf/smile.xcf diff --git a/helm/www/lambdadelta/xcf/wanda_32.xcf b/helm/www/lambdadelta/xcf/wanda_32.xcf new file mode 100644 index 0000000000000000000000000000000000000000..4932d34954317fb2a128e25029b801febd33b1d4 GIT binary patch literal 3026 zcmds3YiJx*6h1TAP10S9$;K)^evD~__Q%E~rmZQpl?tiF3cgB9JF|7OJG&XX*$ums zHYxO>2!beWf7m~Ywo-yrQK(QvP>^grU_)u04M-z0X~Pe+%}WiF3TR$)^B+6CE027RITB7+Ki_2R#Gr%E3~v= zk7rD+kjq%fWuc|1bRw6@<+Y_Ai{{gVajmxB_cBh_+p=2Z#Jpr5y3%HpETPq;MESY%`rQgiI1CkKvI`-V(D-^ zzhiVn>s(zG)~v=QWwlf;Yd@oRZp;l9Y%{ODwkxNt%Vm<<20Nay5_)GtEpMjtxzTJA z%8L^#mM2rG#%96VZ36D?S>D|TaP#UX#r2w7SuJiSu3e&PcMDoqh>BmW*Vk)e=AqT@ z7_r98j5Jm}YgC-0`J%q`@!5;bU2qZwG=XucPYRwD~T7~*WcCC zyBrU)h7OrlddSv#`@1}}4to!zQOA&lLh!!4D&*#TBXHce&>#!R?F*~D2XCQa7QzVp zUgbplloqP6Q&b(5xFmDsXQvpZpo0~aOAfY3bwX4wIz?8UatY5wbr`5y0<1bNQODy6+{@gE}???A{CwU zZ8TeSoDwn>MozIEzPu!z%6VBq21Q_i*l-o`qEwhlO%9(DTmf|;tMVBlB->G|m(QS_ zQ~Q)K&Z3o?4342-gLRxl%7}%@HS~a?VgrC~=s1b(Mr?moLqIoXglK-7VIX6p93$GM z8aH&JlmT2ZDnObHRIbZhi5UqG-6q-I&G5h^NAQdHyLFz zbR7XmH#W7=yr&Q}Dx}BS>ADUp;MmqT#Q;DZRx#B;aySTtu57360m!N`ufrb@-Wm}- zqyV?9<2aySK?-sN)fHL-7;mi}P74JY=KxYUOwA2BL@kW7#aiJI_R$aCT7e#J9rEpK z+!b&IeyaPjX3y`<>oy88`i0wRAxLzB9J!4Lym%eRLGr*IBbNZzv%aBhI(Bw$E4q0l z^AX%)aC(23uCM*|+@H*^1AdSB7~to5Nr+|!<_@dhF(>h9#P(;n-;dF|*P{Raq|i6a zX`-i9zVSIx@bVDwql^PQ!Mua$ec)daZMYr@(WSE-CHjInN6KFpnZG9bFZU?*W zWHT^#5u|hYV$D9pJR5L$@?qvle5a@Q%z88FHd7iKD`XXe60*l-U`p`NKjt%f^MMm^<;W?*I1Q$7?lcnbAQ z1q_}*-V^waTmZiSJ_9}jUIDK(8K~!;sIK3zulw`-BaRm@*vJ66)UrZ;wM@hQ0tSqI H0pkAvkg?6d literal 0 HcmV?d00001 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/static_2/notation/relations/pconveta_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/static_2/notation/relations/pconveta_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.ma index 37dc822fb..d8baf5703 100644 --- a/matita/matita/contribs/lambdadelta/static_2/notation/relations/pconveta_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconveta_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌η break term 46 T2 )" +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 $G $L $T1 $T2 }. + 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/static_2/static/cpce.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma similarity index 50% rename from matita/matita/contribs/lambdadelta/static_2/static/cpce.ma rename to matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma index c24dc49ab..af891c071 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/cpce.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_2_4.ma @@ -12,28 +12,17 @@ (* *) (**************************************************************************) -include "static_2/notation/relations/pconveta_4.ma". -include "static_2/relocation/lifts.ma". -include "static_2/static/aaa.ma". +(* This file was generated by xoa.native: do not edit *********************) -(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************) +include "basics/pts.ma". -(* 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) +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 - "context-sensitive parallel eta-conversion (term)" - 'PConvEta G L T1 T2 = (cpce G L T1 T2). +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/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" * ] -- 2.39.2