Skip to content

Commit

Permalink
Returns after every error message(so function doesn't continue)
Browse files Browse the repository at this point in the history
  • Loading branch information
mokyn committed Apr 12, 2022
1 parent e5e2db2 commit e7785db
Showing 1 changed file with 15 additions and 3 deletions.
18 changes: 15 additions & 3 deletions proof.py
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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]
Expand All @@ -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]
Expand Down Expand Up @@ -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']
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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):
"""
Expand All @@ -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):
"""
Expand All @@ -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)

Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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"]
Expand Down

0 comments on commit e7785db

Please sign in to comment.