[Why3-club] Specializing theories containing axioms
guillaume.melquiond at inria.fr
Wed Apr 6 18:51:18 CEST 2011
We already had this discussion a few months ago, but I experienced the
issue again today, so I feel I should stress the point. Consider the
small example below, which formalizes a cheap axiomatization of ordinary
use import real.Real
use import real.Abs
logic f real : real
logic df real : real
axiom differential : forall x : real. forall eps : real.
exists delta : real. 0. < delta && forall dx : real. abs(dx) <= delta ->
abs((f(x+dx)-f(x)) - dx * df(x)) <= eps * abs(dx)
Then I added a specialization for the exponential function:
use import real.ExpLog
clone export Differential with logic f = exp, logic df = exp
I was expecting Why3 0.64 to ask for a proof that exponential is indeed
its own derivative. But it didn't happen because I had forgotten to add
a "lemma differential" clause to the "clone" statement. (Note that
changing "axiom" to "lemma" or "goal" in the original theory does not
make sense.) So, as it stands, it is way too easy to create arbitrary
properties you never have to prove and hence to inadvertently introduce
inconsistencies in the logic.
Why3 skipping proof obligations should not be the default behavior. The
user should have to explicitly indicate that there is no interest/sense
in proving some obligations, for instance by adding "axiom" clauses to
the "clone" statement. Forgetting "lemma" clauses during cloning should
never cause logic formulas to magically become valid, as it currently
happens! For the sake of conciseness, there could be a special "axiom *"
clause (or whatever the grammar allow) that would prevent all remaining
proof obligations from being generated.
PS: By the way, the formal grammar states that axiom/lemma/goal have to
be followed by uident/uqualid, while Why3 is perfectly fine with
lower-cased identifiers. And I'm too, as a user.
More information about the Why3-club