diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index c0a52f8..43a5bec 100644 Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ diff --git a/abelian_proof.py b/abelian_proof.py index 3ce0fed..475f456 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -23,5 +23,4 @@ p.forallElim(1,['b']) p.substituteRHS(8,9) p.identleft(10) - -## HOW DO WE FINISH THE PROOF? \ No newline at end of file +p.qed(['b','a'],11) diff --git a/proof.py b/proof.py index 5c770d2..749d322 100644 --- a/proof.py +++ b/proof.py @@ -17,8 +17,14 @@ def __init__(self, label, assumption, goal=None, steps=[], justifications = []): # self.currAssumption = [goal.assum] # is this neccessary? self.show() - def qed(self): - return self.goal.conc in self.steps + 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: + return self.goal.conc in self.steps def undo(self): self.steps = self.steps[:-1]