search

proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript
MIT License
8 stars 0 forks source link

Notion of goal #58

Open phlegmaticprogrammer opened 9 years ago

phlegmaticprogrammer commented 9 years ago

In ProofScript we currently have no notion of what the current goal is. For example, you can write

theorem '∀ x. P x'
  by metis

but you cannot write

theorem '∀ x. P x'
  let 'x'
  by metis

because the by clause would not know what goal to apply metis to. If we had a notion of goal, then the let-statement would transform this goal such that the current goal would become P x, and then we could define a free occurrence of by to be acting on the current goal.

Another example is an imaginary cases by construct like

theorem 'P = Q' 
  cases by equivalence
    assume 'P'
    ...
  next
    assume 'Q'
    ...

where the goal P = Q is transformed into two subgoals P → Q and Q → P.

So, the question is: Do we need a notion of goal in ProofScript? It seems that it would help during an interactive proof mode, because the current goal(s) can be displayed to the user as to what has to be tackled with next. But it will usually make a script, once successfully created, less readable. Also, how compatible is such a notion with the current concepts of ProofScript? How difficult would it be to bolt such a notion on top of the current ProofScript implementation?