From: Laurent V. <lpv...@gm...> - 2010-03-25 12:03:59
|
Dear Ken, Le 25 mars 10 à 06:31, Ken Robinson a écrit : > Dear J-R and fellow Rodin/Event-B devotees, > > On 25/03/2010, at 06:02 AM, Jean-Raymond Abrial wrote: > >>> I very much appreciate all the help one gets in this group. > >> Yes, at the moment this group is very active. People are very >> interested >> and enthusiastic. I am just hoping that this will continue in the >> future. > > I would like to echo these thoughts. > > I've been taught two very interesting lessons in the last two weeks > via this forum. > > Most recently was the advice from Kimmo Varpaaniemi advising a > strategy involving contradicting the goal and then showing that the > hypotheses are false. > > Logically this must work, but I would never have used it, although > now I believe I can think of cases where it would have simplified > the proof. > > What interests me is that I wouldn't have used it because I wouldn't > have thought there would be any point of using it. > > The point of interest is that it reveals something interesting about > the provers, not proof itself. > > The second was the help I got on my own problem from Christophe and > Matthias. > > The goal was > > X → Y≠∅ > > where X and Y are finite sets. > > Christophe's directions: > > you can build the proof in the following way : > > from Y/={} you can derive x:Y > > then > you rewrite not ( X-->Y) = {} > > You obtain #x . x : X-->Y > > Then propose the following witness X*{x} > > Looked fine, but I hadn't the foggiest idea of how to execute them. > > Matthias eventually overcame my ignorance and all was fine. > > Except the strategy was bizarre. > > There were hypotheses that once proved were regarded as true and > eliminated from the hypotheses. I'd seen that happen before and > never understood what was happening. I'd never thought of > backtracking to uncover an earlier proved hypothesis. This happens when the hypothesis is considered as useless in the general case. The point in doing this is to reduce clutter in the hypothesis stack. For instance, a hypothesis of form x : Y where Y is a type is considered useless as it is a property of the typing of variable "x", and is not providing any additional information. I nevertheless understand that, here, this property is exactly what you intended to create and that the prover appears deceptive. Design decisions are always debatable and one size doesn't fit all. However, there is another way out that the one you described. The prover is highly configurable. In this case, if you look at the proof tree, you see that your hypothesis has been removed by a reasoner labelled "type rewrites" which has been fired automatically (that is by the post tactic). By clicking on the small down-pointing triangle which appears in the top right of the "Proof Control" window title bar, a menu pops up. Select "Preferences..." in this menu. This is a rapid shortcut to the configuration of the post-tactic. Then, in the right-hand pane, you will see an automated tactic called "Type Rewriter (Simplify)" (as an aside, we're currently working at making these labels more consistent with each other). Click on this tactic and click on the "<<" button to remove it from the post-tactic, then click "OK". From now on, the post-tactic will not perform this kind of simplification anymore. > And there were other things that were a long way from intuitive. > > Apologies for this long ramble, but there is a point. > > And the point is that both of these lessons revealed a lot about the > prover rather than proof as such. > > You have to remember that both of the above goals were trivially > obvious, and there was nothing clever about the final proof. It was > all about how to drive the prover. > > And this happens often. For this particular case, my understanding is that such lemmas shall be discharged automatically and you should not have to spend time with such trivial properties. However, whatever the effort we put in improving the automated provers, there still will be cases where one needs to resort to interactive proof, so your point is very relevant. > Is there any documentation anywhere that helps you to understand how > to drive the prover. There is part of it on the wiki, but it is spread in various places and far from sufficient. We're currently working on better documenting the various tactics, with the stress put on describing their purpose and use cases where they are useful. However, this is not yet available. Currently, the best available documentation remains the tutorial: http://wiki.event-b.org/index.php/Mathematical_proofs_%28Rodin_Tutorial%29 > Otherwise, I am worried. I spend a lot of time discharging POs that > are obvious, but they take more time to prove than I would have > thought reasonable. We would be very happy to get feedback in this area. If you often encounter lemmas that look trivial to you, please report them on this mailing list, or even better, enter a Feature Request on the SourceForge web site. This will make us aware of your typical problems and allow us to tackle them. Another option would be to use the rule-based prover (available as a separate plug-in from the Rodin update site). With this prover, you can enter your own proof rules in a friendly manner in so-called theories (only rewrite rules in the current version, but inference rule will appear this year). This is quite similar to the approach used by the B toolkit or Atelier B. However, there is one difference, you need to prove your rule correct (or at least review it) before using it. But, even if you take this route, please let us know the rules you felt interesting to add. This is very interesting feedback for us to improve the general prover used by everybody. > If I am correct then this is bad news for Rodin, and indirectly > EventB. That's not intended to be a criticism; it's a heartfelt > concern. > > It is necessary to understand the underlying tactics of the > provers. You see it all the time. There are all these red > operators and it's not clear what to do with them. Some times > selecting them works miracles (genuinely) and other times it seems > to send you off on a wild goose chase. Most of the time, when a tactic is not applied automatically, it is because of this risk of leading you to a dead end. So, in general, "red operators" are a double-edge sword and need human expertise to decide whether and when to click on them. I completely understand that taking this decision when you have no idea of what clicking on the operator would do is a very frustrating experience. Hence, the work we've already started on documenting them is really needed. > I don't think that is very good, and it means that this wonderful > community is sometimes spending a lot of time on things that should > be trivial. > > I hope someone is going to tell me that I've missed something and my > concerns are wasted. :-) > > Hoping. As usual your concerns are very helpful to us and to the point. I'm however happy to see that, this time, we started addressing them before you expressed them strongly. From the bright side, your constructive criticism is reinforcing the impression we are on the right track (albeit a bit late, this tactic documentation should have started earlier). Cheers, Laurent. |