diff --git a/__pycache__/element.cpython-38.pyc b/__pycache__/element.cpython-38.pyc new file mode 100644 index 0000000..5cc1d56 Binary files /dev/null and b/__pycache__/element.cpython-38.pyc differ diff --git a/__pycache__/element.cpython-39.pyc b/__pycache__/element.cpython-39.pyc new file mode 100644 index 0000000..9dd0787 Binary files /dev/null and b/__pycache__/element.cpython-39.pyc differ diff --git a/__pycache__/environment.cpython-38.pyc b/__pycache__/environment.cpython-38.pyc new file mode 100644 index 0000000..5567b13 Binary files /dev/null and b/__pycache__/environment.cpython-38.pyc differ diff --git a/__pycache__/environment.cpython-39.pyc b/__pycache__/environment.cpython-39.pyc new file mode 100644 index 0000000..3361f4d Binary files /dev/null and b/__pycache__/environment.cpython-39.pyc differ diff --git a/__pycache__/group.cpython-38.pyc b/__pycache__/group.cpython-38.pyc new file mode 100644 index 0000000..6fb0dd6 Binary files /dev/null and b/__pycache__/group.cpython-38.pyc differ diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc new file mode 100644 index 0000000..d110469 Binary files /dev/null and b/__pycache__/group.cpython-39.pyc differ diff --git a/__pycache__/integer.cpython-38.pyc b/__pycache__/integer.cpython-38.pyc new file mode 100644 index 0000000..91e6300 Binary files /dev/null and b/__pycache__/integer.cpython-38.pyc differ diff --git a/__pycache__/integer.cpython-39.pyc b/__pycache__/integer.cpython-39.pyc new file mode 100644 index 0000000..2546654 Binary files /dev/null and b/__pycache__/integer.cpython-39.pyc differ diff --git a/__pycache__/logicObjects.cpython-38.pyc b/__pycache__/logicObjects.cpython-38.pyc new file mode 100644 index 0000000..3ee516a Binary files /dev/null and b/__pycache__/logicObjects.cpython-38.pyc differ diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc new file mode 100644 index 0000000..39ed0b7 Binary files /dev/null and b/__pycache__/logicObjects.cpython-39.pyc differ diff --git a/__pycache__/proof.cpython-38.pyc b/__pycache__/proof.cpython-38.pyc new file mode 100644 index 0000000..951a1bc Binary files /dev/null and b/__pycache__/proof.cpython-38.pyc differ diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc new file mode 100644 index 0000000..43a5bec Binary files /dev/null and b/__pycache__/proof.cpython-39.pyc differ diff --git a/abelian_proof.py b/abelian_proof.py index 842657a..452e272 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -1,12 +1,27 @@ from proof import * from element import * -from environment import * from group import * from integer import * from logicObjects import * -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']), identity('1','G'),"G")), goal=abelianG) -p.introGroup('G') -p.introGroupElement('a', 'G') -p.introGroupElement('b', 'G') \ No newline at end of file + +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.introGroup(G) +p.introElement(G,'a') +p.introElement(G,'b') +p.closure(G,'a','b') +p.accessAssumption() +p.forallElim(4,['a * b']) +p.leftMult(G.elements['a'],5) +p.forallElim(4,['a']) +p.substituteRHS(6,7) +p.identleft(8) +p.identright(9) +p.rightMult(G.elements['b'],10) +p.forallElim(4,['b']) +p.substituteRHS(11,12) +p.identleft(13) +p.forAllIntroduction(14,["a","b"],[1,2]) +p.qed(15) diff --git a/element.py b/element.py index f542bdb..b9bee3d 100644 --- a/element.py +++ b/element.py @@ -22,7 +22,10 @@ def __repr__(self): return self.elementName def __eq__(self,other): - return self.elementName == other.elementName + try: + return self.elementName == other.elementName + except: + return False def mult(self,other, group): # this is just for representation binOp = group.binaryOperator @@ -60,24 +63,5 @@ def __init__(self, elementName, pg): def fullDescription(self): return "Existential element " + self.elementName + " in group" + self.parentGroups[0].groupName # can only belong to one group -## Special types of elements/groups - -class identity(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) - -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) ## need to add: generator \ No newline at end of file diff --git a/environment.py b/environment.py deleted file mode 100644 index c8ffba8..0000000 --- a/environment.py +++ /dev/null @@ -1,34 +0,0 @@ -import copy - -class Environment: - env = [{}] - assumption = [] - depth = 0 - - #ELEMENTS - - def getElem(self, elem): - return self.env[self.depth]["Elements"][elem] - - def addElemProp(self, elem, type, prop): - #type could be in group, or equality, ect - self.env[self.depth]["Elements"][elem][type].append(prop) - - #GROUPS - - def getGroup(self, group): - return self.env[self.depth]["Groups"][group] - - def addGroupProp(self, group, type, prop): - #type could be for all, contains, ect - self.env[self.depth]["Groups"][group][type].append(prop) - - def newSubproof(self, assume): - self.env.append(self.env[-1].copy()) - self.assumption.append(assume) - self.depth+=1 - - def endSubproof(self): - self.env.pop() - self.depth -= 1 - return self.assumption.pop() \ No newline at end of file diff --git a/group.py b/group.py index 844343d..0002318 100644 --- a/group.py +++ b/group.py @@ -1,17 +1,20 @@ exec(compile(source=open('element.py').read(), filename='element.py', mode='exec')) +from logicObjects import identity, Mult + class group: # TRUTHS for all classes - need to add more here identity_identifier = 'e' elements = {} groupProperties = {} + elementProperties = {} binaryOperator = "" groupName = "" def __init__(self, name, binOp, additionalGroupProperties = None): self.groupName = name self.binaryOperator = binOp - self.elements.update({self.identity_identifier:identity(self.identity_identifier,self)}) + self.elements.update({self.identity_identifier:Mult([identity(self)])}) if additionalGroupProperties != None: self.groupProperties.update(additionalGroupProperties) @@ -31,7 +34,7 @@ def __mul__(self,other): # group cartesian product. Worry about this later # declare new element in group with elementName def newElement(self,elementName): if elementName not in self.elements: - self.elements.update({elementName:element(elementName,self)}) + self.elements.update({elementName:Mult([element(elementName,self)])}) else: print("Sorry, that element already exists!") @@ -43,10 +46,19 @@ def mulElements(self, elem1, elem2): # should this return an equation? try: gelem1 = self.elements[elem1] gelem2 = self.elements[elem2] - result = gelem1.mult(gelem2, self) # need to specify which group we are multiplying in - self.elements.update({result:element(result,self)}) # is this the right? + result = 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!") def addGroupProperty(self, property, propertyName): - self.groupProperties[propertyName] = property \ No newline at end of file + self.groupProperties[propertyName] = property + + def addElementProperty(self, property, elementName): + if elementName in self.elements or elementName == self.identity_identifier: + self.elementProperties[elementName] = property + else: + print("That element doesn't exist!", property, elementName) + + def contains(self, elementName): + return elementName in self.elements \ No newline at end of file diff --git a/logicObjects.py b/logicObjects.py index 522f7ad..e90723f 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -1,7 +1,7 @@ import copy from dataclasses import replace -from element import arbitrary +from element import * class Mult: def __init__(self, elemList): @@ -25,7 +25,17 @@ def __mul__(self,other): return Mult(self.products+[other]) #Mult with element def replace(self, var, expr): - return Mult([x if x != var else expr for x in self.products]) + new_products = [] + i = 0 + #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 + i+=len(var.products) + else: + new_products.append(self.products[i]) + i+=1 + return Mult(new_products) class And: @@ -72,6 +82,14 @@ class Bottom: def elim(self, conclusion): return conclusion +class In: + def __init__(self, elem, grp): + self.elem = elem + self.grp = grp + + def __repr__(self): + return str(self.elem) + " ∈ " + str(self.grp) + class Eq: def __init__(self,LHS,RHS,pg): self.LHS = LHS @@ -121,20 +139,30 @@ def __repr__(self): return 'forall(' + str(self.arbelems) + ' in ' + str(self.group) + ', ' + str(self.eq) +')' def __eq__(self,other): - return self.arbelems == other.arbelems and self.group == other.group and self.eq == other.eq + if not isinstance(other,forall): + return False + if len(self.arbelems)==len(other.arbelems): + print(self,other) + new = copy.deepcopy(self) + replaced = new.replace(other.arbelems) + return replaced == other.eq + else: + return False def replace(self, replacements): # replacements = ['x','y'] - strings of the elements if len(replacements) == len(self.arbelems): - if all(elem in self.group.elements for elem in replacements): # check if replacements are all normal elements of self.group - neweq = copy.deepcopy(self.eq) - for i in range(len(replacements)): - neweq = neweq.replace(self.arbelems[i],replacements[i]) # repeatedly replace - return neweq - else: - raise Exception(f"Replacements contains elements that are not in {self.group}") + #if all(elem in self.group.elements for elem in replacements): # check if replacements are all normal elements of self.group + #The scope of thee elements in a for all should be contained in that for all + #Checking if in the group should happen at elimination and introduction + neweq = copy.deepcopy(self.eq) + for i in range(len(replacements)): + neweq = neweq.replace(Mult([self.arbelems[i]]),self.group.elements[replacements[i]]) # repeatedly replace + return neweq + #else: + #print(f"Replacements contains elements that are not in {self.group}") else: - raise Exception("Replacements is not the same length as the list of arbitrary elements") + print("Replacements is not the same length as the list of arbitrary elements") class thereexists: def __init__(self, vars, g, eq): # should we check that vars is existential elements? @@ -156,6 +184,27 @@ def replace(self, replacements): neweq = neweq.replace(self.existelems[i],replacements[i]) # repeatedly replace return neweq else: - raise Exception(f"Replacements contains elements that are not in {self.group}") + print(f"Replacements contains elements that are not in {self.group}") else: - raise Exception("Replacements is not the same length as the list of existential elements") \ No newline at end of file + print("Replacements is not the same length as the list of existential elements") + +## Special types of elements/groups + +class identity(element): + def __init__(self, pg): + elementName = pg.identity_identifier + 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) + +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) diff --git a/proof.py b/proof.py index 3ea3e5e..cb128ac 100644 --- a/proof.py +++ b/proof.py @@ -1,5 +1,5 @@ +from re import L from element import * -from environment import * from group import * from integer import * from logicObjects import * @@ -8,16 +8,20 @@ class Proof: def __init__(self, label, assumption, goal=None, steps=[], justifications = []): # make goal optional self.label = label - self. assumption = assumption + self.assumption = assumption self.goal = goal # this is an implies + self.steps = [] self.justifications = [] - self.environment = {} # add strings names to environment for parsing + self.env = {} self.depth = 0 - self.currAssumption = [goal.assum] - self.show() - def qed(self): - return self.goal.conc in self.steps + def qed(self, lineNum): + if self.goal == self.steps[lineNum]: + self.steps+=["□"] + self.justifications += ["QED"] + self.show() + else: + print("This is not the same as the goal") def undo(self): self.steps = self.steps[:-1] @@ -46,6 +50,16 @@ 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"] + #deal with environments + self.env[grp.groupName] = grp + self.show() + + def accessAssumption(self): + self.steps += [self.assumption] + self.justifications += ["Accessed Assumption"] self.show() def MultElem(self, element1, element2): @@ -62,11 +76,50 @@ def MultElem(self, element1, element2): l.append(element1) l.append(element2) return Mult(l) + + + def substituteRHS(self, lineNum1, lineNum2): + """ + Given a representation of a mult object, replace all instances of it in one equation + :param lineNum1: Line to substitute into + :param lineNum2: Line with substitutsion of x = y, will replace all instances of x with y in lineNum1 + """ + ev1 = self.steps[lineNum1] + ev2 = self.steps[lineNum2] + if isinstance(ev1, Eq): + if isinstance(ev2, Eq): + replacement = ev1.replace(ev2.LHS,ev2.RHS) + self.steps += [replacement] + self.justifications += [f'Replaced all instances of {ev2.LHS} with {ev2.RHS} on line {lineNum1}'] + self.show() + else: + print("Cannot substitute without an Equation") + else: + print("Cannot substitute without an Equation") + + def substituteLHS(self, lineNum1, lineNum2): + """ + Given a representation of a mult object, replace all instances of it in one equation + :param lineNum1: Line to substitute into + :param lineNum2: Line with substitutsion of y = x, will replace all instances of y with x in lineNum1 + """ + ev1 = self.steps[lineNum1] + ev2 = self.steps[lineNum2] + if isinstance(ev1, Eq): + if isinstance(ev2, Eq): + replacement = ev1.replace(ev2.RHS,ev2.LHS) + self.steps += [replacement] + self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}'] + self.show() + else: + print("Cannot substitute without an Equation") + else: + print("Cannot substitute without an Equation") def modus(self, lineNum1, lineNum2): """ modus pones: given A->B and A, the function concludes B and add it as a new line in the proof - lineNum1 and lineNum2: one line in the proof where the person showed A->B and one line the proof where the person showed A + :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] @@ -87,42 +140,6 @@ def modus(self, lineNum1, lineNum2): else: print (f"Neither of {str(lineNum1)}, {str(lineNum2)} are an implies statement") - def identElimRHS(self, lineNum): - """" - Remove all instances of the identity from an equation - :param lineNum: the line of the proof to be modified on the right hand side - """ - evidence = copy.deepcopy(self.steps[lineNum]) - rhsevidence = evidence.RHS - if isinstance(rhsevidence,Mult): - l = copy.deepcopy(rhsevidence.prodcuts) - try: - while True: - l.remove(evidence.parentgroup.identity_identifier) - except ValueError: - pass - return Mult(l) - else: - print (f"The right hand side on line {lineNum} is not a Mult object") - - def identElimLHS(self, lineNum): - """" - Remove all instances of the identity from an equation - :param lineNum: the line of the proof to be modified on the left hand side - """ - evidence = copy.deepcopy(self.steps[lineNum]) - lhsevidence = evidence.LHS - if isinstance(lhsevidence,Mult): - l = copy.deepcopy(lhsevidence.prodcuts) - try: - while True: - l.remove(evidence.parentgroup.identity_identifier) - except ValueError: - pass - return Mult(l) - else: - print (f"The left hand side on line {lineNum} is not a Mult object") - def inverseElimRHS(self,lineNum): """ finds the first pair of group element and its inverse and returns the group element @@ -147,6 +164,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() @@ -175,6 +193,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() @@ -189,11 +208,12 @@ def forallElim(self, lineNum, replacements): """ evidence = copy.deepcopy(self.steps[lineNum]) if isinstance(evidence, forall) == False: - raise Exception(f"There is no forall statmenent on line {lineNum}") - evidence.replace(replacements) - self.steps += [evidence.expr] - self.justifications += [f'For all elimination on line {lineNum}'] - self.show() + print(f"There is no forall statmenent on line {lineNum}") + else: + expr = evidence.replace(replacements) + self.steps += [expr] + self.justifications += [f'For all elimination on line {lineNum}'] + self.show() def thereexistsElim(self, lineNum, replacements): # We can only do this once! """ @@ -203,11 +223,12 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once! """ evidence = copy.deepcopy(self.steps[lineNum]) if isinstance(evidence, thereexists) == False: - raise Exception(f"There is no there exists statmenent on line {lineNum}") - evidence.replace(replacements) - self.steps += [evidence.expr] - self.justifications += [f'There exists elimination on line {lineNum}'] - self.show() + print(f"There is no there exists statmenent on line {lineNum}") + else: + expr = evidence.replace(replacements) + self.steps += [expr] + self.justifications += [f'There exists elimination on line {lineNum}'] + self.show() ## Multiplication manipulation def leftMult (self, elem, lineNum): @@ -219,6 +240,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] @@ -234,6 +256,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] @@ -265,6 +288,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'] @@ -279,7 +303,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) @@ -298,7 +323,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) @@ -322,6 +348,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): """ @@ -337,6 +364,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): """ @@ -361,6 +389,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) @@ -374,7 +403,7 @@ def identright(self, lineNum): :param lineNum: the line of the proof to be modified """ evidence = self.steps[lineNum] - if isinstance(evidence,Eq) and isinstance(evidence.arg2, Mult): + if isinstance(evidence,Eq): l = evidence.RHS.products l1=[] for i in range(len(l)-1): @@ -391,6 +420,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) @@ -403,6 +433,7 @@ def introReflexive(self,eq): 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] @@ -412,7 +443,9 @@ def introReflexive(self,eq): print ("this is not reflexive") def reduceLogic(self, lineNum): - """Recursively reduces a ND statement by pushing the nots in + """ + Recursively reduces a ND statement by pushing in the nots + :param lineNum: the line of the proof to be modified """ evidence = self.steps[lineNum] if type(lineNum) in [And, Or, Implies, Not]: @@ -423,7 +456,9 @@ def reduceLogic(self, lineNum): print ("this is not a logic statement") def introCases(self, case): - """Introduction of cases (law of excluded middle) + """ + Introduction of cases (law of excluded middle) + :param case: the equation/logical statement of one case (the other is a not of that) """ case1 = case case2 = reduce(Not(case)) @@ -432,8 +467,11 @@ def introCases(self, case): self.show() def introSubproof(self, assum): - """This one returns so the user has access to the new subproof + """ + WIP + This one returns so the user has access to the new subproof 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] @@ -441,8 +479,68 @@ def introSubproof(self, assum): return subproof def concludeSubproof(self, lineNum): - """You conclude a subproof from the parent subproof + """ + WIP + You conclude a subproof from the parent subproof 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 + + def introElement(self,G, name): + """ + Introduces an arbitrary element in G + Can be used as evidence for a forall introduction + :param G: the group the elemen is in + :param name: the name of the new element + """ + if G.contains(name): + print(f"{name} is already in {G}") + else: + self.env[name] = G.newElement(name) + self.steps += [In(name, G)] + self.justifications += ["Introducing an arbitrary element"] + self.show() + + def forAllIntroduction(self, equationLine, vars, elemIntroLines): + ''' + Creates a for all from an equation with arbitrary variables + :param equationLine: the equation + :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 + #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] + 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"] + self.show() + + def closure(self,G,a,b): + ''' + Introduces ab as an element of G by closure + :param G: the group a,b are in + :param a: element a + :param b: element b + ''' + if G.contains(a) and G.contains(b): + G.mulElements(a,b) + self.steps+=[In(G,Mult([a,b]))] + self.justifications+=["Closure"] + self.show() + else: + if not G.contains(a): + print(f"{a} is not in {G}") + else: + print(f"{b} is not in {G}") diff --git a/proofs/proof1.py b/proofs/proof1.py deleted file mode 100644 index e69de29..0000000