diff --git a/__pycache__/group.cpython-38.pyc b/__pycache__/group.cpython-38.pyc index 6fb0dd6..be2271f 100644 Binary files a/__pycache__/group.cpython-38.pyc and b/__pycache__/group.cpython-38.pyc differ diff --git a/__pycache__/logicObjects.cpython-38.pyc b/__pycache__/logicObjects.cpython-38.pyc index 3ee516a..800ea37 100644 Binary files a/__pycache__/logicObjects.cpython-38.pyc and b/__pycache__/logicObjects.cpython-38.pyc differ diff --git a/__pycache__/proof.cpython-38.pyc b/__pycache__/proof.cpython-38.pyc index 951a1bc..94cfe15 100644 Binary files a/__pycache__/proof.cpython-38.pyc and b/__pycache__/proof.cpython-38.pyc differ diff --git a/contradiction_proof.py b/contradiction_proof.py deleted file mode 100644 index dcac2a3..0000000 --- a/contradiction_proof.py +++ /dev/null @@ -1,27 +0,0 @@ -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) -p.qed(12) diff --git a/logicObjects.py b/logicObjects.py index 4075cee..f0449be 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -1,5 +1,6 @@ import copy from dataclasses import replace +from re import L from element import * @@ -49,6 +50,14 @@ def elim(self,num): if num==2: return self.arg2 + def __eq__(self,other): + if not isinstance(other,And): + return False + return (self.arg1==other.arg1 and self.arg2==other.arg2) or (self.arg1==other.arg2 and self.arg2==other.arg1) + + def __repr__(self): + return "("+ str(self.arg1)+" and "+str(self.arg2)+ ")" + class Or: def __init__(self, arg1, arg2): self.arg1 = arg1 @@ -71,15 +80,12 @@ def elim(self, arg): return self.conc def __eq__(self, other): + if not isinstance(other,Implies): + return False return self.assum == other.assum and self.conc == other.conc def __repr__(self): - assumptionstr = "" - for assumption in self.assum: - assumptionstr += str(assumption) - assumptionstr += ", " - assumptionstr = assumptionstr[:-2] - return assumptionstr + " → " + str(self.conc) + return str(self.assum) + " → " + str(self.conc) class Not: def __init__(self, arg): diff --git a/proof.py b/proof.py index 13e5698..ade3e28 100644 --- a/proof.py +++ b/proof.py @@ -5,18 +5,21 @@ from integer import * from logicObjects import * - class Proof: - def __init__(self, label, assumption, goal=None, steps=[], justifications = []): # make goal optional + def __init__(self, label, assumption, goal=None, steps=[], justifications = [], depth=0, linestart=0): # make goal optional + self.linestart = linestart self.label = label + self.depth = depth self.assumption = assumption self.goal = goal # this is an implies - self.steps = [] - self.justifications = [] + self.steps = steps + self.justifications = justifications self.env = {} self.subproof = None def qed(self, lineNum): + print(self.goal, self.steps[lineNum]) + if self.goal == self.steps[lineNum]: self.steps+=["□"] self.justifications += ["QED"] @@ -30,17 +33,21 @@ def undo(self): self.show() 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)): - 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('') + if self.depth==0: + print('') + print('Proof : ' + self.label) + print('--------------------------------') + else: + print('Subproof : assume ' + str(self.assumption)) + print('--------------------------------') + i = self.linestart + while i < len(self.steps): + if isinstance(self.steps[i],Proof): + self.steps[i].show() + i+=len(self.steps[i].steps) + else: + print("\t"*self.depth + str(i) + ': ' + str(self.steps[i]) + '\t' + str(self.justifications[i])) + i+=1 def introAssumption(self, expr): self.steps += [expr] @@ -470,10 +477,11 @@ 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", 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? + subproof = Proof(label="Subproof", assumption=assum, steps=copy.deepcopy(self.steps), justifications=copy.deepcopy(self.justifications), depth=self.depth+1, linestart=len(self.steps)) self.show() + self.steps+=[subproof] + self.justifications+=["IntroSubproof"] + return subproof def concludeSubproof(self, lineNum): """ @@ -482,13 +490,16 @@ 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 """ - evidence = self.steps[lineNum] - if isinstance(evidence, Not): - self.steps += [evidence.arg] - self.justifications += ["Concluded Subproof"] - self.show() + evidence = self.steps[-1] + if isinstance(evidence, Proof): + conc = Implies(evidence.assumption,evidence.steps[lineNum]) + self.steps += [None]*len(evidence.steps) + self.justifications += [None]*len(evidence.steps) + self.steps += [conc] + self.justifications += ["Conclusion of subproof"] else: - print(f"Cannot conclude subproof") # THIS IS A MESS, NEED TO ACTUALLY CATCH ERRORS + print("You can only conclude a subproof right after one") + self.show() def introElement(self,G, name): """ @@ -628,4 +639,24 @@ def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot assums.append(self.steps[line]) self.steps += [Implies(assums,self.steps[lineNumConc])] self.justifications += [f"Introduced implies based on assumptions on lines {lineNumsAssums} to conclude line {lineNumConc}"] - self.show() \ No newline at end of file + self.show() + + def andElim(self, lineNum, n): + ''' + Eliminate a not into a contradiction + :param lineNum1: the line containing the not statement + :param lineNum2: the line which has the real statement + ''' + evidence = self.steps[lineNum] + if isinstance(evidence, And): + if n==1: + self.steps += [evidence.arg1] + self.justifications += ["And elimination"] + elif n==2: + self.steps += [evidence.arg2] + self.justifications += ["And elimination"] + else: + print("You must choose argument 1 or 2") + else: + print("The provided line is not an and statement") + \ No newline at end of file diff --git a/unique inverses.py b/unique inverses.py new file mode 100644 index 0000000..477898c --- /dev/null +++ b/unique inverses.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( And(inversePropertyOne,inversePropertyTwo) , Eq( Mult(['d']), Mult(['c']), G) ) +p = Proof('Unique Inverses', assumption = None, goal=uniqueInverse) +p.introGroup(G) +p.introElement(G,'a') +p.introElement(G,'c') +p.introElement(G,'d') +p2 = p.introSubproof(And(inversePropertyOne,inversePropertyTwo)) +p2.accessAssumption() +p2.andElim(4,1) +p2.andElim(4,2) +p2.rightSidesEq(5,6) +p2.cancelLeft(7, ['a']) +p2.switchSidesOfEqual(8) +p.concludeSubproof(9) +p.qed(15)