\documentclass{article}

\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage{fullpage}

\author{B.~Barras}
\title{A introduction to syntax of Coq V8}

%% Le _ est un caractère normal
\catcode`\_=13
\let\subscr=_
\def_{\ifmmode\sb\else\subscr\fi}

\def\NT#1{\langle\textit{#1}\rangle}
\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
\def\TERM#1{\textsf{\bf #1}}

\newenvironment{transbox}
  {\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline}
  {\end{tabular}\end{center}}
\def\TRANS#1#2
  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} \\}
\def\TRANSCOM#1#2#3
  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} & #3 \\}

\begin{document}

\maketitle

The goal of this document is to introduce by example to the new syntax of
Coq. It is strongly recommended to read first the definition of the new
syntax, but this document should also be useful for the eager user who wants
to start with the new syntax quickly.


\section{Main changes in terms w.r.t. V7}

\subsection{Identifiers}

The lexical conventions changed: \TERM{_} is not a regular identifier
anymore. It is used in terms as a placeholder for subterms to be inferred
at type-checking, and in patterns as a non-binding variable.

\subsection{Precedence of application}

In the new syntax, parentheses are not really part of the syntax of
application. The precedence of application (10) is tighter than all
prefix and infix notations. It makes ot possible to remove the parentheses
in many contexts.

\begin{transbox}
\TRANS{(A x)->(f x)=(g y)}{A x -> f x = g y}
\TRANS{(f [x]x)}{f (fun x => x)}
\end{transbox}


\subsection{Arithmetics and scopes}

The specialized notation for \TERM{Z} and \TERM{R} (introduced by symbols \TERM{`} and \TERM{``}) have disappeared. They have been replaced by the general notion of scope.

\begin{center}
\begin{tabular}{l|l|l}
type & scope name & key \\
\hline
types & type_scope & \TERM{T} \\
\TERM{bool} & bool_scope & \\
\TERM{nat} & nat_scope & \TERM{N} \\
\TERM{Z} & Z_scope & \TERM{Z} \\
\TERM{R} & R_scope & \TERM{R} \\
\TERM{positive} & positive_scope & \TERM{P}
\end{tabular}
\end{center}

In order to use notations of arithmetics on \TERM{Z}, its scope must be opened with command \verb+Open Scope Z_scope.+ Another possibility is using the scope change notation (\TERM{\%}). The latter notation is to be used when notations of several scopes appear in the same expression.

In examples below, scope changes are not needed if the appropriate scope
has been opened.
\begin{transbox}
\TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}}
\TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}}
\TRANSCOM{(0)}{0}{\textrm{nat_scope}}
\end{transbox}

Below is a table that tells which notation is available in which. The
relative precedences and associativity of operators is the same as in
usual mathematics. See the reference manual for more details. However,
it is important to remember that unlike V7, the type operators for
product and sum are left associative, in order not to clash with
arithmetic operators.

\begin{center}
\begin{tabular}{l|l}
scope & notations \\
\hline
nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\
Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\
R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq ~{}^2$ \\
type_scope & $* ~+$ \\
bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{!!}$
\end{tabular}
\end{center}
(Note: $\leq$ is written \TERM{$<=$}, and the square notation uses iso-latin
character 178)



\subsection{Notation for implicit arguments}

The explicitation of arguments is closer to the \emph{bindings} notation in
tactics.

\begin{transbox}
\TRANS{f 1!x 2!y}{f @1:=x @2:=y}
\TRANS{!f x y}{@f x y}
\end{transbox}


\subsection{Universal quantification}

The universal quantification and dependent product types are now
materialized with the \TERM{forall} keyword before the binders and a
comma after the binders.

The syntax of binders also changed significantly. A binder can simply be
a name when its type can be inferred. In other cases, the name and the type
of the variable are put between parentheses. When several consecutive
variables have the same type, they can be grouped. Finally, if all variables
have the same type parentheses can be omitted.

\begin{transbox}
\TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B}
\TRANS{(x,y:nat)P}{forall (x y :~nat), P ~~\textrm{or}~~ forall x y :~nat, P}
\TRANS{(x,y:nat;z:A)P}{forall (x y :~nat) (z:A), P}
\TRANS{(x,y,z,t:?)P}{forall x y z t, P}
\TRANS{(x,y:nat;z:?)P}{forall (x y :~nat) z, P}
\end{transbox}

\subsection{Abstraction}

The notation for $\lambda$-abstraction follows that of universal
quantification. The binders are surrounded by keyword \TERM{fun}
and $\Rightarrow$ (\verb+=>+ in ascii).

\begin{transbox}
\TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c}
\end{transbox}


