[Why3-club] Realized theories and "remove prop" declarations

Guillaume Melquiond guillaume.melquiond at inria.fr
Thu Nov 7 19:05:38 CET 2013

On 07/11/2013 16:46, Stefan Berghofer wrote:

> This brings me to another question: It seems to me that there are
> roughly three strategies for
> linking functions (and predicates) declared in a Why3 theory with their
> counterparts in an
> interactive target prover:
> 1. Add "syntax" declarations for the functions to the *.drv file, but do
> not realize the theory
> 2. Add "syntax" declarations for the functions to the *.drv file, and
> also realize the theory
> 3. Realize the theory, and provide definitions for the functions in the
> file for the target prover
>     generated by Why3
> Is this observation correct? Which is the preferred strategy?

First, it depends on whether you intend to realize a given theory. If 
you don't, 1 is the only possibility. (Sorry for the obviousness of this 

So let us suppose that you are realizing a theory. It now depends on 
whether the Why3 symbol has an explicit definition or it is implicitly 
characterized by some axioms. If there is an explicit definition, then 3 
is impossible, since there is already a definition. So 2 is the way to 
go. Note that, in this case, the Coq realization generator does a bit 
more work and requires you to prove the equivalence between the symbol 
in the driver and the Why3 symbol. (Example: lemma sqr_def in 

The last case to consider is thus: the theory is realized and there is 
no explicit Why3 definition for the symbol. Both solutions 2 and 3 are 
available. Note that using 3 incurs an indirection between the symbol in 
the proof obligations and the symbol from your prover. Assuming this 
indirection has no adverse consequences for the user (e.g. the need for 
explicit unfolding in proof scripts), I can't think of a strong reason 
to choose one over the other. Just choose whichever you prefer.

Best regards,


More information about the Why3-club mailing list