[Why3-club] Realized theories and "remove prop" declarations
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.
More information about the Why3-club