helm/ocaml/tactics/doc/body.tex

   1
   2 \section{Semantics}
   3
   4 \subsection{Language}
   5
   6 \[
   7 \begin{array}{rcll}
   8  S & ::= & & \mbox{(\textbf{continuationals})}\\
   9    &     & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
  10    &  |  & \DOT & \mbox{(dot)} \\
  11    &  |  & \SEMICOLON & \mbox{(semicolon)} \\
  12    &  |  & \BRANCH & \mbox{(branch)} \\
  13    &  |  & \SHIFT & \mbox{(shift)} \\
  14    &  |  & \POS{i} & \mbox{(relative positioning)} \\
  15    &  |  & \MERGE & \mbox{(merge)} \\[2ex]
  16    &  |  & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
  17    &  |  & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
  18    &  |  & S ~ S & \mbox{(sequential composition)} \\[2ex]
  19    T & : := & & \mbox{(\textbf{tactics})}\\
  20      &   & \SKIP & \mbox{(skip)} \\
  21      & | & \mathtt{reflexivity} & \\
  22      & | & \mathtt{apply}~t & \\
  23      & | & \dots &
  24 \end{array}
  25 \]
  26
  27 \subsection{Status}
  28
  29 \[
  30 \begin{array}{rcll}
  31  \xi & & & \mbox{(proof status)} \\
  32  \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]
  33
  34  \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
  35  \mathit{locator} & = & \INT\times\SWITCH & \\
  36  \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]
  37
  38  \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
  39  \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
  40  \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]
  41
  42  \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
  43  \\[2ex]
  44
  45  \mathit{status} & = & \xi\times\mathit{stack} \\
  46 \end{array}
  47 \]
  48
  49 \paragraph{Utilities}
  50 \begin{itemize}
  51  \item $\ZEROPOS([g_1;\cdots;g_n]) =
  52   [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
  53  \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
  54   [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$
  55  \item $\ISFRESH(s) =
  56   \left\{
  57   \begin{array}{ll}
  58    \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
  59    \mathit{false} & \mathrm{otherwise} \\
  60   \end{array}
  61   \right.$
  62  \item $\FILTEROPEN(\mathit{locs})=
  63   \left\{
  64   \begin{array}{ll}
  65    [] & \mathrm{if}~\mathit{locs} = [] \\
  66    \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
  67    & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
  68    \FILTEROPEN(\mathit{tl})
  69    & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
  70   \end{array}
  71   \right.$
  72  \item $\REMOVEGOALS(G,\mathit{locs}) =
  73   \left\{
  74   \begin{array}{ll}
  75    [] & \mathrm{if}~\mathit{locs} = [] \\
  76    \REMOVEGOALS(G,\mathit{tl})
  77    & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
  78      \land g\in G\\
  79    hd :: \REMOVEGOALS(G,\mathit{tl})
  80    & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
  81   \end{array}
  82   \right.$
  83  \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
  84   it returns a new stack $S'$ identical to the given one with the exceptions
  85   that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
  86   components and removed from $\tau$ and $\kappa$ components.
  87  \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
  88   on a given stack $S$, appearing in an \OPEN{} switch.
  89 \end{itemize}
  90
  91 \paragraph{Invariants}
  92 \begin{itemize}
  93  \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
  94   \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
  95   $\tau$ and $\kappa$ components has an \OPEN~switch).
  96  \item Unless \FOCUS{} is used the stack contains no duplicate goals.
  97  \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the
  98   top-level $\Gamma$)}, \ISFRESH(l)$.
  99 \end{itemize}
 100
 101 \subsection{Semantics}
 102
 103 \[
 104 \begin{array}{rcll}
 105  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
 106   \mbox{(continuationals semantics)} \\
 107  \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
 108   \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
 109 \end{array}
 110 \]
 111
 112 \[
 113 \begin{array}{rcl}
 114  \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
 115   \xi\times\GOAL~\LIST\times\GOAL~\LIST
 116 \end{array}
 117 \]
 118
 119 \[
 120 \begin{array}{rlcc}
 121  \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
 122  \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
 123 \end{array}
 124 \]
 125
 126 \[
 127 \begin{array}{rcl}
 128
 129  \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 130  & =
 131  & \langle
 132    \xi_n,
 133    \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
 134 %    \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
 135    :: \DEEPCLOSE(G^c_n,S)
 136    \rangle
 137  \\[1ex]
 138  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
 139  \\[1ex]
 140  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
 141   \Gamma' = \ZEROPOS(G^o_n)
 142   \land \tau' = \REMOVEGOALS(G^c_n,\tau)
 143   \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
 144  }
 145  \\[1ex]
 146  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
 147  \left\{
 148  \begin{array}{rcll}
 149   \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\
 150   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
 151   & =
 152   & \langle\xi_i, G^o_i, G^c_i\rangle
 153   & l_{i+1}\in G^c_i \\
 154   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
 155   & =
 156   & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle
 157   & l_{i+1}\not\in G^c_i \\[1ex]
 158   & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
 159  \end{array}
 160  \right.
 161  }
 162  \\[6ex]
 163
 164  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
 165  & =
 166  & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
 167  \\[1ex]
 168  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
 169  \\[2ex]
 170
 171  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
 172  & =
 173  & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
 174  \\[1ex]
 175  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
 176  \\[2ex]
 177
 178  \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]
 179
 180  \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 181  \quad
 182  & =
 183  & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
 184    ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
 185  \\[1ex]
 186  & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
 187  \\[2ex]
 188
 189  \SEM{~\SHIFT~}
 190   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'}
 191   ::S}
 192  & =
 193  & \langle
 194    \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
 195         ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
 196    \rangle
 197  \\[1ex]
 198  & & \mathrm{where} ~ n\geq 1
 199  \\[2ex]
 200
 201  \SEM{~\POS{i}~}
 202   {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 203  & =
 204  & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
 205    ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
 206  \\[1ex]
 207  & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
 208  \\[2ex]
 209
 210  \SEM{~\POS{i}~}
 211   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
 212   ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 213  & =
 214  & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
 215  ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
 216    \rangle
 217  \\[1ex]
 218  & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
 219  \\[2ex]
 220
 221  \SEM{~\MERGE~}
 222   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
 223   ::S}
 224  & =
 225  & \langle \xi,
 226    \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
 227    :: S
 228    \rangle
 229  \\[2ex]
 230
 231  \SEM{\FOCUS{g_1,\dots,g_n}}{S}
 232  & =
 233  & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG}
 234    ::\DEEPCLOSE(S)
 235    \rangle
 236  \\[1ex]
 237  & & \mathrm{where} ~
 238  \forall i=1,\dots,n,~g_i\in\GOALS(S)
 239  \\[2ex]
 240
 241  \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
 242  & =
 243  & \langle \xi, S\rangle \\[2ex]
 244
 245 \end{array}
 246 \]
 247