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

Stefan Berghofer berghofe at in.tum.de
Thu Nov 7 16:46:40 CET 2013


Dear Guillaume,

thanks a lot for your detailed explanation.

>  From your questions, there seems to be several misunderstandings. First, a "remove prop" declaration means that no corresponding axiom are generated in the proof obligations. So, from a consistency point of view, the more "remove prop" there are, the safer a proof ends up.

Thanks, I was not aware of the exact semantics of "remove prop". It does not seem to be mentioned
in the current version of the manual (0.81), or maybe I have just overlooked it...

> Obviously, in order to keep some completeness, one should remove only the axioms that the target prover already knows about (or those that they are unable to use). For instance, SMT solvers know that arithmetic operations are commutative, associative, distributive, etc, so there are "remove prop" for all these axioms. Similarly, for Coq, everything already proved in the standard library is marked "remove prop", so as to not overwhelm the user with redundant properties.
>
> Now, what about realizations? Realizations act as if all the properties are automatically marked "remove prop". Indeed, if they are realized, there is no point in keeping them around as axioms. In other words, all the "remove prop" declarations from the driver are redundant if the corresponding theories are realized.
>
> Note that realizations are not handled the same way as proof obligations, so the "remove prop" declarations are ignored when generating them. These declarations are thus really pointless; they only matter if someone were to disable realizations in Why3.

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?

Greetings,
Stefan



More information about the Why3-club mailing list