Logical inconsistency has never been a problem in the daily work of a
mathematician. The mathematician simply imposes himself a discipline to
restrict himself to consistent subsets of the mathematical knowledge.
-However, in doing so he doesn't choose the subset in advance by forgetting
-the rest of his knowledge.
+However, in doing so he does not choose the subset in advance by forgetting
+the rest of his knowledge. On the contrary he may proceed with a sort of
+top-down strategy: he may always inspect or use part of his knowledge, but
+when he actually does so he should check recursively that inconsistencies are
+not exploited.
+
+Contrarily to the mathematical practice, the usual tendency in the world of
+assisted automation is that of building a logical environment (a consistent
+subset of the library) in a bottom up way, checking the consistency of a
+new axiom or theorem as soon as it is added to the environment. No lemma
+or definition outside the environment can be used until it is added to the
+library after every notion it depends on. Moreover, very often the logical
+environment is the only part of the library that can be inspected,
+that we can search lemmas in and that can be exploited by automatic tactics.
+
+Moving one by one notions from the library to the environment is a costly
+operation since it involves re-checking the correctness of the notion.
+As a consequence mathematical notions are packages into theories that must
+be added to the environment as a whole. However, the consistency problem is
+only raised at the level of theories: theories must be imported in a bottom
+up way and the system must check that no inconsistency arises.
+
+The practice of limiting the scope on the library to the logical environment
+is contrary to our commitment of being able to fully exploit as much as possible
+of the library at any given time. To reconcile the two worlds, we have
+designed \MATITA \ldots \NOTE{Da completare se lo riteniamo un punto interessante.}
+
+\subsubsection{Accessibility}
+A large library that is completely in scope needs effective indexing and
+searching methods to make the user productive. Libraries of formal results
+are particularly critical since they hold a large percentage of technical
+lemmas that do not have a significative name and that must be retrieved
+using advanced methods based on matching, unification, generalization and
+instantiation.
+
+The efficiency of searching inside the library becomes a critical operation
+when automatic tactics exploit the library during the proof search. In this
+scenario the tactics must retrieve a set of candidates for backward or
+forward reasoning in a few milliseconds.
+
+In Sect.~\ref{sec:metadata} we describe the technique adopted in \MATITA.
+
+\subsubsection{Library management}
-Contrarily to a mathematician, the usual tendency in the world of assisted
-automation is that of restricting in advance the part of the library that
-will be used later on, checking its consistency by construction.
\subsection{ricerca e indicizzazione}
\label{sec:metadata}
proofs: tactic based and declarative. We will not investigate the philosophy
aroud the choice that many proof assistant made, \MATITA{} included, and we will not compare the two diffrent approaches. We will describe the common issues of the first one and how \MATITA{} tries to solve them.
-For first we must highlight the fact that proof scripts made using tactis are
-particularly unreadable. This is not a big deal for the user while he iw
+First we must highlight the fact that proof scripts made using tactis are
+particularly unreadable. This is not a big deal for the user while he is
constructing the proof, but is considerably a problem when he tries to reread
-what he did or whe he shows his work to someone else.
+what he did or when he shows his work to someone else.
Another common issue for tactic based proof scripts is their mantenibility.
Huge libraries have been developed, and backward compatibility is a really time
consuming task. This problem is usually ameliorated with tacticals, that
-contibute structuring proofs, but rise one more difficulty for the user that
-want to read a proof, since they are executed in an atomic way, making the
-user loose intermediate steps.
+help in structuring proofs and consequently their maintenance, but have a bad
+counterpart in script readability. Since tacticals are executed atomically,
+the common practice of executing again a script to review all the proof steps
+doesn't work at all. This issue in addition to the really poor feeling that a
+list of tactics gives about the proof makes script rereading particularly hard.
\MATITA{} uses a language of tactics and tacticals, but adopts a peculiar
strategy to make this technique more user friendly without loosing in
\subsubsection{Tacticals overview}
Before describing the peculiarities of \MATITA{} tacticals we briefly introduce what tacticals are and where they can be useful.
-Tacticals first appered in LCF(cita qualcosa) and can be seen as programming constructs, like
-looping, branching, error recovery or sequential composition.
+Tacticals first appered in LCF(cita qualcosa) and can be seen as programming
+constructs, like looping, branching, error recovery or sequential composition.
+For example $tac_1~.~tac_2$ executes the first tactic and applies the second
+only to the first goal opened by $tac_1$. Baranching can be used to specify a
+diffrent tactic to apply to each new goal opened by another tactic, for example
+$tac_1\verb+;[+~tac_{1.1}~\verb+|+~tac_{1.2}~\verb+|+~\cdots~|~tac_{1.n}~\verb+]+$
+applies respectively $tac_{1.i}$ to the $i$-th goal opened by $tac_1$. Looping
+can be used to iterate a tactic until it works: $\verb+repeat+~tac$ applies
+$tac$ to the current goal, and again $tac$ to the eventually resulting goals
+until all goal are closed or the tactic fails.
-\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
\begin{table}
\caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
\hrule
\hrule
\end{table}
+\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
While one whould expect to find structured constructs like
$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
This is essential for base idea behind matita tacticals: step-by-step execution.
\subsubsection{\MATITA{} Tinycals}
-The low-level tacticals implementation of \MATITA{} allows a step-by-step execution of a tactical, that substantially means that a $\NT{block\_kind}$ is not execute as an atomic operation. This has two major benefits for the user, even being a so simple idea:
+The low-level tacticals implementation of \MATITA{} allows a step-by-step execution of a tactical, that substantially means that a $\NT{block\_kind}$ is not executed as an atomic operation. This has two major benefits for the user, even being a so simple idea:
\begin{description}
\item[Proof structuring]
- is much easyer. Consider for example a proof by induction. After applying the
+ is much easyer. Consider for example a proof by induction, and imagine you are using classical tacticals. After applying the
induction principle, with one step tacticals, you have to choose: structure
the proof or not. If you decide for the former you have to branch with
- \verb+[+ and write tactics for all the cases and the close the tactical with
+ \verb+[+ and write tactics for all the cases separated by \verb+|+ and the
+ close the tactical with
\verb+]+. You can replace most of the cases by the identity tactic just to
- concentrate only on the first goal, but you will have to one step back and
+ concentrate only on the first goal, but you will have to go one step back and
one further every time you add something inside the tactical. And if you are
boared of doing so, you will finish in giving up structuring the proof and
- write a plain list of tactics.
+ write a plain list of tactics.\\
+ With step-by-step tacticals you can apply the induction principle, and just
+ open the branching tactical \verb+[+. Then you can interact with the system
+ reaching a proof of the first case, without having to specify the whole
+ branching tactical. When you have proved all the induction cases, you close
+ the branching tactical with \verb+]+ and you are done with a structured proof.
\item[Rereading]
is possible. Going on step by step shows exactly what is going on.
Consider again a proof by induction, that starts applying the induction
- principle and suddenly baranches with a \verb+[+. This clearly subdivided all
+ principle and suddenly baranches with a \verb+[+. This clearly separates all
the induction cases, but if the square brackets content is executed in one
single step you completely loose the possibility of rereading it. Again,
executing step-by-step is the way you whould like to review the
projects / helm.git / blobdiff