[Why3-club] Specializing theories containing axioms

Guillaume Melquiond 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
differential equations:

        theory Differential
          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:

        theory Exp
          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.

Best regards,


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 mailing list