Add implicit NO_TAC to by

[xrchz]

When one writes subgoal by tac the intended semantics is usually that tac solves the whole subgoal, but by allows tac to not fully solve the subgoal. This should be changed.

[konrad-slind]

A common use-case for me is

.... by all_tac

so that the branch gets created for me to work on interactively. The proposal would result in

.... by (all_tac then NO_TAC)

which (should?) work out properly.

On Mon, Mar 13, 2017 at 6:11 AM, Ramana Kumar notifications@github.com wrote:

When one writes subgoal by tac the intended semantics is usually that tac solves the whole subgoal, but by allows tac to not fully solve the subgoal. This should be changed.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgDxv110yznNFJX4J1XyeXS2Ptg0-Zks5rlSRMgaJpZM4MbHl- .

[xrchz]

The emacs and vim editor modes have special commands for setting up subgoals interactively. I think the vim mode currently uses by ALL_TAC to do that, as you describe, but I think the proposed change to the semantics of by will make that raise an exception. However, I think the right approach (which the emacs mode does?) is to call the underlying primitive (Q.SUBGOAL_THEN) instead. If this is done behind-the-scenes by the editor, it seems fine, but if you have to type it out I can see that being annoying...

If this is a serious concern, then I wouldn't mind having an alternative infix, by1, that is like by but with the "must solve" semantics.

[mn200]

I'd prefer not to be too trapped by history here: if there's strong need, I'd prefer having the old behaviour under the name by1 (or byA or whatever).

[konrad-slind]

I guess the point is that I don't have to go back and edit the "by" to be "byA" later (or the reverse).

Konrad.

On Mon, Mar 13, 2017 at 5:42 PM, Michael Norrish notifications@github.com wrote:

I'd prefer not to be too trapped by history here: if there's strong need, I'd prefer having the old behaviour under the name by1 (or byA or whatever).

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-286266751, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD5GEg0dVhT_Fu3UwRw2DFZh6b7Jqks5rlcZsgaJpZM4MbHl- .

[thtuerk]

I agree with Conrad. Going through existing code and replace "by" with "byA" sounds very time consuming and possibly error-prone to me. I use similar to Conrad "by ALL_TAC" a lot to set up a subgoal. I use the pattern

`...` by ALL_TAC THEN1 (
  some lengthy tactic
)

This allows with the emacs mode to set up in the the subgoal and step through the proof of the subgoal easily. So, for me, changing the semantics of "by" would be very inconvenient.

While the proof above could be rewritten to

`...` by (
  some lengthy tactic
)

with the new semantics, this does not allow to easily step through the subproof while e.g. debugging a proof script. As Ramana points out, this can be solved by having a much more clever interface (e.g. emacs HOL-mode). However, this is not trivial and for me one of the beautiful things about HOL 4 is that it can be used easily in a minimalistic way. Renaming "by ALL_TAC" to "byA ALL_TAC" would need to take place in plenty of places. Therefore, I would prefer keeping the existing semantics of "by" and add an additional "by1" (or somehow differently named) operation that fails.

[mn200]

The correct approach to deal with the possible backwards incompatibility would be to redefine by at the top of the affected files:

fun sg by tac = sg byA tac

[jeremydaw]

But the problem with incompatibilities is not that an arguably minor change has to be made, but that when someone tries to make an old Script file, that proofs crash, and he/she has to delve into the file to find out where and why they crash, before making the arguably minor change

On 15/03/17 16:55, Michael Norrish wrote:

The correct approach to deal with the possible backwards incompatibility would be to redefine |by| at the top of the affected files:

|fun sg by tac = sg byA tac |

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-286648198, or mute the thread https://github.com/notifications/unsubscribe-auth/AJRQWIdcUab63s_e7kz-MQky_f3CBbF_ks5rl31dgaJpZM4MbHl-.

[konrad-slind]

You do need to support backwards compatibility. Having people remember an ever-growing mapping between old and treasured behaviours and new and improved behaviours for the same identifier is a full on pain. The change to Q.PAT_ASSUM still rankles, and I expect it will trouble me with proof scripts for years.

Konrad.

On Wed, Mar 15, 2017 at 12:55 AM, Michael Norrish notifications@github.com wrote:

The correct approach to deal with the possible backwards incompatibility would be to redefine by at the top of the affected files:

fun sg by tac = sg byA tac

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-286648198, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD-AZO9QquqWTx4BvQst1GGyfuxtsks5rl31dgaJpZM4MbHl- .

