first pass

Simple Abelian Proof.tex

@@ -0,0 +1,17 @@
+\documentclass{article}%
+\usepackage[T1]{fontenc}%
+\usepackage[utf8]{inputenc}%
+\usepackage{lmodern}%
+\usepackage{textcomp}%
+\usepackage{lastpage}%
+%
+\title{Simple Abelian Proof}%
+%
+\begin{document}%
+\normalsize%
+\maketitle%
+\textit{Proof:}%
+\begin{enumerate}%
+\addtocounter{enumi}{-1}%
+\end{enumerate}%
+\end{document}

gui.py

@@ -0,0 +1,82 @@
+from tkinter import PhotoImage
+from tkinter import *
+from tkinter import ttk
+from proof import *
+from tkinter.scrolledtext import ScrolledText
+import fitz
+
+class PDFViewer(ScrolledText):
+    def show(self, pdf_file):
+        self.delete('1.0', 'end') # clear current content
+        pdf = fitz.open(pdf_file) # open the PDF file
+        self.images = []   # for storing the page images
+        for page in pdf:
+            pix = page.get_pixmap()
+            pix1 = fitz.Pixmap(pix, 0) if pix.alpha else pix
+            photo = PhotoImage(data=pix1.tobytes('ppm'))
+            # insert into the text box
+            self.image_create('end', image=photo)
+            self.insert('end', '\n')
+            # save the image to avoid garbage collected
+            self.images.append(photo)
+
+
+def enter(*args):
+    input = entry.get()
+    input = "p."+input
+    print(input)
+    try:
+        exec(input)
+    except:
+        messagebox.showerror('Syntax Error', 'You have either called a function that does not exist or passed a variable that is not defined - or both!')
+    showing.set(p.showReturn())
+    entry_bar.delete(0,"end")
+
+
+def generateLaTeX(*args):
+    p.writeLaTeXfile()
+    pdf1.show('Simple Abelian Proof.pdf')
+
+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)
+
+root = Tk()
+root.title("Proof-Check")
+
+mainframe = ttk.Frame(root, padding="3 3 12 12")
+mainframe.grid(column=0, row=0, sticky=(N, W, E, S))
+root.columnconfigure(0, weight=1)
+root.rowconfigure(0, weight=1)
+
+pdf1 = PDFViewer(mainframe, width=80, height=30, spacing3=5, bg='blue')
+pdf1.grid(row=5, column=1, sticky='nsew')
+pdf1.show('Simple Abelian Proof.pdf')
+
+entry = StringVar()
+entry_bar = ttk.Entry(mainframe, width=50, textvariable=entry)
+entry_bar.grid(column=1, row=3, sticky=(W, E))
+
+showing = StringVar()
+showing.set("Proof : Simple Abelian Proof\n--------------------------------")
+
+showProof = ttk.Label(mainframe, background="white", textvariable=showing).grid(column=1, row=2, sticky=(W, E))
+
+ttk.Button(mainframe, text="Enter", command=enter).grid(column=3, row=3, sticky=W)
+
+ttk.Button(mainframe, text="Generate Latex", command=generateLaTeX).grid(column=3, row=4, sticky=W)
+
+for child in mainframe.winfo_children(): 
+    child.grid_configure(padx=5, pady=5)
+
+entry_bar.focus()
+root.bind("<Return>", enter)
+
+# creating object of ShowPdf from tkPDFViewer.
+#v1 = pdf.ShowPdf().pdf_view(mainframe, pdf_location = r"Simple Abelian Proof.pdf").grid(column=1, row=4, sticky=W)
+
+
+# Placing Pdf in my gui.
+#v2.grid(column=1, row=4, sticky=W)
+
+root.mainloop()

logicObjects.py

@@ -37,6 +37,9 @@ def replace(self, var, expr):
                     new_products.append(self.products[i])
                     i+=1
         return Mult(new_products)
+
+    def toLaTeX(self):
+        return "".join(self.elemList)
 
 
 class And:
@@ -57,6 +60,9 @@ def __eq__(self,other):
 
     def __repr__(self):
         return "("+ str(self.arg1)+" and "+str(self.arg2)+ ")"
+
+    def toLaTeX(self):
+        return self.arg1.toLaTeX() + r" and " + self.arg2.toLaTeX()
 
 class Or:
     def __init__(self, arg1, arg2):
@@ -69,6 +75,9 @@ def elim(self,num,implies1,implies2):
         check2 = isinstance(implies2, Implies) and implies2.assum==self.arg2
         if check1 and check2 and implies1.conc==implies2.conc:
             return implies1.conc
+
+    def toLaTeX(self):
+        return self.arg1.toLaTeX() + r" or " + self.arg2.toLaTeX()
 
 class Implies: # expand a little more functionality
     def __init__(self, assum, conc):
@@ -86,6 +95,9 @@ def __eq__(self, other):
 
     def __repr__(self):
         return  str(self.assum) + " → " +  str(self.conc)
+
+    def toLaTeX(self):
+        return self.arg1.toLaTeX() + r" \implies " + self.arg2.toLaTeX()
 
 class Not:
     def __init__(self, arg):
@@ -97,13 +109,19 @@ def elim(self, contradiction):
 
     def __repr__(self):
         return "Not " + str(self.arg)
+
+    def toLaTeX(self):
+        return r"\lnot " + self.arg.toLaTeX()
 
 class Bottom:
     def elim(self, conclusion):
         return conclusion
 
     def __repr__(self):
         return "⊥"
+
+    def toLaTeX(self):
+        return r"\bot"
 
 class In:
     def __init__(self, elem, grp):
@@ -112,6 +130,9 @@ def __init__(self, elem, grp):
 
     def __repr__(self):
         return str(self.elem) + " ∈ " + str(self.group)
+
+    def toLaTeX(self):
+        return str(self.elem) + r" \in " + str(self.grp)
 
 class Eq:
     def __init__(self,LHS,RHS,pg):
@@ -132,6 +153,9 @@ def __eq__(self,other):
 
     def replace(self, var, expr):
         return Eq(self.LHS.replace(var,expr), self.RHS.replace(var,expr), self.group)
+
+    def toLaTeX(self):
+        return str(self.LHS) + r" = " + str(self.RHS)
 
 def reduce(exp):
     if isinstance(exp, Eq):
@@ -172,6 +196,9 @@ def __eq__(self,other):
         else:
             return False
 
+    def toLaTeX(self):
+        return r"\forall " + ",".join(self.arbelems) + r" \in " + str(self.group) + r"\ " + self.eq.toLaTeX()
+
 
     def replace(self, replacements): # replacements = ['x','y'] - strings of the elements
         if len(replacements) == len(self.arbelems):
@@ -211,6 +238,9 @@ def replace(self, replacements):
         else:
             print("Replacements is not the same length as the list of existential elements")
 
+    def toLaTeX(self):
+        return r"\exists " + ",".join(self.existelems) + r" \in " + str(self.group)  + r"\ " + self.toLaTeX(self.eq)
+
 ## Unique class - idk if we need this
 
 class uniqueElementProperty: