technical.tex 22.7 KB
 MARCHE Claude committed Apr 10, 2012 1 \chapter{Technical Informations}  Guillaume Melquiond committed Oct 02, 2017 2 %HEVEA\cutname{technical.html}  MARCHE Claude committed Apr 10, 2012 3 4 5 6 7 8 9  \section{Structure of Session Files} The proof session state is stored in an XML file named \texttt{\textsl{}/why3session.xml}, where \texttt{\textsl{}} is the directory of the project. The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.  10 \lstinputlisting{../share/why3session.dtd}  MARCHE Claude committed Apr 10, 2012 11 12   Guillaume Melquiond committed Jun 26, 2014 13 \section{Prover Detection}  MARCHE Claude committed Apr 12, 2012 14 15 \label{sec:proverdetecttiondata}  Guillaume Melquiond committed May 24, 2016 16 The data configuration for the automatic detection of  MARCHE Claude committed Apr 12, 2012 17 18 installed provers is stored in the file \texttt{provers-detection-data.conf} typically located in directory  Guillaume Melquiond committed May 24, 2016 19 \verb|/usr/local/share/why3| after installation. The content of this  MARCHE Claude committed Apr 12, 2012 20 file is reproduced below.  Guillaume Melquiond committed Oct 29, 2012 21 22 23 %BEGIN LATEX {\footnotesize %END LATEX  Guillaume Melquiond committed Jun 20, 2018 24 \lstinputlisting[language={},morecomment={[l]\#},morestring={[b]"}]{../share/provers-detection-data.conf}  Guillaume Melquiond committed Oct 29, 2012 25 26 27 %BEGIN LATEX } %END LATEX  MARCHE Claude committed Apr 10, 2012 28   Guillaume Melquiond committed Jun 26, 2014 29 \section{The \texttt{why3.conf} Configuration File}  MARCHE Claude committed Apr 10, 2012 30 31 32 \label{sec:whyconffile} \index{why3.conf@\texttt{why3.conf}}\index{configuration file}  Guillaume Melquiond committed Jun 26, 2014 33 34 35 36 37 38 39 40 41 42 43 44 One can use a custom configuration file. The \why tools look for it in the following order: \begin{enumerate} \item the file specified by the \texttt{-C} or \texttt{-{}-config} options, \item the file specified by the environment variable \texttt{WHY3CONFIG} if set, \item the file \texttt{\$HOME/.why3.conf} (\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of local installation, \texttt{why3.conf} in the top directory of \why sources. \end{enumerate} If none of these files exist, a built-in default configuration is used.  MARCHE Claude committed Apr 10, 2012 45 A section begins with a header inside square brackets and ends at the  Guillaume Melquiond committed Jun 20, 2018 46 47 48 beginning of the next section. The header of a section can be a single identifier, \eg \texttt{[main]}, or it can be composed by a family name and a single family argument, \eg \texttt{[prover alt-ergo]}.  MARCHE Claude committed Apr 10, 2012 49   Guillaume Melquiond committed Feb 01, 2013 50 Sections contain associations \texttt{key=value}. A value is either  Guillaume Melquiond committed Jun 26, 2014 51 52 53 an integer (\eg \texttt{-555}), a boolean (\texttt{true}, \texttt{false}), or a string (\eg \texttt{"emacs"}). Some specific keys can be attributed multiple values and are  Guillaume Melquiond committed Feb 01, 2013 54 thus allowed to occur several times inside a given section. In that  Guillaume Melquiond committed Jun 20, 2018 55 case, the relative order of these associations matters.  MARCHE Claude committed Apr 10, 2012 56   Guillaume Melquiond committed Jun 26, 2014 57 \section{Drivers for External Provers}  MARCHE Claude committed Apr 10, 2012 58 59 \label{sec:drivers}  Guillaume Melquiond committed Jun 26, 2014 60 Drivers for external provers are readable files from directory  MARCHE Claude committed Apr 10, 2012 61 62 63 64 65 66 67 68 69 \texttt{drivers}. Experimented users can modify them to change the way the external provers are called, in particular which transformations are applied to goals. [TO BE COMPLETED LATER] \section{Transformations} \label{sec:transformations}  MARCHE Claude committed Sep 16, 2014 70 71 72 73 74 This section documents the available transformations. We first describe the most important ones, and then we provide a quick documentation of the others, first the non-splitting ones, \eg those which produce exactly one goal as result, and the others which produce any number of goals.  MARCHE Claude committed Apr 10, 2012 75 76 77 78 79 80  Notice that the set of available transformations in your own installation is given by \begin{verbatim} why3 --list-transforms \end{verbatim}  Guillaume Melquiond committed Jun 26, 2014 81 \index{list-transforms@\verb+--list-transforms+}  MARCHE Claude committed Apr 10, 2012 82   MARCHE Claude committed Sep 16, 2014 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 \subsection{Inlining definitions} Those transformations generally amount to replace some applications of function or predicate symbols with its definition. \begin{description} \item[inline\_trivial] expands and removes definitions of the form \begin{whycode} function f x_1 ... x_n = (g e_1 ... e_k) predicate p x_1 ... x_n = (q e_1 ... e_k) \end{whycode} when each $e_i$ is either a ground term or one of the $x_j$, and each $x_1 \dots x_n$ occurs at most once in all the $e_i$.  Guillaume Melquiond committed Sep 16, 2014 98 \index{inline-trivial@\verb+inline_trivial+}  MARCHE Claude committed Sep 16, 2014 99 100 101  \item[inline\_goal] expands all outermost symbols of the goal that have a non-recursive definition.  Guillaume Melquiond committed Sep 16, 2014 102 \index{inline-goal@\verb+inline_goal+}  MARCHE Claude committed Sep 16, 2014 103 104 105  \item[inline\_all] expands all non-recursive definitions.  Guillaume Melquiond committed Sep 16, 2014 106 \index{inline-all@\verb+inline_all+}  MARCHE Claude committed Sep 16, 2014 107 108 109 110 111 112  \end{description} \subsection{Induction Transformations}  Jean-Christophe Filliatre committed Sep 17, 2014 113 \begin{description}  Guillaume Melquiond committed May 24, 2016 114 \item[induction\_ty\_lex]  Jean-Christophe Filliatre committed Sep 17, 2014 115  \index{induction-ty-lex@\verb+induction_ty_lex+}  Guillaume Melquiond committed May 24, 2016 116  performs structural, lexicographic induction on  Jean-Christophe Filliatre committed Sep 17, 2014 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132  goals involving universally quantified variables of algebraic data types, such as lists, trees, etc. For instance, it transforms the following goal \begin{whycode} goal G: forall l: list 'a. length l >= 0 \end{whycode} into this one: \begin{whycode} goal G : forall l:list 'a. match l with | Nil -> length l >= 0 | Cons a l1 -> length l1 >= 0 -> length l >= 0 end \end{whycode} When induction can be applied to several variables, the transformation  Guillaume Melquiond committed Jun 20, 2018 133  picks one heuristically. The \verb|[@induction]| attribute can be used to  MARCHE Claude committed Sep 17, 2014 134  force induction over one particular variable, \eg with  Jean-Christophe Filliatre committed Sep 17, 2014 135 \begin{whycode}  Guillaume Melquiond committed Jun 20, 2018 136 goal G: forall l1 [@induction] l2 l3: list 'a.  Jean-Christophe Filliatre committed Sep 17, 2014 137 138  l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 \end{whycode}  Guillaume Melquiond committed Jun 20, 2018 139 induction will be applied on \verb|l1|. If this attribute is attached to  MARCHE Claude committed Sep 17, 2014 140 141 several variables, a lexicographic induction is performed on these variables, from left to right.  MARCHE Claude committed Sep 16, 2014 142   MARCHE Claude committed Sep 17, 2014 143 %\item[] Induction on inductive predicates.  MARCHE Claude committed Sep 16, 2014 144   MARCHE Claude committed Sep 17, 2014 145 146 147 %[TO BE COMPLETED] % TODO: implement also induction on int !  MARCHE Claude committed Sep 16, 2014 148   Jean-Christophe Filliatre committed Sep 17, 2014 149 \end{description}  MARCHE Claude committed Sep 16, 2014 150 151 152  \subsection{Simplification by Computation}  Jean-Christophe Filliatre committed Sep 17, 2014 153 These transformations simplify the goal by applying several kinds of  MARCHE Claude committed Sep 17, 2014 154 155 156 157 simplification, described below. The transformations differ only by the kind of rules they apply: \begin{description} \item[compute\_in\_goal] aggressively applies all known  Guillaume Melquiond committed May 24, 2016 158  computation/simplification rules.  MARCHE Claude committed Sep 17, 2014 159  \index{compute-in-goal@\verb+compute_in_goal+}  Martin Clochard committed Sep 16, 2014 160   MARCHE Claude committed Sep 17, 2014 161 \item[compute\_specified] performs rewriting using only built-in  Guillaume Melquiond committed May 24, 2016 162  operators and user-provided rules.  MARCHE Claude committed Sep 17, 2014 163 164  \index{compute-specified@\verb+compute_specified+} \end{description}  Martin Clochard committed Sep 16, 2014 165   MARCHE Claude committed Sep 17, 2014 166 The kinds of simplification are as follows.  MARCHE Claude committed Sep 16, 2014 167 168 169 170 \begin{itemize} \item Computations with built-in symbols, \eg operations on integers, when applied to explicit constants, are evaluated. This includes evaluation of equality when a decision can be made (on integer  Martin Clochard committed Sep 16, 2014 171 172 173 174 175  constants, on constructors of algebraic data types), Boolean evaluation, simplification of pattern-matching/conditional expression, extraction of record fields, and beta-reduction. At best, these computations reduce the goal to \verb|true| and the transformations thus does not produce any sub-goal.  Guillaume Melquiond committed Sep 16, 2014 176  For example, a goal  Martin Clochard committed Sep 16, 2014 177  like \verb|6*7=42| is solved by those transformations.  Guillaume Melquiond committed May 24, 2016 178 179 \item Unfolding of definitions, as done by \verb|inline_goal|. Transformation \verb|compute_in_goal| unfolds all definitions, including recursive ones.  Martin Clochard committed Sep 16, 2014 180 181  For \verb|compute_specified|, the user can enable unfolding of a specific logic symbol by attaching the meta \verb|rewrite_def| to the symbol.  MARCHE Claude committed Sep 16, 2014 182 183 184 185 186 \begin{whycode} function sqr (x:int) : int = x * x meta "rewrite_def" function sqr \end{whycode} \item Rewriting using axioms or lemmas declared as rewrite rules. When  Guillaume Melquiond committed Sep 16, 2014 187  an axiom (or a lemma) has one of the forms  MARCHE Claude committed Sep 16, 2014 188 \begin{whycode}  Guillaume Melquiond committed Sep 16, 2014 189 axiom a: forall ... t1 = t2  MARCHE Claude committed Sep 16, 2014 190 191 192 \end{whycode} or \begin{whycode}  Guillaume Melquiond committed Sep 16, 2014 193 axiom a: forall ... f1 <-> f2  MARCHE Claude committed Sep 16, 2014 194 195 196 \end{whycode} then the user can declare \begin{whycode}  197 meta "rewrite" prop a  MARCHE Claude committed Sep 16, 2014 198 \end{whycode}  MARCHE Claude committed Sep 17, 2014 199  to turn this axiom into a rewrite rule. Rewriting is always done  MARCHE Claude committed Sep 16, 2014 200 201  from left to right. Beware that there is no check for termination nor for confluence of the set of rewrite rules declared.  MARCHE Claude committed Sep 17, 2014 202 \end{itemize}  MARCHE Claude committed Dec 05, 2016 203 Instead of using a meta, it is possible to declare an axiom as a  Guillaume Melquiond committed Jun 20, 2018 204 rewrite rule by adding the \verb|[@rewrite]| attribute on the axiom name or  MARCHE Claude committed Dec 05, 2016 205 206 on the axiom itself, e.g.: \begin{whycode}  Guillaume Melquiond committed Jun 20, 2018 207 208 axiom a [@rewrite]: forall ... t1 = t2 lemma b: [@rewrite] forall ... f1 <-> f2  MARCHE Claude committed Dec 05, 2016 209 210 211 \end{whycode} The second form allows some form of local rewriting, e.g. \begin{whycode}  Guillaume Melquiond committed Jun 20, 2018 212 lemma l: forall x y. ([@rewrite] x = y) -> f x = f y  MARCHE Claude committed Dec 05, 2016 213 \end{whycode}  Guillaume Melquiond committed Jun 20, 2018 214 can be proved by \verb|introduce_premises| followed by \verb|compute_specified|.  MARCHE Claude committed Sep 17, 2014 215 216 217 218 219 220 221  \paragraph{Bound on the number of reductions} The computations performed by these transformations can take an arbitrarily large number of steps, or even not terminate. For this reason, the number of steps is bounded by a maximal value, which is set by default to 1000. This value can be increased by another meta, \eg  MARCHE Claude committed Sep 16, 2014 222 223 224 \begin{whycode} meta "compute_max_steps" 1_000_000 \end{whycode}  MARCHE Claude committed Sep 17, 2014 225 226 When this upper limit is reached, a warning is issued, and the partly-reduced goal is returned as the result of the transformation.  MARCHE Claude committed Sep 16, 2014 227 228 229  \subsection{Other Non-Splitting Transformations}  MARCHE Claude committed Apr 10, 2012 230 231 232  \begin{description}  Guillaume Melquiond committed Oct 11, 2012 233 234 \item[eliminate\_algebraic] replaces algebraic data types by first-order definitions~\cite{paskevich09rr}.  Guillaume Melquiond committed Sep 16, 2014 235 \index{eliminate-algebraic@\verb+eliminate_algebraic+}  MARCHE Claude committed Apr 10, 2012 236   Guillaume Melquiond committed Oct 11, 2012 237 \item[eliminate\_builtin] removes definitions of symbols that are  Guillaume Melquiond committed May 09, 2012 238  declared as builtin in the driver, \ie with a syntax'' rule.  Guillaume Melquiond committed Sep 16, 2014 239 240 \index{eliminate-builtin@\verb+eliminate_builtin+}  MARCHE Claude committed Apr 10, 2012 241 \item[eliminate\_definition\_func]  Guillaume Melquiond committed Oct 11, 2012 242  replaces all function definitions with axioms.  Guillaume Melquiond committed Sep 16, 2014 243 244 \index{eliminate-definition-func@\verb+eliminate_definition_func+}  MARCHE Claude committed Apr 10, 2012 245 \item[eliminate\_definition\_pred]  Guillaume Melquiond committed Oct 11, 2012 246  replaces all predicate definitions with axioms.  Guillaume Melquiond committed Sep 16, 2014 247 248 \index{eliminate-definition-pred@\verb+eliminate_definition_pred+}  MARCHE Claude committed Apr 10, 2012 249 \item[eliminate\_definition]  Guillaume Melquiond committed Oct 11, 2012 250  applies both transformations above.  Guillaume Melquiond committed Sep 16, 2014 251 252 \index{eliminate-definition@\verb+eliminate_definition+}  MARCHE Claude committed Apr 10, 2012 253 \item[eliminate\_mutual\_recursion]  Guillaume Melquiond committed Oct 11, 2012 254  replaces mutually recursive definitions with axioms.  Guillaume Melquiond committed Sep 16, 2014 255 256 \index{eliminate-mutual-recursion@\verb+eliminate_mutual_recursion+}  MARCHE Claude committed Apr 10, 2012 257 \item[eliminate\_recursion]  Guillaume Melquiond committed Oct 11, 2012 258  replaces all recursive definitions with axioms.  Guillaume Melquiond committed Sep 16, 2014 259 \index{eliminate-recursion@\verb+eliminate_recursion+}  MARCHE Claude committed Apr 10, 2012 260 261 262  \item[eliminate\_if\_term] replaces terms of the form \texttt{if formula then t2 else t3} by lifting them at the level of formulas.  Guillaume Melquiond committed May 24, 2016 263  This may introduce \texttt{if then else} in formulas.  Guillaume Melquiond committed Sep 16, 2014 264 \index{eliminate-if-term@\verb+eliminate_if_term+}  MARCHE Claude committed Apr 10, 2012 265 266 267 268  \item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2 else f3} by an equivalent formula using implications and other connectives.  Guillaume Melquiond committed Sep 16, 2014 269 \index{eliminate-if-fmla@\verb+eliminate_if_fmla+}  MARCHE Claude committed Apr 10, 2012 270 271  \item[eliminate\_if]  Guillaume Melquiond committed Oct 11, 2012 272  applies both transformations above.  Guillaume Melquiond committed Sep 16, 2014 273 \index{eliminate-if@\verb+eliminate_if+}  MARCHE Claude committed Apr 10, 2012 274 275  \item[eliminate\_inductive] replaces inductive predicates by  Guillaume Melquiond committed May 09, 2012 276  (incomplete) axiomatic definitions, \ie construction axioms and  MARCHE Claude committed Apr 10, 2012 277  an inversion axiom.  Guillaume Melquiond committed Sep 16, 2014 278 \index{eliminate-inductive@\verb+eliminate_inductive+}  MARCHE Claude committed Apr 10, 2012 279 280  \item[eliminate\_let\_fmla]  Guillaume Melquiond committed Oct 11, 2012 281  eliminates \texttt{let} by substitution, at the predicate level.  Guillaume Melquiond committed Sep 16, 2014 282 \index{eliminate-let-fmla@\verb+eliminate_let_fmla+}  MARCHE Claude committed Apr 10, 2012 283 284  \item[eliminate\_let\_term]  Guillaume Melquiond committed Oct 11, 2012 285  eliminates \texttt{let} by substitution, at the term level.  Guillaume Melquiond committed Sep 16, 2014 286 \index{eliminate-let-term@\verb+eliminate_let_term+}  MARCHE Claude committed Apr 10, 2012 287 288  \item[eliminate\_let]  Guillaume Melquiond committed Oct 11, 2012 289  applies both transformations above.  Guillaume Melquiond committed Sep 16, 2014 290 \index{eliminate-let@\verb+eliminate_let+}  MARCHE Claude committed Apr 10, 2012 291 292 293 294 295 296  % \item[encoding\_decorate\_mono] % \item[encoding\_enumeration] \item[encoding\_smt]  Guillaume Melquiond committed May 27, 2016 297  encodes polymorphic types into monomorphic types~\cite{conchon08smt}.  Guillaume Melquiond committed Sep 16, 2014 298 \index{encoding-smt@\verb+encoding_smt+}  MARCHE Claude committed Apr 10, 2012 299 300  \item[encoding\_tptp]  Guillaume Melquiond committed Oct 11, 2012 301  encodes theories into unsorted logic. %~\cite{cruanes10}.  Guillaume Melquiond committed Sep 16, 2014 302 \index{encoding-tptp@\verb+encoding_tptp+}  MARCHE Claude committed Apr 10, 2012 303 304 305 306 307 308 309 310 311 312 313 314  % \item[filter\_trigger] *) % \item[filter\_trigger\_builtin] *) % \item[filter\_trigger\_no\_predicate] *) % \item[hypothesis\_selection] *) % Filter hypothesis of goals~\cite{couchot07ftp,cruanes10}. *) \item[introduce\_premises] moves antecedents of implications and universal quantifications of the goal into the premises of the task.  Guillaume Melquiond committed Sep 16, 2014 315 \index{introduce-premises@\verb+introduce_premises+}  MARCHE Claude committed Apr 10, 2012 316 317 318 319  % \item[remove\_triggers] *) % removes the triggers in all quantifications. *)  Guillaume Melquiond committed Oct 11, 2012 320 \item[simplify\_array] automatically rewrites the task using the lemma  Guillaume Melquiond committed Sep 16, 2014 321 322  \verb|Select_eq| of theory \verb|map.Map|. \index{simplify-array@\verb+simplify_array+}  MARCHE Claude committed Apr 10, 2012 323 324  \item[simplify\_formula] reduces trivial equalities $t=t$ to true and  Guillaume Melquiond committed Oct 11, 2012 325 326  then simplifies propositional structure: removes true, false, simplifies $f \land f$ to $f$, etc.  Guillaume Melquiond committed Sep 16, 2014 327 \index{simplify-formula@\verb+simplify_formula+}  MARCHE Claude committed Apr 10, 2012 328 329  \item[simplify\_recursive\_definition] reduces mutually recursive  Guillaume Melquiond committed May 09, 2012 330  definitions if they are not really mutually recursive, \eg  Guillaume Melquiond committed Oct 11, 2012 331 \begin{whycode}  Guillaume Melquiond committed May 24, 2016 332 function f : ... = ... g ...  Guillaume Melquiond committed Oct 11, 2012 333 334 with g : ... = e \end{whycode}  MARCHE Claude committed Apr 10, 2012 335 becomes  Guillaume Melquiond committed Oct 11, 2012 336 337 338 339 340 \begin{whycode} function g : ... = e function f : ... = ... g ... \end{whycode} if $f$ does not occur in $e$.  Guillaume Melquiond committed Sep 16, 2014 341 \index{simplify-recursive-definition@\verb+simplify_recursive_definition+}  MARCHE Claude committed Apr 10, 2012 342 343 344  \item[simplify\_trivial\_quantification] simplifies quantifications of the form  MARCHE Claude committed Sep 16, 2014 345 \begin{whycode}  Guillaume Melquiond committed May 24, 2016 346 forall x, x = t -> P(x)  MARCHE Claude committed Sep 16, 2014 347 \end{whycode}  Guillaume Melquiond committed May 24, 2016 348 into  MARCHE Claude committed Sep 16, 2014 349 \begin{whycode}  MARCHE Claude committed Apr 10, 2012 350 P(t)  MARCHE Claude committed Sep 16, 2014 351 \end{whycode}  Guillaume Melquiond committed May 24, 2016 352 353 354  when $x$ does not occur in $t$. More generally, this simplification is applied whenever $x=t$ or $t=x$ appears in negative position.  Guillaume Melquiond committed Sep 16, 2014 355 \index{simplify-trivial-quantification@\verb+simplify_trivial_quantification+}  MARCHE Claude committed Apr 10, 2012 356 357  \item[simplify\_trivial\_quantification\_in\_goal]  Guillaume Melquiond committed Oct 11, 2012 358  is the same as above but it applies only in the goal.  Guillaume Melquiond committed Sep 16, 2014 359 \index{simplify-trivial-quantification-in-goal@\verb+simplify_trivial_quantification_in_goal+}  MARCHE Claude committed Apr 10, 2012 360   Martin Clochard committed Mar 18, 2016 361 362 \item[split\_premise] replaces axioms in conjunctive form by an equivalent collection of axioms.  Guillaume Melquiond committed Jun 20, 2018 363  In absence of case analysis attributes (see \texttt{split\_goal} for details),  Martin Clochard committed Mar 18, 2016 364 365  the number of axiom generated per initial axiom is linear in the size of that initial axiom.  Guillaume Melquiond committed Sep 16, 2014 366 \index{split-premise@\verb+split_premise+}  MARCHE Claude committed Apr 10, 2012 367   Guillaume Melquiond committed May 24, 2016 368 369 370 371 \item[split\_premise\_full] is similar to \texttt{split\_premise}, but it also converts the axioms to conjunctive normal form. The number of axioms generated per initial axiom may be exponential in the size of the initial axiom.  Martin Clochard committed Mar 18, 2016 372 373 \index{split-premise-full@\verb+split_premise_full+}  MARCHE Claude committed Apr 10, 2012 374 375 \end{description}  Guillaume Melquiond committed May 27, 2016 376 377 \subsection{Other Splitting Transformations} \label{tech:trans:split}  MARCHE Claude committed Apr 10, 2012 378 379 380  \begin{description}  Guillaume Melquiond committed Oct 11, 2012 381 382 \item[simplify\_formula\_and\_task] is the same as \texttt{simplify\_formula} but it also removes the goal if it is equivalent to true.  Martin Clochard committed Mar 18, 2016 383 384 \index{simplify-formula-and-task@\verb+simplify_formula_and_task+}  Guillaume Melquiond committed May 24, 2016 385 \item[split\_goal] changes conjunctive goals into the  Guillaume Melquiond committed Jun 20, 2018 386  corresponding set of subgoals. In absence of case analysis attributes,  Martin Clochard committed Mar 18, 2016 387 388  the number of subgoals generated is linear in the size of the initial goal.  MARCHE Claude committed Mar 18, 2016 389 390  \paragraph{Behavior on asymmetric connectives and \texttt{by}/\texttt{so}}  Martin Clochard committed Mar 18, 2016 391   Guillaume Melquiond committed May 24, 2016 392  The transformation treats specially asymmetric and  MARCHE Claude committed Mar 18, 2016 393 394 395 396  \texttt{by}/\texttt{so} connectives. Asymmetric conjunction \verb|A && B| in goal position is handled as syntactic sugar for \verb|A /\ (A -> B)|. The conclusion of the first subgoal can then be used to prove the second one.  Martin Clochard committed Mar 18, 2016 397   MARCHE Claude committed Mar 18, 2016 398  Asymmetric disjunction \verb+A || B+ in hypothesis position is handled as  Martin Clochard committed Mar 18, 2016 399 400 401 402  syntactic sugar for \verb|A \/ ((not A) /\ B)|. In particular, a case analysis on such hypothesis would give the negation of the first hypothesis in the second case.  MARCHE Claude committed Mar 18, 2016 403 404 405 406 407 408 409 410 411 412 413  The \texttt{by} connective is treated as a proof indication. In hypothesis position, \verb|A by B| is treated as if it were syntactic sugar for its regular interpretation \verb|A|. In goal position, it is treated as if \verb|B| was an intermediate step for proving \verb|A|. \verb|A by B| is then replaced by \verb|B| and the transformation also generates a side-condition subgoal \verb|B -> A| representing the logical cut. Although splitting stops at disjunctive points like symmetric disjunction and left-hand sides of implications, the occurrences of the \texttt{by} connective are not restricted. For instance:  Martin Clochard committed Mar 18, 2016 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444  \begin{itemize} \item Splitting \begin{whycode} goal G : (A by B) && C \end{whycode} generates the subgoals \begin{whycode} goal G1 : B goal G2 : A -> C goal G3 : B -> A (* side-condition *) \end{whycode} \item Splitting \begin{whycode} goal G : (A by B) \/ (C by D) \end{whycode} generates \begin{whycode} goal G1 : B \/ D goal G2 : B -> A (* side-condition *) goal G3 : D -> C (* side-condition *) \end{whycode} \item Splitting \begin{whycode} goal G : (A by B) || (C by D) \end{whycode} generates \begin{whycode} goal G1 : B || D goal G2 : B -> A (* side-condition *) goal G3 : B || (D -> C) (* side-condition *) \end{whycode}  MARCHE Claude committed Mar 18, 2016 445 Note that due to the asymmetric disjunction, the disjunction is kept in the  Martin Clochard committed Mar 18, 2016 446 447 448 449 450 451 452 453 454 455 456 457 458 second side-condition subgoal. \item Splitting \begin{whycode} goal G : exists x. P x by x = 42 \end{whycode} generates \begin{whycode} goal G1 : exists x. x = 42 goal G2 : forall x. x = 42 -> P x (* side-condition *) \end{whycode} Note that in the side-condition subgoal, the context is universally closed. \end{itemize}  MARCHE Claude committed Mar 18, 2016 459 The \texttt{so} connective plays a similar role in hypothesis position, as it serves as a consequence indication. In goal position, \verb|A so B| is treated as if it were syntactic sugar for its regular interpretation \verb|A|. In hypothesis position, it is treated as if both \verb|A| and \verb|B| were true because \verb|B| is a consequence of \verb|A|. \verb|A so B| is replaced by \verb|A /\ B| and the transformation also generates a side-condition subgoal \verb|A -> B| corresponding to the consequence relation between formula.  Martin Clochard committed Mar 18, 2016 460   Guillaume Melquiond committed May 24, 2016 461 462 463 464 As with the \texttt{by} connective, occurrences of \texttt{so} are unrestricted. For instance: \begin{itemize} \item Splitting  Martin Clochard committed Mar 18, 2016 465 466 467 468 469 470 471 472 473 474 475 476 477 478 \begin{whycode} goal G : (((A so B) \/ C) -> D) && E \end{whycode} generates \begin{whycode} goal G1 : ((A /\ B) \/ C) -> D goal G2 : (A \/ C -> D) -> E goal G3 : A -> B (* side-condition *) \end{whycode} \item Splitting \begin{whycode} goal G : A by exists x. P x so Q x so R x by T x (* reads: A by (exists x. P x so (Q x so (R x by T x))) *) \end{whycode}  Guillaume Melquiond committed May 24, 2016 479 generates  Martin Clochard committed Mar 18, 2016 480 481 482 483 484 485 486 \begin{whycode} goal G1 : exists x. P x goal G2 : forall x. P x -> Q x (* side-condition *) goal G3 : forall x. P x -> Q x -> T x (* side-condition *) goal G4 : forall x. P x -> Q x -> T x -> R x (* side-condition *) goal G5 : (exists x. P x /\ Q x /\ R x) -> A (* side-condition *) \end{whycode}  Guillaume Melquiond committed May 24, 2016 487 In natural language, this corresponds to the following proof scheme  MARCHE Claude committed Mar 18, 2016 488 489 490 491 for \verb|A|: There exists a \verb|x| for which \verb|P| holds. Then, for that witness \verb|Q| and \verb|R| also holds. The last one holds because \verb|T| holds as well. And from those three conditions on \verb|x|, we can deduce \verb|A|.  Martin Clochard committed Mar 18, 2016 492 493 \end{itemize}  Guillaume Melquiond committed Jun 20, 2018 494 \paragraph{Attributes controlling the transformation}  Martin Clochard committed Mar 18, 2016 495   MARCHE Claude committed Mar 18, 2016 496 The transformations in the split family can be controlled by using  Guillaume Melquiond committed Jun 20, 2018 497 attributes on formulas.  Martin Clochard committed Mar 18, 2016 498   Guillaume Melquiond committed Jun 20, 2018 499 500 The \verb|[@stop_split]| attribute can be used to block the splitting of a formula. The attribute is removed after blocking, so applying the  MARCHE Claude committed Mar 18, 2016 501 502 transformation a second time will split the formula. This is can be used to decompose the splitting process in several steps. Also, if a  Guillaume Melquiond committed Jun 20, 2018 503 formula with this attribute is found in non-goal position, its  MARCHE Claude committed Mar 18, 2016 504 \texttt{by}/\texttt{so} proof indication will be erased by the  Guillaume Melquiond committed Jun 20, 2018 505 transformation. In a sense, formulas tagged by \verb|[@stop_split]| are  MARCHE Claude committed Mar 18, 2016 506 handled as if they were local lemmas.  Martin Clochard committed Mar 18, 2016 507   Guillaume Melquiond committed Jun 20, 2018 508 The \verb|[@case_split]| attribute can be used to force case analysis on hypotheses.  Martin Clochard committed Mar 18, 2016 509 510 For instance, applying \texttt{split\_goal} on \begin{whycode}  Guillaume Melquiond committed Jun 20, 2018 511 goal G : ([@case_split] A \/ B) -> C  Martin Clochard committed Mar 18, 2016 512 513 514 515 516 517 \end{whycode} generates the subgoals \begin{whycode} goal G1 : A -> C goal G2 : B -> C \end{whycode}  Guillaume Melquiond committed Jun 20, 2018 518 Without the attribute, the transformation does nothing because undesired case analysis  Martin Clochard committed Mar 18, 2016 519 520 may easily lead to an exponential blow-up.  Guillaume Melquiond committed May 24, 2016 521 Note that the precise behavior of splitting transformations in presence of  Guillaume Melquiond committed Jun 20, 2018 522 the \verb|[@case_split]| attribute is not yet specified  Martin Clochard committed Mar 18, 2016 523 524 525 and is likely to change in future versions. \index{split-goal@\verb+split_goal+}  MARCHE Claude committed Apr 10, 2012 526 527  \item[split\_all]  Guillaume Melquiond committed Oct 11, 2012 528  performs both \texttt{split\_premise} and \texttt{split\_goal}.  Guillaume Melquiond committed Sep 16, 2014 529 \index{split-all@\verb+split_all+}  MARCHE Claude committed Apr 10, 2012 530   Guillaume Melquiond committed May 24, 2016 531 532 \item[split\_intro] performs both \texttt{split\_goal} and \texttt{introduce\_premises}.  Guillaume Melquiond committed Sep 16, 2014 533 \index{split-intro@\verb+split_intro+}  MARCHE Claude committed Apr 10, 2012 534   Guillaume Melquiond committed May 24, 2016 535 536 \item[split\_goal\_full] has a behavior similar  Martin Clochard committed Mar 18, 2016 537 538 539 540 541 542 543 544 545  to \texttt{split\_goal}, but also converts the goal to conjunctive normal form. The number of subgoals generated may be exponential in the size of the initial goal. \index{split-goal-full@\verb+split_goal_full+} \item[split\_all\_full] performs both \texttt{split\_premise} and \texttt{split\_goal\_full}. \index{split-all-full@\verb+split_all_full+}  MARCHE Claude committed Apr 10, 2012 546 547 548 \end{description}  MARCHE Claude committed Mar 24, 2016 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 \section{Proof Strategies} \label{sec:strategies} As seen in Section~\ref{sec:ideref}, the IDE provides a few buttons that trigger the run of simple proof strategies on the selected goals. Proof strategies can be defined using a basic assembly-style language, and put into the Why3 configuration file. The commands of this basic language are: \begin{itemize} \item \texttt{c $p$ $t$ $m$} calls the prover $p$ with a time limit $t$ and memory limit $m$. On success, the strategy ends, it continues to next line otherwise \item \texttt{t $n$ $lab$} applies the transformation $n$. On success, the strategy continues to label $lab$, and is applied to each generated sub-goals. It continues to next line otherwise. \item \texttt{g $lab$} inconditionally jumps to label $lab$ \item \texttt{$lab$:} declares the label $lab$. The default label \texttt{exit} allows to stop the program. \end{itemize} To examplify this basic programming language, we give below the default strategies that are attached to the default buttons of the  MARCHE Claude committed Sep 28, 2017 571 IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0  MARCHE Claude committed Mar 24, 2016 572 573 574 575 576 577 578 were detected by the \verb|why3 config --detect| command \begin{description} \item[Split] is bound to the 1-line strategy \begin{verbatim} t split_goal_wp exit \end{verbatim}  MARCHE Claude committed Sep 28, 2017 579 580 581 582 583 584 585 586 587 588 \item[Auto level 0] is bound to \begin{verbatim} c Z3,4.5.0, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000 \end{verbatim} The three provers are tried for a time limit of 1 second and memory limit of 1~Gb, each in turn. This is a perfect strategy for a first attempt to discharge a new goal.  MARCHE Claude committed Mar 24, 2016 589 590 591 \item[Auto level 1] is bound to \begin{verbatim} start:  MARCHE Claude committed Sep 28, 2017 592 593 594 c Z3,4.5.0, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000  MARCHE Claude committed Mar 24, 2016 595 t split_goal_wp start  MARCHE Claude committed Sep 28, 2017 596 597 598 c Z3,4.5.0, 10 4000 c Alt-Ergo,1.30, 10 4000 c CVC4,1.5, 10 4000  MARCHE Claude committed Mar 24, 2016 599 600 601 602 603 604 605 606 607 608 \end{verbatim} The three provers are first tried for a time limit of 1 second and memory limit of 1~Gb, each in turn. If none of them succeed, a split is attempted. If the split works then the same strategy is retried on each sub-goals. If the split does not succeed, the provers are tried again with a larger limits. \item[Auto level 2] is bound to \begin{verbatim} start:  MARCHE Claude committed Sep 28, 2017 609 610 c Z3,4.5.0, 1 1000 c Eprover,2.0, 1 1000  MARCHE Claude committed Mar 24, 2016 611 c Spass,3.7, 1 1000  MARCHE Claude committed Sep 28, 2017 612 613 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000  MARCHE Claude committed Mar 24, 2016 614 t split_goal_wp start  MARCHE Claude committed Sep 28, 2017 615 616 c Z3,4.5.0, 5 2000 c Eprover,2.0, 5 2000  MARCHE Claude committed Mar 24, 2016 617 c Spass,3.7, 5 2000  MARCHE Claude committed Sep 28, 2017 618 619 c Alt-Ergo,1.30, 5 2000 c CVC4,1.5, 5 2000  MARCHE Claude committed Mar 24, 2016 620 621 622 623 624 625 626 t introduce_premises afterintro afterintro: t inline_goal afterinline g trylongertime afterinline: t split_goal_wp start trylongertime:  MARCHE Claude committed Sep 28, 2017 627 628 c Z3,4.5.0, 30 4000 c Eprover,2.0, 30 4000  MARCHE Claude committed Mar 24, 2016 629 c Spass,3.7, 30 4000  MARCHE Claude committed Sep 28, 2017 630 631 c Alt-Ergo,1.30, 30 4000 c CVC4,1.5, 30 4000  MARCHE Claude committed Mar 24, 2016 632 633 634 635 636 637 638 \end{verbatim} Notice that now 5 provers are used. The provers are first tried for a time limit of 1 second and memory limit of 1~Gb, each in turn. If none of them succeed, a split is attempted. If the split works then the same strategy is retried on each sub-goals. If the split does not succeed, the prover are tried again with limits of 5 s and 2 Gb. If all fail, we attempt the transformation of introduction of  MARCHE Claude committed Sep 28, 2017 639  premises in the context, followed by an inlining of the definitions  MARCHE Claude committed Mar 24, 2016 640 641 642 643 644 645  in the goals. We then attempt a split again, if the split succeeds, we restart from the beginning, if it fails then provers are tried again with 30s and 4 Gb. \end{description}  MARCHE Claude committed Apr 10, 2012 646 647 648 649 650 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: