From 9ea8867a0fa8f2a52df102732fdc1a931c659826 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2015 22:12:25 +0200 Subject: Proof using: let-in policy, optional auto-clear, forward closure* - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using . - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. --- doc/refman/RefMan-pro.tex | 30 ++++++++++++++++++++++++------ 1 file changed, 24 insertions(+), 6 deletions(-) (limited to 'doc/refman/RefMan-pro.tex') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 7af87a399a..5dbf315535 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -157,6 +157,14 @@ in Section~\ref{ProofWith}. Use only section variables occurring in the statement. +\variant {\tt Proof using Type*.} + + The {\tt *} operator computes the forward transitive closure. + E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is + in {\tt p*} since {\tt p} occurs in the type of {\tt H}. + {\tt Type* } is the forward transitive closure of the entire set of + section variables occurring in the statement. + \variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}. @@ -164,14 +172,18 @@ in Section~\ref{ProofWith}. \variant {\tt Proof using } {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .} \variant {\tt Proof using } {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .} \variant {\tt Proof using } {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} +\variant {\tt Proof using } {\emph collection$_1$}{\tt* .} - Use section variables being in the set union or set difference of the two - colelctions. See Section~\ref{Collection} to know how to form a named + Use section variables being, respectively, in the set union, set difference, + set complement, set forward transitive closure. + See Section~\ref{Collection} to know how to form a named collection. + The {\tt *} operator binds stronger than {\tt +} and {\tt -}. \subsubsection{{\tt Proof using} options} -\comindex{Default Proof Using} -\comindex{Suggest Proof Using} +\optindex{Default Proof Using} +\optindex{Suggest Proof Using} +\optindex{Proof Using Clear Unused} The following options modify the behavior of {\tt Proof using}. @@ -186,11 +198,17 @@ The following options modify the behavior of {\tt Proof using}. When {\tt Qed} is performed, suggest a {\tt using} annotation if the user did not provide one. +\variant{\tt Unset Proof Using Clear Unused.} + + When {\tt Proof using a} all section variables but for {\tt a} and + the variables used in the type of {\tt a} are cleared. + This option can be used to turn off this behavior. + \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}} \comindex{Collection}\label{Collection} The command {\tt Collection} can be used to name a set of section hypotheses, -with the purpose of making {\tt Proof using} annotations more compat. +with the purpose of making {\tt Proof using} annotations more compact. \variant {\tt Collection Some := x y z.} @@ -209,7 +227,7 @@ with the purpose of making {\tt Proof using} annotations more compat. \variant {\tt Collection Many := Fewer - (x y).} Define the collection named "Many" containing the set difference - of "Fewer" and the unamed collection {\tt x y}. + of "Fewer" and the unnamed collection {\tt x y}. \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}} -- cgit v1.2.3 From cd440dbd43a632cf8f445a80d034f36e4235c63e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 10 Oct 2015 13:02:56 +0200 Subject: Fix a few latex errors in documentation of Proof Using (e.g. \tt*). --- doc/refman/RefMan-pro.tex | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'doc/refman/RefMan-pro.tex') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 5dbf315535..481afa8f87 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -165,14 +165,17 @@ in Section~\ref{ProofWith}. {\tt Type* } is the forward transitive closure of the entire set of section variables occurring in the statement. -\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} +\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$ ).} Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}. -\variant {\tt Proof using } {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .} -\variant {\tt Proof using } {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .} -\variant {\tt Proof using } {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} -\variant {\tt Proof using } {\emph collection$_1$}{\tt* .} +\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .} + +\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .} + +\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).} + +\variant {\tt Proof using \nterm{collection} * .} Use section variables being, respectively, in the set union, set difference, set complement, set forward transitive closure. -- cgit v1.2.3 From 33742251e62a49c7996b96ca7077cf985627d14b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Dec 2015 23:15:02 +0100 Subject: Proof using: do not clear unused section hyps automatically The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account. --- doc/refman/RefMan-pro.tex | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'doc/refman/RefMan-pro.tex') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 481afa8f87..ed1b79e56e 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -186,7 +186,7 @@ in Section~\ref{ProofWith}. \subsubsection{{\tt Proof using} options} \optindex{Default Proof Using} \optindex{Suggest Proof Using} -\optindex{Proof Using Clear Unused} +% \optindex{Proof Using Clear Unused} The following options modify the behavior of {\tt Proof using}. @@ -201,12 +201,12 @@ The following options modify the behavior of {\tt Proof using}. When {\tt Qed} is performed, suggest a {\tt using} annotation if the user did not provide one. -\variant{\tt Unset Proof Using Clear Unused.} - - When {\tt Proof using a} all section variables but for {\tt a} and - the variables used in the type of {\tt a} are cleared. - This option can be used to turn off this behavior. - +% \variant{\tt Unset Proof Using Clear Unused.} +% +% When {\tt Proof using a} all section variables but for {\tt a} and +% the variables used in the type of {\tt a} are cleared. +% This option can be used to turn off this behavior. +% \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}} \comindex{Collection}\label{Collection} -- cgit v1.2.3 From 1af878e0dac2198ae487d0b37438520772f28350 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Jan 2016 17:07:32 +0100 Subject: Documenting Set Bullet Behavior. This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. --- doc/refman/RefMan-pro.tex | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'doc/refman/RefMan-pro.tex') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index ed1b79e56e..c37367de5b 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -407,6 +407,19 @@ Proof. \end{ErrMsgs} +The bullet behavior can be controlled by the following commands. + +\begin{quote} +Set Bullet Behavior "None". +\end{quote} + +This makes bullets inactive. + +\begin{quote} +Set Bullet Behavior "Strict Subproofs". +\end{quote} + +This makes bullets active (this is the default behavior). \section{Requesting information} -- cgit v1.2.3