Abelian proof working except conclusion

abelian_proof.py

@@ -7,25 +7,21 @@
 
 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']), identity('1',G),G)), goal=abelianG)
+p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), G.elements['e'],G)), goal=abelianG)
 p.introGroup(G)
 G.newElement('a')
 G.newElement('b')
+G.mulElements('a','b')
+p.accessAssumption()
+p.forallElim(1,['a * b'])
+p.leftMult(G.elements['a'],2)
+p.forallElim(1,['a'])
+p.substituteRHS(3,4)
+p.identleft(5)
+p.identright(6)
+p.rightMult(G.elements['b'],7)
+p.forallElim(1,['b'])
+p.substituteRHS(8,9)
+p.identleft(10)
 
-"""
-p.introGroup('G')
-p.introGroupElement('a', 'G')
-p.introGroupElement('b', 'G')
-p.closure(3,4)
-p.forallElim(1,[["x",mult(["a","b"])]])
-p.leftmult('a',6)
-p.forallElim(1,[["x", "a"]])
-p.substitution(7,8)
-p.identleft(9)
-p.identright(10)
-p.rightmult('b',11)
-p.forallElim(1,[["x", "b"]])
-p.substitution(12,13)
-p.identleft(14)
-p.abelian(15)
-"""
+## HOW DO WE FINISH THE PROOF?

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

group.py

@@ -1,5 +1,5 @@
 exec(compile(source=open('element.py').read(), filename='element.py', mode='exec'))
-from logicObjects import identity
+from logicObjects import identity, Mult
 
 
 class group:
@@ -14,7 +14,7 @@ class group:
     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)
 
@@ -34,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!")
 
@@ -46,8 +46,8 @@ 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!")
 
@@ -58,4 +58,4 @@ 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!")
+            print("That element doesn't exist!", property, elementName)

logicObjects.py

@@ -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:
@@ -129,7 +139,7 @@ def replace(self, replacements): # replacements = ['x','y'] - strings of the ele
             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
+                    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}")
@@ -163,7 +173,8 @@ def replace(self, replacements):
 ## Special types of elements/groups
 
 class identity(element):
-    def __init__(self, elementName, pg):
+    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)])

proof.py

@@ -44,6 +44,11 @@ def introGroup(self, grp):
         #deal with environments
         self.environment[grp.groupName] = grp
         self.show()
+
+    def accessAssumption(self):
+        self.steps += [self.assumption]
+        self.justifications += ["Accessed Assumption"]
+        self.show()
 
     def MultElem(self, element1, element2):
         l=[]
@@ -59,11 +64,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]
@@ -84,42 +128,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
@@ -186,11 +194,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!
         """
@@ -200,11 +209,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):
@@ -371,7 +381,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):