diff options
Diffstat (limited to 'doc/refman/RefMan-ssr.tex')
| -rw-r--r-- | doc/refman/RefMan-ssr.tex | 4933 |
1 files changed, 0 insertions, 4933 deletions
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex deleted file mode 100644 index 31dabcdd4..000000000 --- a/doc/refman/RefMan-ssr.tex +++ /dev/null @@ -1,4933 +0,0 @@ -\achapter{The SSReflect proof language} -%HEVEA\cutname{ssreflect.html} -\aauthor{Georges Gonthier, Assia Mahboubi, Enrico Tassi} - -\newcommand{\ssr}{{\sc SSReflect}} - -% listing -\ifhevea\newcommand{\ssrC}[1]{\texttt{#1}}\else\newcommand{\ssrC}[1]{\text{\lstinline!#1!}}\fi -\ifhevea\renewenvironment{center}{\@open{div}{class="center"}\@open{div}{class="centered"}}{\@close{div}\@close{div}}\fi -% non-terminal -%\newcommand\ssrN[2][]{\ensuremath{\langle\mbox{\itshape\rmfamily\small #2}\rangle_{#1}}} -\newcommand\ssrN[2][]{{\textsl {#2}}\ensuremath{_{#1}}} -\ifhevea\newcommand{\underbar}[1]{\underline{#1}}\fi - -% TODO: only use \ssrC -\let\ssrL=\lstinline - -\newcommand{\iitem}{{\it i-item}} -\newcommand{\ditem}{{\it d-item}} -\newcommand{\optional}[1]{{\it[}#1{\it]}} -\newcommand{\optsep}{{\it|}} -\newcommand{\idx}[1]{\tacindex{#1 (ssreflect)}} -\newcommand{\idxC}[1]{\comindex{#1 (ssreflect)}} - -\newenvironment{new}% - {\begin{Sbox}\begin{minipage}{0.97\textwidth}% - \begin{flushright}\textcolor{red}{\fbox{Version 1.3}}% - \end{flushright}\noindent}% - {\end{minipage}\end{Sbox}\noindent\doublebox{\TheSbox}} -\section{Introduction}\label{sec:intro} - -This chapter describes a set of tactics known as \ssr{} -originally designed to provide support for the so-called \emph{small scale -reflection} proof methodology. Despite the original purpose this set of tactic -is of general interest and is available in Coq starting from version 8.7. - -\ssr{} was developed independently of the tactics described in -Chapter~\ref{Tactics}. Indeed the scope of the tactics part of -\ssr{} largely overlaps with the standard set of tactics. Eventually -the overlap will be reduced in future releases of Coq. - -Proofs written in \ssr{} typically look quite different from the -ones written using only tactics as per Chapter~\ref{Tactics}. -We try to summarise here the most ``visible'' ones in order to -help the reader already accustomed to the tactics described in -Chapter~\ref{Tactics} to read this chapter. - -The first difference between the tactics described in this -chapter and the tactics described in Chapter~\ref{Tactics} is the way -hypotheses are managed (we call this \emph{bookkeeping}). -In Chapter~\ref{Tactics} the most common -approach is to avoid moving explicitly hypotheses back and forth -between the context and the conclusion of the goal. On the contrary -in \ssr{} -all bookkeeping is performed on the conclusion of the goal, using for -that purpose a couple of syntactic constructions behaving similar to -tacticals (and often named as such in this chapter). -The \ssrC{:} tactical moves hypotheses from the context to the -conclusion, while \ssrC{=>} moves hypotheses from the -conclusion to the context, and \ssrC{in} moves back -and forth an hypothesis from the context to the conclusion for the -time of applying an action to it. - -While naming hypotheses is commonly done by means of an \ssrC{as} -clause in the basic model of Chapter~\ref{Tactics}, it is here to -\ssrC{=>} that this task is devoted. As tactics leave -new assumptions in the conclusion, and are often followed by -\ssrC{=>} to explicitly name them. -While generalizing the goal is normally -not explicitly needed in Chapter~\ref{Tactics}, it is an explicit -operation performed by \ssrC{:}. - -Beside the difference of bookkeeping model, this chapter includes -specific tactics which have no explicit counterpart in -Chapter~\ref{Tactics} such as tactics to mix forward steps and -generalizations as \ssrC{generally have} or \ssrC{without loss}. - -\ssr{} adopts the point of view that rewriting, definition -expansion and partial evaluation participate all to a same concept of -rewriting a goal in a larger sense. As such, all these functionalities are -provided by the \ssrC{rewrite} tactic. - -\ssr{} includes a little language of patterns to select subterms in tactics -or tacticals where it matters. Its most notable application -is in the \ssrC{rewrite} tactic, where patterns are used to specify -where the rewriting step has to take place. - -Finally, \ssr{} supports so-called reflection steps, typically -allowing to switch back and forth between the computational view and -logical view of a concept. - -To conclude it is worth mentioning that \ssr{} tactics -can be mixed with non \ssr{} tactics in the same proof, -or in the same Ltac expression. The few exceptions -to this statement are described in section~\ref{sec:compat}. - -\iffalse -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{How to read this documentation} - -The syntax of the tactics is presented as follows: -\begin{itemize} -\item \ssrC{terminals} are in typewriter font and \ssrN{non terminals} are - between angle brackets. -\item Optional parts of the grammar are surrounded by \optional{ } - brackets. These should not be confused with verbatim brackets - \ssrC{[ ]}, which are delimiters in the \ssr{} syntax. -\item A vertical rule {\optsep} indicates an alternative in the syntax, and - should not be confused with a - verbatim vertical rule between verbatim brackets \ssrC{[ | ]}. -\item A non empty list of non terminals (at least one item should be - present) is represented by \ssrN{non terminals}$^+$. A possibly empty - one is represented by \ssrN{non terminals}$^*$. -\item In a non empty list of non terminals, items are separated by blanks. -\end{itemize} -\fi - -% Hevea has no colors -\ifhevea \else -\noindent We follow the default color scheme of the \ssr{} mode for -ProofGeneral provided in the distribution: - -\centerline{ -\textcolor{dkblue}{\texttt{tactic}} or \textcolor{dkviolet}{\tt - Command} or \textcolor{dkgreen}{\tt keyword} or -\textcolor{dkpink}{\tt tactical}} - -\noindent Closing tactics/tacticals like \ssrC{exact} or \ssrC{by} (see section -\ref{ssec:termin}) are in red. -\fi - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{Acknowledgments} -The authors would like to thank Frédéric Blanqui, François Pottier -and Laurence Rideau for their comments and suggestions. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newpage\section{Usage} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Getting started}\label{sec:files} -To be available, the tactics presented in this manual need the -following minimal set of libraries to loaded: {\tt ssreflect.v}, {\tt -ssrfun.v} and {\tt ssrbool.v}. Moreover, these tactics come with a -methodology specific to the authors of Ssreflect and which requires a -few options to be set in a different way than in their default -way. All in all, this corresponds to working in the following context: - -\begin{lstlisting} - From Coq Require Import ssreflect ssrfun ssrbool. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Compatibility issues}\label{sec:compat} -Requiring the above modules creates an environment which -is mostly compatible with the rest of \Coq{}, up to a few discrepancies: -\begin{itemize} -\item New keywords (\ssrC{is}) might clash with variable, constant, -tactic or tactical names, or with quasi-keywords in tactic or -vernacular notations. -\item New tactic(al)s names (\ssrC{last}, \ssrC{done}, \ssrC{have}, - \ssrC{suffices}, \ssrC{suff}, - \ssrC{without loss}, \ssrC{wlog}, \ssrC{congr}, \ssrC{unlock}) might clash - with user tactic names. -\item Identifiers with both leading and trailing \ssrC{_}, such as \ssrC{_x_}, -are reserved by \ssr{} and cannot appear in scripts. -\item The extensions to the \ssrC{rewrite} tactic are partly -incompatible with those available in current versions of \Coq{}; -in particular: -\ssrC{rewrite .. in (type of k)} or \\ \ssrC{rewrite .. in *} or any other -variant of \ssrC{rewrite} will not work, and the \ssr{} syntax and semantics for occurrence selection and -rule chaining is different. - -Use an explicit rewrite direction (\ssrC{rewrite <-} $\dots$ or \ssrC{rewrite ->} $\dots$) -to access the \Coq{} \ssrC{rewrite} tactic. -\item New symbols (\ssrC{//, /=, //=}) might clash with adjacent existing - symbols (e.g., '\ssrC{//}') instead of '\ssrC{/}''\ssrC{/}'). This can be avoided - by inserting white spaces. -\item New constant and theorem names might clash with the user -theory. This can be avoided by not importing all of \ssr{}: -\begin{lstlisting} - From Coq Require ssreflect. - Import ssreflect.SsrSyntax. -\end{lstlisting} -Note that the full syntax of \ssr{}'s {\tt rewrite} and reserved identifiers are -enabled only if the \ssrC{ssreflect} module has been required and if -\ssrC{SsrSyntax} has been imported. Thus a file that requires (without importing) - \ssrC{ssreflect} and imports \ssrC{SsrSyntax}, can be -required and imported without automatically enabling \ssr{}'s -extended rewrite syntax and reserved identifiers. -\item Some user notations (in particular, defining an infix ';') might -interfere with the "open term", parenthesis free, syntax of tactics -such as \ssrC{have}, \ssrC{set} and \ssrC{pose}. -\item The generalization of \ssrC{if} statements to non-Boolean -conditions is turned off by \ssr{}, because it is mostly subsumed by -\ssrC{Coercion} to \ssrC{bool} of the \ssrC{sum}XXX types (declared in -\ssrC{ssrfun.v}) -and the \ssrC{if} {\term} \ssrC{is} \ssrN{pattern} \ssrC{then} {\term} \ssrC{else} {\term} construct (see -\ref{ssec:patcond}). To use the generalized form, turn off the \ssr{} -Boolean \ssrC{if} notation using the command: -\begin{lstlisting} - Close Scope boolean_if_scope. -\end{lstlisting} -\item The following two options can be unset to disable the - incompatible \ssrC{rewrite} syntax and allow - reserved identifiers to appear in scripts. -\begin{lstlisting} - Unset SsrRewrite. - Unset SsrIdents. -\end{lstlisting} -\end{itemize} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Gallina extensions} - -Small-scale reflection makes an extensive use of the programming -subset of Gallina, \Coq{}'s logical specification language. This subset -is quite suited to the description of functions on representations, -because it closely follows the well-established design of the ML -programming language. The \ssr{} extension provides three additions -to Gallina, for pattern assignment, pattern testing, and polymorphism; -these mitigate minor but annoying discrepancies between Gallina and ML. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Pattern assignment}\label{ssec:patass} -The \ssr{} extension provides the following construct for -irrefutable pattern matching, that is, destructuring assignment: - -\ssrC{let: } \ssrN{pattern} \ssrC{:=} \ssrN[1]{term} \ssrC{in} \ssrN[2]{term} - -Note the colon `\ssrC{:}' after the \ssrC{let} keyword, which avoids any -ambiguity with a function -definition or \Coq{}'s basic destructuring \ssrC{let}. The \ssrC{let:} -construct differs from the latter in that -\begin{itemize} -\item The pattern can be nested (deep pattern matching), in - particular, this allows expression of the form: -\begin{lstlisting} - let: exist (x, y) p_xy := Hp in ... -\end{lstlisting} -\item The destructured constructor is explicitly given in the - pattern, and is used for type inference, e.g., -\begin{lstlisting} - Let f u := let: (m, n) := u in m + n. -\end{lstlisting} -using a colon \ssrC{let:}, infers \ssrC{f : nat * nat -> nat}, whereas -\begin{lstlisting} - Let f u := let (m, n) := u in m + n. -\end{lstlisting} -with a usual \ssrC{let}, requires an extra type annotation. -\end{itemize} -The \ssrC{let:} construct is just (more legible) notation for the primitive Gallina expression - -\begin{center} -\ssrC{match} \ssrN[1]{term} \ssrC{with} \ssrN{pattern} \ssrC{=>} \ssrN[2]{term} \ssrC{end} -\end{center} - -The \ssr{} destructuring assignment supports all the dependent match -annotations; the full syntax is - -\begin{center} -\ssrC{let:} \ssrN[1]{pattern} \ssrC{as} \ssrN{ident} \ssrC{in} \ssrN[2]{pattern} \ssrC{:=} \ssrN[1]{term} \ssrC{return} \ssrN[2]{term} \ssrC{in} \ssrN[3]{term} -\end{center} - -where \ssrN[2]{pattern} is a \emph{type} pattern and \ssrN[1]{term} and -\ssrN[2]{term} are types. - -When the \ssrC{as} and \ssrC{return} are both present, then \ssrN{ident} is bound -in both the type \ssrN[2]{term} and the expression \ssrN[3]{term}; -variables in the optional type pattern \ssrN[2]{pattern} are -bound only in the type \ssrN[2]{term}, and other variables in \ssrN[1]{pattern} are -bound only in the expression \ssrN[3]{term}, however. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Pattern conditional}\label{ssec:patcond} -The following construct can be used for a refutable pattern matching, -that is, pattern testing: - -\begin{center} -\ssrC{if}\ \ssrN[1]{term} \ssrC{is} \ssrN[1]{pattern} \ssrC{then} \ssrN[2]{term} \ssrC{else} \ssrN[3]{term} -\end{center} - -Although this construct is not strictly ML (it does exits in variants -such as the pattern calculus or the $\rho$-calculus), it turns out to be -very convenient for writing functions on representations, -because most such functions manipulate simple datatypes such as Peano -integers, options, -lists, or binary trees, and the pattern conditional above is almost -always the right construct -for analyzing such simple types. For example, the \ssrC{null} and -\ssrC{all} list function(al)s can be defined as follows: -\begin{lstlisting} - Variable d: Set. - Fixpoint |*null*| (s : list d) := if s is nil then true else false. - Variable a : d -> bool. - Fixpoint |*all*| (s : list d) : bool := - if s is cons x s' then a x && all s' else true. -\end{lstlisting} - -The pattern conditional also provides a notation for destructuring -assignment with a refutable pattern, adapted to the pure functional -setting of Gallina, which lacks a \\\texttt{Match\_Failure} exception. - -Like \ssrC{let:} above, the \ssrC{if}$\dots$\ssrC{is} construct is just (more legible) -notation for the primitive Gallina expression: - -\begin{center} -\ssrC{match} \ssrN[1]{term} \ssrC{with} \ssrN{pattern} \ssrC{=>} \ssrN[2]{term} \ssrC{| _ =>} \ssrN[2]{term} \ssrC{end} -\end{center} - -Similarly, it will always be displayed as the expansion of this form -in terms of primitive \ssrC{match} expressions (where the default -expression $\ssrN[3]{term}$ may be replicated). - - -Explicit pattern testing also largely subsumes the generalization of -the \ssrC{if} construct to all binary datatypes; compare: - -\begin{center} -\ssrC{if} {\term} \ssrC{is inl _ then} \ssrN[l]{term} \ssrC{else} \ssrN[r]{term} -\end{center} - -and: - -\begin{center} -\ssrC{if} {\term} \ssrC{then} \ssrN[l]{term} \ssrC{else} \ssrN[r]{term} -\end{center} - -The latter appears to be marginally shorter, but it is quite -ambiguous, and indeed often -requires an explicit annotation term : \ssrC{\{_\}+\{_\}} to type-check, -which evens the character count. - -Therefore, \ssr{} restricts by default the condition of a plain \ssrC{if} -construct to the standard \ssrC{bool} type; this avoids spurious type -annotations, e.g., in: -\begin{lstlisting} - Definition |*orb*| b1 b2 := if b1 then true else b2. -\end{lstlisting} -As pointed out in section~\ref{sec:compat}, this restriction can be removed with -the command: -\begin{lstlisting} - Close Scope boolean_if_scope. -\end{lstlisting} -Like \ssrC{let:} above, the \ssrC{if} {\term} \ssrC{is} \ssrN{pattern} -\ssrC{else} {\term} construct -supports the dependent \ssrC{match} annotations: - -\begin{center} -\ssrC{if} \ssrN[1]{term} \ssrC{is} \ssrN[1]{pattern} \ssrC{as} \ssrN{ident} \ssrC{in} \ssrN[2]{pattern} \ssrC{return} \ssrN[2]{term} \ssrC{then} \ssrN[3]{term} \ssrC{else} \ssrN[4]{term} -\end{center} - -As in \ssrC{let:} the variable \ssrN{ident} (and those in -the type pattern \ssrN[2]{pattern}) are bound in \ssrN[2]{term}; \ssrN{ident} is -also bound in \ssrN[3]{term} (but not in \ssrN[4]{term}), while the -variables in \ssrN[1]{pattern} are bound only in \ssrN[3]{term}. - -\noindent -Another variant allows to treat the else case first: - -\begin{center} -\ssrC{if} \ssrN[1]{term} \ssrC{isn't} \ssrN[1]{pattern} \ssrC{then} \ssrN[2]{term} \ssrC{else} \ssrN[3]{term} -\end{center} - -Note that \ssrN[1]{pattern} eventually binds variables in \ssrN[3]{term} -and not \ssrN[2]{term}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Parametric polymorphism}\label{ssec:parampoly} - -Unlike ML, polymorphism in core Gallina is explicit: the type -parameters of polymorphic functions must be declared explicitly, and -supplied at each point of use. However, \Coq{} provides two features -to suppress redundant parameters: -\begin{itemize} -\item Sections are used to provide (possibly implicit) parameters for - a set of definitions. -\item Implicit arguments declarations are used to tell \Coq{} to use - type inference to deduce some parameters from the context at each - point of call. -\end{itemize} -The combination of these features provides a fairly good emulation of ML-style -polymorphism, but unfortunately this emulation breaks down for -higher-order programming. Implicit arguments are indeed not inferred -at all points of use, but only at -points of call, leading to expressions such as -\begin{lstlisting} - Definition |*all_null*| (s : list T) := all (@null T) s. -\end{lstlisting} -Unfortunately, such higher-order expressions are quite frequent in -representation functions, especially those which use \Coq{}'s -\ssrC{Structure}s to emulate Haskell type classes. - -Therefore, \ssr{} provides a variant of \Coq{}'s implicit argument -declaration, which causes \Coq{} to fill in some implicit parameters -at each point of use, e.g., the above definition can be written: -\begin{lstlisting} - Definition |*all_null*| (s : list d) := all null s. -\end{lstlisting} -Better yet, it can be omitted entirely, since \ssrC{all_null s} isn't -much of an improvement over \ssrC{all null s}. - -The syntax of the new declaration is - -\begin{center} -\ssrC{Prenex Implicits} \ssrN{ident}$^+$. -\end{center} - -Let us denote $_1 \dots c_n$ the list of identifiers given to a -\ssrC{Prenex Implicits} command. -The command checks that each $c_i$ is the name of a functional -constant, whose implicit arguments are prenex, i.e., the first $n_i > -0$ arguments of $c_i$ are implicit; then it assigns -\ssrC{Maximal Implicit} status to these arguments. - -As these prenex implicit arguments are ubiquitous and have often large -display strings, it is strongly recommended to change the default -display settings of \Coq{} so that they are not printed (except after a -\ssrC{Set Printing All} command). -All \ssr{} library files thus start with the incantation -\begin{lstlisting} - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Anonymous arguments} - -When in a definition, the type of a certain argument is mandatory, but -not its name, one usually use ``arrow'' abstractions for prenex -arguments, or the \ssrC{(_ : }{\term}\ssrC{)} syntax for inner arguments. -In \ssr{}, the latter can be replaced by the open syntax `\ssrC{of\ }{\term}' -or (equivalently) `\ssrC{& }{\term}', which are both syntactically -equivalent to a \ssrC{(_ : }{\term}\ssrC{)} expression. - -For instance, the usual two-contrsuctor polymorphic type \ssrC{list}, -i.e. the one of the -standard {\tt List} library, can be defined by the following -declaration: -\begin{lstlisting} - Inductive list (A : Type) : Type := nil | cons of A & list A. -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Wildcards}\label{ssec:wild} - -The terms passed as arguments -to \ssr{} tactics can contain \emph{holes}, materialized by wildcards -\ssrC{_}. -Since \ssr{} allows a more powerful form of type inference for these -arguments, it enhances the possibilities of using such wildcards. -These holes are in particular used as a convenient shorthand for -abstractions, especially in local definitions or type expressions. - -Wildcards may be interpreted as abstractions (see for example sections -\ref{ssec:pose} and \ref{ssec:struct}), or their content can be -inferred from the whole -context of the goal (see for example section \ref{ssec:set}). -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Definitions} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Definitions}\label{ssec:pose} -\idx{pose \dots{} := \dots{}} -\idx{pose fix \dots{} := \dots{}} -\idx{pose cofix \dots{} := \dots{}} - -The \ssrC{pose} tactic allows to add a defined constant to a -proof context. \ssr{} generalizes this tactic in several ways. -In particular, the \ssr{} \ssrC{pose} tactic supports \emph{open syntax}: -the body of -the definition does not need surrounding parentheses. For instance: -\begin{lstlisting} - pose t := x + y. -\end{lstlisting} -is a valid tactic expression. - -The \ssrC{pose} tactic is also improved for the -local definition of higher order terms. -Local definitions of functions can use the same syntax as -global ones. The tactic: -\begin{lstlisting} - pose f x y := x + y. -\end{lstlisting} -adds to the context the defined constant: -\begin{lstlisting} - f := fun x y : nat => x + y : nat -> nat -> nat -\end{lstlisting} - -The \ssr{} \ssrC{pose} tactic also supports (co)fixpoints, -by providing the local counterpart of the -\ssrC{Fixpoint f := $\dots$ } and \ssrC{CoFixpoint f := $\dots$ } constructs. -For instance, the following tactic: -\begin{lstlisting} - pose fix f (x y : nat) {struct x} : nat := - if x is S p then S (f p y) else 0. -\end{lstlisting} -defines a local fixpoint \ssrC{f}, which mimics the standard \ssrC{plus} -operation on natural numbers. - -Similarly, local cofixpoints can be defined by a tactic of the form: -\begin{lstlisting} - pose cofix f (arg : T) ... -\end{lstlisting} - -The possibility to include wildcards in the body of the definitions - offers a smooth -way of defining local abstractions. The type of ``holes'' is -guessed by type inference, and the holes are abstracted. -For instance the tactic: -\begin{lstlisting} - pose f := _ + 1. -\end{lstlisting} -is shorthand for: -\begin{lstlisting} - pose f n := n + 1. -\end{lstlisting} - -When the local definition of a function involves both arguments and -holes, hole abstractions appear first. For instance, the -tactic: -\begin{lstlisting} - pose f x := x + _. -\end{lstlisting} -is shorthand for: -\begin{lstlisting} - pose f n x := x + n. -\end{lstlisting} - - -The interaction of the \ssrC{pose} tactic with the interpretation of -implicit arguments results in a powerful and concise syntax for local -definitions involving dependent types. -For instance, the tactic: -\begin{lstlisting} - pose f x y := (x, y). -\end{lstlisting} -adds to the context the local definition: -\begin{lstlisting} - pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). -\end{lstlisting} -The generalization of wildcards makes the use of the \ssrC{pose} tactic -resemble ML-like definitions of polymorphic functions. - -% The use of \ssrC{Prenex Implicits} declarations (see section -% \ref{ssec:parampoly}), makes this feature specially convenient. -% Note that this combines with the interpretation of wildcards, and that -% it is possible to define: -% \begin{lstlisting} -% pose g x y : prod _ nat := (x, y). -% \end{lstlisting} -% which is equivalent to: -% \begin{lstlisting} -% pose g x (y : nat) := (x, y). -% \end{lstlisting} - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Abbreviations}\label{ssec:set} -\idx{set \dots{} := \dots{}} - - -The \ssr{} \ssrC{set} tactic performs abbreviations: it introduces a -defined constant for a subterm appearing in the goal and/or in the -context. - -\ssr{} extends the \ssrC{set} tactic by supplying: -\begin{itemize} -\item an open syntax, similarly to the \ssrC{pose} tactic; -\item a more aggressive matching algorithm; -\item an improved interpretation of wildcards, taking advantage of the - matching algorithm; -\item an improved occurrence selection mechanism allowing to abstract only - selected occurrences of a term. -\end{itemize} - -The general syntax of this tactic is -\begin{center} -\ssrC{set} \ssrN{ident} \optional{\ssrC{:} \ssrN[1]{term}} \ssrC{:=} \optional{\ssrN{occ-switch}} \ssrN[2]{term} -\end{center} -\begin{center} -\ssrN{occ-switch} ::= \ssrC{\{}[\ssrC{+}|\ssrC{-}] {\naturalnumber}$^*$ \ssrC{\}} -\end{center} - - -where: - -\begin{itemize} -\item \ssrN{ident} is a fresh identifier chosen by the user. -\item \ssrN[1]{term} is -an optional type annotation. The type annotation \ssrN[1]{term} can be -given in open syntax (no surrounding parentheses). If no \ssrN{occ-switch} -(described hereafter) is present, it is also -the case for \ssrN[2]{term}. -On the other hand, in presence of \ssrN{occ-switch}, parentheses -surrounding \ssrN[2]{term} are mandatory. -\item In the occurrence switch \ssrN{occ-switch}, if the first element - of the list is a {\naturalnumber}, this element should be a number, and not - an Ltac variable. The empty list \ssrC{\{\}} is not interpreted as a - valid occurrence switch. -\end{itemize} -% For example, the script: -% \begin{lstlisting} -% Goal forall (f : nat -> nat)(x y : nat), f x + f x = f x. -% move=> f x y. -% \end{lstlisting} - -The tactic: -\begin{lstlisting} - set t := f _. -\end{lstlisting} -transforms the goal \ssrC{f x + f x = f x} into \ssrC{t + t = t}, adding -\ssrC{t := f x} to the context, and the tactic: -\begin{lstlisting} - set t := {2}(f _). -\end{lstlisting} -transforms it into \ssrC{f x + t = f x}, adding \ssrC{t := f x} to the context. - -The type annotation \ssrN[1]{term} may -contain wildcards, which will be filled with the appropriate value by -the matching process. - -The tactic first tries to find a subterm of the goal matching -\ssrN[2]{term} (and its type \ssrN[1]{term}), -and stops at the first subterm it finds. Then the occurrences -of this subterm selected by the optional \ssrN{occ-switch} are replaced -by \ssrN{ident} and a definition \ssrN{ident} \ssrC{:=} {\term} is added to -the context. If no \ssrN{occ-switch} is present, then all the -occurrences are abstracted. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Matching} - -The matching algorithm compares a pattern \textit{term} - with a subterm of the goal by comparing their heads -and then pairwise unifying their arguments (modulo conversion). Head -symbols match under the following conditions: - -\begin{itemize} -\item If the head of \textit{term} is a constant, then it - should be syntactically equal to the head symbol of the subterm. -\item If this head is a projection of a canonical structure, - then canonical structure equations are used for the matching. -\item If the head of \textit{term} is \emph{not} a constant, the - subterm should have the same structure ($\lambda$ abstraction, - \ssrC{let}$\dots$\ssrC{in} structure \dots). -\item If the head of \textit{term} is a hole, the subterm should have - at least as many arguments as \textit{term}. For instance the tactic: -\begin{lstlisting} - set t := _ x. -\end{lstlisting} -transforms the goal \ssrL-x + y = z- into \ssrC{t y = z} and adds -\ssrC{t := plus x : nat -> nat} to the context. - -\item In the special case where \textit{term} is of the form - \ssrC{(let f := }$t_0$ \ssrC{in f) }$t_1\dots t_n$, - then the pattern \textit{term} is treated -as \ssrC{(_ }$t_1\dots t_n$\ssrC{)}. For each subterm in -the goal having the form $(A\ u_1\dots u_{n'})$ with $n' \geq n$, the -matching algorithm successively tries to find the largest -partial application $(A\ u_1\dots u_{i'})$ convertible to the head -$t_0$ of \textit{term}. For instance the following tactic: -\begin{lstlisting} - set t := (let g y z := y.+1 + z in g) 2. -\end{lstlisting} -transforms the goal -\begin{lstlisting} - (let f x y z := x + y + z in f 1) 2 3 = 6. -\end{lstlisting} -into \ssrC{t 3 = 6} and adds the local definition of \ssrC{t} to the -context. -\end{itemize} - -Moreover: -\begin{itemize} -\item Multiple holes in \textit{term} are treated as independent - placeholders. For instance, the tactic: -\begin{lstlisting} - set t := _ + _. -\end{lstlisting} -transforms the goal \ssrC{x + y = z} into \ssrC{t = z} and pushes -\ssrC{t := x + y : nat} in the context. -\item The type of the subterm matched should fit the type - (possibly casted by some type annotations) of the pattern - \textit{term}. -\item The replacement of the subterm found by the instantiated pattern - should not capture variables, hence the following script: -\begin{lstlisting} - Goal forall x : nat, x + 1 = 0. - set u := _ + 1. -\end{lstlisting} -raises an error message, since \ssrC{x} is bound in the goal. -\item Typeclass inference should fill in any residual hole, but -matching should never assign a value to a global existential variable. - -\end{itemize} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Occurrence selection}\label{sssec:occselect} - -\ssr{} provides a generic syntax for the selection of occurrences by -their position indexes. These \emph{occurrence switches} are shared by -all -\ssr{} tactics which require control on subterm selection like rewriting, -generalization, \dots - -An \emph{occurrence switch} can be: -\begin{itemize} -\item A list \ssrC{\{} {\naturalnumber}$^*$ \ssrC{\}} of occurrences affected by the - tactic. -For instance, the tactic: -\begin{lstlisting} - set x := {1 3}(f 2). -\end{lstlisting} -transforms the goal \ssrC{f 2 + f 8 = f 2 + f 2} into -\ssrC{x + f 8 = f 2 + x}, and adds the abbreviation -\ssrC{x := f 2} in the -context. Notice that some occurrences of a -given term may be hidden to the user, for example because of a -notation. The vernacular \ssrC{$\texttt{\textcolor{dkviolet}{Set }}$ - Printing All} command displays all -these hidden occurrences and should be used to find the correct -coding of the occurrences to be selected\footnote{Unfortunately, -even after a call to the Set Printing All command, some occurrences are -still not displayed to the user, essentially the ones possibly hidden -in the predicate of a dependent match structure.}. For instance, the -following script: -\begin{lstlisting} - Notation "a < b":= (le (S a) b). - Goal forall x y, x < y -> S x < S y. - intros x y; set t := S x. -\end{lstlisting} -generates the goal -\ssrC{t <= y -> t < S y} since \ssrC{x < y} is now a notation for -\ssrC{S x <= y}. -\item A list \ssrC{\{}{\naturalnumber}$^+$\ssrC{\}}. This is equivalent to - \ssrC{\{} {\naturalnumber}$^+$ \ssrC{\}} but the list should start with a number, and - not with an Ltac variable. -\item A list \ssrC{\{}{\naturalnumber}$^*$\ssrC{\}} of occurrences \emph{not} to be - affected by the tactic. For instance, the tactic: -\begin{lstlisting} - set x := {-2}(f 2). -\end{lstlisting} -behaves like -\begin{lstlisting} - set x := {1 3}(f 2). -\end{lstlisting} -on the goal \ssrL-f 2 + f 8 = f 2 + f 2- which has three occurrences of -the the term \ssrC{f 2} -\item In particular, the switch \ssrC{\{+\}} selects \emph{all} the - occurrences. This switch is useful to turn - off the default behavior of a tactic which automatically clears - some assumptions (see section \ref{ssec:discharge} for instance). -\item The switch \ssrC{\{-\}} imposes that \emph{no} occurrences of the - term should be affected by the tactic. The tactic: -\begin{lstlisting} - set x := {-}(f 2). -\end{lstlisting} -leaves the goal unchanged and adds the definition \ssrC{x := f 2} to the -context. This kind of tactic may be used to take advantage of the -power of the matching algorithm in a local definition, instead of -copying large terms by hand. -\end{itemize} - - -It is important to remember that matching \emph{precedes} occurrence -selection, hence the tactic: -\begin{lstlisting} - set a := {2}(_ + _). -\end{lstlisting} -transforms the goal \ssrC{x + y = x + y + z} into \ssrC{x + y = a + z} -and fails on the goal \\ -\ssrC{(x + y) + (z + z) = z + z} with the error message: -\begin{lstlisting} - User error: only 1 < 2 occurrence of (x + y + (z + z)) -\end{lstlisting} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Localization}\label{ssec:loc} - - -It is possible to define an abbreviation for a term appearing in the -context of a goal thanks to the \ssrC{in} tactical. - -A tactic of the form: - -\begin{center} - \ssrC{set x :=} {\term} \ssrC{in} \ssrN[1]{fact}\ssrC{...}\ssrN[n]{fact}. -\end{center} - -introduces a defined constant called \ssrC{x} in the context, and folds -it in the facts \textit{fact$_1 \dots$ fact$_n$} -The body of \ssrC{x} is the first subterm matching \textit{term} in -\textit{fact$_1 \dots$ fact$_n$}. - -A tactic of the form: - -\begin{center} - \ssrC{set x :=} {\term} \ssrC{in} \ssrN[1]{fact}\ssrC{...}\ssrN[n]{fact} \ssrC{*.} -\end{center} - -matches {\term} and then folds \ssrC{x} similarly in -\textit{fact$_1 \dots$ fact$_n$}, but also folds \ssrC{x} in the goal. - -A goal \ssrL-x + t = 4-, whose context contains \ssrC{Hx : x = 3}, is left -unchanged by the tactic: -\begin{lstlisting} - set z := 3 in Hx. -\end{lstlisting} -but the context is extended with the definition \ssrC{z := 3} and \ssrC{Hx} becomes -\ssrC{Hx : x = z}. -On the same goal and context, the tactic: -\begin{lstlisting} - set z := 3 in Hx *. -\end{lstlisting} -will moreover change the goal into \ssrL-x + t = S z-. Indeed, remember -that \ssrC{4} is just a notation for \ssrC{(S 3)}. - -The use of the \ssrC{in} tactical is not limited to the localization of -abbreviations: for a complete description of the \ssrC{in} tactical, see -section \ref{ssec:profstack}. -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Basic tactics}\label{sec:book} - - - -A sizable fraction of proof scripts consists of steps that do not -"prove" anything new, but instead perform menial bookkeeping tasks -such as selecting the names of constants and assumptions or splitting -conjuncts. Although they are logically trivial, bookkeeping steps are -extremely important because they define the structure of the data-flow -of a proof script. This is especially true for reflection-based -proofs, which often involve large numbers of constants and -assumptions. Good bookkeeping consists in always explicitly declaring -(i.e., naming) all new constants and assumptions in the script, and -systematically pruning irrelevant constants and assumptions in the -context. This is essential in the context of an interactive -development environment (IDE), because it facilitates navigating the -proof, allowing to instantly "jump back" to the point at which a -questionable assumption was added, and to find relevant assumptions by -browsing the pruned context. While novice or casual \Coq{} users may -find the automatic name selection feature convenient, the usage of -such a feature severely undermines the readability and maintainability -of proof scripts, much like automatic variable declaration in programming -languages. The \ssr{} tactics are therefore designed to support -precise bookkeeping and to eliminate name generation heuristics. -The bookkeeping features of \ssr{} are implemented as tacticals (or -pseudo-tacticals), shared across most \ssr{} tactics, and thus form -the foundation of the \ssr{} proof language. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Bookkeeping}\label{ssec:profstack} -\idx{move: \dots{}} -\idx{move=> \dots{}} -\idx{move: \dots{} => \dots{}} -\idx{\dots{} in \dots{}} - -During the course of a proof \Coq{} always present the user with -a \emph{sequent} whose general form is -\begin{displaymath}\begin{array}{l} -%\arrayrulecolor{dkviolet} -c_i\ \ssrC{:}\ T_i \\ -\dots\\ -d_j\ \ssrC{:=}\ e_j\ \ssrC{:}\ T_j \\ -\dots\\ -F_k\ \ssrC{:}\ P_k \\ -\dots \\[3pt] -\hline\hline\\[-8pt] -\ssrC{forall}\ \ssrC{(}x_\ell\ \ssrC{:}\ T_\ell\ssrC{)}\ \dots,\\ -\ssrC{let}\ y_m\ \ssrC{:=}\ b_m\ \ssrC{in}\ \dots\ \ssrC{in}\\ -P_n\ \ssrC{->}\ \dots\ \ssrC{->}\ C -\end{array}\end{displaymath} -The \emph{goal} to be proved appears below the double line; above the line is -the \emph{context} of the sequent, a set of declarations of -\emph{constants}~$c_i$, \emph{defined constants}~$d_i$, and -\emph{facts}~$F_k$ that can be used to prove the goal (usually, $T_i, -T_j\;:\;\ssrC{Type}$ and $P_k\;:\;\ssrC{Prop}$). The various kinds of -declarations can come in any order. The top part of the context -consists of declarations produced by the \ssrC{Section} commands -\ssrC{Variable}, \ssrC{Let}, and \ssrC{Hypothesis}. This \emph{section context} -is never affected by the \ssr{} tactics: they only operate on -the lower part --- the \emph{proof context}. -As in the figure above, the goal often decomposes into a series of -(universally) quantified \emph{variables} -$\ssrC{(}x_\ell\;\ssrC{:}\;T_\ell\ssrC{)}$, local \emph{definitions} -$\ssrC{let}\;y_m\:\ssrC{:=}\;b_m\;\ssrC{in}$, and \emph{assumptions} -$P_n\;\ssrC{->}$, and a \emph{conclusion}~$C$ (as in the context, variables, -definitions, and assumptions can appear in any order). The conclusion -is what actually needs to be proved --- the rest of the goal can be -seen as a part of the proof context that happens to be ``below the line''. - -However, although they are logically equivalent, there are fundamental -differences between constants and facts on the one hand, and variables -and assumptions on the others. Constants and facts are -\emph{unordered}, but \emph{named} explicitly in the proof text; -variables and assumptions are \emph{ordered}, but \emph{unnamed}: the -display names of variables may change at any time because of -$\alpha$-conversion. - -Similarly, basic deductive steps such as \ssrC{apply} can only operate on -the goal because the Gallina terms that control their action (e.g., -the type of the lemma used by \ssrC{apply}) only provide unnamed bound -variables.\footnote{Thus scripts that depend on bound variable names, e.g., -via \ssrC{intros} or \ssrC{with}, are inherently fragile.} Since the proof -script can only refer directly to the context, it must constantly -shift declarations from the goal to the context and conversely in -between deductive steps. - -In \ssr{} these moves are performed by two \emph{tacticals} `\ssrC{=>}' -and `\ssrC{:}', so that the bookkeeping required by a deductive step can -be directly associated to that step, and that tactics in an \ssr{} -script correspond to actual logical steps in the proof rather than -merely shuffle facts. Still, some isolated bookkeeping is unavoidable, -such as naming variables and assumptions at the beginning of a proof. -\ssr{} provides a specific \ssrC{move} tactic for this purpose. - -Now \ssrC{move} does essentially nothing: it is mostly a placeholder for -`\ssrC{=>}' and `\ssrC{:}'. The `\ssrC{=>}' tactical moves variables, local -definitions, and assumptions to the context, while the `\ssrC{:}' -tactical moves facts and constants to the goal. For example, the proof -of\footnote{The name \ssrC{subnK} reads as -``right cancellation rule for \ssrC{nat} subtraction''.} -\begin{lstlisting} - Lemma |*subnK*| : forall m n, n <= m -> m - n + n = m. -\end{lstlisting}\noindent -might start with -\begin{lstlisting} - move=> m n le_n_m. -\end{lstlisting} -where \ssrC{move} does nothing, but \ssrL|=> m n le_m_n| changes the -variables and assumption of the goal in the constants \ssrC{m n : nat} -and the fact \ssrL|le_n_m : n <= m|, thus exposing the conclusion\\ - \ssrC{m - n + n = m}. - -The `\ssrC{:}' tactical is the converse of `\ssrC{=>}': it removes facts -and constants from the context by turning them into variables and assumptions. -Thus -\begin{lstlisting} - move: m le_n_m. -\end{lstlisting} -turns back \ssrC{m} and \ssrL|le_m_n| into a variable and an assumption, removing -them from the proof context, and changing the goal to -\begin{lstlisting} - forall m, n <= m -> m - n + n = m. -\end{lstlisting} -which can be proved by induction on \ssrC{n} using \ssrC{elim: n}. - -\noindent -Because they are tacticals, `\ssrC{:}' and `\ssrC{=>}' can be combined, as in -\begin{lstlisting} - move: m le_n_m => p le_n_p. -\end{lstlisting} -simultaneously renames \ssrL|m| and \ssrL|le_m_n| into \ssrL|p| and \ssrL|le_n_p|, -respectively, by first turning them into unnamed variables, then -turning these variables back into constants and facts. - -Furthermore, \ssr{} redefines the basic \Coq{} tactics \ssrC{case}, -\ssrC{elim}, and \ssrC{apply} so that they can take better advantage of -'\ssrC{:}' and `\ssrC{=>}'. In there \ssr{} variants, these tactic operate -on the first variable or constant of the goal and they do not use or -change the proof context. The `\ssrC{:}' tactical is used to operate on -an element in the context. For instance the proof of \ssrC{subnK} could -continue with -\begin{lstlisting} - elim: n. -\end{lstlisting} -instead of \ssrC{elim n}; this has the advantage of -removing \ssrC{n} from the context. Better yet, this \ssrC{elim} can be combined -with previous \ssrC{move} and with the branching version of the \ssrC{=>} tactical -(described in~\ref{ssec:intro}), -to encapsulate the inductive step in a single command: -\begin{lstlisting} - elim: n m le_n_m => [|n IHn] m => [_ | lt_n_m]. -\end{lstlisting} -which breaks down the proof into two subgoals, -\begin{lstlisting} - m - 0 + 0 = m -\end{lstlisting} -given \ssrC{m : nat}, and -\begin{lstlisting} - m - S n + S n = m -\end{lstlisting} -given \ssrC{m n : nat}, \ssrL|lt_n_m : S n <= m|, and -\begin{lstlisting} - IHn : forall m, n <= m -> m - n + n = m. -\end{lstlisting} -The '\ssrC{:}' and `\ssrC{=>}' tacticals can be explained very simply -if one views the goal as a stack of variables and assumptions piled -on a conclusion: -\begin{itemize} -\item {\tac} \ssrC{:} $a$ $b$ $c$ pushes the context constants $a$, $b$, $c$ -as goal variables \emph{before} performing {\tac}. -\item {\tac} \ssrC{=>} $a$ $b$ $c$ pops the top three goal variables as -context constants $a$, $b$, $c$, \emph{after} {\tac} -has been performed. -\end{itemize} -These pushes and pops do not need to balance out as in the examples above, -so -\begin{lstlisting} - move: m le_n_m => p. -\end{lstlisting} -would rename \ssrC{m} into \ssrC{p}, but leave an extra assumption \ssrC{n <= p} -in the goal. - -Basic tactics like \ssrC{apply} and \ssrC{elim} can also be used without the -'\ssrC{:}' tactical: for example we can directly start a proof of \ssrC{subnK} -by induction on the top variable \ssrC{m} with -\begin{lstlisting} - elim=> [|m IHm] n le_n. -\end{lstlisting} - -\noindent -The general form of the localization tactical \ssrC{in} is also best -explained in terms of the goal stack: - -\begin{center} - {\tac} \ssrC{in a H1 H2 *.} -\end{center} - -is basically equivalent to - -\begin{center} - \ssrC{move: a H1 H2;} {\tac} \ssrC{=> a H1 H2.} -\end{center} - -with two differences: the \ssrC{in} tactical will preserve the body of \ssrC{a} if -\ssrC{a} is a defined constant, and if the `\ssrC{*}' is omitted it -will use a temporary abbreviation to hide the statement of the goal -from \ssrC{/*tactic*/}. - -The general form of the \ssrC{in} tactical can be used directly with -the \ssrC{move}, \ssrC{case} and \ssrC{elim} tactics, so that one can write -\begin{lstlisting} - elim: n => [|n IHn] in m le_n_m *. -\end{lstlisting} -instead of -\begin{lstlisting} - elim: n m le_n_m => [|n IHn] m le_n_m. -\end{lstlisting} -This is quite useful for inductive proofs that involve many facts. - -\noindent See section \ref{ssec:gloc} for the general syntax and presentation -of the \ssrC{in} tactical. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{The defective tactics}\label{ssec:basictac} - -In this section we briefly present the three basic tactics performing -context manipulations and the main backward chaining tool. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{move} tactic.}\label{sssec:move} -\idx{move} - -The \ssrC{move} tactic, in its -defective form, behaves like the primitive \ssrC{hnf} \Coq{} tactic. For -example, such a defective: -\begin{lstlisting} - move. -\end{lstlisting} -exposes the first assumption in the goal, i.e. its changes the goal -\ssrC{\~ False} into \ssrC{False -> False}. - -More precisely, the \ssrC{move} tactic inspects the goal and does nothing -(\ssrC{idtac}) if an introduction step is possible, i.e. if the -goal is a product or a \ssrC{let}$\dots$\ssrC{in}, and performs \ssrC{hnf} -otherwise. - -Of course this tactic is most often used in combination with the -bookkeeping tacticals (see section \ref{ssec:intro} and -\ref{ssec:discharge}). These combinations mostly subsume the \ssrC{intros}, -\ssrC{generalize}, \ssrC{revert}, \ssrC{rename}, \ssrC{clear} and -\textcolor{dkblue}{\texttt{pattern}} tactics. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{case} tactic.} -\idx{case: \dots{}} - -The \ssrC{case} tactic performs -\emph{primitive case analysis} on (co)inductive types; specifically, -it destructs the top variable or assumption of the goal, -exposing its constructor(s) and its arguments, as well as setting the value -of its type family indices if it belongs to a type family -(see section \ref{ssec:typefam}). - -The \ssr{} \ssrC{case} tactic has a special behavior on -equalities. -If the top assumption of the goal is an equality, the \ssrC{case} tactic -``destructs'' it as a set of equalities between the constructor -arguments of its left and right hand sides, as per the -tactic \ssrC{injection}. -For example, \ssrC{case} changes the goal -\begin{lstlisting} - (x, y) = (1, 2) -> G. -\end{lstlisting} -into -\begin{lstlisting} - x = 1 -> y = 2 -> G. -\end{lstlisting} - -Note also that the case of \ssr{} performs \ssrC{False} -elimination, even if no branch is generated by this case operation. -Hence the command: -\begin{lstlisting} - case. -\end{lstlisting} -on a goal of the form \ssrC{False -> G} will succeed and prove the goal. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{elim} tactic.} -\idx{elim: \dots{}} - -The \ssrC{elim} tactic performs -inductive elimination on inductive types. -The defective: -\begin{lstlisting} - elim. -\end{lstlisting} -tactic performs inductive elimination on a goal whose top assumption -has an inductive type. For example on goal of the form: -\begin{lstlisting} - forall n : nat, m <= n -\end{lstlisting} - in a context containing \ssrC{m : nat}, the -\begin{lstlisting} - elim. -\end{lstlisting} -tactic produces two goals, -\begin{lstlisting} - m <= 0 -\end{lstlisting} -on one hand and -\begin{lstlisting} - forall n : nat, m <= n -> m <= S n -\end{lstlisting} -on the other hand. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{apply} tactic.}\label{sssec:apply} -\idx{apply: \dots{}} - -The \ssrC{apply} tactic is the main -backward chaining tactic of the proof system. It takes as argument any -\ssrC{/*term*/} and applies it to the goal. -Assumptions in the type of \ssrC{/*term*/} that don't directly match the -goal may generate one or more subgoals. - -In fact the \ssr{} tactic: -\begin{lstlisting} - apply. -\end{lstlisting} -is a synonym for: -\begin{lstlisting} - intro top; first [refine top | refine (top _) | refine (top _ _) | ...]; clear top. -\end{lstlisting} -where \ssrC{top} is fresh name, and the sequence of \ssrC{refine} tactics -tries to catch the appropriate number of wildcards to be inserted. -Note that this use of the \ssrC{refine} tactic implies that the tactic -tries to match the goal up to expansion of -constants and evaluation of subterms. - -\ssr{}'s \ssrC{apply} has a special behaviour on goals containing -existential metavariables of sort \ssrC{Prop}. Consider the -following example: -\begin{lstlisting} -Goal (forall y, 1 < y -> y < 2 -> exists x : { n | n < 3 }, proj1_sig x > 0). -move=> y y_gt1 y_lt2; apply: (ex_intro _ (exist _ y _)). - by apply: gt_trans _ y_lt2. -by move=> y_lt3; apply: lt_trans y_gt1. -\end{lstlisting} -Note that the last \ssrC{_} of the tactic \ssrC{apply: (ex_intro _ (exist _ y _))} -represents a proof that \ssrC{y < 3}. Instead of generating the following -goal -\begin{lstlisting} - 0 < (n:=3) (m:=y) ?54 -\end{lstlisting} -\noindent the system tries to prove \ssrC{y < 3} calling the \ssrC{trivial} -tactic. If it succeeds, let's say because the context contains -\ssrC{H : y < 3}, then the system generates the following goal: -\begin{lstlisting} - 0 < proj1_sig (exist (fun n => n < 3) y H -\end{lstlisting} -\noindent Otherwise the missing proof is considered to be irrelevant, and -is thus discharged generating the following goals: -\begin{lstlisting} - y < 3 - forall H : y < 3, proj1_sig (exist (fun n => n < 3) y H) -\end{lstlisting} -Last, the user can replace the \ssrC{trivial} tactic by defining -an Ltac expression named \ssrC{ssrautoprop}. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Discharge}\label{ssec:discharge} -\idx{\dots{} : \dots{}} - -The general syntax of the discharging tactical `\ssrC{:}' is: -\begin{center} - {\tac} \optional{\ssrN{ident}} \ssrC{:} \ssrN[1]{d-item} $\dots$ \ssrN[n]{d-item} \optional{\ssrN{clear-switch}} -\end{center} -where $n > 0$, and \ssrN{d-item} and \ssrN{clear-switch} are defined as -\begin{longtable}{rcl} -\ssrN{d-item} & ::= & \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} {\term} \\ -\ssrN{clear-switch}& ::=& \ssrC{\{} \ssrN[1]{ident}\, \ldots\, \ssrN[m]{ident} \ssrC{\}} -\end{longtable} -with the following requirements: -\begin{itemize} -\item {\tac} must be one of the four basic tactics described - in~\ref{ssec:basictac}, i.e., \ssrC{move}, \ssrC{case}, \ssrC{elim} or \ssrC{apply}, - the \ssrC{exact} tactic (section \ref{ssec:termin}), - the \ssrC{congr} tactic (section \ref{ssec:congr}), or the application - of the \emph{view} tactical `\ssrC{/}' (section \ref{ssec:assumpinterp}) - to one of \ssrC{move}, \ssrC{case}, or \ssrC{elim}. -\item The optional \ssrN{ident} specifies \emph{equation generation} - (section \ref{ssec:equations}), and is only allowed if {\tac} - is \ssrC{move}, \ssrC{case} or \ssrC{elim}, or the application of the - view tactical `\ssrC{/}' (section \ref{ssec:assumpinterp}) - to \ssrC{case} or \ssrC{elim}. -\item An \ssrN{occ-switch} selects occurrences of {\term}, - as in \ref{sssec:occselect}; \ssrN{occ-switch} is not allowed if - {\tac} is \ssrC{apply} or \ssrC{exact}. -\item A clear item \ssrN{clear-switch} specifies facts and constants to be - deleted from the proof context (as per the \ssrC{clear} tactic). -\end{itemize} -The `\ssrC{:}' tactical first \emph{discharges} all the \ssrN{d-item}s, -right to left, and then performs {\tac}, i.e., for each \ssrN{d-item}, -starting with $\ssrN[n]{d-item}$: -\begin{enumerate} -\item The \ssr{} matching algorithm described in section~\ref{ssec:set} - is used to find occurrences of {\term} in the goal, - after filling any holes `\ssrC{_}' in {\term}; however if {\tac} - is \ssrC{apply} or \ssrC{exact} a different matching algorithm, - described below, is used - \footnote{Also, a slightly different variant may be used for the first - \ssrN{d-item} of \ssrC{case} and \ssrC{elim}; see section~\ref{ssec:typefam}.}. -\item~\label{enum:gen} These occurrences are replaced by a new - variable; in particular, - if {\term} is a fact, this adds an assumption to the goal. -\item~\label{enum:clr} If {\term} is \emph{exactly} the name of a constant - or fact in the proof context, it is deleted from the context, - unless there is an \ssrN{occ-switch}. -\end{enumerate} -Finally, {\tac} is performed just after $\ssrN[1]{d-item}$ has been -generalized --- -that is, between steps \ref{enum:gen} and \ref{enum:clr} for $\ssrN[1]{d-item}$. -The names listed in the final \ssrN{clear-switch} (if it is present) -are cleared first, before $\ssrN[n]{d-item}$ is discharged. - -\noindent -Switches affect the discharging of a \ssrN{d-item} as follows: -\begin{itemize} -\item An \ssrN{occ-switch} restricts generalization (step~\ref{enum:gen}) - to a specific subset of the occurrences of {\term}, as per - \ref{sssec:occselect}, and prevents clearing (step~\ref{enum:clr}). -\item All the names specified by a \ssrN{clear-switch} are deleted from the - context in step~\ref{enum:clr}, possibly in addition to {\term}. -\end{itemize} -For example, the tactic: -\begin{lstlisting} - move: n {2}n (refl_equal n). -\end{lstlisting} -\begin{itemize} -\item first generalizes \ssrC{(refl_equal n : n = n)}; -\item then generalizes the second occurrence of \ssrC{n}. -\item finally generalizes all the other occurrences of \ssrC{n}, - and clears \ssrC{n} from the proof context - (assuming \ssrC{n} is a proof constant). -\end{itemize} -Therefore this tactic changes any goal \ssrC{G} into -\begin{lstlisting} - forall n n0 : nat, n = n0 -> G. -\end{lstlisting} -where the name \ssrC{n0} is picked by the \Coq{} display function, -and assuming \ssrC{n} appeared only in~\ssrC{G}. - -Finally, note that a discharge operation generalizes defined constants -as variables, and not as local definitions. To override this behavior, -prefix the name of the local definition with a \ssrC{@}, -like in \ssrC{move: @n}. - -This is in contrast with the behavior of the \ssrC{in} tactical (see section -\ref{ssec:gloc}), which preserves local definitions by default. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Clear rules} - -The clear step will fail if {\term} is a proof constant that -appears in other facts; in that case either the facts should be -cleared explicitly with a \ssrN{clear-switch}, or the clear step should be -disabled. The latter can be done by adding an \ssrN{occ-switch} or simply by -putting parentheses around {\term}: both -\begin{lstlisting} - move: (n). -\end{lstlisting} -and -\begin{lstlisting} - move: {+}n. -\end{lstlisting} -generalize \ssrC{n} without clearing \ssrC{n} from the proof context. - -The clear step will also fail if the \ssrN{clear-switch} contains a -\ssrN{ident} that is not in the \emph{proof} context. -Note that \ssr{} never clears a section constant. - -If {\tac} is \ssrC{move} or \ssrC{case} and an equation \ssrN{ident} is given, -then clear (step~\ref{enum:clr}) for $\ssrN[1]{d-item}$ is suppressed -(see section \ref{ssec:equations}). - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Matching for \ssrC{apply} and \ssrC{exact}}\label{sss:strongapply} - -The matching algorithm for \ssrN{d-item}s of the \ssr{} \ssrC{apply} and -\ssrC{exact} tactics -exploits the type of $\ssrN[1]{d-item}$ to interpret -wildcards in the other \ssrN{d-item} and to determine which occurrences of -these should be generalized. -Therefore, \ssrN{occur switch}es are not needed for \ssrC{apply} and \ssrC{exact}. - -Indeed, the \ssr{} tactic \ssrC{apply: H x} is equivalent to -\begin{lstlisting} - refine (@H _ ... _ x); clear H x -\end{lstlisting} -with an appropriate number of wildcards between \ssrC{H} and~\ssrC{x}. - -Note that this means that matching for \ssrC{apply} and \ssrC{exact} has -much more context to interpret wildcards; in particular it can accommodate -the `\ssrC{_}' \ssrN{d-item}, which would always be rejected after `\ssrC{move:}'. -For example, the tactic -\begin{lstlisting} - apply: trans_equal (Hfg _) _. -\end{lstlisting} -transforms the goal \ssrC{f a = g b}, whose context contains -\ssrC{(Hfg : forall x, f x = g x)}, into \ssrC{g a = g b}. -This tactic is equivalent (see section \ref{ssec:profstack}) to: -\begin{lstlisting} - refine (trans_equal (Hfg _) _). -\end{lstlisting} -and this is a common idiom for applying transitivity on the left hand side -of an equation. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{abstract} tactic}\label{ssec:abstract} -\idx{abstract: \dots{}} - -The \ssrC{abstract} tactic assigns an abstract constant previously introduced with -the \ssrC{[: name ]} intro pattern (see section~\ref{ssec:intro}, -page~\pageref{ssec:introabstract}). -In a goal like the following: -\begin{lstlisting} - m : nat - abs : <hidden> - n : nat - ============= - m < 5 + n -\end{lstlisting} -The tactic \ssrC{abstract: abs n} first generalizes the goal with respect to -\ssrC{n} (that is not visible to the abstract constant \ssrC{abs}) and then -assigns \ssrC{abs}. The resulting goal is: -\begin{lstlisting} - m : nat - n : nat - ============= - m < 5 + n -\end{lstlisting} -Once this subgoal is closed, all other goals having \ssrC{abs} in their context -see the type assigned to \ssrC{abs}. In this case: -\begin{lstlisting} - m : nat - abs : forall n, m < 5 + n -\end{lstlisting} - -For a more detailed example the user should refer to section~\ref{sssec:have}, -page~\pageref{sec:havetransparent}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Introduction}\label{ssec:intro} -\idx{\dots{} => \dots{}} - -The application of a tactic to a given goal can generate -(quantified) variables, assumptions, or definitions, which the user may want to -\emph{introduce} as new facts, constants or defined constants, respectively. -If the tactic splits the goal into several subgoals, -each of them may require the introduction of different constants and facts. -Furthermore it is very common to immediately decompose -or rewrite with an assumption instead of adding it to the context, -as the goal can often be simplified and even -proved after this. - -All these operations are performed by the introduction tactical -`\ssrC{=>}', whose general syntax is -\begin{center} - {\tac} \ssrC{=>} \ssrN[1]{i-item} $\dots$ \ssrN[n]{i-item} -\end{center} -where {\tac} can be any tactic, $n > 0$ and -\begin{longtable}{rcl} - \ssrN{i-item}& ::=& \ssrN{i-pattern} {\optsep} \ssrN{s-item} {\optsep} \ssrN{clear-switch} {\optsep} \ssrC{/}{\term} \\ - \ssrN{s-item}& ::=& \ssrC{/=} {\optsep} \ssrC{//} {\optsep} \ssrC{//=} \\ - \ssrN{i-pattern}& ::=& \ssrN{ident} {\optsep} \ssrC{_} {\optsep} \ssrC{?} {\optsep} \ssrC{*} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{->} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{<-} {\optsep} \\ - && \ssrC{[} \ssrN[1]{i-item}$^*$ \ssrC{|} $\dots$ \ssrC{|} \ssrN[m]{i-item}$^*$ \ssrC{]} {\optsep} \ssrC{-} {\optsep} \ssrC{[:} \ssrN{ident}$^+$ \ssrC{]} -\end{longtable} - -The `\ssrC{=>}' tactical first executes {\tac}, then the -\ssrN{i-item}s, left to right, i.e., starting from $\ssrN[1]{i-item}$. An -\ssrN{s-item} specifies a simplification operation; a $\ssrN{clear -switch}$ specifies context pruning as in~\ref{ssec:discharge}. The -\ssrN{i-pattern}s can be seen as a variant of \emph{intro patterns}~\ref{intros-pattern}: -each performs an introduction operation, i.e., pops some variables or -assumptions from the goal. - -An \ssrN{s-item} can simplify the set of subgoals or the subgoal themselves: -\begin{itemize} -\item \ssrC{//} removes all the ``trivial'' subgoals that can be resolved by - the \ssr{} tactic \ssrC{done} described in~\ref{ssec:termin}, i.e., it - executes \ssrC{try done}. -\item \ssrC{/=} simplifies the goal by performing partial evaluation, as - per the tactic \ssrC{simpl}.\footnote{Except \ssrC{/=} does not - expand the local definitions created by the \ssr{} \ssrC{in} tactical.} -\item \ssrC{//=} combines both kinds of simplification; it is equivalent - to \ssrC{/= //}, i.e., \ssrC{simpl; try done}. -\end{itemize} -When an \ssrN{s-item} bears a \ssrN{clear-switch}, then the \ssrN{clear-switch} is -executed \emph{after} the \ssrN{s-item}, e.g., \ssrL|{IHn}//| will solve -some subgoals, possibly using the fact \ssrL|IHn|, and will erase \ssrL|IHn| -from the context of the remaining subgoals. - -The last entry in the \ssrN{i-item} grammar rule, \ssrC{/}{\term}, -represents a view (see section~\ref{sec:views}). If $\ssrN[k+1]{i-item}$ -is a view \ssrN{i-item}, the view is applied to the assumption in top -position once $\ssrN[1]{i-item} \dots \ssrN[k]{i-item}$ have been performed. - -The view is applied to the top assumption. - -\ssr{} supports the following \ssrN{i-pattern}s: -\begin{itemize} -\item \ssrN{ident} pops the top variable, assumption, or local definition into - a new constant, fact, or defined constant \ssrN{ident}, respectively. - Note that defined constants cannot be introduced when - $\delta$-expansion is required to expose the top variable or assumption. -\item \ssrC{?} pops the top variable into an anonymous constant or fact, - whose name is picked by the tactic interpreter. - \ssr{} only generates names that - cannot appear later in the user script.\footnote{\ssr{} reserves - all identifiers of the form ``\ssrC{_x_}'', which is used for such - generated names.} -\item \ssrC{_} pops the top variable into an anonymous constant that will be - deleted from - the proof context of all the subgoals produced by the \ssrC{=>} tactical. - They should thus never be displayed, except in an error message - if the constant is still actually used in the goal or context after - the last \ssrN{i-item} has been executed (\ssrN{s-item}s can erase goals - or terms where the constant appears). -\item \ssrC{*} pops all the remaining apparent variables/assumptions - as anonymous constants/facts. Unlike \ssrC{?} and \ssrC{move} the \ssrC{*} - \ssrN{i-item} does not expand definitions in the goal to expose - quantifiers, so it may be useful to repeat a \ssrC{move=> *} tactic, - e.g., on the goal -\begin{lstlisting} - forall a b : bool, a <> b -\end{lstlisting} -a first \ssrC{move=> *} adds only \ssrC{_a_ : bool} and \ssrC{_b_ : bool} to -the context; it takes a second \ssrC{move=> *} to add -\ssrC{_Hyp_ : _a_ = _b_}. -\item $[\ssrN{occ-switch}]$\ssrC{->} (resp. $[\ssrN{occ-switch}]$\ssrC{<-}) - pops the top assumption - (which should be a rewritable proposition) into an anonymous fact, - rewrites (resp. rewrites right to left) the goal with this fact - (using the \ssr{} \ssrC{rewrite} tactic described in section~\ref{sec:rw}, - and honoring the optional occurrence selector), - and finally deletes the anonymous fact from the context. -\item\ssrC{[ $\ssrN[1]{i-item}^*$ | $\dots$ | $\ssrN[m]{i-item}^*$ ]}, - when it is the very \emph{first} \ssrN{i-pattern} after ${\tac}\;\ssrC{=>}$ - tactical \emph{and} {\tac} is not a \ssrC{move}, is a \emph{branching} - \ssrN{i-pattern}. It executes - the sequence $\ssrN[i]{i-item}^*$ on the $i^{\rm th}$ - subgoal produced by {\tac}. The execution of {\tac} - should thus generate exactly $m$ - subgoals, unless the \ssrC{[$\dots$]} \ssrN{i-pattern} comes after an initial - \ssrC{//} or \ssrC{//=} \ssrN{s-item} that closes some of the goals produced by - {\tac}, in which case exactly $m$ subgoals should remain after the - \ssrN{s-item}, or we have the trivial branching \ssrN{i-pattern} \ssrC{[]}, - which always does nothing, regardless of the number of remaining subgoals. -\item\ssrC{[ $\ssrN[1]{i-item}^*$ | $\dots$ | $\ssrN[m]{i-item}^*$ ]}, when it is - \emph{not} the first \ssrN{i-pattern} or when {\tac} is a - \ssrC{move}, is a \emph{destructing} \ssrN{i-pattern}. It starts by - destructing the top variable, using the \ssr{} \ssrC{case} tactic - described in~\ref{ssec:basictac}. It then behaves as the - corresponding branching \ssrN{i-pattern}, executing the sequence - $\ssrN[i]{i-item}^*$ in the $i^{\rm th}$ subgoal generated by the case - analysis; unless we have the trivial destructing \ssrN{i-pattern} - \ssrC{[]}, the latter should generate exactly $m$ subgoals, i.e., the - top variable should have an inductive type with exactly $m$ - constructors.\footnote{More precisely, it should have a quantified - inductive type with $a$ assumptions and $m - a$ constructors.} - While it is good style to use the $\ssrN[i]{i-item}^*$ - to pop the variables and assumptions corresponding to each constructor, - this is not enforced by \ssr{}. -\item\ssrC{-} does nothing, but counts as an intro pattern. It can also - be used to force the interpretation of - \ssrC{[ $\ssrN[1]{i-item}^*$ | $\dots$ | $\ssrN[m]{i-item}^*$ ]} - as a case analysis like in \ssrC{move=> -[H1 H2]}. It can also be used - to indicate explicitly the link between a view and a name like in - \ssrC{move=> /eqP-H1}. Last, it can serve as a separator between - views. Section~\ref{ssec:multiview} explains in which respect - the tactic \ssrC{move=> /v1/v2} differs from the tactic - \ssrC{move=> /v1-/v2}. -\item\ssrC{[: $\ssrN{ident}^+$ ]} introduces in the context an abstract constant - for each \ssrN{ident}. Its type has to be fixed later on by using - the \ssrC{abstract} tactic (see page~\pageref{ssec:abstract}). Before then - the type displayed is \ssrC{<hidden>}.\label{ssec:introabstract} -\end{itemize} -Note that \ssr{} does not support the syntax -$\ssrC{(}\ssrN{ipat}\ssrC{,}\dots\ssrC{,}\ssrN{ipat}\ssrC{)}$ for destructing -intro-patterns. - -Clears are deferred until the end of the intro pattern. For -example, given the goal: -\begin{lstlisting} -x, y : nat -================== -0 < x = true -> (0 < x) && (y < 2) = true -\end{lstlisting} -the tactic \ssrC{move=> \{x\} ->} successfully rewrites the goal and -deletes \ssrC{x} and the anonymous equation. The goal is thus turned into: -\begin{lstlisting} -y : nat -================== -true && (y < 2) = true -\end{lstlisting} -If the cleared names are reused in the same intro pattern, a renaming -is performed behind the scenes. - -Facts mentioned in a clear switch must be valid -names in the proof context (excluding the section context). - -The rules for interpreting branching and destructing \ssrN{i-pattern} -are motivated by the fact that it would be pointless to have a branching -pattern if {\tac} is a \ssrC{move}, and in most of the remaining cases -{\tac} is \ssrC{case} or \ssrC{elim}, which implies destruction. -The rules above imply that -\begin{lstlisting} - move=> [a b]. - case=> [a b]. - case=> a b. -\end{lstlisting} -are all equivalent, so which one to use is a matter of style; -\ssrC{move} should be used for casual decomposition, -such as splitting a pair, and \ssrC{case} should be used for actual decompositions, -in particular for type families (see~\ref{ssec:typefam}) -and proof by contradiction. - -The trivial branching \ssrN{i-pattern} can be used to force the branching -interpretation, e.g., -\begin{lstlisting} - case=> [] [a b] c. - move=> [[a b] c]. - case; case=> a b c. -\end{lstlisting} -are all equivalent. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Generation of equations}\label{ssec:equations} -\idx{move eq : \dots{}} - -The generation of named equations option stores the definition of a -new constant as an equation. The tactic: -\begin{lstlisting} - move En: (size l) => n. -\end{lstlisting} -where \ssrC{l} is a list, replaces \ssrC{size l} by \ssrC{n} in the goal and -adds the fact \ssrC{En : size l = n} to the context. - This is quite different from: -\begin{lstlisting} - pose n := (size l). -\end{lstlisting} -which generates a definition \ssrC{n := (size l)}. It is not possible to -generalize or -rewrite such a definition; on the other hand, it is automatically -expanded during -computation, whereas expanding the equation \ssrC{En} requires explicit -rewriting. - -The use of this equation name generation option with a \ssrC{case} or an -\ssrC{elim} tactic changes the status of the first \iitem{}, in order to -deal with the possible parameters of the constants introduced. - -On the -goal \ssrC{a <> b} where \ssrC{a, b} are natural numbers, the tactic: -\begin{lstlisting} - case E : a => [|n]. -\end{lstlisting} -generates two subgoals. The equation \ssrC{E : a = 0} (resp. \ssrC{E : a = - S n}, and the constant \ssrC{n : nat}) has been added to -the context of the goal \ssrC{0 <> b} (resp. \ssrC{S n <> b}). - -If the user does not provide a branching \iitem{} as first \iitem{}, -or if the \iitem{} does not provide enough names for the arguments of -a constructor, -then the constants generated are introduced under fresh \ssr{} names. -For instance, on the goal \ssrC{a <> b}, the tactic: -\begin{lstlisting} - case E : a => H. -\end{lstlisting} -also generates two subgoals, both requiring a proof of \ssrC{False}. - The hypotheses \ssrC{E : a = 0} and -\ssrC{H : 0 = b} (resp. \ssrC{E : a = S _n_} and -\ssrC{H : S _n_ = b}) have been added to the context of the first -subgoal (resp. the second subgoal). - -Combining the generation of named equations mechanism with the -\ssrC{case} tactic strengthens the power of a case analysis. On the other -hand, when combined with the \ssrC{elim} tactic, this feature is mostly -useful for -debug purposes, to trace the values of decomposed parameters and -pinpoint failing branches. - -% This feature is also useful -% to analyse and debug generate-and-test style scripts that prove program -% properties by generating a large set of input patterns and uniformly -% solving the corresponding subgoals by computation and rewriting, e.g, - -% \begin{lstlisting} -% case: et => [|e' et]; first by case: s. -% case: e => //; case: b; case: w. -% \end{lstlisting} -% If the above sequence fails, then it's easy enough to replace the line -% above with -% \begin{lstlisting} -% case: et => [|e' et]. -% case Ds: s; case De: e => //; case Db: b; case Dw: w=> [|s' w'] //=. -% \end{lstlisting} -% Then the first subgoal that appears will be the failing one, and the -% equations \ssrC{Ds}, \ssrC{De}, \ssrC{Db} -% and \ssrC{Dw} will pinpoint its branch. When the constructors of -% the decomposed type have arguments (like \ssrC{w : (seq nat)} -% above) these need to be -% introduced in order to generate the equation, so there should -% always be an explicit \iitem{} (\ssrC{\[|s' w'\]} above) that -% assigns names to these arguments. If this \iitem{} -% is omitted the arguments are introduced with default -% name; this -% feature should be -% avoided except for quick debugging runs (it has some uses in complex tactic -% sequences, however). - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Type families}\label{ssec:typefam} -\idx{case: \dots{} / \dots{}} - -When the top assumption of a goal has an inductive type, two -specific operations are possible: the case analysis performed by the -\ssrC{case} tactic, and the application of an induction principle, -performed by the \ssrC{elim} tactic. When this top assumption has an -inductive type, which is moreover an instance of a type family, \Coq{} -may need help from the user to specify which occurrences of the parameters -of the type should be substituted. - -A specific \ssrC{/} switch indicates the type family parameters of the -type of a \ditem{} immediately following this \ssrC{/} switch, using the -syntax: - -\begin{center} - \ssrC{[} \ssrC{case} {\optsep} \ssrC{elim} \ssrC{]:} \ssrN{d-item}$^+$ \ssrC{/} \ssrN{d-item}$^*$ -\end{center} - -The \ssrN{d-item}s on the right side of the \ssrC{/} switch are discharged -as described in section \ref{ssec:discharge}. The case analysis or -elimination will be done on the type of the top assumption after these -discharge operations. - -Every \ssrN{d-item} preceding the \ssrC{/} is interpreted as arguments of this -type, which should be an instance of an inductive type family. These terms are -not actually generalized, but rather selected for substitution. Occurrence -switches can be used to restrict the substitution. If a {\term} is left -completely implicit (e.g. writing just $\ssrC{\_}$), then a pattern is inferred -looking at the type of the top assumption. This allows for the compact syntax -\ssrC{case: \{2\}\_ / eqP}, were \ssrC{\_} is interpreted as \ssrC{(\_ == \_)}. Moreover -if the \ssrN{d-item}s list is too short, it is padded with an initial -sequence of $\ssrC{\_}$ of the right length. - -Here is a small example on lists. We define first a function which -adds an element at the end of a given list. -\begin{lstlisting} - Require Import List. - - Section LastCases. - Variable A : Type. - - Fixpoint |*add_last*|(a : A)(l : list A): list A := - match l with - |nil => a :: nil - |hd :: tl => hd :: (add_last a tl) - end. -\end{lstlisting} -Then we define an inductive predicate for -case analysis on lists according to their last element: -\begin{lstlisting} - Inductive |*last_spec*| : list A -> Type := - | LastSeq0 : last_spec nil - | LastAdd s x : last_spec (add_last x s). - - Theorem |*lastP*| : forall l : list A, last_spec l. -\end{lstlisting} -Applied to the goal: -\begin{lstlisting} - Goal forall l : list A, (length l) * 2 = length (app l l). -\end{lstlisting} -the command: -\begin{lstlisting} - move=> l; case: (lastP l). -\end{lstlisting} -generates two subgoals: -\begin{lstlisting} - length nil * 2 = length (nil ++ nil) -\end{lstlisting} -and -\begin{lstlisting} - forall (s : list A) (x : A), - length (add_last x s) * 2 = length (add_last x s ++ add_last x s) -\end{lstlisting} -both having \ssrC{l : list A} in their context. - -Applied to the same goal, the command: -\begin{lstlisting} - move=> l; case: l / (lastP l). -\end{lstlisting} -generates the same subgoals but \ssrC{l} has been cleared from both -contexts. - -Again applied to the same goal, the command: -\begin{lstlisting} - move=> l; case: {1 3}l / (lastP l). -\end{lstlisting} -generates the subgoals \ssrL-length l * 2 = length (nil ++ l)- and -\ssrL-forall (s : list A) (x : A), length l * 2 = length (add_last x s++l)- -where the selected occurrences on the left of the \ssrC{/} switch have -been substituted with \ssrC{l} instead of being affected by the case -analysis. - -The equation name generation feature combined with a type family \ssrC{/} - switch generates an equation for the \emph{first} dependent d-item -specified by the user. -Again starting with the above goal, the command: -\begin{lstlisting} - move=> l; case E: {1 3}l / (lastP l)=>[|s x]. -\end{lstlisting} -adds \ssrC{E : l = nil} and \ssrC{E : l = add_last x s}, -respectively, to the context of the two subgoals it generates. - -There must be at least one \emph{d-item} to the left of the \ssrC{/} -switch; this prevents any -confusion with the view feature. However, the \ditem{}s to the right of -the \ssrC{/} are optional, and if they are omitted the first assumption -provides the instance of the type family. - -The equation always refers to the first \emph{d-item} in the actual -tactic call, before any padding with initial $\ssrC{\_}$s. Thus, if an -inductive type has two family parameters, it is possible to have -\ssr{} generate an equation for the second one by omitting the pattern -for the first; note however that this will fail if the type of the -second parameter depends on the value of the first parameter. -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Control flow} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Indentation and bullets}\label{ssec:indent} - -A linear development of \Coq{} scripts gives little information on -the structure of the proof. In addition, replaying a proof after some -changes in the statement to be proved will usually not display information to -distinguish between the various branches of case analysis for instance. - -To help the user in this organization of the proof script at -development time, \ssr{} provides some bullets to highlight the -structure of branching proofs. The available bullets are \ssrC{-}, -\ssrC{+} and \ssrC{*}. Combined with tabulation, this lets us highlight four -nested levels of branching; the most we have ever -needed is three. Indeed, the use of ``simpl and closing'' switches, of -terminators (see above section \ref{ssec:termin}) and selectors (see - section \ref{ssec:select}) is powerful enough -to avoid most of the time more than two levels of indentation. - -Here is a fragment of such a structured script: - -\begin{lstlisting} -case E1: (abezoutn _ _) => [[| k1] [| k2]]. -- rewrite !muln0 !gexpn0 mulg1 => H1. - move/eqP: (sym_equal F0); rewrite -H1 orderg1 eqn_mul1. - by case/andP; move/eqP. -- rewrite muln0 gexpn0 mulg1 => H1. - have F1: t %| t * S k2.+1 - 1. - apply: (@dvdn_trans (orderg x)); first by rewrite F0; exact: dvdn_mull. - rewrite orderg_dvd; apply/eqP; apply: (mulgI x). - rewrite -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //. - by move: P1; case t. - rewrite dvdn_subr in F1; last by exact: dvdn_mulr. - + rewrite H1 F0 -{2}(muln1 (p ^ l)); congr (_ * _). - by apply/eqP; rewrite -dvdn1. - + by move: P1; case: (t) => [| [| s1]]. -- rewrite muln0 gexpn0 mul1g => H1. -... -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Terminators}\label{ssec:termin} -\idx{by \dots{}} - -To further structure scripts, \ssr{} -supplies \emph{terminating} tacticals to explicitly close off tactics. -When replaying scripts, we then have the nice property that -an error immediately occurs when a closed tactic fails to prove its -subgoal. - -It is hence recommended practice that the proof of any subgoal should -end with a tactic which \emph{fails if it does not solve the current - goal}, like \ssrC{discriminate}, \ssrC{contradiction} or \ssrC{assumption}. - -In fact, \ssr{} provides a generic tactical which turns any tactic into -a closing one (similar to \ssrC{now}). Its general syntax is: - -\begin{center} - \ssrC{by} {\tac}\ssrC{.} -\end{center} - -The Ltac expression: - -\begin{center} - \ssrC{by [}\ssrN[1]{tactic} \ssrC{| [}\ssrN[2]{tactic} \ssrC{| ...].} -\end{center} - -is equivalent to: - -\begin{center} - \ssrC{[by} \ssrN[1]{tactic} \ssrC{| by} \ssrN[2]{tactic} \ssrC{| ...].} -\end{center} - -and this form should be preferred to the former. - -In the script provided as example in section \ref{ssec:indent}, the -paragraph corresponding to each sub-case ends with a tactic line prefixed -with a \ssrC{by}, like in: - -\begin{center} - \ssrC{by apply/eqP; rewrite -dvdn1.} -\end{center} - - -The \ssrC{by} tactical is implemented using the user-defined, -and extensible \ssrC{done} tactic. This \ssrC{done} tactic tries to solve -the current goal by some trivial means and fails if it doesn't succeed. -Indeed, the tactic expression: - -\begin{center} - \ssrC{by} {\tac}\ssrC{.} -\end{center} - -is equivalent to: - -\begin{center} - {\tac}\ssrC{; done.} -\end{center} - -Conversely, the tactic - -\begin{center} - \ssrC{by [ ].} -\end{center} - -is equivalent to: - -\begin{center} - \ssrC{done.} -\end{center} - -The default implementation of the \ssrC{done} tactic, in the {\tt - ssreflect.v} file, is: - -\begin{lstlisting} -Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] - | discriminate | contradiction | split] - | case not_locked_false_eq_true; assumption - | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -\end{lstlisting} - -The lemma \ssrC{|*not_locked_false_eq_true*|} is needed to discriminate -\emph{locked} boolean predicates (see section \ref{ssec:lock}). -The iterator tactical \ssrC{do} is presented in section -\ref{ssec:iter}. -This tactic can be customized by the user, for instance to include an -\ssrC{auto} tactic. - -A natural and common way of closing a goal is to apply a lemma which -is the \ssrC{exact} one needed for the goal to be solved. The defective -form of the tactic: -\begin{lstlisting} - exact. -\end{lstlisting} -is equivalent to: -\begin{lstlisting} - do [done | by move=> top; apply top]. -\end{lstlisting} -where \ssrC{top} is a fresh name affected to the top assumption of the goal. -This applied form is supported by the \ssrC{:} discharge tactical, and -the tactic: -\begin{lstlisting} - exact: MyLemma. -\end{lstlisting} -is equivalent to: -\begin{lstlisting} - by apply: MyLemma. -\end{lstlisting} -(see section \ref{sss:strongapply} for the documentation of the \ssrC{apply:} -combination). - -\textit{Warning} The list of tactics, possibly chained by -semi-columns, that follows a \ssrC{by} keyword is considered as a -parenthesized block -applied to the current goal. Hence for example if the tactic: -\begin{lstlisting} - by rewrite my_lemma1. -\end{lstlisting} -succeeds, then the tactic: -\begin{lstlisting} - by rewrite my_lemma1; apply my_lemma2. -\end{lstlisting} -usually fails since it is equivalent to: -\begin{lstlisting} - by (rewrite my_lemma1; apply my_lemma2). -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Selectors}\label{ssec:select} -\idx{last \dots{} first} -\idx{first \dots{} last} - -When composing tactics, the two tacticals \ssrC{first} and -\ssrC{last} let the user restrict the application of a tactic to only one -of the subgoals generated by the previous tactic. This -covers the frequent cases where a tactic generates two subgoals one of -which can be easily disposed of. - -This is an other powerful way of linearization of scripts, since it -happens very often that a trivial subgoal can be solved in a less than -one line tactic. For instance, the tactic: - -\begin{center} - \ssrN[1]{tactic}\ssrC{; last by} \ssrN[2]{tactic}\ssrC{.} -\end{center} - -tries to solve the last subgoal generated by \ssrN[1]{tactic} using the -\ssrN[2]{tactic}, and fails if it does not succeeds. Its analogous - -\begin{center} - \ssrN[1]{tactic}\ssrC{; first by} \ssrN[2]{tactic}. -\end{center} - -tries to solve the first subgoal generated by \ssrN[1]{tactic} using the -tactic \ssrN[2]{tactic}, and fails if it does not succeeds. - - -\ssr{} also offers an extension of this facility, by supplying -tactics to \emph{permute} the subgoals generated by a tactic. -The tactic: - -\begin{center} - {\tac}\ssrC{; last first.} -\end{center} - -inverts the order of the subgoals generated by {\tac}. It is -equivalent to: - -\begin{center} - {\tac}\ssrC{; first last.} -\end{center} - - -More generally, the tactic: - -\begin{center} - {\tac}\ssrC{; last }${\naturalnumber}$ \ssrC{first.} -\end{center} - -where ${\naturalnumber}$ is -a \Coq{} numeral, or and Ltac variable denoting -a \Coq{} numeral, having the value $k$. It -rotates the $n$ subgoals $G_1, -\dots, G_n$ generated by {\tac}. The first subgoal becomes -$G_{n + 1 - k}$ and the circular order of subgoals remains unchanged. - -Conversely, the tactic: - - {\tac}\ssrC{; first }${\naturalnumber}$ \ssrC{last.} - -rotates the $n$ subgoals $G_1, -\dots, G_n$ generated by \ssrC{tactic} in order that the first subgoal -becomes $G_{k}$. - -Finally, the tactics \ssrC{last} and \ssrC{first} combine with the -branching syntax of Ltac: -if the tactic $\ssrN[0]{tactic}$ generates $n$ -subgoals on a given goal, then the tactic - - $tactic_0$\ssrC{; last }${\naturalnumber}$ \ssrC{[}$tactic_1$\ssrC{|}$\dots$\ssrC{|}$tactic_m$\ssrC{] || }$tactic_{m+1}$\ssrC{.} - -where ${\naturalnumber}$ denotes the integer $k$ as above, applies $tactic_1$ to the -$n -k + 1$-th goal, $\dots tactic_m$ to the $n -k + 2 - m$-th -goal and $tactic_{m+1}$ to the others. - -For instance, the script: -\begin{lstlisting} - Inductive test : nat -> Prop := - C1 : forall n, test n | C2 : forall n, test n | - C3 : forall n, test n | C4 : forall n, test n. - - Goal forall n, test n -> True. - move=> n t; case: t; last 2 [move=> k| move=> l]; idtac. -\end{lstlisting} - -creates a goal with four subgoals, the first and the last being -\ssrC{nat -> True}, the second and the third being \ssrC{True} with -respectively \ssrC{k : nat} and \ssrC{l : nat} in their context. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Iteration}\label{ssec:iter} -\idx{do \dots{} [ \dots{} ]} - -\ssr{} offers an accurate control on the repetition of -tactics, thanks to the \ssrC{do} tactical, whose general syntax is: - -\begin{center} - \ssrC{do} \optional{\ssrN{mult}} \ssrC{[} \ssrN[1]{tactic} \ssrC{|} $\dots$ \ssrC{|} \ssrN[n]{tactic} \ssrC{]} -\end{center} -where \ssrN{mult} is a \emph{multiplier}. - -Brackets can only be omitted if a single tactic is given \emph{and} a -multiplier is present. - -A tactic of the form: - -\begin{center} - \ssrC{do [} \tac$_1$ \ssrC{|} $\dots$ \ssrC{|} \tac$_n$\ssrC{].} -\end{center} - -is equivalent to the standard Ltac expression: - -\begin{center} - \ssrC{first [} \tac$_1$ \ssrC{|} $\dots$ \ssrC{|} \tac$_n$\ssrC{].} -\end{center} - - -The optional multiplier \ssrN{mult} specifies how many times -the action of {\tac} should be repeated on the current subgoal. - -There are four kinds of multipliers: - \begin{itemize} - \item \ssrC{n!}: the step {\tac} is repeated exactly $n$ times - (where $n$ is a positive integer argument). - \item \ssrC{!}: the step {\tac} is repeated as many times as possible, - and done at least once. - \item \ssrC{?}: the step {\tac} is repeated as many times as possible, - optionally. - \item \ssrC{n?}: the step {\tac} is repeated up to $n$ times, - optionally. - \end{itemize} - -For instance, the tactic: - -\begin{center} - {\tac} \ssrL+; do 1?rewrite mult_comm.+ -\end{center} - -rewrites at most one time the lemma \ssrC{mult_com} in all the subgoals -generated by {\tac} , whereas the tactic: - -\begin{center} - {\tac} \ssrL+; do 2!rewrite mult_comm.+ -\end{center} - -rewrites exactly two times the lemma \ssrC{mult_com} in all the subgoals -generated by {\tac}, and fails if this rewrite is not possible -in some subgoal. - -Note that the combination of multipliers and \ssrC{rewrite} is so often -used that multipliers are in fact integrated to the syntax of the \ssr{} -\ssrC{rewrite} tactic, see section \ref{sec:rw}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Localization}\label{ssec:gloc} -\idx{\dots{} in \dots{}} - -In sections \ref{ssec:loc} and \ref{ssec:profstack}, we have already -presented the \emph{localization} tactical \ssrC{in}, whose general -syntax is: -\begin{center} - {\tac} \ssrC{in} \ssrN{ident}$^+$ \optional{\ssrC{*}} -\end{center} - -where \ssrN{ident}$^+$ is a non empty list of fact -names in the context. On the left side of \ssrC{in}, {\tac} can be -\ssrC{move}, \ssrC{case}, \ssrC{elim}, \ssrC{rewrite}, \ssrC{set}, - or any tactic formed with the general iteration tactical \ssrC{do} (see - section \ref{ssec:iter}). - -The operation described by {\tac} is performed in the facts -listed in \ssrN{ident}$^+$ and in the goal if a \ssrC{*} ends -the list. - -The \ssrC{in} tactical successively: -\begin{itemize} -\item generalizes the selected hypotheses, possibly ``protecting'' the - goal if \ssrC{*} is not present, -\item performs {\tac}, on the obtained goal, -\item reintroduces the generalized facts, under the same names. -\end{itemize} - -This defective form of the \ssrC{do} tactical is useful to avoid clashes -between standard Ltac \ssrC{in} and the \ssr{} tactical \ssrC{in}. -For example, in the following script: -\begin{lstlisting} - Ltac |*mytac*| H := rewrite H. - - Goal forall x y, x = y -> y = 3 -> x + y = 6. - move=> x y H1 H2. - do [mytac H2] in H1 *. -\end{lstlisting} -the last tactic rewrites the hypothesis \ssrC{H2 : y = 3} both in -\ssrC{H1 : x = y} and in the goal \ssrC{x + y = 6}. - -By default \ssrC{in} keeps the body of local definitions. To erase -the body of a local definition during the generalization phase, -the name of the local definition must be written between parentheses, -like in \ssrC{rewrite H in H1 (def_n) $\;\;$H2}. - -From \ssr{} 1.5 the grammar for the \ssrC{in} tactical has been extended -to the following one: - -\begin{center} - {\tac} \ssrC{in} \optional{ - \ssrN{clear-switch} {\optsep} - \optional{\ssrC{@}}\ssrN{ident} {\optsep} - \ssrC{(}\ssrN{ident}\ssrC{)} {\optsep} - \ssrC{(}\optional{\ssrC{@}}\ssrN{ident} \ssrC{:=} \ssrN{c-pattern}\ssrC{)} - }$^+$ \optional{\ssrC{*}} -\end{center} - -In its simplest form the last option lets one rename hypotheses that can't be -cleared (like section variables). For example \ssrC{(y := x)} generalizes -over \ssrC{x} and reintroduces the generalized -variable under the name \ssrC{y} (and does not clear \ssrC{x}).\\ -For a more precise description the $\ssrC{(}[\ssrC{@}]\ssrN{ident}\ \ssrC{:=}\ \ssrN{c-pattern}\ssrC{)}$ -item refer to the ``Advanced generalization'' paragraph at page~\pageref{par:advancedgen}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Structure}\label{ssec:struct} - -Forward reasoning structures the script by explicitly specifying some -assumptions to be added to the proof context. It is closely associated -with the declarative style of proof, since an extensive use of these -highlighted statements -make the script closer to a (very detailed) text book proof. - -Forward chaining tactics allow to state an intermediate lemma and start a -piece of script dedicated to the proof of this statement. The use of -closing tactics (see section \ref{ssec:termin}) and of -indentation makes syntactically explicit the portion of the script -building the proof of the intermediate statement. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{have} tactic.} -\label{sssec:have} -\idx{have: \dots{}} -\idx{have: \dots{} := \dots{}} - -The main \ssr{} forward reasoning tactic is the \ssrC{have} tactic. It -can be use in two modes: one starts a new (sub)proof for an -intermediate result in the main proof, and the other -provides explicitly a proof term for this intermediate step. - -In the first mode, the syntax of \ssrC{have} in its defective form is: - - \ssrC{have: }{\term}\ssrC{.} - -This tactic supports open syntax for {\term}. -Applied to a goal \ssrC{G}, it generates a first subgoal requiring a -proof of {\term} in the context of \ssrC{G}. The second generated -subgoal is of the form {\term} \ssrC{-> G}, where {\term} becomes -the new top assumption, instead of being introduced with a fresh -name. At the proof-term level, the \ssrC{have} tactic creates a $\beta$ -redex, and introduces the lemma under a fresh name, automatically -chosen. - - -Like in the case of the \ssrC{pose} tactic (see section \ref{ssec:pose}), -the types of the holes are abstracted in {\term}. -For instance, the tactic: -\begin{lstlisting} - have: _ * 0 = 0. -\end{lstlisting} -is equivalent to: -\begin{lstlisting} - have: forall n : nat, n * 0 = 0. -\end{lstlisting} -The \ssrC{have} tactic also enjoys the same abstraction mechanism as the -\ssrC{pose} tactic for the non-inferred implicit arguments. For instance, -the tactic: -\begin{lstlisting} - have: forall x y, (x, y) = (x, y + 0). -\end{lstlisting} -opens a new subgoal to prove that: - -\noindent\ssrC{forall (T : Type) (x : T) (y : nat), (x, y) = (x, y + 0)} - - -The behavior of the defective \ssrC{have} tactic makes it possible to -generalize it in the -following general construction: -\begin{center} - \ssrC{have} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} - \optional{\ssrN{s-item} {\optsep} \ssrN{binder}$^+$} - \optional{\ssrC{:} \ssrN[1]{term}} - \optional{\ssrC{:=} \ssrN[2]{term} {\optsep} \ssrC{by} {\tac}} -\end{center} - -Open syntax is supported for $\ssrN[1]{term}$ and $\ssrN[2]{term}$. For the -description of -\iitem{}s and clear switches see section \ref{ssec:intro}. -The first mode of the \ssrC{have} tactic, which opens a sub-proof for an -intermediate result, uses tactics of the form: - -\begin{center} - \ssrC{have} \ssrN{clear-switch} \ssrN{i-item} \ssrC{:} {\term} \ssrC{by} {\tac}. -\end{center} - -which behave like:\\ - -\begin{center} - \ssrC{have:} {\term} \ssrC{; first by } {\tac}. -\end{center} -\begin{center} - \ssrC{ move=>} \ssrN{clear-switch} \ssrN{i-item}. -\end{center} - - -Note that the \ssrN{clear-switch} \emph{precedes} the -\ssrN{i-item}, which allows to reuse a name of the context, possibly used -by the proof of the assumption, to introduce the new assumption -itself. - -The \ssrC{by} feature is especially convenient when the proof script of the -statement is very short, basically when it fits in one line like in: -\begin{lstlisting} - have H : forall x y, x + y = y + x by move=> x y; rewrite addnC. -\end{lstlisting} - -The possibility of using \iitem{}s supplies a very concise -syntax for the further use of the intermediate step. For instance, -\begin{lstlisting} - have -> : forall x, x * a = a. -\end{lstlisting} -on a goal \ssrC{G}, opens a new subgoal asking for a proof of -\ssrC{forall x, x * a = a}, and a second subgoal in which the lemma - \ssrC{forall x, x * a = a} has been rewritten in the goal \ssrC{G}. Note - that in this last subgoal, the intermediate result does not appear in - the context. -Note that, thanks to the deferred execution of clears, the following -idiom is supported (assuming \ssrC{x} occurs in the goal only): -\begin{lstlisting} - have {x} -> : x = y -\end{lstlisting} - -An other frequent use of the intro patterns combined with \ssrC{have} is the -destruction of existential assumptions like in the tactic: -\begin{lstlisting} - have [x Px]: exists x : nat, x > 0. -\end{lstlisting} -which opens a new subgoal asking for a proof of \ssrC{exists x : nat, x > - 0} and a second subgoal in which the witness is introduced under -the name \ssrC{x : nat}, and its property under the name \ssrC{Px : x > 0}. - -An alternative use of the \ssrC{have} tactic is to provide the explicit proof -term for the intermediate lemma, using tactics of the form: - -\begin{center} - \ssrC{have} \optional{\ssrN{ident}} \ssrC{:=} {\term}. -\end{center} - -This tactic creates a new assumption of type the type of -{\term}. If the -optional \ssrN{ident} is present, this assumption is introduced under -the name \ssrN{ident}. Note that the body of the constant is lost for -the user. - -Again, non inferred implicit arguments and explicit holes are abstracted. For -instance, the tactic: -\begin{lstlisting} - have H := forall x, (x, x) = (x, x). -\end{lstlisting} -adds to the context \ssrC{H : Type -> Prop}. This is a schematic example but -the feature is specially useful when the proof term to give involves -for instance a lemma with some hidden implicit arguments. - -After the \ssrN{i-pattern}, a list of binders is allowed. -For example, if \ssrC{Pos_to_P} is a lemma that proves that -\ssrC{P} holds for any positive, the following command: -\begin{lstlisting} - have H x (y : nat) : 2 * x + y = x + x + y by auto. -\end{lstlisting} -will put in the context \ssrC{H : forall x, 2 * x = x + x}. A proof term -provided after \ssrC{:=} can mention these bound variables (that are -automatically introduced with the given names). -Since the \ssrN{i-pattern} can be omitted, to avoid ambiguity, bound variables -can be surrounded with parentheses even if no type is specified: -\begin{lstlisting} - have (x) : 2 * x = x + x by auto. -\end{lstlisting} - -The \ssrN{i-item}s and \ssrN{s-item} can be used to interpret the -asserted hypothesis with views (see section~\ref{sec:views}) or -simplify the resulting goals. - -The \ssrC{have} tactic also supports a \ssrC{suff} modifier which allows for -asserting that a given statement implies the current goal without -copying the goal itself. For example, given a goal \ssrC{G} the tactic -\ssrC{have suff H : P} results in the following two goals: -\begin{lstlisting} - |- P -> G - H : P -> G |- G -\end{lstlisting} -Note that \ssrC{H} is introduced in the second goal. The \ssrC{suff} -modifier is not compatible with the presence of a list of binders. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Generating \ssrC{let in} context entries with \ssrC{have}} -\label{sec:havetransparent} - -Since \ssr{} 1.5 the \ssrC{have} tactic supports a ``transparent'' modifier to -generate \ssrC{let in} context entries: the \ssrC{@} symbol in front of the context -entry name. For example: - -\begin{lstlisting} -have @i : 'I_n by apply: (Sub m); auto. -\end{lstlisting} -generates the following two context entry: -\begin{lstlisting} -i := Sub m proof_produced_by_auto : 'I_n -\end{lstlisting} - -Note that the sub-term produced by \ssrC{auto} is in general huge and -uninteresting, and hence one may want to hide it. - -For this purpose the \ssrC{[: name ]} intro pattern and the tactic -\ssrC{abstract} (see page~\pageref{ssec:abstract}) are provided. -Example: -\begin{lstlisting} -have [:blurb] @i : 'I_n by apply: (Sub m); abstract: blurb; auto. -\end{lstlisting} -generates the following two context entries: -\begin{lstlisting} -blurb : (m < n) (*1*) -i := Sub m blurb : 'I_n -\end{lstlisting} -The type of \ssrC{blurb} can be cleaned up by its annotations by just simplifying -it. The annotations are there for technical reasons only. - -When intro patterns for abstract constants are used in conjunction -with \ssrC{have} and an explicit term, they must be used as follows: - -\begin{lstlisting} -have [:blurb] @i : 'I_n := Sub m blurb. - by auto. -\end{lstlisting} - -In this case the abstract constant \ssrC{blurb} is assigned by using it -in the term that follows \ssrC{:=} and its corresponding goal is left to -be solved. Goals corresponding to intro patterns for abstract constants -are opened in the order in which the abstract constants are declared (not -in the ``order'' in which they are used in the term). - -Note that abstract constants do respect scopes. Hence, if a variable -is declared after their introduction, it has to be properly generalized (i.e. -explicitly passed to the abstract constant when one makes use of it). -For example any of the following two lines: -\begin{lstlisting} -have [:blurb] @i k : 'I_(n+k) by apply: (Sub m); abstract: blurb k; auto. -have [:blurb] @i k : 'I_(n+k) := apply: Sub m (blurb k); first by auto. -\end{lstlisting} -generates the following context: -\begin{lstlisting} -blurb : (forall k, m < n+k) (*1*) -i := fun k => Sub m (blurb k) : forall k, 'I_(n+k) -\end{lstlisting} - -Last, notice that the use of intro patterns for abstract constants is -orthogonal to the transparent flag \ssrC{@} for \ssrC{have}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{The \ssrC{have} tactic and type classes resolution} -\label{ssec:havetcresolution} - -Since \ssr{} 1.5 the \ssrC{have} tactic behaves as follows with respect to type -classes inference. - -\begin{itemize} -\item \ssrC{have foo : ty.} - Full inference for \ssrC{ty}. - The first subgoal demands a proof of such instantiated statement. -\item \ssrC{have foo : ty := .} - No inference for \ssrC{ty}. Unresolved instances are quantified in - \ssrC{ty}. The first subgoal demands a proof of such quantified - statement. Note that no proof term follows \ssrC{:=}, hence two - subgoals are generated. -\item \ssrC{have foo : ty := t.} - No inference for \ssrC{ty} and \ssrC{t}. -\item \ssrC{have foo := t.} - No inference for \ssrC{t}. Unresolved instances are quantified in the - (inferred) type of \ssrC{t} and abstracted in \ssrC{t}. -\end{itemize} - -The behavior of \ssr{} 1.4 and below (never resolve type classes) -can be restored with the option \ssrC{Set SsrHave NoTCResolution}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Variants: the \ssrC{suff} and \ssrC{wlog} tactics.} -\label{ssec:wlog} -\idx{suff: \dots{}} -\idx{suffices: \dots{}} -\idx{wlog: \dots{} / \dots{}} -\idx{without loss: \dots{} / \dots{}} - -As it is often the case in mathematical textbooks, forward -reasoning may be used in slightly different variants. -One of these variants is to show that the intermediate step $L$ -easily implies the initial goal $G$. By easily we mean here that -the proof of $L \Rightarrow G$ is shorter than the one of $L$ -itself. This kind of reasoning step usually starts with: -``It suffices to show that \dots''. - -This is such a frequent way of reasoning that \ssr{} has a variant of the -\ssrC{have} tactic called \ssrC{suffices} (whose abridged name is -\ssrC{suff}). The \ssrC{have} and \ssrC{suff} tactics are equivalent and -have the same syntax but: -\begin{itemize} -\item the order of the generated subgoals is inversed -\item but the optional clear item is still performed in the - \emph{second} branch. This means that the tactic: -\begin{lstlisting} - suff {H} H : forall x : nat, x >= 0. -\end{lstlisting} -fails if the context of the current goal indeed contains an -assumption named \ssrC{H}. -\end{itemize} -The rationale of this clearing policy is to make possible ``trivial'' -refinements of an assumption, without changing its name in the main -branch of the reasoning. - -The \ssrC{have} modifier can follow the \ssrC{suff} tactic. -For example, given a goal \ssrC{G} the tactic -\ssrC{suff have H : P} results in the following two goals: -\begin{lstlisting} - H : P |- G - |- (P -> G) -> G -\end{lstlisting} -Note that, in contrast with \ssrC{have suff}, the name \ssrC{H} has been introduced -in the first goal. - -Another useful construct is reduction, -showing that a particular case is in fact general enough to prove -a general property. This kind of reasoning step usually starts with: -``Without loss of generality, we can suppose that \dots''. -Formally, this corresponds to the proof of a goal \ssrC{G} by introducing -a cut \ssrN{wlog\_statement} \ssrC{-> G}. Hence the user shall provide a -proof for both \ssrC{(}\ssrN{wlog\_statement} \ssrC{-> G) -> G} and -\ssrN{wlog\_statement} \ssrC{-> G}. However, such cuts are usually rather -painful to perform by hand, because the statement -\ssrN{wlog\_statement} is tedious to write by hand, and somtimes even -to read. - -\ssr{} implements this kind of reasoning step through the \ssrC{without loss} -tactic, whose short name is \ssrC{wlog}. It offers support to describe -the shape of the cut statements, by providing the simplifying -hypothesis and by pointing at the elements of the initial goals which -should be generalized. The general syntax of \ssrC{without loss} is: - -\begin{center} - \ssrC{wlog} \optional{\ssrC{suff}} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-item}} \ssrC{:} \optional{\ssrN[1]{ident} $\dots$ \ssrN[n]{ident}} \ssrC{/} {\term} -\end{center} - -where \ssrN[1]{ident} $\dots$ \ssrN[n]{ident} are identifiers for constants -in the context of the goal. Open syntax is supported for {\term}. - -In its defective form: - -\begin{center} - \ssrC{wlog: /} {\term}. -\end{center} - -on a goal \ssrC{G}, it creates two subgoals: a first one to prove the formula -\ssrC{(}{\term} \ssrC{-> G) -> G} and a second one to prove the formula -{\term} \ssrC{-> G}. - -:browse confirm wa -If the optional list \ssrN[1]{ident} $\dots$ \ssrN[n]{ident} is present on the left -side of \ssrC{/}, these constants are generalized in the premise -\ssrC{(}{\term} \ssrC{-> G)} of the first subgoal. By default the body of -local definitions is erased. This behavior can be inhibited -prefixing the name of the local definition with the \ssrC{@} character. - -In the second subgoal, the tactic: - -\begin{center} - \ssrC{move=>} \ssrN{clear-switch}\ssrC{} \ssrN{i-item}\ssrC{.} -\end{center} - -is performed if at least one of these optional switches is present in -the \ssrC{wlog} tactic. - -The \ssrC{wlog} tactic is specially useful when a symmetry argument -simplifies a proof. Here is an example showing the beginning of the -proof that quotient and reminder of natural number euclidean division -are unique. -\begin{lstlisting} - Lemma quo_rem_unicity: forall d q1 q2 r1 r2, - q1*d + r1 = q2*d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2). - move=> d q1 q2 r1 r2. - wlog: q1 q2 r1 r2 / q1 <= q2. - by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith. -\end{lstlisting} - -The \ssrC{wlog suff} variant is simpler, since it cuts -\ssrN{wlog\_statement} instead of \ssrN{wlog\_statement} \ssrC{-> G}. It thus -opens the goals \ssrN{wlog\_statement} \ssrC{-> G} and \ssrN{wlog\_statement}. - -In its simplest form -the \ssrC{generally have :...} tactic -is equivalent to \ssrC{wlog suff :...} followed by \ssrC{last first}. -When the \ssrC{have} tactic -is used with the \ssrC{generally} (or \ssrC{gen}) modifier it accepts an -extra identifier followed by a comma before the usual intro pattern. -The identifier will name the new hypothesis in its more general form, -while the intro pattern will be used to process its instance. For example: -\begin{lstlisting} - Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). -\end{lstlisting} -The first subgoal will be -\begin{lstlisting} - n : nat - ngt0 : 0 < n - ==================== - (0 <= n) && (n != 0) -\end{lstlisting} -while the second one will be -\begin{lstlisting} - n : nat - ltnV : forall n, 0 < n -> (0 <= n) && (n != 0) - nge0 : 0 <= n - neqn0 : n != 0 - ==================== - P n -\end{lstlisting} - -\paragraph{Advanced generalization}\label{par:advancedgen} -The complete syntax for the items on the left hand side of the \ssrC{/} -separator is the following one: -\begin{center} -\ssrN{clear-switch} {\optsep} \optional{\ssrC{@}} \ssrN{ident} {\optsep} \ssrC{(}\optional{\ssrC{@}}\ssrN{ident} \ssrC{:=} \ssrN{c-pattern}\ssrC{)} -\end{center} -Clear operations are intertwined with generalization operations. This -helps in particular avoiding dependency issues while generalizing some facts. - -\noindent -If an \ssrN{ident} is prefixed with the \ssrC{@} prefix mark, then a -let-in redex is created, which keeps track if its body (if any). The -syntax \ssrC{(}\ssrN{ident}\ssrC{:=}\ssrN{c-pattern}\ssrC{)} allows to -generalize an arbitrary term using a given name. Note that its simplest -form \ssrC{(x := y)} is just a renaming of \ssrC{y} into \ssrC{x}. In -particular, this can be useful in order to simulate the generalization -of a section variable, otherwise not allowed. Indeed renaming does not -require the original variable to be cleared. - - -\noindent -The syntax \ssrC{(@x := y)} generates a let-in abstraction but with the following -caveat: \ssrC{x} will not bind \ssrC{y}, but its body, whenever \ssrC{y} can be -unfolded. This cover the case of both local and global definitions, as -illustrated in the following example: - -\begin{lstlisting} -Section Test. -Variable x : nat. -Definition addx z := z + x. -Lemma test : x <= addx x. -wlog H : (y := x) (@twoy := addx x) / twoy = 2 * y. -\end{lstlisting} -\noindent -The first subgoal is: -\begin{lstlisting} - (forall y : nat, let twoy := y + y in twoy = 2 * y -> y <= twoy) -> - x <= addx x -\end{lstlisting} -\noindent -To avoid unfolding the term captured by the pattern \ssrC{add x} one -can use the pattern \ssrC{id (addx x)}, that would produce the following first -subgoal: -\begin{lstlisting} - (forall y : nat, let twoy := addx y in twoy = 2 * y -> y <= twoy) -> - x <= addx x -\end{lstlisting} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Rewriting}\label{sec:rw} -\idx{rewrite \dots{}} - -The generalized use of reflection implies that most of the -intermediate results handled are properties of effectively computable -functions. The most efficient mean of establishing such results are -computation and simplification of expressions involving such -functions, i.e., rewriting. \ssr{} therefore includes an extended -\ssrC{rewrite} tactic, that unifies and combines most of the rewriting -functionalities. -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{An extended \ssrC{rewrite} tactic}\label{ssec:extrw} -The main features of the \ssrC{rewrite} tactic are: -\begin{itemize} -\item It can perform an entire series of such operations in any - subset of the goal and/or context; -\item It allows to perform rewriting, - simplifications, folding/unfolding of definitions, closing of goals; -\item Several rewriting operations can be chained in a single tactic; -\item Control over the occurrence at which rewriting is to be performed is - significantly enhanced. -\end{itemize} - - -The general form of an \ssr{} rewrite tactic is: - -\begin{center} - \ssrC{rewrite} \ssrN{rstep}$^+$\ssrC{.} -\end{center} - -The combination of a rewrite tactic with the \ssrC{in} tactical (see -section \ref{ssec:loc}) performs rewriting in both the context and the -goal. - -A rewrite step \ssrN{rstep} has the general form: - -\begin{center} - \optional{\ssrN{r-prefix}}\ssrN{r-item} -\end{center} - -where: - -\begin{longtable}{rcl} -\ssrN{r-prefix} & ::= & - \optional{\ssrC{-}} \optional{\ssrN{mult}} \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} \optional{\ssrC{[}\ssrN{r-pattern}\ssrC{]}}\\ -\ssrN{r-pattern} & ::= & -{\term} {\optsep} \ssrC{in} \optional{\ssrN{ident} \ssrC{in}} {\term} {\optsep} \optional{{\term} \ssrC{in} {\optsep} {\term} \ssrC{as} } \ssrN{ident} \ssrC{in} {\term}\\ -\ssrN{r-item} & ::= & -\optional{\ssrC{/}}{\term} {\optsep} \ssrN{s-item} \\ -\end{longtable} - - -% \begin{eqnarray*} -% \ssrN{r-prefix} & ::= & -% [\ssrC{-}]\ [\ssrN{mult}][\ssrN{occ-switch} | \ssrN{cl-item}][{\term}]\\ -% \ssrN{r-item} & ::= & -% [\ssrC{-}]{\term}\ |\ [\ssrC{-}]\ssrC{[}\ssrN[1]{term}\ssrC{]}\ssrC{/(}\ssrN[2]{term}\ssrC{)} \ |\ -% \ssrN{simpl switch} \ |\ \\ -% && \ssrN{eq-term} \ |\ \ssrC{(} \ssrN[1]{eq-term}\ssrC{,}\dots -% \ssrC{,}\ssrN[n]{eq-term} \ssrC{)} \ |\ \ssrC{(_ :}\ssrN{eq-term} \ssrC{)} -% \end{eqnarray*} - - -An \ssrN{r-prefix} contains annotations to qualify where and how the -rewrite operation should be performed: -\begin{itemize} -\item The optional initial \ssrC{-} indicates the direction of the rewriting - of \ssrN{r-item}: if present the direction is right-to-left and it is - left-to-right otherwise. -\item The multiplier \ssrN{mult} (see section \ref{ssec:iter}) - specifies if and how the rewrite operation should be repeated. -\item A rewrite operation matches the occurrences of a \emph{rewrite - pattern}, and replaces these occurrences by an other term, according - to the given \ssrN{r-item}. - The optional \emph{redex switch} $\ssrC{[}\ssrN{r-pattern}\ssrC{]}$, which - should always be surrounded by brackets, gives explicitly this - rewrite pattern. In its simplest form, it is a regular term. - If no explicit redex switch - is present the rewrite pattern to be matched is inferred from the - \ssrN{r-item}. -\item This optional {\term}, or - the \ssrN{r-item}, may be preceded by an - occurrence switch (see section \ref{ssec:select}) or a clear item - (see section \ref{ssec:discharge}), these two possibilities being - exclusive. An occurrence switch selects the occurrences of the - rewrite pattern which should be affected by the rewrite operation. -\end{itemize} - - -An \ssrN{r-item} can be: - - -\begin{itemize} -\item A \emph{simplification r-item}, represented by a - \ssrN{s-item} (see section \ref{ssec:intro}). -% In some cases, \ssrN{r-prefix}es are not supported. - Simplification operations are - intertwined with the possible other rewrite operations specified by - the list of r-items. -\item A \emph{folding/unfolding r-item}. The tactic: - - \ssrC{rewrite /}{\term} - -unfolds the head constant of \textit{term} in every occurrence of the -first matching of \textit{term} in the goal. In particular, if -\ssrC{my_def} is a (local or global) defined constant, the tactic: -\begin{lstlisting} - rewrite /my_def. -\end{lstlisting} -is analogous to: -\begin{lstlisting} - unfold my_def. -\end{lstlisting} -Conversely: -\begin{lstlisting} - rewrite -/my_def. -\end{lstlisting} -is equivalent to: -\begin{lstlisting} - fold my_def. -\end{lstlisting} -%\emph{Warning} The combination of redex switch with unfold -%\ssrN{r-item} is not yet implemented. - -When an unfold r-item is combined with a redex pattern, a conversion -operation is performed. A tactic of the form: - -\begin{center} - \ssrC{rewrite -[}\ssrN[1]{term}\ssrC{]/}\ssrN[2]{term}\ssrC{.} -\end{center} - -is equivalent to: - - -\begin{center} - \ssrC{change} \ssrN[1]{term} \ssrC{with} \ssrN[2]{term}\ssrC{.} -\end{center} - - -If \ssrN[2]{term} is a single constant and \ssrN[1]{term} head symbol -is not \ssrN[2]{term}, then the head symbol of \ssrN[1]{term} is -repeatedly unfolded until \ssrN[2]{term} appears. - -\begin{lstlisting} - Definition double x := x + x. - Definition ddouble x := double (double x). - Lemma ex1 x : ddouble x = 4 * x. - rewrite [ddouble _]/double. -\end{lstlisting} - -The resulting goal is: - -\begin{lstlisting} - double x + double x = 4 * x -\end{lstlisting} - -\emph{Warning} The \ssr{} terms containing holes are \emph{not} -typed as abstractions in this context. Hence the following script: -\begin{lstlisting} - Definition f := fun x y => x + y. - Goal forall x y, x + y = f y x. - move=> x y. - rewrite -[f y]/(y + _). -\end{lstlisting} -raises the error message -\begin{verbatim} - User error: fold pattern (y + _) does not match redex (f y) -\end{verbatim} -but the script obtained by replacing the last line with: -\begin{lstlisting} - rewrite -[f y x]/(y + _). -\end{lstlisting} -is valid. - - -\item A term, which can be: - \begin{itemize} - \item A term whose type has the form: - $$\ssrC{forall}\ (x_1\ :\ A_1)\dots(x_n\ :\ A_n),\ eq\ term_1\ term_2$$ - where $eq$ is the Leibniz equality or a registered setoid - equality. %In the case of setoid relations, the only supported - %r-prefix is the directional \ssrC{-}. - \item A list of terms $(t_1,\dots,t_n)$, each $t_i$ having a type of the - form: $$\ssrC{forall}\ (x_1\ :\ A_1)\dots(x_n\ :\ A_n),\ eq\ term_1\ term_2$$ where - $eq$ is the Leibniz equality or a registered setoid - equality. The tactic: - - \centerline{\ssrC{rewrite} \ssrN{r-prefix}\ssrC{(}$t_1$\ssrC{,}$\dots$\ssrC{,}$t_n$\ssrC{).}} - - is equivalent to: - - \centerline{\ssrC{do [rewrite} \ssrN{r-prefix} $t_1$ \ssrC{|} $\dots$ \ssrC| rewrite} \ssrN{r-prefix} $t_n$\ssrC{].} - - \item An anonymous rewrite lemma - \ssrC{(_ :} {\term}), where \textit{term} has again the form: - $$\ssrC{forall}\ (x_1\ :\ A_1)\dots(x_n\ :\ A_n),\ eq\ term_1\ term_2$$ - The tactic: - - \centerline{\ssrC{rewrite (_ :} {\term}\ssrC{)}} - - is in fact synonym of: - - \centerline{\ssrC{cutrewrite (}{\term}\ssrC{).}} - - - \end{itemize} - -\end{itemize} - - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Remarks and examples}\label{ssec:rwex} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Rewrite redex selection} -The general strategy of \ssr{} -is to grasp as many redexes as possible and to let the user select the -ones to be rewritten thanks to the improved syntax for the control of -rewriting. - -This may be a source of incompatibilities between the two \ssrC{rewrite} -tactics. - -In a rewrite tactic of the form: - - \ssrC{rewrite} \ssrN{occ-switch}\ssrC{[}\ssrN[1]{term}\ssrC{]}\ssrN[2]{term}. - -\ssrN[1]{term} is the explicit rewrite redex and -\ssrN[2]{term} is the -rewrite rule. This execution of this tactic unfolds as follows: - -\begin{itemize} -\item First \ssrN[1]{term} and \ssrN[2]{term} are $\beta\iota$ normalized. Then - \ssrN[2]{term} is put in head normal form if the Leibniz equality - constructor \ssrC{eq} is not the head symbol. This may involve $\zeta$ - reductions. -\item Then, the matching algorithm (see section \ref{ssec:set}) - determines the first subterm of the goal matching the rewrite pattern. - The rewrite pattern is - given by \ssrN[1]{term}, if an explicit redex pattern switch is provided, or by - the type of \ssrN[2]{term} otherwise. However, matching skips over - matches that would lead to trivial rewrites. All the - occurrences of this subterm in the goal are candidates for rewriting. -\item Then only the occurrences coded by \ssrN{occ-switch} (see again - section \ref{ssec:set}) are finally selected for rewriting. -\item The left hand side of $\ssrN[2]{term}$ is unified with the subterm found - by the matching algorithm, and if this succeeds, all the selected - occurrences in the goal are replaced by the right hand side of - $\ssrN[2]{term}$. -\item Finally the goal is $\beta\iota$ normalized. -\end{itemize} - -In the case $\ssrN[2]{term}$ is a list of terms, the first top-down (in -the goal) left-to-right (in the list) matching rule gets selected. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Chained rewrite steps} - - -The possibility to chain rewrite operations in a single tactic makes -scripts more compact and gathers in a single command line a bunch -of surgical -operations which would be described by a one sentence in a pen and -paper proof. - -Performing rewrite and simplification operations in a single tactic -enhances significantly the concision of scripts. For instance the -tactic: -\begin{lstlisting} - rewrite /my_def {2}[f _]/= my_eq //=. -\end{lstlisting} -unfolds \ssrC{my_def} in the goal, simplifies the second occurrence of the -first subterm matching pattern \ssrC{[f _]}, rewrites \ssrC{my_eq}, -simplifies the whole goal and closes trivial goals. - -Here are some concrete examples of chained rewrite operations, in the -proof of basic results on natural numbers arithmetic: - -\begin{lstlisting} - Lemma |*addnS*| : forall m n, m + n.+1 = (m + n).+1. - Proof. by move=> m n; elim: m. Qed. - - Lemma |*addSnnS*| : forall m n, m.+1 + n = m + n.+1. - Proof. move=> *; rewrite addnS; apply addSn. Qed. - - Lemma |*addnCA*| : forall m n p, m + (n + p) = n + (m + p). - Proof. by move=> m n; elim: m => [|m Hrec] p; rewrite ?addSnnS -?addnS. Qed. - - Lemma |*addnC*| : forall m n, m + n = n + m. - Proof. by move=> m n; rewrite -{1}[n]addn0 addnCA addn0. Qed. -\end{lstlisting} - -Note the use of the \ssrC{?} switch for parallel rewrite operations in -the proof of \ssrC{|*addnCA*|}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Explicit redex switches are matched first} -If an \ssrN{r-prefix} involves a \emph{redex switch}, the first step is to -find a subterm matching this redex pattern, independently from the left hand -side \ssrC{t1} of the equality the user wants to rewrite. - -For instance, if \ssrL-H : forall t u, t + u = u + t- is in the context of a -goal \ssrL-x + y = y + x-, the tactic: -\begin{lstlisting} - rewrite [y + _]H. -\end{lstlisting} -transforms the goal into \ssrL-x + y = x + y-. - -Note that if this first pattern matching is not compatible with the -\emph{r-item}, the rewrite fails, even if the goal contains a correct -redex matching both the redex switch and the left hand side of the -equality. For instance, if \ssrL-H : forall t u, t + u * 0 = t- is -in the context of a goal \ssrL-x + y * 4 + 2 * 0 = x + 2 * 0-, then tactic: -\begin{lstlisting} - rewrite [x + _]H. -\end{lstlisting} -raises the error message: -\begin{verbatim} - User error: rewrite rule H doesn't match redex (x + y * 4) -\end{verbatim} -while the tactic: -\begin{lstlisting} - rewrite (H _ 2). -\end{lstlisting} -transforms the goal into \ssrL-x + y * 4 = x + 2 * 0-. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Occurrence switches and redex switches} -The tactic: -\begin{lstlisting} - rewrite {2}[_ + y + 0](_: forall z, z + 0 = z). -\end{lstlisting} -transforms the goal: -\begin{lstlisting} - x + y + 0 = x + y + y + 0 + 0 + (x + y + 0) -\end{lstlisting} -into: -\begin{lstlisting} - x + y + 0 = x + y + y + 0 + 0 + (x + y) -\end{lstlisting} -and generates a second subgoal: -\begin{lstlisting} - forall z : nat, z + 0 = z -\end{lstlisting} -The second subgoal is generated by the use of an anonymous lemma in -the rewrite tactic. The effect of the tactic on the initial goal is to -rewrite this lemma at the second occurrence of the first matching -\ssrL-x + y + 0- of the explicit rewrite redex \ssrL-_ + y + 0-. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Occurrence selection and repetition} -Occurrence selection has priority over repetition switches. This means -the repetition of a rewrite tactic specified by a multiplier -will perform matching each time an elementary rewrite operation is -performed. Repeated rewrite tactics apply to every subgoal generated -by the previous tactic, including the previous instances of the -repetition. For example: -\begin{lstlisting} - Goal forall x y z : nat, x + 1 = x + y + 1. - move=> x y z. -\end{lstlisting} -creates a goal \ssrC{ x + 1 = x + y + 1}, which is turned into \ssrC{z = z} -by the additional tactic: -\begin{lstlisting} - rewrite 2!(_ : _ + 1 = z). -\end{lstlisting} -In fact, this last tactic generates \emph{three} subgoals, -respectively -\ssrC{ x + y + 1 = z}, \ssrC{ z = z} and \ssrC{x + 1 = z}. Indeed, the second -rewrite operation specified with the \ssrC{2!} multiplier applies to -the two subgoals generated by the first rewrite. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Multi-rule rewriting} -The \ssrC{rewrite} tactic can be provided a \emph{tuple} of rewrite rules, -or more generally a tree of such rules, since this tuple can feature -arbitrary inner parentheses. We call \emph{multirule} such a -generalized rewrite rule. This feature is of special interest when it -is combined with multiplier switches, which makes the \ssrC{rewrite} -tactic iterates the rewrite operations prescribed by the rules on the -current goal. For instance, let us define two triples \ssrC{multi1} and -\ssrC{multi2} as: -\begin{lstlisting} - Variables (a b c : nat). - - Hypothesis eqab : a = b. - - Hypothesis eqac : a = c. -\end{lstlisting} - -Executing the tactic: -\begin{lstlisting} - rewrite (eqab, eqac) -\end{lstlisting} -on the goal: -\begin{lstlisting} - ========= - a = a -\end{lstlisting} -turns it into \ssrC{b = b}, as rule \ssrC{eqab} is the first to apply among -the ones gathered in the tuple passed to the \ssrC{rewrite} -tactic. This multirule \ssrC{(eqab, eqac)} is actually a \Coq{} term and we -can name it with a definition: -\begin{lstlisting} -Definition |*multi1*| := (eqab, eqac). -\end{lstlisting} -In this case, the tactic \ssrC{rewrite multi1} is a synonym for -\ssrC{(eqab, eqac)}. More precisely, a multirule rewrites -the first subterm to which one of the rules applies in a left-to-right -traversal of the goal, with the first rule from the multirule tree in -left-to-right order. Matching is performed according to the algorithm -described in Section~\ref{ssec:set}, but literal matches have -priority. For instance if we add a definition and a new multirule to -our context: - -\begin{lstlisting} - Definition |*d*| := a. - - Hypotheses eqd0 : d = 0. - - Definition |*multi2*| := (eqab, eqd0). -\end{lstlisting} -then executing the tactic: -\begin{lstlisting} - rewrite multi2. -\end{lstlisting} -on the goal: -\begin{lstlisting} - ========= - d = b -\end{lstlisting} -turns it into \ssrC{0 = b}, as rule \ssrC{eqd0} applies without unfolding -the definition of \ssrC{d}. For repeated rewrites the selection process -is repeated anew. For instance, if we define: - -\begin{lstlisting} - Hypothesis eq_adda_b : forall x, x + a = b. - - Hypothesis eq_adda_c : forall x, x + a = c. - - Hypothesis eqb0 : b = 0. - - Definition |*multi3*| := (eq_adda_b, eq_adda_c, eqb0). -\end{lstlisting} -then executing the tactic: -\begin{lstlisting} - rewrite 2!multi3. -\end{lstlisting} -on the goal: -\begin{lstlisting} - ========= - 1 + a = 12 + a -\end{lstlisting} -turns it into \ssrC{0 = 12 + a}: it uses \ssrC{eq_adda_b} then \ssrC{eqb0} on the -left-hand side only. Now executing the tactic \ssrC{rewrite !multi3} -turns the same goal into \ssrC{0 = 0}. - -The grouping of rules inside a multirule does not affect the selection -strategy but can make it easier to include one rule set in another or -to (universally) quantify over the parameters of a subset of rules (as -there is special code that will omit unnecessary quantifiers for rules that -can be syntactically extracted). It is also possible to -reverse the direction of a rule subset, using a special dedicated syntax: -the tactic \ssrC{rewrite (=~ multi1)} is equivalent to -\ssrC{rewrite multi1_rev} with: -\begin{lstlisting} - Hypothesis eqba : b = a. - - Hypothesis eqca : c = a. - - Definition |*multi1_rev*| := (eqba, eqca). -\end{lstlisting} -except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created. - -Rewriting with multirules is useful to implement simplification or -transformation procedures, to be applied on terms of small to medium -size. For instance, the library \ssrL{ssrnat} --- available in the -external math-comp library --- provides two implementations for -arithmetic operations on natural numbers: an elementary one and a tail -recursive version, less inefficient but also less convenient for -reasoning purposes. The library also provides one lemma per such -operation, stating that both versions return the same values when -applied to the same arguments: - -\begin{lstlisting} - Lemma |*addE*| : add =2 addn. - Lemma |*doubleE*| : double =1 doublen. - Lemma |*add_mulE*| n m s : add_mul n m s = addn (muln n m) s. - Lemma |*mulE*| : mul =2 muln. - Lemma |*mul_expE*| m n p : mul_exp m n p = muln (expn m n) p. - Lemma |*expE*| : exp =2 expn. - Lemma |*oddE*| : odd =1 oddn. -\end{lstlisting} - -The operation on the left hand side of each lemma is the efficient -version, and the corresponding naive implementation is on the right -hand side. In order to reason conveniently on expressions involving -the efficient operations, we gather all these rules in the -definition \ssrC{|*trecE*|}: -\begin{lstlisting} - Definition |*trecE*| := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). -\end{lstlisting} -The tactic: -\begin{lstlisting} - rewrite !trecE. -\end{lstlisting} -restores the naive versions of each operation in a goal involving the -efficient ones, e.g. for the purpose of a correctness proof. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Wildcards vs abstractions} - The \ssrC{rewrite} tactic supports r-items containing holes. For example - in the tactic $(1)$: -\begin{lstlisting} - rewrite (_ : _ * 0 = 0). -\end{lstlisting} - the term \ssrC{_ * 0 = 0} is interpreted as \ssrC{forall n : nat, n * 0 = 0}. - Anyway this tactic is \emph{not} equivalent to the tactic $(2)$: -\begin{lstlisting} - rewrite (_ : forall x, x * 0 = 0). -\end{lstlisting} - The tactic $(1)$ transforms the goal - \ssrL-(y * 0) + y * (z * 0) = 0- into \ssrC{y * (z * 0) = 0} - and generates a new subgoal to prove the statement \ssrC{y * 0 = 0}, - which is the \emph{instance} of the\\ \ssrC{forall x, x * 0 = 0} - rewrite rule that - has been used to perform the rewriting. On the other hand, tactic - $(2)$ performs the same rewriting on the current goal but generates a - subgoal to prove \ssrC{forall x, x * 0 = 0}. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{When \ssr{} \ssrC{rewrite} fails on standard \Coq{} licit rewrite} -In a few cases, the \ssr{} \ssrC{rewrite} tactic fails -rewriting some redexes which standard \Coq{} successfully rewrites. -There are two main cases: - -\begin{itemize} -\item \ssr{} never accepts to rewrite indeterminate patterns like: -\begin{lstlisting} - Lemma |*foo*| : forall x : unit, x = tt. -\end{lstlisting} -\ssr{} will however accept the $\eta\zeta$ expansion of this rule: -\begin{lstlisting} - Lemma |*fubar*| : forall x : unit, (let u := x in u) = tt. -\end{lstlisting} -\item In standard \Coq{}, suppose that we work in the following context: -\begin{lstlisting} - Variable g : nat -> nat. - Definition |*f*| := g. -\end{lstlisting} -then rewriting \ssrC{H : forall x, f x = 0} in the goal -\ssrC{g 3 + g 3 = g 6} succeeds -and transforms the goal into \ssrC{0 + 0 = g 6}. - -This rewriting is not possible in \ssr{} because there is no -occurrence of the head symbol \ssrC{f} of the rewrite rule in the -goal. Rewriting with \ssrC{H} first requires unfolding the occurrences of -\ssrC{f} where the substitution is to be performed (here there is a single -such occurrence), using tactic \ssrC{rewrite /f} (for a global -replacement of \ssrC{f} by \ssrC{g}) or \ssrC{rewrite $\ \ssrN{pattern}$/f}, for a -finer selection. -\end{itemize} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Existential metavariables and rewriting} -\label{ssec:rewcaveats} -The \ssrC{rewrite} tactic will not instantiate existing existential -metavariables when matching a redex pattern. - -If a rewrite rule generates a goal -with new existential metavariables, these will be generalized as for \ssrC{apply} -(see page~\pageref{sssec:apply}) and corresponding new goals will be generated. -For example, consider the following script: - -\begin{lstlisting} - Lemma |*ex3*| (x : 'I_2) y (le_1 : y < 1) (E : val x = y) : Some x = insub y. - rewrite insubT ?(leq_trans le_1)// => le_2. -\end{lstlisting} - -Since \ssrC{insubT} has the following type: - -\begin{lstlisting} - forall T P (sT : subType P) (x : T) (Px : P x), insub x = Some (Sub x Px) -\end{lstlisting} - -and since the implicit argument corresponding to the \ssrC{Px} abstraction is not -supplied by the user, the resulting goal should be \ssrC{Some x = Some (Sub y -$\;\;?_{Px}$)}. Instead, \ssr{} \ssrC{rewrite} tactic generates the two following -goals: -\begin{lstlisting} - y < 2 - forall Hyp0 : y < 2, Some x = Some (Sub y Hyp0) -\end{lstlisting} -The script closes the former with \ssrC{?(leq_trans le_1)//}, then it introduces -the new generalization naming it \ssrC{le_2}. - -\begin{lstlisting} - x : 'I_2 - y : nat - le_1 : y < 1 - E : val x = y - le_2 : y < 2 - ============================ - Some x = Some (Sub y le_2) -\end{lstlisting} - -As a temporary limitation, this behavior is available only if the rewriting -rule is stated using Leibniz equality (as opposed to setoid relations). -It will be extended to other rewriting relations in the future. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Locking, unlocking} \label{ssec:lock} - -As program proofs tend to generate large goals, it is important to be -able to control the partial evaluation performed by the simplification -operations that are performed by the tactics. These evaluations can -for example come from a \ssrC{/=} simplification switch, or from rewrite steps -which may expand large terms while performing conversion. We definitely -want to avoid repeating large subterms of the goal in -the proof script. We do this by -``clamping down'' selected function symbols in the goal, which -prevents them from -being considered in simplification or rewriting steps. This clamping -is accomplished by using the occurrence switches (see section -\ref{sssec:occselect}) together with ``term tagging'' operations. - -\ssr{} provides two levels of tagging. - -The first one uses auxiliary definitions to introduce a provably equal -copy of any term \ssrC{t}. However this copy is (on purpose) -\emph{not convertible} to \ssrC{t} in the \Coq{} system\footnote{This is - an implementation feature: there is not such obstruction in the - metatheory}. The job is done by the following construction: - -\begin{lstlisting} - Lemma |*master_key*| : unit. Proof. exact tt. Qed. - Definition |*locked*| A := let: tt := master_key in fun x : A => x. - Lemma |*lock*| : forall A x, x = locked x :> A. -\end{lstlisting} -Note that the definition of \ssrC{|*master_key*|} is explicitly opaque. -The equation \ssrC{t = locked t} given by the \ssrC{lock} lemma can be used -for selective rewriting, blocking on the fly the reduction in the -term \ssrC{t}. -For example the script: -\begin{lstlisting} - Require Import List. - Variable A : Type. - - Fixpoint |*my_has*| (p : A -> bool)(l : list A){struct l} : bool:= - match l with - |nil => false - |cons x l => p x || (my_has p l) - end. - - Goal forall a x y l, a x = true -> my_has a ( x :: y :: l) = true. - move=> a x y l Hax. -\end{lstlisting} -where \ssrL{||} denotes the boolean disjunction, results in a goal -\ssrC{my_has a ( x :: y :: l) = true}. The tactic: -\begin{lstlisting} - rewrite {2}[cons]lock /= -lock. -\end{lstlisting} -turns it into \ssrC{a x || my_has a (y :: l) = true}. -Let us now start by reducing the initial goal without blocking reduction. -The script: -\begin{lstlisting} - Goal forall a x y l, a x = true -> my_has a ( x :: y :: l) = true. - move=> a x y l Hax /=. -\end{lstlisting} -creates a goal \ssrC{(a x) || (a y) || (my_has a l) = true}. Now the -tactic: -\begin{lstlisting} - rewrite {1}[orb]lock orbC -lock. -\end{lstlisting} -where \ssrC{orbC} states the commutativity of \ssrC{orb}, changes the -goal into\\ \ssrC{(a x) || (my_has a l) || (a y) = true}: only the -arguments of the second disjunction where permuted. - - -It is sometimes desirable to globally prevent a definition from being -expanded by simplification; this is done by adding \ssrC{locked} in the -definition. - -For instance, the function \ssrC{|*fgraph_of_fun*|} maps a function whose -domain and codomain are finite types to a concrete representation of -its (finite) graph. Whatever implementation of this transformation we -may use, we want it to be hidden to simplifications and tactics, to -avoid the collapse of the graph object: -\begin{lstlisting} - Definition |*fgraph_of_fun*| := - locked - (fun (d1 :finType) (d2 :eqType) (f : d1 -> d2) => Fgraph (size_maps f _)). -\end{lstlisting} - -We provide a special tactic \ssrC{unlock} for unfolding such definitions -while removing ``locks'', e.g., the tactic: - - \ssrC{unlock} \ssrN{occ-switch}\ssrC{fgraph_of_fun}. - -replaces the occurrence(s) of \ssrC{fgraph_of_fun} coded by the \ssrN{occ-switch} -with \ssrC{(Fgraph (size_maps _ _))} in the goal. - -We found that it was usually preferable to prevent the expansion of -some functions by the partial evaluation switch ``/='', unless -this allowed the evaluation of a condition. This is possible thanks to -an other mechanism of term tagging, resting on the following -\emph{Notation}: -\begin{lstlisting} - Notation "'nosimpl' t" := (let: tt := tt in t). -\end{lstlisting} - -The term \ssrC{(nosimpl t)} simplifies to t \emph{except} in a -definition. More precisely, -given: -\begin{lstlisting} - Definition |*foo*| := (nosimpl bar). -\end{lstlisting} -the term \ssrC{foo (or (foo t'))} will \emph{not} be expanded by the -\emph{simpl} tactic unless it is in a forcing context (e.g., in -\ssrC{match foo t' with $\dots$ end}, \ssrC{foo t'} will be reduced if this allows -\ssrC{match} to be reduced). Note that \ssrC{nosimpl bar} is simply notation -for a term that reduces to \ssrC{bar}; hence \ssrC{unfold foo} will replace - \ssrC{foo} by \ssrC{bar}, and \ssrC{fold foo} will replace \ssrC{bar} by - \ssrC{foo}. - -\emph{Warning} The \ssrC{nosimpl} trick only works if no reduction is -apparent in \ssrC{t}; in particular, the declaration: -\begin{lstlisting} - Definition |*foo*| x := nosimpl (bar x). -\end{lstlisting} -will usually not work. Anyway, the common practice is to tag only the -function, and to use the following definition, which blocks the -reduction as expected: -\begin{lstlisting} - Definition |*foo*| x := nosimpl bar x. -\end{lstlisting} - - -A standard example making this technique shine is the case of -arithmetic operations. We define for instance: -\begin{lstlisting} - Definition |*addn*| := nosimpl plus. -\end{lstlisting} -The operation \ssrC{addn} behaves exactly like plus, except that -\ssrC{(addn (S n) m)} will not -simplify spontaneously to \ssrC{(S (addn n m))} (the two terms, however, are -inter-convertible). In addition, the unfolding step: -\begin{lstlisting} -rewrite /addn -\end{lstlisting} -will replace \ssrC{addn} directly with \ssrC{plus}, so the \ssrC{nosimpl} form -is essentially invisible. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Congruence}\label{ssec:congr} - -Because of the way matching interferes with type families parameters, -the tactic: -\begin{lstlisting} - apply: my_congr_property. -\end{lstlisting} -will generally fail to perform congruence simplification, even on -rather simple cases. We therefore provide a -more robust alternative in which the function is supplied: -$$\ssrC{congr}\ [\ssrN{int}]\ {\term}$$ - -This tactic: -\begin{itemize} -\item checks that the goal is a Leibniz equality -\item matches both sides of this equality with ``{\term} applied to - some arguments'', inferring the right number of arguments from the goal - and the type of {\term}. This may - expand some definitions or fixpoints. -\item generates the subgoals corresponding to pairwise equalities of - the arguments present in the goal. -\end{itemize} - -The goal can be a non dependent product \ssrC{P -> Q}. -In that case, the system asserts the equation \ssrC{P = Q}, uses it to solve -the goal, and calls the \ssrC{congr} tactic on the remaining goal -\ssrC{P = Q}. This can be useful for instance to perform a transitivity -step, like in the following situation: -\begin{lstlisting} - x, y, z : nat - =============== - x = y -> x = z -\end{lstlisting} -the tactic \ssrC{congr (_ = _)} turns this goal into: - -\begin{lstlisting} - x, y, z : nat - =============== - y = z -\end{lstlisting} -which can also be obtained starting from: -\begin{lstlisting} - x, y, z : nat - h : x = y - =============== - x = z -\end{lstlisting} -and using the tactic \ssrC{congr (_ = _): h}. - -The optional \ssrN{int} forces the number of arguments for which the -tactic should generate equality proof obligations. - -This tactic supports equalities between applications with dependent -arguments. Yet dependent arguments should have exactly the same -parameters on both sides, and these parameters should appear as first -arguments. - -The following script: -\begin{lstlisting} - Definition f n := match n with 0 => plus | S _ => mult end. - Definition g (n m : nat) := plus. - - Goal forall x y, f 0 x y = g 1 1 x y. - by move=> x y; congr plus. - Qed. -\end{lstlisting} -shows that the \ssrC{congr} tactic matches \ssrC{plus} with \ssrC{f 0} on the -left hand side and \ssrC{g 1 1} on the right hand side, and solves the goal. - -The script: -\begin{lstlisting} - Goal forall n m, m <= n -> S m + (S n - S m) = S n. - move=> n m Hnm; congr S; rewrite -/plus. -\end{lstlisting} -generates the subgoal \ssrC{m + (S n - S m) = n}. The tactic -\ssrC{rewrite -/plus} folds back the expansion of \ssrC{plus} which was -necessary for matching both sides of the equality with an application -of \ssrC{S}. - -Like most \ssr{} arguments, {\term} can contain wildcards. -The script: -\begin{lstlisting} - Goal forall x y, x + (y * (y + x - x)) = x * 1 + (y + 0) * y. - move=> x y; congr ( _ + (_ * _)). -\end{lstlisting} -generates three subgoals, respectively \ssrC{x = x * 1}, \ssrC{y = y + 0} -and \ssrC{ y + x - x = y}. -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Contextual patterns} -\label{ssec:rewp} - -The simple form of patterns used so far, ${\term}s$ possibly containing -wild cards, often require an additional \ssrN{occ-switch} to be specified. -While this may work pretty fine for small goals, the use of polymorphic -functions and dependent types may lead to an invisible duplication of functions -arguments. These copies usually end up in types hidden by the implicit -arguments machinery or by user defined notations. In these situations -computing the right occurrence numbers is very tedious because they must be -counted on the goal as printed after setting the \ssrC{Printing All} flag. -Moreover the resulting script is not really informative for the reader, since -it refers to occurrence numbers he cannot easily see. - -Contextual patterns mitigate these issues allowing to specify occurrences -according to the context they occur in. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Syntax} - -The following table summarizes the full syntax of -\ssrN{c-pattern} and the corresponding subterm(s) identified -by the pattern. -In the third column we use s.m.r. for -``the subterms matching the redex'' specified in the second column. - -\begin{center} -%\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.21\textwidth}|>{\arraybackslash}m{0.39\textwidth}} -\begin{tabular}{llp{10em}} -\ssrN{c-pattern} & redex & subterms affected \\ -\hline -{\term} & {\term} & all occurrences of {\term}\\ -\hline -$\ssrN{ident}\ \ssrC{in}\ {\term}$ & - subterm of {\term} selected by \ssrN{ident} & - all the subterms identified by \ssrN{ident} in all - the occurrences of {\term} \\ -\hline -$\ssrN[1]{term}\ \ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ & $\ssrN[1]{term}$ & - in all s.m.r. in all the subterms identified by \ssrN{ident} in all - the occurrences of $\ssrN[2]{term}$ \\ -\hline -$\ssrN[1]{term}\ \ssrC{as}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ & $\ssrN[1]{term}$ & - in all the subterms identified by \ssrN{ident} in all - the occurrences of $\ssrN[2]{term}[\ssrN[1]{term}/\ssrN{ident}]$\\ -\hline -%\end{tabularx} -\end{tabular} -\end{center} - -The \ssrC{rewrite} tactic supports two more patterns obtained -prefixing the first two with \ssrC{in}. The intended meaning is that the -pattern identifies all subterms of the specified context. The -\ssrC{rewrite} tactic will infer a pattern for the redex looking at the -rule used for rewriting. - -\begin{center} -\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.21\textwidth}|>{\arraybackslash}m{0.39\textwidth}} -\ssrN{r-pattern} & redex & subterms affected \\ -\hline -$\ssrC{in}\ {\term}$ & inferred from rule & - in all s.m.r. in all occurrences of {\term}\\ -\hline -$\ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ {\term}$ & inferred from rule & - in all s.m.r. in all the subterms identified by \ssrN{ident} in all - the occurrences of {\term} \\ -\hline -\end{tabularx} -\end{center} - -The first \ssrN{c-pattern} is the simplest form matching any -context but selecting a specific redex and has been described in the -previous sections. We have seen so far that the possibility of -selecting a redex using a term with holes is already a powerful mean of redex -selection. Similarly, any {\term}s provided by the -user in the more complex forms of \ssrN{c-pattern}s presented in the -tables above can contain holes. - -For a quick glance at what can be expressed with the last -\ssrN{r-pattern} consider the goal \ssrC{a = b} and the tactic -\begin{lstlisting} - rewrite [in X in _ = X]rule. -\end{lstlisting} -It rewrites all occurrences of the left hand side of \ssrC{rule} inside -\ssrC{b} only (\ssrC{a}, and the hidden type of the equality, are ignored). -Note that the variant \ssrC{rewrite [X in _ = X]rule} would have -rewritten \ssrC{b} exactly (i.e., it would only work if \ssrC{b} and the -left hand side of \ssrC{rule} can be unified). - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Matching contextual patterns} - -The \ssrN{c-pattern}s and \ssrN{r-pattern}s involving -{\term}s with holes are matched -against the goal in order to find a closed instantiation. This -matching proceeds as follows: - -\begin{center} -\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.65\textwidth}} -\ssrN{c-pattern} & instantiation order and place for $\ssrN[i]{term}$ and redex\\ -\hline -{\term} & {\term} is matched against the goal, redex is unified with - the instantiation of {\term}\\ -\hline -$\ssrN{ident}\ \ssrC{in}\ {\term}$ & - {\term} is matched against the goal, redex is - unified with the subterm of the - instantiation of {\term} identified by \ssrN{ident}\\ -\hline -$\ssrN[1]{term}\ \ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ & - $\ssrN[2]{term}$ is matched against the goal, $\ssrN[1]{term}$ is - matched against the subterm of the - instantiation of $\ssrN[1]{term}$ identified by \ssrN{ident}, - redex is unified with the instantiation of $\ssrN[1]{term}$\\ -\hline -$\ssrN[1]{term}\ \ssrC{as}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ & - $\ssrN[2]{term}[\ssrN[1]{term}/\ssrN{ident}]$ - is matched against the goal, - redex is unified with the instantiation of $\ssrN[1]{term}$\\ -\hline -\end{tabularx} -\end{center} - -In the following patterns, the redex is intended to be inferred from the -rewrite rule. - -\begin{center} -\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.65\textwidth}} -\ssrN{r-pattern} & instantiation order and place for $\ssrN[i]{term}$ and redex\\ -\hline -$\ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ {\term}$ & - {\term} is matched against the goal, the redex is - matched against the subterm of the - instantiation of {\term} identified by \ssrN{ident}\\ -\hline -$\ssrC{in}\ {\term}$ & {\term} is matched against the goal, redex is - matched against the instantiation of {\term}\\ -\hline -\end{tabularx} -\end{center} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Examples} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection{Contextual pattern in \ssrC{set} and the \ssrC{:} tactical} - -As already mentioned in section~\ref{ssec:set} the \ssrC{set} tactic -takes as an argument a term in open syntax. This term is interpreted -as the simplest for of \ssrN{c-pattern}. To void confusion in the grammar, -open syntax is supported only for the simplest form of patterns, while - parentheses are required around more complex patterns. - -\begin{lstlisting} -set t := (X in _ = X). -set t := (a + _ in X in _ = X). -\end{lstlisting} - -Given the goal \ssrC{a + b + 1 = b + (a + 1)} the first tactic -captures \ssrC{b + (a + 1)}, while the latter \ssrC{a + 1}. - -Since the user may define an infix notation for \ssrC{in} the former -tactic may result ambiguous. The disambiguation rule implemented is -to prefer patterns over simple terms, but to interpret a pattern with -double parentheses as a simple term. For example -the following tactic would capture any occurrence of the term `\ssrC{a in A}'. - -\begin{lstlisting} -set t := ((a in A)). -\end{lstlisting} - -Contextual pattern can also be used as arguments of the \ssrC{:} tactical. -For example: -\begin{lstlisting} -elim: n (n in _ = n) (refl_equal n). -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection{Contextual patterns in \ssrC{rewrite}} -As a more comprehensive example consider the following goal: -\begin{lstlisting} - (x.+1 + y) + f (x.+1 + y) (z + (x + y).+1) = 0 -\end{lstlisting} -The tactic \ssrC{rewrite [in f _ _]addSn} turns it into: -\begin{lstlisting} - (x.+1 + y) + f (x + y).+1 (z + (x + y).+1) = 0 -\end{lstlisting} -since the simplification rule \ssrC{addSn} is applied only under the \ssrC{f} symbol. -Then we simplify also the first addition and expand \ssrC{0} into \ssrC{0+0}. -\begin{lstlisting} - rewrite addSn -[X in _ = X]addn0. -\end{lstlisting} -obtaining: -\begin{lstlisting} - (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + 0 -\end{lstlisting} -Note that the right hand side of \ssrC{addn0} is undetermined, but the -rewrite pattern specifies the redex explicitly. The right hand side of -\ssrC{addn0} is unified with the term identified by \ssrC{X}, \ssrC{0} here. - -The following pattern does not specify a redex, since it -identifies an entire region, hence the rewrite rule has to be instantiated -explicitly. Thus the tactic: -\begin{lstlisting} - rewrite -{2}[in X in _ = X](addn0 0). -\end{lstlisting} -changes the goal as follows: -\begin{lstlisting} - (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + (0 + 0) -\end{lstlisting} -The following tactic is quite tricky: -\begin{lstlisting} - rewrite [_.+1 in X in f _ X](addnC x.+1). -\end{lstlisting} -and the resulting goals is: -\begin{lstlisting} - (x + y).+1 + f (x + y).+1 (z + (y + x.+1)) = 0 + (0 + 0) -\end{lstlisting} -The explicit redex \ssrC{_.+1} is important since its head -constant \ssrC{S} differs from the head constant inferred from -\ssrC{(addnC x.+1)} (that is \ssrC{addn}, denoted \ssrC{+} here). -Moreover, the pattern \ssrC{f _ X} is important to rule out the first occurrence -of \ssrC{(x + y).+1}. Last, only the subterms of \ssrC{f _ X} identified by \ssrC{X} are -rewritten, thus the first argument of \ssrC{f} is skipped too. -Also note the pattern \ssrC{_.+1} is interpreted in the context -identified by \ssrC{X}, thus it gets instantiated to \ssrC{(y + x).+1} and -not \ssrC{(x + y).+1}. - -The last rewrite pattern allows to specify exactly the shape of the term -identified by \ssrC{X}, that is thus unified with the left hand side of the -rewrite rule. -\begin{lstlisting} - rewrite [x.+1 + y as X in f X _]addnC. -\end{lstlisting} -The resulting goal is: -\begin{lstlisting} - (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0) -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Patterns for recurrent contexts} - -The user can define shortcuts for recurrent contexts corresponding to the -\ssrN{ident} \ssrC{in} {\term} part. The notation scope identified -with \ssrC{\%pattern} provides a special notation `\ssrC{(X in t)}' the user -must adopt to define context shortcuts. - -The following example is taken from \ssrC{ssreflect.v} where the -\ssrC{LHS} and \ssrC{RHS} shortcuts are defined. - -\begin{lstlisting} -Notation RHS := (X in _ = X)%pattern. -Notation LHS := (X in X = _)%pattern. -\end{lstlisting} - -Shortcuts defined this way can be freely used in place of the -trailing \ssrN{ident} \ssrC{in} {\term} part of any contextual -pattern. -Some examples follow: - -\begin{lstlisting} -set rhs := RHS. -rewrite [in RHS]rule. -case: (a + _ in RHS). -\end{lstlisting} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Views and reflection}\label{sec:views} - -The bookkeeping facilities presented in section \ref{sec:book} are -crafted to ease simultaneous introductions and generalizations of facts and -casing, -naming $\dots$ operations. It also a common practice to make a stack -operation immediately followed by an \emph{interpretation} of the fact -being pushed, -that is, to apply a lemma to this fact before passing it -to a tactic for decomposition, application and so on. - - -% possibly - -% Small scale reflection consists in using a two levels -% approach locally when developing formal proofs. This means that a -% fact, which may be an assumption, or the goal itself, will often be -% \emph{interpreted} before being passed to a tactic -% for decomposition, application and so on. - -\ssr{} provides a convenient, unified syntax to combine these -interpretation operations with the proof stack operations. This -\emph{view mechanism} relies on the combination of the \ssrC{/} view -switch with bookkeeping tactics and tacticals. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Interpreting eliminations} -\idx{elim/\dots{}} - -The view syntax combined with the \ssrC{elim} tactic specifies an -elimination scheme to -be used instead of the default, generated, one. Hence the \ssr{} tactic: -\begin{lstlisting} - elim/V. -\end{lstlisting} -is a synonym for: -\begin{lstlisting} - intro top; elim top using V; clear top. -\end{lstlisting} -where \ssrC{top} is a fresh name and \ssrC{V} any second-order lemma. - -Since an elimination view supports the two bookkeeping tacticals of -discharge and introduction (see section \ref{sec:book}), the \ssr{} tactic: -\begin{lstlisting} - elim/V: x => y. -\end{lstlisting} -is a synonym for: -\begin{lstlisting} - elim x using V; clear x; intro y. -\end{lstlisting} -where \ssrC{x} is a variable in the context, \ssrC{y} a fresh name and \ssrC{V} -any second order lemma; \ssr{} relaxes the syntactic restrictions of -the \Coq{} \ssrC{elim}. The first pattern following \ssrC{:} can be a \ssrC{_} -wildcard if the conclusion of the view \ssrC{V} specifies a pattern for -its last argument (e.g., if \ssrC{V} is a functional induction lemma -generated by the \ssrC{Function} command). - -The elimination view mechanism is compatible with the equation name -generation (see section \ref{ssec:equations}). - -The following script illustrate a toy example of this feature. Let us -define a function adding an element at the end of a list: -\begin{lstlisting} - Require Import List. - - Variable d : Type. - - Fixpoint |*add_last*|(s : list d) (z : d) {struct s} : list d := - match s with - | nil => z :: nil - | cons x s' => cons x (add_last s' z) - end. -\end{lstlisting} - -One can define an alternative, reversed, induction principle on inductively -defined \ssrC{list}s, by proving the following lemma: - -\begin{lstlisting} - Lemma |*last_ind_list*| : forall (P : list d -> Type), - P nil -> - (forall (s : list d) (x : d), P s -> P (add_last s x)) -> forall s : list d, P s. -\end{lstlisting} - -Then the combination of elimination views with equation names result -in a concise syntax for reasoning inductively using the user -defined elimination scheme. The script: -\begin{lstlisting} - Goal forall (x : d)(l : list d), l = l. - move=> x l. - elim/last_ind_list E : l=> [| u v]; last first. -\end{lstlisting} -generates two subgoals: the first one to prove \ssrC{nil = nil} in a -context featuring \ssrC{E : l = nil} and the second to prove -\ssrC{add_last u v = add_last u v}, in a context containing -\ssrC{E : l = add_last u v}. - -User provided eliminators (potentially generated with the -\ssrC{Function} \Coq{}'s command) can be combined with the type family switches -described in section~\ref{ssec:typefam}. Consider an eliminator -\ssrC{foo_ind} of type: - - \ssrC{foo_ind : forall $\dots$, forall x : T, P p$_1$ $\dots$ p$_m$} - -and consider the tactic - - \ssrC{elim/foo_ind: e$_1$ $\dots$ / e$_n$} - -The \ssrC{elim/} tactic distinguishes two cases: -\begin{description} -\item[truncated eliminator] when \ssrC{x} does not occur in \ssrC{P p$_1 \dots$ p$_m$} - and the type of \ssrC{e$_n$} unifies with \ssrC{T} and \ssrC{e$_n$} is not \ssrC{_}. - In that case, \ssrC{e$_n$} is passed to the eliminator as the last argument - (\ssrC{x} in \ssrC{foo_ind}) and \ssrC{e$_{n-1} \dots$ e$_1$} are used as patterns - to select in the goal the occurrences that will be bound by the - predicate \ssrC{P}, thus it must be possible to unify the sub-term of - the goal matched by \ssrC{e$_{n-1}$} with \ssrC{p$_m$}, the one matched by - \ssrC{e$_{n-2}$} with \ssrC{p$_{m-1}$} and so on. -\item[regular eliminator] in all the other cases. Here it must be - possible to unify the term matched by - \ssrC{e$_n$} with \ssrC{p$_m$}, the one matched by - \ssrC{e$_{n-1}$} with \ssrC{p$_{m-1}$} and so on. Note that - standard eliminators have the shape \ssrC{$\dots$forall x, P $\dots$ x}, thus - \ssrC{e$_n$} is the pattern identifying the eliminated term, as expected. -\end{description} -As explained in section~\ref{ssec:typefam}, the initial prefix of -\ssrC{e$_i$} can be omitted. - -Here an example of a regular, but non trivial, eliminator: -\begin{lstlisting} - Function |*plus*| (m n : nat) {struct n} : nat := - match n with 0 => m | S p => S (plus m p) end. -\end{lstlisting} -The type of \ssrC{plus_ind} is -\begin{lstlisting} -plus_ind : forall (m : nat) (P : nat -> nat -> Prop), - (forall n : nat, n = 0 -> P 0 m) -> - (forall n p : nat, n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) -> - forall n : nat, P n (plus m n) -\end{lstlisting} -Consider the following goal -\begin{lstlisting} - Lemma |*exF*| x y z: plus (plus x y) z = plus x (plus y z). -\end{lstlisting} -The following tactics are all valid and perform the same elimination -on that goal. -\begin{lstlisting} - elim/plus_ind: z / (plus _ z). - elim/plus_ind: {z}(plus _ z). - elim/plus_ind: {z}_. - elim/plus_ind: z / _. -\end{lstlisting} -In the two latter examples, being the user provided pattern a wildcard, the -pattern inferred from the type of the eliminator is used instead. For both -cases it is \ssrC{(plus _ _)} and matches the subterm \ssrC{plus (plus x y)$\;$z} thus -instantiating the latter \ssrC{_} with \ssrC{z}. Note that the tactic -\ssrC{elim/plus_ind: y / _} would have resulted in an error, since \ssrC{y} and \ssrC{z} -do no unify but the type of the eliminator requires the second argument of -\ssrC{P} to be the same as the second argument of \ssrC{plus} in the second -argument of \ssrC{P}. - -Here an example of a truncated eliminator. Consider the goal -\begin{lstlisting} - p : nat_eqType - n : nat - n_gt0 : 0 < n - pr_p : prime p - ================= - p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 -> - exists2 x : nat * nat, x \in prime_decomp n & p = x.1 -\end{lstlisting} -and the tactic -\begin{lstlisting} -elim/big_prop: _ => [| u v IHu IHv | [q e] /=]. -\end{lstlisting} -where the type of the eliminator is -\begin{lstlisting} -big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R), - Pb idx -> - (forall x y : R, Pb x -> Pb y -> Pb (op1 x y)) -> - forall (I : Type) (r : seq I) (P : pred I) (F : I -> R), - (forall i : I, P i -> Pb (F i)) -> - Pb (\big[op1/idx]_(i <- r | P i) F i) -\end{lstlisting} -Since the pattern for the argument of \ssrC{Pb} is not specified, the inferred one -is used instead: \ssrC{(\\big[_/_]_(i <- _ | _ i) _ i)}, and after the -introductions, the following goals are generated. -\begin{lstlisting} -subgoal 1 is: - p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 -subgoal 2 is: - p %| u * v -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 -subgoal 3 is: - (q, e) \in prime_decomp n -> p %| q ^ e -> - exists2 x : nat * nat, x \in prime_decomp n & p = x.1 -\end{lstlisting} -Note that the pattern matching algorithm instantiated all the variables -occurring in the pattern. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Interpreting assumptions}\label{ssec:assumpinterp} -\idx{move/\dots{}} - -Interpreting an assumption in the context of a proof is applying it a -correspondence lemma before generalizing, and/or decomposing it. -For instance, with the extensive use of boolean reflection (see -section \ref{ssec:boolrefl}), it is -quite frequent to need to decompose the logical interpretation of (the -boolean expression of) a -fact, rather than the fact itself. -This can be achieved by a combination of \ssrC{move : _ => _} -switches, like in the following script, where \ssrC{||} is a notation for -the boolean disjunction: -\begin{lstlisting} - Variables P Q : bool -> Prop. - Hypothesis |*P2Q*| : forall a b, P (a || b) -> Q a. - - Goal forall a, P (a || a) -> True. - move=> a HPa; move: {HPa}(P2Q _ _ HPa) => HQa. -\end{lstlisting} -which transforms the hypothesis \ssrC{HPn : P n} which has been -introduced from the initial statement into \ssrC{HQn : Q n}. -This operation is so common that the tactic shell has -specific syntax for it. -The following scripts: -\begin{lstlisting} - Goal forall a, P (a || a) -> True. - move=> a HPa; move/P2Q: HPa => HQa. -\end{lstlisting} -or more directly: -\begin{lstlisting} - Goal forall a, P (a || a) -> True. - move=> a; move/P2Q=> HQa. -\end{lstlisting} -are equivalent to the former one. The former script shows how to -interpret a fact (already in the context), thanks to the discharge -tactical (see section \ref{ssec:discharge}) and the latter, how to -interpret the top assumption of a goal. Note -that the number of wildcards to be inserted to find the correct -application of the view lemma to the hypothesis has been automatically -inferred. - -The view mechanism is compatible with the \ssrC{case} tactic and with the -equation name generation mechanism (see section \ref{ssec:equations}): -\begin{lstlisting} - Variables P Q: bool -> Prop. - Hypothesis |*Q2P*| : forall a b, Q (a || b) -> P a \/ P b. - - Goal forall a b, Q (a || b) -> True. - move=> a b; case/Q2P=> [HPa | HPb]. -\end{lstlisting} -creates two new subgoals whose contexts no more contain -\ssrC{HQ : Q (a || b)} but respectively \ssrC{HPa : P a} and -\ssrC{HPb : P b}. This view tactic -performs: -\begin{lstlisting} - move=> a b HQ; case: {HQ}(Q2P _ _ HQ) => [HPa | HPb]. -\end{lstlisting} - -The term on the right of the \ssrC{/} view switch is called a \emph{view - lemma}. Any \ssr{} term coercing to a product type can be used as a -view lemma. - - -The examples we have given so far explicitly provide the direction of the -translation to be performed. In fact, view lemmas need not to be -oriented. The view mechanism is able to detect which -application is relevant for the current goal. For instance, the -script: -\begin{lstlisting} - Variables P Q: bool -> Prop. - Hypothesis |*PQequiv*| : forall a b, P (a || b) <-> Q a. - - Goal forall a b, P (a || b) -> True. - move=> a b; move/PQequiv=> HQab. -\end{lstlisting} -has the same behavior as the first example above. - -The view mechanism can insert automatically a \emph{view hint} to -transform the double implication into the expected simple implication. -The last script is in fact equivalent to: -\begin{lstlisting} - Goal forall a b, P (a || b) -> True. - move=> a b; move/(iffLR (PQequiv _ _)). -\end{lstlisting} -where: -\begin{lstlisting} - Lemma |*iffLR*| : forall P Q, (P <-> Q) -> P -> Q. -\end{lstlisting} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Specializing assumptions} -\idx{move/\dots{}} - -The special case when the \emph{head symbol} of the view lemma is a -wildcard is used to interpret an assumption by \emph{specializing} -it. The view mechanism hence offers the possibility to -apply a higher-order assumption to some given arguments. - -For example, the script: -\begin{lstlisting} - Goal forall z, (forall x y, x + y = z -> z = x) -> z = 0. - move=> z; move/(_ 0 z). -\end{lstlisting} -changes the goal into: -\begin{lstlisting} - (0 + z = z -> z = 0) -> z = 0 -\end{lstlisting} - - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Interpreting goals}\label{ssec:goalinterp} - -In a similar way, it is also often convenient to interpret a goal by changing -it into an equivalent proposition. The view mechanism of \ssr{} has a -special syntax \ssrC{apply/} for combining simultaneous goal -interpretation operations and -bookkeeping steps in a single tactic. - -With the hypotheses of section \ref{ssec:assumpinterp}, the following -script, where \ssrL+~~+ denotes the boolean negation: -\begin{lstlisting} - Goal forall a, P ((~~ a) || a). - move=> a; apply/PQequiv. -\end{lstlisting} -transforms the goal into \ssrC{Q (~~ a)}, and is equivalent to: -\begin{lstlisting} - Goal forall a, P ((~~ a) || a). - move=> a; apply: (iffRL (PQequiv _ _)). -\end{lstlisting} -where \ssrC{iffLR} is the analogous of \ssrC{iffRL} for the converse -implication. - -Any \ssr{} term whose type coerces to a double implication can be used -as a view for goal interpretation. - -Note that the goal interpretation view mechanism supports both -\ssrC{apply} and \ssrC{exact} tactics. As expected, a goal interpretation -view command \ssrC{exact/$term$} should solve the current goal or it will -fail. - - -\emph{Warning} Goal interpretation view tactics are \emph{not} compatible -with the bookkeeping tactical \ssrC{=>} since this would be redundant with -the \ssrC{apply:} {\term} \ssrC{=> _} construction. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Boolean reflection}\label{ssec:boolrefl} -In the Calculus of Inductive Construction, there is -an obvious distinction between logical propositions and boolean values. -On the one hand, logical propositions are objects -of \emph{sort} \ssrC{Prop} which is the carrier of intuitionistic -reasoning. Logical connectives in \ssrC{Prop} are \emph{types}, which give precise -information on the structure of their proofs; this information is -automatically exploited by \Coq{} tactics. For example, \Coq{} knows that a -proof of \ssrL+A \/ B+ is either a proof of \ssrC{A} or a proof of \ssrC{B}. -The tactics \ssrC{left} and \ssrC{right} change the goal \ssrL+A \/ B+ -to \ssrC{A} and \ssrC{B}, respectively; dualy, the tactic \ssrC{case} reduces the goal -\ssrL+A \/ B => G+ to two subgoals \ssrC{A => G} and \ssrC{B => G}. - -On the other hand, \ssrC{bool} is an inductive \emph{datatype} -with two constructors \ssrC{true} and \ssrC{false}. -Logical connectives on \ssrC{bool} are \emph{computable functions}, defined by -their truth tables, using case analysis: -\begin{lstlisting} - Definition (b1 || b2) := if b1 then true else b2. -\end{lstlisting} -Properties of such connectives are also established using case -analysis: the tactic \ssrC{by case: b} solves the goal -\begin{lstlisting} - b || ~~ b = true -\end{lstlisting} -by replacing \ssrC{b} first by \ssrC{true} and then by \ssrC{false}; in either case, -the resulting subgoal reduces by computation to the trivial -\ssrC{true = true}. - -Thus, \ssrC{Prop} and \ssrC{bool} are truly complementary: the former -supports robust natural deduction, the latter allows brute-force -evaluation. -\ssr{} supplies -a generic mechanism to have the best of the two worlds and move freely -from a propositional version of a -decidable predicate to its boolean version. - -First, booleans are injected into propositions -using the coercion mechanism: -\begin{lstlisting} - Coercion |*is_true*| (b : bool) := b = true. -\end{lstlisting} -This allows any boolean formula~\ssrC{b} to be used in a context -where \Coq{} would expect a proposition, e.g., after \ssrC{Lemma $\dots$ : }. -It is then interpreted as \ssrC{(is_true b)}, i.e., -the proposition \ssrC{b = true}. Coercions are elided by the pretty-printer, -so they are essentially transparent to the user. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{The \ssrC{reflect} predicate}\label{ssec:reflpred} - -To get all the benefits of the boolean reflection, it is in fact -convenient to introduce the following inductive predicate -\ssrC{reflect} to relate propositions and booleans: - -\begin{lstlisting} - Inductive |*reflect*| (P: Prop): bool -> Type := - | Reflect_true: P => reflect P true - | Reflect_false: ~P => reflect P false. -\end{lstlisting} - -The statement \ssrC{(reflect P b)} asserts that \ssrC{(is_true b)} -and \ssrC{P} are logically equivalent propositions. - -For instance, the following lemma: -\begin{lstlisting} - Lemma |*andP*|: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). -\end{lstlisting} -relates the boolean conjunction \ssrC{&&} to -the logical one \ssrL+/\+. -Note that in \ssrC{andP}, \ssrC{b1} and \ssrC{b2} are two boolean variables and -the proposition \ssrL+b1 /\ b2+ hides two coercions. -The conjunction of \ssrC{b1} and \ssrC{b2} can then be viewed -as \ssrL+b1 /\ b2+ or as \ssrC{b1 && b2}. - - -Expressing logical equivalences through this family of inductive types -makes possible to take benefit from \emph{rewritable equations} -associated to the case analysis of \Coq{}'s inductive types. - -Since the equivalence predicate is defined in \Coq{} as: -\begin{lstlisting} - Definition |*iff*| (A B:Prop) := (A -> B) /\ (B -> A). -\end{lstlisting} -where \ssrC{/\\} is a notation for \ssrC{and}: -\begin{lstlisting} - Inductive |*and*| (A B:Prop) : Prop := - conj : A -> B -> and A B -\end{lstlisting} - -This make case analysis very different according to the way an -equivalence property has been defined. - - -For instance, if we have proved the lemma: -\begin{lstlisting} - Lemma |*andE*|: forall b1 b2, (b1 /\ b2) <-> (b1 && b2). -\end{lstlisting} -let us compare the respective behaviours of \ssrC{andE} and \ssrC{andP} on a -goal: -\begin{lstlisting} - Goal forall b1 b2, if (b1 && b2) then b1 else ~~(b1||b2). -\end{lstlisting} - -The command: -\begin{lstlisting} - move=> b1 b2; case (@andE b1 b2). -\end{lstlisting} -generates a single subgoal: -\begin{lstlisting} - (b1 && b2 -> b1 /\ b2) -> (b1 /\ b2 -> b1 && b2) -> - if b1 && b2 then b1 else ~~ (b1 || b2) -\end{lstlisting} - -while the command: -\begin{lstlisting} - move=> b1 b2; case (@andP b1 b2). -\end{lstlisting} -generates two subgoals, respectively \ssrL+b1 /\ b2 -> b1+ and -\ssrL+~ (b1 /\ b2) -> ~~ (b1 || b2)+. - - - -Expressing reflection relation through the \ssrC{reflect} predicate -is hence a very convenient way to deal with classical reasoning, by -case analysis. Using the \ssrC{reflect} predicate allows moreover to -program rich specifications inside -its two constructors, which will be automatically taken into account -during destruction. This formalisation style gives far more -efficient specifications than quantified (double) implications. - - -A naming convention in \ssr{} is to postfix the name of view lemmas with \ssrC{P}. -For example, \ssrC{orP} relates \ssrC{||} and \ssrL+\/+, \ssrC{negP} relates -\ssrL+~~+ and \ssrL+~+. - -The view mechanism is compatible with \ssrC{reflect} predicates. - -For example, the script -\begin{lstlisting} - Goal forall a b : bool, a -> b -> a /\\ b. - move=> a b Ha Hb; apply/andP. -\end{lstlisting} -changes the goal \ssrL+a /\ b+ to \ssrC{a && b} (see section \ref{ssec:goalinterp}). - -Conversely, the script -\begin{lstlisting} - Goal forall a b : bool, a /\ b -> a. - move=> a b; move/andP. -\end{lstlisting} -changes the goal \ssrL+a /\ b -> a+ into \ssrC{a && b -> a} (see section -\ref{ssec:assumpinterp}). - - -The same tactics can also be used to perform the converse -operation, changing a boolean conjunction into a logical one. The view -mechanism guesses the direction of the -transformation to be used i.e., the constructor of the \ssrC{reflect} -predicate which should be chosen. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{General mechanism for interpreting goals and assumptions} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Specializing assumptions} -\idx{move/\dots{}} - -The \ssr{} -tactic: - - \ssrC{move/(_} \ssrN[1]{term} $\dots$ \ssrN[n]{term}\ssrC{)} - -\noindent -is equivalent to the tactic: - - \ssrC{intro top; generalize (top} \ssrN[1]{term} $\dots$ \ssrN[n]{term}\ssrC{); clear top.} - -\noindent -where \ssrC{top} is a fresh name for introducing the top assumption of -the current goal. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Interpreting assumptions} -\label{sssec:hypview} -The general form of an assumption view tactic is: - -\begin{center} - \optional{\ssrC{move} {\optsep} \ssrC{case}} \ssrC{/} \ssrN[0]{term} -\end{center} - -The term \ssrN[0]{term}, called the \emph{view lemma} can be: -\begin{itemize} -\item a (term coercible to a) function; -\item a (possibly quantified) implication; -\item a (possibly quantified) double implication; -\item a (possibly quantified) instance of the \ssrC{reflect} predicate - (see section \ref{ssec:reflpred}). -\end{itemize} - -Let \ssrC{top} be the top assumption in the goal. - -There are three steps in the behaviour of an assumption view tactic: -\begin{itemize} -\item It first introduces \ssrL+top+. -\item If the type of \ssrN[0]{term} is neither a double implication nor - an instance of the \ssrC{reflect} predicate, then the tactic - automatically generalises a term of the form: - -\begin{center} - \ssrC{(}\ssrN[0]{term} \ssrN[1]{term} $\dots$ \ssrN[n]{term}\ssrC{)} -\end{center} - - where the terms \ssrN[1]{term} $\dots$ \ssrN[n]{term} instantiate the - possible quantified variables of \ssrN[0]{term}, in order for - \ssrC{(}\ssrN[0]{term} \ssrN[1]{term} $\dots$ \ssrN[n]{term} \ssrC{top)} to be well typed. -\item If the type of $\ssrN[0]{term}$ is an equivalence, or - an instance of the \ssrC{reflect} predicate, it generalises a term of - the form: - \begin{center} - (\ssrN[vh]{term} (\ssrN[0]{term} \ssrN[1]{term} $\dots$ \ssrN[n]{term})) - \end{center} - where the term \ssrN[vh]{term} inserted is called an - \emph{assumption interpretation view hint}. -\item It finally clears \ssrC{top}. -\end{itemize} -For a \ssrC{case/}\ssrN[0]{term} tactic, the generalisation step is -replaced by a case analysis step. - -\emph{View hints} are declared by the user (see section -\ref{ssec:vhints}) and are stored in the \ssrC{Hint View} database. -The proof engine automatically -detects from the shape of the top assumption \ssrC{top} and of the view -lemma $\ssrN[0]{term}$ provided to the tactic the appropriate view hint in -the database to be inserted. - -If $\ssrN[0]{term}$ is a double implication, then the view hint \ssrC{A} will -be one of the defined view hints for implication. These hints are by -default the ones present in the file {\tt ssreflect.v}: -\begin{lstlisting} - Lemma |*iffLR*| : forall P Q, (P <-> Q) -> P -> Q. -\end{lstlisting} -which transforms a double implication into the left-to-right one, or: -\begin{lstlisting} - Lemma |*iffRL*| : forall P Q, (P <-> Q) -> Q -> P. -\end{lstlisting} -which produces the converse implication. In both cases, the two first -\ssrC{Prop} arguments are implicit. - -If $\ssrN[0]{term}$ is an instance of the \ssrC{reflect} predicate, then \ssrC{A} -will be one of the defined view hints for the \ssrC{reflect} -predicate, which are by -default the ones present in the file {\tt ssrbool.v}. -These hints are not only used for choosing the appropriate direction of -the translation, but they also allow complex transformation, involving -negations. - For instance the hint: -\begin{lstlisting} - Lemma |*introN*| : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~ b. -\end{lstlisting} -makes the following script: -\begin{lstlisting} - Goal forall a b : bool, a -> b -> ~~ (a && b). - move=> a b Ha Hb. apply/andP. -\end{lstlisting} -transforms the goal into \ssrC{ \~ (a /\ b)}. -In fact\footnote{The current state of the proof shall be displayed by - the \ssrC{Show Proof} command of \Coq{} proof mode.} -this last script does not exactly use the hint \ssrC{introN}, but the -more general hint: -\begin{lstlisting} - Lemma |*introNTF*| : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c -\end{lstlisting} -The lemma \ssrL+|*introN*|+ is an instantiation of \ssrC{introNF} using - \ssrC{c := true}. - -Note that views, being part of \ssrN{i-pattern}, can be used to interpret -assertions too. For example the following script asserts \ssrC{a \&\& b} -but actually used its propositional interpretation. -\begin{lstlisting} - Lemma |*test*| (a b : bool) (pab : b && a) : b. - have /andP [pa ->] : (a && b) by rewrite andbC. -\end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsubsection*{Interpreting goals} -\idx{apply/\dots{}} - -A goal interpretation view tactic of the form: - -\begin{center} - \ssrC{apply/} \ssrN[0]{term} -\end{center} -applied to a goal \ssrC{top} is interpreted in the following way: -\begin{itemize} -\item If the type of $\ssrN[0]{term}$ is not an instance of the - \ssrC{reflect} predicate, nor an equivalence, - then the term $\ssrN[0]{term}$ is applied to the current goal \ssrC{top}, - possibly inserting implicit arguments. -\item If the type of $\ssrN[0]{term}$ is an instance of the \ssrC{reflect} - predicate or an equivalence, then -a \emph{goal interpretation view hint} can possibly be inserted, which -corresponds to the application of a term -\ssrC{($\ssrN[vh]{term}$ ($\ssrN[0]{term}$ _ $\dots$ _))} to the current -goal, possibly inserting implicit arguments. -\end{itemize} - -Like assumption interpretation view hints, goal interpretation ones -are user defined lemmas stored (see section \ref{ssec:vhints}) in the -\ssrC{Hint View} database bridging -the possible gap between the type of $\ssrN[0]{term}$ and the type of the -goal. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Interpreting equivalences} -\idx{apply/\dots{}/\dots{}} - -Equivalent boolean propositions are simply \emph{equal} boolean terms. -A special construction helps the user to prove boolean equalities by -considering them as logical double implications (between their coerced -versions), while -performing at the same time logical operations on both sides. - -The syntax of double views is: -\begin{center} - \ssrC{apply/} \ssrN[l]{term} \ssrC{/} \ssrN[r]{term} -\end{center} - -The term \ssrN[l]{term} is the view lemma applied to the left hand side of the -equality, \ssrN[r]{term} is the one applied to the right hand side. - -In this context, the identity view: -\begin{lstlisting} -Lemma |*idP*| : reflect b1 b1. -\end{lstlisting} -is useful, for example the tactic: -\begin{lstlisting} - apply/idP/idP. -\end{lstlisting} -transforms the goal -\ssrL+~~ (b1 || b2)= b3+ - into two subgoals, respectively - \ssrL+~~ (b1 || b2) -> b3+ and \\ -\ssrL+b3 -> ~~ (b1 || b2).+ - -The same goal can be decomposed in several ways, and the user may -choose the most convenient interpretation. For instance, the tactic: -\begin{lstlisting} - apply/norP/idP. -\end{lstlisting} -applied on the same goal \ssrL+~~ (b1 || b2) = b3+ generates the subgoals -\ssrL+~~ b1 /\ ~~ b2 -> b3+ and\\ -\ssrL+b3 -> ~~ b1 /\ ~~ b2+. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Declaring new \ssrC{Hint View}s}\label{ssec:vhints} -\idxC{Hint View} - -The database of hints for the view mechanism is extensible via a -dedicated vernacular command. As library {\tt ssrbool.v} already -declares a corpus of hints, this feature is probably useful only for -users who define their own logical connectives. Users can declare -their own hints following the syntax used in {\tt ssrbool.v}: - -\begin{center} - \ssrC{Hint View for} {\tac} \ssrC{/} \ssrN{ident} \optional{\ssrC{|}{\naturalnumber}} -\end{center} - - where {\tac}$\in \{$\ssrC{move, apply}$\}$, \ssrN{ident} is the -name of the lemma to be declared as a hint, and ${\naturalnumber}$ a natural -number. If \ssrL+move+ is used as {\tac}, the hint is declared for -assumption interpretation tactics, \ssrL+apply+ declares hints for goal -interpretations. -Goal interpretation view hints are declared for both simple views and -left hand side views. The optional natural number ${\naturalnumber}$ is the -number of implicit arguments to be considered for the declared hint -view lemma \ssrC{name_of_the_lemma}. - -The command: - -\begin{center} - \ssrC{Hint View for apply//} \ssrN{ident}\optional{\ssrC{|}{\naturalnumber}}. -\end{center} - -with a double slash \ssrL+//+, declares hint views for right hand sides of -double views. - - -\noindent See the files {\tt ssreflect.v} and {\tt ssrbool.v} for examples. - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Multiple views}\label{ssec:multiview} - -The hypotheses and the goal can be interpreted applying multiple views in -sequence. Both \ssrC{move} and \ssrC{apply} can be followed by an arbitrary number -of \ssrC{/}$\ssrN[i]{term}$. The main difference between the following two tactics -\begin{lstlisting} - apply/v1/v2/v3. - apply/v1; apply/v2; apply/v3. -\end{lstlisting} -is that the former applies all the views to the principal goal. -Applying a view with hypotheses generates new goals, and the second line -would apply the view \ssrC{v2} to all the goals generated by \ssrC{apply/v1}. -Note that the NO-OP intro pattern \ssrC{-} can be used to separate two -views, making the two following examples equivalent: -\begin{lstlisting} - move=> /v1; move=> /v2. - move=> /v1-/v2. -\end{lstlisting} - -The tactic \ssrC{move} can be used together with the \ssrC{in} -tactical to pass a given hypothesis to a lemma. For example, if -\ssrC{P2Q : P -> Q } and \ssrC{Q2R : Q -> R}, the following -tactic turns the hypothesis \ssrC{p : P} into \ssrC{P : R}. -\begin{lstlisting} - move/P2Q/Q2R in p. -\end{lstlisting} - -If the list of views is of length two, \ssrC{Hint View}s for interpreting -equivalences are indeed taken into account, otherwise only single -\ssrC{Hint View}s are used. -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{\ssr{} searching tool} -\idxC{Search \dots{}} - -\ssr{} proposes an extension of the \ssrC{Search} command. Its syntax is: - -\begin{center} - \ssrC{Search} \optional{\ssrN{pattern}} \optional{\optional{\ssrC{\-}} \optional{\ssrN{string}\optional{\ssrC{\%}\ssrN{key}} {\optsep} \ssrN{pattern}}}$^*$ \optional{\ssrC{in} \optional{\optional{\ssrC{\-}} \ssrN{name} }$^+$} -\end{center} - -% \begin{lstlisting} -% Search [[\~]\ssrN{string}]$^*$ [\ssrN{pattern}] [[$\ssrN[1]{pattern} \dots $ $\ssrN[n]{pattern}$]] $[[$inside$|$outside$]$ $M_1 \dots M_n$]. -% \end{lstlisting} - -% This tactic returns the list of defined constants matching the -% given criteria: -% \begin{itemize} -% \item \ssrL+[[-]\ssrN{string}]$^*$+ is an open sequence of strings, which sould -% all appear in the name of the returned constants. The optional \ssrL+-+ -% prefixes strings that are required \emph{not} to appear. -% % \item \ssrN{pattern} should be a subterm of the -% % \emph{conclusion} of the lemmas found by the command. If a lemma features -% % an occurrence -% % of this pattern only in one or several of its assumptions, it will not be -% % selected by the searching tool. -% \item -% \ssrL=[$\ssrN{pattern}^+$]= -% is a list of \ssr{} terms, which may -% include types, that are required to appear in the returned constants. -% Terms with holes should be surrounded by parentheses. -% \item $\ssrC{in}\ [[\ssrC{\-}]M]^+$ limits the search to the signature -% of open modules given in the list, but the ones preceeded by the -% $\ssrC{\-}$ flag. The -% command: -% \begin{lstlisting} -% Search in M. -% \end{lstlisting} -% is hence a way of obtaining the complete signature of the module \ssrL{M}. -% \end{itemize} -where \ssrN{name} is the name of an open module. -This command search returns the list of lemmas: -\begin{itemize} -\item whose \emph{conclusion} contains a subterm matching the optional - first \ssrN{pattern}. A $\ssrC{-}$ reverses the test, producing the list - of lemmas whose conclusion does not contain any subterm matching - the pattern; -\item whose name contains the given string. A $\ssrC{-}$ prefix reverses - the test, producing the list of lemmas whose name does not contain the - string. A string that contains symbols or -is followed by a scope \ssrN{key}, is interpreted as the constant whose -notation involves that string (e.g., \ssrL=+= for \ssrL+addn+), if this is -unambiguous; otherwise the diagnostic includes the output of the -\ssrC{Locate} vernacular command. - -\item whose statement, including assumptions and types, contains a - subterm matching the next patterns. If a pattern is prefixed by - $\ssrC{-}$, the test is reversed; -\item contained in the given list of modules, except the ones in the - modules prefixed by a $\ssrC{-}$. -\end{itemize} - -Note that: -\begin{itemize} -\item As for regular terms, patterns can feature scope - indications. For instance, the command: -\begin{lstlisting} - Search _ (_ + _)%N. -\end{lstlisting} -lists all the lemmas whose statement (conclusion or hypotheses) -involve an application of the binary operation denoted by the infix -\ssrC{+} symbol in the \ssrC{N} scope (which is \ssr{} scope for natural numbers). -\item Patterns with holes should be surrounded by parentheses. -\item Search always volunteers the expansion of the notation, avoiding the - need to execute Locate independently. Moreover, a string fragment - looks for any notation that contains fragment as - a substring. If the \ssrL+ssrbool+ library is imported, the command: -\begin{lstlisting} - Search "~~". -\end{lstlisting} -answers : -\begin{lstlisting} -"~~" is part of notation (~~ _) -In bool_scope, (~~ b) denotes negb b -negbT forall b : bool, b = false -> ~~ b -contra forall c b : bool, (c -> b) -> ~~ b -> ~~ c -introN forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~ b -\end{lstlisting} - \item A diagnostic is issued if there are different matching notations; - it is an error if all matches are partial. -\item Similarly, a diagnostic warns about multiple interpretations, and - signals an error if there is no default one. -\item The command \ssrC{Search in M.} -is a way of obtaining the complete signature of the module \ssrL{M}. -\item Strings and pattern indications can be interleaved, but the - first indication has a special status if it is a pattern, and only - filters the conclusion of lemmas: -\begin{itemize} - \item The command : - \begin{lstlisting} - Search (_ =1 _) "bij". - \end{lstlisting} -lists all the lemmas whose conclusion features a '$\ssrC{=1}$' and whose -name contains the string \verb+bij+. -\item The command : - \begin{lstlisting} - Search "bij" (_ =1 _). - \end{lstlisting} -lists all the lemmas whose statement, including hypotheses, features a -'$\ssrC{=1}$' and whose name contains the string \verb+bij+. - -\end{itemize} - -\end{itemize} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Synopsis and Index} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{Parameters} - -\begin{minipage}[c]{\textwidth}\renewcommand{\footnoterule}{} -\begin{longtable}{lcl} -\ssrN{d-tactic} && one of the - \ssrC{elim}, \ssrC{case}, \ssrC{congr}, \ssrC{apply}, \ssrC{exact} - and \ssrC{move} \ssr{} tactics \\ -\ssrN{fix-body} && standard \Coq{} \textit{fix\_body}\\ -\ssrN{ident} && standard \Coq{} identifier\\ -\ssrN{int} && integer literal \\ -\ssrN{key} && notation scope\\ -\ssrN{name} && module name\\ -${\naturalnumber}$ && \ssrN{int} or Ltac variable denoting a standard \Coq{} numeral\footnote{The name of this Ltac variable should not be the name of a tactic which can be followed by a bracket - \ssrL+[+, like \ssrL+do+, \ssrL+ have+,\dots}\\ -\ssrN{pattern} && synonym for {\term}\\ -\ssrN{string} && standard \Coq{} string\\ -{\tac} && standard \Coq{} tactic or \ssr{} tactic\\ -{\term} & \hspace{1cm} & Gallina term, possibly containing wildcards\\ -%\ssrN{view} && global constant\\ -\end{longtable} -\end{minipage} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{Items and switches} - -\begin{longtable}{lclr} -\ssrN{binder} & {\ident} {\optsep} \ssrC{(} {\ident} \optional{\ssrC{:} {\term} } \ssrC{)} & binder& p. \pageref{ssec:pose}\\ -\\ -\ssrN{clear-switch} & \ssrC{\{} {\ident}$^+$ \ssrC{\}} & clear switch & p. \pageref{ssec:discharge}\\ -\\ -\ssrN{c-pattern} & \optional{{\term} \ssrC{in} {\optsep} {\term} \ssrC{as}} {\ident} \ssrC{in} {\term} & context pattern & p. \pageref{ssec:rewp} \\ -\\ -\ssrN{d-item} & \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} \optional{{\term} {\optsep} \ssrC{(}\ssrN{c-pattern}\ssrC{)}} & discharge item & p. \pageref{ssec:discharge}\\ -\\ -\ssrN{gen-item} & \optional{\ssrC{@}}{\ident} {\optsep} \ssrC{(}{\ident}\ssrC{)} {\optsep} \ssrC{(}\optional{\ssrC{@}}{\ident} \ssrC{:=} \ssrN{c-pattern}\ssrC{)} & generalization item & p. \pageref{ssec:struct}\\ -\\ -\ssrN{i-pattern} & {\ident} {\optsep} \ssrC{_} {\optsep} \ssrC{?} {\optsep} \ssrC{*} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{->} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{<-} {\optsep} & intro pattern & p. \pageref{ssec:intro}\\ -& \ssrC{[} \ssrN{i-item}$^*$ \ssrC{|} $\dots$ \ssrC{|} \ssrN{i-item}$^*$ \ssrC{]} {\optsep} \ssrC{-} {\optsep} \ssrC{[:} {\ident}$^+$\ssrC{]} &\\ -\\ -\ssrN{i-item} & \ssrN{clear-switch} {\optsep} \ssrN{s-item} {\optsep} \ssrN{i-pattern} {\optsep} \ssrC{/}{\term} & intro item & p. \pageref{ssec:intro}\\ -\\ -\ssrN{int-mult} & \optional{{\naturalnumber}} \ssrN{mult-mark} & multiplier & p. \pageref{ssec:iter}\\ -\\ -\ssrN{occ-switch} & \ssrC{\{} \optional{\ssrC{+} {\optsep} \ssrC{-}} {\naturalnumber}$^*$\ssrC{\}} & occur. switch & p. \pageref{sssec:occselect}\\ -\\ -\ssrN{mult} & \optional{{\naturalnumber}} \ssrN{mult-mark} & multiplier & p. \pageref{ssec:iter}\\ -\\ -\ssrN{mult-mark} & \ssrC{?} {\optsep} \ssrC{!} & multiplier mark & p. \pageref{ssec:iter}\\ -\\ -\ssrN{r-item} & \optional{\ssrC{/}} {\term} {\optsep} \ssrN{s-item} & rewrite item & p. \pageref{ssec:extrw}\\ -\\ -\ssrN{r-prefix} & \optional{\ssrC{-}} \optional{\ssrN{int-mult}} \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} \optional{\ssrC{[}\ssrN{r-pattern}\ssrC{]}} & rewrite prefix & p. \pageref{ssec:extrw}\\ -\\ -\ssrN{r-pattern} & {\term} {\optsep} \ssrN{c-pattern} {\optsep} \ssrC{in} \optional{{\ident} \ssrC{in}} {\term} & rewrite pattern & p. \pageref{ssec:extrw}\\ -\\ -\ssrN{r-step} & \optional{\ssrN{r-prefix}}\ssrN{r-item} & rewrite step & p. \pageref{ssec:extrw}\\ -\\ -\ssrN{s-item} & \ssrC{/=} {\optsep} \ssrC{//} {\optsep} \ssrC{//=} & simplify switch & p. \pageref{ssec:intro}\\ -\\ -\end{longtable} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{Tactics} -\emph{Note}: \ssrC{without loss} and \ssrC{suffices} are synonyms for \ssrC{wlog} and -\ssrC{suff} respectively. - -\begin{longtable}{llr} -\ssrC{move} & \textcolor{dkblue}{\texttt{idtac}} or \ssrC{hnf}& p. \pageref{ssec:profstack} \\ -\ssrC{apply} & application & p. \pageref{ssec:basictac}\\ -\ssrC{exact} &&\\ -\ssrC{abstract} && p. \pageref{ssec:abstract}, \pageref{sec:havetransparent}\\ -\\ -\ssrC{elim} & induction & p. \pageref{ssec:basictac}\\ -\ssrC{case} & case analysis & p. \pageref{ssec:basictac}\\ -\\ -\ssrC{rewrite} \ssrN{rstep}$^+$ & rewrite& p. \pageref{ssec:extrw}\\ -\\ -\ssrC{have} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} \optional{\ssrN{s-item} {\optsep} \ssrN{binder}$^+$} \optional{\ssrC{:} {\term}} \ssrC{:=} {\term} & forward & p. \pageref{ssec:struct}\\ -\ssrC{have} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} \optional{\ssrN{s-item}{\optsep} \ssrN{binder}$^+$} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & chaining & \\ -\ssrC{have suff} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-pattern}} \optional{\ssrC{:} {\term}} \ssrC{:=} {\term} & & \\ -\ssrC{have suff} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-pattern}} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & & \\ -\ssrC{gen have} \optional{{\ident}\ssrC{,}} \optional{\ssrN{i-pattern}} \ssrC{:} \ssrN{gen-item}$^+$ \ssrC{/} {\term} \optional{\ssrC{by} {\tac}} & & \\ -\\ -\ssrC{wlog} \optional{\ssrC{suff}} \optional{\ssrN{i-item}} \ssrC{:} \optional{\ssrN{gen-item}{\optsep} \ssrN{clear-switch}}$^*$ \ssrC{/} {\term} & specializing & p. \pageref{ssec:struct} \\ -\\ -\ssrC{suff} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} \optional{\ssrN{binder}$^+$} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & backchaining & p. \pageref{ssec:struct}\\ -\ssrC{suff} \optional{\ssrC{have}} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-pattern}} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & & \\ -\\ -\ssrC{pose} {\ident} \ssrC{:=} {\term} & local definition& p. \pageref{ssec:pose}\\ -\ssrC{pose} {\ident} \ssrN{binder}$^+$ \ssrC{:=} {\term} & \rlap{local function definition}& \\ -\ssrC{pose fix} \ssrN{fix-body} & \rlap{local fix definition} & \\ -\ssrC{pose cofix} \ssrN{fix-body} & \rlap{local cofix definition} & \\ -\\ -\ssrC{set} {\ident} \optional{\ssrC{:} {\term}} \ssrC{:=} \optional{\ssrN{occ-switch}} \optional{{\term}{\optsep} \ssrC{(}\ssrN{c-pattern}\ssrC{)}} & abbreviation&p. \pageref{ssec:set}\\ -\\ -\ssrC{unlock} \optional{\ssrN{r-prefix}]{\ident}}$^*$ & unlock & p. \pageref{ssec:lock}\\ -\\ -\ssrC{congr} \optional{\naturalnumber} {\term} & congruence& p. \pageref{ssec:congr}\\ -\end{longtable} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{Tacticals} - -\begin{longtable}{lclr} -\ssrN{d-tactic} \optional{\ident} \ssrC{:} \ssrN{d-item}$^{+}$ \optional{\ssrN{clear-switch}} & & discharge & p. \pageref{ssec:discharge}\\ -\\ -{\tac} \ssrC{=>} \ssrN{i-item}$^+$ && introduction & p. \pageref{ssec:intro}\\ -\\ -{\tac} \ssrC{in} \optional{\ssrN{gen-item} {\optsep} \ssrN{clear-switch}}$^+$ \optional{\ssrC{*}} && localization & p. \pageref{ssec:gloc}\\ -\\ -\ssrC{do} \optional{\ssrN{mult}} \ssrC{[} \nelist{\tac}{|} \ssrC{]}&& iteration & p. \pageref{ssec:iter}\\ -\ssrC{do} \ssrN{mult} {\tac} &&& \\ -\\ -{\tac} \ssrC{ ; first} \optional{\naturalnumber} \ssrC{[}\nelist{\tac}{|}\ssrC{]} && selector & p. \pageref{ssec:select}\\ -{\tac} \ssrC{ ; last} \optional{\naturalnumber} \ssrC{[}\nelist{\tac}{|}\ssrC{]} \\ -{\tac} \ssrC{ ; first} \optional{\naturalnumber} \ssrC{last} && subgoals & p. \pageref{ssec:select}\\ -{\tac} \ssrC{; last} \optional{\naturalnumber} \ssrC{first} && rotation & \\ -\\ -\ssrC{by [} \nelist{\tac}{|} \ssrC{]} && closing & p. \pageref{ssec:termin}\\ -\ssrC{by []} \\ -\ssrC{by} {\tac} \\ -\end{longtable} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection*{Commands} -\begin{longtable}{lclr} -\ssrL+Hint View for+ \optional{\ssrL+move+ {\it |} \ssrL+apply+} {\tt /} {\ident} \optional{{\tt|} {\naturalnumber}} && view hint -declaration & p. \pageref{ssec:vhints}\\ -\\ -\ssrL+Hint View for apply//+ {\ident} \optional{{\tt|}{\naturalnumber}} && right hand side double - & p. \pageref{ssec:vhints}\\ -&& view hint declaration &\\ -\\ -%\ssrL+Import Prenex Implicits+ && enable prenex implicits & -%p. \pageref{ssec:parampoly}\\ -%\\ -\ssrL+Prenex Implicits+ {\ident}$^+$ & \hspace{.6cm} & prenex implicits decl. - & p. \pageref{ssec:parampoly}\\ - -\end{longtable} - -\iffalse - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Changes} - -\subsection{\ssr{} version 1.3} -All changes are retrocompatible extensions but for: -\begin{itemize} -\item Occurrences in the type family switch now refer only to the goal, while - before they used to refer also to the types in the abstractions of the - predicate used by the eliminator. This bug used to affect lemmas like - \ssrC{boolP}. See the relative comments in \ssrC{ssrbool.v}. -\item Clear switches can only mention existing hypothesis and - otherwise fail. This can in particular affect intro patterns - simultaneously applied to several goals. - % commit: 2686 -\item A bug in the \ssrC{rewrite} tactic allowed to - instantiate existential metavariables occurring in the goal. - This is not the case any longer (see section~\ref{ssec:rewcaveats}). -\item The \ssrC{fold} and \ssrC{unfold} \ssrN{r-items} for \ssrC{rewrite} used to - fail silently when used in combination with a \ssrN{r-pattern} matching no - goal subterm. They now fail. The old behavior can be obtained using - the \ssrC{?} multiplier (see section~\ref{ssec:extrw}). -\item \Coq{} 8.2 users with a statically linked toplevel must comment out the\\ - \ssrC{Declare ML Module "ssreflect".}\\ - line at the beginning of \ssrC{ssreflect.v} to compile the 1.3 library. -\end{itemize} -New features: -\begin{itemize} -\item Contextual \ssrC{rewrite} patterns. - The context surrounding the redex can now be used to specify which - redex occurrences should be rewritten (see section~\ref{ssec:rewp}).\\ - \ssrC{rewrite [in X in _ = X]addnC.} - % commit: 2690, 2689, 2718, 2733 -\item Proof irrelevant interpretation of goals with existential metavariables. - Goals containing an existential metavariable of sort \ssrC{Prop} are - generalized over it, and a new goal for the missing subproof is - generated (see page~\pageref{sssec:apply} and - section~\ref{ssec:rewcaveats}).\\ - \ssrC{apply: (ex_intro _ (@Ordinal _ y _)).}\\ - \ssrC{rewrite insubT.} - % commit: 2553, 2544, 2543, 2733 -\item Views are now part of \ssrN{i-pattern} and can thus be used - inside intro patterns (see section~\ref{ssec:intro}).\\ - \ssrC{move=> a b /andP [Ha Hb].} - % commit: 2720 -\item Multiple views for \ssrC{move}, \ssrC{move $\dots$ in} and \ssrC{apply} - (see section~\ref{ssec:multiview}).\\ - \ssrC{move/v1/v2/v3.}\\ - \ssrC{move/v1/v2/v3 in H.}\\ - \ssrC{apply/v1/v2/v3.} - % commit: 2720 -\item \ssrC{have} and \ssrC{suff} idiom with view (see section~\ref{sssec:hypview}). -\begin{lstlisting} - Lemma |*test*| (a b : bool) (pab : a && b) : b. - have {pab} /= /andP [pa ->] // : true && (a && b) := pab. -\end{lstlisting} - % commit: 2726 -\item \ssrC{have suff}, \ssrC{suff have} and \ssrC{wlog suff} forward reasoning - tactics (see section~\ref{ssec:struct}).\\ - \ssrC{have suff H : P.} - % commit: 2633 -\item Binders support in \ssrC{have} (see section~\ref{sssec:have}).\\ - \ssrC{have H x y (r : R x y) : P x -> Q y.} - % commit: 2633 -\item Deferred clear switches. Clears are deferred to the end of the - intro pattern. In the meanwhile, cleared variables are still - part of the context, thus the goal can mention them, but are - renamed to non accessible dummy names (see section~\ref{ssec:intro}).\\ - \ssrC{suff: G \\x H = K; first case/dprodP=> \{G H\} [[G H -> -> defK]].} - % commit: 2660 -\item Relaxed alternation condition in intro patterns. The - \ssrN{i-item} grammar rule is simplified (see section~\ref{ssec:intro}).\\ - \ssrC{move=> a \{H\} /= \{H1\} // b c /= \{H2\}.} - % commit: 2713 -\item Occurrence selection for \ssrC{->} and \ssrC{<-} intro pattern - (see section~\ref{ssec:intro}).\\ - \ssrC{move=> a b H \{2\}->.} - % commit: 2714 -\item Modifiers for the discharging '\ssrC{:}' and \ssrC{in} tactical to override - the default behavior when dealing with local definitions (let-in): - \ssrC{@f} forces the body of \ssrC{f} to be kept, \ssrC{(f)} forces the body of - \ssrC{f} to be dropped (see sections~\ref{ssec:discharge} - and~\ref{ssec:gloc}).\\ - \ssrC{move: x y @f z.}\\ - \ssrC{rewrite rule in (f) $\;\;$H.} - %commit: 2659, 2710 -\item Type family switch in \ssrC{elim} and \ssrC{case} - can contain patterns with occurrence switch - (see section~\ref{ssec:typefam}).\\ - \ssrC{case: \{2\}(_ == x) / eqP.} - % commit: 2593, 2598, 2539, 2538, 2527, 2529 -\item Generic second order predicate support for \ssrC{elim} - (see section~\ref{sec:views}).\\ - \ssrC{elim/big\_prop: _} - % commit: 2767 -\item The \ssrC{congr} tactic now also works on products (see - section~\ref{ssec:congr}). -\begin{lstlisting} - Lemma |*test*| x (H : P x) : P y. - congr (P _): H. -\end{lstlisting} - % commit: 2608 -\item Selectors now support Ltac variables - (see section~\ref{ssec:select}).\\ - \ssrC{let n := 3 in tac; first n last.} - % commit: 2725 -\item Deprecated use of \ssrC{Import Prenex Implicits} directive. - It must be replaced with the \Coq{} \ssrC{Unset Printing - Implicit Defensive} vernacular command. -\item New synonym \ssrC{Canonical} for \ssrC{Canonical Structure}. -\end{itemize} -\subsection{\ssr{} version 1.4} -New features: -\begin{itemize} -\item User definable recurrent contexts (see section~\ref{ssec:rewp}).\\ - \ssrC{Notation RHS := (X in _ = X)\%pattern} -\item Contextual patterns in - \ssrC{set} and `\ssrC{:}' (see section~\ref{ssec:rewp}).\\ - \ssrC{set t := (a + _ in RHS)} -\item NO-OP intro pattern (see section~\ref{ssec:intro}).\\ - \ssrC{move=> /eqP-H /fooP-/barP} -\item \ssrC{if $\ {\term}\ $ isn't $\ \ssrN{pattern}\ $ then $\ {\term}\ $ - else $\ {\term}\ $} notation (see section~\ref{ssec:patcond}).\\ - \ssrC{if x isn't Some y then simple else complex y} -\end{itemize} -\subsection{\ssr{} version 1.5} -Incompatibilities: -\begin{itemize} -\item The \ssrC{have} tactic now performs type classes resolution. The old - behavior can be restored with \ssrC{Set SsrHave NoTCResolution} -\end{itemize} -Fixes: -\begin{itemize} -\item The \ssrC{let foo := type of t in} syntax of standard \ssrC{Ltac} has - been made compatible with \ssr{} and can be freely used even if - the \ssr{} plugin is loaded -\end{itemize} -New features: -\begin{itemize} -\item Generalizations supported in have (see section~\ref{ssec:struct}).\\ - \ssrC{generally have hx2px, pa : a ha / P a.} -\item Renaming and patterns in wlog (see section~\ref{ssec:struct} and - page \pageref{par:advancedgen}).\\ - \ssrC{wlog H : (n := m)$\;$ (x := m + _)$\;$ / T x}.\\ - \ssrC{wlog H : (n := m)$\;$ (@ldef := secdef m)$\;$ / T x}. -\item Renaming, patterns and clear switches in \ssrC{in} - tactical (see section~\ref{ssec:gloc}).\\ - \ssrC{$\dots$ in H1 \{H2\} (n := m).} -\item Handling of type classes in \ssrC{have} - (see page~\pageref{ssec:havetcresolution}).\\ - \ssrC{have foo : ty. (* TC inference for ty *)}\\ - \ssrC{have foo : ty := . (* no TC inference for ty *)}\\ - \ssrC{have foo : ty := t. (* no TC inference for ty and t *)}\\ - \ssrC{have foo := t. (* no TC inference for t *)} -\item Transparent flag for \ssrC{have} to generate a \ssrC{let in} context entry - (see page~\pageref{sec:havetransparent}).\\ - \ssrC{have @i : 'I\_n by apply: (Sub m); auto.} -\item Intro pattern \ssrC{[: foo bar ]} to create abstract variables - (see page~\pageref{ssec:introabstract}). -\item Tactic \ssrC{abstract:} to assign an abstract variable - (see page~\pageref{ssec:abstract}).\\ - \ssrC{have [: blurb ] @i : 'I\_n by apply: (Sub m); abstract: blurb; auto.}\\ - \ssrC{have [: blurb ] i : 'I\_n := Sub m blurb; first by auto.} - -\end{itemize} - -\fi |