\end{figure}
}
-\usepackage[show]{ed}
-\usepackage{draftstamp}
+%\usepackage[show]{ed}
+%\usepackage{draftstamp}
\newcommand{\musing}{\texttt{musing}}
\newcommand{\musings}{\texttt{musings}}
new status are sent to the broker as soon as the proof change (e.g. when the
user applies a tactic or when a new proof is started) and hints are shown to
the user be the means of some effect in the user interface (e.g. popping a
- dialog box or enlightening a tactic button).\ednote{CSC: questo \'e un
- possibile posto dove mettere una reference a una mini-sessione interattiva.
- \'E l'appendice un posto dove metterla?}
-
- \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
- {\hbugs{} \wss{} interfaces}
+ dialog box or enlightening a tactic button).
\hbugs{} clients act as MONET clients and ask brokers to provide access to a
set of services (the tutors). \hbugs{} has no actors corresponding to
Getter.
\paragraph{Brokers}
+ \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
+ {\hbugs{} \wss{} interfaces}
+
Brokers are the key actors of the \hbugs{} architecture since they
act as intermediaries between clients and tutors. They behave as \wss{}
providers and requesters for \emph{both} clients and tutors, see Fig.
\hbugs{} tutors act as MONET services.
\section{An \hbugs{} Session Example}
+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,
+prove that
+\begin{displaymath}
+x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
+\end{displaymath}
+\end{exercise}
+
+\myincludegraphics{step1}{t}{12cm}{Example session, snapshot 1.}
+ {Example session, snapshot 1.}
+%\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
+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
+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.
+
+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
+of the window in background in Fig. \ref{step1}.
+
+While the user is wondering how to proceed in the proof, the tutors are
+trying to progress in the proof. After a while, the tutors' suggestions
+start to appear in the lower part of the \hbugs{} interface window
+(the topmost window in Fig. \ref{prima}). In this case, the tutors are able
+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
+not really simplified.
+All the residual 21 hints suggest to apply one lemma from the distributed
+library of \helm{}.
+
+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
+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
+to apply.}.
+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.
+% 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*\frac{((x+1)*(x+1)-1-x*x)}{2}$.
+To proceed in the proof, indeed, 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
+\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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Comandi da dare a gTopLevel %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% New proof:
+% !x.(not (eqT ? (Rplus R1 R1) R0)) -> (eqT ? x (Rdiv (Rminus (Rminus (Rmult (Rplus x R1) (Rplus x R1)) R1) (Rmult x x)) (Rplus R1 R1)))
+% Intros x H
+% Apply r_Rmult_mult
+% 3: Apply H
+% Simpl (per fare unfold di Rdiv)
+% Rewrite <-
+% (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1)))
+% Rewrite ->
+% (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H)
+% *** Ring
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Implementation's Highlights}
\label{implementation}
exchange status in WSDL using the XML Schema type system, we have chosen an
XML format as the target format for the serialization.
- A schematic representation of the gTopLevel internal status is depicted in
- Fig. \ref{status}. Each proof is represented by a tuple of four elements:
+% A schematic representation of the gTopLevel internal status is depicted in
+% Fig. \ref{status}.
+ Each proof is represented by a tuple of four elements:
\emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
- \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
- status}
+% \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
+% status}
\begin{description}
\item[uri]: an URI chosen by the user at the beginning of the proof
the proof found: the client applies the hint reconstructing (and checking
the correctness of) the proof from the witness, without having to
re-discover the proof itself.
- \ednote{Zack: che ne dici di un "reinvent the whell" qui sopra? fa sempre
- effetto ...}
An alternative implementation where the tutors are trusted would simply
send back to the client a new proof-status. Upon receiving the
\ws{}.
Additionally tutors are required to send an human readable description of
their capabilities; this information could be used by client's user to
- decide which tutors he needs to subscribe to. Like clients\ednote{Zack: mi
- pare che questo sia un caso in cui si debba usare "as" e non like, ma non ne
- sono certo}, tutors can
+ decide which tutors he needs to subscribe to. As the clients, tutors can
unregister from brokers using \texttt{Unregister\_broker} method.
Each time the client status change, it get sent sent to the
broker using its \texttt{Status} method. Using both clients registry (to
lookup client's subscription) and tutors registry (to check if some tutors
has unsubscribed), the broker is able to decide to which tutors the
- new status have to be forwarded.\ednote{CSC: qui o nei lavori futuri parlare
- della possibilit\'a di avere un vero brocker che multiplexi le richieste
- dei client localizzando i servizi, etc.}
+ new status have to be forwarded.
+% \ednote{CSC: qui o nei lavori futuri parlare
+% della possibilit\'a di avere un vero brocker che multiplexi le richieste
+% dei client localizzando i servizi, etc.}
The forwarding operation is performed using the \texttt{Start\_musing}
method of the tutors, that is a request to start a new computation
or more constructors when the goal thesis is an inductive type or a
proposition inductively defined according to the declarative
style\footnote{An example of a proposition that can be given in
- declarative style is the $\le$ relation: $\le$ is the smallest relation
+ declarative style is the $\le$ relation over natural numbers:
+ $\le$ is the smallest relation
such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
of $n \le n$ is simply the application of the first constructor to
$n$ and a proof of $n \le m$ is the application of the second
constructor to $n,m$ and a proof of $n \le m$.}.
- \ednote{Zack: non e' necessario specificare che stai parlando di numeri
- naturali nella footnote?}
Since disjunction, conjunction, existential quantification and
Leibniz equality are particular cases of inductive propositions,
all the other tutors of this class are instantiations of the
projects / helm.git / blobdiff