\newcommand{\COQIDE}{CoqIde}
\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\GDOME}{Gdome}
+\newcommand{\GTK}{GTK+}
\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IR}{\ensuremath{\dR}}
\newcommand{\IZ}{\ensuremath{\dZ}}
\newcommand{\LIBXSLT}{LibXSLT}
+\newcommand{\LEGO}{Lego}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATHML}{MathML}
\MATITA{} is the Proof Assistant under development by the \HELM{}
team~\cite{mkm-helm} at the University of Bologna, under the direction of
-Prof.~Asperti. The paper describes the overall architecture of
+Prof.~Asperti. This paper describes the overall architecture of
the system, focusing on its most distinctive and innovative
features.
The origins of \MATITA{} go back to 1999. At the time we were mostly
interested to develop tools and techniques to enhance the accessibility
-via Web of formal libraries of mathematics. Due to its dimension, the
+via Web of libraries of formal mathematics. Due to its dimension, the
library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
was chosen as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably
-with \NUPRL~\cite{nuprl-book}.
+with \NUPRL~\cite{nuprl-book}.\TODO{citare la tesi di vincenzo(?)}
The work, mostly performed in the framework of the recently concluded
European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the
following steps:
-\begin{itemize}
-\item exporting the information from the internal representation of
- \COQ{} to a system and platform independent format. Since XML was at the
-time an emerging standard, we naturally adopted this technology, fostering
-a content-centric architecture~\cite{content-centric} where the documents
-of the library were the the main components around which everything else
-has to be build;
-\item developing indexing and searching techniques supporting semantic
- queries to the library;
-\item developing languages and tools for a high-quality notational
-rendering of mathematical information\footnote{We have been
-active in the \MATHML{} Working group since 1999.};
-\end{itemize}
+\begin{enumerate}
+
+ \item exporting the information from the internal representation of
+ \COQ{} to a system and platform independent format. Since XML was at
+ the time an emerging standard, we naturally adopted that technology,
+ fostering a content-centric architecture~\cite{content-centric} where
+ the documents of the library were the the main components around which
+ everything else has to be build;
+
+ \item developing indexing and searching techniques supporting semantic
+ queries to the library;
+
+ \item developing languages and tools for a high-quality notational
+ rendering of mathematical information.\footnote{We have been active in
+ the \MATHML{} Working group since 1999.}
+
+\end{enumerate}
According to our content-centric commitment, the library exported from
\COQ{} was conceived as being distributed and most of the tools were developed
-as Web services. The user could interact with the library and the tools by
+as Web services. The user can interact with the library and the tools by
means of a Web interface that orchestrates the Web services.
-The Web services and the other tools have been implemented as front-ends
+Web services and other tools have been implemented as front-ends
to a set of software components, collectively called the \HELM{} components.
At the end of the \MOWGLI{} project we already disposed of the following
tools and software components:
\begin{itemize}
-\item XML specifications for the Calculus of Inductive Constructions,
-with components for parsing and saving mathematical objects in such a
-format~\cite{exportation-module};
-\item metadata specifications with components for indexing and querying the
-XML knowledge base;
-\item a proof checker library (i.e. the {\em kernel} of a proof assistant),
-implemented to check that we exported from the \COQ{} library all the
-logically relevant content;
-\item a sophisticated parser (used by the search engine), able to deal
-with potentially ambiguous and incomplete information, typical of the
-mathematical notation~\cite{disambiguation};
-\item a {\em refiner} library, i.e. a type inference system, based on
-partially specified terms, used by the disambiguating parser;
-\item complex transformation algorithms for proof rendering in natural
-language~\cite{remathematization};
-\item an innovative, \MATHML-compliant rendering widget for the GTK
-graphical environment~\cite{padovani}, supporting
-high-quality bidimensional
-rendering, and semantic selection, i.e. the possibility to select semantically
-meaningful rendering expressions, and to paste the respective content into
-a different text area.
+
+ \item XML specifications for the Calculus of Inductive Constructions,
+ with components for parsing and saving mathematical objects in such a
+ format~\cite{exportation-module};
+
+ \item metadata specifications with components for indexing and querying the
+ XML knowledge base;
+
+ \item a proof checker (i.e. the \emph{kernel} of a proof assistant),
+ implemented to check that we exported from the \COQ{} library all the
+ logically relevant content;
+
+ \item a sophisticated term parser (used by the search engine), able to deal
+ with potentially ambiguous and incomplete information, typical of the
+ mathematical notation~\cite{disambiguation};
+
+ \item a \emph{refiner} component, i.e. a type inference system, based on
+ partially specified terms, used by the disambiguating parser;
+
+ \item complex transformation algorithms for proof rendering in natural
+ language~\cite{remathematization};
+
+ \item an innovative, \MATHML-compliant rendering widget~\cite{padovani}
+ for the \GTK{} graphical environment,\footnote{\url{http://www.gtk.org/}}
+ supporting high-quality bidimensional
+ rendering, and semantic selection, i.e. the possibility to select semantically
+ meaningful rendering expressions, and to paste the respective content into
+ a different text area.
+
\end{itemize}
+
Starting from all this, developing our own proof assistant was not
too far away: essentially, we ``just'' had to
add an authoring interface, and a set of functionalities for the
Church enriched with primitive inductive and co-inductive data types.
Via the Curry-Howard isomorphism, the calculus can be seen as a very
rich higher order logic and proofs can be simply represented and
-stored as lambda-terms. \COQ{} and Lego are other systems that adopt
-(variations of) CIC as their foundation.
+stored as lambda-terms. \COQ{} and \LEGO~\cite{lego} are other systems
+that adopt (variations of) CIC as their foundation.
The proof language of \MATITA{} is procedural, in the tradition of the LCF
-theorem prover. \COQ, \NUPRL, PVS, Isabelle are all examples of others systems
+theorem prover~\cite{lcf}. \COQ, \NUPRL, PVS, Isabelle are all examples of
+others systems
whose proof language is procedural. Traditionally, in a procedural system
the user interacts only with the \emph{script}, while proof terms are internal
records kept by the system. On the contrary, in \MATITA{} proof terms are
-praised as declarative versions of the proof. With this role, they are the
+praised as declarative versions of the proof. Playing that role, they are the
primary mean of communication of proofs (once rendered to natural language
for human audiences).
above than the result of a deliberate design. In particular, we
(essentially) share the same foundational dialect of \COQ{} (the
Calculus of (Co)Inductive Constructions), the same implementation
-language (\OCAML{}), and the same (script based) authoring philosophy.
-However, the analogy essentially stops here and no code is shared by the
-two systems.
+language (\OCAML\footnote{\url{http://caml.inria.fr/}}),
+and the same (procedural, script based) authoring philosophy.
+However, the analogy essentially stops here and no code is shared
+between the two systems.
In a sense, we like to think of \MATITA{} as the way \COQ{} would
look like if entirely rewritten from scratch: just to give an
idea, although \MATITA{} currently supports almost all functionalities of
\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
by \COQ{} (and we are convinced that, starting from scratch again,
-we could reduce our code even further in sensible way).
+we could reduce our code even further in a sensible way).
Moreover, the complexity of the code of \MATITA{} is greatly reduced with
respect to \COQ. For instance, the API of the components of \MATITA{} comprise
The size and complexity improvements over \COQ{} must be understood
historically. \COQ{} is a quite old
-system whose development started 20 years ago. Since then
+system whose development started 20 years ago. Since then,
several developers have took over the code and several new research ideas
that were not considered in the original architecture have been experimented
and integrated in the system. Moreover, there exists a lot of developments
\end{figure}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
-(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
-project. Each node is annotated with the number of lines of source code
-(comprising comments).
+(circle nodes) and \emph{applications} (squared nodes) developed in the
+\HELM{} project. Each node is annotated with the number of lines of
+source code (comprising comments).
-Applications and \components{} depend over other \components{} forming a
+Applications and \components{} depend on other \components{} forming a
directed acyclic graph (DAG). Each \component{} can be decomposed in
-a a set of \emph{modules} also forming a DAG.
+a set of \emph{modules} also forming a DAG.
Modules and \components{} provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
Only the proof assistant \MATITA{} and the \WHELP{} search engine are
applications meant to be used directly by the user. All the other applications
-are Web services developed in the HELM and MoWGLI projects and already described
-elsewhere. In particular:
+are Web services developed in the \HELM{} and \MOWGLI{} projects and already
+described elsewhere. In particular:
\begin{itemize}
- \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
- from a physical location (URL) given its logical name (URI). The Getter is
- responsible of updating a table that maps URIs to URLs. Thanks to the Getter
- it is possible to work on a logically monolithic library that is physically
- distributed on the network. More information on the Getter can be found
- in~\cite{zack-master}.
- \item \emph{\WHELP} is a search engine to index and locate mathematical
- notions (axioms, theorems, definitions) in the logical library managed
- by the Getter. Typical examples of a query to Whelp are queries that search
- for a theorem that generalize or instantiate a given formula, or that
- can be immediately applied to prove a given goal. The output of Whelp is
- an XML document that lists the URIs of a complete set of candidates that
- are likely to satisfy the given query. The set is complete in the sense
- that no notion that actually satisfies the query is thrown away. However,
- the query is only approximated in the sense that false matches can be
- returned. Whelp has been described in~\cite{whelp}.
- \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
- notion in the distributed library, renders it according to the user provided
- two dimensional mathematical notation. \UWOBO{} may also embed the rendering
- of mathematical notions into arbitrary documents before returning them.
- The Getter is used by \UWOBO{} to retrieve the document to be rendered.
- \UWOBO{} has been described in~\cite{zack-master}.
- \item The \emph{Proof Checker} is a Web service that, given the URI of
- notion in the distributed library, checks its correctness. Since the notion
- is likely to depend in an acyclic way over other notions, the proof checker
- is also responsible of building in a top-down way the DAG of all
- dependencies, checking in turn every notion for correctness.
- The proof checker has been described in~\cite{zack-master}.
- \item The \emph{Dependency Analyzer} is a Web service that can produce
- a textual or graphical representation of the dependencies of an object.
- The dependency analyzer has been described in~\cite{zack-master}.
+
+ \item The \emph{\GETTER}~\cite{zack-master} is a Web service to
+ retrieve an (XML) document from a physical location (URL) given its
+ logical name (URI). The Getter is responsible of updating a table that
+ maps URIs to URLs. Thanks to the Getter it is possible to work on a
+ logically monolithic library that is physically distributed on the
+ network.
+
+ \item \emph{\WHELP}~\cite{whelp} is a search engine to index and
+ locate mathematical concepts (axioms, theorems, definitions) in the
+ logical library managed by the Getter. Typical examples of
+ \WHELP{} queries are those that search for a theorem that generalize or
+ instantiate a given formula, or that can be immediately applied to
+ prove a given goal. The output of Whelp is an XML document that lists
+ the URIs of a complete set of candidates that are likely to satisfy
+ the given query. The set is complete in the sense that no concept that
+ actually satisfies the query is thrown away. However, the query is
+ only approximated in the sense that false matches can be returned.
+
+ \item \emph{\UWOBO}~\cite{zack-master} is a Web service that, given the
+ URI of a mathematical concept in the distributed library, renders it
+ according to the user provided two dimensional mathematical notation.
+ \UWOBO{} may also inline the rendering of mathematical concepts into
+ arbitrary documents before returning them. The Getter is used by
+ \UWOBO{} to retrieve the document to be rendered.
+
+ \item The \emph{Proof Checker}~\cite{zack-master} is a Web service
+ that, given the URI of a concept in the distributed library, checks its
+ correctness. Since the concept is likely to depend in an acyclic way
+ on other concepts, the proof checker is also responsible of building
+ in a top-down way the DAG of all dependencies, checking in turn every
+ concept for correctness.
+
+ \item The \emph{Dependency Analyzer}~\cite{zack-master} is a Web
+ service that can produce a textual or graphical representation of the
+ dependencies of a concept.
+
\end{itemize}
The dependency of a \component{} or application over another \component{} can
be satisfied by linking the \component{} in the same executable.
For those \components{} whose functionalities are also provided by the
aforementioned Web services, it is also possible to link stub code that
-forwards the request to a remote Web service. For instance, the Getter
-is just a wrapper to the \GETTER{} \component{} that allows the
-\component{} to be used as a Web service. \MATITA{} can directly link the code
-of the \GETTER{} \component, or it can use a stub library with the same
-API that forwards every request to the Getter.
+forwards the request to a remote Web service. For instance, the
+\GETTER{} application is just a wrapper to the \GETTER{} \component{}
+that allows it to be used as a Web service. \MATITA{} can directly link
+the code of the \GETTER{} \component, or it can use a stub library with
+the same API that forwards every request to the Web service.
To better understand the architecture of \MATITA{} and the role of each
-\component, we can focus on the representation of the mathematical information.
-\MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
-Constructions (CIC). In CIC terms are used to represent mathematical
-formulae, types and proofs. \MATITA{} is able to handle terms at
-four different levels of specification. On each level it is possible to provide
-a different set of functionalities. The four different levels are:
-fully specified terms; partially specified terms;
-content level terms; presentation level terms.
+\component, we can focus on the representation of the mathematical
+information. In CIC terms are used to represent mathematical formulae,
+types and proofs. \MATITA{} is able to handle terms at four different
+levels of specification. On each level it is possible to provide a
+different set of functionalities. The four different levels are: fully
+specified terms; partially specified terms; content level terms;
+presentation level terms.
\subsection{Fully specified terms}
\label{sec:fullyintro}
\emph{Fully specified terms} are CIC terms where no information is
missing or left implicit. A fully specified term should be well-typed.
- The mathematical notions (axioms, definitions, theorems) that are stored
+ The mathematical concepts (axioms, definitions, theorems) that are stored
in our mathematical library are fully specified and well-typed terms.
Fully specified terms are extremely verbose (to make type-checking
decidable). Their syntax is fixed and does not resemble the usual
consumption.
The \texttt{cic} \component{} defines the data type that represents CIC terms
- and provides a parser for terms stored in an XML format.
+ and provides a parser for terms stored in XML format.
The most important \component{} that deals with fully specified terms is
\texttt{cic\_proof\_checking}. It implements the procedure that verifies
\emph{conversion} judgement that verifies if two given terms are
computationally equivalent (i.e. they share the same normal form).
- Terms may reference other mathematical notions in the library.
+ Terms may reference other mathematical concepts in the library.
One commitment of our project is that the library should be physically
distributed. The \GETTER{} \component{} manages the distribution,
providing a mapping from logical names (URIs) to the physical location
- of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
+ of a concept (an URL). The \texttt{urimanager} \component{} provides the URI
data type and several utility functions over URIs. The
\texttt{cic\_proof\_checking} \component{} calls the \GETTER{}
\component{} every time it needs to retrieve the definition of a mathematical
- notion referenced by a term that is being type-checked.
+ concept referenced by a term that is being type-checked.
- The Proof Checker is the Web service that provides an interface
+ The Proof Checker application is the Web service that provides an interface
to the \texttt{cic\_proof\_checking} \component.
- We use metadata and a sort of crawler to index the mathematical notions
- in the distributed library. We are interested in retrieving a notion
+ We use metadata and a sort of crawler to index the mathematical concepts
+ in the distributed library. We are interested in retrieving a concept
by matching, instantiation or generalization of a user or system provided
mathematical formula. Thus we need to collect metadata over the fully
specified terms and to store the metadata in some kind of (relational)
database for later usage. The \texttt{hmysql} \component{} provides
a simplified
- interface to a (possibly remote) MySql database system used to store the
- metadata. The \texttt{metadata} \component{} defines the data type of the
- metadata
+ interface to a (possibly remote) MySQL\footnote{\url{http://www.mysql.com/}}
+ database system used to store the metadata.
+ The \texttt{metadata} \component{} defines the data type of the metadata
we are collecting and the functions that extracts the metadata from the
- mathematical notions (the main functionality of the crawler).
+ mathematical concepts (the main functionality of the crawler).
The \texttt{whelp} \component{} implements a search engine that performs
approximated queries by matching/instantiation/generalization. The queries
operate only on the metadata and do not involve any actual matching
- (that will be described later on and that is implemented in the
- \texttt{cic\_unification} \component). Not performing any actual matching
- the query only returns a complete and hopefully small set of matching
+ (see the \texttt{cic\_unification} \component in
+ Sect.~\ref{sec:partiallyintro}). Not performing any actual matching
+ a query only returns a complete and hopefully small set of matching
candidates. The process that has issued the query is responsible of
actually retrieving from the distributed library the candidates to prune
out false matches if interested in doing so.
- The Whelp search engine is the Web service that provides an interface to
+ The \WHELP{} application is the Web service that provides an interface to
the \texttt{whelp} \component.
According to our vision, the library is developed collaboratively so that
- changing or removing a notion can invalidate other notions in the library.
- Moreover, changing or removing a notion requires a corresponding change
+ changing or removing a concept can invalidate other concepts in the library.
+ Moreover, changing or removing a concept requires a corresponding change
in the metadata database. The \texttt{library} \component{} is responsible
of preserving the coherence of the library and the database. For instance,
- when a notion is removed, all the notions that depend on it and their
+ when a concept is removed, all the concepts that depend on it and their
metadata are removed from the library. This aspect will be better detailed
in Sect.~\ref{sec:libmanagement}.
a sequent. The formers are called \emph{implicit terms} and they occur only
linearly. The latters may occur multiple times and are called
\emph{metavariables}. An \emph{explicit substitution} is applied to each
-occurrence of a metavariable. A metavariable stand for a term whose type is
+occurrence of a metavariable. A metavariable stands for a term whose type is
given by the conclusion of the sequent. The term must be closed in the
context that is given by the ordered list of hypotheses of the sequent.
The explicit substitution instantiates every hypothesis with an actual
Partially specified terms are not required to be well-typed. However a
partially specified term should be \emph{refinable}. A \emph{refiner} is
a type-inference procedure that can instantiate implicit terms and
-metavariables and that can introduce \emph{implicit coercions} to make a
+metavariables and that can introduce
+\emph{implicit coercions}~\cite{barthe95implicit} to make a
partially specified term well-typed. The refiner of \MATITA{} is implemented
in the \texttt{cic\_unification} \component. As the type checker is based on
the conversion check, the refiner is based on \emph{unification} that is
to communicate formulae with the user and with external tools, it seems good
practice to stick to the usual imprecise mathematical ontology. In the
Mathematical Knowledge Management community this imprecise language is called
-the \emph{content level} representation of formulae.
+the \emph{content level}~\cite{adams} representation of formulae.
-In \MATITA{} we provide two translations: from partially specified terms
+In \MATITA{} we provide translations from partially specified terms
to content level terms and the other way around. The first translation can also
be applied to fully specified terms since a fully specified term is a special
case of partially specified term where no metavariable or implicit term occurs.
adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
isomorphic to it. Terms that represent formulae are translated to \MATHML{}
Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
-for the representation of content level formulae in an XML extensible format.
+for the representation of content level formulae in an extensible XML format.
The translation to content level is implemented in the
\texttt{acic\_content} \component. Its input are \emph{annotated partially
proofs and terms that represent formulae. Part of it is also stored at the
content level since it is required to generate the natural language rendering
of proofs. The terms need to be maximally unshared (i.e. they must be a tree
-and not a DAG). The reason is that to the occurrences of a subterm in
-two different positions we need to associate different typing informations.
+and not a DAG). The reason is that to different occurrences of a subterm
+we need to associate different typing information.
This association is made easier when the term is represented as a tree since
it is possible to label each node with an unique identifier and associate
the typing information using a map on the identifiers.
is guided by an \emph{interpretation}, that is a function that chooses for
every ambiguous formula one partially specified term. The
\texttt{cic\_disambiguation} \component{} implements the
-disambiguation algorithm we presented in~\cite{disambiguation} that is
-responsible of building in an efficient way the set of all ``correct''
+disambiguation algorithm presented in~\cite{disambiguation} that is
+responsible of building in an efficient way the set of all correct
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
-In Sect.~\ref{sec:partiallyintro} the last section we described the semantics of
+In Sect.~\ref{sec:partiallyintro} we described the semantics of
a command as a
-function from status to status. We also suggested that the formulae in a
+function from status to status. We also hinted that the formulae in a
command are encoded as partially specified terms. However, consider the
command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
The elegant solution we have implemented consists in representing terms
in a command as functions from a context to a partially refined term. The
function is obtained by partially applying our disambiguation function to
-the content term to be disambiguated. Our solution should be compared with
+the content level term to be disambiguated. Our solution should be compared with
the one adopted in the \COQ{} system, where ambiguity is only relative to
De Brujin indexes.
-In \COQ{} variables can be bound either by name or by position. A term
+In \COQ, variables can be bound either by name or by position. A term
occurring in a command has all its variables bound by name to avoid the need of
-a context during disambiguation. Moreover, this makes more complex every
+a context during disambiguation. This makes more complex every
operation over terms (i.e. according to our architecture every module that
depends on \texttt{cic}) since the code must deal consistently with both kinds
-of binding. Also, this solution cannot cope with other forms of ambiguity (as
-the context dependent meaning of the exponent in the previous example).
+of binding. Moreover, this solution cannot cope with other forms of ambiguity
+(as the context dependent meaning of the exponent in the previous example).
\subsection{Presentation level terms}
\label{sec:presentationintro}
level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
\GTKMATHVIEW{}
widget developed by Luca Padovani~\cite{padovani}. The widget is
-particularly interesting since it allows to implement \emph{semantic
+particularly interesting since it allows the implementation of \emph{semantic
selection}.
Semantic selection is a technique that consists in enriching the presentation
Once the rendering of a lower level term is
selected it is possible for the application to retrieve the pointer to the
lower level term. An example of applications of semantic selection is
-\emph{semantic cut\&paste}: the user can select an expression and paste it
+\emph{semantic copy \& paste}: the user can select an expression and paste it
elsewhere preserving its semantics (i.e. the partially specified term),
possibly performing some semantic transformation over it (e.g. renaming
variables that would be captured or lambda-lifting free variables).
axioms, definitions) and notation. The concepts are authored sequentially
using scripts that are (ordered) sequences of procedural commands.
However, once they are produced we store them independently in the library.
-The only relation implicitly kept between the notions are the logical,
+The only relation implicitly kept between the concepts are the logical,
acyclic dependencies among them. This way the library forms a global (and
distributed) hypertext.
Scripts are not seen as constituents of the library. They are not published
and indexed, so they cannot be searched or browsed using \HELM{} tools.
However, they play a central role for the maintenance of the library.
-Indeed, once a notion is invalidated, the only way to restore it is to
+Indeed, once a concept is invalidated, the only way to restore it is to
fix the possibly broken script that used to generate it.
Moreover, during the authoring phase, scripts are a natural way to
-group notions together. They also constitute a less fine grained clustering
-of notions for invalidation.
+group concepts together. They also constitute a less fine grained clustering
+of concepts for invalidation.
In the rest of this section we present in more details the functionalities of
\MATITA{} related to library management and exploitation.
rendering.\footnote{This may change with the future release of Proof General
based on Eclipse, but is not yet the case.} The second reason is that we wanted
to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
-as GTK is.
+as \GTK{} is.
Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
featuring two windows. The background one is very like to the Proof General
immediately structure the proof or postpone the structuring.
If you decide for the former you have to apply the branching tactical and write
at once tactics for all the cases. Since the user does not even know the
-generated goals yet, she can only replace all the cases with the identity
+generated goals yet, he can only replace all the cases with the identity
tactic and execute the command, just to receive feedback on the first
-goal. Then she has to go one step back to replace the first identity
+goal. Then he has to go one step back to replace the first identity
tactic with the wanted one and repeat the process until all the
branches are closed.
For instance, reconsider the previous example of a proof by induction.
With step-by-step tacticals the user can apply the induction principle, and just
-open the branching tactical ``\texttt{[}''. Then she can interact with the
+open the branching tactical ``\texttt{[}''. Then he can interact with the
system until the proof of the first case is terminated. After that
``\texttt{|}'' is used to move to the next goal, until all goals are
closed. After the last goal, the user closes the branching tactical with
projects / helm.git / commitdiff