consistency changes

abelian_proof.py

@@ -14,12 +14,12 @@
 p.closure(G,'a','b')
 p.accessAssumption()
 p.forallElim(4,['a * b'])
-p.leftMult(G.elements['a'],5) # G.elements should be a function not a dictionary
+p.leftMult('a',5) # G.elements should be a function not a dictionary
 p.forallElim(4,['a'])
 p.substituteRHS(6,7)
 p.identleft(8)
 p.identright(9)
-p.rightMult(G.elements['b'],10)
+p.rightMult('b',10)
 p.forallElim(4,['b'])
 p.substituteRHS(11,12)
 p.identleft(13)

logicObjects.py

@@ -123,9 +123,9 @@ def __repr__(self):
         return str(self.LHS) + ' = ' + str(self.RHS)
 
     def __eq__(self,other):
-        if self.LHS == other.LHS and self.RHS == other.RHS:
+        if self.LHS == other.LHS and self.RHS == other.RHS and self.group == other.group:
             return True 
-        elif self.LHS == other.RHS and self.RHS == other.LHS: # a=b is the same as b=a
+        elif self.LHS == other.RHS and self.RHS == other.LHS and self.group == other.group: # a=b is the same as b=a
             return True 
         else: 
             return False
@@ -211,7 +211,7 @@ def replace(self, replacements):
         else:
             print("Replacements is not the same length as the list of existential elements")
 
-## Unique class
+## Unique class - idk if we need this
 
 class uniqueElementProperty:
     def __init__ (self, prpty, pg):
@@ -239,3 +239,5 @@ def __init__(self, elementName, pg):
         rhs = Mult([pg.identity_identifier])
         inverseEq = Eq(lhs,rhs,pg)
         pg.addGroupProperty(inverseEq, "Inverse of " + elementName)
+
+## TO DO: class generator(element):

proof.py

@@ -102,9 +102,9 @@ def substituteRHS(self, lineNum1, lineNum2):
                 self.justifications += [f'Replaced all instances of {ev2.LHS} with {ev2.RHS} on line {lineNum1}']
                 self.show()
             else:
-                print("Cannot substitute without an Equation")
+                print(f"The statement on line {lineNum2} is not an equality, substitutition is not possible")
         else:
-            print("Cannot substitute without an Equation")
+            print(f"The statement on line {lineNum1} is not an equality, substitutition is not possible")
 
     def substituteLHS(self, lineNum1, lineNum2):
         """
@@ -121,37 +121,40 @@ def substituteLHS(self, lineNum1, lineNum2):
                 self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}']
                 self.show()
             else:
-                print("Cannot substitute without an Equation")
+                print(f"The statement on line {lineNum2} is not an equality, substitutition is not possible")
         else:
-            print("Cannot substitute without an Equation")
+            print(f"The statement on line {lineNum1} is not an equality, substitutition is not possible")
 
     def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think)
         """
         modus pones: given A->B and A, the function concludes B and add it as a new line in the proof
         :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 = []
-        for line in lineNums:
-            ev2 += self.steps[line]
-        if isinstance(ev1, Implies): 
-            A = ev1.assum
-            B = ev1.conc
-            if A == ev2: 
-                self.steps += [B]
-                self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] 
-                self.show() 
+        if isinstance(lineNums, list):
+            ev2 = []
+            for line in lineNums:
+                ev2 += self.steps[line]
+            if isinstance(ev1, Implies): 
+                A = ev1.assum
+                B = ev1.conc
+                if A == ev2: 
+                    self.steps += [B]
+                    self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] 
+                    self.show() 
+            else:
+                print (f"Line {str(lineNum1)} is not an implies statement")
         else:
-            print (f"Line {str(lineNum1)} is not an implies statement")
+            print("The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list")
 
     def inverseElimRHS(self,lineNum):
         """
         finds the first pair of group element and its inverse and returns the group element
         :param lineNum: the line of the proof to be modified on the right hand side
         """
