From 7a9b394943d524181128816a4b02152aa79929fe Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 7 Jul 2009 13:15:30 +0000 Subject: [PATCH] Let's play a bit with NG. This library is NOT meant to be the final one, just a way to experiment with features. --- helm/software/matita/nlibrary/Makefile | 19 ++++ helm/software/matita/nlibrary/depends | 3 + helm/software/matita/nlibrary/depends.dot | 8 ++ helm/software/matita/nlibrary/depends.png | Bin 0 -> 16838 bytes .../matita/nlibrary/logic/connectives.ma | 42 +++++++++ helm/software/matita/nlibrary/logic/pts.ma | 20 +++++ helm/software/matita/nlibrary/root | 1 + helm/software/matita/nlibrary/sets/sets.ma | 83 ++++++++++++++++++ 8 files changed, 176 insertions(+) create mode 100644 helm/software/matita/nlibrary/Makefile create mode 100644 helm/software/matita/nlibrary/depends create mode 100644 helm/software/matita/nlibrary/depends.dot create mode 100644 helm/software/matita/nlibrary/depends.png create mode 100644 helm/software/matita/nlibrary/logic/connectives.ma create mode 100644 helm/software/matita/nlibrary/logic/pts.ma create mode 100644 helm/software/matita/nlibrary/root create mode 100644 helm/software/matita/nlibrary/sets/sets.ma diff --git a/helm/software/matita/nlibrary/Makefile b/helm/software/matita/nlibrary/Makefile new file mode 100644 index 000000000..33368a32d --- /dev/null +++ b/helm/software/matita/nlibrary/Makefile @@ -0,0 +1,19 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../matitac +$(DIR).opt opt all.opt: + ../matitac.opt +clean: + ../matitaclean +clean.opt: + ../matitaclean.opt +depend: + ../matitadep -dot +depend.opt: + ../matitadep.opt -dot + +%.mo: + ../matitac $*.ma +%.mo.opt: + ../matitac.opt $*.ma diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends new file mode 100644 index 000000000..857215f68 --- /dev/null +++ b/helm/software/matita/nlibrary/depends @@ -0,0 +1,3 @@ +sets/sets.ma logic/connectives.ma +logic/connectives.ma logic/pts.ma +logic/pts.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot new file mode 100644 index 000000000..710415825 --- /dev/null +++ b/helm/software/matita/nlibrary/depends.dot @@ -0,0 +1,8 @@ +digraph g { + "sets/sets.ma" []; + "sets/sets.ma" -> "logic/connectives.ma" []; + "logic/connectives.ma" []; + "logic/connectives.ma" -> "logic/pts.ma" []; + "logic/pts.ma" []; + + } \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png new file mode 100644 index 0000000000000000000000000000000000000000..631218af159fc61cadef10e8bce1304422377a7d GIT binary patch literal 16838 zcmeIaX*ibK|2KRRQIw$)3Wa1hAcV}xREAWN%+VxcDMF@Xo+=3;B&lR7GS5XKLWayk zri_s()BQQyzu*0T-rUFWym;O`$8qm%r`_c`uXV0-t?&0Ut^Bk!RW@y8-$)R|rsJxL zrwM{W2)|#VU5{VK6F!muv))uqMUhw||BWk53MGhL#Bs%=+P9;}I~{e;I26fEIqaf% z%d~4uizQ6y)bnTj{{D3S2|7#PN>g+!u2@>7#n``ykn#iYb?sk`M~I`8hO#g%&F+C7Y7)SEpfM;)gbHH(f6**%P&Uwpb} zFC{m(5PiAsuKh)HCam6$S_ev4y)$(G{Z#>f<}H_^6Y%&k%T-Z!R{HhdT3Vv$C)E>A z$Iqmm^^hlMXnX{$KAIjH8yh2t;NW0JKgIi17x~KBUPv7%QT7-dy!i+N{^VV(K;^X3oj~_q2eDg-p(ecQ> z{rgXyJ?quba9UJM?1}Wr11t_Z$bsEIk;qqi!NP*hPm%JK_QoAMc1TD_$nRp5=ijOz z5bp3wO(6Ujzo?-&JN^2rqE7^@f(j+M@197!Ym}yP=FFBSPoBiJjB4D?eD&&;TB|*M zPi^7RNcHuCf`U1Dd1alQ91{~0$izkaQyqvQSh^*(FeOPBWe2L!}7U85ir;u)VleL6Ke>lGWzwYZ1`V-L&7cN}rxGQwMPf<1TbdlO+r?20>-D}UbvD^Rj+c)iw zB9|!VljUV)LKe*j6qS^A3kx#~2ngH>mwuK(>@cCGrj~G9l}Mkj%9hk}x z*+2Z3zdZ4JbtcL5^P_)g>FF<8j50klOOrf&cw4xjv9gnsB>nnz6(L+9pFXMLq8GXf z9H(Yx`tv)Oyr^4`U9+~X_!zML!TtO0@2=Ew@83_i(TnoIg9pBWfghre*a=y+i8jAu zzl8O4|KY>C)!~9XM~<+aOEV(3!Cg;JrX4#1A|hB7RaD-ck>O;fOQ+GoBC#o2T;J`s zCL>^&cdxlwM^RDHr0U@w-5lH9+}zx{lm3V5o148KJ=)64$JbXADWZD(xQ8ll89pxk z=E!O3UmvziO;7jbs|S=*z6rtpxIWf;Xy=g|RC22eJUcl!GHwi<_)t+{y1Kk*d*eo5 zzGB5)JiXoj{IlUo-P4a)O7W*(F>c%D)s%eBtm*Yxtj&RZ#efpZH#8|JDH5*B5_1!s z0W(8&#{|O720n-B7CIefIiO2CQ2pTGS3~=?t(CpT10^;5f`XM#Wt`Km)NyL-=$PV_)=cv)EC=N)h(d2?4+ z*PZZ+Km{cwrG?*(Cx3mv5*v>aWYPSlbZ)%;kadSdk=hPf-*}Xhwzrq)Hh3vK5xPLh zAz|x&Q<9_m(jj^#Ci5)4wqiFqY8skQE&k_MVqG4eP*YnJu+U{~qIl6bGJMkQ&lbOr zrqjQE#k;MH8ebG*T@VPkP;<@7D$!+W?g91*UUi!JBCfLHZ~x6&p{vMc#||;el9i?T zUvup?{a)LR+=GHP;ltF^@S(D+3ueoUb#BV?^2FR^cgX$wj78ObA72)5kE(FF+{5Bj z*ca9}6zf(|Em&MrRvq~J_f1+VO8dD5Au|h$fbO-``5ea?z7M8{UTDVn7q8By-3k8~ zaB7>0;ytVO_q}1~j7rIg;&NS}Fslq6$bUnzmyvcCBQ2+swA}L4I>Kb4BbPxYb%I_y zC854G!|eJtW6i+ zN>L%b)55}{0Ix-enlm@QIlsQ`X))2W>iS7aVO~|>**OcLj?O2SN7A*oB85s6Psw*qR-vd&Mc+rkjuWF*0&w%wjzFy1~9Me=+M0)w#L3 z=i2+sD}y-{6}8WvRl0utI&avCmfIpoC9F9pmTY z^R9g=(?0rpG2MCI`o{I^ha6*6-kxGIaa)~o7%dUdl7V6x>!kFe1 z{T8bzJm%BMO^V-~`F~$>QdHz}TRub)mu1nic}Xwd%rg7V;TtvSy^f8>#Ob6jE++ZU}0ja?<#cOK%hOaFAIavb6yA3^sedOs#ElWp6!QMn5k6?}5|=knsx z(iXx$C@3-9$jMK3X-wqvmoJCSMO^;eq?B(-GoGAY#xA9lr=XzdNPnsjFWAV#eZ#?F zFYzcc^4}-dVQy~Tk^cJiYfhi)i^8GTdH3w8pB|{L>gqBDXIKwpIZ{Sw!M^&j*hp!EBav&pFf}A=6)*bA|6*a`c9GhMj)ld3!-Crn>?b;oV|_i>;-@82 zbTjVyuG*Y=ogH<`hVGnA;}Qzj1|mf->so6|Tj)eZXG6_En7DCqIzQ4ONV_0#Y zb=#G`;)T9|1w8gsXU>#kIivN^&}`l*fBg7{wzf7cW8;v?qNUA5j$Oi2w^c`?q#;r5 z*Fd=Ovz#2(^_~=xF`JJZIntW%Ab7bpx+BTqW zF%Dfv4GlT;^z>}|K5Ve;$hrPCX(bK_hP+xI{u|7H6klrNx;bcW&i=^}JH8Zy+#9Wi zR+KW9m#x0P^|Hvut;^axwrb0K)n4fwg{3}EOW?zA9oc&=r>QMBb;78fhNH-3$^KoV z(YwoE(#Jg5=-2;gN^@1R8>$_j?h4W_ALU?G%+1Zk)44j@oKpVti-xA=iz`nZy_Z*3 zj`MGQsJ$-{)7jv|<=VQ(GW6lYt7w&EN#K6qi!$tW@7~v$Iysvg-%ci;uE%b#YH0~? zrxzBmEYz693zPO-jkdtU>6A4lLSIpvmC&?!nf$V*xEe-omJ5`$wYQJt4n5`Z zQaCz4**%mWy<6l?m&b0~iH;+0Gcw{eqQtNQ@W&TMUL`%{CVsCjP0ko@Y*f)pc`Rnx zD*yid`cE>V-y>_ds=c|Je6;S8Z&D z@})07vaqqK9BE9-u>3Bp9xKZc6cm($tpVucd#S0`ub(#TO8-FlW;=!_apMPV@XjN5NuNb=uW;}yXQxYdeVLkCfywktPzmY7Krv+`cr-OL%dqWLn42+E zkKMX;YY%2eRb5^2^l4^M_DzE|k)Am@5^waf{FgTKHA=CVFrbF-Ogb5>te`;2yk*NN zu$rD8lLP19Qqi#-kiU457p-qWAe3$W&!0a@ppLE6`+KAj_400L=oV8`Q$~PWVB_-g za?eTOg8;V_U;o9e(XuY=etv#A*ZbFFi8C=X-^GNOVg$ba{_GEmk5=6b3k~)B@#CUF zq0_c=sRl=}R8ff;nV3Ah=(d}p(fIoMx})TEC+bPFn0U%3)c5>sO70l{GdueAs;I4l zg9;X8Sy>sLt@qTF?ZVR1jG@4cyDu$D{lelE1z*m!;R=h^2kUT}jCoIihFh?O2hwTIFQU7dFGW@RjpM<@1l zUlQT?_U#+VDeyBnE=yt{Mt)!}_(z_X`9j&f4IL-`*|%?Fe0=;HpTktT?!Oe1oBDu8 z`79;_1L?uF3HQ^lev};$5@I}h^eC&i^-fT`U1292Q(Z4MTovWtw@<;^THwZw8#yJP zYipIQtPT?Lz~2qek9V9Hs#oFq`22Wi>#M`k7D_U#Ga*w|7X-DPD8 z0?#q`J)@%mB_;BqVXC-eX&D*Er(0g|u$ZtsOH8B&ir}L&0LLW>q?VTZ^z@C;IkZPG z2NJD!baVjZZ3K6gIC7*E1fL}PH*fx!&~IC13sUw3ti!%KmU#O5{OHf0pu81cXO)zw z(W^0@OVf847#IW=TwGi78akH zx>-X*!|R-n14dkDhnMo`R+^c=@f=^Uj{8&=s(G;D8tgLODHf=Jwo-+1cXlKX&Zabq`W-DlAf~OYC1`5AvqlX?OHl z{nZ>|=<)_ts8fTSLe!)u|`+OKdK%ubPDEJ%g)GP`*1FZEm+t6 zkmu!k~W?JVp%_aSiofszOck;^r# zKZb_pTPwP|xvvxld(>1SoP_0>BP$G*y;vUT3ym9Y6{s+}Sb| zGD%!q-0s)DY$Li1foww9gS4AAdCBh@o{o^;C4coQKb_!Z`3%Br{kMvs9T%*uIxpp* z{(v%kI;K>kS|PSOlH#n6&Uzago13e;8>lEBJ$i(N5SsKk;(_lhMmI1r;&=Yt<`XLl9_=z^2$g zzYN$!8qzsgMS4(u({KMWrS($4*8!t~2(RrT{Ny4r#UjC*@TFVqD$_k6#PjI>Bqi(W z$W2Ks=XC@qd3{^kMpEtSYs<{eK9-_0FYy%0-SACGLSA2ghj>9s$|hsCmBU0yb2AIG z-}A~}{98AMdJ>yAZ)T*W`d9KJh`*{@lxxi%5oSztd9-Gdr(VjS^}eu;=w2ODq=cBI z_fmTwE-QNY@X>^N`Q#>rg!(u%Ey4@!Dd_)8UVDq zlG@tMrWve|Q-EWjF{13cE5wsuo}TOIsxAamw=#Ymoqd^-qNJg*32TLv0l_3uOYBN7 z7NnhirB0cgnD}u_f|~MZHeI|rpC{_T){WGFXTT~w!^5;CnL`cwbrlOa4-5o+v|3$~ z4F8IQc5AVcw>A=_m|`8FoX~4O5ryIyhb_A%wcg4`MybEQ;sOA|!Gi~(X?`8KdDYT# zOl&z{pFS`x<)D%W1+Hbsl`}W(nZ(RS+ zA}8&vzw5f+YUt<)1dM|c7fGc(R9xXAL+pB>+SA)haplUDP=;juq=BKKhHODaF~|Hb zp~q>3g`LmCtqeTQo;`bu%?JZUpGXzou>960-7N0b>Jp^B66`zEjEKtIovzA;?ys7z z3B*m$%$$Ovcq2JAb+GLO??Y=jEsiyea7IEUFcH+3fB*ht*s39JQtM+dQKXvL-(S8m z3zaf0O%TdzycYlM=!AH2?se)ZIy`&#(g4MOs;wQI7#bLe+gwv$ z+#KgEuJxC1lh+jxP)0w>o<6*K5b`U!NlP;t58B636O&z(l$4A+ch+=r`Ndud*d)ZQ zfFHH)%p-+T$PnE46g2UduU}J6sbzO83{tOOZwgp$pt|_yPg!kk@KCNvgilh_HI2Im z1qB(v5ip<%P>h^T4s2IoLk03P)~#dOy7k`iP`=W-y1KDF_YZg|QRxDjLX@=~Z9e!s zDT#-NXB|`sW&9!8VEg;c?1TD8N2})!A4<@3c9w!-oNxI6BYO7oB`r2cdUkf@2fr;$ z?Ck!KQOMR0vE`xC7(1Ii#S5L}>nne58RXk<0;c)&=~GYYyHxFcx!WZ~MYjTU&~Dgp zK}w8mkOCEeM?@rabStYA?X6q4u$>`h9z%V5p&t1cg`qx{TZ=quApn?FfV)x+^SwzV zhAU%Mc5zeD(3n9eHPG_%_I_KPAymW2fAFA^vhsQoDv>t^sDv4$^dP`j<3akg{&E1)pNO1K0IWMUCZm6N`LF@mcnfm&Yu=2&p*xH!eRYLS@0G2ridHRjB z^foy=JA-z3-XDQReEuw9tC5G`?? z68EgdzcoVKhLZ%eTef(*ySsZl($Fy^2pz+$D7TvcOH-Mfr_d5);db6De#yoxcv@LX# zJ5UROofRMf_Vx9p+mGwryLXTN(@oBOC4fRxK&|~H9_v2U)O>(Imq8MWj~_2g|EOAb zdRMv7V?h}i4j%@tiU&L@_hVy80TI1~B1+uGJ0PHXUC6u#<=EhtsN0i;^R`ffKV1}- zp8a-4H{bps#xhspB}6YG`TY6wo~hn)lHk|3w)&n;*6D3JXY7)$$uN6NPmleeVcsL? zAToc36Mlc(ZmgxIrsk$xx}W$~cYg4ap14gHFY#k^R4QF5$mG~!m+-oT+}ubAk#6;P zSjTrUel-h`QHEBt!mbjl+4J(%t5T6VX-`n-XQ+mdrR1+&+xOJz=Rb3|qK{6MGsqFd zU~Npb-JWtE`CTR|uT@wxbOS+ndr1)#0-@HaQyzG8AL#KhLqo&Zih2w8Jy=gz?qC)Y zwmk&7aG_AXWjG_~`?5XY$E-KC?wU-^=$9$AU5q9p4T(ASyKbEo`b|ZJdsGg4@&J;F0Q() zT#yWkT_;c0xyohB&6vJP%gPGtx-+9O{rflX164)f>`a^PB5ULPqW62bNiF+Jj8r(f z-}lzmuUJ4Mc(i-MPBf)CifFcXq~y0aV?b2yAe;?}sXQvdjKmXZ#~a0?&8}n|B=B4c6<-Paq+O623@uQSuEA!n$ zU9q)~59%uuIdu+hKRXK??P7n91n1UiRJI67OBYm6k!tSc%KAk?D6&3(T@J|WNZ+XW@vK6Saw8&b-H?)=7VKTuBC9i)u4!NE;KLqjPq zw6I9j_6CYrf`&^?NXP{jlROpLS?uO6m|d-;<8-ArTnob&v|KpUr=Yqa*h zZ6mWze@2pGuR@@wayN1w&vGpkD5O>#s@%VSKdEV{@;(EAvc7%m)?o;N5NRNRH%&Uh z?xlz$)%<frmOaP>alWR;-KMd zaQ`mwv(%Gj1Ia^~m`-VFF;c|cyGIpj50`5Ej60jS`R1JxU(JHxVN$sZi-`R9X~Q(T z*zo@O^LzRcHDB<&PsYl|5MO6UTk^k|T5>TmejRcgl~`GowjLX}v;3>FBfWTSWs=IB z(|Ig|=5T>hw9L%R!ry}h z68Civ@C9xU(*AE2fSVh*mr@?eI^Q_#!arM0Dh_8WCycx=`mfx~SH3j;?}|oQ$j_WK zcm2~~#QlJgfVRvB9Tgu319CqzEtP@(1J!T1&(s%PoO1SKtQ2uDFRfc4Z_pAeOWkX( zaZZ8;Ir4yohGN~2gG4R)wkKR)Pr z`jz618^Y7m)3$4?E+mpTk=XDfd*9L-8_0YcH*U23)u%Mpk-G(}8qHS1Zjk=H<@bi6 zHi+;`hdYJ^-4^M5X$6ZGxZl2eSKrV;$qko&awhYj24KhCyLU0Xny1PcR_$U?w61(u zzG3G8_(eg$LUjqR)O;$vfdDF_Bo-DIDG1oVrVXhxYcMnR%E}hCi*?4VHH8n&T`^i8 z^(!Ecjg75i@%*4Qhs96xF2Xix5(H^JcQZVsH-`Bvgl$g=#ZC!Zf=IXSlnm`|8ar87 zBDh=DVZxvQ_7W-Ck!Cm{53mqx;j9I4NVs!I+3yk(x-a!$x$k3ur>vDMsUl8x72fXk z+Fm0r)N-luS{B(D^a^fY57*#R^VT%9><_j{Jbhdxgfp?CLiw7d<#Rle(1e79s^Cev zr7-FW=sMh4+v08Yee7w z-Q_%ay%BAFD+hr06MOtHK^oJ-~8C zRh3p|ZFz=IW%-Y=4Vv$J>&_EJMMZe^&o&d_JI?vrC-+{SPwWEJbsCJk@(CsFp2BW; zd`~2A?Q>b^_2HB1q1j&oH1`PJ3fC#Z4*4+HH#WAjPtgmUj41 zfv?jBA#Uz0Jq@fi-kxxtgTTb=bcR(;I+lHdgI!<#BB3OeJ9P3Dir0Y`4phfTIq-{# zJtn?3o|MyoXjUkj)FNny$WOo9+PvHK-ZE-rgm}<>mx>y$zC#*;lzCwfUCUypVc`5Q z>9*!flxzXW(CQ!Tr{yiDry*e$8Y4-4AcGj>*itObje8mhOs-U|99Q)$mB;&@1M`vv z7mD*4L{ks`y(=jyE4AMS7dg8>1wf>g7(GUg>9Xf<6m7bAN3LN$8XL4E} zTn#>-0XFYLf_wH*rxi?Zgh%vip+Dpp|JFW;RjMaXk`n!&l^vlBD+!#iawsJ0iKVopX@CMOW72lx7LFf34u4_zZGoV1(VegFE7q@s=TbB(YMwaJ z=Q?JOr4k|QA_nfuV3Ba7^Hd%YwH^v zV>XG|wtYJfVkTq`1*GSGWaI{JlI{RzGeO!XJpiccV>H*3N zv&9P@`q|c`+Dt&|4aUmZec%8+GEs^ECg?W3!^5BKnlOdrEQpJ5|Ni|u$-)(q-@aug zNKxY!JBppqrO#WbsHmn4vK-6BN@`vuC-*ngXIpoceTfo(5EiF?nGO3z8Rs?A$J1UMggw`1FrF{>GI4k`VFn)za3!IDPrj zl`A|L1~N}qEi634!nPrsg`^mRv9U3hG&BhY)C@9228~*go2mOF|pu1eht9QqJRxz!me|2T4^i9&;%ABonWEM%F5pU@j#_#WMl)x^4m^MWss^kv`oD3Ax?Jo>^6jK z@N_-iz7>WCVMlTHUo#;yD~nF9^d`=JvI`+??J8VG}8cc=%%j0|Ol^ z7;h+pft6KC)r_U3WzX0cJybOQuoDRQ9et&Jqa5mAFFqAYC#h>fh}!6NH>TBMH(c{L zon*wV;!eLJ?Q^V7Bt@RRc(MNQ;lre`33d>PS7(+gm!< zJ?Bo{NI!Hg4a>g6?h>@i+>kO!0xaUuog&(6}OHo zU29ug8Sc*B-kvewqjUjt`8hi~5g>-2qoeVSBVVBoLWqQL3u8)DOpG*nP@M5KJ3HI4 zQkz{-Q6bQu{r>%+j&4QRqvYh|suODDjbg^(uT+=sKlC=8=s%7{s=e=Q8ePDz%LeVq zP1hhk*{K*gKl|5(L7oy{4^*iDU9GpAJHTRR;ozk}v44NEHJ3QrqRhmZLzP~GWcXJ?>Qpm^fx z@1vp-9+i|ecW;dyB}Hf`(C~6_JCJW7RHNy@EP`bSv7B#r!?$lAteRQp=WosDoT^;8 zJNSFG;oyIL zmUW3J6u1r2sQFKGI)A>(%klhqHqx|#o*|=xs&`>q>u1QHLl*Ei9bk61j-RJ8(vE)t>CY5iYXMNDfz0r`53wX{l77(tVB z!aP8k0WA2`BTBsVbahz~fOUMjj&$6m_rcpBK}kcy{U=ZSkuga10lx4A&_d{%qQ5dk z1@^-z8$C(J1onsIJ4`;y%-mWc*ex0%d}$*o^FvHjj})dx;z;_Oj1!{K+@S4$V-btf zmkjc5ZXol?xM9%mL$1rWt>eiz0==}ZMqYRkA5Q@`+2PN3@E~ajkmv$^l@$3Qn3~Rw zeW#_P6It@Izubch^Wwr}SO=+%oD#$s(1pu7a_tV;4XTqP06Ozl^#mDMLOH--+(xy4knDuYnN2N~@|iAk9%(7nlllfC{kmD#wmlXw^gm)Zn9k!7cpeRhjM{2OOL&m`7L>aLVsZv#1nBq~ zPrt7-p=eft%R|PmR#)eXd5~s0{c0;IwKk_2hk*Zvjv60Qw*h9bU0rtEDS4B&+jZ$6 zM7IpwQo&Rioo>PHjPKPqL<}>CQ6)1oo}z_5x@8FPN(hc1T7B=J{(DmPPS463Kp=|h zs=0Y76m&9!O&T#cKG6Q&svPb%u)?B%jjkC*a}dObvDS=rW&Yb~^UehG;P0IFdIw}o|Q&z+kw zWET01?~Q7Lg^EaRh=LIO`BllaC}6I8!TISgwKNORLUO4<6e5BBSX)*A$2Qa3Lt|rs z46+LZNh2c;nK5#31Z8(Q1>_sdzpQk)JDrl5`3MX6IJ4h9*~K4Qj4UYRkIg=ouE~T? zb)5Lr(&AteVCpm*;?j&vu!656|}Xt0#Yvu_?=4-D*^m z5x60}aPS0#+;dz*%9#fnnO`NN;B@o-aVVIEtv~s?Jyo8p~ z471A3_q@E0az7wx1-K0w=Wc>_fkF2;oEyj!)2@ zNz(Mfi;CPwq2^(Imu6Mf)F@&chzV(wRZGYs;{$$k42OLL!u#>ORE{3?IG$fyH=-L* zYEpuVc<9zo?N0+Yd=-g)hOAn3&ON1EfA)r=%Pc7Sx^Z8U- z>Op+PO!)Z@Lzmc1h@y?;xvoee-9df};*ffOlHxsr@s#p6a-(rnLk%5_G!`H*WJ1tL zH3SC=p<97=kvn3XZyyA$Vgs@AE5vQgzKsK?7AWN>3uZQ-)z;QR6r`!SxdCn)lzt@_ z*G)+pQOc#(zQ0HHUpYQLuMFE2(7HNy2 zeEN5ig01oK@l@`lNQ*8T(_wXQAtY^kzl9 zKG)QUN)_R(%@cY#cncJ9$gev{jRyyMY~Qg1h2b}|3qIpfR8+f}#^6u%lYVdL_OlWO ze4&wnP#^qY7ioeJBA2S+bO8j&CG`?N#IZliGj)psW}kxc2f$6K|GxqAI{|+K=AW%CMy0JiOTVV|D#Nhl^N^p?ipsb%_51hp`EIw^Nn!7f zm+gL&0|Q=U|CTC=?1Io9fwM4i8a$Gc>;POjw|{XXJMM?HCNLFF{j5jX9GSVDmw(UB zCft6t+IW?cy9_61d=Y2>xO4Z#QMRSST*rlxh6tD>K9Dn4Fsh4 zKq>!gqRw-cq$LVHDzwxjE-z2=Pmd>qx>)$q4EvlzPEyidin#Ii>@$FhhsDLACKgmN zb@g6eoF2$Tzb>lo`8ee)?kx{V25L;?`1h$-GnCJou9>6Rbxs8M1qbuRXsRd{|2_~T z)hgBX*HcvG-#RC8u+Zov!U@CndI%Bo5I=tWP(;VaU?+Zi1t*K!C~ zW>SR4(uQCBkErM)*omcH;ioWM(!ZMAm$@E|_$t~po}9O#yJ4YI7zXC@yI$o^ zcv)2Mj5U1*D32ZjY~)}8$`%B!d>w1g4jE062~2wGem6o9A9h`2rT!l5iVmt%4TXE)V| zVK^JYOA>VH@ig&pU8v3RaC5pS@*uoURrGx4t5BrHKVsR8|=RWG<#1BIJB%?8O2hCw459ppldJK=}lq!S_u zIXMyJqeKRgG@VHMM-}YPkVWJKRIN7HLJ0OeM7GhYt02-)Hg8A5++A-MQvbx}>A@)| zZ-l!^7$-g7VTVxJP`>D8s@FiXekyl8o=y@AE7667@Bc3 zC&P8c2`Tb>E0W?fTF{(|)>fUNlQ1F#;*Ngz)Oq5_`)6aIIxBIFBcw`Bz6eR0%s;^u z@PM*xhQlK1Z`o%n6(eNfH&#OPzdqG-6m}&&iU^qy3Oy<7hXhMTn5kSk;Vh4-Bh9(Z z9Fq5-%aG&|OmqPUKD^M>H!Z216*&g1(GNsUx{sPMlB6aGiE$myejGC}*!fpLuIC1& zA&^%i=>j=wk}Kh43;4<3OHtFYm>@+_XjI|FcAmuPNSQ~=xpD42`Sb&1{M}nO9=cMy z^ML+)deRgvE|%-QM8?~?c#RWl3nU&{coHeX{|fT;rF|bMR0chc z%;+G{zW@|_ zxH=iRLx&)pa>CFKAYJdqaVNTDoH7Q_q=6VuxGru|Hq&KuuJ!Qn82cnrr|Z7y42V4+ z-D#X(Ms5I4kD@2sBH!83k(9;Bh&g$%dS#_|Xo!YXsU00NRt~Ni!?Gkb4kM#rXw3*3 z^C0|3YUKR(wNoUZIwuf^g^heF%TL|C*BD`Ipw1>u3SP`9?Yw^ z?ej%pT)FhimrbM)VSMGvb78qKf}k)X|6YJAWKzDq{=w2HQmU`CKlew^0%&Z3I*U^n zSEjSUf3c-V<=5Q&A2KM9L&M-|6S>G=(m9z;?I?ExZyWo)ovxhH@*Y%(A?uj!KVY4a zhx7CD+AhY6y#);{Q|EqQdoBx$4Z0C{p%*kvm;n$r2^^EZF&~8gxhNc2l}_rt#Z-y) zS51UibC$s6AO-&$faNO(1I*z(+orieMR)y?gh*m$Q9jN>L#c_|eoy>wo@Iga7>12E+)m=0fx{ dyH>fj4}D!{Tc=`)znFnIuB54$s$g>We*s~bpfdmf literal 0 HcmV?d00001 diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma new file mode 100644 index 000000000..aca4af449 --- /dev/null +++ b/helm/software/matita/nlibrary/logic/connectives.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "logic/pts.ma". + +ninductive True: CProp ≝ + I : True. + +ninductive False: CProp ≝. + +ndefinition Not: CProp → CProp ≝ + λA. A → False. + +interpretation "logical not" 'not x = (Not x). + +ninductive And (A,B:CProp) : CProp ≝ + conj : A → B → And A B. + +interpretation "logical and" 'and x y = (And x y). + +ninductive Or (A,B:CProp) : CProp ≝ + or_introl : A → Or A B + | or_intror : B → Or A B. + +interpretation "logical or" 'or x y = (Or x y). + +(* BUG HERE: WHY IS IT ACCEPTED??? *) +inductive Ex (A:Type[1]) (P:A \to CProp[1]) : CProp[0] \def + ex_intro: \forall x:A. P x \to Ex A P. + +interpretation "exists" 'exists x = (Ex ? x). \ No newline at end of file diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma new file mode 100644 index 000000000..623a87a18 --- /dev/null +++ b/helm/software/matita/nlibrary/logic/pts.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +universe constraint Type[0] < Type[1]. +universe constraint CProp[0] < CProp[1]. +universe constraint Type[0] ≤ CProp[0]. +universe constraint CProp[0] ≤ Type[0]. +universe constraint Type[1] ≤ CProp[1]. +universe constraint CProp[1] ≤ Type[1]. diff --git a/helm/software/matita/nlibrary/root b/helm/software/matita/nlibrary/root new file mode 100644 index 000000000..8fa6d62d3 --- /dev/null +++ b/helm/software/matita/nlibrary/root @@ -0,0 +1 @@ +baseuri=cic:/matita/ng diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma new file mode 100644 index 000000000..c06ce33f6 --- /dev/null +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "logic/connectives.ma". + +nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }. +(* This is a projection! *) +ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f]. + +interpretation "powerset" 'powerset A = (powerset A). + +interpretation "subset construction" 'subset \eta.x = (mk_powerset ? x). + +interpretation "mem" 'mem a S = (mem ? S a). + +ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V. + +interpretation "subseteq" 'subseteq U V = (subseteq ? U V). + +ntheorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S. + #A; #S; #x; #H; nassumption; +nqed. + +ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3. + #A; #S1; #S2; #S3; #H12; #H23; #x; #H; + napply (H23 ??); napply (H12 ??); nassumption; +nqed. + +ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V. + +interpretation "overlaps" 'overlaps U V = (fun1 ??? (overlaps ?) U V). + +definition intersects: + ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A). + intros; + constructor 1; + [ apply (λU,V. {x | x ∈ U ∧ x ∈ V }); + intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1; + | intros; + split; intros 2; simplify in f ⊢ %; + [ apply (. (#‡H)‡(#‡H1)); assumption + | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]] +qed. + +interpretation "intersects" 'intersects U V = (fun1 ??? (intersects ?) U V). + +definition union: + ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A). + intros; + constructor 1; + [ apply (λU,V. {x | x ∈ U ∨ x ∈ V }); + intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1 + | intros; + split; intros 2; simplify in f ⊢ %; + [ apply (. (#‡H)‡(#‡H1)); assumption + | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]] +qed. + +interpretation "union" 'union U V = (fun1 ??? (union ?) U V). + +definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A). + intros; constructor 1; + [ apply (λA:setoid.λa:A.{b | a=b}); + intros; simplify; + split; intro; + apply (.= H1); + [ apply H | apply (H \sup -1) ] + | intros; split; intros 2; simplify in f ⊢ %; apply trans; + [ apply a |4: apply a'] try assumption; apply sym; assumption] +qed. + +interpretation "singleton" 'singl a = (fun_1 ?? (singleton ?) a). \ No newline at end of file -- 2.39.2