diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc index c908826..bc3dd3f 100644 Binary files a/__pycache__/group.cpython-39.pyc and b/__pycache__/group.cpython-39.pyc differ diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index 08f9c57..228e8e8 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 f56f9fb..0e857c7 100644 Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ diff --git a/contradiction_proof.py b/contradiction_proof.py new file mode 100644 index 0000000..a8e489e --- /dev/null +++ b/contradiction_proof.py @@ -0,0 +1,26 @@ +from enum import unique +from proof import * +from element import * +from group import * +from integer import * +from logicObjects import * + + +G = group('G','*') +inversePropertyOne = Eq( Mult(['a','c']) , Mult([G.identity_identifier]) , G) +inversePropertyTwo = Eq( Mult(['a','d']) , Mult([G.identity_identifier]) , G) +uniqueInverse = Implies( [inversePropertyOne,inversePropertyTwo] , Eq( Mult(['d']), Mult(['c']), G) ) +p = Proof('u', assumption = None, goal=uniqueInverse) +p.introGroup(G) +p.introElement(G,'a') +p.introElement(G,'c') +p.introElement(G,'d') +p.introAssumption(inversePropertyOne) +p.introAssumption(inversePropertyTwo) +p.introSubproof(Not(Eq(Mult(['d']), Mult(['c']), G))) +p.rightSidesEq(4,5) +p.cancelLeft(7, ['a']) +p.switchSidesOfEqual(8) +p.notElim(6,9) +p.concludeSubproof(6) +#p.impliesIntroduction([4,5],11) \ No newline at end of file diff --git a/group.py b/group.py index 0002318..0dc18d8 100644 --- a/group.py +++ b/group.py @@ -54,6 +54,9 @@ def mulElements(self, elem1, elem2): # should this return an equation? def addGroupProperty(self, property, propertyName): self.groupProperties[propertyName] = property + def deleteGroupProperty(self, propertyName): + del self.groupProperties[propertyName] + def addElementProperty(self, property, elementName): if elementName in self.elements or elementName == self.identity_identifier: self.elementProperties[elementName] = property diff --git a/logicObjects.py b/logicObjects.py index e90723f..8ec70d7 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -77,10 +77,16 @@ def __init__(self, arg): def elim(self, contradiction): if self.arg == contradiction: return Bottom() + + def __repr__(self): + return "Not " + str(self.arg) class Bottom: def elim(self, conclusion): return conclusion + + def __repr__(self): + return "⊥" class In: def __init__(self, elem, grp): @@ -188,6 +194,14 @@ def replace(self, replacements): else: print("Replacements is not the same length as the list of existential elements") +## Unique class + +class uniqueElementProperty: + def __init__ (self, prpty, pg): + self.property = prpty + self.group = pg + + ## Special types of elements/groups class identity(element): @@ -202,9 +216,9 @@ def __init__(self, pg): class inverse(element): def __init__(self, elementName, pg): - super().__init__(elementName, pg) - lhs = Mult([arbitrary('x',pg),elementName]) # self or elementName? - rhs = Mult([arbitrary('x',pg)]) - eq = Eq(lhs,rhs,pg) - idnty = forall([arbitrary('x',pg)], pg, eq) - pg.addElementProperty(idnty,elementName) + inverseName = elementName + "^(-1)" + super().__init__(inverseName, pg) + lhs = Mult([inverseName,elementName]) # self or elementName? + rhs = Mult([pg.identity_identifier]) + inverseEq = Eq(lhs,rhs,pg) + pg.addGroupProperty(inverseEq, "Inverse of " + elementName) diff --git a/proof.py b/proof.py index cb128ac..6041010 100644 --- a/proof.py +++ b/proof.py @@ -1,4 +1,5 @@ from re import L + from element import * from group import * from integer import * @@ -13,7 +14,7 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []): self.steps = [] self.justifications = [] self.env = {} - self.depth = 0 + self.subproof = None def qed(self, lineNum): if self.goal == self.steps[lineNum]: @@ -32,8 +33,13 @@ def show(self): print('') print('Proof : ' + self.label) print('--------------------------------') + subProofIndent = "" # might need to change, this is just for now for i in range(len(self.steps)): - print(str(i) + ': ' + str(self.steps[i]) + '\t' + str(self.justifications[i])) + if self.justifications[i] == "Intro Subproof Assumption": + subProofIndent += '\t' + if self.justifications[i] == "Concluded Subproof": + subProofIndent = subProofIndent.replace('\t', '', 1) + print(subProofIndent + str(i) + ': ' + str(self.steps[i]) + '\t' + str(self.justifications[i])) print('') def introAssumption(self, expr): @@ -46,10 +52,6 @@ def introGroup(self, groupName): self.justifications += ["introGroup"] self.show() - def introGroupElement(self, elementName, groupName): - self.steps += [groupElement(elementName, groupName)] - self.justifications += ['introGroupElement'] - default = {"in":[groupName], "prop":[]} def introGroup(self, grp): self.steps += [grp] self.justifications += ["introGroup"] @@ -116,29 +118,24 @@ def substituteLHS(self, lineNum1, lineNum2): else: print("Cannot substitute without an Equation") - def modus(self, lineNum1, lineNum2): + def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think) """ modus pones: given A->B and A, the function concludes B and add it as a new line in the proof :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 = self.steps[lineNum2] + 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(lineNum2)}'] + self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] self.show() - elif isinstance(ev2, Implies): - A = ev2.assum - B = ev2.conc - if A == ev1: - self.steps += [B] - self.justifications += [f'Modus Ponens on {str(lineNum2)}, {str(lineNum1)}'] - self.show() else: - print (f"Neither of {str(lineNum1)}, {str(lineNum2)} are an implies statement") + print (f"Line {str(lineNum1)} is not an implies statement") def inverseElimRHS(self,lineNum): """ @@ -473,10 +470,10 @@ def introSubproof(self, assum): 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] - self.justifications += ["intro subproof"] - return subproof + subproof = Proof(label="Subproof", assumption=assum, steps=[self.steps], justifications = [self.justifications]) # how do we deal with this? + self.steps += [assum] + self.justifications += ["Intro Subproof Assumption"] # How can we track subproof throughout parent proof? + self.show() def concludeSubproof(self, lineNum): """ @@ -485,8 +482,13 @@ def concludeSubproof(self, lineNum): 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 + evidence = self.steps[lineNum] + if isinstance(evidence, Not): + self.steps += [evidence.arg] + self.justifications += ["Concluded Subproof"] + self.show() + else: + print(f"Cannot conclude subproof") # THIS IS A MESS, NEED TO ACTUALLY CATCH ERRORS def introElement(self,G, name): """ @@ -544,3 +546,73 @@ def closure(self,G,a,b): print(f"{a} is not in {G}") else: print(f"{b} is not in {G}") + + def cancelRight(self, lineNum, mult): + ''' + Cancels element from right side of multiplication if it exists + :param lineNum: the line where the equation resides + :param mult: the list of elements to eliminate + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, Eq): + rhselems = evidence.RHS.products + 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.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}") + else: + print(f"It doesn't seem like line {lineNum} contains an equation") + + def cancelLeft(self, lineNum, mult): + ''' + Cancels element from left side of multiplication if it exists + :param lineNum: the line where the equation resides + :param mult: the list of elements to eliminate + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, Eq): + rhselems = evidence.RHS.products + 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.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}") + else: + print(f"It doesn't seem like line {lineNum} contains an equation") + + def switchSidesOfEqual(self, lineNum): + ''' + Switches an equality like x=y to become y=x + :param lineNum: the line where the equality to be flipped is on + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, Eq): + rhs = evidence.RHS + lhs = evidence.LHS + self.steps += [Eq(rhs , lhs , evidence.parentgroup )] + self.justifications += [f"Switched sides of line {lineNum}"] + self.show() + else: + print(f"Hmm, it doesn't look like line {lineNum} isn't an equality") + + def notElim(self, lineNum1, lineNum2): + ''' + Eliminate a not into a contradiction + :param lineNum1: the line containing the not statement + :param lineNum2: the line which has the real statement + ''' + evidence1 = self.steps[lineNum1] + if isinstance(evidence1, Not): + result = evidence1.elim(self.steps[lineNum2]) + self.steps += [result] + self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] + self.show() + else: + print(f"The statement on line {lineNum1} isn't a Not") \ No newline at end of file