| 36 | 36 |
prev = None
|
| 37 | 37 |
rewritten_eqn = None
|
| 38 | 38 |
eqn_shown = False
|
| 39 | |
for step in theorem.steps:
|
|
39 |
for step_num, step in enumerate(theorem.steps):
|
| 40 | 40 |
if prev is None:
|
| 41 | 41 |
self.log("Verifying that {} follows from established rules", render(step.eqn))
|
| 42 | 42 |
if step.eqn.lhs == step.eqn.rhs:
|
| 43 | 43 |
rewritten_eqn = step.eqn
|
| 44 | 44 |
self.log("Confirmed that {} follows from Reflexivity", render(step.eqn))
|
| 45 | 45 |
else:
|
| 46 | |
raise DerivationError("Could not derive {} from established rules".format(render(step.eqn)))
|
|
46 |
raise DerivationError("In step {} of {}: Could not derive {} from established rules".format(step_num + 1, theorem.name, render(step.eqn)))
|
| 47 | 47 |
else:
|
| 48 | 48 |
self.log("Verifying that {} follows from {}", render(step.eqn), render(prev.eqn))
|
| 49 | 49 |
rewritten_eqn = self.obtain_rewritten_step(step, prev)
|
| 50 | 50 |
if not rewritten_eqn:
|
| 51 | |
raise DerivationError("Could not derive {} from {}".format(render(step.eqn), render(prev.eqn)))
|
|
51 |
raise DerivationError("In step {} of {}: Could not derive {} from {}".format(step_num + 1, theorem.name, render(step.eqn), render(prev.eqn)))
|
| 52 | 52 |
|
| 53 | 53 |
if rewritten_eqn == theorem.eqn:
|
| 54 | 54 |
self.log("With {} we have now shown the theorem {}".format(render(rewritten_eqn), render(theorem.eqn)))
|
|
| 56 | 56 |
prev = step
|
| 57 | 57 |
|
| 58 | 58 |
if not eqn_shown:
|
| 59 | |
raise DerivationError("No step in proof showed {}".format(render(theorem.eqn)))
|
|
59 |
raise DerivationError("No step in proof of {} showed {}".format(theorem.name, render(theorem.eqn)))
|
| 60 | 60 |
|
| 61 | 61 |
def obtain_rewritten_step(self, step, prev):
|
| 62 | 62 |
rules_to_try = self.rules
|