Merge branch 'main' of https://github.com/isahers1/global-environment

abelian_proof.py

@@ -4,6 +4,7 @@
 from integer import *
 from logicObjects import *
 
+
 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']), G.elements['e'],G)), goal=abelianG)

proof.py

@@ -16,7 +16,6 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []):
         self.depth = 0
 
     def qed(self, lineNum):
-        print(self.goal, self.steps[lineNum])
         if self.goal == self.steps[lineNum]:
             self.steps+=["□"]
             self.justifications += ["QED"]
@@ -42,6 +41,15 @@ def introAssumption(self, expr):
         self.justifications += ['introAssumption'] 
         self.show()
 
+    def introGroup(self, groupName):
+        self.steps += [group(groupName)]
+        self.justifications += ["introGroup"]
+        self.show()
+
+    def introGroupElement(self, elementName, groupName):
+        self.steps += [groupElement(elementName, groupName)]
+        self.justifications += ['introGroupElement']
+        default = {"in":[groupName], "prop":[]}
     def introGroup(self, grp):
         self.steps += [grp]
         self.justifications += ["introGroup"]
@@ -156,6 +164,7 @@ def inverseElimRHS(self,lineNum):
                     break
             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()
@@ -184,6 +193,7 @@ def inverseElimLHS(self,lineNum):
                     break
             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()
@@ -230,6 +240,7 @@ def leftMult (self, elem, lineNum):
         eq = copy.deepcopy(self.steps[lineNum])
         if isinstance(eq, Eq) == False:
             print (f"Line {lineNum} is not an equation")
+            return
         product = self.MultElem(elem, eq.LHS)
         result = Eq(product, self.MultElem(elem,eq.RHS), eq.parentgroup)
         self.steps += [result]
@@ -245,6 +256,7 @@ def rightMult (self, elem, lineNum):
         eq = copy.deepcopy(self.steps[lineNum])
         if isinstance(eq, Eq) == False:
             print (f"Line {lineNum} is not an equation")
+            return
         product = self.MultElem(eq.LHS, elem)
         result = Eq(product, self.MultElem(eq.RHS,elem), eq.parentgroup)
         self.steps += [result]
@@ -276,6 +288,7 @@ def combinePower(self, mult):
         for i in multList: 
             if i != e: 
                 print ("Need a single element but given multiple")
+                return
         result=power(e,len(multList)) 
         self.steps += [result]
         self.justifications += ['Convert multiplications to equivalent powers'] 
@@ -290,7 +303,8 @@ def splitPowerAddition(self,power):
         exp=self.exponent
         l=exp.split("+")
         if len(l)==1:
-            print ("No power addition to be split apart") 
+            print ("No power addition to be split apart")
+            return
         multList=[]
         for i in l: 
             elem=power(element,i)
@@ -309,7 +323,8 @@ def splitPowerMult(self,power):
         exp=self.exponent
         l=exp.split("*")
         if len(l)==1:
-            print ("No power multiplication to be split apart") 
+            print ("No power multiplication to be split apart")
+            return
         elem=element
         for i in l: 
             e=power(elem,i)
@@ -333,6 +348,7 @@ def rightSidesEq(self, lineNum1, lineNum2):
             self.show()
         else:
             print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides")
+            return
 
     def leftSidesEq(self, lineNum1, lineNum2):
         """
@@ -348,6 +364,7 @@ def leftSidesEq(self, lineNum1, lineNum2):
             self.show()
         else:
             print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides")
+            return
 
     def identleft(self, lineNum):
         """
@@ -372,6 +389,7 @@ def identleft(self, lineNum):
                 # else we can't apply identity elimination 
             if l1==[]:
                 print ("identity can't be applied")
+                return
             newProduct = Mult(l1)
             ret = Eq(newProduct,evidence.RHS,evidence.parentgroup)
 
@@ -402,6 +420,7 @@ def identright(self, lineNum):
                 # else we can't apply identity elimination 
             if l1==[]:
                 print ("identity can't be applied")
+                return
             newProduct = Mult(l1)
             ret = Eq(evidence.LHS,newProduct,evidence.parentgroup)
 
@@ -499,8 +518,10 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines):
             l = elemIntroLines[i]
             if self.steps[l].elem!=vars[i]:
                 print("Line", l, "does not introduce variable", v)
+                return
             if self.steps[l].grp!=G:
                 print("Element", v, "is not in group", G)
+                return
         #If you make it here, this is a valid for all intro
         self.steps+=[forall(vars,G,self.steps[equationLine])]
         self.justifications+=["For all introduction"]