[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
statement.)
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
lib/coq/real/Square.v.)
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,
Guillaume
More information about the Why3-club
mailing list