From 73ffe6c83179e70b0491aeaaace262d03e72fc37 Mon Sep 17 00:00:00 2001 From: Isaac Date: Mon, 18 Apr 2022 15:58:24 -0700 Subject: [PATCH] Tried subproof, but it's not great --- __pycache__/group.cpython-39.pyc | Bin 2590 -> 2743 bytes __pycache__/logicObjects.cpython-39.pyc | Bin 8115 -> 8719 bytes __pycache__/proof.cpython-39.pyc | Bin 17602 -> 20463 bytes contradiction_proof.py | 26 ++++++ group.py | 3 + logicObjects.py | 26 ++++-- proof.py | 118 +++++++++++++++++++----- 7 files changed, 144 insertions(+), 29 deletions(-) create mode 100644 contradiction_proof.py diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc index c9088261dc660428ff23a2d5d26b5ce36809e149..bc3dd3fc828b664eeaf0575f3e073c8909516c14 100644 GIT binary patch delta 247 zcmbOyvR#xfk(ZZ?0SM&o#U?3oPvqOpST^yL3Zult_ny3BDdH^*Q9>!q!3>&`n{65Y zvNEomY|WlEc?yT*WPfI^NLz*!hG2#wZlL}mO(3DkR3rpqYl8?;I3WgP-4aeo%}Fgu zbuY>C9;cQ$5cI)T@UaI+L=aJYkvjxEAHBfA;hT?w+`ZoX*92eehWTZ_XLfd`IeOz8 zeL~Z^1bUwReddI;S25wkUk__x>YGd>qK%)#Yc@N+Rr zaGa=9BG@j`X%)ZFBgz`rlQ$dLMC`ZRpI70{vQ5P!+daUP&Incl|$uffo~(A&37amcwi8OHPKz z$o?nK&O29ujnTJ>;*O~#`lcP@-<{9IDARa3Qd^i9#*bZI`cEU?y%S??y{92=P!KBm7OSBY@Dm}TxL5G0*tA`5sDmB>s7dN)2V-jz4qm~|p5j>bqDtvs*q}z!N qx72OLvRRw9w)0!9W(ZUWh^nZs(EWNq_Yrz^RgbC>(!_N&)b&3tehw)B delta 776 zcmYk4O=uHQ5XX0RH_0a1Y|2$j{|MC(oTC@95)_8@pu5xhDRt#)C4Z{EEBn>TOv-8|rAwDCZ| zC(wthxry(Ix)z6b^{(gfqEwR#!GnSkHxl!Lk!a3C1`G-5q!WgxUVNc;;y2$940_vf zLG>y!B~d_;u%YU>8js;;b$IJZ3RXqV4>SI3#j+~X+lv>^O&?9mW|E?&&PZX#lW6H7 z_XJr}uYlQu70*5#&FKE}niIxITbSOD~9+5KEQci8k3R=j&k#d7h= zC3EjHEVq9RHkWzDC@Pj2{z& zsHWPk@@*xu>KMTiYC;2Su*JI~2$pC`2KhD7hLTu=S?PbI1T>c|*_LdX6w<8Aa;>RL zw8wT)%x#Mex9zrpvl+sWVCLzNw8uO}gQ+r#e7;#=>|$gXrwOD|*gwPA%@|>fGO~=b zj4{T)_B2zzrBIb~3!p(5LZCtv^^P6kH@v`YqQ_y-kZ!?=j!caI`=7H1*lQMWjJ+Jb f?C9#`XQqHEDx$Vo^J}W+)f7!8iz*R{#6rH`Ldd8` diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index f56f9fb67f6c9bda5b7bd862faa5da7b0a4436d3..0e857c7cc0903b81c6265c5711667f11ec3e73dc 100644 GIT binary patch literal 20463 zcmeHPYm8jiU7vgBxwGr_X1(zv&zqOyNj6UGK9agg8pp4=btb9p(spp-&d#~JJDb^= z-Fxra-pec$oK`&A5}=eqNo7m@P$R?##0RJl9{`D}Lj6!A5CcL2K0qY+j94MT@Ap6F zo;!DTH)&|37Svtuxv%s7zaPiVUAw9|{514Ock}xrN+(Ub!m&y3;_Xs`z@YQBWmS#tF) z-lpzT_v1RP9#9YBx<@^v4&pka9#)5NyI!VO;mC$JG$UIb82k$JO(= z-mgxmlej*hPN~zlKB&&97jS(@omC&j^`QEgI*04S%E6YuI4Hgx^m_C4R%vLXdGF%y z1pdOqDEdx6cRAO0Q9AuRN_QcLGB0JJ&HJKaSyDOl>eOrHL9x@E^E-oTGYr?3SE6>W zJ18vlnw>#0jQo{wFuAlAM(z1_tI2QSAn$jt3@YK;+zKaDD-8;v-Hf-;K= zi!l_pa=|WKHqV|ocIgwLAB30MVYAt~bh3A~+vzn`cTB%wpT2Ulk^lIqld*Sku^oE&*X>1KwCHfMR&p&+YFEw1W` z@l$4IoE57HJidvW2(#j@;)=aqa`xrSliq7*!-?DoxV==kj(R6^uPkk_Ua^mrr~)AP z(Y~XKPv$nT2J^OrxAT4H2H2N!RQYBeeSlV?a^Jm<{#9jP4)^GheaM@lc_Y2@4d<}> zL^3zom9hFD7guCi-Z3xs9(#wM%>!qXE)((HzO$5n8tc4KNXR&N5RJigENc$PJA#KV#~ZBSpIt zPKJ&%97bdjfiHX|gAO}vaLuj9dycnSei(uPQj{<|ttAWPiA*&hwvNnkFx8aiX(6X045UKYt_NcW;7)be~IV%J+U!JLt17saXKqb8fn*J0tBJwo7{e&Vms_;Nmo*E-RlvJ&*vS}O_%rRK_t-&KPWYWP8f{iIxJRQ!%lsd~iT z9UVBG(Jig8vs0)kgtH$Fb6^fLU<>;pZzrUjbgNF)Nn~!)AhW6D??fEw*2 zd$VL}l|Te#62a;(Mir>B1Vbgc(+X{~h@Gr@=I2cNir@8`9yn?MeWV+S=HvC|@opI# z;`Qd1{8lu}3S_xnv(xbs0EDd9j_~aDy1wVHu1Ra#`LUH|&|LP6SU+;iI|l*pMLiF! z8hTc=7Wrr!^>%1*)HJx-juz7lz8KZHvCa5db-$fDPWq;{7Nx$QOKo zuZevD;%vk!0}nnn;-y?Hyz2#1v34I=>eBU9xQ!Ef7oR~P*NT$Fvm z#KiDaR;frN)3eRKk2ZED@zjg5;+N673&!5{Hr-iovv`i<$9E;x9T;7Ed8O0#Lk~hY z61kc|xA}48sZ)leTwJcLns;v(+h(S^WD=Z1_iEt;2a+~ z&yS*LQNXi~TA@hlVimHw0zOw2+n9F`g5$;Gn%_z7jHXGnw5HgXArYh84WmmQ$lZiK zx#31Y&Zv0ZeZvXnps|#0oHwzb=jQs^2e-1DTWe6DkkYpwurd?P86mb5XGm$C0iprYqaQSW^W)(M;PY ztI|fn!T77ESD&`yb2Rg0#^;Ql-eG)sZ|3s@&!JzSuE!mVCRJHf6ObWH>%s*PKAj8w zglJ)N;CZ*I=vszMcY{o)M2km@+F1NY7D4CRU8Ow=^X(vvyp?7&%SeP_w=nA8-)L;ooeL2;S$J>U{NM4&g22)_mGg~iBQ z4rS1I_I$QayBfdK zUT$}die}W3+HC`n7+pom_g8qQ)em9$)IowrSP-to@VD2{|YO%{NQmsHmX?ealOXiKF;7E z-;RSbf;vTWA0_WeGpSQpFLatOpuYJ0a>Z$A;-vMx&Qs9LtDthy{ZlaFllv;(7eN1e zop?r5f3~w9vjH-xEo|sVn+^P-C95A*Hqi0s--!zZXMo2SgBMW7kDklae+LQ=&Z155 zQ5F*vT7jg@X-o_+EBH8G1rM+o!SAZ> zju8AdKI@1|X$mr93cekY8pcJLR?OHlKUBO8E@IB7iEVax_fR8l^WW^S&Bm2IQaiKPRM4%GP9?zd2q?gy{Vb0-Dm=oa zPt4eKqI7~!z}vP|hEJ^k6&d`(ys6xD@qX-j-uT*F>ub|Iq^gS1IPJ-OIis9b(RRXe zky89umI#EK(;wJg>8yKmU<0BIih~R$Q{oxZYywL*EW!}e77`_eBM_#k(>BgnfkOWv zxe=w*&dBf*j$pdcPEa-wS!HJ{tjo4L9XyAP-rO@}@Ff$d$DXW{enDBMFruF_lil#< z*1cQ1wj*Ngh!E++fP@xb)K3TFTF(@%e8fgf9AgD8ArQUN^;a8Z7|_%i2PLp-Ok|Y6 zD_k7c_Alr^WV4(mZzzRy40+dZ4V(`ehIeDJ0o46C|r6o z|F+0ij{nkvOj`>Up6@O835?$}%+tn_ovK}e#=79s*zS5fqZgD#v$#O~3L2;pTw*c8 z*vF)6_WU3Cx-H;6C*G|s0$Vp@43O1WmE==+Ktv;lfUC0vRzqi1geZuFVJGRZLYyPd zc*W{|Q9%l@*WqwCtU{|LaMzn>>zG$A;~DYq*rgi}d`A1|v|j^De-&zlF!v^jvFWX> z!`Te~OE>Zt{D3Zb+O_z=oidJkvYPglCgP=t#P`^T9msHm6*!9m%@X9+a1eNDU@=E9 zL(z;K+IH~+h}QBOykTgX3}mXA$9k;-v+o-HW$;jo1}etpV+57xtYU>)*DCFbpRUu1RBzY1N&fyolxo z%1|^VNaMmGc?Z-=cynIM2XI6x@nFD*k-w0GV-i9Gswv)GPl7b?(PW@rREaW5r(;P3 z2HMt&@$cJBP2w)Ypwl`e1V?uPTBDH-v-B>??!%*qJqH>LL*WqA6bSz&d~Q%QfeuVB z@gKpj2LJnNc1Qz%j;O&uJT`iUCn7}x+e#c5@u9j8%xI3x&6|Uot9_&F3o^m4$Fm8x zm{& zRM|^Zk(dZjrDA`f^ATO9HBT6BkUvpX=tjNeK5Cyy;LCqIz7@Pirftt|pqK z!O(bNt*ZIZ96*KyFLt64OYm$*#$+5>f``J#6xxd;OR!F(+$(%Hf^yR`gdp5;GoOP* zygN`=^QbB~6f;ifvf{mPtNj}Nwl>}w39q2TcZY<1@+u;*8AYpl13 zvoYiB%r?wuwlrOBDDLZcNJDXQC#eZAiI`%*j1HtEz+YcjB1^j_3@JyajHD<)Ixe}_ z^9Dz>Z~yxZz}=q-z}ZlpD!d5>2sw*ToK97U|K8%-SvcaaB5?qI?usd4^i2 ztE7XW9ZJSQ3x3JsW;T97Ki!Z8IHT5XD#UZ)BA1S|V7-mZ1*` zsnf{y@LoBJ-(6=Rz~6XX;_FTT%HJxRUX zXo+!5n@6nH)v;PeX;wptVDx>lq)D9cBm)QoZZEKO`bqSlq2kda8antyA`)Oz~ zUTsoa5E3Ryx!p({w34*d^7~O@UCJb_Bp(iMYUeT|o52bT3h_oYjb=9TFw93$cTC11 zPIig7jDY5lv``g&a3(+Pcupx#gQVorK#^nySIiURvas#{Um-J5nF#%^kvWL4fm=Z= zpv!_dSVPSr=%x(FLN}m7Jqod^?6|P&FTP8VB}vXC5a}QTGv)$NQxyjEJZ|WKppywi zua$AQoQz_nJ<&)yG0(^$)k)6C>O@3L)FrwW3h`fCsyWL@EAzqWBW1Iw7!-zUUyW0)DBks2pPb+o78b zI|WhFjwYb}W>|s0dJM-!hUT;0Tl20qwYy5P&N+44DxTiDg!pz$&7L>0-|O%x32+4o zvYNQS-z0qpuWkcv#67WV=acRFT|&Hydb#q1sMp9Pve^W~6*G_}RIO+c2V#=@OVNTz z0#9>9a1_oLt{_5dRBFjo%P7)i3vU~@1iZ&G@csq6Md$t2S`Y%ph&%*7caP4(`pKaX zAUvllYoWjsN-$YCB9)=-;RoZ=@$OD!skx+o8r5K^ zUIu>j@>uw3%0wENIXVIH3+iJE6WxDM2$I;crcoq585lCcR7`{}T)khn`h5=9Ffk%^g{BH?cjuL=S?iUMm$pJk0VgP|} z1eZ#zRD9RR*_e$6Z|vV$zc{Q1IIgM?VwUS6}4qyqpF#}K8aosWUOBvWee%dMPVWVBso zk#t~NH7Xa9Q;UV6^NJ}~Jb-+5%BR^#uOHb11ga!JpIYk(zjhIc`H}V2-5>bNpMo55tiCG$ak|bD=VD$YjsF z`JlHfyQqVa_Cwl9FL;gK0|0q}2_i__7I3b0l&9KZYYpf?sR@w65-0OJY};mgAs5w|PS~+9R6SS6(eg+RXkBGxWH=W=fnpg;Lf=H2@Et%Kd zXYmz*wVNbma8@4V0@*U020h4f*(9KraNRVZruCoi+ATVp=szG;czl96_(pLd!W zLl%RDn913B#k(cu*Fm^T$?28YOV&m0YP*F=2o7+GnmC^$a2BiNl(xzA0XUJn?%8gN z5a#&gz&SH0a8jdaF(HdLo&5VSO3c7M5$hMaS)pdMwgDjkg za`i^pAX&T{w4*C&PeVL&+H7aijD%PlA5Aqm1k_4XoCEQ&ORVP;{E(_GW1>ekCWiNT zP~bi`CP|0so@h1m^K5<}ih*-Q2ZBcA;WWT~ywj0(X1o52l)_L%t_+a~N}*NH!-VwK z!3(uf&hL0lcQt)Xj2W=ipSf#fmvtcg%mWC@E13hJn)@ICG<{vTT+%0}EgK!OJtya0zJ~zH?^Wc$aof zntB541Qn9R2FnIlzZ;E%sq)Mfm@&^= z$(hqByp`i0s$z2SnD#Oj|G7mK2;P zjfl+Q3}iSOK5xN&0a4-BBE_R7TjZpyYr?+vjCfz?5J84zu>Q<7+vfY^aMBeR2dtU- zP8;v|b&G86=AMg-6tq-0@F)(>dM$|8@6221m+ zi|y8;IJ87A`NM8R+dMvSVt7_sO0zlA4vN4A<;8n1VsJaKm1prpf-+vc7j5-RG?3Tb zUQV@gtz#J+v3UoLvBV-j5^R^|SH`Njov#o*cz{Vu9D1QBYZ8Ua)T$lg|EEPW>GI`4 z_3~vN3-0iK;__u8nf?;&CYtVHv5$qsr0?h5Lo8}6o?!6|i)UG!W^tay1s0!VLH~d7 z85T_z^DNpdIxLo11S~=pS6N(RvCiUWSbUbn&$77A;^$fX5{oaf_;nUvVeuO*zRDss zOXQCGA^trIdU3PiT=ZC_QYlt;;jdUJ<8P|6M}F_F+*{d=r>V+ql}VH{_~p~R_?<-k z@yZ0g@2>2xOv|_3(lg-Na05TU_UCj~)Ir?wP^si74<^Jz{gV72BBAy*ZZpY2rEPQR5HKSTojU-JHoDs(som-!HYCE3yfj9-v#QZKE^ zWXtn4nN8V}3STLiC;KH?x-5%lh029z#g<-FUy_KF(JhJJP{yVlEyq$Bi}_)CrXvIZ z9M!yl|&*WBA1cn$T^nH&h?enm_@@X{P8d9*+?}! zY@X{Ifod|mUK6MxB*c4z4fUSA)z9S9)`_&SIJ%w;o|608V7w!rSaST#$fc9Bpw6k& z7aZlj(-(v$h2TQxcYQ3xe^u7s?3uCL%+Hus%F0^?47!KsD*D#Xl)pyi<0x7;!XAVk zfa!R^)e$bskT2^)*o)AQfL2;slMUeGXD>Y z*T}OHmEjHy_F3t9wa^F5{6)WT$Yy@2uWkL|NF}LU4ow>=>#D(G*}2$qeJsfgZtrMb z6?@>nXEB#f8K$EpO*6mfsI%G3tgDWOEjj@g5WYBwZ-)?u5%vK%WWphnUVUkcS(-Pq z@ZH3fBrQnr=YyXPhSn~VAa9J0kf(W~CPp4zf4pXZgderS)Ndmtph)uF1Kv8iaXm$i%&ft7!($?tPTrWv zA#utY@w+BmCK1XQH^BC3e%3O*e8Q>Bb%UA4iF9faEbgl?%tYgov?wV9Vk%c_TKJv% zT7I~u>Ho0$TXY--if}#6j>7HzY=Xa0H?%s5uhE)Zdlk01En)0(9N`4QNrY1frxCU) zg587fJl4FK4Vd%G&;{7=|5SIc->E+&dj&xm9N%1)CDUnldf`ANWosp6C&~&wy=Y`W zji1BSo3{}m=uU_Fd;^yc14zCIgvN->UvKjBD~->QY5qy$!wHXCP?|&tP1-PSrc78w zFy1N>I|seIv@13Z!i9gyzuR<*JjoYhu}Gh#QQ4Nkv6SZ(w7#C^G1%2>&Gkg%Pc%D? zA8S*Pxndtz#!_Z1leJ>WOw3ryC#_UA!8a^Q>^ zOBkQW=`ikL7uA5M$%GNh#!|wcbIsH7F~fwIx|txR2}e&Ga~4M1ci_p402Fk}M`J@^ zmfJFYDK-{R1$FItMKJbpx%KV91sKil2jK6tHtw5d58(6X5j^G;V5#}5V%d-2>*i(G z2ium&oG?}4svS65R0hI_H!LV#;H%}bHw@+|m87uifXI2a!p}Ti%=0=9&hieR5nFUA4X29^6$03 z$6x5^Tb+*k6FRD2tSsPPZcC-YB)`+y21UbLoeh=6kgr3?4+z0E{%PmiWSqaf zyGve<^Yh(Ryt1nrSOncj@d!$#nGp3Xmx5sQnfp-)pMtU2zRO4i!>8cqlEX66OD-yw z5Y#3ptxutQG$O}3=!_hFz^{zx{Ee;&!jNA_k)LGCkTF%*t|;V80$J0yCa?Hy|BALW z$j`-VH)#8cnT~3FIsR>+9qaDnXS)Z0uU_KI3=~jom|!amue59bgQH-Exq+cUc{zql z9MRYMOY{OIet|tl_^TCR{$cMTar5!}dqRX9;Q#D7y^8+N9z+oJNI%{Q!M3K|yM@5I zk#-$9Jpk9BSE4fEffpdlnJ1PeQ64v*V$Q82&7_?K<>jbb*g;qR!`@vU;l9+T6W;-p z<0^l;zwfdTsU)EgcpC{>3Wsfnw z|Hs~c`!PR4YUF<(I5LCbev_8k@zG8DaOdcl*r5=7%uNC!s+5$wvDcf+0XHWJQ(nNy z8u>GW)h!+h0WmM~xPk=Q`OV=L{-?pA?PY#_=;Ue!=8A{Cm8OtotIRBms|te@;+8bM zAuh{d7mr9mA(GhWTS6x2{)=HAE_kI zts5gIA*1}a`x^#Pz_?OM?5^58GKH7{<&rU#olniavfg>%Bx${YGhas#%jfZKgIHXJ zdj6@=x(3fY?uq7D(lpHP^VdiB@fSt{M-ReKJeA=&bzYoQ=OK1Kr9f=QVwl*)lPG)> zC)Hv&hu9A%VwImh`2MOQj%}_iD8@3>K5%%7!2tr2X?6}MsvE*$hazWOJ)sx7c{ih6 z%yOYH$(y(zNLTXL;4z9USGvBI;;$TP>c9n#!DZF}c+cIKsX$u7+YbNk94tNxeHfl^ zh0H~1umoU-5ImZTV9B1&Q==%$&rud!QSwL0`pS{JgjDd|yT!zrsb%;)jy`1i*fd zPj@ z?xt%hD>(Jm8pZV=Fkt+IOFJa#kQuKg{j=$;nP*gHd4@LN z9yYOJV|WH=w`ix~A)J`QeJ_mGG<68}(+r0-o>+ z1LE5X_%*{Xte3axA-zlw!iyR)Ar@CMGnkAk97nj9-#HtLcm?3UI9nSiltsGoUkMKq AH2?qr diff --git a/contradiction_proof.py b/contradiction_proof.py new file mode 100644 index 0000000..a8e489e --- /dev/null +++ b/contradiction_proof.py @@ -0,0 +1,26 @@ +from enum import unique +from proof import * +from element import * +from group import * +from integer import * +from logicObjects import * + + +G = group('G','*') +inversePropertyOne = Eq( Mult(['a','c']) , Mult([G.identity_identifier]) , G) +inversePropertyTwo = Eq( Mult(['a','d']) , Mult([G.identity_identifier]) , G) +uniqueInverse = Implies( [inversePropertyOne,inversePropertyTwo] , Eq( Mult(['d']), Mult(['c']), G) ) +p = Proof('u', assumption = None, goal=uniqueInverse) +p.introGroup(G) +p.introElement(G,'a') +p.introElement(G,'c') +p.introElement(G,'d') +p.introAssumption(inversePropertyOne) +p.introAssumption(inversePropertyTwo) +p.introSubproof(Not(Eq(Mult(['d']), Mult(['c']), G))) +p.rightSidesEq(4,5) +p.cancelLeft(7, ['a']) +p.switchSidesOfEqual(8) +p.notElim(6,9) +p.concludeSubproof(6) +#p.impliesIntroduction([4,5],11) \ No newline at end of file diff --git a/group.py b/group.py index 0002318..0dc18d8 100644 --- a/group.py +++ b/group.py @@ -54,6 +54,9 @@ def mulElements(self, elem1, elem2): # should this return an equation? def addGroupProperty(self, property, propertyName): self.groupProperties[propertyName] = property + def deleteGroupProperty(self, propertyName): + del self.groupProperties[propertyName] + def addElementProperty(self, property, elementName): if elementName in self.elements or elementName == self.identity_identifier: self.elementProperties[elementName] = property diff --git a/logicObjects.py b/logicObjects.py index e90723f..8ec70d7 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -77,10 +77,16 @@ def __init__(self, arg): def elim(self, contradiction): if self.arg == contradiction: return Bottom() + + def __repr__(self): + return "Not " + str(self.arg) class Bottom: def elim(self, conclusion): return conclusion + + def __repr__(self): + return "⊥" class In: def __init__(self, elem, grp): @@ -188,6 +194,14 @@ def replace(self, replacements): else: print("Replacements is not the same length as the list of existential elements") +## Unique class + +class uniqueElementProperty: + def __init__ (self, prpty, pg): + self.property = prpty + self.group = pg + + ## Special types of elements/groups class identity(element): @@ -202,9 +216,9 @@ def __init__(self, pg): class inverse(element): def __init__(self, elementName, pg): - super().__init__(elementName, pg) - lhs = Mult([arbitrary('x',pg),elementName]) # self or elementName? - rhs = Mult([arbitrary('x',pg)]) - eq = Eq(lhs,rhs,pg) - idnty = forall([arbitrary('x',pg)], pg, eq) - pg.addElementProperty(idnty,elementName) + inverseName = elementName + "^(-1)" + super().__init__(inverseName, pg) + lhs = Mult([inverseName,elementName]) # self or elementName? + rhs = Mult([pg.identity_identifier]) + inverseEq = Eq(lhs,rhs,pg) + pg.addGroupProperty(inverseEq, "Inverse of " + elementName) diff --git a/proof.py b/proof.py index cb128ac..6041010 100644 --- a/proof.py +++ b/proof.py @@ -1,4 +1,5 @@ from re import L + from element import * from group import * from integer import * @@ -13,7 +14,7 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []): self.steps = [] self.justifications = [] self.env = {} - self.depth = 0 + self.subproof = None def qed(self, lineNum): if self.goal == self.steps[lineNum]: @@ -32,8 +33,13 @@ def show(self): print('') print('Proof : ' + self.label) print('--------------------------------') + subProofIndent = "" # might need to change, this is just for now for i in range(len(self.steps)): - print(str(i) + ': ' + str(self.steps[i]) + '\t' + str(self.justifications[i])) + if self.justifications[i] == "Intro Subproof Assumption": + subProofIndent += '\t' + if self.justifications[i] == "Concluded Subproof": + subProofIndent = subProofIndent.replace('\t', '', 1) + print(subProofIndent + str(i) + ': ' + str(self.steps[i]) + '\t' + str(self.justifications[i])) print('') def introAssumption(self, expr): @@ -46,10 +52,6 @@ def introGroup(self, groupName): self.justifications += ["introGroup"] self.show() - def introGroupElement(self, elementName, groupName): - self.steps += [groupElement(elementName, groupName)] - self.justifications += ['introGroupElement'] - default = {"in":[groupName], "prop":[]} def introGroup(self, grp): self.steps += [grp] self.justifications += ["introGroup"] @@ -116,29 +118,24 @@ def substituteLHS(self, lineNum1, lineNum2): else: print("Cannot substitute without an Equation") - def modus(self, lineNum1, lineNum2): + def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think) """ modus pones: given A->B and A, the function concludes B and add it as a new line in the proof :param lineNum1 and lineNum2: one line in the proof where the person showed A->B and one line the proof where the person showed A """ ev1 = self.steps[lineNum1] - ev2 = self.steps[lineNum2] + ev2 = [] + for line in lineNums: + ev2 += self.steps[line] if isinstance(ev1, Implies): A = ev1.assum B = ev1.conc if A == ev2: self.steps += [B] - self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNum2)}'] + self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] self.show() - elif isinstance(ev2, Implies): - A = ev2.assum - B = ev2.conc - if A == ev1: - self.steps += [B] - self.justifications += [f'Modus Ponens on {str(lineNum2)}, {str(lineNum1)}'] - self.show() else: - print (f"Neither of {str(lineNum1)}, {str(lineNum2)} are an implies statement") + print (f"Line {str(lineNum1)} is not an implies statement") def inverseElimRHS(self,lineNum): """ @@ -473,10 +470,10 @@ def introSubproof(self, assum): We will have to make show recursive to make the subproof steps show :param assum: the assumption for the subproof """ - subproof = Proof(label="Subproof", steps=[self.steps], justifications = [self.justifications]) - self.steps += [subproof] - self.justifications += ["intro subproof"] - return subproof + subproof = Proof(label="Subproof", assumption=assum, steps=[self.steps], justifications = [self.justifications]) # how do we deal with this? + self.steps += [assum] + self.justifications += ["Intro Subproof Assumption"] # How can we track subproof throughout parent proof? + self.show() def concludeSubproof(self, lineNum): """ @@ -485,8 +482,13 @@ def concludeSubproof(self, lineNum): Work in progress, we should discuss how to do this. :param lineNum: the conclusion of the subproof to turn into an implies """ - conc = Implies(self.assumption, self.steps[lineNum]) - return conc + evidence = self.steps[lineNum] + if isinstance(evidence, Not): + self.steps += [evidence.arg] + self.justifications += ["Concluded Subproof"] + self.show() + else: + print(f"Cannot conclude subproof") # THIS IS A MESS, NEED TO ACTUALLY CATCH ERRORS def introElement(self,G, name): """ @@ -544,3 +546,73 @@ def closure(self,G,a,b): print(f"{a} is not in {G}") else: print(f"{b} is not in {G}") + + def cancelRight(self, lineNum, mult): + ''' + Cancels element from right side of multiplication if it exists + :param lineNum: the line where the equation resides + :param mult: the list of elements to eliminate + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, Eq): + rhselems = evidence.RHS.products + lhselems = evidence.LHS.products + l = -1*len(mult) + if rhselems[l:] == mult and lhselems[l:] == mult: + self.steps += [Eq( Mult(lhselems[:l]), Mult(rhselems[:l]) , evidence.parentgroup )] + self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] + self.show() + else: + print(f"It seems like the right hand sides on line {lineNum} are equal to {mult}") + else: + print(f"It doesn't seem like line {lineNum} contains an equation") + + def cancelLeft(self, lineNum, mult): + ''' + Cancels element from left side of multiplication if it exists + :param lineNum: the line where the equation resides + :param mult: the list of elements to eliminate + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, Eq): + rhselems = evidence.RHS.products + lhselems = evidence.LHS.products + l = len(mult) + if rhselems[:l] == mult and lhselems[:l] == mult: + self.steps += [Eq( Mult(lhselems[l:]), Mult(rhselems[l:]) , evidence.parentgroup )] + self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] + self.show() + else: + print(f"It seems like the left hand sides on line {lineNum} are equal to {mult}") + else: + print(f"It doesn't seem like line {lineNum} contains an equation") + + def switchSidesOfEqual(self, lineNum): + ''' + Switches an equality like x=y to become y=x + :param lineNum: the line where the equality to be flipped is on + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, Eq): + rhs = evidence.RHS + lhs = evidence.LHS + self.steps += [Eq(rhs , lhs , evidence.parentgroup )] + self.justifications += [f"Switched sides of line {lineNum}"] + self.show() + else: + print(f"Hmm, it doesn't look like line {lineNum} isn't an equality") + + def notElim(self, lineNum1, lineNum2): + ''' + Eliminate a not into a contradiction + :param lineNum1: the line containing the not statement + :param lineNum2: the line which has the real statement + ''' + evidence1 = self.steps[lineNum1] + if isinstance(evidence1, Not): + result = evidence1.elim(self.steps[lineNum2]) + self.steps += [result] + self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] + self.show() + else: + print(f"The statement on line {lineNum1} isn't a Not") \ No newline at end of file