syntax.tex 16.9 KB
 MARCHE Claude committed Jul 02, 2011 1 \chapter{The \why Language}  MARCHE Claude committed Sep 08, 2010 2 \label{chap:syntax}  MARCHE Claude committed Sep 06, 2010 3 4 5 6  This chapter describes the input syntax, and informally gives its semantics, illustrated by examples.  MARCHE Claude committed Jul 02, 2011 7 A \why text contains a list of \emph{theories}.  Jean-Christophe Filliâtre committed Dec 13, 2010 8 A theory is a list of \emph{declarations}. Declarations introduce new  Andrei Paskevich committed Dec 20, 2010 9 types, functions and predicates, state axioms, lemmas and goals.  Jean-Christophe Filliâtre committed Dec 13, 2010 10 These declarations can be directly written in the theory or taken from  MARCHE Claude committed Jul 02, 2011 11 existing theories. The base logic of \why is first-order  Andrei Paskevich committed Dec 20, 2010 12 logic with polymorphic types.  MARCHE Claude committed Sep 06, 2010 13   Guillaume Melquiond committed Jun 26, 2014 14 \section{Example 1: Lists}  Andrei Paskevich committed Dec 20, 2010 15   Guillaume Melquiond committed Apr 28, 2013 16 17 18 19 20 %BEGIN LATEX Figure~\ref{fig:tutorial1} contains an example of \why input text, containing three theories. %END LATEX %HEVEA The code below is an example of \why input text, containing three theories.  Jean-Christophe Filliâtre committed Dec 13, 2010 21   Guillaume Melquiond committed Apr 28, 2013 22 %BEGIN LATEX  Jean-Christophe Filliâtre committed Dec 13, 2010 23 \begin{figure}  Andrei Paskevich committed Dec 20, 2010 24 \centering  Guillaume Melquiond committed Apr 28, 2013 25 %END LATEX  26 \begin{whycode}  Jean-Christophe Filliâtre committed Dec 13, 2010 27 28 29 30 31 32 33 34 theory List type list 'a = Nil | Cons 'a (list 'a) end theory Length use import List use import int.Int  Andrei Paskevich committed Jun 30, 2011 35  function length (l : list 'a) : int =  Jean-Christophe Filliâtre committed Dec 13, 2010 36 37 38 39 40  match l with | Nil -> 0 | Cons _ r -> 1 + length r end  Andrei Paskevich committed Dec 20, 2010 41  lemma Length_nonnegative : forall l:list 'a. length l >= 0  Jean-Christophe Filliâtre committed Dec 13, 2010 42 43 44 45 46 end theory Sorted use import List use import int.Int  Andrei Paskevich committed Dec 20, 2010 47   Andrei Paskevich committed Dec 17, 2010 48  inductive sorted (list int) =  Andrei Paskevich committed Dec 20, 2010 49  | Sorted_Nil :  Jean-Christophe Filliâtre committed Dec 13, 2010 50  sorted Nil  Andrei Paskevich committed Dec 20, 2010 51  | Sorted_One :  Jean-Christophe Filliâtre committed Dec 13, 2010 52  forall x:int. sorted (Cons x Nil)  Andrei Paskevich committed Dec 20, 2010 53 54  | Sorted_Two : forall x y : int, l : list int.  Jean-Christophe Filliâtre committed Dec 13, 2010 55 56  x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end  57 \end{whycode}  Guillaume Melquiond committed Apr 28, 2013 58 %BEGIN LATEX  Guillaume Melquiond committed Jun 26, 2014 59 60 \vspace*{-1em}%\hrulefill \caption{Example of \why text}  Jean-Christophe Filliâtre committed Dec 13, 2010 61 62 \label{fig:tutorial1} \end{figure}  Guillaume Melquiond committed Apr 28, 2013 63 64 65 66 67 68 69 70 71 72 73 %END LATEX The first theory, \texttt{List}, declares a new algebraic type for polymorphic lists, \texttt{list 'a}. As in ML, \texttt{'a} stands for a type variable. The type \texttt{list 'a} has two constructors, \texttt{Nil} and \texttt{Cons}. Both constructors can be used as usual function symbols, respectively of type \texttt{list 'a} and \texttt{'a $\times$ list 'a $\rightarrow$ list 'a}. We deliberately make this theory that short, for reasons which will be discussed later.  Jean-Christophe Filliâtre committed Dec 13, 2010 74 75 76 77 78 79  The next theory, \texttt{Length}, introduces the notion of list length. The \texttt{use import List} command indicates that this new theory may refer to symbols from theory \texttt{List}. These symbols are accessible in a qualified form, such as \texttt{List.list} or \texttt{List.Cons}. The \texttt{import} qualifier additionally allows  Jean-Christophe Filliâtre committed Dec 20, 2010 80 us to use them without qualification.  Jean-Christophe Filliâtre committed Dec 13, 2010 81 82 83 84 85 86  Similarly, the next command \texttt{use import int.Int} adds to our context the theory \texttt{int.Int} from the standard library. The prefix \texttt{int} indicates the file in the standard library containing theory \texttt{Int}. Theories referred to without prefix either appear earlier in the current file, \eg\ \texttt{List}, or are  Andrei Paskevich committed Dec 20, 2010 87 predefined.  Jean-Christophe Filliâtre committed Dec 13, 2010 88   Jean-Christophe Filliâtre committed Dec 20, 2010 89 The next declaration defines a recursive function, \texttt{length},  Andrei Paskevich committed Jun 30, 2011 90 91 92 which computes the length of a list. The \texttt{function} and \texttt{predicate} keywords are used to introduce function and predicate symbols, respectively.  MARCHE Claude committed Jul 02, 2011 93 \why checks every recursive, or mutually recursive, definition for  Jean-Christophe Filliâtre committed Dec 15, 2010 94 termination. Basically, we require a lexicographic and structural  Andrei Paskevich committed Dec 20, 2010 95 96 descent for every recursive call for some reordering of arguments. Notice that matching must be exhaustive and that every \texttt{match}  Jean-Christophe Filliâtre committed Dec 15, 2010 97 98 expression must be terminated by the \texttt{end} keyword.  MARCHE Claude committed Jul 02, 2011 99 Despite using higher-order curried'' syntax, \why does not permit  Andrei Paskevich committed Dec 20, 2010 100 101 partial application: function and predicate arities must be respected.  Jean-Christophe Filliâtre committed Dec 15, 2010 102 The last declaration in theory \texttt{Length} is a lemma stating that  Andrei Paskevich committed Dec 20, 2010 103 the length of a list is non-negative.  Jean-Christophe Filliâtre committed Dec 15, 2010 104   Andrei Paskevich committed Dec 17, 2010 105 106 107 108 109 The third theory, \texttt{Sorted}, demonstrates the definition of an inductive predicate. Every such definition is a list of clauses: universally closed implications where the consequent is an instance of the defined predicate. Moreover, the defined predicate may only occur in positive positions in the antecedent. For example, a clause:  110 \begin{whycode}  Andrei Paskevich committed Dec 17, 2010 111 112 113  | Sorted_Bad : forall x y : int, l : list int. (sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l))  114 \end{whycode}  Andrei Paskevich committed Dec 17, 2010 115 116 would not be allowed. This positivity condition assures the logical soundness of an inductive definition.  Jean-Christophe Filliâtre committed Dec 13, 2010 117   Jean-Christophe Filliâtre committed Apr 20, 2012 118 Note that the type signature of \lstinline{sorted} predicate does not  Andrei Paskevich committed Dec 17, 2010 119 120 include the name of a parameter (see \texttt{l} in the definition of \texttt{length}): it is unused and therefore optional.  MARCHE Claude committed Sep 06, 2010 121   Guillaume Melquiond committed Jun 26, 2014 122 \section{Example 1 (continued): Lists and Abstract Orderings}  Andrei Paskevich committed Dec 20, 2010 123 124 125 126  In the previous section we have seen how a theory can reuse the declarations of another theory, coming either from the same input text or from the library. Another way to referring to a theory is  MARCHE Claude committed Dec 20, 2010 127 by cloning''. A \texttt{clone} declaration constructs a local  Andrei Paskevich committed Dec 20, 2010 128 copy of the cloned theory, possibly instantiating some of its  MARCHE Claude committed Oct 10, 2013 129 abstract (\ie declared but not defined) symbols.  Andrei Paskevich committed Dec 20, 2010 130   Guillaume Melquiond committed Apr 28, 2013 131 132 133 134 135 136 137 138 139 140 141 %BEGIN LATEX Consider the continued example in Figure~\ref{fig:tutorial2}. %END LATEX %HEVEA Consider the continued example below. We write an abstract theory of partial orders, declaring an abstract type \texttt{t} and an abstract binary predicate \texttt{<=}. Notice that an infix operation must be enclosed in parentheses when used outside a term. We also specify three axioms of a partial order. %BEGIN LATEX  Andrei Paskevich committed Dec 20, 2010 142 143 \begin{figure} \centering  Guillaume Melquiond committed Apr 28, 2013 144 %END LATEX  145 \begin{whycode}  Andrei Paskevich committed Dec 20, 2010 146 147 theory Order type t  Andrei Paskevich committed Jun 30, 2011 148  predicate (<=) t t  Andrei Paskevich committed Dec 20, 2010 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170  axiom Le_refl : forall x : t. x <= x axiom Le_asym : forall x y : t. x <= y -> y <= x -> x = y axiom Le_trans: forall x y z : t. x <= y -> y <= z -> x <= z end theory SortedGen use import List clone import Order as O inductive sorted (l : list t) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:t. sorted (Cons x Nil) | Sorted_Two : forall x y : t, l : list t. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end theory SortedIntList use import int.Int  Andrei Paskevich committed Jun 30, 2011 171  clone SortedGen with type O.t = int, predicate O.(<=) = (<=)  Andrei Paskevich committed Dec 20, 2010 172 end  173 \end{whycode}  Guillaume Melquiond committed Apr 28, 2013 174 %BEGIN LATEX  Guillaume Melquiond committed Jun 26, 2014 175 176 \vspace*{-1em}%\hrulefill \caption{Example of \why text (continued)}  Andrei Paskevich committed Dec 20, 2010 177 178 \label{fig:tutorial2} \end{figure}  Guillaume Melquiond committed Apr 28, 2013 179 %END LATEX  Andrei Paskevich committed Dec 20, 2010 180 181 182 183 184 185 186 187 188 189 190 191 192  There is little value in \texttt{use}'ing such a theory: this would constrain us to stay with the type \texttt{t}. However, we can construct an instance of theory \texttt{Order} for any suitable type and predicate. Moreover, we can build some further abstract theories using order, and then instantiate those theories. Consider theory \texttt{SortedGen}. In the beginning, we \texttt{use} the earlier theory \texttt{List}. Then we make a simple \texttt{clone} theory \texttt{Order}. This is pretty much equivalent to copy-pasting every declaration from \texttt{Order} to \texttt{SortedGen};  MARCHE Claude committed Jul 02, 2011 193 the only difference is that \why traces the history  Andrei Paskevich committed Dec 20, 2010 194 195 196 197 198 of cloning and transformations and drivers often make use of it (see Section~\ref{sec:drivers}). Notice an important difference between \texttt{use} and \texttt{clone}. If we \texttt{use} a theory, say  MARCHE Claude committed Oct 10, 2013 199 \texttt{List}, twice (directly or indirectly: \eg by  Andrei Paskevich committed Dec 20, 2010 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 making \texttt{use} of both \texttt{Length} and \texttt{Sorted}), there is no duplication: there is still only one type of lists and a unique pair of constructors. On the contrary, when we \texttt{clone} a theory, we create a local copy of every cloned declaration, and the newly created symbols, despite having the same names, are different from their originals. Returning to the example, we finish theory \texttt{SortedGen} with a familiar definition of predicate \texttt{sorted}; this time we use the abstract order on the values of type \texttt{t}. Now, we can instantiate theory \texttt{SortedGen} to any ordered type, without having to retype the definition of \texttt{sorted}. For example, theory \texttt{SortedIntList}  MARCHE Claude committed Oct 10, 2013 216 makes \texttt{clone} of \texttt{SortedGen} (\ie copies its  Andrei Paskevich committed Dec 20, 2010 217 218 declarations) substituting type \texttt{int} for type \texttt{O.t} of \texttt{SortedGen} and the default order  MARCHE Claude committed Jul 02, 2011 219 on integers for predicate \texttt{O.(<=)}. \why will  Andrei Paskevich committed Dec 20, 2010 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 control that the result of cloning is well-typed. Several remarks ought to be made here. First of all, why should we clone theory \texttt{Order} in \texttt{SortedGen} if we make no instantiation? Couldn't we write \texttt{use import Order as O} instead? The answer is no, we could not. When cloning a theory, we only can instantiate the symbols declared locally in this theory, not the symbols imported with \texttt{use}. Therefore, we create a local copy of \texttt{Order} in \texttt{SortedGen} to be able to instantiate \texttt{t} and \texttt{(<=)} later. Secondly, when we instantiate an abstract symbol, its declaration is not copied from the theory being cloned. Thus, we will not create a second declaration of type \texttt{int} in \texttt{SortedIntList}. The mechanism of cloning bears some resemblance to modules and functors  MARCHE Claude committed Jul 02, 2011 236 237 of ML-like languages. Unlike those languages, \why makes no distinction between modules and module signatures, modules and functors. Any \why  Andrei Paskevich committed Dec 20, 2010 238 239 240 241 242 243 244 245 246 247 248 theory can be \texttt{use}'d directly or instantiated in any of its abstract symbols. The command-line tool \texttt{why3} (described in Section~\ref{sec:batch}), allows us to see the effect of cloning. If the input file containing our example is called \texttt{lists.why}, we can launch the following command: \begin{verbatim} > why3 lists.why -T SortedIntList \end{verbatim} to see the resulting theory \texttt{SortedIntList}:  249 \begin{whycode}  Andrei Paskevich committed Dec 20, 2010 250 251 252 253 254 255 256 257 258 259 theory SortedIntList (* use BuiltIn *) (* use Int *) (* use List *) axiom Le_refl : forall x:int. x <= x axiom Le_asym : forall x:int, y:int. x <= y -> y <= x -> x = y axiom Le_trans : forall x:int, y:int, z:int. x <= y -> y <= z -> x <= z  Andrei Paskevich committed Jun 30, 2011 260  (* clone Order with type t = int, predicate (<=) = (<=),  Andrei Paskevich committed Dec 20, 2010 261 262 263 264 265 266 267 268 269  prop Le_trans1 = Le_trans, prop Le_asym1 = Le_asym, prop Le_refl1 = Le_refl *) inductive sorted (list int) = | Sorted_Nil : sorted (Nil:list int) | Sorted_One : forall x:int. sorted (Cons x (Nil:list int)) | Sorted_Two : forall x:int, y:int, l:list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))  Andrei Paskevich committed Jun 30, 2011 270 271  (* clone SortedGen with type t1 = int, predicate sorted1 = sorted, predicate (<=) = (<=), prop Sorted_Two1 = Sorted_Two,  Andrei Paskevich committed Dec 20, 2010 272 273 274 275  prop Sorted_One1 = Sorted_One, prop Sorted_Nil1 = Sorted_Nil, prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym, prop Le_refl2 = Le_refl *) end  276 \end{whycode}  Andrei Paskevich committed Dec 20, 2010 277 278 279 280 281 282 283 284 285 286 287 288 289  In conclusion, let us briefly explain the concept of namespaces in \why. Both \texttt{use} and \texttt{clone} instructions can be used in three forms (the examples below are given for \texttt{use}, the semantics for \texttt{clone} is the same): \begin{itemize} \item \texttt{use List as L} --- every symbol $s$ of theory \texttt{List} is accessible under the name \texttt{L.$s$}. The \texttt{as L} part is optional, if it is omitted, the name of the symbol is \texttt{List.$s$}. \item \texttt{use import List as L} --- every symbol $s$ from \texttt{List} is accessible under the name \texttt{L.$s$}. It is also accessible simply as \texttt{$s$}, but only up to the end of the current  MARCHE Claude committed Oct 10, 2013 290 namespace, \eg the current theory. If the current theory, that is the  Andrei Paskevich committed Dec 20, 2010 291 292 293 294 295 296 297 298 299 300 301 302 303 one making \texttt{use}, is later used under the name \texttt{T}, the name of the symbol would be \texttt{T.L.$s$}. (This is why we could refer directly to the symbols of \texttt{Order} in theory \texttt{SortedGen}, but had to qualify them with \texttt{O.} in \texttt{SortedIntList}.) As in the previous case, \texttt{as L} part is optional. \item \texttt{use export List} --- every symbol $s$ from \texttt{List} is accessible simply as \texttt{$s$}. If the current theory is later used under the name \texttt{T}, the name of the symbol would be \texttt{T.$s$}. \end{itemize}  MARCHE Claude committed Jul 02, 2011 304 \why allows to open new namespaces explicitly in the text. In particular,  Andrei Paskevich committed Dec 20, 2010 305 306 the instruction \texttt{clone import Order as O}'' can be equivalently written as:  307 308 309 310 311 \begin{whycode} namespace import O clone export Order end \end{whycode}  Guillaume Melquiond committed Jun 26, 2014 312 However, since \why favors short theories over long and complex ones,  Andrei Paskevich committed Dec 20, 2010 313 314 this feature is rarely used.  Guillaume Melquiond committed Jun 26, 2014 315 \section{Example 2: Einstein's Problem}  Jean-Christophe committed Dec 16, 2010 316 317 \index{Einstein's logic problem}  MARCHE Claude committed Jul 02, 2011 318 We now consider another, slightly more complex example: how to use \why  Jean-Christophe committed Dec 16, 2010 319 to solve a little puzzle known as Einstein's logic  Guillaume Melquiond committed Apr 28, 2013 320 321 322 323 324 problem''.% %BEGIN LATEX \footnote{This \why example was contributed by St\'ephane Lescuyer.} %END LATEX %HEVEA {} (This \why example was contributed by St\'ephane Lescuyer.)  MARCHE Claude committed May 13, 2016 325 326 327 The code given below is available in the source distribution in directory \verb|examples/logic/einstein.why|.  Jean-Christophe Filliâtre committed Dec 16, 2010 328 329 330 The problem is stated as follows. Five persons, of five different nationalities, live in five houses in a row, all painted with different colors.  Guillaume Melquiond committed Jun 26, 2014 331 These five persons own different pets, drink different beverages and  Jean-Christophe Filliâtre committed Dec 16, 2010 332 333 smoke different brands of cigars. We are given the following information:  Jean-Christophe committed Dec 16, 2010 334 \begin{itemize}  Jean-Christophe Filliâtre committed Dec 16, 2010 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 \item The Englishman lives in a red house; \item The Swede has dogs; \item The Dane drinks tea; \item The green house is on the left of the white one; \item The green house's owner drinks coffee; \item The person who smokes Pall Mall has birds; \item The yellow house's owner smokes Dunhill; \item In the house in the center lives someone who drinks milk; \item The Norwegian lives in the first house; \item The man who smokes Blends lives next to the one who has cats; \item The man who owns a horse lives next to the one who smokes Dunhills; \item The man who smokes Blue Masters drinks beer; \item The German smokes Prince; \item The Norwegian lives next to the blue house; \item The man who smokes Blends has a neighbour who drinks water.  Jean-Christophe committed Dec 16, 2010 364 365 366 367 368 369 370 \end{itemize} The question is: what is the nationality of the fish's owner? We start by introducing a general-purpose theory defining the notion of \emph{bijection}, as two abstract types together with two functions from one to the other and two axioms stating that these functions are inverse of each other.  371 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 372 373 374 375 theory Bijection type t type u  Andrei Paskevich committed Jun 30, 2011 376  function of t : u  MARCHE Claude committed May 13, 2016 377  function to_ u : t  Jean-Christophe committed Dec 16, 2010 378   MARCHE Claude committed May 13, 2016 379 380  axiom To_of : forall x : t. to_ (of x) = x axiom Of_to : forall y : u. of (to_ y) = y  Jean-Christophe committed Dec 16, 2010 381 end  382 \end{whycode}  Jean-Christophe committed Dec 16, 2010 383 384 385  We now start a new theory, \texttt{Einstein}, which will contain all the individuals of the problem.  386 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 387 theory Einstein "Einstein's problem"  388 \end{whycode}  Jean-Christophe committed Dec 16, 2010 389 390 First we introduce enumeration types for houses, colors, persons, drinks, cigars and pets.  391 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 392 393 394 395 396 397  type house = H1 | H2 | H3 | H4 | H5 type color = Blue | Green | Red | White | Yellow type person = Dane | Englishman | German | Norwegian | Swede type drink = Beer | Coffee | Milk | Tea | Water type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince type pet = Birds | Cats | Dogs | Fish | Horse  398 \end{whycode}  Jean-Christophe committed Dec 16, 2010 399 400 We now express that each house is associated bijectively to a color, by cloning the \texttt{Bijection} theory appropriately.  401 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 402  clone Bijection as Color with type t = house, type u = color  403 \end{whycode}  Jean-Christophe committed Dec 16, 2010 404 It introduces two functions, namely \texttt{Color.of} and  MARCHE Claude committed May 13, 2016 405 \texttt{Color.to\_}, from houses to colors and colors to houses,  Jean-Christophe committed Dec 16, 2010 406 407 408 respectively, and the two axioms relating them. Similarly, we express that each house is associated bijectively to a person  409 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 410  clone Bijection as Owner with type t = house, type u = person  411 \end{whycode}  Jean-Christophe committed Dec 16, 2010 412 and that drinks, cigars and pets are all associated bijectively to persons:  413 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 414 415 416  clone Bijection as Drink with type t = person, type u = drink clone Bijection as Cigar with type t = person, type u = cigar clone Bijection as Pet with type t = person, type u = pet  417 \end{whycode}  Jean-Christophe committed Dec 16, 2010 418 419 Next we need a way to state that a person lives next to another. We first define a predicate \texttt{leftof} over two houses.  420 \begin{whycode}  Andrei Paskevich committed Jun 30, 2011 421  predicate leftof (h1 h2 : house) =  Jean-Christophe committed Dec 16, 2010 422  match h1, h2 with  Andrei Paskevich committed Dec 20, 2010 423 424 425  | H1, H2 | H2, H3 | H3, H4  Jean-Christophe committed Dec 16, 2010 426 427 428  | H4, H5 -> true | _ -> false end  429 \end{whycode}  Andrei Paskevich committed Dec 20, 2010 430 Note how we advantageously used pattern matching, with an or-pattern  Jean-Christophe committed Dec 16, 2010 431 432 433 for the four positive cases and a universal pattern for the remaining 21 cases. It is then immediate to define a \texttt{neighbour} predicate over two houses, which completes theory \texttt{Einstein}.  434 \begin{whycode}  Andrei Paskevich committed Jun 30, 2011 435  predicate rightof (h1 h2 : house) =  Jean-Christophe committed Dec 16, 2010 436  leftof h2 h1  Andrei Paskevich committed Jun 30, 2011 437 438  predicate neighbour (h1 h2 : house) = leftof h1 h2 \/ rightof h1 h2  Jean-Christophe committed Dec 16, 2010 439 end  440 \end{whycode}  Jean-Christophe committed Dec 16, 2010 441 442 443  The next theory contains the 15 hypotheses. It starts by importing theory \texttt{Einstein}.  444 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 445 446 theory EinsteinHints "Hints" use import Einstein  447 \end{whycode}  MARCHE Claude committed May 13, 2016 448 Then each hypothesis is stated in terms of \texttt{to\_} and \texttt{of}  Jean-Christophe committed Dec 16, 2010 449 450 functions. For instance, the hypothesis The Englishman lives in a red house'' is declared as the following axiom.  451 \begin{whycode}  MARCHE Claude committed May 13, 2016 452  axiom Hint1: Color.of (Owner.to_ Englishman) = Red  453 \end{whycode}  Jean-Christophe committed Dec 16, 2010 454 455 456 And so on for all other hypotheses, up to The man who smokes Blends has a neighbour who drinks water'', which completes this theory.  457 \begin{whycode}  Jean-Christophe committed Dec 16, 2010 458 459  ... axiom Hint15:  MARCHE Claude committed May 13, 2016 460  neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water))  Jean-Christophe committed Dec 16, 2010 461 end  462 \end{whycode}  Andrei Paskevich committed Dec 20, 2010 463 Finally, we declare the goal in the fourth theory:  464 \begin{whycode}  Jean-Christophe Filliâtre committed Dec 16, 2010 465 466 467 theory Problem "Goal of Einstein's problem" use import Einstein use import EinsteinHints  Jean-Christophe committed Dec 16, 2010 468   MARCHE Claude committed May 13, 2016 469  goal G: Pet.to_ Fish = German  Jean-Christophe Filliâtre committed Dec 16, 2010 470 end  471 \end{whycode}  MARCHE Claude committed Jul 02, 2011 472 and we are ready to use \why to discharge this goal with any prover  Jean-Christophe Filliâtre committed Dec 16, 2010 473 of our choice.  MARCHE Claude committed Sep 06, 2010 474 475 476 477 478 479  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: