From: Enrico Tassi Date: Wed, 16 Nov 2005 20:46:31 +0000 (+0000) Subject: added first draft for patterns X-Git-Tag: V_0_7_2_3~59 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=af30b22696bb1a58511a637130ea3c354d7efec5;p=helm.git added first draft for patterns --- diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index 7b849c928..506d43167 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -5,8 +5,10 @@ \usepackage{amssymb,amsmath} \usepackage{hyperref} \usepackage{picins} +\usepackage{color} \usepackage{fancyvrb} +\definecolor{gray}{gray}{0.85} %\newcommand{\logo}[3]{ %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}} %} @@ -53,6 +55,18 @@ \newcommand{\NOTE}[1]{\marginpar{\scriptsize #1}} \newcommand{\TODO}[1]{\textbf{TODO: #1}} +\newsavebox{\tmpxyz} +\newcommand{\sequent}[2]{ + \savebox{\tmpxyz}[0.9\linewidth]{ + \begin{minipage}{0.9\linewidth} + \ensuremath{#1} \\ + --------------------------\\ % come si fa una linea orizzontale? + \ensuremath{#2} + \end{minipage}}\setlength{\fboxsep}{3mm}% + \begin{center} + \fcolorbox{black}{gray}{\usebox{\tmpxyz}} + \end{center}} + \title{The Matita proof assistant} \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi and Stefano Zacchiroli} @@ -113,7 +127,7 @@ none of the advantages of the previous representations). Partially related to this problem, there is the issue of the {\em granularity} of the library: scripts usually comprise small developments with many definitions and theorems, while -proof objects correspond to individual mathemtical items. +proof objects correspond to individual mathematical items. In our case, the choice of the content encoding was eventually dictated by the methodological assumption of offering the information in a @@ -171,7 +185,7 @@ existential variables, used by the disambiguating parser; language; \item an innovative rendering widget, supporting high-quality bidimensional rendering, and semantic selection, i.e. the possibility to select semantically -meaningfull rendering expressions, and to past the respective content into +meaningful rendering expressions, and to past the respective content into a different text area. \NOTE{il widget\\ non ha sel\\ semantica} \end{itemize} @@ -191,10 +205,10 @@ language (\OCAML{}), and the same (script based) authoring philosophy. However, as we shall see, the analogy essentially stops here. In a sense; we like to think of \MATITA{} as the way \COQ{} would -look like if entirely rerwritten from scratch: just to give an +look like if entirely rewritten from scratch: just to give an idea, although \MATITA{} currently supports almost all functionalities of \COQ{}, it links 60'000 lins of \OCAML{} code, against ... of \COQ{} (and -we are convinced that, starting from scratch againg, we could furtherly +we are convinced that, starting from scratch again, we could furtherly reduce our code in sensible way).\NOTE{righe\\\COQ{}} \begin{itemize} @@ -217,7 +231,223 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} \ASSIGNEDTO{csc} \subsection{pattern} -\ASSIGNEDTO{gares} +\ASSIGNEDTO{gares}\\ +Patterns are the textual counterpart of the MathML widget graphical +selection. + +Matita benefits of a graphical interface and a powerful MathML rendering +widget that allows the user to select pieces of the sequent he is working +on. While this is an extremely intuitive way for the user to +restrict the application of a tactic, for example, to some subterms of the +conclusion or some hypothesis, the way this action is recorded to the text +script is not obvious.\\ +In \MATITA{} this issue is addressed by patterns. + +\subsubsection{Pattern syntax} +A pattern is composed of two terms: a $\NT{sequent\_path}$ and a +$\NT{wanted}$. +The former mocks-up a sequent, replacing unwanted subterms with $?$ and +selecting the interesting parts with the placeholder $\%$. +The latter is a term that lives in the context of the placeholders. + +The concrete syntax is reported in table \ref{tab:pathsyn} +\NOTE{uso nomi diversi \\dalla grammatica \\ ma che hanno + senso} +\begin{table} + \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut} +\hrule +\[ +\begin{array}{@{}rcll@{}} + \NT{pattern} & + ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\ + \NT{sequent\_path} & + ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~ + [~\verb+\vdash+~\NT{multipath}~] & \\ + \NT{wanted} & ::= & \NT{term} & \\ + \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\ +\end{array} +\] +\hrule +\end{table} + +\subsubsection{How patterns work} +Patterns mimic the user's selection in two steps. The first one +selects roots (subterms) of the sequent, using the +$\NT{sequent\_path}$, while the second +one searches the $\NT{wanted}$ term starting from these roots. Both are +optional steps, and by convention the empty pattern selects the whole +goal. + +\begin{description} +\item[Phase 1] + concerns only the $[~\verb+in+~\NT{sequent\_path}~]$ + part of the syntax. $\NT{ident}$ is an hypothesis name and + selects the assumption where the following optional $\NT{multipath}$ + will operate. \verb+\vdash+ can be considered the name for the goal. + If the whole pattern is omitted, the whole goal will be selected. + If one or more hypotheses names are given the selection is restricted to + these assumptions. If a $\NT{multipath}$ is omitted the whole + assumption is selected. Remember that the user can be mostly + unaware of this syntax, since the system is able to write down a + $\NT{sequent\_path}$ starting from a visual selection. + \NOTE{Questo ancora non va\\in matita} + + A $\NT{multipath}$ is a CiC term in which a special constant $\%$ + is allowed. + The roots of discharged subterms are marked with $?$, while $\%$ + is used to select roots. The default $\NT{multipath}$, the one that + selects the whole term, is simply $\%$. + Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$ + that respectively select the first argument of an application or + the source of an arrow and the head of the application that is + found in the arrow target. + + The first phase selects not only terms (roots of subterms) but also + their context that will be eventually used in the second phase. + +\item[Phase 2] + plays a role only if the $[~\verb+in match+~\NT{wanted}~]$ + part is specified. From the first phase we have some terms, that we + will see as subterm roots, and their context. For each of these + contexts the $\NT{wanted}$ term is disambiguated in it and the + corresponding root is searched for a subterm $\alpha$-equivalent to + $\NT{wanted}$. The result of this search is the selection the + pattern represents. + +\end{description} + +\noindent +Since the first step is equipotent to the composition of the two +steps, the system uses it to represent each visual selection. +The second step is only meant for the +experienced user that writes patterns by hand, since it really +helps in writing concise patterns as we will see in the +following examples. + +\subsubsection{Examples} +To explain how the first step works let's give an example. Consider +you want to prove the uniqueness of the identity element $0$ for natural +sum, and that you can relay on the previously demonstrated left +injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$. +Typing +\begin{grafite} +theorem valid_name: \forall n,m. m + n = n \to m = O. + intros (n m H). +\end{grafite} +\noindent +leads you to the following sequent +\sequent{ +n:nat\\ +m:nat\\ +H: m + n = n}{ +m=O +} +\noindent +where you want to change the right part of the equivalence of the $H$ +hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$. +\begin{grafite} + change in H:(? ? ? %) with (O + n). +\end{grafite} +\noindent +This pattern, that is a simple instance of the $\NT{sequent\_path}$ +grammar entry, acts on $H$ that has type (without notation) +$(eq~nat~(m+n)~n)$ and discharges the head of the application and the +first two arguments with a $?$ and selects the last argument with +$\%$. The syntax may seem uncomfortable, but the user can simply +select with the mouse the right part of the equivalence and left to the +system the burden of writing down in the script file the corresponding +pattern with $?$ and $\%$ in the right place (expecially where implicit +arguments are hidden by the notation, like the type $nat$ in this +example). + +Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$ +works too and can be done, by the experienced user, writing directly +a simpler pattern that uses the second phase. +\begin{grafite} + change in match n in H with (O + n). +\end{grafite} +\noindent +In this case the $\NT{sequent\_path}$ selects the whole $H$, while +the second phase searches the wanted $n$ inside it by +$\alpha$-equivalence. The resulting +equivalence will be $m+(O+n)=O+n$ since the second phase found two +occurrences of $n$ in $H$ and the tactic changed both. + +Just for completeness the second pattern is equivalent to the +following one, that is less readable but uses only the first phase. +\begin{grafite} + change in H:(? ? (? ? %) %) with (O + n). +\end{grafite} +\noindent + +\subsubsection{Tactics supporting patterns} +In \MATITA{} the following tactics can be restricted to subterms of +the working sequent: simplify, change, fold, unfold, generalize, replace and +rewrite. +\NOTE{attualmente rewrite e \\ fold non supportano \\ phase 2. per +supportarlo\\bisogna far loro trasformare\\il pattern phase1+phase2\\ +in un pattern phase1only\\come faccio nell'ultimo esempio.\\lo si fa +con una pattern\_of(select(pattern))} + +\subsubsection{Comparison with Coq} +Coq has a two diffrent ways of restricting the application of tactis to +subterms of the sequent, both relaying on the same special syntax to identify +a term occurrence. + +The first way is to use this special syntax to specify directly to the +tactic the occurrnces of a wanted term that should be affected, while +the second is to prepare the sequent with another tactic called +pattern and the apply the real tactic. Note that the choice is not +left to the user, since some tactics needs the sequent to be prepared +with pattern and do not accept directly this special syntax. + +The base idea is that to identify a subterm of the sequent we can +write it and say that we want, for example, the third and the fifth +occurce of it (counting from left to right). In our previous example, +to change only the left part of the equivalence, the correct command +is +\begin{grafite} + change n at 2 in H with (O + H) +\end{grafite} +\noindent +meaning that in the hypothesis $H$ the $n$ we want to change is the +second we encounter proceeding from left toright. + +The tactic pattern computes a +$\beta$-expansion of a part of the sequent with respect to some +occurrences of the given term. In the previous example the following +command +\begin{grafite} + pattern n at 2 in H +\end{grafite} +\noindent +would have resulted in this sequent +\begin{grafite} + n : nat + m : nat + H : (fun n0 : nat => m + n = n0) n + ============================ + m = 0 +\end{grafite} +\noindent +where $H$ is $\beta$-expanded over the second $n$ +occurrence. This is a trick to make the unification algorithm ignore +the head of the application (since the unification is essentially +first-order) but normally operate on the arguments. +This works for some tactics, like rewrite and replace, +but for example not for change and other tactics that do not relay on +unification. + +The idea behind this way of identifying subterms in not really far +from the idea behind patterns patterns, but really fails in help using +complex notation, since it relays on the way the user sees the +sequent. Notation can swap arguments, or place them upside-down or +even put them inside a bidimensional matrix. In these cases using the +mouse to select the wanted term is probably the only way to tell the +system exactly what you want to do. + +One of the goals of \MATITA{} is to use modern publishing techiques, and +adopting a method for restricting tactics application domain that discourages +using heavy math notation, would definitively be a bad choice. \subsection{tatticali} \ASSIGNEDTO{gares}