Semantics

A simple command in a goal is interpreted as a rule that needs to be proved derivable automatically by PhoX. A natural command can be seen as a tree of simple command and is therefore interpreted as a tree of derivable rule, that is a derivable rule itself.

We will just describe the interpretation of a simple command: let us assume the current goal is $\Gamma \vdash A$ then a simple command is interpreted as a rule whose conclusion is $\Gamma \vdash A$ and whose premises are defined by induction on the structure of the command. Thus, we only need to prove the premises to prove the current goal.

First some syntactic sugar can be elliminated:

• $\hbox{\tt let } I \hbox{ \tt and } I'$ is interpreted as $\hbox{\tt let } I \hbox{ \tt let } I'$
• $\hbox{\tt let } x_1,\dots,x_n \star P$ (where $\star$ is $:$ or an infix symbol is interpreted as $\hbox{\tt let } x_1 \star P \dots \hbox{\tt let } x_n \star P$
• $\hbox{\tt let } x : P$ is interpreted as $\hbox{\tt let } x \hbox{ \tt assume } P x$
• $\hbox{\tt let } x \star P$ is interpreted as $\hbox{\tt let } x \hbox{ \tt assume } x \star P$ where $\star$ is an infix symbol.
• The keyword deduce is interpreted as assume.
• $\hbox{\tt assume } A_1 \hbox{ \tt and } \dots \hbox{ \tt and } A_n$ is interpreted as $\hbox{\tt assume } A_1 \hbox{ \tt assume } \dots \hbox{ \tt assume } A_n$

Then the set of premises $\vert C\vert$ associated to the simple command $C$ if the current goal is $\Gamma \vdash A$ is defined by

$$\begin{array}{lcl} \vert\hbox{\tt let } x \; C\vert &=& \ver... ...\tt begin } C \hbox{\tt end }\vert &=& \vert C\vert \end{array}$$