From: Stefano Zacchiroli Date: Tue, 25 Oct 2005 15:36:46 +0000 (+0000) Subject: fixed some type error X-Git-Tag: V_0_7_2_3~190 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6138662d1a9d564f2be9fdc79cf8ed3cbae58b5;p=helm.git fixed some type error --- diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index 15091f009..0680231a8 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -1,4 +1,4 @@ -\documentclass[a4paper,draft]{article} +\documentclass[a4paper]{article} \usepackage{a4wide} \usepackage{pifont} @@ -23,7 +23,7 @@ \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}} \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}} \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}} -\newcommand{\ENDFOCUS}{\ensuremath{\mathtt{unfocus}}} +\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}} \newcommand{\SKIP}{\MATHTT{skip}} \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}} @@ -42,7 +42,7 @@ \newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle} \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}} -\newcommand{\GIN}[1][1]{\ensuremath{[s_{#1};\cdots;s_n]}} +\newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}} \newcommand{\ZEROPOS}{\MATHIT{zero\_pos}} \newcommand{\INITPOS}{\MATHIT{init\_pos}} @@ -51,9 +51,11 @@ \newcommand{\FILTEROPEN}{\MATHIT{filter\_open}} \newcommand{\ISOPEN}{\MATHIT{is\_open}} \newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}} +\newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}} +\newcommand{\GOALS}{\MATHIT{goals}} \newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}} -\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{S}}} +\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}} \newlength{\sidecondlen} \setlength{\sidecondlen}{2cm} @@ -76,7 +78,8 @@ & | & \POS{i} & \mbox{(relative positioning)} \\ & | & \MERGE & \mbox{(merge)} \\[2ex] & | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\ - & | & \ENDFOCUS & \mbox{(unfocus)} \\[2ex] + & | & \UNFOCUS & \mbox{(unfocus)} \\[2ex] + & | & S ~ S & \mbox{(sequential composition)} \\[2ex] T & : := & & \mbox{(\textbf{tactics})}\\ & & \SKIP & \mbox{(skip)} \\ & | & \mathtt{reflexivity} & \\ @@ -89,14 +92,16 @@ \[ \begin{array}{rcll} + \xi & & & \mbox{(proof status)} \\ + \mathit{goal} & & & \mbox{(proof goal)} \\[2ex] + \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\ \mathit{locator} & = & \INT\times\SWITCH & \\ \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex] - \xi & = & (\INT\times\alpha)~\LIST& \mbox{(metasenv)} \\ \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\ - \tau & = & \SWITCH~\LIST & \mbox{(todo)} \\ - \kappa & = & \SWITCH~\LIST & \mbox{(dot's future)} \\[2ex] + \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\ + \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex] \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST \\[2ex] @@ -107,22 +112,52 @@ \paragraph{Utilities} \begin{itemize} - \item \ZEROPOS: map $g -> 0, \OPEN~g$ - \item \INITPOS: map $g -> i, \OPEN~g$ - \item \ISFRESH: $\OPEN~g, 0 -> true | \_ -> false$ - \item \FILTEROPEN: $G -> \FILTER(\ISOPEN,G)$ - \item \DEEPCLOSE: prende uno stack ed un insieme di goal da chiudere, traversa - lo stack rimuovendo le occorrenze dei goal da $\tau$ e $\kappa$ e marcandole - chiuse in $\Gamma$ + \item $\ZEROPOS([g_1;\cdots;g_n]) = + [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$ + \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) = + [\langle 1,\OPEN~s_1\rangle;\cdots;\langle n,\OPEN~s_n\rangle]$ + \item $\ISFRESH(s) = + \left\{ + \begin{array}{ll} + \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\ + \mathit{false} & \mathrm{otherwise} \\ + \end{array} + \right.$ + \item $\FILTEROPEN(\mathit{locs})= + \left\{ + \begin{array}{ll} + [] & \mathrm{if}~\mathit{locs} = [] \\ + \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\ + \FILTEROPEN(\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\ + \end{array} + \right.$ + \item $\REMOVEGOALS(G,\mathit{locs}) = + \left\{ + \begin{array}{ll} + [] & \mathrm{if}~\mathit{locs} = [] \\ + \REMOVEGOALS(G,\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} + \land g\in G\\ + hd :: \REMOVEGOALS(G,\mathit{tl}) + & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\ + \end{array} + \right.$ + \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$ + it returns a new stack $S'$ identical to the given one with the exceptions + that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack + components and removed from $\tau$ and $\kappa$ components. + \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position + on a given stack $S$. \end{itemize} \paragraph{Invariants} \begin{itemize} - \item $\forall \ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s \in\tau\cup\kappa, - \exists g, s = \OPEN~g$ (i goal in $\tau$ e $\kappa$ sono aperti) - \item la lista dei goal nel metasenv contiene tutti e soli i goal presenti - sullo stack - \item lo stack puo' contenere goal duplicati nel caso di uso della select + \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s + \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in + $\tau$ and $\kappa$ components has an \OPEN~switch). + \item Unless \FOCUS{} is used the stack contains no duplicate goals. \end{itemize} \subsection{Semantics} @@ -157,40 +192,47 @@ & = & \langle \xi_n, - \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t} + \ENTRY{\Gamma'}{\tau'}{\kappa'}{t} +% \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t} :: \DEEPCLOSE(G^c_n,S) \rangle \\[1ex] - \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ + \Gamma' = \ZEROPOS(G^o_n) + \land \tau' = \REMOVEGOALS(G^c_n,\tau) + \land \kappa' = \REMOVEGOALS(G^o_n,\kappa) + } + \\[1ex] + \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~ \left\{ \begin{array}{rcll} \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\ \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle & = & \langle\xi_i, G^o_i, G^c_i\rangle - & s_{i+1}\in G^c_i \\ + & l_{i+1}\in G^c_i \\ \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle & = & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle - & s_{i+1}\not\in G^c_i \\[1ex] - & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{s_{i+1}} - \\ + & l_{i+1}\not\in G^c_i \\[1ex] + & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\ \end{array} \right. } - \\[2ex] + \\[6ex] \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S} & = - & \langle \xi, \ENTRY{s_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle + & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle \\[1ex] - & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN + & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1 \\[2ex] - \SEM{~\DOT~}{\ENTRY{[]}{\tau}{s::\kappa}{t}::S} + \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S} & = - & \langle \xi, \ENTRY{\Gamma}{\tau}{\kappa}{t}::S \rangle + & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle + \\[1ex] + & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[] \\[2ex] \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex] @@ -198,39 +240,42 @@ \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} \quad & = - & \langle\xi, \ENTRY{s_1'}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{[s_2';\cdots;s_n']}{\tau}{\kappa}{t}::S + & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S \\[1ex] - & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[s_1';\cdots;s_n'] + & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n'] \\[2ex] \SEM{~\SHIFT~} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t}::S} + {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'} + ::S} & = & \langle - \xi, \ENTRY{s_1}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{\GIN[2]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t}::S + \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG} + ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S \rangle + \\[1ex] + & & \mathrm{where} ~ n\geq 1 \\[2ex] - \SEM{\POS{i}} - {\ENTRY{[s]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} + \SEM{~\POS{i}~} + {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} & = - & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{s_i :: (\Gamma'\setminus [s_i])}{\tau'}{\kappa'}{t'}::S \rangle + & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle \\[1ex] - & & \mathrm{where} ~ \langle i,s'\rangle = s_i\in \Gamma'~\land~\ISFRESH(s) + & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l) \\[2ex] - \SEM{\POS{i}} + \SEM{~\POS{i}~} {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG} ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} & = - & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{\Gamma'\setminus [s_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S + & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG} + ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S \rangle \\[1ex] - & & \mathrm{where} ~ \langle i, s'\rangle = s_i\in \Gamma' + & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma' \\[2ex] \SEM{~\MERGE~} @@ -245,14 +290,15 @@ \SEM{\FOCUS{g_1,\dots,g_n}}{S} & = - & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}::S + & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG} + ::\DEEPCLOSE(S) \rangle \\[1ex] & & \mathrm{where} ~ - \forall ~ i=1,\dots,n,~\exists~\alpha_i,n_i,~\langle n_i,\alpha_i\rangle\in\xi + \forall i=1,\dots,n,~g_i\in\GOALS(S) \\[2ex] - \SEM{\ENDFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S} + \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S} & = & \langle \xi, S\rangle \\[2ex]