Merge

abelian_proof.py

@@ -1,12 +1,27 @@
 from proof import *
 from element import *
-from environment import *
 from group import *
 from integer import *
 from logicObjects import *
 
-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.introGroup('G')
-p.introGroupElement('a', 'G')
-p.introGroupElement('b', 'G')
+
+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)
+p.introGroup(G)
+p.introElement(G,'a')
+p.introElement(G,'b')
+p.closure(G,'a','b')
+p.accessAssumption()
+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)

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
@@ -60,24 +63,5 @@ def __init__(self, elementName, pg):
     def fullDescription(self):
         return  "Existential element " + self.elementName + " in group" + self.parentGroups[0].groupName # can only belong to one group
 
-## Special types of elements/groups
-
-class identity(element):
-    def __init__(self, elementName, pg):
-        super().__init__(elementName, pg)
-        lhs = Mult([arbitrary('x',pg),elementName]) # self or elementName?
-        rhs = Mult([arbitrary('x',pg)])
-        eq = Eq(lhs,rhs,pg)
-        idnty = forall([arbitrary('x',pg)], pg, eq)
-        pg.addElementProperty(idnty,elementName)
-
-class inverse(element):
-    def __init__(self, elementName, pg):
-        super().__init__(elementName, pg)
-        lhs = Mult([arbitrary('x',pg),elementName]) # self or elementName?
-        rhs = Mult([arbitrary('x',pg)])
-        eq = Eq(lhs,rhs,pg)
-        idnty = forall([arbitrary('x',pg)], pg, eq)
-        pg.addElementProperty(idnty,elementName)
 
 ## need to add: generator

group.py

@@ -1,17 +1,20 @@
 exec(compile(source=open('element.py').read(), filename='element.py', mode='exec'))
+from logicObjects import identity, Mult
+
 
 class group:
     # TRUTHS for all classes - need to add more here
     identity_identifier = 'e'
     elements = {}
     groupProperties = {} 
+    elementProperties = {}
     binaryOperator = ""
     groupName = ""
 
     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)
 
@@ -31,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!")
 
@@ -43,10 +46,19 @@ 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!")
 
     def addGroupProperty(self, property, propertyName):
-        self.groupProperties[propertyName] = property
+        self.groupProperties[propertyName] = property
+
+    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!", property, elementName)
+
+    def contains(self, elementName):
+        return elementName in self.elements

logicObjects.py

@@ -1,7 +1,7 @@
 import copy
 from dataclasses import replace
 
-from element import arbitrary
+from element import *
 
 class Mult:
     def __init__(self, elemList):
@@ -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:
@@ -72,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
@@ -121,20 +139,30 @@ 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(self.arbelems[i],replacements[i]) # repeatedly replace
-                return neweq
-            else:
-                raise Exception(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:
-            raise Exception("Replacements is not the same length as the list of arbitrary elements")
+            print("Replacements is not the same length as the list of arbitrary elements")
 
 class thereexists:
     def __init__(self, vars, g, eq): # should we check that vars is existential elements?
@@ -156,6 +184,27 @@ def replace(self, replacements):
                     neweq = neweq.replace(self.existelems[i],replacements[i]) # repeatedly replace
                 return neweq
             else:
-                raise Exception(f"Replacements contains elements that are not in {self.group}")
+                print(f"Replacements contains elements that are not in {self.group}")
         else:
-            raise Exception("Replacements is not the same length as the list of existential elements")
+            print("Replacements is not the same length as the list of existential elements")
+
+## Special types of elements/groups
+
+class identity(element):
+    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)])
+        eq = Eq(lhs,rhs,pg)
+        idnty = forall([arbitrary('x',pg)], pg, eq)
+        pg.addElementProperty(idnty,elementName)
+
+class inverse(element):
+    def __init__(self, elementName, pg):
+        super().__init__(elementName, pg)
+        lhs = Mult([arbitrary('x',pg),elementName]) # self or elementName?
+        rhs = Mult([arbitrary('x',pg)])
+        eq = Eq(lhs,rhs,pg)
+        idnty = forall([arbitrary('x',pg)], pg, eq)
+        pg.addElementProperty(idnty,elementName)