diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000..c8693d7 Binary files /dev/null and b/.DS_Store differ diff --git a/__pycache__/element.cpython-39.pyc b/__pycache__/element.cpython-39.pyc index 9dd0787..b886ac3 100644 Binary files a/__pycache__/element.cpython-39.pyc and b/__pycache__/element.cpython-39.pyc differ diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc index e2a172c..bb40103 100644 Binary files a/__pycache__/group.cpython-39.pyc and b/__pycache__/group.cpython-39.pyc differ diff --git a/__pycache__/integer.cpython-39.pyc b/__pycache__/integer.cpython-39.pyc index 2546654..504441c 100644 Binary files a/__pycache__/integer.cpython-39.pyc and b/__pycache__/integer.cpython-39.pyc differ diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index 74f4fb5..a913b8e 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 9a283a2..e9a55eb 100644 Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ diff --git a/abelian_proof.py b/abelian_proof.py index 2ff40c0..4027512 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -7,13 +7,13 @@ G = group('G','*') 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']), G.elements['e'],G)), goal=abelianG) +p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), Mult([G.elements['e']]),G)), goal=abelianG) p.introGroup(G) p.introElement(G,'a') p.introElement(G,'b') p.closure(G,'a','b') -p.accessAssumption() -p.forallElim(4,['a * b']) +p.accessAssumption() # this and below one +p.forallElim(4,['a * b']) # combine two steps p.leftMult('a',5) p.forallElim(4,['a']) p.substituteRHS(6,7) diff --git a/element.py b/element.py index b9bee3d..9401d8d 100644 --- a/element.py +++ b/element.py @@ -34,6 +34,7 @@ def mult(self,other, group): # this is just for representation elif binOp in self.elementName and ')' != self.elementName[-1]: return "(" + self.elementName + ")" + binOp + other.elementName else: + return self.elementName + binOp + other.elementName def addToGroup(self, group): diff --git a/group.py b/group.py index 50699f3..6302c32 100644 --- a/group.py +++ b/group.py @@ -1,6 +1,6 @@ exec(compile(source=open('element.py').read(), filename='element.py', mode='exec')) -from logicObjects import identity, Mult, inverse - +from logicObjects import identity, Mult +from element import * class group: # TRUTHS for all classes - need to add more here @@ -15,7 +15,7 @@ class group: def __init__(self, name, binOp, additionalGroupProperties = None): self.groupName = name self.binaryOperator = binOp - self.elements.update({self.identity_identifier:Mult([identity(self)])}) + self.elements.update({self.identity_identifier:identity(self)}) if additionalGroupProperties != None: self.groupProperties.update(additionalGroupProperties) @@ -41,7 +41,7 @@ def newInverse(self, elementName): # declare new element in group with elementName def newElement(self,elementName): if elementName not in self.elements: - self.elements.update({elementName:Mult([element(elementName,self)])}) + self.elements.update({elementName:element(elementName,self)}) else: print("Sorry, that element already exists!") @@ -53,7 +53,7 @@ def mulElements(self, elem1, elem2): # should this return an equation? try: gelem1 = self.elements[elem1] gelem2 = self.elements[elem2] - result = gelem1 * gelem2 # need to specify which group we are multiplying in + result = Mult([gelem1 ,gelem2]) # need to specify which group we are multiplying in self.elements.update({repr(result):result}) # is this the right? except: print("Sorry, one or both of these elements are not in the group!") diff --git a/inverse_of_ab.py b/inverse_of_ab.py new file mode 100644 index 0000000..dd865a7 --- /dev/null +++ b/inverse_of_ab.py @@ -0,0 +1,26 @@ +from enum import unique +from telnetlib import GA +from proof import * +from element import * +from group import * +from integer import * +from logicObjects import * + +G = group('G','*') +ab_inverse = forall(['a','b'], G, Eq(Mult([inverse('b',G),inverse('a',G)]),Mult([inverse(Mult(['a','b']),G)]),G)) +p = Proof('Inverse of ab Proof', assumption = None, goal = ab_inverse) +p.introGroup(G) +p.introElement(G,'a') +p.introElement(G,'b') +p.closure(G,'a','b') +p.introInverse(G, Mult(['a','b'])) +p.rightMultInverse('b',4) +p.inverseElimLHS(5) +p.identleft(6) +p.identright(7) +p.rightMultInverse('a',8) +p.inverseElimLHS(9) +p.identleft(10) +p.switchSidesOfEqual(11) +p.forAllIntroduction(12,["a","b"],[1,2]) +p.qed(13) \ No newline at end of file diff --git a/logicObjects.py b/logicObjects.py index 0440b52..43a843b 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -31,7 +31,10 @@ def replace(self, var, expr): #print(self.products,var.products,expr.products) while i < len(self.products): if self.products[i:i+len(var.products)] == var.products: - new_products += expr.products + if isinstance(expr,Mult): + new_products += expr.products + else: + new_products.append(expr) i+=len(var.products) else: new_products.append(self.products[i]) @@ -253,6 +256,11 @@ def __init__ (self, prpty, pg): ## Special types of elements/groups +# class element_(element): +# def __init__(self, pg, elementName): +# elementName = elementName +# super().__init__(elementName, pg) + class identity(element): def __init__(self, pg): elementName = pg.identity_identifier @@ -264,12 +272,24 @@ def __init__(self, pg): pg.addElementProperty(idnty,elementName) class inverse(element): - def __init__(self, elementName, pg): - inverseName = '(' + elementName + ")^(-1)" + def __init__(self, object, pg): + if type(object) == str: + elementName = object + inverseName = elementName + "^(-1)" + # lhs = Mult([inverseName,pg.elements[object]]) + else: + elementName = repr(object) + inverseName = "(" + elementName + ")" + "^(-1)" + # lhs = Mult([inverseName]+object.products) 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) + self.inverseName = inverseName + self.elementName = elementName + def __repr__(self): + return self.inverseName + # self or elementName? + # rhs = Mult([pg.identity_identifier]) + # inverseEq = Eq(lhs,rhs,pg) + # pg.addGroupProperty(inverseEq, "Inverse of " + elementName) + ## TO DO: class generator(element): diff --git a/proof.py b/proof.py index 7c986c0..3e267fe 100644 --- a/proof.py +++ b/proof.py @@ -1,3 +1,4 @@ +import os, sys from email import message from re import L @@ -23,7 +24,7 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = [], def qed(self, lineNum): if self.goal == self.steps[lineNum]: - self.steps+=["□"] + self.steps+=["."] self.justifications += ["QED"] self.show() else: @@ -399,9 +400,9 @@ def substituteRHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.LHS} with {ev2.RHS} on line {lineNum1}'] self.show() else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def substituteLHS(self, lineNum1, lineNum2): """ @@ -418,9 +419,9 @@ def substituteLHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}'] self.show() else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + print('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think) """ @@ -440,9 +441,9 @@ def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] self.show() else: - messagebox.showerror('Proof Error',f"Line {str(lineNum1)} is not an implies statement") + print('Proof Error',f"Line {str(lineNum1)} is not an implies statement") else: - messagebox.showerror('Proof Error',"The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") + print('Proof Error',"The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") def inverseElimRHS(self,lineNum): """ @@ -467,15 +468,15 @@ def inverseElimRHS(self,lineNum): lawApplied=True break if lawApplied==False: - messagebox.showerror('Proof Error',f"Inverse laws can't be applied on line {lineNum}") + print('Proof Error',f"Inverse laws can't be applied on line {lineNum}") else: self.steps += [newProducts] self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") - + def inverseElimLHS(self,lineNum): """ finds the first pair of group element and its inverse and returns the group element @@ -488,30 +489,31 @@ def inverseElimLHS(self,lineNum): for i in range(len(l)-1): if isinstance(l[i],element) and isinstance(l[i+1],inverse) and (l[i].elementName == l[i+1].elementName): group = l[i].parentGroups[0] # how to deal with multiple groups? - l[i] = group.identity_identifier + l[i] = group.elements[group.identity_identifier] newProducts = Mult(l[:i+1]+l[i+2:]) lawApplied=True break elif isinstance(l[i],inverse) and isinstance(l[i+1],element) and (l[i].elementName == l[i+1].elementName): group = l[i+1].parentGroups[0] # how to deal with multiple groups? - l[i] = group.identity_identifier + l[i] = group.elements[group.identity_identifier] newProducts = Mult(l[:i+1]+l[i+2:]) # should we include 'e' in the Mult object? lawApplied=True break if lawApplied==False: - messagebox.showerror('Proof Error',f"Inverse laws can't be applied on line {lineNum}") + print('Proof Error',f"Inverse laws can't be applied on line {lineNum}") else: - self.steps += [newProducts] + self.steps += [Eq(newProducts,evidence.RHS,evidence.group)] self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") ## For all and there exists elimination def forallElim(self, lineNum, replacements): """ - Given an expression forall(a,b,statement), forallElim substitutes a with another input variable to create a new forall statement + Given an expression forall(a,b,statement), forallElim substitutes a with another input + variable to create a new forall statement :param lineNum: The line number of the line that showed the original forall statement :param replacements: the list of elements to replace the existential elements """ @@ -522,7 +524,7 @@ def forallElim(self, lineNum, replacements): self.justifications += [f'For all elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error',f"There is no forall statmenent on line {lineNum}") + print('Proof Error',f"There is no forall statmenent on line {lineNum}") def thereexistsElim(self, lineNum, replacements): # We can only do this once! @@ -538,7 +540,7 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once! self.justifications += [f'There exists elimination on line {lineNum}'] self.show() else: - messagebox.showerror('Proof Error', f"There is no there exists statmenent on line {lineNum}") + print('Proof Error', f"There is no there exists statmenent on line {lineNum}") ## Multiplication manipulation @@ -558,9 +560,9 @@ def leftMult(self, elemName, lineNum): self.justifications += [f'Left multiply line {lineNum} by {elem}'] self.show() else: - messagebox.showerror('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) else: - messagebox.showerror('Proof Error', f"Line {lineNum} is not an equation") + print('Proof Error', f"Line {lineNum} is not an equation") def rightMult (self, elemName, lineNum): """ @@ -578,9 +580,39 @@ def rightMult (self, elemName, lineNum): self.justifications += [f'Right multiply line {lineNum} by {elem}'] self.show() else: - messagebox.showerror('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + else: + print('Proof Error', f"Line {lineNum} is not an equation") + + + def rightMultInverse (self, elemName, lineNum): + eq = copy.deepcopy(self.steps[lineNum]) + if isinstance(eq, Eq): + if elemName in eq.group.elements: + product = self.MultElem(eq.LHS,inverse(elemName,eq.group)) + result = Eq(product, self.MultElem(eq.RHS, inverse(elemName,eq.group)), eq.group) + self.steps += [result] + self.justifications += ['Right multiply line {lineNum} by ' + elemName] + self.show() + else: + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) else: - messagebox.showerror('Proof Error', f"Line {lineNum} is not an equation") + print('Proof Error', f"Line {lineNum} is not an equation") + + def leftMultInverse (self, elemName, lineNum): + eq = copy.deepcopy(self.steps[lineNum]) + if isinstance(eq, Eq): + if elemName in eq.group.elements: + product = self.MultElem(inverse(elemName,eq.group), eq.LHS) + result = Eq(product, self.MultElem(inverse(elemName,eq.group), eq.RHS), eq.group) + self.steps += [result] + self.justifications += ['Right multiply line {lineNum} by ' + elemName] + self.show() + else: + print('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) + else: + print('Proof Error', f"Line {lineNum} is not an equation") + ##power methods def breakPower(self,input): """ @@ -597,7 +629,7 @@ def breakPower(self,input): self.justifications += ['Convert power object to mult object'] self.show() else: - messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") + print('Proof Error',f"Expected a power object but received type {type(input)}") def combinePower(self, mult): """ @@ -619,7 +651,7 @@ def combinePower(self, mult): self.justifications += ['Convert multiplications to equivalent powers'] self.show() else: - messagebox.showerror('Proof Error',f"Expected a Mult object but received type {type(mult)}") + print('Proof Error',f"Expected a Mult object but received type {type(mult)}") def splitPowerAddition(self,input): """ @@ -631,7 +663,7 @@ def splitPowerAddition(self,input): exp=input.exponent l=exp.split("+") if len(l)==1: - messagebox.showerror('Proof Error',"No power addition to be split apart") + print('Proof Error',"No power addition to be split apart") else: multList=[] for i in l: @@ -641,7 +673,7 @@ def splitPowerAddition(self,input): self.justifications += ["Split up power with addition in exponents"] self.show() else: - messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") + print('Proof Error',f"Expected a power object but received type {type(input)}") def splitPowerMult(self,input): @@ -654,7 +686,7 @@ def splitPowerMult(self,input): exp=input.exponent l=exp.split("*") if len(l)==1: - messagebox.showerror('Proof Error',"No power multiplication to be split apart") + print('Proof Error',"No power multiplication to be split apart") else: elem=element for i in l: @@ -664,7 +696,7 @@ def splitPowerMult(self,input): self.justifications += ["Split up power with multiplication in exponents"] self.show() else: - messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") + print('Proof Error',f"Expected a power object but received type {type(input)}") ## Identity and equality elimination def rightSidesEq(self, lineNum1, lineNum2): @@ -680,7 +712,7 @@ def rightSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same right side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - messagebox.showerror('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") + print('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") def leftSidesEq(self, lineNum1, lineNum2): """ @@ -695,7 +727,7 @@ def leftSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same left side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - messagebox.showerror('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") + print('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") def identleft(self, lineNum): """ @@ -719,7 +751,7 @@ def identleft(self, lineNum): break # else we can't apply identity elimination if l1==[]: - messagebox.showerror('Proof Error',"Identity can't be applied") + print('Proof Error',"Identity can't be applied") else: newProduct = Mult(l1) ret = Eq(newProduct,evidence.RHS,evidence.group) @@ -727,7 +759,7 @@ def identleft(self, lineNum): self.justifications += ["identity elimination "] self.show() else: - messagebox.showerror('Proof Error',f"Expected an equation on line {lineNum} but received {type(evidence)}") + print('Proof Error',f"Expected an equation on line {lineNum} but received {type(evidence)}") def identright(self, lineNum): @@ -738,6 +770,7 @@ def identright(self, lineNum): evidence = self.steps[lineNum] if isinstance(evidence,Eq): l = evidence.RHS.products + print(type(l[0]),type(l[1])) l1=[] for i in range(len(l)-1): # deals with the case a*1 @@ -760,23 +793,26 @@ def identright(self, lineNum): self.justifications += ["identity elimination "] self.show() else: - messagebox.showerror('Proof Error', f"Expected an equation on line {lineNum} but received {type(evidence)}") + print('Proof Error', f"Expected an equation on line {lineNum} but received {type(evidence)}") - def introReflexive(self,eq): + def introReflexive(self,name,G): """ Introduce a reflexive equality (like x=x) Necessary to show something equals something else when not given a starting equation :param eq: The equality you want to introduce """ - if eq.LHS == eq.RHS: - self.steps+=[eq] - self.justifications += ["reflexive equality"] - self.show() - else: - messagebox.showerror('Proof Error', "This is not reflexive") + self.steps+=[Eq(name,name,G)] + self.justifications += ["reflexive equality"] + self.show() + # if eq.LHS == eq.RHS: + # self.steps+=[eq] + # self.justifications += ["reflexive equality"] + # self.show() + # else: + # print('Proof Error', "This is not reflexive") def reduceLogic(self, lineNum): """ @@ -789,7 +825,7 @@ def reduceLogic(self, lineNum): self.justifications += ["logic reduction"] self.show() else: - messagebox.showerror('Proof Error', "This is not a logic statement") + print('Proof Error', "This is not a logic statement") def introCases(self, case): """ @@ -842,7 +878,7 @@ def introElement(self,G, name): :param name: the name of the new element """ if G.contains(name): - messagebox.showerror('Proof Error', f"{name} is already in {G}") + print('Proof Error', f"{name} is already in {G}") else: self.env[name] = G.newElement(name) self.steps += [In(name, G)] @@ -863,9 +899,9 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): v = vars[i] l = elemIntroLines[i] if self.steps[l].elem!=vars[i]: - messagebox.showerror('Proof Error', f'Line {l} does not introduce variable {v}') + print('Proof Error', f'Line {l} does not introduce variable {v}') elif self.steps[l].group!=G: - messagebox.showerror('Proof Error', f'Element {v} is not in group {G}') + print('Proof Error', f'Element {v} is not in group {G}') else: #If you make it here, this is a valid for all intro self.steps+=[forall(vars,G,evidence)] @@ -887,9 +923,9 @@ def closure(self,G,a,b): self.show() else: if not G.contains(a): - messagebox.showerror('Proof Error',f"{a} is not in {G}") + print('Proof Error',f"{a} is not in {G}") else: - messagebox.showerror('Proof Error',f"{b} is not in {G}") + print('Proof Error',f"{b} is not in {G}") def cancelRight(self, lineNum, mult): ''' @@ -907,9 +943,9 @@ def cancelRight(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - messagebox.showerror('Proof Error',f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") + print('Proof Error',f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def cancelLeft(self, lineNum, mult): ''' @@ -927,9 +963,9 @@ def cancelLeft(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - messagebox.showerror('Proof Error',f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") + print('Proof Error',f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") else: - messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") + print('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def switchSidesOfEqual(self, lineNum): ''' @@ -944,7 +980,7 @@ def switchSidesOfEqual(self, lineNum): self.justifications += [f"Switched sides of line {lineNum}"] self.show() else: - messagebox.showerror('Proof Error',f"Hmm, it doesn't look like line {lineNum} isn't an equality") + print('Proof Error',f"Hmm, it doesn't look like line {lineNum} isn't an equality") def notElim(self, lineNum1, lineNum2): ''' @@ -959,7 +995,7 @@ def notElim(self, lineNum1, lineNum2): self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] self.show() else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum1} isn't a Not statement") + print('Proof Error',f"The statement on line {lineNum1} isn't a Not statement") def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it ''' @@ -991,7 +1027,27 @@ def andElim(self, lineNum, n): self.justifications += ["And elimination"] self.show() else: - messagebox.showerror('Proof Error',"You must choose argument 1 or 2") + print('Proof Error',"You must choose argument 1 or 2") + else: + print('Proof Error',f"The statement on line {lineNum} isn't an And statement") + + def introInverse(self, G, name): + if type(name) == "str": + if not G.contains(name): + print('Proof Error', f"{name} is not defined") + return else: - messagebox.showerror('Proof Error',f"The statement on line {lineNum} isn't an And statement") - \ No newline at end of file + for x in name.products: + if not G.contains(x): + print('Proof Error', f"{x} is not defined") + return + if type(name) == str: + lhs = self.MultElem(inverse(name,G),G.elements[name]) + + else: + name_ = Mult([G.elements[x] for x in name.products]) + lhs = self.MultElem(inverse(name_,G),name_) + rhs = Mult([G.elements["e"]]) + self.steps += [Eq(lhs,rhs,G)] + self.justifications += ["Introducing the inverse of an element"] + self.show() \ No newline at end of file diff --git a/unique inverses.py b/unique_inverses.py similarity index 100% rename from unique inverses.py rename to unique_inverses.py