diff options
| author | barras | 2003-12-15 11:44:13 +0000 |
|---|---|---|
| committer | barras | 2003-12-15 11:44:13 +0000 |
| commit | 6f798e203b800eddb7688d685cc3ad54c6f27f42 (patch) | |
| tree | d2ea7e90f0aa5ba5cf58238597c58db270057ac8 | |
| parent | a73344798c51422a6f00507c42b0c07b37f3fb7e (diff) | |
doc du traducteur + premiere mise a jour du refman
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8397 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/RefMan-gal.tex | 355 | ||||
| -rwxr-xr-x | doc/RefMan-lib.tex | 423 | ||||
| -rw-r--r-- | doc/RefMan-ltac.tex | 605 | ||||
| -rw-r--r-- | doc/Translator.tex | 416 |
4 files changed, 1088 insertions, 711 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index e27c729ce9..cf918484dd 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -49,8 +49,9 @@ Blanks are ignored but they separate tokens. \paragraph{Comments} Comments in {\Coq} are enclosed between {\tt (*} and {\tt - *)}\index{Comments}, and can be nested. Comments are treated as -blanks. + *)}\index{Comments}, and can be nested. They can contain any +character. However, string literals must be correctly closed. Comments +are treated as blanks. \paragraph{Identifiers and access identifiers} @@ -62,17 +63,16 @@ they are recognized by the following lexical class: \index{ident@\ident} \begin{center} \begin{tabular}{rcl} -{\firstletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{\_}%\op\ml{\$} +{\firstletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{\_}%\op\ml{unicode-letter} \\ {\subsequentletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{0..9}\op\ml{\_}%\op\ml{\$} \op\ml{'} \\ {\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}\\ \end{tabular} \end{center} -Identifiers can contain at most 80 characters, and all characters are -meaningful. In particular, identifiers are case-sensitive. +All characters are meaningful. In particular, identifiers are case-sensitive. Access identifiers, written {\accessident}, are identifiers prefixed -by \verb!.! (dot). They are used in the syntax of qualified +by \verb!.! (dot) without blank. They are used in the syntax of qualified identifiers. \paragraph{Natural numbers and integers} @@ -89,181 +89,184 @@ Numerals are sequences of digits. Integers are numerals optionally preceded by a \paragraph{Strings} Strings are delimited by \verb!"! (double quote), and enclose a -sequence of any characters different from \verb!"! and \verb!\!, or -one of the following sequences -\begin{center} -\begin{tabular}{|l|l|} -\hline -Sequence & Character denoted \\ -\hline -\verb"\\" & backslash (\verb"\") \\ -\verb'\"' & double quote (\verb'"') \\ -\verb"\n" & newline (LF) \\ -\verb"\r" & return (CR) \\ -\verb"\t" & horizontal tabulation (TAB) \\ -\verb"\b" & backspace (BS) \\ -\verb"\"$ddd$ & the character with ASCII code $ddd$ in decimal \\ -\hline -\end{tabular} -\end{center} -Strings can be split on several lines using a backslash (\verb!\!) at -the end of each line, just before the newline. For instance, - -\begin{flushleft} -\begin{small} -\begin{verbatim} -Add LoadPath "/usr/local/coq/\ -contrib/Rocq/LAMBDA". -\end{verbatim} -\end{small} -\end{flushleft} +sequence of any characters different from \verb!"! or the sequence +\verb!""! to denote the double quote character. +%% \begin{center} +%% \begin{tabular}{|l|l|} +%% \hline +%% Sequence & Character denoted \\ +%% \hline +%% \verb"\\" & backslash (\verb"\") \\ +%% \verb'\"' & double quote (\verb'"') \\ +%% \verb"\n" & newline (LF) \\ +%% \verb"\r" & return (CR) \\ +%% \verb"\t" & horizontal tabulation (TAB) \\ +%% \verb"\b" & backspace (BS) \\ +%% \verb"\"$ddd$ & the character with ASCII code $ddd$ in decimal \\ +%% \hline +%% \end{tabular} +%% \end{center} + +%% Strings can be split on several lines using a backslash (\verb!\!) at +%% the end of each line, just before the newline. For instance, + +%% \begin{flushleft} +%% \begin{small} +%% \begin{verbatim} +%% Add LoadPath "/usr/local/coq/\ +%% contrib/Rocq/LAMBDA". +%% \end{verbatim} +%% \end{small} +%% \end{flushleft} -is correctly parsed, and equivalent to +%% is correctly parsed, and equivalent to -\begin{flushleft} -\begin{small} -\begin{verbatim} -Add LoadPath "/usr/local/coq/contrib/Rocq/LAMBDA". -\end{verbatim} -\end{small} -\end{flushleft} +%% \begin{flushleft} +%% \begin{small} +%% \begin{verbatim} +%% Add LoadPath "/usr/local/coq/contrib/Rocq/LAMBDA". +%% \end{verbatim} +%% \end{small} +%% \end{flushleft} \paragraph{Keywords} The following identifiers are reserved keywords, and cannot be employed otherwise: \begin{center} -\begin{tabular}{lllll} +\begin{tabular}{llllll} +\verb!_! & \verb!as! & -\verb!end! & +\verb!cofix! & +\verb!else! & +\verb!end! \\ +\verb!exists! & +\verb!exists2! & +\verb!fix! & +\verb!for! \\ +\verb!forall! & +\verb!fun! & +\verb!if! \\ \verb!in! & -\verb!of! & -\verb!using! \\ +\verb!let! & +\verb!match! & +\verb!mod! & +\verb!return! & +\verb!then! \\ +\verb!using! & \verb!with! & -\verb!Axiom! & -\verb!Cases! & -\verb!CoFixpoint! & -\verb!CoInductive!\\ -\verb!Compile! & -\verb!Definition! & -\verb!Fixpoint! & -\verb!Grammar! & -\verb!Hypothesis! \\ -\verb!Inductive! & -\verb!Load! & -%%\verb!Orelse! & -\verb!Parameter! & -\verb!Proof! & -\verb!Prop! \\ -\verb!Qed! & -\verb!Quit! & +\verb!IF! & +\verb!Prop! & \verb!Set! & -\verb!Syntax! & -\verb!Theorem! \\ -\verb!Type! & -\verb!Variable! & & & +\verb!Type! \\ \end{tabular} \end{center} -Although they are not considered as keywords, it is not advised to use -words of the following list as identifiers: -\begin{center} -\begin{tabular}{lllll} -\verb!Add! & -\verb!AddPath! & -\verb!Abort! & -\verb!Abstraction!& -\verb!All! \\ -\verb!Begin! & -\verb!Cd! & -\verb!Chapter! & -\verb!Check! & -\verb!Compute! \\ -% \verb!Conjectures! \\ que dans Show Conjectures sans conflit avec ident -\verb!Defined! & -\verb!DelPath! & -\verb!Drop! & -\verb!End! & -\verb!Eval! \\ -% \verb!Explain! n'est pas documente -\verb!Extraction! & -\verb!Fact! & -\verb!Focus! & -% \verb!for! n'intervient que pour Scheme ... Induction ... sans conflit -% \verb!Go! n'est pas documente et semble peu robuste aux erreurs -\verb!Goal! & -\verb!Guarded! \\ -\verb!Hint! & -\verb!Immediate! & -\verb!Induction! & -\verb!Infix! & -\verb!Inspect! \\ -\verb!Lemma! & -\verb!Let! & -\verb!LoadPath! & -\verb!Local! & -\verb!Minimality! \\ -\verb!ML! & -\verb!Module! & -\verb!Modules! & -\verb!Mutual! & -% \verb!Node! que dans Show Node sans conflit avec ident -\verb!Opaque! \\ -\verb!Parameters! & -\verb!Print! & -\verb!Pwd! & -\verb!Remark! & -\verb!Remove! \\ -\verb!Require! & -\verb!Reset! & -\verb!Restart! & -\verb!Restore! & -\verb!Resume! \\ -\verb!Save! & -\verb!Scheme! & -% \verb!Script! que dans Show Script sans conflit avec ident -\verb!Search! & -\verb!Section! & -\verb!Show! \\ -\verb!Silent! & -\verb!State! & -\verb!States! & -\verb!Suspend! & -\verb!Syntactic! \\ -\verb!Test! & -\verb!Transparent!& -% \verb!Tree! que dans Show Tree et Explain Proof Tree sans conflit avec id -\verb!Undo! & -\verb!Unset! & -\verb!Unfocus! \\ -\verb!Variables! & -\verb!Write! & & & -\end{tabular} -\end{center} +%% Hard to maintain... + +%% Although they are not considered as keywords, it is not advised to use +%% words of the following list as identifiers: +%% \begin{center} +%% \begin{tabular}{lllll} +%% \verb!Add! & +%% \verb!AddPath! & +%% \verb!Abort! & +%% \verb!Abstraction!& +%% \verb!All! \\ +%% \verb!Begin! & +%% \verb!Cd! & +%% \verb!Chapter! & +%% \verb!Check! & +%% \verb!Compute! \\ +%% % \verb!Conjectures! \\ que dans Show Conjectures sans conflit avec ident +%% \verb!Defined! & +%% \verb!DelPath! & +%% \verb!Drop! & +%% \verb!End! & +%% \verb!Eval! \\ +%% % \verb!Explain! n'est pas documente +%% \verb!Extraction! & +%% \verb!Fact! & +%% \verb!Focus! & +%% % \verb!for! n'intervient que pour Scheme ... Induction ... sans conflit +%% % \verb!Go! n'est pas documente et semble peu robuste aux erreurs +%% \verb!Goal! & +%% \verb!Guarded! \\ +%% \verb!Hint! & +%% \verb!Immediate! & +%% \verb!Induction! & +%% \verb!Infix! & +%% \verb!Inspect! \\ +%% \verb!Lemma! & +%% \verb!Let! & +%% \verb!LoadPath! & +%% \verb!Local! & +%% \verb!Minimality! \\ +%% \verb!ML! & +%% \verb!Module! & +%% \verb!Modules! & +%% \verb!Mutual! & +%% % \verb!Node! que dans Show Node sans conflit avec ident +%% \verb!Opaque! \\ +%% \verb!Parameters! & +%% \verb!Print! & +%% \verb!Pwd! & +%% \verb!Remark! & +%% \verb!Remove! \\ +%% \verb!Require! & +%% \verb!Reset! & +%% \verb!Restart! & +%% \verb!Restore! & +%% \verb!Resume! \\ +%% \verb!Save! & +%% \verb!Scheme! & +%% % \verb!Script! que dans Show Script sans conflit avec ident +%% \verb!Search! & +%% \verb!Section! & +%% \verb!Show! \\ +%% \verb!Silent! & +%% \verb!State! & +%% \verb!States! & +%% \verb!Suspend! & +%% \verb!Syntactic! \\ +%% \verb!Test! & +%% \verb!Transparent!& +%% % \verb!Tree! que dans Show Tree et Explain Proof Tree sans conflit avec id +%% \verb!Undo! & +%% \verb!Unset! & +%% \verb!Unfocus! \\ +%% \verb!Variables! & +%% \verb!Write! & & & +%% \end{tabular} +%% \end{center} \paragraph{Special tokens} The following sequences of characters are special tokens: \begin{center} \begin{tabular}{lllllll} -\verb!|! & +\verb!(! & +\verb!)! & +\verb!{! & +\verb!}! & \verb!:! & +\verb!,! & +\verb!|! \\ +\verb!=>! & +\verb!->! & \verb!:=! & +\verb!@! & +\verb!\%! & +\verb!.(! & +\verb!+! \\ +\verb!-! & +\verb!*! & +\verb!/! & \verb!=! & +\verb!<>! & \verb!>! & -\verb!>>! & -\verb!<>! \\ -\verb!<<! & -\verb!<! & -\verb!->! & +\verb!<! \\ +\verb!.! & \verb!;! & -\verb!#! & -\verb!*! & -\verb!,! \\ -\verb!?! & -\verb!@! & -\verb!::! & -\verb!/! & \verb!<-! & -\verb!=>! & \end{tabular} \end{center} @@ -1029,18 +1032,18 @@ Fixpoint add (n m:nat) {struct n} : nat := end. \end{coq_example} -The {\tt Cases} operator matches a value (here \verb:n:) with the +The {\tt match} operator matches a value (here \verb:n:) with the various constructors of its (inductive) type. The remaining arguments give the respective values to be returned, as functions of the parameters of the corresponding constructor. Thus here when \verb:n: equals \verb:O: we return \verb:m:, and when \verb:n: equals \verb:(S p): we return \verb:(S (add p m)):. -The {\tt Cases} operator is formally described +The {\tt match} operator is formally described in detail in section \ref{Caseexpr}. The system recognizes that in the inductive call {\tt (add p m)} the first argument actually -decreases because it is a {\em pattern variable} coming from {\tt Cases - n of}. +decreases because it is a {\em pattern variable} coming from {\tt match + n with}. \begin{Variants} \item {\tt Fixpoint {\ident} [ {\params} ] : \type$_0$ := @@ -1064,12 +1067,9 @@ error message: Set Printing Depth 50. \end{coq_eval} \begin{coq_example} -Fixpoint wrongplus - (n - - (********** The following is not correct and should produce **********) - (********* Error: Recursive call applied to an illegal term **********) - (* Just to adjust the prompt: *) m:nat) {struct n} : nat := +(********** The following is not correct and should produce **********) +(********* Error: Recursive call to wrongplus ... **********) +Fixpoint wrongplus (n m:nat) {struct n} : nat := match m with | O => n | S p => S (wrongplus n p) @@ -1091,11 +1091,11 @@ Fixpoint plus (n m:nat) {struct m} : nat := The ordinary match operation on natural numbers can be mimicked in the following way. \begin{coq_example*} -Fixpoint nat_match (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} - : C := match n with - | O => f0 - | S p => fS p (nat_match C f0 fS p) - end. +Fixpoint nat_match (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C := + match n with + | O => f0 + | S p => fS p (nat_match C f0 fS p) + end. \end{coq_example*} The recursive call may not only be on direct subterms of the recursive variable {\tt n} but also on a deeper subterm and we can directly @@ -1138,8 +1138,8 @@ Fixpoint tree_size (t:tree) : nat := end with forest_size (f:forest) : nat := match f with - | leaf b => 1%N - | cons t f' => (tree_size t + forest_size f')%N + | leaf b => 1 + | cons t f' => (tree_size t + forest_size f') end. \end{coq_example*} A generic command {\tt Scheme} is useful to build automatically various @@ -1182,12 +1182,9 @@ function does not satisfy the guard condition: Set Printing Depth 50. \end{coq_eval} \begin{coq_example*} -CoFixpoint filter - ( - (********** The following is not correct and should produce **********) - (***************** Error: Unguarded recursive call *******************) - (* Just to adjust the prompt: *) p:nat -> bool) (s:Stream) : - Stream := +(********** The following is not correct and should produce **********) +(***************** Error: Unguarded recursive call *******************) +CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). \end{coq_example*} diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index 1b75c92a35..be1be5ca05 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -28,16 +28,54 @@ This chapter briefly reviews these libraries. This section lists the basic notions and results which are directly available in the standard \Coq\ system -\footnote{These constructions are defined in the +\footnote{Most of these constructions are defined in the {\tt Prelude} module in directory {\tt theories/Init} at the {\Coq} root directory; this includes the modules -% {\tt Core} l'inexplicable let +{\tt Notations}, {\tt Logic}, {\tt Datatypes}, {\tt Specif}, {\tt Peano}, -and {\tt Wf} -plus the module {\tt Logic\_Type}}. +and {\tt Wf}. +Module {\tt Logic\_Type} also makes it in the initial state}. + +\subsection{Notations} \label{Notations} + +This module defines the parsing and pretty-printing of many symbols +(infixes, prefixes, etc.). However, it does not assign a meaning to these +notations. The purpose of this is to define precedence and +associativity of very common notations, and avoid users to use them +with other precedence, which may be confusing. + +\begin{figure} +\begin{center} +\begin{tabular}{|cll|} +\hline +Notation & Precedence & Associativity \\ +\hline +\verb!<->! & 95 & no \\ +\verb!\/! & 85 & right \\ +\verb!/\! & 80 & right \\ +\verb!~! & 75 & right \\ +\verb!=! & 70 & no \\ +\verb!<>! & 70 & no \\ +\verb!<! & 70 & no \\ +\verb!>! & 70 & no \\ +\verb!<=! & 70 & no \\ +\verb!>=! & 70 & no \\ +\verb!+! & 50 & left \\ +\verb!-! & 50 & left \\ +\verb!*! & 40 & left \\ +\verb!/! & 40 & left \\ +\verb!u-! & 35 & right \\ +\verb!u/! & 35 & right \\ +\verb!^! & 30 & left \\ +\hline +\end{tabular} +\end{center} +\caption{Notations in the initial state} +\label{init-notations} +\end{figure} \subsection{Logic} \label{Logic} @@ -105,16 +143,12 @@ First, we find propositional calculus connectives: Set Printing Depth 50. \end{coq_eval} \begin{coq_example*} -Inductive True : - (********** Next parsing errors for /\ and \/ are harmless ***********) (******************* since output is not displayed *******************) -(* Just to adjust the prompt: *) Prop := - I : True. -Inductive False : Prop :=. +Inductive True : Prop := I. +Inductive False : Prop := . Definition not (A: Prop) := A -> False. -Inductive and (A B:Prop) : Prop := - conj : A -> B -> A /\ B. +Inductive and (A B:Prop) : Prop := conj (_:A) (_:B). Section Projections. Variables A B : Prop. Theorem proj1 : A /\ B -> A. @@ -131,8 +165,8 @@ Abort All. \begin{coq_example*} End Projections. Inductive or (A B:Prop) : Prop := - | or_introl : A -> A \/ B - | or_intror : B -> A \/ B. + | or_introl (_:A) + | or_intror (_:B). Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P). Definition IF (P Q R:Prop) := P /\ Q \/ ~ P /\ R. \end{coq_example*} @@ -142,33 +176,29 @@ Definition IF (P Q R:Prop) := P /\ Q \/ ~ P /\ R. Then we find first-order quantifiers: \ttindex{all} -\ttindex{All} \ttindex{ex} -\ttindex{Ex} -\ttindex{EX} +\ttindex{exists} \ttindex{ex\_intro} \ttindex{ex2} -\ttindex{Ex2} +\ttindex{exists2} \ttindex{ex\_intro2} \begin{coq_example*} Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := - ex_intro : forall x:A, P x -> ex A P. + ex_intro (x:A) (_:P x). Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop := - ex_intro2 : forall x:A, P x -> Q x -> ex2 A P Q. + ex_intro2 : (x:A) (_:P x) (_:Q x). \end{coq_example*} The following abbreviations are allowed: \begin{center} \begin{tabular}[h]{|l|r|} \hline - \verb+(ALL x:A | P)+ & \verb+(all A [x:A]P)+ \\ - \verb+(ALL x | P)+ & \verb+(all A [x:A]P)+ \\ - \verb+(EX x:A | P)+ & \verb+(ex A [x:A]P)+ \\ - \verb+(EX x | P)+ & \verb+(ex A [x:A]P)+ \\ - \verb+(EX x:A | P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\ - \verb+(EX x | P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\ + \verb+(exists x:A | P)+ & \verb+(ex A [x:A]P)+ \\ + \verb+(exists x | P)+ & \verb+(ex A [x:A]P)+ \\ + \verb+(exists2 x:A | P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\ + \verb+(exists2 x | P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\ \hline \end{tabular} \end{center} @@ -180,7 +210,7 @@ synthesized by the system. \index{Equality} Then, we find equality, defined as an inductive relation. That is, -given a \verb:Set: \verb:A: and an \verb:x: of type \verb:A:, the +given a \verb:Type: \verb:A: and an \verb:x: of type \verb:A:, the predicate \verb:(eq A x): is the smallest one which contains \verb:x:. This definition, due to Christine Paulin-Mohring, is equivalent to define \verb:eq: as the smallest reflexive relation, and it is also @@ -190,7 +220,7 @@ equivalent to Leibniz' equality. \ttindex{refl\_equal} \begin{coq_example*} -Inductive eq (A:Set) (x:A) : A -> Prop := +Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : eq A x x. \end{coq_example*} @@ -211,20 +241,13 @@ Abort. \ttindex{sym\_not\_eq} \begin{coq_example*} Section equality. -Variables A B : - Set. -Variable f : - A -> B. -Variables x y z : - A. -Theorem sym_eq : - x = y -> y = x. -Theorem trans_eq : - x = y -> y = z -> x = z. -Theorem f_equal : - x = y -> f x = f y. -Theorem sym_not_eq : - x <> y -> y <> x. +Variables A B : Type. +Variable f : A -> B. +Variables x y z : A. +Theorem sym_eq : x = y -> y = x. +Theorem trans_eq : x = y -> y = z -> x = z. +Theorem f_equal : x = y -> f x = f y. +Theorem sym_not_eq : x <> y -> y <> x. \end{coq_example*} \begin{coq_eval} Abort. @@ -240,11 +263,11 @@ Abort. \begin{coq_example*} End equality. Definition eq_ind_r : - forall (A:Set) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. + forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. Definition eq_rec_r : - forall (A:Set) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. + forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. Definition eq_rect_r : - forall (A:Set) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y. + forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y. \end{coq_example*} \begin{coq_eval} Abort. @@ -253,7 +276,7 @@ Abort. \end{coq_eval} %Abort (for now predefined eq_rect) \begin{coq_example*} -Hints Immediate sym_eq sym_not_eq : core. +Hint Immediate sym_eq sym_not_eq : core. \end{coq_example*} \ttindex{f\_equal$i$} @@ -263,7 +286,7 @@ arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3}, For instance {\tt f\_equal3} is defined the following way. \begin{coq_example*} Theorem f_equal3 : - forall (A1 A2 A3 B:Set) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) + forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. \end{coq_example*} \begin{coq_eval} @@ -296,17 +319,10 @@ again defined as inductive constructions over the sort \ttindex{None} \begin{coq_example*} -Inductive unit : Set := - tt : unit. -Inductive bool : Set := - | true : bool - | false : bool. -Inductive option (A:Set) : Set := - | Some : A -> option A - | None : option A. -Inductive nat : Set := - | O : nat - | S : nat -> nat. +Inductive unit : Set := tt. +Inductive bool : Set := true | false. +Inductive nat : Set := O | S (n:nat). +Inductive option (A:Set) : Set := Some (_:A) | None. \end{coq_example*} Note that zero is the letter \verb:O:, and {\sl not} the numeral @@ -325,29 +341,19 @@ We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and \ttindex{pair} \ttindex{fst} \ttindex{snd} -\ttindex{Fst} -\ttindex{Snd} \begin{coq_example*} -Inductive sum (A B:Set) : Set := - | inl : A -> sum A B - | inr : B -> sum A B. -Inductive prod (A B:Set) : Set := - pair : A -> B -> prod A B. +Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B). +Inductive prod (A B:Set) : Set := pair (_:A) (_:B). Section projections. -Variables A B : - Set. -Definition fst (H: - prod A B) := match H with +Variables A B : Set. +Definition fst (H: prod A B) := match H with | pair x y => x end. -Definition snd (H: - prod A B) := match H with +Definition snd (H: prod A B) := match H with | pair x y => y end. End projections. -Notation Fst := (fst _ _). -Notation Snd := (snd _ _). \end{coq_example*} \subsection{Specification} @@ -359,13 +365,13 @@ figure \ref{specif-syntax}\footnote{This syntax can be found in the module {\tt SpecifSyntax.v}}. For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct -\verb+{x:A | (P x)}+ (in abstract syntax \verb+(sig A P)+) is a +\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a \verb:Set:. We may build elements of this set as \verb:(exist x p): whenever we have a witness \verb|x:A| with its justification -\verb|p:(P x)|. +\verb|p:P x|. From such a \verb:(exist x p): we may in turn extract its witness -\verb|x:A| (using an elimination construct such as \verb:Cases:) but +\verb|x:A| (using an elimination construct such as \verb:match:) but {\sl not} its justification, which stays hidden, like in an abstract data type. In technical terms, one says that \verb:sig: is a ``weak (dependent) sum''. A variant \verb:sig2: with two predicates is also @@ -379,10 +385,8 @@ provided. \ttindex{exist2} \begin{coq_example*} -Inductive sig (A:Set) (P:A -> Prop) : Set := - exist : forall x:A, P x -> sig A P. -Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := - exist2 : forall x:A, P x -> Q x -> sig2 A P Q. +Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). +Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 : (x:A) (_:P x) (_:Q x). \end{coq_example*} A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined, @@ -399,21 +403,16 @@ constructor. \ttindex{existS2} \begin{coq_example*} -Inductive sigS (A:Set) (P:A -> Set) : Set := - existS : forall x:A, P x -> sigS A P. +Inductive sigS (A:Set) (P:A -> Set) : Set := existS (x:A) (_:P x). Section sigSprojections. -Variable A : - Set. -Variable P : - A -> Set. -Definition projS1 (H: - sigS A P) := let (x, h) := H in x. -Definition projS2 (H: - sigS A P) := - let (x, h) as H return P (projS1 H) := H in h. +Variable A : Set. +Variable P : A -> Set. +Definition projS1 (H:sigS A P) := let (x, h) := H in x. +Definition projS2 (H:sigS A P) := + let (x, h) return P (projS1 H) := H in h. End sigSprojections. Inductive sigS2 (A: Set) (P Q:A -> Set) : Set := - existS2 : forall x:A, P x -> Q x -> sigS2 A P Q. + existS2 : (x:A) (_:P x) (_:Q x). \end{coq_example*} A related non-dependent construct is the constructive sum @@ -425,9 +424,7 @@ A related non-dependent construct is the constructive sum \ttindex{\{A\}+\{B\}} \begin{coq_example*} -Inductive sumbool (A B:Prop) : Set := - | left : A -> sumbool A B - | right : B -> sumbool A B. +Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B). \end{coq_example*} This \verb"sumbool" construct may be used as a kind of indexed boolean @@ -440,9 +437,7 @@ in the \verb"Set" \verb"A+{B}". \ttindex{A+\{B\}} \begin{coq_example*} -Inductive sumor (A:Set) (B:Prop) : Set := - | inleft : A -> sumor A B - | inright : B -> sumor A B. +Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B). \end{coq_example*} \begin{figure} @@ -529,7 +524,7 @@ Definition except := False_rec. Notation Except := (except _). Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Theorem and_rec : - forall (A B:Prop) (C:Set), (A -> B -> C) -> A /\ B -> C. + forall (A B:Prop) (P:Set), (A -> B -> P) -> A /\ B -> P. \end{coq_example*} %\begin{coq_eval} %Abort. @@ -538,9 +533,33 @@ Theorem and_rec : \subsection{Basic Arithmetics} -The basic library includes a few elementary properties of natural numbers, -together with the definitions of predecessor, addition and -multiplication\footnote{This is in module {\tt Peano.v}}. +The basic library includes a few elementary properties of natural +numbers, together with the definitions of predecessor, addition and +multiplication\footnote{This is in module {\tt Peano.v}}. It also +provides a scope {\tt nat\_scope} gathering standard notations for +common operations (+,*) and a decimal notation for numbers. That is he +can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on +the left hand side of a \texttt{match} expression (see for example +section \ref{Refine-example}). This scope is opened by default. + +%Remove the redefinition of nat +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +The following example is not part of the standard library, but it +shows the usage of the notations: + +\begin{coq_example*} +Fixpoint even (n:nat) : bool := + match n with + | 0 => true + | 1 => false + | S (S n) => even n + end. +\end{coq_example*} + + \ttindex{eq\_S} \ttindex{pred} \ttindex{pred\_Sn} @@ -557,20 +576,20 @@ multiplication\footnote{This is in module {\tt Peano.v}}. \ttindex{mult\_n\_Sm} \begin{coq_example*} -Theorem eq_S : forall n m:nat, n = m -> S n = S m. +Theorem eq_S : forall x y:nat, x = y -> S x = S y. \end{coq_example*} \begin{coq_eval} Abort. \end{coq_eval} \begin{coq_example*} Definition pred (n:nat) : nat := - match n return nat with - | O => O + match n with + | 0 => 0 | S u => u end. Theorem pred_Sn : forall m:nat, m = pred (S m). Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. -Hints Immediate eq_add_S : core. +Hint Immediate eq_add_S : core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. \end{coq_example*} \begin{coq_eval} @@ -579,10 +598,10 @@ Abort All. \begin{coq_example*} Definition IsSucc (n:nat) : Prop := match n with - | O => False + | 0 => False | S p => True end. -Theorem O_S : forall n:nat, O <> S n. +Theorem O_S : forall n:nat, 0 <> S n. Theorem n_Sn : forall n:nat, n <> S n. \end{coq_example*} \begin{coq_eval} @@ -591,10 +610,10 @@ Abort All. \begin{coq_example*} Fixpoint plus (n m:nat) {struct n} : nat := match n with - | O => m + | 0 => m | S p => S (plus p m) end. -Lemma plus_n_O : forall n:nat, n = plus n O. +Lemma plus_n_O : forall n:nat, n = plus n 0. Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus n (S m). \end{coq_example*} \begin{coq_eval} @@ -603,10 +622,10 @@ Abort All. \begin{coq_example*} Fixpoint mult (n m:nat) {struct n} : nat := match n with - | O => O - | S p => plus m (mult p m) + | 0 => 0 + | S p => m + mult p m end. -Lemma mult_n_O : forall n:nat, O = mult n O. +Lemma mult_n_O : forall n:nat, 0 = mult n 0. Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult n (S m). \end{coq_example*} \begin{coq_eval} @@ -626,9 +645,10 @@ Finally, it gives the definition of the usual orderings \verb:le:, Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m:nat, le n m -> le n (S m). -Definition lt (n m:nat) := le (S n) m. -Definition ge (n m:nat) := le m n. -Definition gt (n m:nat) := lt m n. +Infix "+" := plus : nat_scope. +Definition lt (n m:nat) := S n <= m. +Definition ge (n m:nat) := m <= n. +Definition gt (n m:nat) := m < n. \end{coq_example*} Properties of these relations are not initially known, but may be @@ -641,7 +661,7 @@ induction principle. \begin{coq_example*} Theorem nat_case : - forall (n:nat) (P:nat -> Prop), P O -> (forall m:nat, P (S m)) -> P n. + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. \end{coq_example*} \begin{coq_eval} Abort All. @@ -649,8 +669,8 @@ Abort All. \begin{coq_example*} Theorem nat_double_ind : forall R:nat -> nat -> Prop, - (forall n:nat, R O n) -> - (forall n:nat, R (S n) O) -> + (forall n:nat, R 0 n) -> + (forall n:nat, R (S n) 0) -> (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. \end{coq_example*} \begin{coq_eval} @@ -678,14 +698,13 @@ Inductive Acc : A -> Prop := Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. \end{coq_example*} \begin{coq_eval} -olddestruct 1; trivial. +simple destruct 1; trivial. Defined. \end{coq_eval} \begin{coq_example*} Section AccRec. Variable P : A -> Set. -Variable - F : +Variable F : forall x:A, (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x. Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x := @@ -719,8 +738,7 @@ Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x := F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)). Definition Fix (x:A) := Fix_F x (Rwf x). -Hypothesis - F_ext : +Hypothesis F_ext : forall (x:A) (f g:forall y:A, R y x -> P y), (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g. Lemma Fix_F_eq : @@ -743,106 +761,39 @@ The basic library includes the definitions\footnote{This is in module {\tt Logic\_Type.v}} of logical quantifiers axiomatized at the \verb:Type: level. -\ttindex{allT} -\ttindex{AllT} +\ttindex{all} \ttindex{inst} \ttindex{gen} -\ttindex{exT} -\ttindex{ExT} -\ttindex{EXT} -\ttindex{exT\_intro} -\ttindex{ExT2} -\ttindex{exT2} \ttindex{EmptyT} \ttindex{UnitT} \ttindex{notT} \begin{coq_example*} -Definition allT (A: Type) (P:A -> Prop) := forall x:A, P x. -Section universal_quantification. -Variable A : Type. -Variable P : A -> Prop. -Theorem inst : forall x:A, ( ALL x : _ | P x) -> P x. -Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> allT _ P. +Definition all (A:Type) (P:A->Prop) : Prop := forall x:A, P x. \end{coq_example*} \begin{coq_eval} -Abort All. +Reset Initial. \end{coq_eval} \begin{coq_example*} -End universal_quantification. -Inductive exT (A:Type) (P:A -> Prop) : Prop := - exT_intro : forall x:A, P x -> exT A P. -Inductive exT2 (A:Type) (P Q:A -> Prop) : Prop := - exT_intro2 : forall x:A, P x -> Q x -> exT2 A P Q. -\end{coq_example*} - -It defines also Leibniz equality \verb:x==y: when \verb:x: and -\verb:y: belong to \verb+A:Type+. -\ttindex{eqT} -\ttindex{refl\_eqT} -\ttindex{sum\_eqT} -\ttindex{sym\_not\_eqT} -\ttindex{trans\_eqT} -\ttindex{congr\_eqT} -\ttindex{eqT\_ind\_r} -\ttindex{eqT\_rec\_r} - -\begin{coq_example*} -Inductive eqT (A:Type) (x:A) : A -> Prop := - refl_eqT : eqT A x x. -Section Equality_is_a_congruence. -Variables A B : Type. -Variable f : A -> B. -Variables x y z : A. -Lemma sym_eqT : x = y -> y = x. -Lemma trans_eqT : x = y -> y = z -> x = z. -Lemma congr_eqT : x = y -> f x = f y. +Section universal_quantification. +Variable A : Type. +Variable P : A -> Prop. +Theorem inst : forall x:A, (all (fun (x:A) => P x)) -> P x. +Theorem gen : forall B:Prop, (forall y:A, B -> P y) -> B -> all P. \end{coq_example*} \begin{coq_eval} Abort All. \end{coq_eval} \begin{coq_example*} -End Equality_is_a_congruence. -Hints Immediate sym_eq sym_not_eqT : core. -Definition eqT_ind_r : - forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. +End universal_quantification. \end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} - -The figure \ref{formulas-syntax-type} presents the syntactic notations -corresponding to the main definitions -\footnote{This syntax is defined in module {\tt Logic\_TypeSyntax}} - -\begin{figure} -\label{formulas-syntax-type} -\begin{center} -\begin{tabular}{|lclr|} -\hline -{\form} & ::= & {\tt ( ALLT} {\ident} \zeroone{{\tt :} {\specif}} {\tt |} - {\form} {\tt )} & ({\tt allT})\\ - & $|$ & {\tt ( EXT} {\ident} \zeroone{{\tt :} {\specif}} {\tt - |} {\form} {\tt )} & ({\tt exT})\\ - & $|$ & {\tt ( EXT} {\ident} \zeroone{{\tt :} {\specif}} {\tt - |} {\form} {\tt \&} {\form} {\tt )} & ({\tt exT2})\\ - & $|$ & {\term} {\tt ==} {\term} & ({\tt eqT})\\ -\hline -\end{tabular} -\end{center} -\caption{Syntax of first-order formulas in the type universe} -\end{figure} At the end, it defines datatypes at the {\Type} level. \begin{coq_example*} -Inductive EmptyT : Type :=. -Inductive UnitT : Type := - IT : UnitT. -Definition notT (A:Type) := A -> EmptyT. -Inductive identityT (A: - Type) (a:A) : A -> Type := - refl_identityT : identityT A a a. +Definition notT (A:Type) := A -> False. +Inductive identity (A:Type) (a:A) : A -> Type := + refl_identity : identity A a a. \end{coq_example*} \section{The standard library} @@ -901,6 +852,7 @@ operators which bind less than the others constructions. All the binary operators are left associative. The {\tt [}~...~{\tt ]} allows to escape the {\zarith} grammar. +%% Should describe Z_scope instead \begin{figure} \begin{center} \begin{tabular}{|lcl|} @@ -939,47 +891,32 @@ allows to escape the {\zarith} grammar. \caption{Syntax of expressions in integer arithmetics} \end{figure} -\subsection{Notations for Peano's arithmetic (\texttt{nat})} -\index{Peano's arithmetic notations} - -After having required the module \texttt{Arith}, the user can type the -naturals using decimal notation. That is he can write \texttt{(3)} -for \texttt{(S (S (S O)))}. The number must be between parentheses. -This works also in the left hand side of a \texttt{Cases} expression -(see for example section \ref{Refine-example}). +\subsection{Peano's arithmetic (\texttt{nat})} +\index{Peano's arithmetic} -%Remove the redefinition of nat -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Require Import Arith. -Fixpoint even (n:nat) : bool := - match n with - | O => true - | S O => false - | S (S n) => even n - end. -\end{coq_example*} +While in the initial state, many operations and predicates of Peano's +arithmetic are defined, further operations and results belong to other +modules. For instance, the decidability of the basic predicates are +defined here. This is provided by requiring the module {\tt Arith}. -\begin{coq_eval} -Reset Initial. -\end{coq_eval} \subsection{Real numbers library} \subsubsection{Notations for real numbers} \index{Notations for real numbers} -This is provided by requiring the module {\tt Reals}. This notation is very -similar to the notation for integer arithmetics (see figure -\ref{zarith-syntax}) where Inverse (/x) and division (x/y) have been added. -This syntax is used parenthesizing by a double back-quote (\verb:``:). +This is provided by requiring the module {\tt Reals}. This notation is +very similar to the notation for integer arithmetics where Inverse +(/x) and division (x/y) have been added. +\begin{coq_eval} +Reset Initial. +\end{coq_eval} \begin{coq_example} Require Import Reals. Check (2 + 3)%R. +Open Scope R_scope. +Check 2 + 3. \end{coq_example} \subsubsection{Some tactics} @@ -993,7 +930,7 @@ another real integer constante c2. \begin{coq_example*} Require Import DiscrR. -Goal 5%R <> 0%R. +Goal 5 <> 0. \end{coq_example*} \begin{coq_example} @@ -1010,7 +947,7 @@ corresponding conjonctions. \begin{coq_example*} Require Import SplitAbsolu. -Goal forall x:R, (x <= Rabs x)%R. +Goal forall x:R, x <= Rabs x. \end{coq_example*} \begin{coq_example} @@ -1028,29 +965,37 @@ product. \begin{coq_example*} Require Import SplitRmult. -Goal forall x y z:R, (x * y * z)%R <> 0%R. +Goal forall x y z:R, x * y * z <> 0. \end{coq_example*} \begin{coq_example} intros; split_Rmult. \end{coq_example} -All this tactics has been written with the new tactic language. +All this tactics has been written with the tactic language Ltac +described in chapter~\ref{TacticLanguage}.\\ -\bigskip - -More details are available in this document: {\tt http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\ +More details are available in this document: {\tt +http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\ \begin{coq_eval} Reset Initial. \end{coq_eval} +\subsection{List library} +\index{Notations for lists} + +Some elementary operations on polymorphic lists are defined here. They +can be accessed by requiring module {\tt List}. + + + \section{Users' contributions} \index{Contributions} \label{Contributions} Numerous users' contributions have been collected and are available on -the WWW at the following address: \verb!pauillac.inria.fr/coq/contribs!. +the WWW at the following address: \verb!coq.inria.fr/contribs/!. On this web page, you have a list of all contributions with informations (author, institution, quick description, etc.) and the possibility to download them one by one. diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex index d4408ace7e..e2e54e40dd 100644 --- a/doc/RefMan-ltac.tex +++ b/doc/RefMan-ltac.tex @@ -1,16 +1,14 @@ \chapter{The tactic language} \label{TacticLanguage} -% Très très provisoire -% À articuler notamment avec le chapitre "Tactiques utilisateurs" - %\geometry{a4paper,body={5in,8in}} -This chapter gives a compact documentation of the tactic language available in -the toplevel of {\Coq}. We start by giving the syntax and, next, we present the -informal semantic. Finally, we show some examples which deal with small but -also with non-trivial problems. If you want to know more regarding this -language and especially about its fundations, you can refer to~\cite{Del00}. +This chapter gives a compact documentation of Ltac, the tactic +language available in {\Coq}. We start by giving the syntax and, next, +we present the informal semantics. Finally, we show some examples which +deal with small but also with non-trivial problems. If you want to +know more regarding this language and especially about its fundations, +you can refer to~\cite{Del00}. \section{Syntax} @@ -18,7 +16,6 @@ language and especially about its fundations, you can refer to~\cite{Del00}. \def\tacexprinf{\textrm{\textsl{tacexpr$_i$}}} \def\tacexprpref{\textrm{\textsl{tacexpr$_p$}}} \def\atom{\textrm{\textsl{atom}}} -\def\inputfun{\textrm{\textsl{input\_fun}}} \def\recclause{\textrm{\textsl{rec\_clause}}} \def\letclause{\textrm{\textsl{let\_clause}}} \def\matchrule{\textrm{\textsl{match\_rule}}} @@ -26,23 +23,26 @@ language and especially about its fundations, you can refer to~\cite{Del00}. \def\contexthyps{\textrm{\textsl{context\_hyps}}} \def\primitivetactic{\textrm{\textsl{primitive\_tactic}}} \def\tacarg{\textrm{\textsl{arg}}} +\def\qstring{\textrm{\textsl{string}}} + -The syntax of the tactic language is given in table~\ref{ltac}. -% We use a \bn{}-like notation. -Terminal symbols are set in -%sans serif font ({\sf like this}). -typewriter font ({\tt like this}). -Non-terminal symbols are set in italic font ($like\sm{}that$). ... {\it -|} ... denotes the or operation. \nelist{$entry$}{} denotes one or several -repetitions of entry $entry$. \nelist{$entry$}{$sep$} denotes one or several repetitions separated by $sep$. +The syntax of the tactic language is given in tables~\ref{ltac} +and~\ref{ltax_aux}. Terminal symbols are set in typewriter font ({\tt +like this}). Non-terminal symbols are set in italic font +($like\sm{}that$). ... {\it |} ... denotes the or +operation. \nelist{$entry$}{} denotes one or several repetitions of +entry $entry$. \nelist{$entry$}{$sep$} denotes one or several +repetitions separated by $sep$. %Parentheses {\it (}...{\it )} denote grouping. -The main entry is {\tacexpr} and the entries {\naturalnumber}, {\integer}, -{\ident}, {\qualid}, {\term}, {\pattern} and {\primitivetactic} represent respectively the natural and integer -numbers, the authorized identificators and qualified names, {\Coq}'s terms and patterns and all the basic -tactics. In {\pattern}, there can be specific variables like {\tt ?n} where {\tt n} -is a {\naturalnumber} or {\tt ?}, which are metavariables for pattern matching. {\tt ?n} -allows us to keep instantiations and to make constraints whereas {\tt ?} shows -that we are not interested in what will be matched. +The main entry is {\tacexpr} and the entries {\naturalnumber}, +{\integer}, {\ident}, {\qualid}, {\term}, {\pattern} and +{\primitivetactic} represent respectively the natural and integer +numbers, the authorized identificators and qualified names, {\Coq}'s +terms and patterns and all the basic tactics. In {\pattern}, there can +be specific variables like {\tt ?id} where {\tt id} is a {\ident} or +{\tt \_}, which are metavariables for pattern matching. {\tt ?id} allows +us to keep instantiations and to make constraints whereas {\tt \_} +shows that we are not interested in what will be matched. This language is used in proof mode but it can also be used in toplevel definitions as shown in table~\ref{ltactop}. @@ -52,70 +52,93 @@ definitions as shown in table~\ref{ltactop}. {\parbox{6in} {\begin{center} \begin{tabular}{lp{0.1in}l} -{\tacexpr} & \cn{}::= & {\tacexpr} {\tt ;} {\tacexpr}\\ +{\tacexpr} & \cn{}::= & + {\tacexpr} {\tt ;} {\tacexpr}\\ & \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\ & \cn{}| & {\tacexprpref}\\ \\ -{\tacexprpref} & \cn{}::= & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ -& \cn{}| & {\tt Repeat} {\tacexprpref}\\ -& \cn{}| & {\tt Try} {\tacexprpref}\\ -& \cn{}| & {\tt Progress} {\tacexprpref}\\ -& \cn{}| & {\tt Info} {\tacexprpref}\\ +{\tacexprpref} & \cn{}::= & + {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ +& \cn{}| & {\tt info} {\tacexprpref}\\ +& \cn{}| & {\tt progress} {\tacexprpref}\\ +& \cn{}| & {\tt repeat} {\tacexprpref}\\ +& \cn{}| & {\tt try} {\tacexprpref}\\ & \cn{}| & {\tacexprinf} \\ \\ -{\tacexprinf} & \cn{}::= & {\atom} {\tt Orelse} {\tacexprpref}\\ +{\tacexprinf} & \cn{}::= & + {\atom} {\tt ||} {\tacexprpref}\\ & \cn{}| & {\atom}\\ \\ -{\atom} & \cn{}::= & {\tt Fun} \nelist{\ident}{} {\tt ->} {\tacexpr}\\ +{\atom} & \cn{}::= & +%% TODO: not ident, but ident or _ +{\tt fun} \nelist{\ident}{} {\tt =>} {\tacexpr}\\ & \cn{}| & -{\tt Let} \nelist{\letclause}{\tt And} {\tt In} +{\tt let} \nelist{\letclause}{\tt with} {\tt in} {\tacexpr}\\ -% & \cn{}| & {\tt Rec} {\recclause}\\ & \cn{}| & -{\tt Rec} \nelist{\recclause}{\tt And} {\tt In} +{\tt let rec} \nelist{\recclause}{\tt with} {\tt in} {\tacexpr}\\ & \cn{}| & -{\tt Match Context With} \nelist{\contextrule}{\tt |}\\ +{\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ & \cn{}| & -{\tt Match} {\term} {\tt With} \nelist{\matchrule}{\tt |}\\ -& \cn{}| & {\tt (} {\tacexpr} {\tt )}\\ -& \cn{}| & {\tt (} {\qualid} \nelist{\tacarg}{} {\tt )}\\ -& \cn{}| & {\tt First [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ -& \cn{}| & {\tt Solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ -& \cn{}| & {\tt Idtac}\\ -& \cn{}| & {\tt Fail} ~|~ {\tt Fail} {\naturalnumber}\\ +{\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& \cn{}| & +{\tt match} {\term} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ +& \cn{}| & {\tt abstract} {\atom}\\ +& \cn{}| & {\tt abstract} {\atom} {\tt using} {\ident} \\ +& \cn{}| & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ +& \cn{}| & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ +& \cn{}| & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\ +& \cn{}| & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\ +& \cn{}| & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\ +& \cn{}| & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\ +& \cn{}| & {\tt eval} {$redexpr$} {\tt in} {\term}\\ +& \cn{}| & {\tt type} {\term}\\ +& \cn{}| & {\tt constr :} {\term}\\ +& \cn{}| & {\qualid} \sequence{\tacarg}{}\\ +& \cn{}| & ()\\ & \cn{}| & \primitivetactic\\ -& \cn{}| & \tacarg\\ -\\ -%{\inputfun} & \cn{}::= & {\ident}\\ -%& \cn{}| & {\tt ()}\\ -%\\ -\letclause & \cn{}::= & {\ident} {\tt =} {\tacarg}\\ +& \cn{}| & {\tt (} {\tacexpr} {\tt )}\\ +\end{tabular} +\end{center}}} +\caption{Syntax of the tactic language} +\label{ltac} +\end{table} + + + +\begin{table}[htbp] +\noindent{}\framebox[6in][l] +{\parbox{6in} +{\begin{center} +\begin{tabular}{lp{0.1in}l} +\letclause & \cn{}::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}\\ \\ -\recclause & \cn{}::= & {\ident} \nelist{\ident}{} {\tt ->} {\tacexpr}\\ +\recclause & \cn{}::= & {\ident} \nelist{\ident}{} {\tt :=} {\tacexpr}\\ \\ \contextrule & \cn{}::= & -{\tt [} \nelist{\contexthyps}{\tt ;} {\tt |-} -{\pattern} {\tt ] ->} {\tacexpr}\\ -& \cn{}| & {\tt [ |-} {\pattern} {\tt ] ->} {\tacexpr}\\ -& \cn{}| & {\tt \_ ->} {\tacexpr}\\ +\nelist{\contexthyps}{\tt ;} {\tt |-} +{\pattern} {\tt =>} {\tacexpr}\\ +& \cn{}| & {\tt |-} {\pattern} {\tt =>} {\tacexpr}\\ +& \cn{}| & {\tt \_ =>} {\tacexpr}\\ \\ -\contexthyps & \cn{}::= & {\ident} {\tt :} {\pattern}\\ +\contexthyps & \cn{}::= & + {\ident} {\tt :} {\pattern}\\ & \cn{}| & {\tt \_ :} {\pattern}\\ \\ -\matchrule & \cn{}::= & {\tt [} {\pattern} {\tt ] ->} {\tacexpr}\\ -& \cn{}| & {\tt \_ ->} {\tacexpr}\\ +\matchrule & \cn{}::= & + {\pattern} {\tt =>} {\tacexpr}\\ +& \cn{}| & {\tt \_ =>} {\tacexpr}\\ \\ -\tacarg -%& \cn{}::= & {\tt ()}\\ -& \cn{}| & {integer}\\ -& \cn{}| & {\ident}\\ -& \cn{}| & {\tt '}{\term}\\ -& \cn{}| & {\tacexpr}\\ +\tacarg & \cn{}::= & + {\qualid}\\ +& \cn{}| & {\tt ()} \\ +& \cn{}| & {\tt ltac :}{\tacexpr}\\ +& \cn{}| & {\term}\\ \end{tabular} \end{center}}} -\caption{Syntax of the tactic language} -\label{ltac} +\caption{Syntax of the tactic language (continued)} +\label{ltac_aux} \end{table} \begin{table}[ht] @@ -123,12 +146,9 @@ definitions as shown in table~\ref{ltactop}. {\parbox{6in} {\begin{center} \begin{tabular}{lp{0.1in}l} -$top$ & \cn{}::= & {\tt Tactic Definition} {\ident} \nelist{\ident}{} {\tt :=} -{\tacexpr} \\ -& \cn{}| & {\tt Recursive Tactic Definition} \nelist{$trec\_clause$}{\tt -And}\\ +$top$ & \cn{}::= & {\tt Ltac} \nelist{$ltac\_def$}{\tt with} \\ \\ -$trec\_clause$ & \cn{}::= & {\ident} \nelist{\ident}{} {\tt :=} {\tacexpr} +$ltac\_def$ & \cn{}::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr} \end{tabular} \end{center}}} \caption{Tactic toplevel definitions} @@ -142,11 +162,15 @@ evaluation yields either a term, an integer or a tactic. Intermediary results can be terms or integers but the final result must be a tactic which is then applied to the current goal. -There is a special case for {\tt Match Context} expressions of which +There is a special case for {\tt match goal} expressions of which the clauses evaluate to tactics. Such expressions can only be used as end result of a tactic expression (never as argument of a local definition or of an application). +The rest of this section explains the semantics of every construction +of Ltac. + + %% \subsection{Values} %% Values are given by table~\ref{ltacval}. All these values are tactic values, @@ -199,10 +223,10 @@ Local definitions can be done as follows: %\vfill{} \begin{tabular}{l} -{\tt Let} {\ident}$_1$ {\tt =} {\tacexpr}$_1$\\ -{\tt And} {\ident}$_2$ {\tt =} {\tacexpr}$_2$\\ +{\tt let} {\ident}$_1$ {\tt :=} {\tacexpr}$_1$\\ +{\tt with} {\ident}$_2$ {\tt :=} {\tacexpr}$_2$\\ ...\\ -{\tt And} {\ident}$_n$ {\tt =} {\tacexpr}$_n$ {\tt In}\\ +{\tt with} {\ident}$_n$ {\tt :=} {\tacexpr}$_n$ {\tt in}\\ {\tacexpr} \end{tabular} @@ -210,44 +234,54 @@ each {\tacexpr}$_i$ is evaluated to $v_i$, then, {\tacexpr} is evaluated by subs to each occurrence of {\ident}$_i$, for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$ and the {\ident}$_i$. +Local definitions can be recursive by using {\tt let rec} instead of +{\tt let}. Only functions can be defined by recursion, so at least one +argument is required. + \subsubsection{Pattern matching on terms} We can carry out pattern matching on terms with: \begin{tabular}{l} -{\tt Match} {\term} {\tt With}\\ -~~~{\pattern}$_1$ {\tt ->} {\tacexpr}$_1$\\ -~{\tt |} {\pattern}$_2$ {\tt ->} {\tacexpr}$_2$\\ +{\tt match} {\tacexpr} {\tt with}\\ +~~~{\pattern}$_1$ {\tt =>} {\tacexpr}$_1$\\ +~{\tt |} {\pattern}$_2$ {\tt =>} {\tacexpr}$_2$\\ ~...\\ -~{\tt |} {\pattern}$_n$ {\tt ->} {\tacexpr}$_n$\\ -~{\tt |} {\tt \_} {\tt ->} {\tacexpr}$_{n+1}$ +~{\tt |} {\pattern}$_n$ {\tt =>} {\tacexpr}$_n$\\ +~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\ +{\tt end} \end{tabular} -the {\term} is matched (non-linear first order unification) against -{\pattern}$_1$ then {\tacexpr}$_1$ is evaluated into some value by -substituting the pattern matching instantiations to the -metavariables. If the matching with {\pattern}$_1$ fails, -{\pattern}$_2$ is used and so on. The pattern {\_} matches any term -and shunts all remaining patterns if any. If {\tacexpr}$_1$ evaluates -to a tactic, this tactic is not immediately applied to the current -goal (in contrast with {\tt Match Context}). If all clauses fail (in -particular, there is no pattern {\_}) then a no-matching error is -raised. \\ +The {\tacexpr} is evaluated and should yield a term which is matched +(non-linear first order unification) against {\pattern}$_1$ then +{\tacexpr}$_1$ is evaluated into some value by substituting the +pattern matching instantiations to the metavariables. If the matching +with {\pattern}$_1$ fails, {\pattern}$_2$ is used and so on. The +pattern {\_} matches any term and shunts all remaining patterns if +any. If {\tacexpr}$_1$ evaluates to a tactic, this tactic is not +immediately applied to the current goal (in contrast with {\tt match +goal}). If all clauses fail (in particular, there is no pattern {\_}) +then a no-matching error is raised. \\ -{\tt Error message:}\\ +{\tt Error messages:}\\ -{\tt No matching clauses for Match} +{\tt No matching clauses for match} \hx{4}No pattern can be used and, in particular, there is no {\tt \_} pattern. +{\tt Argument of match does not evaluate to a term} + +\hx{4}This happens when {\tacexpr} does not denote a term. + \subsubsection{Application} An application is an expression of the following form:\\ -{\tt (} {\qualid} {\tacexpr}$_1$ ... {\tacexpr}$_n$ {\tt )}\\ +{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$\\ -The reference {\qualid} must be bound to some defined tactic definition expecting at least $n$ arguments. -The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$. +The reference {\qualid} must be bound to some defined tactic +definition expecting at least $n$ arguments. The expressions +{\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$. %If {\tacexpr} is a {\tt Fun} or {\tt Rec} value then the body is evaluated by %substituting $v_i$ to the formal parameters, for $i=1,...,n$. For recursive %clauses, the bodies are lazily substituted (when an identifier to be evaluated @@ -261,36 +295,38 @@ A sequence is an expression of the following form:\\ {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$\\ -{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be -tactic values. $v_1$ is then applied and $v_2$ is applied to the subgoals -generated by the application of $v_1$. Sequence is left associating. +{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and +$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied +and $v_2$ is applied to the subgoals generated by the application of +$v_1$. Sequence is left associating. \subsubsection{General sequence} We can generalize the previous sequence operator by:\\ -{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\ +{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} +{\tacexpr}$_n$ {\tt ]}\\ -{\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is applied and $v_i$ is -applied to the $i$-th generated subgoal by the application of $v_0$, for -$=1,...,n$. It fails if the application of $v_0$ does not generate exactly $n$ -subgoals. +{\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is +applied and $v_i$ is applied to the $i$-th generated subgoal by the +application of $v_0$, for $=1,...,n$. It fails if the application of +$v_0$ does not generate exactly $n$ subgoals. \subsubsection{Branching} We can easily branch with the following structure:\\ -{\tacexpr}$_1$ {\tt Orelse} {\tacexpr}$_2$\\ +{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$\\ -{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be -tactic values. $v_1$ is applied and if it fails then $v_2$ is applied. -Branching is left associating. +{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and +$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if +it fails then $v_2$ is applied. Branching is left associating. \subsubsection{For loop} We have a for loop with:\\ -{\tt Do} $n$ {\tacexpr}\\ +{\tt do} $n$ {\tacexpr}\\ {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied $n$ times. Supposing $n>1$, after the first application of $v$, $v$ is applied, at @@ -301,29 +337,30 @@ $v$ fails before the $n$ applications have been completed. We have a repeat loop with:\\ -{\tt Repeat} {\tacexpr}\\ +{\tt repeat} {\tacexpr}\\ -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied until it -fails. Supposing $n>1$, after the first application of $v$, $v$ is applied, at -least once, to the generated subgoals and so on. It stops when it fails for all -the generated subgoals. It never fails. +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +applied until it fails. Supposing $n>1$, after the first application +of $v$, $v$ is applied, at least once, to the generated subgoals and +so on. It stops when it fails for all the generated subgoals. It never +fails. \subsubsection{Error catching} We can catch the tactic errors with:\\ -{\tt Try} {\tacexpr}\\ +{\tt try} {\tacexpr}\\ -{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied. If the -application of $v$ fails, it catches the error and leaves the goal unchanged. -It never fails. +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +applied. If the application of $v$ fails, it catches the error and +leaves the goal unchanged. It never fails. \subsubsection{First tactic to work} We may consider the first tactic to work (i.e. which does not fail) among a panel of tactics:\\ -{\tt First [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\ +{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\ {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it @@ -338,7 +375,7 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic.\\ We may consider the first to solve (i.e. which generates no subgoal) among a panel of tactics:\\ -{\tt Solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\ +{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\ {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it @@ -352,66 +389,69 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\ We have the identity tactic:\\ -{\tt Idtac} and {\tt Idtac ``message''}\\ +{\tt idtac} and {\tt idtac "message"}\\ It leaves the goal unchanged but it appears in the proof script. -If there is a string as an argument then it prints this string on the +If there is a string as argument then it prints this string on the standard output. \subsubsection{Failing} We have the failing tactic:\\ -{\tt Fail} and {\tt Fail $n$} \\ +{\tt fail}, {\tt fail $n$}, {\tt fail "message"} + and {\tt fail $n$ "message"} \\ It always fails and leaves the goal unchanged. It does not appear in -the proof script and can be catched by {\tt Try}. The number $n$ is +the proof script and can be catched by {\tt try}. The number $n$ is the failure level. If no level is specified, it defaults to $0$. The -level is used in {\tt Match Context}. If $0$, it makes {\tt Match -Context} considering the next clause. If non zero, the current {\tt -Match Context} block is aborted and the level is decremented. +level is used in {\tt match goal}. If $0$, it makes {\tt match +goal} considering the next clause. If non zero, the current {\tt +match goal} block is aborted and the level is decremented. {\tt Error message:}\\ -{\tt Fail tactic always fails (level $n$)}. +{\tt Tactic Failure "message" (level $n$)}. -\subsubsection{Pattern matching on proof contexts} +\subsubsection{Pattern matching on goals} -We can make pattern matching on proof contexts using the following -expression: +We can make pattern matching on goals using the following expression: \begin{tabular}{l} -{\tt Match Context With}\\ -~~~{\tt [}$context\_hyps_{1,1}${\tt ;}...{\tt ;}$context\_hyps_{1,m_1}$ - ~~{\tt |-}{\pattern}$_1${\tt ] ->} {\tacexpr}$_1$\\ -~~{\tt |[}$context\_hyps_{2,1}${\tt ;}...{\tt ;}$context\_hyps_{2,m_2}$ - ~~{\tt |-}{\pattern}$_2${\tt ] ->} {\tacexpr}$_2$\\ +{\tt match goal with}\\ +~~~$context\_hyps_{1,1}${\tt ;}...{\tt ;}$context\_hyps_{1,m_1}$ + ~~{\tt |-}{\pattern}$_1${\tt =>} {\tacexpr}$_1$\\ +~~{\tt |}$context\_hyps_{2,1}${\tt ;}...{\tt ;}$context\_hyps_{2,m_2}$ + ~~{\tt |-}{\pattern}$_2${\tt =>} {\tacexpr}$_2$\\ ~~...\\ -~~{\tt |[}$context\_hyps_{n,1}${\tt ;}...{\tt ;}$context\_hyps_{n,m_n}$ - ~~{\tt |-}{\pattern}$_n${\tt ] ->} {\tacexpr}$_n$\\ -~~{\tt |\_}~~~~{\tt ->} {\tacexpr}$_{n+1}$ +~~{\tt |}$context\_hyps_{n,1}${\tt ;}...{\tt ;}$context\_hyps_{n,m_n}$ + ~~{\tt |-}{\pattern}$_n${\tt =>} {\tacexpr}$_n$\\ +~~{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\ +{\tt end} \end{tabular} -If each hypothesis pattern $context\_hyps_{1,i}$, with $i=1,...,m_1$ is matched -(non-linear first order unification) by an hypothesis of the goal and if -{\pattern}$_1$ is matched by the conclusion of the goal, then {\tacexpr}$_1$ is evaluated -to $v_1$ by substituting the pattern matching to the metavariables and the real -hypothesis names bound to the possible hypothesis names occurring in the -hypothesis patterns. If $v_1$ is a tactic value, then it is applied to the -goal. If this application fails, then another combination of hypotheses is -tried with the same proof context pattern. If there is no other combination of -hypotheses then the second proof context pattern is tried and so on. If the -next to last proof context pattern fails then {\tacexpr}$_{n+1}$ is evaluated to -$v_{n+1}$ and $v_{n+1}$ is applied.\\ +% TODO: specify order of hypothesis and explain reverse... + +If each hypothesis pattern $context\_hyps_{1,i}$, with $i=1,...,m_1$ +is matched (non-linear first order unification) by an hypothesis of +the goal and if {\pattern}$_1$ is matched by the conclusion of the +goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the +pattern matching to the metavariables and the real hypothesis names +bound to the possible hypothesis names occurring in the hypothesis +patterns. If $v_1$ is a tactic value, then it is applied to the +goal. If this application fails, then another combination of +hypotheses is tried with the same proof context pattern. If there is +no other combination of hypotheses then the second proof context +pattern is tried and so on. If the next to last proof context pattern +fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$ +is applied.\\ {\tt Error message:}\\ -{\tt No matching clauses for Match Context} +{\tt No matching clauses for match goal} -\hx{4}No proof context pattern can be used and, in particular, there is no {\tt -\_} proof - -\hx{4}context pattern. +\hx{4}No goal pattern can be used and, in particular, there is no {\tt +\_} goal pattern. \subsection{Tactic toplevel definitions} @@ -424,26 +464,26 @@ Basically, tactics toplevel definitions are made as follows:\\ % %We can define functional definitions by:\\ -{\tt Tactic Definition} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=} +{\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=} {\tacexpr}\\ \noindent This defines a new tactic that can be used in any tactic script or new tactic toplevel definition. \Rem The preceding definition can equivalently be written:\\ -{\tt Tactic Definition} {\ident} {\tt := Fun} {\ident}$_1$ ... {\ident}$_n$ -{\tt ->} {\tacexpr}\\ +{\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$ +{\tt =>} {\tacexpr}\\ \noindent Recursive and mutual recursive function definitions are also possible with the syntax: \medskip \begin{tabular}{l} -{\tt Recursive Tactic Definition} {\ident}$_1$ {\ident}$_{1,1}$ ... +{\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ... {\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\ -{\tt And} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=} +{\tt with} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=} {\tacexpr}$_2$\\ ...\\ -{\tt And} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=} +{\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=} {\tacexpr}$_n$ \end{tabular} @@ -463,8 +503,7 @@ proof of such a lemma can be done as shown in table~\ref{cnatltac}. \begin{coq_eval} Reset Initial. Require Import Arith. -Require Import PolyList. -Require Import PolyListSyntax. +Require Import List. \end{coq_eval} \begin{table}[ht] @@ -473,15 +512,13 @@ Require Import PolyListSyntax. { \begin{coq_example*} Lemma card_nat : - ~ ( EX x : nat | ( EX y : nat | (forall z:nat, x = z /\ y = z))). + ~ (exists x : nat | exists y : nat | forall z:nat, x = z \/ y = z). Proof. -red; intro H. -elim H; intros a Ha. -elim Ha; intros b Hb. -elim (Hb 0%N); elim (Hb 1%N); elim (Hb 2%N); intros; - match context with - | [_:(?X1 = ?X2),_:(?X1 = ?X3) |- _ ] => - cut (X2 = X3); [ discriminate | apply trans_equal with X1; auto ] +red; intros (x, (y, Hy)). +elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; + match goal with + | [_:(?a = ?b),_:(?a = ?c) |- _ ] => + cut (b = c); [ discriminate | apply trans_equal with a; auto ] end. Qed. \end{coq_example*} @@ -492,8 +529,8 @@ Qed. We can notice that all the (very similar) cases coming from the three eliminations (with three distinct natural numbers) are successfully solved by -a {\tt Match Context} structure and, in particular, with only one pattern (use -of non-linear unification). +a {\tt match goal} structure and, in particular, with only one pattern (use +of non-linear matching). \subsection{Permutation on closed lists} @@ -509,17 +546,12 @@ First, we define the permutation predicate as shown in table~\ref{permutpred}. \begin{coq_example*} Section Sort. Variable A : Set. -Inductive permut : -list A -> list A -> Prop := - | permut_refl : forall l:list A, permut l l - | permut_cons : - forall (a:A) (l0 l1:list A), - permut l0 l1 -> permut (a :: l0) (a :: l1) - | permut_append : - forall (a:A) (l:list A), permut (a :: l) (l ^ a :: nil) - | permut_trans : - forall l0 l1 l2:list A, - permut l0 l1 -> permut l1 l2 -> permut l0 l2. +Inductive permut : list A -> list A -> Prop := + | permut_refl : forall l, permut l l + | permut_cons : forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1) + | permut_append : forall a l, permut (a :: l) (l ++ a :: nil) + | permut_trans : + forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. End Sort. \end{coq_example*} }} @@ -546,8 +578,8 @@ numbers of {\Coq} for the rotation counter. In table~\ref{ltac}, we can see that it is possible to use usual natural numbers but they are only used as arguments for primitive tactics and they cannot be handled, in particular, we cannot make computations with them. So, a natural choice is to use {\Coq} data -structures so that {\Coq} makes the computations (reductions) by {\tt Eval -Compute in} and we can get the terms back by {\tt Match}. +structures so that {\Coq} makes the computations (reductions) by {\tt eval +compute in} and we can get the terms back by {\tt match}. \begin{table}[p] \noindent{}\framebox[6in][l] @@ -555,26 +587,25 @@ Compute in} and we can get the terms back by {\tt Match}. { \begin{coq_example} Ltac Permut n := - match context with - | [ |- (permut _ ?X1 ?X1) ] => apply permut_refl - | [ |- (permut _ (?X1 :: ?X2) (?X1 :: ?X3)) ] => - let newn := eval compute in (length X2) in + match goal with + | |- (permut _ ?l ?l) => apply permut_refl + | |- (permut _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in (apply permut_cons; Permut newn) - | [ |- (permut ?X1 (?X2 :: ?X3) ?X4) ] => + | |- (permut ?A (?a :: ?l1) ?l2) => match eval compute in n with - | [1%N] => fail + | 1 => fail | _ => - let l0' := '(X3 ^ X2 :: nil) in - (apply (permut_trans X1 (X2 :: X3) l0' X4); + let l1' := constr:(l1 ++ a :: nil) in + (apply (permut_trans A (a :: l1) l1' l2); [ apply permut_append | compute; Permut (pred n) ]) end end. Ltac PermutProve := - match context with - | [ |- (permut _ ?X1 ?X2) ] => - match eval compute in - (length X1 = length X2) with - | [(?X1 = ?X1)] => Permut X1 + match goal with + | |- (permut _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => Permut n end end. \end{coq_example} @@ -592,19 +623,15 @@ table~\ref{permutlem}. { \begin{coq_example*} Lemma permut_ex1 : - permut nat (1%N :: 2%N :: 3%N :: nil) (3%N :: 2%N :: 1%N :: nil). + permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). Proof. PermutProve. Qed. + Lemma permut_ex2 : - - permut nat - (0%N - :: 1%N - :: 2%N :: 3%N :: 4%N :: 5%N :: 6%N :: 7%N :: 8%N :: 9%N :: nil) - (0%N - :: 2%N - :: 4%N :: 6%N :: 8%N :: 9%N :: 7%N :: 5%N :: 3%N :: 1%N :: nil). + permut nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). Proof. PermutProve. Qed. @@ -616,7 +643,7 @@ Qed. \subsection{Deciding intuitionistic propositional logic} -The pattern matching on proof contexts allows a complete and so a powerful +The pattern matching on goals allows a complete and so a powerful backtracking when returning tactic values. An interesting application is the problem of deciding intuitionistic propositional logic. Considering the contraction-free sequent calculi {\tt LJT*} of Roy~Dyckhoff (\cite{Dyc92}), it @@ -634,54 +661,53 @@ for the left implication to get rid of the contraction and the right or). { \begin{coq_example} Ltac Axioms := - match context with - | [ |- True ] => trivial - | [_:False |- _ ] => elimtype False; assumption - | [_:?X1 |- ?X1 ] => auto + match goal with + | |- True => trivial + | _:False |- _ => elimtype False; assumption + | _:?A |- ?A => auto end. Ltac DSimplif := repeat - ( - intros; - match context with - | [id:(~ _) |- _ ] => red in id - | [id:(_ /\ _) |- _ ] => + (intros; + match goal with + | id:(~ _) |- _ => red in id + | id:(_ /\ _) |- _ => elim id; do 2 intro; clear id - | [id:(_ \/ _) |- _ ] => + | id:(_ \/ _) |- _ => elim id; intro; clear id - | [id:(?X1 /\ ?X2 -> ?X3) |- _ ] => - cut (X1 -> X2 -> X3); + | id:(?A /\ ?B -> ?C) |- _ => + cut (A -> B -> C); [ intro | intros; apply id; split; assumption ] - | [id:(?X1 \/ ?X2 -> ?X3) |- _ ] => - cut (X2 -> X3); - [ cut (X1 -> X3); - [ intros | intro; apply id; left; assumption ] + | id:(?A \/ ?B -> ?C) |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear id + | intro; apply id; left; assumption ] | intro; apply id; right; assumption ] - | [id0:(?X1 -> ?X2),id1:?X1 |- _ ] => - cut X2; [ intro; clear id0 | apply id0; assumption ] - | [ |- (_ /\ _) ] => split - | [ |- (~ _) ] => red + | id0:(?A -> ?B),id1:?A |- _ => + cut B; [ intro; clear id0 | apply id0; assumption ] + | |- (_ /\ _) => split + | |- (~ _) => red end). Ltac TautoProp := DSimplif; Axioms || - match context with - | [id:((?X1 -> ?X2) -> ?X3) |- _ ] => - - cut (X2 -> X3); - [ intro; cut (X1 -> X2); - [ intro; cut X3; + match goal with + | id:((?A -> ?B) -> ?C) |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; [ intro; clear id | apply id; assumption ] | clear id ] | intro; apply id; intro; assumption ]; TautoProp - | [id:(~ ?X1 -> ?X2) |- _ ] => - cut (False -> X2); - [ intro; cut (X1 -> False); - [ intro; cut X2; + | id:(~ ?A -> ?B) |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; [ intro; clear id | apply id; assumption ] | clear id ] | intro; apply id; red; intro; assumption ]; TautoProp - | [ |- (_ \/ _) ] => (left; TautoProp) || (right; TautoProp) + | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) end. \end{coq_example} }} @@ -701,9 +727,9 @@ Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. Proof. TautoProp. Qed. + Lemma tauto_ex2 : - - forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. Proof. TautoProp. Qed. @@ -727,22 +753,19 @@ table~\ref{isosax}. { \begin{coq_eval} Reset Initial. -Require Import Arith. \end{coq_eval} \begin{coq_example*} +Open Scope type_scope. Section Iso_axioms. -Variables A B C : - Set. -Axiom Com : - A * B = B * A. +Variables A B C : Set. +Axiom Com : A * B = B * A. Axiom Ass : A * (B * C) = A * B * C. Axiom Cur : (A * B -> C) = (A -> B -> C). Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). Axiom P_unit : A * unit = A. Axiom AR_unit : (A -> unit) = unit. Axiom AL_unit : (unit -> A) = A. -Lemma Cons : - B = C -> A * B = A * C. +Lemma Cons : B = C -> A * B = A * C. Proof. intro Heq; rewrite Heq; apply refl_equal. Qed. @@ -768,40 +791,36 @@ CompareStruct}). The main tactic to be called and realizing this algorithm is { \begin{coq_example} Ltac DSimplif trm := - match - trm with - | [(?X1 * ?X2 * ?X3)] => - rewrite <- (Ass X1 X2 X3); try MainSimplif - | [(?X1 * ?X2 -> ?X3)] => - rewrite (Cur X1 X2 X3); try MainSimplif - | [(?X1 -> ?X2 * ?X3)] => - rewrite (Dis X1 X2 X3); try MainSimplif - | [(?X1 * unit)] => - rewrite (P_unit X1); try MainSimplif - | [(unit * ?X1)] => - rewrite (Com unit X1); try MainSimplif - | [(?X1 -> unit)] => - rewrite (AR_unit X1); try MainSimplif - | [(unit -> ?X1)] => - rewrite (AL_unit X1); try MainSimplif - | [(?X1 * ?X2)] => - (DSimplif X1; try MainSimplif) || (DSimplif X2; try MainSimplif) - | [(?X1 -> ?X2)] => - (DSimplif X1; try MainSimplif) || (DSimplif X2; try MainSimplif) + match trm with + | (?A * ?B * ?C) => + rewrite <- (Ass A B C); try MainSimplif + | (?A * ?B -> ?C) => + rewrite (Cur A B C); try MainSimplif + | (?A -> ?B * ?C) => + rewrite (Dis A B C); try MainSimplif + | (?A * unit) => + rewrite (P_unit A); try MainSimplif + | (unit * ?B) => + rewrite (Com unit B); try MainSimplif + | (?A -> unit) => + rewrite (AR_unit A); try MainSimplif + | (unit -> ?B) => + rewrite (AL_unit B); try MainSimplif + | (?A * ?B) => + (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) + | (?A -> ?B) => + (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) end with MainSimplif := - match context with - | [ |- (?X1 = ?X2) ] => try DSimplif X1; try DSimplif X2 + match goal with + | |- (?A = ?B) => try DSimplif A; try DSimplif B end. Ltac Length trm := - match - trm with - | [(_ * ?X1)] => let succ := Length X1 in - '(S succ) - | _ => '1%N + match trm with + | (_ * ?B) => let succ := Length B in constr:(S succ) + | _ => constr:1 end. -Ltac assoc := repeat - rewrite <- Ass. +Ltac assoc := repeat rewrite <- Ass. \end{coq_example} }} \caption{Type isomorphism tactic (1)} @@ -814,25 +833,25 @@ Ltac assoc := repeat { \begin{coq_example} Ltac DoCompare n := - match context with - | [ |- (?X1 = ?X1) ] => apply refl_equal - | [ |- (?X1 * ?X2 = ?X1 * ?X3) ] => - apply Cons; let newn := Length X2 in + match goal with + | [ |- (?A = ?A) ] => apply refl_equal + | [ |- (?A * ?B = ?A * ?C) ] => + apply Cons; let newn := Length B in DoCompare newn - | [ |- (?X1 * ?X2 = ?X3) ] => + | [ |- (?A * ?B = ?C) ] => match eval compute in n with - | [1%N] => fail + | 1 => fail | _ => - pattern (X1 * X2) 1; rewrite Com; assoc; DoCompare (pred n) + pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n) end end. Ltac CompareStruct := - match context with - | [ |- (?X1 = ?X2) ] => - let l1 := - Length X1 with l2 := Length X2 in + match goal with + | [ |- (?A = ?B) ] => + let l1 := Length A + with l2 := Length B in match eval compute in (l1 = l2) with - | [(?X1 = ?X1)] => DoCompare X1 + | (?n = ?n) => DoCompare n end end. Ltac IsoProve := MainSimplif; CompareStruct. @@ -850,15 +869,15 @@ Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}. { \begin{coq_example*} Lemma isos_ex1 : - forall A B:Set, A * unit * B = B * (unit * A). + forall A B:Set, A * unit * B = B * (unit * A). Proof. intros; IsoProve. Qed. + Lemma isos_ex2 : - - forall A B C:Set, - (A * unit -> B * (C * unit)) = - (A * unit -> (C -> unit) * C) * (unit -> A -> B). + forall A B C:Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). Proof. intros; IsoProve. Qed. diff --git a/doc/Translator.tex b/doc/Translator.tex new file mode 100644 index 0000000000..02cbdf02e8 --- /dev/null +++ b/doc/Translator.tex @@ -0,0 +1,416 @@ +\ifx\pdfoutput\undefined % si on est pas en pdflatex +\documentclass[11pt,a4paper]{article} +\else +\documentclass[11pt,a4paper,pdftex]{article} +\fi +\usepackage[latin1]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{pslatex} +\usepackage{url} +\usepackage{verbatim} + +\title{Translation from Coq V7 to V8} +\author{The Coq Development Team} + +%% Macros etc. +\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 + +\section{Introduction} + +The goal of this document is to introduce to the new syntax of Coq on +simple examples, rather than just giving the new grammar. It is +strongly recommended to read first the definition of the new syntax +(in the reference manual), but this document should also be useful for +the eager user who wants to start with the new syntax quickly. + +\section{The new syntax on examples} + +The toplevel has an option {\tt -translate} which allows to +interactively translate commands. All the examples below can be tested +by entering the V7 commands in the toplevel launched this option. This +toplevel translator accepts a command, prints the translation on +standard output (after a \verb+New syntax:+ balise), executes the +command, and waits for another command. The only requirements is that +they should be syntactically correct, but they do not have to be +well-typed. + +%% + +\subsection{Changes in lexical conventions w.r.t. V7} + +\subsubsection{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. + +Furthermore, only letters (unicode letters), digits, single quotes and +_ are allowed after the first character. + +\subsubsection{Quoted string} + +Quoted strings are used typically to give a filename (which may not +be a regular identifier). As before they are written between double +quotes ("). Unlike for V7, there is no escape character: characters +are written normaly but the double quote which is doubled. + +\subsection{Main changes in terms w.r.t. V7} + + +\subsubsection{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 it possible to remove 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} + + +\subsubsection{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 & delimiter \\ +\hline +types & type_scope & \TERM{T} \\ +\TERM{bool} & bool_scope & \\ +\TERM{nat} & nat_scope & \TERM{nat} \\ +\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. Scope nat_scope is opened in the initial state of Coq. +\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 +scope. 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$ \\ +type_scope & $* ~+$ \\ +bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\ +list_scope & $\TERM{::} ~\TERM{++}$ +\end{tabular} +\end{center} +(Note: $\leq$ is written \TERM{$<=$}) + + + +\subsubsection{Notation for implicit arguments} + +The explicitation of arguments is closer to the \emph{bindings} notation in +tactics. Argument positions follow the argument names of the head constant. + +\begin{transbox} +\TRANS{f 1!t1 2!t2}{f (x:=t1) (y:=t2)} +\TRANS{!f t1 t2}{@f t1 t2} +\end{transbox} + + +\subsubsection{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} + +\subsubsection{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} + + +\subsubsection{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 objects. + +The idea is that for each destructured object, one may specify a variable +name to tell how the branches types depend on this destructured objects (case +of a dependent elimination), and also how they depend on the value of the +arguments of the inductive type of the destructured objects. 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} + + +\subsubsection{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 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. + +\subsubsection{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. + +\subsubsection{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} + +\subsubsection{Named arguments of theorems} + +\begin{transbox} +\TRANS{Apply thm with x:=t 1:=u}{apply thm with (x:=t) (1:=u)} +\end{transbox} + + +\subsubsection{Occurrences} + +To avoid ambiguity between a numeric literal and the optionnal +occurence numbers of this term, the occurence numbers are put after +the term itself. This applies to tactic \TERM{pattern} and also +\TERM{unfold} +\begin{transbox} +\TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern (f x at 1 2) (d at 3 4) y z} +\end{transbox} + + +\subsection{Main changes in vernacular commands w.r.t. V7} + + +\subsubsection{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} + +\subsubsection{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{Hint Extern 4 (toto ?) Apply lemma}{Hint Extern 4 (toto _) => apply lemma} +\end{transbox} + + + + +%% Doc of the translator +\section{A guide to translation} + +\subsection{Overview of the translation process} + +Tools: +\begin{itemize} +\item {\tt coqc -translate} +is the automatic translator. It is a parser/pretty-printer. This means +that the translation is made by parsing using a parser of old syntax, +and every command is printed using the new syntax. Many efforts were +made to preserve as much as possible the quality of the presentation: +it avoids expansion of syntax extensions, comments are not discarded +and placed at the same place. +\item {\tt tools/check-v8} will help translate developments that +compile with a Makefile with minimum requirements. +\end{itemize} + +\subsection{What to do before the translation} + +First of all, it is mandatory that files compile with the current +version of Coq with option {\tt -v7}. Translation is a complicated +task that involves the full compilation of the development. If your +development was compiled with older versions, first upgrade to Coq V8 +with option {\tt -v7}. If you use a Makefile similar to those produced +by {\tt coq\_makefile}, you probably just have to do + +{\tt make OPT="-opt -v7"} ~~~or~~~ {\tt make OPT="-byte -v7"} + +When the development compiles successfully, there are several changes +that might be necessary for the translation. Essentially, this is +about syntax extensions (see section below dedicated to porting syntax +extensions). If you do not use such features, then you can try and +make the translation. + +The preferred way is to use script {\tt check-v8} if your development +is compiled by a Makfile with the following constraints: +\begin{itemize} +\item compilation is achievd by invoke make without arguments +\item options are passed to Coq with make variable COQFLAGS that + includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML. +\end{itemize} +These constraints are met by the makefiles produced by {\tt coq\_makefile} + +Otherwise, modify your build program so as to pass option {\tt +-translate} to program {\tt coqc}. The effect of this option is to +ouptut the translated source of any {\tt .v} file in a file with +extension {\tt .v8} located in the same directory than the original +file. + +The following section describes events that may happen during the +translation and measures to adopt. + +\subsection{What may happens during the translation} + +Warnings: + +... + +\subsection{Errors occurring after translation} + +Equality in {\tt Z} or {\tt R}... + + + +\subsection{Particular cases} + +\subsubsection{Lexical conventions} + +The definition of identifiers changed. Most of those changes are +handled by the translator. They include: +\begin{itemize} +\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt +x\_} +\item avoid clash with new keywords by adding a trailing {\tt \_} +\end{itemize} + +If the choices made by translation or in the following cases: +\begin{itemize} +\item usage of latin letters +\item usage if iso-latin characters in notations +\end{itemize} +the user should change his development prior to translation. + + +\subsubsection{Syntax extensions} + +\paragraph{Notation and Infix} + +These commands do not necessarily need to be changed. + +Some work will have to be done manually if the notation conflicts with +the new syntax (for instance, using keywords like {\tt fun} or {\tt +exists}, overloading of symbols of the old syntax). + + +\paragraph{Grammar and Syntax} + +{\tt Grammar} and {\tt Syntax} are not supported by translation. They +should be replaced by an equivalent {\tt Notation} command and be +processed as decribed above. Before attempting translation, users +should verify that compilation with option {\tt -v7} succeeds. + +In the cases where {\tt Grammar} and {\tt Syntax} cannot be emulated +by {\tt Notation}, users have to change manually they development as +they wish to avoid the use of {\tt Grammar}. If this is not done, the +translator will simply expand the notations and the output of the +translator will use the reuglar Coq syntax. + + +\end{document} |