From: Claudio Sacerdoti Coen Date: Fri, 30 May 2003 17:13:42 +0000 (+0000) Subject: Minor modifications to the new session. X-Git-Tag: submitted~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=9098cb78fcc3cd643f170e934905fb3c3019629d Minor modifications to the new session. --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index b79b81a74..2625d6b7d 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -123,6 +123,7 @@ brokers. In Sect. \ref{architecture} we present the architecture of \hbugs{}. + An usage session is shown in Sect. \ref{usage}. Further implementation details are given in Sect. \ref{implementation}. Sect. \ref{tutors} is an overview of the tutors that have been implemented. As usual, the final section of this paper is devoted to conclusions and future works. @@ -237,34 +238,35 @@ \hbugs{} tutors act as MONET services. \section{An \hbugs{} Session Example} +\label{usage} In this section we describe a typical \hbugs{} session. The aim of the session is to solve the following easy exercise: \begin{exercise} -Let $x$ be a generic real numbers. Using the \helm{} proof-engine, +Let $x$ be a generic real number. Using the \helm{} proof-engine, prove that \begin{displaymath} x = \frac{(x+1)*(x+1) - 1 - x*x}{2} \end{displaymath} \end{exercise} -\myincludegraphics{step1}{t}{12cm}{Example session.} - {Example session.} -%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.} -% {Example session, snapshot 2.} - -Let us suppose that the \hbugs{} broker is already running and that several +Let us suppose that the \hbugs{} broker is already running and that the tutors already registered themselves to the broker. When the user starts \texttt{gTopLevel}, the system registers itself to the broker, that sends back the list of available tutors. By default, -\texttt{gTopLevel} notifies the broker its intention of subscribing to every +\texttt{gTopLevel} notifies to the broker its intention of subscribing to every tutor available. The user can always open a configuration window where she is presented the list of available tutors and she can independently subscribe -and unsubscribe each tutor. +and unsubscribe the system to each tutor. + +\myincludegraphics{step1}{t}{12cm}{Example session.} + {Example session.} +%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.} +% {Example session, snapshot 2.} The user can now insert into the system the statement of the theorem and start proving it. Let us suppose that the first step of the user is proving that the denominator 2 is different from 0. Once that this technical result -is proven, the user must prove the goal shown in the upper left corner +is proven, the user must prove the goal shown in the upper right corner of the window in background in Fig. \ref{step1}. While the user is wondering how to proceed in the proof, the tutors are @@ -275,15 +277,14 @@ to produce 23 hints. The first and not very useful hint suggests to proceed in the proof by exchanging the two sides of the equality. The second hint suggests to reduce both sides of the equality to their normal form by using only reductions which are justified by the ring structure of the -real numbers. The two normal forms, though, are so different that the proof is +real numbers; the two normal forms, though, are so different that the proof is not really simplified. All the residual 21 hints suggest to apply one lemma from the distributed -library of \helm{}. +library of \helm{}. The user can look at the statement of the lemma by clicking +on its URI. -The user can look at the list of suggestions and realize that a good one is -that of applying the lemma \texttt{r\_Rmult\_mult} which -allow\footnote{The user can always look at -the statement of a theorem by clicking on its URI.} to multiply both equality +The user can now look at the list of suggestions and realize that a good one is +applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality members by the same scalar\footnote{Even if she does not receive the hint, the user probably already knows that this is the right way to proceed. The difficult part where the hint helps is guessing what is the name of the lemma @@ -292,25 +293,26 @@ Double-clicking on the hint automatically applies the lemma, reducing the proof to closing three new goals. The first one asks the user the scalar to use as an argument of the previous lemma; the second one states that the scalar is different from 0; the third lemma (the main -one) asks to prove the equality between the products of the two old members -with the scalar. +one) asks to prove the equality between the two new members. % is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for % the still unkown scalar argument, which can have only $H$ and $x$ as % free variables. The user proceeds by istantiating the scalar with the number 2. The -\texttt{Assumption} tutor now suggests to close the second goal by applying -the hypothesis $H$. No useful suggestions, instead, are generated for the -main goal $2x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$. -To proceed in the proof, indeed, the user needs to symplify the +\texttt{Assumption} tutor now suggests to close the second goal (that +states that $2 \neq 0$) by applying the hypothesis $H$. +No useful suggestions, instead, are generated for the main goal +$2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$. +To proceed in the proof the user needs to symplify the expression using the lemma $Rinv\_r\_simpl\_m$ that states that $\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor suggesting symplifications, the user must find out this symplication by himself. Once she founds it, the goal is reduced to proving that -$2x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the +$2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the \texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is just one of the 22 hints that the user receives. It is the only hint that -does not open new goals.} to the user how to directly finish the proof. +does not open new goals, but the user right now does not have any way to know +that.} to the user how to directly finish the proof. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Comandi da dare a gTopLevel %