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

Guillaume Melquiond guillaume.melquiond at inria.fr
Thu Nov 7 09:22:48 CET 2013


On 06/11/2013 15:28, Stefan Berghofer wrote:
> Dear Why3-Club,
>
> the file coq-common.gen contains many "remove prop" declarations for
> theories that are
> realized, such as "remove prop Div_mod" for theory int.ComputerDivision.
> What is the
> rationale behind these declarations? Shouldn't a proof obligation be
> generated to make
> sure that the Coq functions ZOdiv and Z0mod behave the same way as the
> corresponding Why3
> functions div and mod?

 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.

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.

To sum it up, "remove prop Div_mod" means that no proof obligations 
generated by Why3 will ever contain a line "Axiom Div_prop", yet the 
realization lib/coq/int/ComputerDivision.v does contain a line "Lemma 
Div_mod" that proves that ZOdiv and ZOmod match div and mod.

Best regards,

Guillaume



More information about the Why3-club mailing list