\newcommand{\component}{component}
\newcommand{\components}{components}
-\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\BOXML}{BoxML}
\newcommand{\COQ}{Coq}
-\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{\IN}{\ensuremath{\dN}}
-\newcommand{\INSTANCE}{\textsc{Instance}}
-\newcommand{\IR}{\ensuremath{\dR}}
-\newcommand{\IZ}{\ensuremath{\dZ}}
-\newcommand{\LIBXSLT}{LibXSLT}
+% \newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\LEGO}{Lego}
-\newcommand{\LOCATE}{\textsc{Locate}}
-\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATHML}{MathML}
\newcommand{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\MOWGLIIST}{IST-2001-33562}
-\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
-\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\NUPRL}{NuPRL}
\newcommand{\OCAML}{OCaml}
-\newcommand{\PROP}{\mathit{Prop}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\REWRITEHINT}{\textsc{RewriteHint}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
the parser for ambiguous mathematical notation.
The size and complexity improvements over \COQ{} must be understood
-historically. \COQ{}\cite{CoqArt} is a quite old
+historically. \COQ~\cite{CoqArt} is a quite old
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
\begin{grafite}
theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
+ \forall x,y,z. x < y \to y < z \to x < z.
\end{grafite}
The symbol \OP{<} is likely to be overloaded in the library
\begin{grafite}
alias symbol "lt" = "integer 'less than'".
theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
+ \forall x,y,z. x < y \to y < z \to x < z.
\end{grafite}
The ``alias'' command in the example sets the preferred alias for the
Consider, for example:
\begin{grafite}
theorem Zlt_mono:
- \forall x, y, k. x < y \to x < y + k.
+ \forall x,y, k. x < y \to x < y + k.
\end{grafite}
No refinable partially specified term corresponds to the preferences:
Consider now the following theorem:
\begin{grafite}
theorem lt_to_Zlt_pos_pos:
- \forall n, m: nat. n < m \to pos n < pos m.
+ \forall n,m: nat. n < m \to pos n < pos m.
\end{grafite}
and assume that there exist in the library aliases for \OP{<} over natural
numbers and over integer numbers. None of the passes described above is able to
Consider the following theorem about derivation:
\begin{grafite}
theorem power_deriv:
- \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+ \forall n: nat, x: R. d x^n dx = n * x^(n - 1).
\end{grafite}
and assume that in the library there is an alias mapping \OP{\^} to a partially
specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
main parameters: the \emph{depth} (whit the obvious meaning), and the
\emph{width} that is the maximum number of (new) open goals allowed at
any instant. \MATITA{} has only one notion of metavariable, corresponding
-to the so called existential variables of Coq; so, \MATITA's \TAC{auto}
+to the so called existential variables of \COQ; so, \MATITA's \TAC{auto}
tactic should be compared with \COQ's \TAC{EAuto} tactic.
Recently we have extended automation with paramodulation based
\begin{grafite}
theorem example2:
- \forall x, y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
+ \forall x,y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
intros; demodulate; reflexivity
qed.
\end{grafite}
Similarly, consider the statement
\begin{grafite}
-\forall n, m: nat. n < m to n \leq m
+\forall n,m: nat. n < m to n \leq m
\end{grafite}
In this case \texttt{lt\_to\_le} is a legal name,
while \texttt{lt\_le} is not.
symmetric property for relations:
\begin{grafite}
definition symmetric \def
- \lambda A: Type. \lambda R. \forall x, y: A.
+ \lambda A: Type. \lambda R. \forall x,y: A.
R x y \to R y x.
\end{grafite}
Then, you may state the symmetry of equality as:
match expression.
A typical example is the following:
\begin{grafite}
-\forall n, m: nat.
+\forall n,m: nat.
match (eqb n m) with
[ true \Rightarrow n = m
- | false \Rightarrow n \neq m]
+ | false \Rightarrow n \neq m ]
\end{grafite}
where \texttt{eqb} is boolean equality.
In this cases, the name can be build starting from the matched
\begin{grafite}
pattern n at 2 in H
\end{grafite}
-would have resulted in this sequent:
+would have resulted in the sequent:
\sequent{n: nat\\m : nat\\H: (fun n0: nat => m + n = n0) n}{m = 0}
where \texttt{H} is $\beta$-expanded over the second \texttt{n}
occurrence.
However, authoring a proof structured with tacticals is annoying.
Consider for example a proof by induction, and imagine you
-are using one of the state of the art graphical interfaces for proof assistant:
-Proof General. After applying the induction principle you have to choose:
+are using one of the state of the art graphical interfaces for proof assistant
+like Proof General. After applying the induction principle you have to choose:
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
projects / helm.git / commitdiff