Solid Intuition/Debt

From SE Wiki
Revision as of 16:37, 22 December 2010 by (Talk)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

We have assumed everywhere that unification is done automatically in the background. Unification instantiates forall-quantified variables, thereby doing scope applications (function applications). Side condition of those applications is that the function argument is in the function's domain. Thus we have to prove this condition for every instantiation done. I'll call such an addition proof-goal a "debt".

Here's what the user should be able to do with his debt:

  • eyeball-check that a statement is provable before pushing it into debt
  • at every point be able to choose between continue proving along the main thread or working off some debt
  • keep track of all the context that belongs to every item of debt
  • be able to find and apply proof steps that have preconditions, e.g. for "a ⇒ x=y": replace x by z and make a debt