From b4672e875f1bae19cccbde083d755b7fc2f71ca4 Mon Sep 17 00:00:00 2001 From: Isaac Date: Mon, 31 Oct 2022 13:49:45 -0700 Subject: [PATCH] Second subgroup proof --- group.py | 8 ++- logicObjects.py | 2 +- proof.py | 115 ++++++++++++++++++++++++++++++++++++++----- sub_group_proof_2.py | 22 +++++++++ 4 files changed, 132 insertions(+), 15 deletions(-) create mode 100644 sub_group_proof_2.py diff --git a/group.py b/group.py index f21ddf0..50699f3 100644 --- a/group.py +++ b/group.py @@ -1,5 +1,5 @@ exec(compile(source=open('element.py').read(), filename='element.py', mode='exec')) -from logicObjects import identity, Mult +from logicObjects import identity, Mult, inverse class group: @@ -31,6 +31,12 @@ def __mul__(self,other): # group cartesian product. Worry about this later return group(newName, [self.binaryOperator,other.binaryOperator], newProperties) # group functions + def newInverse(self, elementName): + if elementName in self.elements: + inverseName = '(' + elementName + ')^(-1)' + self.elements.update({inverseName:inverse(elementName,self)}) + else: + print("Sorry, you cannot add the inverse of an element that does not exist!") # declare new element in group with elementName def newElement(self,elementName): diff --git a/logicObjects.py b/logicObjects.py index 58900ff..0440b52 100644 --- a/logicObjects.py +++ b/logicObjects.py @@ -265,7 +265,7 @@ def __init__(self, pg): class inverse(element): def __init__(self, elementName, pg): - inverseName = elementName + "^(-1)" + inverseName = '(' + elementName + ")^(-1)" super().__init__(inverseName, pg) lhs = Mult([inverseName,elementName]) # self or elementName? rhs = Mult([pg.identity_identifier]) diff --git a/proof.py b/proof.py index 5248d4d..7c986c0 100644 --- a/proof.py +++ b/proof.py @@ -115,7 +115,7 @@ def introSet(self, setName, grp, property): 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.justifications += [f'Introduced set {setName} in {grp}'] self.show() else: if setName in self.env['sets']: @@ -125,8 +125,38 @@ def introSet(self, setName, grp, property): self.env['setProperty'][setName] = [grp,property] self.env['setElements'][setName] = [] self.steps += [setName] - self.justifications += [f'Introduced set {setName} in group {grp}'] + self.justifications += [f'Introduced set {setName} in {grp}'] self.show() + + def addElemToSet(self, setName, elementName, grp): + """" + Given a set, and a grp it belongs to, introduce element from that group into the set + :param setName: name of set to take add element to + :param elementName: name of the element + :param grp: grp that contains the element + """ + if 'sets' in self.env: + if setName in self.env['sets']: + if elementName not in self.env['setElements'][setName]: + if grp.contains(elementName): + if isinstance(self.env['setProperty'][setName][1],In): + if self.env['setProperty'][setName][0] == grp: + elemDeclaration = In(elementName, grp) + self.env['setElements'][setName].append(elementName) + self.steps += [elemDeclaration] + self.justifications += [f'Added element {elementName} to set {setName}'] + self.show() + else: + messagebox.showerror('Proof Error', f'Set {setName} is in a different group than {grp}') + else: + messagebox.showerror('Proof Error', f"{elementName} is not in {grp}") + 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 getArbElem(self, setName, elementName): """" @@ -141,7 +171,10 @@ def getArbElem(self, setName, elementName): 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) + if isinstance(self.env['setProperty'][setName][1],In): + elemDeclaration = In(elementName, pg) + elif isinstance(self.env['setProperty'][setName][1],Eq): + 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() @@ -154,6 +187,30 @@ def getArbElem(self, setName, elementName): else: messagebox.showerror("You haven't defined any sets yet!") + def getSpecificElem(self, setName, elementName): + """" + Given a set, select an specific element and put it on it's own line + :param setName: name of set to take element from + :param elementName: name of the specific 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 pg.contains(elementName): + self.env['setElements'][setName].append(elementName) + self.steps += [Eq(elementName,pg.elements[elementName],pg)] + self.justifications += [f'Introduced element {elementName} in set {setName}'] + self.show() + else: + messagebox.showerror('Proof Error', f"{elementName} is not 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 @@ -185,17 +242,28 @@ def setClosure(self, setName, arbIntros, closure): ev = self.steps[closure] if setName in self.env['sets']: if len(arbIntros) == 2: + arb1 = self.steps[arbIntros[0]] + arb2 = self.steps[arbIntros[1]] 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') + if arb1.LHS in self.env['setElements'][setName] and arb2.LHS in self.env['setElements'][setName]: + if isinstance(self.env['setProperty'][setName][1],Eq): + if len(ev.LHS.products) == 2 and arb1.LHS in ev.LHS.products and arb2.LHS in ev.LHS.products: + 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') + elif isinstance(ev,In): + if isinstance(self.env['setProperty'][setName][1],In): + if len(ev.elem.products) == 2 and arb1.elem in ev.elem.products and arb2.elem in ev.elem.products and ev.group == arb1.group and ev.group == arb2.group: + 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: @@ -239,7 +307,8 @@ def setInverse(self, setName, lineNum): 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 str(el1) in self.env['setElements'][setName] and str(el2) in self.env['setElements'][setName]: + print(type(ev.RHS.products[0]),type(self.env['setProperty'][setName][0].elements['e'].products[0])) 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'] @@ -294,6 +363,26 @@ def MultElem(self, e1, e2): l.append(element2) return Mult(l) + def introInverse(self, G, name): + if isinstance(name,str): + if not G.contains(name): + print('Proof Error', f"{name} is not defined") + return + else: + for x in name.products: + if not G.contains(x): + print('Proof Error', f"{x} is not defined") + return + if isinstance(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_) + G.newInverse(name) + rhs = G.elements["e"] + self.steps += [Eq(lhs,rhs,G)] + self.justifications += ["Introducing the inverse of an element"] + self.show() def substituteRHS(self, lineNum1, lineNum2): """ diff --git a/sub_group_proof_2.py b/sub_group_proof_2.py new file mode 100644 index 0000000..5adeaea --- /dev/null +++ b/sub_group_proof_2.py @@ -0,0 +1,22 @@ +from proof import * +from element import * +from group import * +from integer import * +from logicObjects import * + +G = group('G','*') +subGroupG = G.subGroup(In('x',G)) +p = Proof('Simple Subgroup Proof', None, goal=subGroupG) +p.introGroup(G) +p.introSet('S',G,In('x',G)) +p.getSpecificElem('S','e') +p.setContainsIdentity('S',2) +p.getArbElem('S','a') +p.getArbElem('S','b') +p.closure(G,'a','b') +p.setClosure('S',[4,5],6) +p.introInverse(G,'a') +p.addElemToSet('S','(a)^(-1)',G) +p.setInverse('S',8) +p.concludeSubgroup('S') +p.qed(11)