Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Whoops. It's both a typo and use of the wrong release. The patch happens to work against Isabelle2013-1 or Isabelle2013-2, since there are no relevant differences in the theory sources. I can confirm that isabelle build -a works in either 2013-1 or 2013-2. Short version of the story, I forgot the name of the newest release. Long version: The confusion was caused in part because the newest l4.verified branch is called '2013-1'. It contains Isabelle 2013-2, but the switch was accomplished so straightforwardly that we didn't end up with a new branch name. Apologies about the confusion, Thomas. On 16/01/14 02:00, Makarius wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
The name makes sense: thin refers to deleting the assumption. It is ugly of course, which will be an incentive for users to update their proofs. Larry On 15 Jan 2014, at 15:05, Makarius wrote: > On Tue, 14 Jan 2014, Thomas Sewell wrote: > >> If there is some collection of proofs that are especially bad, we can just >> declare [[ hypsubst_thin = true ]] > > Larry, you are the original author of hypsubst. > > Does the "hypsubst_thin" terminology make sense to you? It is used here both > for the configuration option and its attribute, and the alternate proof > method that has it already enabled. > > For me it does make sense, i.e. we don't need to make it explicitly "legacy" > in the wording. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] Larry, you are the original author of hypsubst. Does the "hypsubst_thin" terminology make sense to you? It is used here both for the configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly "legacy" in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
This sounds great! You seem to have done everything right. Having the compatibility mode will make it easy to get everything working again quickly, with the conversion to the new setup becoming a background task (possibly to be combined with refactoring horrible old proofs). Larry On 14 Jan 2014, at 13:43, Thomas Sewell wrote: > For those reasons I'd prefer to plough ahead as long as the impact is > manageable. I'll test the AFP and ISABELLE_FULL_TEST soon. I'm running out of > energy for this side project, however. If there is some collection of proofs > that are especially bad, we can just declare [[ hypsubst_thin = true ]] > globally in them, but I hope to avoid that for the same reason as (2) above: > having invisible adjustments to standard tactics seems like something we > should avoid. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Hi Thomas, Am 14.01.2014 um 14:43 schrieb Thomas Sewell : > To address Jasmin and Larry's concern, it is possible to switch back to the > "compatibility mode" by setting a config variable in the context, or by > calling the ML version with an extra parameter. Any legacy proof script can > be repaired by adding the line "using [[ hypsubst_thin = true ]]" before any > apply/by line. That's perfect. > I understand why Tjark and Larry would prefer a minimal change, using > contextual information to decide when to deviate from the old behaviour. It > would certainly create less maintenance work. Let me elaborate why this > approach is my first preference: > [...] > 2) Having the behaviour of tactics change because of largely invisible > background concerns seems a recipe for confusion. This particularly applies > to building-block tactics such as safe and clarify. I would prefer they be > predictable and reliable. Yes. While I agree with Tjark in principle, it appears to me that the syntactic conditions you described are weird enough (even though they make sense upon reflection) that they would confuse users, possibly even those who have been following this thread. Regards, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Note that this change would affect auto, force, fast, etc. Possibly a “legacy” version of auto would help with compatibility, or otherwise some sort of option setting to (locally) restore the old behaviour in all affected methods. Larry On 13 Jan 2014, at 15:47, Makarius wrote: > With an easy escape, i.e. the alternate name of the proof method and a > confifuration option to recover the old behaviour, users should manage to > convert their old stuff reasonably well. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Mon, 13 Jan 2014, Lawrence Paulson wrote: I think the problem is that the unsafe situations cannot be detected locally, i.e., there is no way for the tactic to know that a particular free variable is actually a locale constant. Indeed. The proposed change is basically some form of "localization" of hypsubst, in the sense that it does not make implicit assumptions how free variables got introduced, their scope etc. In ancient times, a Free was fixed in the immediate scape of the goal state, but that is long past. the current treatment of contexts may make this information available after all. That is a very old topic, and there are various ideas in some drawer that have accumulated a lot of dust. It could easily take a few more years to revisit that. It somehow belongs to the national debts problem from 2006. Since December 2013, I am again improving the situation concerning the formal proof context within proof tools, notably the Simplifier and its add-ons. It is always surprising how long really tiny steps take, e.g. see current Isabelle/f26a7f06266d. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Mon, 13 Jan 2014, Thomas Sewell wrote: Given a hypothesis of the form "x = Suc a" or "Suc a = x", where x is a free (blue) variable, hypsubst will substitute "Suc a" for x throughout the goal, and then discard the hypothesis. The substitution is almost always wanted. Discarding the hypothesis may, however, be unsafe, since there may be facts about x at the proof or locale level that now cannot be used. It may also be unsafe in the subtle case where a schematic variable in the goal can be instantiated to functions of x but not of "Suc a". This unsafeness is undesirable because hypsubst is called from tactics that are meant to be safe. Here's what's changed: 1) the new behaviour is to keep hypotheses of the form "x = Suc a" where x is free, and to reorient equalities of the form "Suc a = x" (to "x = Suc a", which is kept). Equalities on bound variables are still removed immediately. 2) when any action is taken (substitution or reorientation) and a hypothesis kept, it is moved to last place amongst the hypotheses in the goal. This is different to my previous proposed patch. I suspect it might reduce the number of times the new hypotheses are picked by erule or similar in old scripts. I do not yet have any empirical evidence this helps. 3) the old behaviour is provided via new method hypsubst_thin and Hypsubst.hyp_subst_tac_thin in ML. The setting [[ hypsubst_thin = true ]] also restores the old behaviour, and can be used to repair otherwise unrepairable proofs.Some of these features might need a better name. This sounds quite reasonable to me, although I am not a proven expert of hypsubst. Whenever I had a question about it in the past, I would first consult Stefan Berghofer. As I've already pointed out in the discussion some years ago, the "proof of correctness" of such a change works empirically, against the body of existing applications in the Isabelle repository and AFP. You have also access to classified L4.verified material, and might take big external projects like IsaFoR into account. The changes so far appear to be below the level of significance -- we've had much more substantial upheavals in the past. With an easy escape, i.e. the alternate name of the proof method and a confifuration option to recover the old behaviour, users should manage to convert their old stuff reasonably well. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
I’m impressed with your determination to slog through so many changes, but I am not sure that we have the right to impose this on our users, which is why I would prefer one of the other solutions, namely (1) contextual information if available (2) some sort of compatibility mode. Thank you very much indeed for taking up this matter again, because I do believe it is important. Larry On 13 Jan 2014, at 12:38, Thomas Sewell wrote: > If there's interest in getting this change installed, I'll slog through > these, and then figure out what's broken and what's expected to be broken in > the latest tip of Isabelle and in the AFP. I'd call for volunteers to help > with that bit though. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
I think the problem is that the unsafe situations cannot be detected locally, i.e., there is no way for the tactic to know that a particular free variable is actually a locale constant. I could be wrong: the current treatment of contexts may make this information available after all. That would be the best solution. But if this contextual information is not available, then I think that some sort of compatibility mode will unfortunately be necessary, given the number of instances where introducing the safe behaviour causes proofs to fail. I have to say, in most cases these are tricky proofs that refer to specific assumptions, but lots of these still exist. Larry On 13 Jan 2014, at 12:50, Tjark Weber wrote: > I will freely admit my ignorance of the issues involved, but perhaps it > would be desirable to identify these unsafe situations in the code and > discard the hypothesis if (and only if) doing so is safe? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
> If there's interest in getting this change installed, I'll slog through > these, and then figure out what's broken and what's expected to be broken in > the latest tip of Isabelle and in the AFP. I'd call for volunteers to help > with that bit though. > I would very much appreciate such a change to hypsubst! (Having thought of doing this patch myself several times, not knowing about the older discussion on this list ;) ) -- Peter > All comments welcome, > Thomas. > > > > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Hi Thomas, Am 13.01.2014 um 13:38 schrieb Thomas Sewell : > The change requires, for instance, about a dozen lines of changes to the > files in HOL/Library, which contain about 50K lines of proof, or 3 lines of > changes to HOL/Bali, with 30K. The change to the Nominal examples (30K), > however, is a bit longer (100 changes) and a bit more unpleasant. I've also > checked the change against one chunk of L4.verified, with 70K lines in it, > and have around 60 lines of changes to make. From my perspective, this level > of impact seems to be annoying but not too annoying. I'm interested in what > others think. Your suggested change looks very reasonable to me. However, if possible, it would be nice if the old behavior could be kept via a flag -- unless it's easy to simulate reliably (e.g. using "thin_rl"). One reason for my concern is that the new (co)datatype package's tactics rely extensively on "hyp_subst_tac" and we currently don't have enough tests in the repository to catch all failures. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Mon, 2014-01-13 at 12:38 +, Thomas Sewell wrote: > Given a hypothesis of the form "x = Suc a" or "Suc a = x", where x is a > free (blue) variable, hypsubst will substitute "Suc a" for x throughout > the goal, and then discard the hypothesis. The substitution is almost > always wanted. Discarding the hypothesis may, however, be unsafe, since > there may be facts about x at the proof or locale level that now cannot > be used. It may also be unsafe in the subtle case where a schematic > variable in the goal can be instantiated to functions of x but not of > "Suc a". This unsafeness is undesirable because hypsubst is called from > tactics that are meant to be safe. I will freely admit my ignorance of the issues involved, but perhaps it would be desirable to identify these unsafe situations in the code and discard the hypothesis if (and only if) doing so is safe? Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