[xrchz]

This is turning into a more general discussion. Perhaps @myreen would like to comment on the original topic though, since I got the idea from him.

I'd probably like to stay out of the general discussion about backwards (in)compatibility: it comes up in many projects, and it's a tricky issue.

It sounds as if adding by1 with failing semantics is winning currently, leaving intact the by ALL_TAC interactive idiom used by people who eschew editor support.

[thtuerk]

I would prefer having a new by1. The keyword by is used really a lot and by nearly every HOL user. Changing its meaning sounds for me to very likely cause a lot of confusion. grep "by ALL_TAC" * -R --include "*Script.sml" in the HOL directory, i.e. looking for by ALL_TAC in src and examples finds 1780 usages. There are 10 more for by all_tac. These will surely break if changing the meaning of by. More seriously, it is unclear how many other uses of by, which is really used everywhere will break. Grep finds 29577 usages of by, but some of these will be e.g. in a comment.

I fear that such a change, which even requires changing the vim and emacs modes, would confuse lots of users. While with quite some work, one can quickly enough update the HOL distribution itself, it would in my opinion be a source of issues for a long time. Getting old code to run or explaining to new users why very simple looking examples found somewhere on the net don't work any more sounds problematic. The same applies to sporadic users of HOL as well. I know that a few months ago while working in industry with Coq and not following the HOL discussions by still every few weeks using HOL this would have confused me a lot. Moreover, there are large HOL 4 developments out there which are not part of the main HOL repository. Lots of work will most likely have to be invested to get these working again.

In principle, the idea of having by fail can lead to easier maintainable scripts. I looked at the usages of by a bit while grepping. Many are already safe. Often something like ... by DECIDE_TAC or ... by METIS_TAC[...] or by PROVE_TAC[...] is used, i.e. tactics are used that fail if they can't show the new subgoal. Idioms like by ALL_TAC THEN1 (...) are also safe. However, there are also many cases of ... by SIMP_TAC ... or ... by SRW_TAC .... These and others would clearly benefit from a failing by. However, I would really prefer a new variant with failing semantics instead of changing the semantics of the current one.

[mn200]

