First subgroup proof!

abelian_proof.py

@@ -24,4 +24,4 @@
 p.substituteRHS(11,12)
 p.identleft(13)
 p.forAllIntroduction(14,["a","b"],[1,2])
-p.qed(15)
+p.qed(15)

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
+        return self.groupName

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:

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

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)

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