Split QED into QED and for all introduction. Made introducing element…

…s a proof step (still uses group class).

abelian_proof.py

@@ -1,6 +1,5 @@
 from proof import *
 from element import *
-from environment import *
 from group import *
 from integer import *
 from logicObjects import *
@@ -9,18 +8,22 @@
 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)
 p.introGroup(G)
-G.newElement('a')
-G.newElement('b')
-G.mulElements('a','b')
+#G.newElement('a')
+#G.newElement('b')
+#G.mulElements('a','b')
+p.introElement(G,'a')
+p.introElement(G,'b')
+p.closure(G,'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.qed(['b','a'],11)
+p.forallElim(4,['a * b'])
+p.leftMult(G.elements['a'],5)
+p.forallElim(4,['a'])
+p.substituteRHS(6,7)
+p.identleft(8)
+p.identright(9)
+p.rightMult(G.elements['b'],10)
+p.forallElim(4,['b'])
+p.substituteRHS(11,12)
+p.identleft(13)
+p.forAllIntroduction(14,["a","b"],[1,2])
+p.qed(15)

logicObjects.py

@@ -82,6 +82,14 @@ class Bottom:
     def elim(self, conclusion):
         return conclusion
 
+class In:
+    def __init__(self, elem, grp):
+        self.elem = elem
+        self.grp = grp
+
+    def __repr__(self):
+        return str(self.elem) + " ∈ " + str(self.grp)
+
 class Eq:
     def __init__(self,LHS,RHS,pg):
         self.LHS = LHS
@@ -131,18 +139,28 @@ def __repr__(self):
         return 'forall(' + str(self.arbelems) + ' in ' + str(self.group) + ', ' + str(self.eq) +')'
 
     def __eq__(self,other):
-        return self.arbelems == other.arbelems and self.group == other.group and self.eq == other.eq
+        if not isinstance(other,forall):
+            return False
+        if len(self.arbelems)==len(other.arbelems):
+            print(self,other)
+            new = copy.deepcopy(self)
+            replaced = new.replace(other.arbelems)
+            return replaced == other.eq
+        else:
+            return False
 
 
     def replace(self, replacements): # replacements = ['x','y'] - strings of the elements
         if len(replacements) == len(self.arbelems):
-            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(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}")
+            #if all(elem in self.group.elements for elem in replacements): # check if replacements are all normal elements of self.group
+            #The scope of thee elements in a for all should be contained in that for all
+            #Checking if in the group should happen at elimination and introduction
+            neweq = copy.deepcopy(self.eq)
+            for i in range(len(replacements)):
+                 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}")
         else:
             print("Replacements is not the same length as the list of arbitrary elements")
 

proof.py

@@ -1,5 +1,5 @@
+from re import L
 from element import *
-from environment import *
 from group import *
 from integer import *
 from logicObjects import *
@@ -12,21 +12,17 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []):
         self.goal = goal # this is an implies
         self.steps = []
         self.justifications = []
-        self.environment = {} # add strings names to environment for parsing 
+        self.env = {}
         self.depth = 0
-        # self.currAssumption = [goal.assum] # is this neccessary?
-        self.show() 
 
-    def qed(self, replacements, lineNum):
-        if isinstance(self.goal, forall): # how do I know a line is a replacement of a forall?
-            if self.goal.replace(replacements) == self.steps[lineNum]: # how do I know replacement variables are all arbitrarily introduced?
-                self.steps += [True]
-                self.justifications += [f"Proof is finished by line {lineNum}"]
-                self.show()
-            else:
-                print("Hmm, that line doesn't seem to prove what you think it does. Is there another line you meant? You may have also replaced incorrectly.")
-        else:    
-            return self.goal.conc in self.steps
+    def qed(self, lineNum):
+        print(self.goal, self.steps[lineNum])
+        if self.goal == self.steps[lineNum]:
+            self.steps+=["□"]
+            self.justifications += ["QED"]
+            self.show()
+        else:
+            print("This is not the same as the goal")
 
     def undo(self):
         self.steps = self.steps[:-1]
@@ -50,7 +46,7 @@ def introGroup(self, grp):
         self.steps += [grp]
         self.justifications += ["introGroup"]
         #deal with environments
-        self.environment[grp.groupName] = grp
+        self.env[grp.groupName] = grp
         self.show()
 
     def accessAssumption(self):
@@ -461,3 +457,31 @@ def concludeSubproof(self, lineNum):
         """
         conc = Implies(self.assumption, self.steps[lineNum])
         return conc
+
+    def introElement(self,G, name):
+        self.env[name] = G.newElement(name)
+        self.steps += [In(name, G)]
+        self.justifications += ["Introducing an arbitrary element"]
+        self.show()
+
+    def forAllIntroduction(self, equationLine, vars, elemIntroLines):
+        evidence = copy.deepcopy(self.steps[equationLine])
+        G = self.steps[elemIntroLines[0]].grp
+        #Checking that the lines introduce the arbitrary variables, and that the variables are all in the same group
+        for i in range(len(vars)):
+            v = vars[i]
+            l = elemIntroLines[i]
+            if self.steps[l].elem!=vars[i]:
+                print("Line", l, "does not introduce variable", v)
+            if self.steps[l].grp!=G:
+                print("Element", v, "is not in group", G)
+        #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"]
+        self.show()
+
+    def closure(self,G,a,b):
+        G.mulElements(a,b)
+        self.steps+=[In(G,Mult([a,b]))]
+        self.justifications+=["Closure"]
+        self.show()