I am afraid that I'm with Makarius on this sort of issue: we shouldn't shackle the system with its history, and thereby lose the opportunity to create a better system for people who come to it fresh. (When teaching people the system in tutorials like those we're due to have this year at PLDI and ICFP, do you really want us to have to say: “Oh, you should use by1 because by has been reserved for another, worse, meaning?”)

Nor is "lots of work" required to get old scripts to work: one line at the top of files that are affected will be all that's required (as above). There are 83 files in the main distribution that will require fixing: I did

grep -R --include='*Script.sml' -i -l by.all_tac * | wc -l

to derive this number.

There are 10 files in src that I would fix by hand to illustrate the new style; the remaining 73 I would probably just use the redefinition to fix. Conversely, I suggest there are probably still more files that could benefit from having the improved by; I do not want to have to edit those instead. (As @thtuerk notes, making the change is certainly an improvement for existing files too: it makes them more maintainable.)

[mn200]

In essence: I'd prefer to make the relatively small number of current users suffer a little if there were some prospect of attracting an even greater number of new users, who might even stick around if they didn't have to learn a system full of ugly warts.

[thtuerk]

@mn200 I did not say that it is certainly an improvement! I did say it is an improvement in a comparably small number of cases. In fact, I argued that many use cases would brake, for many it is unclear what would happen, most cases are unaffected and a few might improve.

The usage of by to set up a subgoal is that common that even the emacs and vim interfaces would not work after the change any more!

For me, such changes achieve exactly the opposite of what you want. New users have a harder time learning, since old examples, manuals, mailing list stuff does not work any more. Having different definitions for common concepts like by in different parts of the source is very confusing. As a new user you can't even look at existing code in source and use patterns in your own proofs. That's why for me headers are problematic. Existing users have to invest serious amounts of work. Fixing 83 files is huge. Moreover, this is just an estimate based on "by all_tac". These are comparably easily fixed. The much more problematic cases are those that can't be recognised easily syntactically. Adding a header for changing by locally is just confusing and even worse than changing everything. Moreover, if you update your code only every few month or for example only with new HOL releases, such changes are very annoying and time consuming to put in. The necessary change is usually hidden in some checkin or git-hub issue (most likely closed by then). So you need to investigate whats going on and which headers to add. But just adding headers makes your files unmaintainable in the medium run.

So for me, for new users it is confusing, for very active current ones annoying and for infrequent users a lot of work and very upsetting.

For me, a good recent example is the change of Q.PAT_ASSUM. The documentation was not updated everywhere and there were even questions on the mailing list about it (see emails of 16th Jan 2017). It took me some time to figure out what was going on. If we can't even get it right in the HOL repository itself, people using HOL releases and developments not in the HOL repository have an even harder time. Getting it right for something as ubiquitous as by sounds nearly impossible to me. Older examples I remember are the removal of MEM, which still causes minor trouble for me sometimes.

[xrchz]

Just noting that I agree with @mn200 about not wanting to be trapped by history (something I also expect most new users to appreciate), and some minor points: the Vim mode will be very easy to for me to update, at least one frequent active user (i.e., me) would welcome the changed semantics.

[jeremydaw]

But new users won't appreciate the prospect - if they are warned of it - that their proofs won't run in 5 or 10 o 20 years time, unless they spend a large part of their time exploring why they crash, and fixing them.

What's the big deal, anyway, asking users who want new semantics of a function to type in a new name, even if it is more than two letters?

For that matter - since it has been suggested that existing proofs have fun sg by tac = sg byA tac added, what's the problem with asking those who want the new semantics to add fun sg byms tac = sg by (tac THEN NO_TAC) or fun sg byms tac = sg by (ALL_TAC THEN1 tac) (byms = "must solve"). (Am I right in thinking that's the meaning of what's proposed?)

the only reason we can read MS Word or pdf documents that were created years ago is that the developers of these systems have "shackle[d] the system with its history, and thereby los[t] the opportunity to create a better system for people who come to it fresh"

And when referees want to run my proofs as well as read my paper, they're not happy with proofs that run in Isabelle2005.

Incidentally, many years ago I decided to stick with Isabelle2005 rather than spend the time (then and as I foresaw, in the future) updating everything I'd ever proved. The particular issue I encountered then that led me to this decision was a change for which it was not so difficult to fix my proofs: rather the point was that the developers' reasoning for making their change was so pathetic that it showed that they just didn't care (or understand) about the value of keeping compatibility.

Sorry for the rant but this issue is exactly why I would never recommend anyone to start using Isabelle

On 15/03/17 22:42, Ramana Kumar wrote:

Just noting that I agree with @mn200 https://github.com/mn200 about not wanting to be trapped by history (something I also expect most new users to appreciate), and some minor points: the Vim mode will be very easy to for me to update, at least one frequent active user (i.e., me) would welcome the changed semantics.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-286717851, or mute the thread https://github.com/notifications/unsubscribe-auth/AJRQWHHLSaKhZUFDIz4l9si3aYJls_8vks5rl86ygaJpZM4MbHl-.

[mn200]

It's pretty clear from Isabelle's example that polished systems with relatively little regard for backwards compatibility can attract and retain new users. HOL4's record of attracting and retaining new users is miserable in comparison. Nor am I interested in developing a system whose specification is required to look as hideous as MS Word's because of a fixation with backwards compatibility.

I think it's relatively clear that a system with by specified as per Ramana's suggestion is better than one as it is implemented now. Given that, I don't want to be told “Ooh, you can't get there from here” and be trapped forever as the principal author of a needlessly inferior system.

[mn200]

Documentation is never perfect of course. Nonetheless, we continue to make it better, and to fix the bugs that arise. I also document serious backwards incompatibilities in the release notes: the change to MEM, changes to Holmake's behaviour, the change to PAT_ASSUM and others have all been explicitly mentioned there.

[thtuerk]

For me, one cannot easily compare Isabelle/HOL and HOL 4 in these respects. Instead of trying to minic Isabelle (and just getting a very poor version), it is in my opinion sensible to focus on HOL 4's strength and make it a good alternative system for people with different needs instead of a poor copy no-one uses. But this is a separate discussion.

For the concrete case: Isabelle / HOL has much better documentation than HOL 4, much easier maintainable declarative Isar proofs and the archive of formal proofs. For Isabelle, thanks to Isar most proofs can still be fixed comparably easily and many proofs are fixed by the Isabelle developers. That's why they can get away with even rather big backward compatibility issues. For me, it is not clear that Isabelle is popular because of the disregard for backwards compatibility. I agree with @jeremydaw that even with this, it is often a pain and there are for my taste too many compatibility issues. The success of Isabelle might have something to do with a principled system, but - I believe - more importantly with its great user interface, declarative proof language, its automation, ease of installation and good documentation. In contrast the strength of HOL 4 is for me that it has no user-interface to speak of. It allows you to easily write your own automation and can be used to implement own tools. It is great for writing things like CakeML, Anthony's ARM model, Holfoot or experimenting with things that require a lot of special automation like the PMATCH case expressions or quantifier heuristics. These are examples with lots of code that needs some degree of backwards compatibility.

I agree that one should not religiously preserve backwards compatibility. by is used a lot to set up subgoals that are solved later. This idiom is that well established that it is even used by the vim and emacs modes. by is used everywhere and it is in its current form in the system since ages. Changing something like this without a pressing need sounds like a very bad idea to me. I don't see a pressing need to change the behaviour of by. There is no bug, there is no problematic behaviour. It's just that for one of the common use cases of by a slightly different semantics would be nicer. The other common use cases would not work after the change any more, though. Making changes like this which cause a lot of trouble with backwards compatibility without significantly improving the system, HOL 4 is going to loose users instead of gaining new ones, I believe.

[mn200]

I don't want to mimic Isabelle in any technical way or create a poor copy. Rather, I want to mimic its success. You say that Isabelle is not successful because of its disregard for backwards compatibility, but rather because of a long list of great features. However, it is exactly this disregard that has allowed them to evolve their system so that it is now in a better state than it was in 2005. @jeremydaw may be wedded to that system, but wouldn't any new user prefer to work with Isabelle2016 instead? Notice how all of those great features you list are things that happened over the last 10 years.

I agree that HOL4's strength is its flexibility and ease-of-use when it comes to writing automation. Thankfully, changing by will not affect that because no-one would/should ever use by in any piece of automation.

The use of by in the editor mode implementations is a red herring; it will be trivial to modify their code.

I really do not want to be held hostage, and not allowed to make the system better. Affected users have a trivial fix to apply to old and new developments alike (if they want to stay in the "old world" with their new developments); new users get a better system.

[mn200]

Incidentally, all this love for

`goal` by ALL_TAC

seems symptomatic of coders’ Stockholm syndrome. That ALL_TAC is positively redolent of “code smell”. Much better to have a tactic sg with the following implementation:

fun sg q = Q.SUBGOAL_THEN q STRIP_ASSUME_TAC

allowing one to write

sg `goal`

which would presumably be followed up with a THEN1 or >- in many proofs.

[thtuerk]

@mn200 Let's please try to have a non heated, objective exchange of opinion. I find phrases like "red herring", "wedded to", "Stockholm syndrome" or "all this love for" offensive. No one wants to "hold you hostage" or prevent you from making the system better. I believe everyone involved is interested in making HOL better, we just discuss how this can be achieved.

About the red herring: Perhaps my command of English as a non native speaker is too poor, but a "red herring" is as I understand it is a deliberate deception. I did not want to deceive anyone and feel insulted by the suggestion! For me the editor modes are an important point. I never said that it would be hard to change. It is trivial. I argued that the "by ALL_TAC" is currently the standard way to set up a subgoal and used the editor modes as evidence.

I disagree about Isabelle. Of course to implement these new features, they needed to break some things. For my taste, they broke things more frequently than needed and often without good justification. An example are the frequent changes of how the default sets are represented. I still believe that one should find a decent balance between improving the system and breaking compatibility.

I agree that a proper subgoal tactic would be better than by ALL_TAC. However, no such subgoal mechanism exists currently. It should be added though. With the proposed change, one would use this to still be able to debug a proof script without special editor support for setting up subgoals. The fact remains that currently the by ALL_TAC idiom is used a lot. And this was just an example where the proposed semantics will break things. I don't see a way without a lot of work to change the old code decently and even if there was one, I would still believe the change confuses rather than helps new users because of legacy examples and documentation.

Redefine by at the top of each old file is not a solution for me. I believe things like this make developments very hard to maintain. I believe we have too much of this sort of thing in HOL already. I was just 1 h ago for example confused that the THEN1 tactical used by the definition of by in BasicProvers.sml is not the commonly used THEN1 from Tactical but one with the same signature and similar behaviour defined in BasicProvers.sml. It does not fail though, if the first tactic does solve the goal or the second one does not solve the first subgoal.

So, I just don't see a big enough benefit for changing the semantics of by. There is a minor improvement and huge disadvantages for me. I strongly believe that introducing a new by1 is better.

[mn200]

I don't mean to accuse you of deception with the phrase "red herring". You mentioned the editor modes more than once, and I believe it to be a distraction as it is not a user visible change. Thus the phrase.

We will have to agree to disagree: this discussion has made me more convinced that the proposed change is good for the system and worth pursuing. If my experience in making the change or using the system after it is made brings up new data I may change my mind of course, and then the change can be reverted.

I will try replacing instances of

`goal` by ALL_TAC

with the new sg tactic mentioned earlier so that documentation and HOL sources do not have that potential to confuse that you are concerned about.

[acjf3]

Don't really want to be dragged into this that much but I thought I'd offer a few opinions:

• The proposed new behaviour of "by" is probably better than the old one. For me it's what it should have been in the first place.
• The heavy use of "by ALL_TAC" is an unfortunate use case of the existing "by". Something else should have been used/available instead.
• Breaking compatibility shouldn't be taken lightly. Having a gung-ho attitude to making improvements is bound to ruffle feathers in a big way, especially given the effort that's required to first write and then fix proofs/code. I tend to agree that this shouldn't be a barrier to progress, even if the benefits of a change are relatively small compared to cost/annoyance. However, I have full sympathy for those that take the opposite view here.
• A better way of managing proof-rot is needed. Having to know (find out) what magic boilerplate is needed to fix things isn't good. Being tied to building/using an old version of a prover isn't great either. Perhaps each proof script should load a file that names the version of HOL that it was developed under, e.g. "kananaskis_11". These files could then be updated to reverse incompatibilities. Obviously some changes may be hard to reverse and I can't see this working well in all cases, i.e. when definitions change leading to incompatibles between theories. However, for light stuff like "PAT_ASSUM" and "by" it may be worthwhile. At the very least these version files could easy the task of coping with frequent disruptive changes - they'd also be a place to look if you'd been away from the system for a while.

[konrad-slind]

I like Anthony's last point. A general approach to incompatibility would be nice. For example, if I could deal with new behaviours for old names by (say)

open Kan10;

at the top of a proof script then I have a place to go look for changes when my scripts break upon the release of Kan11.

That might localize the place for looking up incompatibilities. Asking people to go back and read RELEASE notes seems to put the burden on the users rather than the developers.

Konrad.

On Thu, Mar 16, 2017 at 3:19 AM, acjf3 notifications@github.com wrote:

Don't really want to be dragged into this that much but I thought I'd offer a few opinions:

• The proposed new behaviour of "by" is probably better than the old one. For me it's what it should have been in the first place.
• The heavy use of "by ALL_TAC" is an unfortunate use case of the existing "by". Something else should have been used/available instead.
• Breaking compatibility shouldn't be taken lightly. Having a gung-ho attitude to making improvements is bound to ruffle feathers in a big way, especially given the effort that's required to first write and then fix proofs/code. I tend to agree that this shouldn't be a barrier to progress, even if the benefits of a change are relatively small compared to cost/annoyance. However, I have full sympathy for those that take the opposite view here.
• A better way of managing proof-rot is needed. Having to know (find out) what magic boilerplate is needed to fix things isn't good. Being tied to building/using an old version of a prover isn't great either. Perhaps each proof script should load a file that names the version of HOL that it was developed under, e.g. "kananaskis_11". These files could then be updated to reverse incompatibilities. Obviously some changes may be hard to reverse and I can't see this working well in all cases, i.e. when definitions change leading to incompatibles between theories. However, for light stuff like "PAT_ASSUM" and "by" it may be worthwhile. At the very least these version files could easy the task of coping with frequent disruptive changes - they'd also be a place to look if you'd been away from the system for a while.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-286987146, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgDy4ruIQcVjN2eOsu2wpQcatHhYR3ks5rmPB3gaJpZM4MbHl- .

[acjf3]

It should be possible to make supporting old behaviour incremental, i.e. Kan10 would open Kan11 and undo more changes. I can see the downside to this though. You could end up with a lot of scripts that make use of this mechanism instead of using the latest "official/better" methods of doing things. I can see it being most useful for stuff under examples/ and outside of the HOL repository, whereas stuff under src/ would be best kept up to date.

I think Konrad's point about shifting most of the burden to developers is certainly a valid one. When using a theorem prover, trust in it's future development is an important issue. You want to be confident that your efforts can last a reasonable amount of time without requiring an undue amount of maintenance.

[myreen]

I realise that I'm a bit late to this discussion, but I would just like to reply to what Ramana wrote:

Perhaps @myreen would like to comment on the original topic though, since I got the idea from him.

The idea came from a development where Ramana and I started using by1 with the following definition:

fun op by1 (q,tac) = q by (tac THEN NO_TAC)
infix 8 by1

Ramana and I wanted to move this by1 up so that it's in HOL. My intention was never for it to replace the current by. I agree with many of the concerns raised in this discussion of the implications of changing the current by.

How about keeping by as it is and instead insert by1 into HOL under a better name? I suggest from or via. The docuemntation should change so that new users use from/via instead of by.

[konrad-slind]

BTW, I just wanted to say that all my uses of "by" depend on the supplied tactic succeeding in proving the given quote-term completely.

But the more general point about backwards compatibility is important. It wasn't so long ago that someone on the mailing list was looking at some ancient CCS theories that surprisingly didn't take that much work to get going again. This was no doubt due to the fact that the underlying tactics hadn't been improved. Improvement is good! But having old stuff still run is also good.

Another name for by1: BY (it's very emphatic).

Konrad.

On Mon, Mar 20, 2017 at 1:50 AM, myreen notifications@github.com wrote:

I realise that I'm a bit late to this discussion, but I would just like to reply to what Ramana wrote:

Perhaps @myreen https://github.com/myreen would like to comment on the original topic though, since I got the idea from him.

The idea came from a development where Ramana and I started using by1 with the following definition:

fun op by1 (q,tac) = q by (tac THEN NO_TAC) infix 8 by1

Ramana and I wanted to move this by1 up so that it's in HOL. My intention was never for it to replace the current by. I agree with many of the concerns raised in this discussion of the implications of changing the current by.

How about keeping by as it is and instead insert by1 into HOL under a better name? I suggest from or via. The docuemntation should change so that new users use from/via instead of by.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-287687768, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgDy_xUcScbFhOJ2GTUN3inXfEAvfpks5rniGugaJpZM4MbHl- .

[thtuerk]

Sorry for disappearing from the discussion for some days. I was unluckily very busy moving to Stockholm and hardly online.

1) I like Anthony's idea about managing proof rot. As noted above, there is a danger of using it overly much. So I'm in favor of establishing the proposed policy of not using it in src. Moreover, I would encourage people to not use it in the examples directory much.

2) I'm in favor of adding a subgoal tactic. I personally find short names like the proposed sg very hard to read and understand. Therefore, I would like an alias with a longer, more speaking, more self-documenting name that makes reading proof scripts easier. How about having for example "SUBGOAL" or "subgoal"?

