From: Claudio Sacerdoti Coen Date: Fri, 23 May 2003 11:50:12 +0000 (+0000) Subject: First part of the chapter about tutors. The automatic generation part is X-Git-Tag: submitted~29 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7bb771f1c2c1a08c482a3862f4a7081880484d7f First part of the chapter about tutors. The automatic generation part is still missing. --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index bd1a64768..87e20b3c6 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -224,8 +224,109 @@ \section{???} \label{implementation} -\section{???} +\section{The \hbugs Tutors} \label{tutors} +To test the \hbugs architecture and to assess the utility of a suggestion +engine for the end user, we have implemented several tutors. In particular, +we have investigated three classes of tutors: +\begin{enumerate} + \item \emph{Tutors for beginners}. These are tutors that implement tactics + which are neither computationally expensive nor difficult to understand: + an expert user can always understand if the tactic can be applied or not + withouth having to try it. For example, the following implemented tutors + belong to this class: + \begin{itemize} + \item \emph{Assumption Tutor}: it ends the proof if the thesis is + equivalent\footnote{The equivalence relation is convertibility. In some + cases, expecially when non-trivial computations are involved, the user + is totally unable to figure out the convertibility of two terms. + In these cases the tutor becomes handy also for expert users.} + to one of the hypotheses. + \item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad + adsurdum} if one hypothesis is equivalent to $False$. + \item \emph{Symmetry Tutor}: if the goal thesis is an equality, it + suggests to apply the commutative property. + \item \emph{Left/Right/Exists/Split/Constructor Tutors}: the Constructor + Tutor suggests to proceed in the proof by applying one or more + constructors when the goal thesis is an inductive type or a + proposition inductively defined according to the declarative style. + Since disjunction, conjunction and existential quantifications are + particular cases of inductive propositions, + all the other tutors of this class implements restrictions of the + the Constructor tactic: Left and Right suggest to prove a disjunction + by proving its left/right member; Split reduces the proof of a + conjunction to the two proof of its members; Exists suggests to + prove an existential quantification by providing a + witness\footnote{This task is left to the user.}. + \end{itemize} + Beginners, when first faced with a tactic-based proof-assistant, get + lost quite soon since the set of tactics is large and their names and + semantics must be remembered by heart. Tutorials are provided to guide + the user step-by-step in a few proofs, suggesting the tactics that must + be used. We believe that our beginners tutors can provide an auxiliary + learning tool: after the tutorial, the user is not suddendly left alone + with the system, but she can experiment with variations of the proof given + in the tutorial as much as she like, still getting useful suggestions. + Thus the user is allowed to focus on learning how to do a formal proof + instead of wasting efforts trying to remember the interface to the system. + \item{Tutors for Computationally Expensive Tactics}. Several tactics have + an unpredictable behaviour, in the sense that it is unfeasible to understand + wether they will succeed or they will failt when applied and what will be + their result. Among them, there are several tactics either computationally + expensive or resources consuming. In the first case, the user is not + willing to try a tactic and wait for a long time just to understand its + outcome: she would prefer to keep on concentrating on the proof and + have the tactic applied in background and receive out-of-band notification + of its success. The second case is similar, but the tactic application must + be performed on a remote machine to avoid overloading the user host + with several concurrent resource consuming applications. + + Finally, several complex tactics and in particular all the tactics based + on reflexive techniques depend on a pretty large set of definitions, lemmas + and theorems. When these tactics are applied, the system needs to retrieve + and load all the lemmas. Pre-loading all the material needed by every + tactic can quickly lead to long initialization times and to large memory + footstamps. A specialized tutor running on a remote machine, instead, + can easily pre-load the required theorems. + + As an example of computationally expensive task, we have implemented + a tutor for the \emph{Ring} tactic. The tutor is able to prove an equality + over a ring by reducing both members to a common normal form. The reduction, + which may require some time in complex cases, + is based on the usual commutative, associative and neutral element properties + of a ring. The tactic is implemented using a reflexive technique, which + means that the reduction trace is not stored in the proof-object itself: + the type-checker is able to perform the reduction on-the-fly thanks to + the conversion rules of the system. As a consequence, in the library there + must be stored both the algorithm used for the reduction and the proof of + correctness of the algorithm, based on the ring axioms. This big proof + and all of its lemmas must be retrieved and loaded in order to apply the + tactic. The Ring tutor loads and cache all the required theorems the + first time it is conctacted. + \item{Intelligent Tutors}. Expert users can already benefit from the previous + class of tutors. Nevertheless, to achieve a significative production gain, + they need more intelligent tutors implementing domain-specific theorem + provers or able to perform complex computations. These tutors are not just + plain implementations of tactics or decision procedures, but can be + more complex software agents interacting with third-parties software, + such as proof-planners, CAS or theorem-provers. + + To test the productivity impact of intelligent tutors, we have implemented + a tutor that is interfaced with the HELM + Proof-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that + is able to look for every theorem in the distributed library that can + be applied to proceed in the proof. Even if the tutor deductive power + is extremely limited\footnote{We do not attempt to check if the new goals + obtained applying a lemma can be authomatically proved or, even better, + auhomatically disproved to reject the lemma.}, it is not unusual for + the tutor to come up with precious hints that can save several minutes of + works that would be spent in proving again already proven results or + figuring out where the lemmas could have been stored in the library. +\end{enumerate} + +Once the code that implements a tactic or decision procedure is available, +transforming it into a tutor is not a difficult task, but it is surely +repetitive and error prone. \section{???} \label{conclusions}