diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index 7285b63..b287f70 100644 Binary files a/__pycache__/logicObjects.cpython-39.pyc and b/__pycache__/logicObjects.cpython-39.pyc differ diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index c898826..f1cc578 100644 Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ diff --git a/logicObjects.py b/logicObjects.py index f0449be..d9e8249 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -108,16 +108,16 @@ def __repr__(self): class In: def __init__(self, elem, grp): self.elem = elem - self.grp = grp + self.group = grp def __repr__(self): - return str(self.elem) + " ∈ " + str(self.grp) + return str(self.elem) + " ∈ " + str(self.group) class Eq: def __init__(self,LHS,RHS,pg): self.LHS = LHS self.RHS = RHS - self.parentgroup = pg + self.group = pg def __repr__(self): return str(self.LHS) + ' = ' + str(self.RHS) @@ -131,7 +131,7 @@ def __eq__(self,other): return False def replace(self, var, expr): - return Eq(self.LHS.replace(var,expr), self.RHS.replace(var,expr), self.parentgroup) + return Eq(self.LHS.replace(var,expr), self.RHS.replace(var,expr), self.group) def reduce(exp): if isinstance(exp, Eq): diff --git a/proof.py b/proof.py index 4fc1927..e7e39eb 100644 --- a/proof.py +++ b/proof.py @@ -246,7 +246,7 @@ def leftMult (self, elem, lineNum): 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) + result = Eq(product, self.MultElem(elem,eq.RHS), eq.group) self.steps += [result] self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] self.show() @@ -262,7 +262,7 @@ def rightMult (self, elem, lineNum): 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) + 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() @@ -358,8 +358,8 @@ def rightSidesEq(self, lineNum1, lineNum2): """ l1 = self.steps[lineNum1] l2 = self.steps[lineNum2] - if l1.RHS == l2.RHS and l1.parentgroup == l2.parentgroup: - self.steps += [Eq(l1.LHS,l2.LHS, l1.parentgroup)] + if l1.RHS == l2.RHS and l1.group == l2.group: + self.steps += [Eq(l1.LHS,l2.LHS, l1.group)] self.justifications += [f"Equations with same right side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: @@ -374,8 +374,8 @@ def leftSidesEq(self, lineNum1, lineNum2): """ l1 = self.steps[lineNum1] l2 = self.steps[lineNum2] - if l1.LHS == l2.LHS and l1.parentgroup == l2.parentgroup: - self.steps += [Eq(l1.RHS,l2.RHS, l1.parentgroup)] + if l1.LHS == l2.LHS and l1.group == l2.group: + self.steps += [Eq(l1.RHS,l2.RHS, l1.group)] self.justifications += [f"Equations with same left side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: @@ -407,7 +407,7 @@ def identleft(self, lineNum): print ("identity can't be applied") return newProduct = Mult(l1) - ret = Eq(newProduct,evidence.RHS,evidence.parentgroup) + ret = Eq(newProduct,evidence.RHS,evidence.group) else: print(f"Expected an equation on line {lineNum} but received {type(evidence)}") return @@ -441,7 +441,7 @@ def identright(self, lineNum): print ("identity can't be applied") return newProduct = Mult(l1) - ret = Eq(evidence.LHS,newProduct,evidence.parentgroup) + ret = Eq(evidence.LHS,newProduct,evidence.group) else: print(f"Expected an equation on line {lineNum} but received {type(evidence)}") return @@ -541,8 +541,8 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): :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 + evidence = copy.deepcopy(self.steps[equationLine]) # Mo, do you need this? + G = self.steps[elemIntroLines[0]].group #Checking that the lines introduce the arbitrary variables, and that the variables are all in the same group for i in range(len(vars)): v = vars[i] @@ -550,11 +550,11 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): if self.steps[l].elem!=vars[i]: print("Line", l, "does not introduce variable", v) return - if self.steps[l].grp!=G: + if self.steps[l].group!=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.steps+=[forall(vars,G,evidence)] self.justifications+=["For all introduction"] self.show() @@ -588,11 +588,11 @@ def cancelRight(self, lineNum, mult): 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.steps += [Eq( Mult(lhselems[:l]), Mult(rhselems[:l]) , evidence.group )] 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}") + print(f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") else: print(f"It doesn't seem like line {lineNum} contains an equation") @@ -608,11 +608,11 @@ def cancelLeft(self, lineNum, mult): 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.steps += [Eq( Mult(lhselems[l:]), Mult(rhselems[l:]) , evidence.group )] 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}") + print(f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") else: print(f"It doesn't seem like line {lineNum} contains an equation") @@ -625,7 +625,7 @@ def switchSidesOfEqual(self, lineNum): if isinstance(evidence, Eq): rhs = evidence.RHS lhs = evidence.LHS - self.steps += [Eq(rhs , lhs , evidence.parentgroup )] + self.steps += [Eq(rhs , lhs , evidence.group )] self.justifications += [f"Switched sides of line {lineNum}"] self.show() else: @@ -644,7 +644,7 @@ def notElim(self, lineNum1, lineNum2): self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] self.show() else: - print(f"The statement on line {lineNum1} isn't a Not") + print(f"The statement on line {lineNum1} isn't a Not statement") def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it ''' @@ -676,5 +676,5 @@ def andElim(self, lineNum, n): else: print("You must choose argument 1 or 2") else: - print("The provided line is not an and statement") + print(f"The statement on line {lineNum} isn't an And statement") \ No newline at end of file