-        evidence = copy.deepcopy(self.steps[lineNum]).RHS
-        if isinstance(evidence,Mult): 
-            l = evidence.products.copy()
+        evidence = copy.deepcopy(self.steps[lineNum])
+        if isinstance(evidence,Eq): 
+            l = evidence.RHS.products.copy()
             lawApplied = False
             for i in range(len(l)-1):
                 if isinstance(l[i],element) and isinstance(l[i+1],inverse) and (l[i].elementName == l[i+1].elementName):
@@ -169,18 +172,21 @@ def inverseElimRHS(self,lineNum):
             if lawApplied==False:
                 print (f"Inverse laws can't be applied on line {lineNum}")
                 return
-        self.steps += [newProducts]
-        self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] 
-        self.show()
+            self.steps += [newProducts]
+            self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] 
+            self.show()
+        else:
+            print(f"It doesn't seem like line {lineNum} contains an equation")
+
 
     def inverseElimLHS(self,lineNum):
         """
         finds the first pair of group element and its inverse and returns the group element
         :param lineNum: the line of the proof to be modified on the left hand side
         """
-        evidence = copy.deepcopy(self.steps[lineNum]).LHS
-        if isinstance(evidence,Mult): 
-            l = evidence.products.copy()
+        evidence = copy.deepcopy(self.steps[lineNum])
+        if isinstance(evidence,Eq): 
+            l = evidence.LHS.products.copy()
             lawApplied = False
             for i in range(len(l)-1):
                 if isinstance(l[i],element) and isinstance(l[i+1],inverse) and (l[i].elementName == l[i+1].elementName):
@@ -198,9 +204,11 @@ def inverseElimLHS(self,lineNum):
             if lawApplied==False:
                 print (f"Inverse laws can't be applied on line {lineNum}")
                 return
-        self.steps += [newProducts]
-        self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] 
-        self.show()
+            self.steps += [newProducts]
+            self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] 
+            self.show()
+        else:
+            print(f"It doesn't seem like line {lineNum} contains an equation")
 
     ## For all and there exists elimination
 
@@ -235,38 +243,45 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once!
             self.show() 
 
     ## Multiplication manipulation
-    def leftMult (self, elem, lineNum):
+    def leftMult(self, elemName, lineNum):
         """
         Left Multiply both sides of an equation with the input element 
         :param lineNum: the equation in the proof that is to be modified 
-        :param elem: the element to left Multiply with 
+        :param elemName: the name of the element to left Multiply with 
         """
         eq = copy.deepcopy(self.steps[lineNum])
-        if isinstance(eq, Eq) == False:
+        if isinstance(eq, Eq): 
+            if elemName in eq.group.elements:
+                elem = eq.group.elements[elemName]
+                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.show()
+            else:
+                print("The element " + elemName + " is not in the group " + eq.group)
+        else:
             print (f"Line {lineNum} is not an equation")
-            return
-        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.show()
 
-    def rightMult (self, elem, lineNum):
+    def rightMult (self, elemName, lineNum):
         """
         Right Multiply both sides of an equation with the input element 
         :param lineNum: the line in the proof that is to be modified 
-        :param elem: the element to right Multiply 
+        :param elemName: the name of the element to right Multiply with
         """
         eq = copy.deepcopy(self.steps[lineNum])
-        if isinstance(eq, Eq) == False:
+        if isinstance(eq, Eq):
+            if elemName in eq.group.elements:
+                elem = eq.group.elements[elemName]
+                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.show()
+            else:
+                print("The element " + elemName + " is not in the group " + eq.group)
+        else:
             print (f"Line {lineNum} is not an equation")
-            return
-        product = self.MultElem(eq.LHS, elem)
-        result = Eq(product, self.MultElem(eq.RHS,elem), eq.group)
-        self.steps += [result]
-        self.justifications += [f'Right multiply line {lineNum} by ' +str(elem)] 
-        self.show()
-
     ##power methods 
     def breakPower(self,input):
         """