From 43f0ea436c2ba22f51b0cc7189065bc455670fad Mon Sep 17 00:00:00 2001 From: Isaac Date: Tue, 19 Apr 2022 13:07:49 -0700 Subject: [PATCH] consistency changes --- __pycache__/logicObjects.cpython-39.pyc | Bin 9418 -> 9435 bytes __pycache__/proof.cpython-39.pyc | Bin 22276 -> 22742 bytes abelian_proof.py | 4 +- logicObjects.py | 8 +- proof.py | 107 ++++++++++++++---------- 5 files changed, 68 insertions(+), 51 deletions(-) diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index b287f701f9695a9d16d9b7aeba68ee4286dfd3d3..9404317657960878169f048ae3e7203513d13a9c 100644 GIT binary patch delta 768 zcmYjOO=uHg5Z&2LvRhr4w{K_O%$sk&_jCJmdPCO_OY~HJ z-e|t-=&z3)+f`hpGHbfZ;;bnqsgw(dL3)Yv3{wQIe5Z|1g9Zk|&0s%^c6gz+M72$6 zRoaAAX-yU5BsDB+t}8p_?zu{?x&vI?g!^|i@(2IjF4ufqkL&|^{Vdq&}?1S+Tls-g~wqG$Xl zSmw4F-+5A^wFL#=JfFTY%(t{h;qU+z#1hF2e3Chdd+Co*#1~_!WPwVq zX4%%dwQ+Buv2MAFz2dlvSaIlQeI0u^(jtWzVyF>(q44L`ym_xe*SV}S3@}{7+IZ&F zO{N8cns$5Rz9k%s=ZglXo17l>(xtnig}dXE6Bd`W1Ni6MrrdW5-I=v6{MK`7ol2*s;xJ$Uvcir}T-O#XCX-p;;xGw+-I4l|!JT1nH6OZ0sF zb-SExYWpY8BxF}!UMRS7exV?ysg&@F0eXq63^N3-r*Riw_;vIK%l;0FnqlIT;Klqb z)pw*#X$Ll?nn#$F1LeSZ1q!_ye@}I5tefIm#X}(#BoU$^2~XD$KO8ghimv($@PdIE zeNAn9dPpQ@T5t3NfH`~=I!o9LjNnn^68;WV!NR5zd>Qnj6MnAFvzV6=79I7Sn&xzf zVIDslF|b-cj3flwvL&XMJKAI<4vUzJtivo$YDSp*UQsv-fdYz8k(EJ_?ixS!TikZ7 z=e#$(3mH6Tj;eX)`~D_2%o^ldU(EzS7X71#Nfx+rsa_ZV*>h8Xp}p&3f5r-)h+glU z2y)nno+9McUq^Q#)iY1UibJc^@`b|T0Sbs!lIge~`vYlwI~E;D5$&pW-QKddA7o2g zwky{+99I?_4*jT~V~>Z+q!5D)MS^b>y;;TXtn+vfe-^mK5{<#fu!gnq_=R;&+2f{q zZ~LJw9GgAF9i~f64|Hkkz9{4S@#)D5m()J|bFUKjoucQ?-w9nT;pvGRkvVQ?Uuljr Q-nxBUQKd@@;M1& diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index f1cc578409937bde7e5285ce5151b455c9d6180d..325fdf2242c75580b9b8bb5dce2fa89529fcb8e5 100644 GIT binary patch delta 3342 zcmd6pTWl298OP_$UcGmGS+Bv^;|tj9__i@N-~ho;7uUcV@Flg|l&n2td(G~SeRkGh zXI!T>X#!1DluxB3DFjm`m8$}Uky5FONN6e*RjNeVs*(1IHY#eL(x*PSFa5sR#ZHjZ zhgPa;dw)LHZ_fFj@BC-a-e7;c#e6ZZ*CpW3nc&IM-)C<5D%=ok3b{0zO71Olz08`!7|Q-aRQgar#qBbw4&gJ@vO zV!0`m1*LjLw@g_V>`2>!L$~YJQzE~r3s#!xm|!~vQ8stnEXDXlCaI(} zDLtuX60$U^NHHl9Piu`*GB$^`IW;4xsl=Q#8JktGg#GDsCOK^$N)rw`g|RYRku+7B z&S+8`|58|vN$GfMBB5w_b`&ofcIC8nk+@kawLwkclO?;bI^s;kQ%W?GO!H3C^(mMt zY^W^9qF{3|7qc=a3*dh{{!*!yxx^scEUd46hY5lvTxF=bNUATh1yQr0?$#yo0^_gg z;*<^kSypw?zW7 zQzzxcyz&85eiJE=>Ft*bs84p~RF|!o-fm;2xQ0Qvx2+~zn6-|n({ov;tSHk|dOXKE z;O8aJSnF}K;0-1M7qO6THTNE19_E2_!8*|;!q0-O|F_$P`OvQ&J-Frp{uSscYn|l1 zSmB2e;X;0d%0~&0-7fP^g{dP-s37zajuDO%P7wMDBv9_!t>3}{ynxk#cd=&!#f*l{ zJH_e^9-g(2t2~xSrSf_<2tO^aVIRZ&a)W&p&Tbv<*kIy_Tboq4qMX6xP3LFR zs@4}YVmiY1iU50vp-LfIQR8#q5IcSj(lXzL#fmM9{F;uwIc1x&&kFo}u4I~q6%)&$ zTd~EtEH2nIt8QCsDOeV15}q4^HmV5E)GAR_tFJvbWY;Wq6qvO1UeUf z5)tLkQE`+~72kOAiAn8fCZV~|O8<>$#xJVxGrM^^qi~_NmG!~h+9pqfhNOua zF0^vPxbj-u8H`&DHyeFy*tpYZ6WKoaRdbKqOiW5!-UhEn%6%&~Gc!58(D-iXYN=<_ z##GDSnSCF%oQCHj&ERQq+1sev0aqd+cE()tZz3M{g7I<0DY71T&^8k=M|{Q{A+}@d zXP!3&{$QDh4^kXcgE_ddqm5mF_d42)lJ<7izkpp~|KoORuJ|##{U!x5#Wwxbe5ko8 zQ~PyeTZCKX#qPL_-xbV^xoy1Hah=)C@g1PIr2$ffhNd{K2@rOJ;tG zl(lrF@O8rnQ`~P%VIbea_w>E&ez{XW)7I*3XjOQ$=gL~<9jz=2=MyA$!`Ib-zrhYZ!+-rvc-1hM`) zb_ve)XUi|sGqxb+{dlYhPxIYli9XNOgo$PH04$d#` zp~-s*hX_N2X9!;-e4Q{(m>{SGPRI~u3C|OB!V83N5xz}$iSRPv9N|3SdxX~r-zU5w tgphAi@rQ&fgtrLGaDS*2_6^l}gHFj=<@7rP&SGaV@S#0ucsGXz{{?!OAfNl56a;&8w5RJBP$1>6O50Spe;_mj2sEt{o!WtfrXYq5<&f{D4g}B+94QH|2Jy7&L z!x^*B14s$ySEHEYfD}@!+wL}~uG$$*B$9@jnjK0Rabwod)Dv-IEIDha(S+JDGaEJH z$prR$UH}*V(^L1&<>PJl4ZPs%Z|DwX>#U_7WHc}$j3!1S!_CNJ3MUe?c=wsG5> zLbT6inTlzjkoC)^WM?T^IKHu|IG;RXGZYi%;W;U0zhYxQEqQ0_nr86ar8<6@+pxBU z^cZwb#uHli>{LqM#QL^jN8Y;P01YLF3+&(oKe#}lH;*dGg7bMbm6t%04Cy5xZDqD% z0Z2R9AUh1ly!` zoiRq zyMy{}VtRd-HiE|rY6e1U^gT48?`4P-6zP^Rj^{#*eT-7ZgN!c5LyT@l4@0EoN|yGD z1g$If`LEOJYR6cQ6}QOct1jj{7nPBu9-W-bh>PHFOKOxp7GKWta$K3!j>-7cEi5gy z;2^$VI-q0(VSP~bi?Uf!qo0md!0%~qAwD0h@G2yWKRfA@`T<@qFFq9mO8N%F5tB`s zQrxzb;*<-N7nJx^99awUoSo8;%4liExggVg_PmXXi_1ke9ZT6Hi)UBNVYsh<32d;Tm2WzEY z2>)-O^O=4jQnZR6g)>Tc#O>pnqI>CU(XLHuQ+hrRWo-uA%hz>&LJuhxBPo9HQd!!G z0s0O=+S{uqlOy3tZNzwJcG4KO@wTPcT|T|^O?*loHQ_Fw+Qz9Szuu=JLdq4}|MYEE z8gAlL#mnT?vdUoVlAl#I<6eD$)b38_?~jj;8R`@n6Q7}q^b|n4*jS| z;1?@h#b46nJ^iABb))h&D556z;S1Gu@F3o*-T*%9i|Sh0KTHP)o$TnYc*@X+a8szt zJ4%y_py?`o>&L|*|9F_kFz;d+KW-YCTqe2b9e`GmVKz*e|+@$VYLa34ay|z>JXlyGRbq zSbvTR(tPaaDUe!M6&}*YIdX>;JeE-;M(fIHO*6H?6@SoyqzsnHK zcn&|@yc7Ol-M8gk_^QqQX=|mjjdys&P3kr;{LR|9ZG#M3@z{=VreAKy3p*<1&%k(;I(<)!AZzZ|(@4a;}VU_kh1A)&A4vuMR z%7_|5Q8k&!R5<=}f3=I&spLOI(<$*z1QHbBkk1R&Kx=P EZ^xOP4FCWD diff --git a/abelian_proof.py b/abelian_proof.py index a636ef6..38b8615 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -14,12 +14,12 @@ p.closure(G,'a','b') p.accessAssumption() p.forallElim(4,['a * b']) -p.leftMult(G.elements['a'],5) # G.elements should be a function not a dictionary +p.leftMult('a',5) # G.elements should be a function not a dictionary p.forallElim(4,['a']) p.substituteRHS(6,7) p.identleft(8) p.identright(9) -p.rightMult(G.elements['b'],10) +p.rightMult('b',10) p.forallElim(4,['b']) p.substituteRHS(11,12) p.identleft(13) diff --git a/logicObjects.py b/logicObjects.py index d9e8249..65cfce8 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -123,9 +123,9 @@ def __repr__(self): return str(self.LHS) + ' = ' + str(self.RHS) def __eq__(self,other): - if self.LHS == other.LHS and self.RHS == other.RHS: + if self.LHS == other.LHS and self.RHS == other.RHS and self.group == other.group: return True - elif self.LHS == other.RHS and self.RHS == other.LHS: # a=b is the same as b=a + elif self.LHS == other.RHS and self.RHS == other.LHS and self.group == other.group: # a=b is the same as b=a return True else: return False @@ -211,7 +211,7 @@ def replace(self, replacements): else: print("Replacements is not the same length as the list of existential elements") -## Unique class +## Unique class - idk if we need this class uniqueElementProperty: def __init__ (self, prpty, pg): @@ -239,3 +239,5 @@ def __init__(self, elementName, pg): rhs = Mult([pg.identity_identifier]) inverseEq = Eq(lhs,rhs,pg) pg.addGroupProperty(inverseEq, "Inverse of " + elementName) + +## TO DO: class generator(element): diff --git a/proof.py b/proof.py index e7e39eb..42dfb3f 100644 --- a/proof.py +++ b/proof.py @@ -102,9 +102,9 @@ def substituteRHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.LHS} with {ev2.RHS} on line {lineNum1}'] self.show() else: - print("Cannot substitute without an Equation") + print(f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - print("Cannot substitute without an Equation") + print(f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def substituteLHS(self, lineNum1, lineNum2): """ @@ -121,9 +121,9 @@ def substituteLHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}'] self.show() else: - print("Cannot substitute without an Equation") + print(f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - print("Cannot substitute without an Equation") + print(f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think) """ @@ -131,27 +131,30 @@ def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may :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 = [] - 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(lineNums)}'] - self.show() + if isinstance(lineNums, list): + 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(lineNums)}'] + self.show() + else: + print (f"Line {str(lineNum1)} is not an implies statement") else: - print (f"Line {str(lineNum1)} is not an implies statement") + print("The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") def inverseElimRHS(self,lineNum): """ finds the first pair of group element and its inverse and returns the group element :param lineNum: the line of the proof to be modified on the right hand side """ - evidence = copy.deepcopy(self.steps[lineNum]).RHS - if isinstance(evidence,Mult): - l = evidence.products.copy() + evidence = copy.deepcopy(self.steps[lineNum]) + if isinstance(evidence,Eq): + l = evidence.RHS.products.copy() lawApplied = False for i in range(len(l)-1): if isinstance(l[i],element) and isinstance(l[i+1],inverse) and (l[i].elementName == l[i+1].elementName): @@ -169,18 +172,21 @@ def inverseElimRHS(self,lineNum): if lawApplied==False: print (f"Inverse laws can't be applied on line {lineNum}") return - self.steps += [newProducts] - self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] - self.show() + self.steps += [newProducts] + self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] + self.show() + else: + print(f"It doesn't seem like line {lineNum} contains an equation") + def inverseElimLHS(self,lineNum): """ finds the first pair of group element and its inverse and returns the group element :param lineNum: the line of the proof to be modified on the left hand side """ - evidence = copy.deepcopy(self.steps[lineNum]).LHS - if isinstance(evidence,Mult): - l = evidence.products.copy() + evidence = copy.deepcopy(self.steps[lineNum]) + if isinstance(evidence,Eq): + l = evidence.LHS.products.copy() lawApplied = False for i in range(len(l)-1): if isinstance(l[i],element) and isinstance(l[i+1],inverse) and (l[i].elementName == l[i+1].elementName): @@ -198,9 +204,11 @@ def inverseElimLHS(self,lineNum): if lawApplied==False: print (f"Inverse laws can't be applied on line {lineNum}") return - self.steps += [newProducts] - self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] - self.show() + self.steps += [newProducts] + self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] + self.show() + else: + print(f"It doesn't seem like line {lineNum} contains an equation") ## For all and there exists elimination @@ -235,38 +243,45 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once! self.show() ## Multiplication manipulation - def leftMult (self, elem, lineNum): + def leftMult(self, elemName, lineNum): """ Left Multiply both sides of an equation with the input element :param lineNum: the equation in the proof that is to be modified - :param elem: the element to left Multiply with + :param elemName: the name of the element to left Multiply with """ eq = copy.deepcopy(self.steps[lineNum]) - if isinstance(eq, Eq) == False: + if isinstance(eq, Eq): + if elemName in eq.group.elements: + elem = eq.group.elements[elemName] + product = self.MultElem(elem, eq.LHS) + result = Eq(product, self.MultElem(elem,eq.RHS), eq.group) + self.steps += [result] + self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] + self.show() + else: + print("The element " + elemName + " is not in the group " + eq.group) + else: print (f"Line {lineNum} is not an equation") - return - product = self.MultElem(elem, eq.LHS) - result = Eq(product, self.MultElem(elem,eq.RHS), eq.group) - self.steps += [result] - self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] - self.show() - def rightMult (self, elem, lineNum): + def rightMult (self, elemName, lineNum): """ Right Multiply both sides of an equation with the input element :param lineNum: the line in the proof that is to be modified - :param elem: the element to right Multiply + :param elemName: the name of the element to right Multiply with """ eq = copy.deepcopy(self.steps[lineNum]) - if isinstance(eq, Eq) == False: + if isinstance(eq, Eq): + if elemName in eq.group.elements: + elem = eq.group.elements[elemName] + product = self.MultElem(eq.LHS, elem) + result = Eq(product, self.MultElem(eq.RHS, elem), eq.group) + self.steps += [result] + self.justifications += ['Right multiply line {lineNum} by ' +str(elem) ] + self.show() + else: + print("The element " + elemName + " is not in the group " + eq.group) + else: print (f"Line {lineNum} is not an equation") - return - product = self.MultElem(eq.LHS, elem) - result = Eq(product, self.MultElem(eq.RHS,elem), eq.group) - self.steps += [result] - self.justifications += [f'Right multiply line {lineNum} by ' +str(elem)] - self.show() - ##power methods def breakPower(self,input): """