From 1a157eca6c2b81a1042204a47c59198a4c912a3b Mon Sep 17 00:00:00 2001 From: Alina Hu Date: Sun, 10 Apr 2022 15:44:23 -0700 Subject: [PATCH 1/3] adding in intro group --- abelian_proof.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/abelian_proof.py b/abelian_proof.py index f5f43c4..842657a 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -6,4 +6,7 @@ from logicObjects import * 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']), identity('1','G'),"G")), goal=abelianG) \ No newline at end of file +p = Proof('Simple Abelian Proof', forall(['x'], 'G', Eq(Mult(['x', 'x']), identity('1','G'),"G")), goal=abelianG) +p.introGroup('G') +p.introGroupElement('a', 'G') +p.introGroupElement('b', 'G') \ No newline at end of file From e7785dbb8884966cd1298bd624eaaf496668d47f Mon Sep 17 00:00:00 2001 From: Morris Kyn Date: Tue, 12 Apr 2022 13:52:47 -0700 Subject: [PATCH 2/3] Returns after every error message(so function doesn't continue) --- proof.py | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/proof.py b/proof.py index 759b737..228b562 100644 --- a/proof.py +++ b/proof.py @@ -16,7 +16,6 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []): self.depth = 0 def qed(self, lineNum): - print(self.goal, self.steps[lineNum]) if self.goal == self.steps[lineNum]: self.steps+=["□"] self.justifications += ["QED"] @@ -156,6 +155,7 @@ def inverseElimRHS(self,lineNum): break 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() @@ -184,6 +184,7 @@ def inverseElimLHS(self,lineNum): break 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() @@ -230,6 +231,7 @@ def leftMult (self, elem, lineNum): eq = copy.deepcopy(self.steps[lineNum]) if isinstance(eq, Eq) == False: print (f"Line {lineNum} is not an equation") + return product = self.MultElem(elem, eq.LHS) result = Eq(product, self.MultElem(elem,eq.RHS), eq.parentgroup) self.steps += [result] @@ -245,6 +247,7 @@ def rightMult (self, elem, lineNum): eq = copy.deepcopy(self.steps[lineNum]) if isinstance(eq, Eq) == False: print (f"Line {lineNum} is not an equation") + return product = self.MultElem(eq.LHS, elem) result = Eq(product, self.MultElem(eq.RHS,elem), eq.parentgroup) self.steps += [result] @@ -276,6 +279,7 @@ def combinePower(self, mult): for i in multList: if i != e: print ("Need a single element but given multiple") + return result=power(e,len(multList)) self.steps += [result] self.justifications += ['Convert multiplications to equivalent powers'] @@ -290,7 +294,8 @@ def splitPowerAddition(self,power): exp=self.exponent l=exp.split("+") if len(l)==1: - print ("No power addition to be split apart") + print ("No power addition to be split apart") + return multList=[] for i in l: elem=power(element,i) @@ -309,7 +314,8 @@ def splitPowerMult(self,power): exp=self.exponent l=exp.split("*") if len(l)==1: - print ("No power multiplication to be split apart") + print ("No power multiplication to be split apart") + return elem=element for i in l: e=power(elem,i) @@ -333,6 +339,7 @@ def rightSidesEq(self, lineNum1, lineNum2): self.show() else: print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") + return def leftSidesEq(self, lineNum1, lineNum2): """ @@ -348,6 +355,7 @@ def leftSidesEq(self, lineNum1, lineNum2): self.show() else: print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") + return def identleft(self, lineNum): """ @@ -372,6 +380,7 @@ def identleft(self, lineNum): # else we can't apply identity elimination if l1==[]: print ("identity can't be applied") + return newProduct = Mult(l1) ret = Eq(newProduct,evidence.RHS,evidence.parentgroup) @@ -402,6 +411,7 @@ def identright(self, lineNum): # else we can't apply identity elimination if l1==[]: print ("identity can't be applied") + return newProduct = Mult(l1) ret = Eq(evidence.LHS,newProduct,evidence.parentgroup) @@ -499,8 +509,10 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): l = elemIntroLines[i] if self.steps[l].elem!=vars[i]: print("Line", l, "does not introduce variable", v) + return if self.steps[l].grp!=G: print("Element", v, "is not in group", G) + return #If you make it here, this is a valid for all intro self.steps+=[forall(vars,G,self.steps[equationLine])] self.justifications+=["For all introduction"] From 23a74ab77c63b6d49abd9c44aabf9641ef503c54 Mon Sep 17 00:00:00 2001 From: Alina Hu Date: Fri, 15 Apr 2022 21:05:09 -0700 Subject: [PATCH 3/3] update --- proof.py | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/proof.py b/proof.py index 8913503..3ea3e5e 100644 --- a/proof.py +++ b/proof.py @@ -36,6 +36,17 @@ def introAssumption(self, expr): self.steps += [expr] self.justifications += ['introAssumption'] self.show() + + def introGroup(self, groupName): + self.steps += [group(groupName)] + self.justifications += ["introGroup"] + self.show() + + def introGroupElement(self, elementName, groupName): + self.steps += [groupElement(elementName, groupName)] + self.justifications += ['introGroupElement'] + default = {"in":[groupName], "prop":[]} + self.show() def MultElem(self, element1, element2): l=[]