From dd7f689183f83f394266c6bd038e17b9bc27cee7 Mon Sep 17 00:00:00 2001 From: Isaac Date: Tue, 18 Oct 2022 13:29:26 -0700 Subject: [PATCH] First subgroup proof! --- abelian_proof.py | 2 +- group.py | 7 +- logicObjects.py | 2 + proof.py | 175 +++++++++++++++++++++++++++++++++++++++++++-- sub_group_proof.py | 20 ++++++ unique inverses.py | 5 +- 6 files changed, 201 insertions(+), 10 deletions(-) create mode 100644 sub_group_proof.py diff --git a/abelian_proof.py b/abelian_proof.py index 043d56a..2ff40c0 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -24,4 +24,4 @@ p.substituteRHS(11,12) p.identleft(13) p.forAllIntroduction(14,["a","b"],[1,2]) -p.qed(15) \ No newline at end of file +p.qed(15) diff --git a/group.py b/group.py index ba15fb6..f21ddf0 100644 --- a/group.py +++ b/group.py @@ -8,6 +8,7 @@ class group: elements = {} groupProperties = {} elementProperties = {} + subGroups = [] binaryOperator = "" groupName = "" @@ -50,6 +51,10 @@ def mulElements(self, elem1, elem2): # should this return an equation? 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 subGroup(self, property): + self.subGroups.append(property) + return f'{property} is a subgroup of {self}' def addGroupProperty(self, property, propertyName): self.groupProperties[propertyName] = property @@ -67,4 +72,4 @@ def contains(self, elementName): return elementName in self.elements def toLaTeX(self): - return self.groupName \ No newline at end of file + return self.groupName diff --git a/logicObjects.py b/logicObjects.py index d9ab9f9..58900ff 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -241,6 +241,8 @@ def replace(self, replacements): def toLaTeX(self): return r"\exists " + ",".join(self.existelems) + r" \in " + str(self.group) + r"\ " + self.toLaTeX(self.eq) + + ## Unique class - idk if we need this class uniqueElementProperty: diff --git a/proof.py b/proof.py index 5a26adb..5248d4d 100644 --- a/proof.py +++ b/proof.py @@ -1,3 +1,4 @@ +from email import message from re import L from element import * @@ -21,8 +22,6 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = [], self.subproof = None def qed(self, lineNum): - print(self.goal, self.steps[lineNum]) - if self.goal == self.steps[lineNum]: self.steps+=["□"] self.justifications += ["QED"] @@ -110,12 +109,177 @@ def introGroup(self, grp): self.env[grp.groupName] = grp self.show() + def introSet(self, setName, grp, property): + if 'sets' not in self.env: + self.env['sets'] = [setName] + self.env['setProperty'] = {setName:[grp,property]} + self.env['setElements'] = {setName:[]} + self.steps += [f'{setName} with property {property}'] + self.justifications += [f'Introduced set {setName} in group {grp}'] + self.show() + else: + if setName in self.env['sets']: + messagebox.showerror("A set with this name already exists, maybe try another name?") + else: + self.env['sets'].append(setName) + self.env['setProperty'][setName] = [grp,property] + self.env['setElements'][setName] = [] + self.steps += [setName] + self.justifications += [f'Introduced set {setName} in group {grp}'] + self.show() + + def getArbElem(self, setName, elementName): + """" + Given a set, select an arbitrary element and put it on it's own line + :param setName: name of set to take element from + :param elementName: name of the arbitrary element + """ + if 'sets' in self.env: + if setName in self.env['sets']: + if elementName not in self.env['setElements'][setName]: + pg = self.env['setProperty'][setName][0] + if not pg.contains(elementName): + self.env[elementName] = pg.newElement(elementName) + self.env['setElements'][setName].append(elementName) + elemDeclaration = Eq(elementName,self.env['setProperty'][setName][1].RHS,pg) + self.steps += [elemDeclaration] + self.justifications += [f'Introduced arbitrary element {elementName} in set {setName}'] + self.show() + else: + messagebox.showerror('Proof Error', f"{elementName} is already in {pg}") + else: + messagebox.showerror("You have already defined an element in this set with that name, maybe try another name?") + else: + messagebox.showerror("You haven't defined a set with that name yet!") + else: + messagebox.showerror("You haven't defined any sets yet!") + + def multBothSides(self, lineNum1, lineNum2): + """ + Given two lines multiply the left hand sides together and the right hand sides together + :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) and ev1.group == ev2.group: + LHSproduct = self.MultElem(ev1.LHS, ev2.LHS) + RHSproduct = self.MultElem(ev1.RHS, ev2.RHS) + result = Eq(LHSproduct, RHSproduct, ev1.group) + self.steps += [result] + self.justifications += [f'Multiplied line {lineNum1} by line {lineNum2}'] + self.show() + else: + messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, multiplication is not possible") + else: + messagebox.showerror('Proof Error',f"The statement on line {lineNum1} is not an equality, multiplication is not possible") + + def setClosure(self, setName, arbIntros, closure): + """ + Given a set, two arbitrary elements, and their multiplication, confirm that the set is closed + :param setName: Name of set we are trying to prove closure for + :param arbIntros: List of lineNums which contain the arbitrary element intros. + :param closure: Line where multiplication of arbitrary elements is on LHS and RHS is an element of set + """ + ev = self.steps[closure] + if setName in self.env['sets']: + if len(arbIntros) == 2: + if isinstance(ev, Eq): + arb1 = self.steps[arbIntros[0]] + arb2 = self.steps[arbIntros[1]] + # check that lines are intros? + if arb1.LHS in self.env['setElements'][setName] and arb2.LHS in self.env['setElements'][setName] and ev.RHS == self.env['setProperty'][setName][1].RHS: + self.env['setProperty'][setName].append('Closure') + self.steps += [f'Set {setName} is closed'] + self.justifications += [f'Introduction on lines {arbIntros[0]},{arbIntros[1]} and closure on line {closure}'] + self.show() + else: + messagebox.showerror('Proof error',f'These lines do not prove closure, double check you typed everythin in correctly') + else: + messagebox.showerror('Proof error',f'Line proving closure must be an equation of the form a*b=c where a,b are arbitrary elements of set {setName} and c is in set {setName}') + else: + messagebox.showerror('Proof error',f"To prove closure you need 2 arbitrary elements, but you did not pass 2 line numbers") + else: + messagebox.showerror('Proof error',f'Set {setName} does not exist, did you type the name wrong?') + + def setContainsIdentity(self, setName, lineNum): + """ + Given a set, verify there exists an element equal to the identity + :param setName: Name of set we are trying to show contains the identity + :param lineNum: Line whith left hand side equal to element in set, right hand side is identity + """ + ev = self.steps[lineNum] + if setName in self.env['sets']: + if isinstance(ev, Eq): + if ev.LHS in self.env['setElements'][setName]: + if self.env['setProperty'][setName][0].elements['e'].products == ev.RHS.products: + self.env['setProperty'][setName].append('Identity') + self.steps += [f'Set {setName} contains the identity'] + self.justifications += [f'Identity equal to element of set {setName} on line {lineNum}'] + self.show() + else: + messagebox.showerror('Proof error', f'Right hand side of line {lineNum} is not the identity') + else: + messagebox.showerror('Proof error', f'Left hand side of line {lineNum} is not element of set {setName}') + else: + messagebox.showerror('Proof error',f'Line proving identity is in set must be an equation') + else: + messagebox.showerror('Proof error',f'Set {setName} does not exist, did you type the name wrong?') + + def setInverse(self, setName, lineNum): + """ + Given a set, verify that inverse exists for arbitrary element + :param setName: Name of set we are trying to show contains inverses + :param lineNum: Line whith left hand side equal to two elements in set multiplied, right hand side is identity + """ + ev = self.steps[lineNum] + if setName in self.env['sets']: + if isinstance(ev, Eq): + if len(ev.LHS.products) == 2: + el1 = ev.LHS.products[0] + el2 = ev.LHS.products[1] + if el1 in self.env['setElements'][setName] and el2 in self.env['setElements'][setName]: + if self.env['setProperty'][setName][0].elements['e'].products == ev.RHS.products: + self.env['setProperty'][setName].append('Inverses') + self.steps += [f'Set {setName} contains inverses'] + self.justifications += [f'Identity equal to product of two elements of {setName} on line {lineNum}'] + self.show() + else: + messagebox.showerror('Proof error', f'Right hand side of line {lineNum} is not the identity') + else: + messagebox.showerror('Proof error', f'One or more elements of left hand side of line {lineNum} is not element of set {setName}') + else: + messagebox.showerror('Proof error',f'Line {lineNum} does not contain two elements on the right hand side') + else: + messagebox.showerror('Proof error',f'Line proving identity is in set must be an equation') + else: + messagebox.showerror('Proof error',f'Set {setName} does not exist, did you type the name wrong?') + + def concludeSubgroup(self, setName): + """ + Given a set, verify that it is a subgroup + :param setName: Name of set we are trying to show contains inverses + """ + if setName in self.env['sets']: + if 'Closure' in self.env['setProperty'][setName][2:] and 'Identity' in self.env['setProperty'][setName][2:] and 'Inverses' in self.env['setProperty'][setName][2:]: + pg = self.env['setProperty'][setName][0] + self.steps += [pg.subGroup(self.env['setProperty'][setName][1])] + self.justifications += [f'Set {setName} meets all requirements to be a subgroup'] + self.show() + else: + messagebox.showerror('Proof error',f'Set {setName} does not contain all of the requisites for subgroup (Closure,Identity,Inverses)') + else: + messagebox.showerror('Proof error',f'Set {setName} does not exist, did you type the name wrong?') + def accessAssumption(self): self.steps += [self.assumption] self.justifications += ["Accessed Assumption"] self.show() - def MultElem(self, element1, element2): + def MultElem(self, e1, e2): + element1 = copy.deepcopy(e1) + element2 = copy.deepcopy(e2) l=[] if isinstance(element1,Mult) and isinstance(element2, Mult): l=element1.products+element2.products @@ -302,7 +466,7 @@ def leftMult(self, elemName, lineNum): product = self.MultElem(elem, eq.LHS) result = Eq(product, self.MultElem(elem,eq.RHS), eq.group) self.steps += [result] - self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] + 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)) @@ -322,7 +486,7 @@ def rightMult (self, elemName, lineNum): product = self.MultElem(eq.LHS, elem) result = Eq(product, self.MultElem(eq.RHS, elem), eq.group) self.steps += [result] - self.justifications += ['Right multiply line {lineNum} by ' +str(elem) ] + 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)) @@ -618,6 +782,7 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): self.steps+=[forall(vars,G,evidence)] self.justifications+=["For all introduction"] self.show() + break def closure(self,G,a,b): ''' diff --git a/sub_group_proof.py b/sub_group_proof.py new file mode 100644 index 0000000..e9992c4 --- /dev/null +++ b/sub_group_proof.py @@ -0,0 +1,20 @@ +from proof import * +from element import * +from group import * +from integer import * +from logicObjects import * + +G = group('G','*') +subGroupG = G.subGroup(Eq('x',G.elements['e'],G)) +p = Proof('Simple Subgroup Proof', None, goal=subGroupG) +p.introGroup(G) +p.introSet('S',G,Eq('x',G.elements['e'],G)) # change to mult objects? +p.getArbElem('S','a') +p.getArbElem('S','b') +p.multBothSides(2,3) +p.identright(4) +p.setClosure('S',[2,3],5) +p.setContainsIdentity('S',2) +p.setInverse('S',5) +p.concludeSubgroup('S') +p.qed(9) \ No newline at end of file diff --git a/unique inverses.py b/unique inverses.py index 56e31e2..adc28a4 100644 --- a/unique inverses.py +++ b/unique inverses.py @@ -5,7 +5,7 @@ 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) @@ -24,5 +24,4 @@ p2.switchSidesOfEqual(8) p.concludeSubproof(9) p.qed(10) -''' -print(dir(Proof)) +