3) Similar to a subgoal tactic, a suffices tactic that correspond to suffices_by would be nice.

4) I still don't like changing the semantics of something as ubiquitous as by much. I still fear this might cause quite some work updating old scripts (which admittedly were perhaps not well written). I think for example of the proofs I saw LEM users write. Therefore, I would prefer an having "by1". About the name for "by1": I like the name BY best. If there are objection because of capital letters, from sounds good to me.

[jeremydaw]

Re naming a subgoal tactic, calling it SUBGOAL_TAC would correspond to a somewhat general pattern, xxx_TAC = xxx_THEN ASSUME_TAC (if I'm not mistaken, it would be SUBGOAL_TAC tm = SUBGOAL_THEN tm ASSUME_TAC

On 22/03/17 19:07, Thomas Tuerk wrote:

Sorry for disappearing from the discussion for some days. I was unluckily very busy moving to Stockholm and hardly online.

1.

I like Anthony's idea about managing proof rot. As noted above,
there is a danger of using it overly much. So I'm in favor of
establishing the proposed policy of not using it in |src|. Moreover,
I would encourage people to not use it in the |examples| directory much.

2.

I'm in favor of adding a subgoal tactic. I personally find short
names like the proposed |sg| very hard to read and understand.
Therefore, I would like an alias with a longer, more speaking, more
self-documenting name that makes reading proof scripts easier. How
about having for example "SUBGOAL" or "subgoal"?

3.

Similar to a subgoal tactic, a suffices tactic that correspond to
|suffices_by| would be nice.

4.

I still don't like changing the semantics of something as ubiquitous
as |by| much. I still fear this might cause quite some work updating
old scripts (which admittedly were perhaps not well written). I
think for example of the proofs I saw LEM users write. Therefore, I
would prefer an having "by1". About the name for "by1": I like the
name |BY| best. If there are objection because of capital letters,
|from| sounds good to me.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/407#issuecomment-288325749, or mute the thread https://github.com/notifications/unsubscribe-auth/AJRQWHRUhoaPj4zE0Grtwfyo_KyEVw4uks5roNbTgaJpZM4MbHl-.

[mn200]

Indeed, it's because of the existence of Q.SUBGOAL_THEN q STRIP_ASSUME_TAC, which perfectly emulates the old by behaviour except for the provision of the solving tactic, that I wanted to provide a shorter (admittedly more cryptic) alternative in sg. If people want a longer, more explicit form, it's already available. More later.

[mn200]

The issue with alternative names for the new behaviour is that it doesn't give the existing uses of by the benefit of the improved behaviour. I'd really like to have existing uses of

`subgoal` by simp[....]

fail if the simplification no longer solves the goal. I'm pretty confident that very few uses of ... by simp will expect the tactic to possibly not solve the goal, so this would be a big maintenance win for all those existing uses.

[acjf3]

Another option could be to make "q by tac" issue a warning if it fails to prove the subgoal (printing out the original subgoal). That would mean that scripts using "by ALL_TAC" will issue warnings and this could encourage the script writer to tidy things up.

The current Holmake behaviour does tend to hide warning messages. I wonder if this could be improved, e.g. have an option for printing them out?

With regard to a subgoal tactic, I prefer "SUBGOAL_TAC" with a short form "subgoal".

[thtuerk]

@mn200 I agree about subgoal by simp [....]. However, this is a just one among many use cases. Just a few figures (unreliable) I got from grep ... -R in HOL directory:

Unchanged:

5251 by METIS_TAC[...]
2040 by DECIDE_TAC
1926 by PROVE_TAC[...]
 176 by decide_tac

Improved:

1613 by RW_TAC ...
 648 by FULL_SIMP_TAC ...
 601 by SRW_TAC ...
 238 by simp ...
 196 by ASM_SIMP_TAC ...
 190 by IMP_RES_TAC
 116 by REWRITE_TAC ...
  95 by SIMP_TAC ...
  73 by rw_tac ...
  60 by srw_tac ...
  48 by ASM_REWRITE_TAC ...
  14 by full_simp_tac ...
   2 by asm_simp_tac ...

broken

1836 by ALL_TAC

So the majority of use cases of simple by-patterns would not be affected by the change. Quite a few would be improved, but nearly as many break. This is of course just a rough estimate based on some common patterns. So I don't believe it is worth breaking backwards compatibility for getting this benefit. As simple as replacing all occurrences of e.g. q by ALL_TAC with as suggested SUBGOAL_THEN q STRIP_ASSUME_TAC, one could replace by simp with BY simp. If one forgets some cases, it still works and nothing is worse than the original situation.

[thtuerk]

I like Anthony's proposal of adding a warning to by. One could even go further. One could add a mechanism to make such warnings fail hard instead of just printing a warning message.

[binghe]

Add my two cents here:

(my a little experience) in the past months I was porting old HOL88 code into HOL4, and I'm surprised that the work is so "easy" in the sense that all the old tacticals are still there and work as is, and basically I just re-play the proof again and make superficial changes and finish the porting work. The only thing which is not compatible sometimes, is GEN_ALL, in which the order of the universal qualified variables sometimes changed, and this breaks other code that build new theorems using a chain of SPECs.

If today I still need to port proof scripts written in more than 20 years ago (1994, to be precise), then it's not hard to imagine that, 20 years later some others still need to port the proof scripts that we wrote today. I'm sure that future people will be appreciated that today HOL maintainers didn't make too much incompatible changes.

On the other side, I see some other theorem provers almost never break the compatibility (e.g. Coq), but as the result, the API set are very hard to learn from beginner's view, because many API names do not make sense any more. Let's recall the "famous" changes from PAT_ASSUM to a pair of APIs (PAT_ASSUM and PAT_X_ASSUM) in which "X" indicates the removal of assumption just like other X series of tacticals. Such API changes are absolutely welcome from beginners' view, although it breaks many old scripts. I think, as long as the number of such incompatible changes are small and rare, people do can live with that. (if header libraries like "Hol88lib" can be provided to "fix" old scripts automatically, that's even better)