Merge pull request #2 from isahers1/Isaac-Subgroup

Isaac subgroup

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):

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])

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):
         """

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)