-\documentclass[a4paper]{llncs}
-\pagestyle{headings}
+\documentclass{kluwer}
\usepackage{color}
\usepackage{graphicx}
-\usepackage{amssymb,amsmath}
+% \usepackage{amssymb,amsmath}
\usepackage{hyperref}
-\usepackage{picins}
+% \usepackage{picins}
\usepackage{color}
\usepackage{fancyvrb}
+\usepackage[show]{ed}
\definecolor{gray}{gray}{0.85}
%\newcommand{\logo}[3]{
\fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
\end{center}}
+\newcounter{example}
+\newenvironment{example}{\stepcounter{example}\emph{Example} \arabic{example}.}
+ {}
\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\FILE}[1]{\texttt{#1}}
-\newcommand{\NOTE}[1]{\marginpar{\scriptsize #1}}
+% \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
+\newcommand{\NOTE}[1]{\ednote{x~\hspace{-10cm}y#1}{foo}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\newsavebox{\tmpxyz}
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\end{center}}
+\bibliographystyle{plain}
+
+\begin{document}
+
+\begin{opening}
+
\title{The Matita proof assistant}
+\runningtitle{The Matita proof assistant}
+
\author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
and Stefano Zacchiroli}
+\runningauthor{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
+ and Stefano Zacchiroli}
+
\institute{Department of Computer Science, University of Bologna\\
Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
\email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}
-\bibliographystyle{plain}
-\begin{document}
-\maketitle
+\date{data}
\begin{abstract}
+ abstract qui
\end{abstract}
+\keywords{parole, chiave}
+
+\end{opening}
+
\section{Introduction}
\label{sec:intro}
{\em Matita} is the proof assistant under development by the \HELM{} team
\end{itemize}
\end{itemize}
-\section{Features}
+\section{\HELM{} library(??)}
-\subsection{mathml}
-\ASSIGNEDTO{zack}
-
-\subsection{metavariabili}
-\label{sec:metavariables}
+\subsection{libreria tutta visibile}
\ASSIGNEDTO{csc}
-\subsection{pattern}
-\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 tactics, 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, discharging 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
-conclusion.
-
-\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 (that is not
-trivial, 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{} all the tactics that can be restricted to subterm of the working
-sequent accept the pattern syntax. In particular these tactics are: 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 + n)
-\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.
+\subsection{ricerca e indicizzazione}
+\label{sec:metadata}
+\ASSIGNEDTO{andrea}
-The idea behind this way of identifying subterms in not really far
-from the idea behind patterns, but really fails in extending to
-complex notation, since it relays on a mono-dimensional sequent representation.
-Real math notation places arguments upside-down (like in indexed sums or
-integrations) or even puts 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.
+\subsection{auto}
+\ASSIGNEDTO{andrea}
-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{sostituzioni esplicite vs moduli}
+\ASSIGNEDTO{csc}
-\subsection{tatticali}
+\subsection{xml / gestione della libreria}
\ASSIGNEDTO{gares}
-\begin{verbatim}
-\end{verbatim}
+\section{User Interface (da cambiare)}
+
+\subsection{assenza di proof tree / resa in linguaggio naturale}
+\ASSIGNEDTO{andrea}
\subsection{Disambiguation}
\label{sec:disambiguation}
\ASSIGNEDTO{zack}
-\begin{table}
- \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in
- notation\strut}
-\hrule
-\[
-\begin{array}{@{}rcll@{}}
- \NT{term} & ::= & & \mbox{\bf terms} \\
- & & x & \mbox{(identifier)} \\
- & | & n & \mbox{(number)} \\
- & | & s & \mbox{(symbol)} \\
- & | & \mathrm{URI} & \mbox{(URI)} \\
- & | & \verb+_+ & \mbox{(implicit)}\TODO{sync} \\
- & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
- & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
- & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
- & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
- & | & \NT{term}~\NT{term} & \mbox{(application)} \\
- & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
- & | & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
- & & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
- ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
- & & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
- & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
- & | & \verb+(+~\NT{term}~\verb+)+ \\
- \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
- & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
- \NT{fun} & ::= & & \mbox{\bf functions} \\
- & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
- \NT{binder} & ::= & & \mbox{\bf binders} \\
- & & \verb+\forall+ \mid \verb+\lambda+ \\
- \NT{arg} & ::= & & \mbox{\bf single argument} \\
- & & \verb+_+ \mid x \\
- \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
- & & \NT{arg} \\
- & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
- \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
- & & \NT{arg} \\
- & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
- \NT{kind} & ::= & & \mbox{\bf induction kind} \\
- & & \verb+rec+ \mid \verb+corec+ \\
- \NT{rule} & ::= & & \mbox{\bf rules} \\
- & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
-\end{array}
-\]
-\hrule
-\end{table}
-
\subsubsection{Term input}
The primary form of user interaction employed by \MATITA{} is textual script
\TODO{notazione per i numeri}.
\emph{Operators} (question 3) are intuitively head of applications, as such they
-are always applied to a non empty sequence of arguments. Their ambiguity is a
-need since it is often the case that some notation is used in an overloaded
+are always applied to a (possiblt empty) sequence of arguments. Their ambiguity
+is a need since it is often the case that some notation is used in an overloaded
fashion to hide the use of different CIC constants which encodes similar
concepts. For example, in the standard library of \MATITA{} the infix \texttt{+}
notation is available building a binary \texttt{Op(+)} node, whose
gia' parlato\\
di refine}
-
A \emph{disambiguation algorithm} takes as input a content level term and return
a fully determined CIC term. The key observation on which a disambiguation
algorithm is based is that given a content level term with more than one sources
interpretation of \texttt{1} as the Peano number $1$ can't coexists. The notion
of ``can't coexists'' in the disambiguation of \MATITA{} is inherited from the
refiner described in Sect.~\ref{sec:metavariables}: as long as
-$\mathit{refine}(c)\neq\bot$, the combination of interpretation which led to $c$
+$\mathit{refine}(c)\neq\epsilon$, the combination of interpretation which led to
+$c$
can coexists.
The \emph{naive disambiguation algorithm} takes as input a content level term
interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC term is
fully determined. Iterate over all possible interpretations of $t$ and refine
the corresponding CIC terms, keep only interpretations which lead to CIC terms
- $c$ s.t. $\mathit{refine}(c)\neq\bot$ (i.e. interpretations that determine
+ $c$ s.t. $\mathit{refine}(c)\neq\epsilon$ (i.e. interpretations that determine
typable terms).
\item Let $n$ be the number of interpretations who survived step 2. If $n=0$
The actual algorithm used in \MATITA{} is far more efficient being, in the
average case, linear in the number of ambiguity sources.
+The efficient algorithm --- thoroughly described along with an analysis of its
+complexity in~\cite{disambiguation} --- exploit the refiner and the metavariable
+extension (Sect.~\ref{sec:metavariables}) of the calculus used in \MATITA.
+
\TODO{FINQUI}
The efficient algorithm can be applied if the logic can be extended with
be found in~\cite{disambiguation}, where an equivalent algorithm
that avoids backtracking is also presented.
+
\subsection{notazione}
\label{sec:notation}
\ASSIGNEDTO{zack}
-\subsection{libreria tutta visibile}
-\ASSIGNEDTO{csc}
+\subsection{mathml}
+\ASSIGNEDTO{zack}
-\subsection{ricerca e indicizzazione}
-\label{sec:metadata}
-\ASSIGNEDTO{andrea}
+\subsection{selezione semantica, cut paste, hyperlink}
+\ASSIGNEDTO{zack}
-\subsection{auto}
-\ASSIGNEDTO{andrea}
+\subsection{pattern}
+\ASSIGNEDTO{gares}\\
+Patterns are the textual counterpart of the MathML widget graphical
+selection.
-\subsection{xml / gestione della libreria}
+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 tactics, 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, discharging 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
+conclusion.
+
+\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 (that is not
+trivial, 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{} all the tactics that can be restricted to subterm of the working
+sequent accept the pattern syntax. In particular these tactics are: 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 + n)
+\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, but really fails in extending to
+complex notation, since it relays on a mono-dimensional sequent representation.
+Real math notation places arguments upside-down (like in indexed sums or
+integrations) or even puts 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}
-\subsection{named variable}
+\subsection{named variable e disambiguazione lazy}
\ASSIGNEDTO{csc}
-\subsection{assenza di proof tree / resa in linguaggio naturale}
-\ASSIGNEDTO{andrea}
+\subsection{metavariabili}
+\label{sec:metavariables}
+\ASSIGNEDTO{csc}
-\subsection{selezione semantica, cut paste, hyperlink}
-\ASSIGNEDTO{zack}
+\begin{verbatim}
-\subsection{sostituzioni esplicite vs moduli}
-\ASSIGNEDTO{csc}
+\end{verbatim}
\section{Drawbacks, missing, \dots}
\subsection{localizzazione errori}
\ASSIGNEDTO{}
-\textbf{Acknowledgements}
+\acknowledgements
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to
the development of Matita, and in particular
A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
V.Tamburrelli.
+\theendnotes
+
\bibliography{matita}
+
\end{document}
projects / helm.git / blobdiff