From e5e2db246f679f4b42af257ec31cc450d82d3a1a Mon Sep 17 00:00:00 2001 From: Morris Kyn Date: Tue, 12 Apr 2022 13:26:01 -0700 Subject: [PATCH] Testing interactive proofs, more feedback, better comments --- __pycache__/group.cpython-38.pyc | Bin 2443 -> 2567 bytes __pycache__/proof.cpython-38.pyc | Bin 16353 -> 17579 bytes abelian_proof.py | 3 -- group.py | 5 ++- proof.py | 62 +++++++++++++++++++++++++------ 5 files changed, 54 insertions(+), 16 deletions(-) diff --git a/__pycache__/group.cpython-38.pyc b/__pycache__/group.cpython-38.pyc index f1d2c5805480c67d1c21bcade6bb52d74fbc8a85..6fb0dd6ab47dc3d6d3492e9bb172341bc4fe7c48 100644 GIT binary patch delta 239 zcmeAcZWrMV<>lpK0D{PSp-DR@^6p{Gn|MlvQEcLSM_!Q>(H4d%!4&3T22JtJri>Su z8CPy*W0hoP(*$ZLQkksE;cuAC1kw!!AT|g)1936P*c!$fhAf6`wqS-LZXj2av50T7 z0*8bqM{<5%Nn&PRu{}s7*a*fdzVxE}(gHo0lqRE}rqJX{4iiS5$?G_jL{))Gi!?xl rHi*y#5qgs!a40It0ht_3ER1l-#Kp>NBC%p7c!6*;p2y}l~~ delta 106 zcmZn{=@#Y<<>lpK00OnMp-CwddG|1;O+2N-C^GTABP(+-gQnk diff --git a/__pycache__/proof.cpython-38.pyc b/__pycache__/proof.cpython-38.pyc index aca1409174df7a03e77fe9d601a16ba89956017c..951a1bceefdd198dac14feb0b38ffd7ed1f8ebed 100644 GIT binary patch delta 1622 zcma)+OK2oT7=WvKW-`6gc`QqadT=S%%MQ32Om-)kjfoH?M3%)@blHp6%v3TRdb(z- zsuMc2+ba=dMNlYY4^c^uz7C$eif74DTt!e2ym;}tAXI7!fv$5t9@qP5ezGr*XSMibvnM_@w8DM49U$S5n`YUDJ0je&l_Q5t8HJwWi}s zw;G?0uH3uS+9*7CsbuZ!GWb?L51$J7mfxiTk%}rdU?vE@NqEQz=#ul`h?_+aUlIyF zL9Y5#HHkjoioI{Zah7gPf7yy=ezuNZUw_f=^|^%)%k-&~(IAf^+YTWPvdKjjn2b6@ z!TF~CY$5i(1LH1aRo535U!J*Z4c=$`)?%dhW~ZO-@~|6363k^mGE!QD%Bo0&P+m@` zc@Ktx&!qly@rrj0UaGm5)%JY)rr9R=5GBqL7H1VsoCDOu2|hrdRQ54O;j)oBAWhJA zC2^Kef~sh{s%nXo;C*Kcw~&M0sAi{Qz4Ci3L5KAtgi){Z3TjsOj%_mQWzS8CLy}U_ z@s*$=CM?KXVmiKNwO5T!hmlCK9-)%39lyuIF3T!NVWmM}F@oCKn*{}HdGWUdkA^u6 znH%V^ZQ#l{rT-?q=4x!QDpa!qFx^+PG9 zOl|e=?U$y0w7}LIc-qm=Uj8eso4UC4Q6sT7SB){n06hQ%GTRh<0A(r(CcD1slTpof zsPJhgVA9&KW0xa;#Sb4Cf6`m&A>Yb@P@PHXviH^&ql*QZ%5;d zIjbC`sCVM9;QeD8{z=|Dz%aD4K-~=P8tKHO8*mv3X7BtLyYvZj+f)dsy${-y(6+Tm z9}tqxNY=5k>-E*#Q9-_{ng4ty1BACG3idYo;&U~ M+$ncP$1DAR0Z)3)lK=n! delta 461 zcmYL^&r1S96vyYyZtL2(VTT|H!t&&$i|J-1iCZ0lq#qa|K@dqMrlGsHDGe#=CcHzp zSdY;u>e?ZQF8zQAJVYHL`UARji`vns8Tc}f?|bw4zLNuZEq5d}t(`b0@swP7m^tmZ z4}y&^K^xBocR;~V=n&%A2n{eZllJ8cX34jn$La79I|f2Z9x*E6XSf17R&*V^hBn!` zaGIY=SR1mShCPuQzD73Lg>Y0cBjeKW99VcYY~lWh!LEfPx17evpfBz`IoO2LI&hK& zPDcqRGRaa?;*wbmIlK@TNY_y*S6x@x@vb#S3;Cu9=+2Kmy*VrO1#ImrBm$4vw z6iwZN1^6ACDo_5gxKyXm;(+N;nk;FJR-sDQKqr(eJ87I0@+$n+GADLhod8*FrAfJr zT%lwY(*Y&LHmux4F1?Y?o28;yySOF9FT^dx>qtPAi%b;TcoXmIeEZ+P1HIq{Y%^|I aMKn}}?BTPK(lnK+Zs)pGMfIXFp7{ZczHd7K diff --git a/abelian_proof.py b/abelian_proof.py index 341e2bb..f5be741 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -8,9 +8,6 @@ abelianG = forall(['x', 'y'], G, Eq(Mult(['x', 'y']), Mult(['y','x']),G)) p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), G.elements['e'],G)), goal=abelianG) p.introGroup(G) -#G.newElement('a') -#G.newElement('b') -#G.mulElements('a','b') p.introElement(G,'a') p.introElement(G,'b') p.closure(G,'a','b') diff --git a/group.py b/group.py index 33a6160..0002318 100644 --- a/group.py +++ b/group.py @@ -58,4 +58,7 @@ def addElementProperty(self, property, elementName): if elementName in self.elements or elementName == self.identity_identifier: self.elementProperties[elementName] = property else: - print("That element doesn't exist!", property, elementName) \ No newline at end of file + print("That element doesn't exist!", property, elementName) + + def contains(self, elementName): + return elementName in self.elements \ No newline at end of file diff --git a/proof.py b/proof.py index 5238355..759b737 100644 --- a/proof.py +++ b/proof.py @@ -414,6 +414,7 @@ def introReflexive(self,eq): Introduce a reflexive equality (like x=x) Necessary to show something equals something else when not given a starting equation + :param eq: The equality you want to introduce """ if eq.LHS == eq.RHS: self.steps+=[eq] @@ -423,7 +424,9 @@ def introReflexive(self,eq): print ("this is not reflexive") def reduceLogic(self, lineNum): - """Recursively reduces a ND statement by pushing the nots in + """ + Recursively reduces a ND statement by pushing in the nots + :param lineNum: the line of the proof to be modified """ evidence = self.steps[lineNum] if type(lineNum) in [And, Or, Implies, Not]: @@ -434,7 +437,9 @@ def reduceLogic(self, lineNum): print ("this is not a logic statement") def introCases(self, case): - """Introduction of cases (law of excluded middle) + """ + Introduction of cases (law of excluded middle) + :param case: the equation/logical statement of one case (the other is a not of that) """ case1 = case case2 = reduce(Not(case)) @@ -443,8 +448,11 @@ def introCases(self, case): self.show() def introSubproof(self, assum): - """This one returns so the user has access to the new subproof + """ + WIP + This one returns so the user has access to the new subproof 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] @@ -452,19 +460,37 @@ def introSubproof(self, assum): return subproof def concludeSubproof(self, lineNum): - """You conclude a subproof from the parent subproof + """ + WIP + You conclude a subproof from the parent subproof 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 def introElement(self,G, name): - self.env[name] = G.newElement(name) - self.steps += [In(name, G)] - self.justifications += ["Introducing an arbitrary element"] - self.show() + """ + Introduces an arbitrary element in G + Can be used as evidence for a forall introduction + :param G: the group the elemen is in + :param name: the name of the new element + """ + if G.contains(name): + print(f"{name} is already in {G}") + else: + self.env[name] = G.newElement(name) + self.steps += [In(name, G)] + self.justifications += ["Introducing an arbitrary element"] + self.show() def forAllIntroduction(self, equationLine, vars, elemIntroLines): + ''' + Creates a for all from an equation with arbitrary variables + :param equationLine: the equation + :param vars: the names of the arbitrary variables + :param elemIntroLines: the lines of the introductions of the variables (to show they are arbitrary) + ''' evidence = copy.deepcopy(self.steps[equationLine]) G = self.steps[elemIntroLines[0]].grp #Checking that the lines introduce the arbitrary variables, and that the variables are all in the same group @@ -481,7 +507,19 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): self.show() def closure(self,G,a,b): - G.mulElements(a,b) - self.steps+=[In(G,Mult([a,b]))] - self.justifications+=["Closure"] - self.show() + ''' + Introduces ab as an element of G by closure + :param G: the group a,b are in + :param a: element a + :param b: element b + ''' + if G.contains(a) and G.contains(b): + G.mulElements(a,b) + self.steps+=[In(G,Mult([a,b]))] + self.justifications+=["Closure"] + self.show() + else: + if not G.contains(a): + print(f"{a} is not in {G}") + else: + print(f"{b} is not in {G}")