\subsection{Pattern-matching}

Beside the usage of the keyword pair \TERM{match}/\TERM{with} instead of
\TERM{Cases}/\TERM{of}, the main change is the notation for the type of
branches and return type. It is no longer written between \TERM{$<$ $>$} before
the \TERM{Cases} keyword, but interleaved with the destructured object.

The idea is that for each destructured object, one may specify a variable
name to tell how the branches type depend on this destructured object (case
of a dependent elimination), and also how they depend on the value of the
arguments of the inductive type of the destructured object. The type of
branches is then given after the keyword \TERM{return}, unless it can be
inferred.

Moreover, when the destructured object is a variable, one may use this
variable in the return type.

\begin{transbox}
\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| (S k) => 1 end}
\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| .. end}
\TRANS{<[n:nat](P n)>Cases T of ... end}{match T as n return P n with ... end}
\TRANS{<[n:nat][p:(even n)]\~{}(odd n)>Cases p of\\~~ ... \\end}{match p in even n return \~{} odd n with\\~~ ...\\end}
\end{transbox}


\subsection{Fixpoints and cofixpoints}

An easier syntax for non-mutual fixpoints is provided, making it very close
to the usual notation for non-recursive functions. The decreasing argument
is now indicated by an annotation between curly braces, regardless of the
binders grouping. The annotation can be omitted if the binders introduce only
one variable. The type of the result can be omitted if inferable.

\begin{transbox}
\TRANS{Fix plus\{plus [n:nat] : nat -> nat :=\\~~ [m]...\}}{fix plus (n m:nat) \{struct n\}: nat := ...}
\TRANS{Fix fact\{fact [n:nat]: nat :=\\
~~Cases n of\\~~~~ O -> (1) \\~~| (S k) => (mult n (fact k)) end\}}{fix fact
  (n:nat) :=\\
~~match n with \\~~~~0 => 1 \\~~| (S k) => n * fact k end}
\end{transbox}

There is a syntactic sugar for non-mutual fixpoints associated to a local
definition:

\begin{transbox}
\TRANS{let f := Fix f \{f [x:A] : T := M\} in\\(g (f y))}{let fix f (x:A) : T := M in\\g (f x)}
\end{transbox}

The same applies to cofixpoints, annotations are not allowed in that case.

\subsection{Notation for type cast}

\begin{transbox}
\TRANS{O :: nat}{0 : nat}
\end{transbox}

\section{Main changes in tactics w.r.t. V7}

The main change is that all tactic names are lowercase. This also holds for
Ltac keywords.

\subsection{Ltac}

Definitions of macros are introduced by \TERM{Ltac} instead of \TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive Definition}.

Rules of a match command are not between square brackets anymore.

Context (understand a term with a placeholder) instantiation \TERM{inst}
became \TERM{context}. Syntax is unified with subterm matching.

\begin{transbox}
\TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]}
\end{transbox}

\subsection{List of arguments}

Since the precedence of application is now very tight, tactics that take
a list of terms would require to put parenthesis around each argument
very often. In the new syntax, terms are separated by commas. Tactics
affected by this change are: \TERM{pattern}, \TERM{unfold}, \TERM{fold},
\TERM{generalize} and the list of dependent bindings of \TERM{apply},
\TERM{elim}, \TERM{case}, \TERM{specialize}, \TERM{left}, \TERM{right},
\TERM{exists}, \TERM{split} and \TERM{constructor}.

\begin{transbox}
\TRANS{Generalize t (f x)}{generalize t, f x}
\TRANS{Apply t with (f x) b (g y)}{apply t with f x, b, g y}
\end{transbox}

\subsection{Occurrences}

Occurences of a term are now listed after the term itself.
\begin{transbox}
\TRANS{Pattern 1 2 (f x) 3 4 d}{pattern (f x) 1 2, d 3 4}
\end{transbox}

\section{Main changes in vernacular commands w.r.t. V7}


\subsection{Binders}

The binders of vernacular commands changed in the same way as those of
fixpoints. This also holds for parameters of inductive definitions.


\begin{transbox}
\TRANS{Definition x [a:A] : T := M}{Definition x (a:A) : T := M}
\TRANS{Inductive and [A,B:Prop]: Prop := \\~~conj : A->B->(and A B)}%
      {Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
\end{transbox}

\subsection{Hints}

The syntax of \emph{extern} hints changed: the pattern and the tactic
to be applied are separated by a \TERM{$\Rightarrow$}.
\begin{transbox}
\TRANS{Extern 4 (toto ?) Apply lemma}{Extern 4 toto _ => Apply lemma}
\end{transbox}

\end{document}