diff --git a/README.md b/README.md index 2d31569..392d39e 100644 --- a/README.md +++ b/README.md @@ -1 +1,26 @@ -# global-environment \ No newline at end of file +# Automated Proof Checker + +## Set up + +1. Clone the repository using `git clone` +2. Install packages using preferred installer - need to fix, create pip requirements file + +## Codebase + +The codebase we have designed seperates the elements of abstract algebra into different environments to make writing proofs a seamless experience. The main files are `proof.py,group.py,element.py,` and `logicObjects.py`. The names are pretty self explanatory, but to learn more about how each of the files work poke around some of the `__init__` calls and member functions of those files to see how they interact together. + +## Usage + +There are two options to use our proof-checker, but we **highly** recommend using the first option. + ++ Using our graphical user interface! + 1. Run `python gui.py` to open the interface + 2. The **Enter** button is used to enter new steps. As you type in the black text box the possible functions yoiu could call will appear below so you never make spelling errors! Warnings will appear if you attempt a step that is not valid. + 3. The **Generate Latex** will take the proof, convert it to a latex file and display the corresponding pdf inside of the GUI in real time! + 4. The **Undo** button deletes the last step you did - be careful to only use this when you need it! ++ Using our raw language in a python file + 1. Open a new file called `my_proof_name_here.py`, with a descriptive name for your proof + 2. Create a new proof object using the `Proof` function from `proof.py` + 3. Enter the steps of your proof using the functions in `proof.py` + 4. Run the command `python my_proof_name_here.py` to see the proof steps in the console. + diff --git a/Simple Abelian Proof.pdf b/Simple Abelian Proof.pdf new file mode 100644 index 0000000..20ed1fe Binary files /dev/null and b/Simple Abelian Proof.pdf differ diff --git a/Simple Abelian Proof.tex b/Simple Abelian Proof.tex new file mode 100644 index 0000000..154abd2 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/__pycache__/group.cpython-39.pyc b/__pycache__/group.cpython-39.pyc index bc3dd3f..e2a172c 100644 Binary files a/__pycache__/group.cpython-39.pyc and b/__pycache__/group.cpython-39.pyc differ diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc index 9404317..74f4fb5 100644 Binary files a/__pycache__/logicObjects.cpython-39.pyc and b/__pycache__/logicObjects.cpython-39.pyc differ diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index e4c533c..9a283a2 100644 Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ diff --git a/group.py b/group.py index 0dc18d8..ba15fb6 100644 --- a/group.py +++ b/group.py @@ -64,4 +64,7 @@ def addElementProperty(self, property, elementName): print("That element doesn't exist!", property, elementName) def contains(self, elementName): - return elementName in self.elements \ No newline at end of file + return elementName in self.elements + + def toLaTeX(self): + return self.groupName \ No newline at end of file diff --git a/gui.py b/gui.py new file mode 100644 index 0000000..865701f --- /dev/null +++ b/gui.py @@ -0,0 +1,161 @@ +from tkinter import PhotoImage +from tkinter import ttk +from tkinter import * +from turtle import undo +from proof import * +from tkinter.scrolledtext import ScrolledText +import fitz +from ttkwidgets.autocomplete import AutocompleteCombobox + + +proof_methods = ['MultElem', 'accessAssumption', 'andElim', 'breakPower', 'cancelLeft', +'cancelRight', 'closure', 'combinePower', 'concludeSubproof', 'forAllIntroduction', 'forallElim', +'identleft', 'identright', 'impliesIntroduction', 'introAssumption', 'introCases', 'introElement', +'introGroup', 'introReflexive', 'introSubproof', 'inverseElimLHS', 'inverseElimRHS', 'leftMult', +'leftSidesEq', 'modus', 'notElim', 'qed', 'reduceLogic', 'rightMult', 'rightSidesEq', 'show', +'showReturn', 'splitPowerAddition', 'splitPowerMult', 'substituteLHS', 'substituteRHS', +'switchSidesOfEqual', 'thereexistsElim', 'undo', 'writeLaTeXfile'] + +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') + + +def match_string(): + hits = [] + got = entry_bar.get() + for item in proof_methods: + if item.startswith(got): + hits.append(item) + return hits + +def match_string_del(): + hits = [] + got = entry_bar.get()[:-1] + for item in proof_methods: + if item.startswith(got): + hits.append(item) + return hits + +def check_empty(event): + if len(entry_bar.get()) == 1: + suggestions.set("") + else: + hits = match_string_del() + show_hit(hits) + +def get_typed(event): + if len(event.keysym) == 1: + hits = match_string() + show_hit(hits) + +def show_hit(lst): + suggestions.set(lst) + if len(lst) == 1: + entry.set(lst[0]) + detect_pressed.filled = True + entry_bar.icursor(END) + +def detect_pressed(event): + key = event.keysym + if len(key) == 1 and detect_pressed.filled is True: + pos = entry_bar.index(INSERT) + entry_bar.delete(pos, END) + +detect_pressed.filled = False + + +entry = StringVar() +entry_bar = Entry( + mainframe, + width = 50, + bg='black', + insertbackground='white', + fg='white', + textvariable=entry) +entry_bar.grid(column=1, row=3, sticky=(W, E)) +entry_bar.focus_set() +entry_bar.bind('', get_typed) +entry_bar.bind('', detect_pressed) +entry_bar.bind('', check_empty) + +def undo(*args): + p.undo() + showing.set(p.showReturn()) + + +#entry_bar = AutocompleteCombobox(mainframe, width=50, textvariable=entry, completevalues = proof_methods) + + +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="Undo", command=undo).grid(column=3, row=2, sticky=W) + +ttk.Button(mainframe, text="Generate Latex", command=generateLaTeX).grid(column=3, row=4, sticky=W) + +suggestions = StringVar() +showSuggestions = ttk.Label(mainframe, width = 50, background="white", textvariable=suggestions).grid(column=1, row=4, sticky=(W, E)) + +for child in mainframe.winfo_children(): + child.grid_configure(padx=5, pady=5) + +entry_bar.focus() +root.bind("", 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() \ No newline at end of file diff --git a/logicObjects.py b/logicObjects.py index 65cfce8..d9ab9f9 100644 --- a/logicObjects.py +++ b/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,6 +109,9 @@ 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): @@ -104,6 +119,9 @@ def elim(self, 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.group) 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: diff --git a/proof.py b/proof.py index 7bd5772..5a26adb 100644 --- a/proof.py +++ b/proof.py @@ -4,6 +4,9 @@ from group import * from integer import * from logicObjects import * +from tkinter import messagebox +from pylatex import Document, Section, Subsection, Command, Enumerate +from pylatex.utils import italic, NoEscape class Proof: def __init__(self, label, assumption, goal=None, steps=[], justifications = [], depth=0, linestart=0): # make goal optional @@ -31,7 +34,48 @@ def undo(self): self.steps = self.steps[:-1] self.justifications = self.justifications[:-1] self.show() - + + def writeLaTeXfile(self): + doc = Document(page_numbers=False) + doc.preamble.append(Command('title', self.label)) + doc.append(NoEscape(r'\maketitle')) + doc.append(italic("Proof:")) + with doc.create(Enumerate()) as enum: + doc.append(NoEscape(r"\addtocounter{enumi}{-1}")) + for i in range(len(self.steps)): + if isinstance(self.steps[i],str): + enum.add_item(NoEscape(self.steps[i]+r"\hfill")) + else: + enum.add_item(NoEscape("$"+self.steps[i].toLaTeX()+r"$\hfill")) + enum.append(" by " + str(self.justifications[i])) + doc.generate_tex(self.label) + doc.generate_pdf(self.label) + + def showReturn(self): + showstr = "" + if self.depth==0: + showstr += 'Proof : ' + showstr += self.label + showstr += '\n' + showstr += '--------------------------------' + showstr += '\n' + else: + showstr += 'Subproof : assume ' + showstr += str(self.assumption) + showstr += '\n' + showstr += '--------------------------------' + showstr += '\n' + i = self.linestart + while i < len(self.steps): + if isinstance(self.steps[i],Proof): + showstr += self.steps[i].show() + i+=len(self.steps[i].steps)-self.steps[i].linestart-1 + else: + linestr = "\t"*self.depth + str(i) + ': ' + str(self.steps[i]) + '\t' + str(self.justifications[i]) + '\n' + showstr += linestr + i+=1 + return showstr + def show(self): if self.depth==0: print('') @@ -102,9 +146,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('\n'+f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - print('\n'+f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + messagebox.showerror('Proof Error',f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def substituteLHS(self, lineNum1, lineNum2): """ @@ -121,9 +165,9 @@ def substituteLHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}'] self.show() else: - print('\n'+f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + messagebox.showerror('Proof Error',f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - print('\n'+f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + messagebox.showerror('Proof Error',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) """ @@ -143,9 +187,9 @@ def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] self.show() else: - print ('\n'+f"Line {str(lineNum1)} is not an implies statement") + messagebox.showerror('Proof Error',f"Line {str(lineNum1)} is not an implies statement") else: - print('\n'+"The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") + messagebox.showerror('Proof Error',"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): """ @@ -170,13 +214,13 @@ def inverseElimRHS(self,lineNum): lawApplied=True break if lawApplied==False: - print ('\n'+f"Inverse laws can't be applied on line {lineNum}") + messagebox.showerror('Proof Error',f"Inverse laws can't be applied on line {lineNum}") else: self.steps += [newProducts] self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] self.show() else: - print('\n'+f"It doesn't seem like line {lineNum} contains an equation") + messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def inverseElimLHS(self,lineNum): @@ -202,13 +246,13 @@ def inverseElimLHS(self,lineNum): lawApplied=True break if lawApplied==False: - print ('\n'+f"Inverse laws can't be applied on line {lineNum}") + messagebox.showerror('Proof Error',f"Inverse laws can't be applied on line {lineNum}") else: self.steps += [newProducts] self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] self.show() else: - print('\n'+f"It doesn't seem like line {lineNum} contains an equation") + messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") ## For all and there exists elimination @@ -225,7 +269,7 @@ def forallElim(self, lineNum, replacements): self.justifications += [f'For all elimination on line {lineNum}'] self.show() else: - print('\n'+f"There is no forall statmenent on line {lineNum}") + messagebox.showerror('Proof Error',f"There is no forall statmenent on line {lineNum}") def thereexistsElim(self, lineNum, replacements): # We can only do this once! @@ -241,7 +285,7 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once! self.justifications += [f'There exists elimination on line {lineNum}'] self.show() else: - print('\n' + f"There is no there exists statmenent on line {lineNum}") + messagebox.showerror('Proof Error', f"There is no there exists statmenent on line {lineNum}") ## Multiplication manipulation @@ -261,9 +305,9 @@ def leftMult(self, elemName, lineNum): self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] self.show() else: - print('\n' + "The element " + elemName + " is not in the " + str(eq.group)) + messagebox.showerror('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) else: - print ('\n' + f"Line {lineNum} is not an equation") + messagebox.showerror('Proof Error', f"Line {lineNum} is not an equation") def rightMult (self, elemName, lineNum): """ @@ -281,9 +325,9 @@ def rightMult (self, elemName, lineNum): self.justifications += ['Right multiply line {lineNum} by ' +str(elem) ] self.show() else: - print('\n' + "The element " + elemName + " is not in the " + str(eq.group)) + messagebox.showerror('Proof Error', "The element " + elemName + " is not in the " + str(eq.group)) else: - print ('\n' + f"Line {lineNum} is not an equation") + messagebox.showerror('Proof Error', f"Line {lineNum} is not an equation") ##power methods def breakPower(self,input): """ @@ -300,7 +344,7 @@ def breakPower(self,input): self.justifications += ['Convert power object to mult object'] self.show() else: - print ('\n'+f"Expected a power object but received type {type(input)}") + messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") def combinePower(self, mult): """ @@ -322,7 +366,7 @@ def combinePower(self, mult): self.justifications += ['Convert multiplications to equivalent powers'] self.show() else: - print ('\n' +f"Expected a Mult object but received type {type(mult)}") + messagebox.showerror('Proof Error',f"Expected a Mult object but received type {type(mult)}") def splitPowerAddition(self,input): """ @@ -334,7 +378,7 @@ def splitPowerAddition(self,input): exp=input.exponent l=exp.split("+") if len(l)==1: - print ('\n'+"No power addition to be split apart") + messagebox.showerror('Proof Error',"No power addition to be split apart") else: multList=[] for i in l: @@ -344,7 +388,7 @@ def splitPowerAddition(self,input): self.justifications += ["Split up power with addition in exponents"] self.show() else: - print ('\n'+f"Expected a power object but received type {type(input)}") + messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") def splitPowerMult(self,input): @@ -357,7 +401,7 @@ def splitPowerMult(self,input): exp=input.exponent l=exp.split("*") if len(l)==1: - print ('\n'+"No power multiplication to be split apart") + messagebox.showerror('Proof Error',"No power multiplication to be split apart") else: elem=element for i in l: @@ -367,7 +411,7 @@ def splitPowerMult(self,input): self.justifications += ["Split up power with multiplication in exponents"] self.show() else: - print ('\n'+f"Expected a power object but received type {type(input)}") + messagebox.showerror('Proof Error',f"Expected a power object but received type {type(input)}") ## Identity and equality elimination def rightSidesEq(self, lineNum1, lineNum2): @@ -383,7 +427,7 @@ def rightSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same right side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - print ('\n' +f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") + messagebox.showerror('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") def leftSidesEq(self, lineNum1, lineNum2): """ @@ -398,7 +442,7 @@ def leftSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same left side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - print ('\n' +f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") + messagebox.showerror('Proof Error',f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") def identleft(self, lineNum): """ @@ -422,7 +466,7 @@ def identleft(self, lineNum): break # else we can't apply identity elimination if l1==[]: - print('\n' +"Identity can't be applied") + messagebox.showerror('Proof Error',"Identity can't be applied") else: newProduct = Mult(l1) ret = Eq(newProduct,evidence.RHS,evidence.group) @@ -430,7 +474,7 @@ def identleft(self, lineNum): self.justifications += ["identity elimination "] self.show() else: - print('\n' +f"Expected an equation on line {lineNum} but received {type(evidence)}") + messagebox.showerror('Proof Error',f"Expected an equation on line {lineNum} but received {type(evidence)}") def identright(self, lineNum): @@ -463,7 +507,7 @@ def identright(self, lineNum): self.justifications += ["identity elimination "] self.show() else: - print('\n' + f"Expected an equation on line {lineNum} but received {type(evidence)}") + messagebox.showerror('Proof Error', f"Expected an equation on line {lineNum} but received {type(evidence)}") @@ -479,7 +523,7 @@ def introReflexive(self,eq): self.justifications += ["reflexive equality"] self.show() else: - print ('\n' + "This is not reflexive") + messagebox.showerror('Proof Error', "This is not reflexive") def reduceLogic(self, lineNum): """ @@ -492,7 +536,7 @@ def reduceLogic(self, lineNum): self.justifications += ["logic reduction"] self.show() else: - print ('\n' + "This is not a logic statement") + messagebox.showerror('Proof Error', "This is not a logic statement") def introCases(self, case): """ @@ -545,7 +589,7 @@ def introElement(self,G, name): :param name: the name of the new element """ if G.contains(name): - print('\n' + f"{name} is already in {G}") + messagebox.showerror('Proof Error', f"{name} is already in {G}") else: self.env[name] = G.newElement(name) self.steps += [In(name, G)] @@ -566,11 +610,9 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): v = vars[i] l = elemIntroLines[i] if self.steps[l].elem!=vars[i]: - print('\n') - print("Line", l, "does not introduce variable", v) + messagebox.showerror('Proof Error', f'Line {l} does not introduce variable {v}') elif self.steps[l].group!=G: - print('\n') - print("Element", v, "is not in group", G) + messagebox.showerror('Proof Error', f'Element {v} is not in group {G}') else: #If you make it here, this is a valid for all intro self.steps+=[forall(vars,G,evidence)] @@ -591,9 +633,9 @@ def closure(self,G,a,b): self.show() else: if not G.contains(a): - print('\n'+f"{a} is not in {G}") + messagebox.showerror('Proof Error',f"{a} is not in {G}") else: - print('\n'+f"{b} is not in {G}") + messagebox.showerror('Proof Error',f"{b} is not in {G}") def cancelRight(self, lineNum, mult): ''' @@ -611,9 +653,9 @@ def cancelRight(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - print('\n'+f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") + messagebox.showerror('Proof Error',f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") else: - print('\n'+f"It doesn't seem like line {lineNum} contains an equation") + messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def cancelLeft(self, lineNum, mult): ''' @@ -631,9 +673,9 @@ def cancelLeft(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - print('\n'+f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") + messagebox.showerror('Proof Error',f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") else: - print('\n'+f"It doesn't seem like line {lineNum} contains an equation") + messagebox.showerror('Proof Error',f"It doesn't seem like line {lineNum} contains an equation") def switchSidesOfEqual(self, lineNum): ''' @@ -648,7 +690,7 @@ def switchSidesOfEqual(self, lineNum): self.justifications += [f"Switched sides of line {lineNum}"] self.show() else: - print('\n'+f"Hmm, it doesn't look like line {lineNum} isn't an equality") + messagebox.showerror('Proof Error',f"Hmm, it doesn't look like line {lineNum} isn't an equality") def notElim(self, lineNum1, lineNum2): ''' @@ -663,7 +705,7 @@ def notElim(self, lineNum1, lineNum2): self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] self.show() else: - print('\n'+f"The statement on line {lineNum1} isn't a Not statement") + messagebox.showerror('Proof Error',f"The statement on line {lineNum1} isn't a Not statement") def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it ''' @@ -695,7 +737,7 @@ def andElim(self, lineNum, n): self.justifications += ["And elimination"] self.show() else: - print('\n'+"You must choose argument 1 or 2") + messagebox.showerror('Proof Error',"You must choose argument 1 or 2") else: - print('\n'+f"The statement on line {lineNum} isn't an And statement") + messagebox.showerror('Proof Error',f"The statement on line {lineNum} isn't an And statement") \ No newline at end of file diff --git a/unique inverses.py b/unique inverses.py index 005533e..56e31e2 100644 --- a/unique inverses.py +++ b/unique inverses.py @@ -5,7 +5,7 @@ from integer import * from logicObjects import * - +''' G = group('G','*') inversePropertyOne = Eq( Mult(['a','c']) , Mult([G.identity_identifier]) , G) inversePropertyTwo = Eq( Mult(['a','d']) , Mult([G.identity_identifier]) , G) @@ -24,3 +24,5 @@ p2.switchSidesOfEqual(8) p.concludeSubproof(9) p.qed(10) +''' +print(dir(Proof))