Commutativity of addition
Nathan Collins
Can anyone figure out why the 'lem_add_symmetric' proof is failing?
It's timing out, not returning a counter model, so maybe it's already
provable, but who knows? Attached is the TPTP file, with an axiom
added at the bottom that I thought I might need, but which doesn't
seem to help (it's been running for a half hour).
The example source, with a long comment explaining how I hope the
proof would go, including why I think I need that extra axiom, is also
attached (and available at [1]).
Cheers,
-nathan
Nathan Collins
I still don't understand why the extra axiom I mention in the comments
in add-symmetric.hs [1] isn't needed, so hopefully there isn't a bug
lurking here ...
The key to making this work was adding a '--no-ptr' option, as
suggested by Koen, that prevents the generation of pointer axioms
(what I actually implemented was a very simple and sound approximation
to Koen's suggestion: simply don't generate any pointer axioms. If it
turns out they're needed, then the theory will simply be too weak).
With '--no-ptr', the time for Paradox to find counter models went from
3 - 5 minutes to less than one second! Looking at the models I was
able to see that some things were returning 'bad' which should not
have. Adding the appropriate CF contracts (with a few false starts)
made the proof go through.
Specifically, I needed a separate 'CF -> CF -> CF -> CF' contract on
'lem_eqNat_trans' [2], in addition to its "lemma" contract. I don't
understand why this was necessary, but Paradox told me it was needed.
Still very painful, but we've actually proved something (relatively)
non-trivial, that makes real use of lemmas. For maintainability, it
might be good to be explicit about which other contracts a contract
depends on. Right now a contract depends on any contract for any
function it depends on (transitively). This could get confusing, like
hint databases in Coq.
-nathan
[1] https://github.com/cpa/haskellcontracts-examples/blob/2501b6f46f5798337b2cfd280a39eee19fc8ab13/yes/add-symmetric.hs
[2] https://github.com/cpa/haskellcontracts-examples/blob/2501b6f46f5798337b2cfd280a39eee19fc8ab13/Lem/EqNatTrans.hs
p.s. here's a (slightly edited) hcc usage example: while tweaking the
'lem_add_symmetric' I used '--only-check lem_add_symmetric' to make
all other contracts be assumed as axioms, and I used '--keep-tmps' to
keep the .tptp files around, so I could feed them to Paradox while
Equinox was running:
time ../src/hcc -o lem_add_symmetric yes/add-symmetric.hs -vk
Then, when 'lem_add_symmetric' finally checked, I checked everything:
time ../src/hcc yes/add-symmetric.hs -k --no-ptr
Writing add-symmetric.hs.add.tptp
["add"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_eqNat_reflexive.tptp
["lem_eqNat_reflexive"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_add_S_r.tptp
["lem_add_S_r"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_add_Z_r.tptp
["lem_add_Z_r"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_add_Z_r2.tptp
["lem_add_Z_r2"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_eqNat_trans.tptp
["lem_eqNat_trans"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_add_symmetric.tptp
["lem_add_symmetric"] are mutually recursive. Checking them altogether...
OK :)
Writing add-symmetric.hs.lem_eqNat_reflexive2.tptp
["lem_eqNat_reflexive2"] are mutually recursive. Checking them altogether...
OK :)
yes/add-symmetric.hs: all the contracts hold.
../src/hcc yes/add-symmetric.hs -k --no-ptr 52.16s user 2.11s
system 101% cpu 53.610 total
Without the '--no-ptr' switch it still works, but takes twice as long.
Koen Claessen
> I still don't understand why the extra axiom I mention in the comments
> in add-symmetric.hs [1] isn't needed, so hopefully there isn't a bug
> lurking here ...
Hm... I read those comments and do not really understand what you want
to achieve there. Perhaps you can explain this in the next telephone
meeting?
> (what I actually implemented was a very simple and sound approximation
> to Koen's suggestion: simply don't generate any pointer axioms. If it
> turns out they're needed, then the theory will simply be too weak).
Ah, genius. As long as we don't use higher-order functions, this will work fine.
> With '--no-ptr', the time for Paradox to find counter models went from
> 3 - 5 minutes to less than one second! Looking at the models I was
> able to see that some things were returning 'bad' which should not
> have. Adding the appropriate CF contracts (with a few false starts)
> made the proof go through.
OK, I am a bit surprised that Paradox found the models and Equinox
didn't (but I can see cases where this might happen, I just hoped it
wouldn't). In any case, perhaps we should add Paradox to the tool
chain as well, in which case we should be thinking about a way of
showing models from Paradox as Haskell counter examples too. (This is
harder, since I need typing information for this.)
/Koen
Koen Claessen
> 'lem_eqNat_trans' [2], in addition to its "lemma" contract. I don't
> understand why this was necessary, but Paradox told me it was needed.
This brings me back to a question we discussed on the phone when Simon was away.
What was the reason for separating CF out of the normal boolean
contracts? It seems to be one most often wants it there.
Simon, do you remember why we took it out? Was it simply to simplify
the definitions / implementation, or was there a deeper reason (i.e.
we could not express things that we wanted to express)?
In any case, Dimitrios, Nathan and I were speculating about some
syntactic sugar:
{ x | p x } -- boolean contract, may crash
( x | p x ) -- boolean contract, shorthand for CF&&{ x | p x }
Easy to remember because { }'s have a bump in them (so you may crash),
whereas ( )'s are amooth (so no crashing possible). :-)
/Koen
Simon Peyton-Jones
| contracts? It seems to be one most often wants it there.
|
| Simon, do you remember why we took it out? Was it simply to simplify
| the definitions / implementation, or was there a deeper reason (i.e.
| we could not express things that we wanted to express)?
No, it was just to simplify. Also, you might want a boolean contract like
{ x | head x > 1 }
where you want to accept (4 : error "urk"). If CF is built into boolean contracts you couldn't do that. So we took it out, reasoning that you can put it back in with &&CF.
But yes to syntactic sugar!
Simon
Nathan Collins
To clarify, my problem was not with whether CF is implicit in
predicate contracts. The "lemma" contract I have on 'lem_eqNat_trans'
is
{-# CONTRACT
lem_eqNat_trans ::: x:CF -> y:(CF&&{y: x `eqNat` y})
-> z:(CF&&{z: y `eqNat` z})
-> CF&&{qed: x `eqNat` z}
#-};;
But Paradox gave me a counter model where 'lem_eqNat_trans' crashed
when given some CF args that were *not* 'eqNat' to each other. So, I
added
{-# CONTRACT
lem_eqNat_trans ::: x:CF -> y:CF
-> z:CF
-> CF
#-};;
I have CFs on all arguments in both contracts.
I still think we want the sugar, but I don't think it's relevant to my
problem. My confusion was that I thought I only instantiated
'lem_eqNat_trans' on args that were 'eqNat' to each other, but I guess
Equinox has to consider a case where they are not 'eqNat'.
-nathan
Nathan Collins
> This is really cool and great to hear!
>
>> I still don't understand why the extra axiom I mention in the comments
>> in add-symmetric.hs [1] isn't needed, so hopefully there isn't a bug
>> lurking here ...
>
> Hm... I read those comments and do not really understand what you want
> to achieve there. Perhaps you can explain this in the next telephone
> meeting?
Thanks for taking a look. Hopefully I'm just confused about what
happens in the proof, but yes, I will try to explain in the next phone
meeting.
>> With '--no-ptr', the time for Paradox to find counter models went from
>> 3 - 5 minutes to less than one second! Looking at the models I was
>> able to see that some things were returning 'bad' which should not
>> have. Adding the appropriate CF contracts (with a few false starts)
>> made the proof go through.
>
> OK, I am a bit surprised that Paradox found the models and Equinox
> didn't (but I can see cases where this might happen, I just hoped it
> wouldn't). In any case, perhaps we should add Paradox to the tool
> chain as well, in which case we should be thinking about a way of
> showing models from Paradox as Haskell counter examples too. (This is
> harder, since I need typing information for this.)
Probably you inferred this, but the '--no-ptr' speedup for Paradox was
because the minimal counter model got smaller. It goes from size 5 or
6 to size 3 or 4 in the examples I tried.
Yes, adding Paradox to the toolchain sounds like a good idea. At
minimum, we could add an option that runs Paradox, to quickly look for
counter-models. A simple way to make the Paradox output easier to use
would be to
(1) mark all terms for which we have 'min' each time they occur
(e.g. with '$'). Equations we don't have 'min' for are often
irrelevant.
(2) mark each term as CF (e.g. with '~'), or not CF (e.g. with '#'),
or at least mark all the non-CF terms. Equations between a
function applied to CF args and a non-CF result are of particular
interest.
-nathan
Koen Claessen
> (e.g. with '$'). Equations we don't have 'min' for are often
> irrelevant.
Yes. Since Paradox finds minimal models (size-wise), and the way $min
is set up, there will always be exactly one element in the domain that
is not in $min.
> (2) mark each term as CF (e.g. with '~'), or not CF (e.g. with '#'),
> or at least mark all the non-CF terms. Equations between a
> function applied to CF args and a non-CF result are of particular
> interest.
Indeed. Good idea.
The main problem is that in this case, I cannot simply print out "the"
constructor term for a domain element (as I can do in Equinox). The
reason is that for any given domain element, there might be several
constructor terms that have that value (all having different types).
So I need to know the types of things.
I think it goes too far building all of this into Paradox.
Alternatives:
* I can synchronize the syntax of models from Paradox and Equinox, and
we make a special tool that reads the models in and displays them the
way we like.
* We import Paradox and Equinox as libraries.
/Koen
Nathan Collins
>> (2) mark each term as CF (e.g. with '~'), or not CF (e.g. with '#'),
>> or at least mark all the non-CF terms. Equations between a
>> function applied to CF args and a non-CF result are of particular
>> interest.
>
> Indeed. Good idea.
>
> The main problem is that in this case, I cannot simply print out "the"
> constructor term for a domain element (as I can do in Equinox). The
> reason is that for any given domain element, there might be several
> constructor terms that have that value (all having different types).
> So I need to know the types of things.
Sorry, I did not explain well. I'm not asking for the constructor; as
you say it's not well-defined. I'm just saying it could be useful to
mark the CF-ness locally. E.g. if
cf(!1) <=> $true
cf(!2) <=> $false
f(!1,!1) = !2
then it can be useful to know that 'f' takes CF args to a non-CF
result. So e.g. 'f' above might be easier to use if displayed as
f(~!1,~!1) = #!2,
where '~' means CF and '#' means not-CF, because then you can tell at
a glance how 'f' fails to be CF -> CF -> CF. Of course, this is only
helpful for CF -> ... -> CF, not more general properties. But in the
add-symmetric example these were exactly the mistakes I was making.
-nathan
Dimitrios Vytiniotis
One more thing:
It would be very helpful to only print function application equations for those applications that are in the min() table, and no more.
After all min() is special so let the printing of the model related to min() be special too! It should be quite simple to add to Paradox and Equinox?
thanks!
d-