Re: [isabelle-dev] Safe approach to hypothesis substitution
I'm pretty sure this one is a bug. Try typing this into your favourite Isabelle session: lemma foo: "fwrap f = (%v. f v) ==> P f" apply clarify And note the system hangs. I think this is a pretty good argument to support the case that it doesn't occur in any existing Isabelle scripts. Just to be safe, though, I can test this change in isolation against all the HOL libraries and the AFP thisevening when my machine has spare CPU time. I guess I should test against Isabelle 2009-2 rather than a development snapshot since the AFP will be known to build? Yours, Thomas. On 26/08/10 02:49, Makarius wrote: On Wed, 25 Aug 2010, Thomas Sewell wrote: Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Often it is hard to tell what is a bug or an obscure feature required like that by some other tool. Anyway, I recommend to try that tiny bit of the change on all existing Isabelle + AFP theories. Then we can apply it independently, with a more informative log message that "fixed bug", though. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On Wed, 25 Aug 2010, Thomas Sewell wrote: Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Often it is hard to tell what is a bug or an obscure feature required like that by some other tool. Anyway, I recommend to try that tiny bit of the change on all existing Isabelle + AFP theories. Then we can apply it independently, with a more informative log message that "fixed bug", though. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On Wed, 25 Aug 2010, Thomas Sewell wrote: Indeed bounds, frees and consts can all be seen as the same kind of thing. At the moment the only real benefits of hyp_subst over asm_full_simp are robustness in the case of Vars and the capacity to reorient equations in order to rewrite bounds -> frees -> expressions. Adjusting this to rewrite bounds -> frees -> consts -> expressions would be easy - is this what you are asking for? I don't see this as widely useful, but perhaps you have an application in mind. Your bounds -> frees -> expressions already sounds quite good. In the end you need to 'prove' it empirically against the existing setup of other tools, and usage in concrete applications (Isabelle repos and AFP). It looks like there is a good chance to manage that. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Let's try to answer everyone again: Alex: I think I was wrong about the cases involving algebra. There may be something interesting going on. The prenormalisation phase calls clarify_tac, then full_atomize_tac, then some other stuff. With a Free variable x assumed to be even, the resulting goals with the old and new versions of hypsubst are of the form "ALL k. P (2 * k)" and "ALL k. x = 2 * k --> P (2 * k)". It's possible that the quantifier elimination process that follows doesn't know what to do with the additional implication, or maybe just its left hand side. If the same problem occurs for more interesting examples, it could be fixed by following clarify_tac with Hypsubst.thin_triv_tac in groebner.ML. Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Makarius: Indeed bounds, frees and consts can all be seen as the same kind of thing. At the moment the only real benefits of hyp_subst over asm_full_simp are robustness in the case of Vars and the capacity to reorient equations in order to rewrite bounds -> frees -> expressions. Adjusting this to rewrite bounds -> frees -> consts -> expressions would be easy - is this what you are asking for? I don't see this as widely useful, but perhaps you have an application in mind. Finally, the full run of "isabelle make test" is indeed quite broken, including apparently going into a loop while defining a record in Hoare_Parallel. I'll look into it. Yours, 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-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On Wed, 25 Aug 2010, Andreas Schropp wrote: What does this say about our equality-elimination criterion, which wants to check if there are any assumptions involving a Free? It does not want to check that, and the version by Thomas does not do it. In fact his approach looks like going in the right direction. Going back tp that, it has already been mentioned that goal parameters (bounds) can somehow be treated as private to the proof state, while frees can reach back into the context arbitraily. In fact, a Free is just like a local Const in most situations, i.e. Free/Const are only different in their scopes. Is there any chance to get a practically useful version of hypsubst that does not distinguish local constants (Free) from constants of the background theory (Const)? Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/25/2010 07:57 AM, Thomas Sewell wrote: It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines. Sorry for that. ^^ I'm trying to steer clear of contexts - it would seem more elegant to me if there was a purely tactical solution to this problem. Well as you said There's no truly safe way to delete an equality on a Free variable without inspecting the whole context. To answer Andreas' question about blast_hyp_subst_tac: I made some attempts, but it seemed that making blast_hyp_subst_tac share behaviour or even code with the other versions led to incompatibilities I didn't really understand. The patch I sent keeps blast_hyp_subst_tac strictly in compatibility mode with previous behaviour. Ahh, ok. I think you've outlined why there was a problem - blast is guessing incorrectly what the tactic will do. Perhaps in the future the Hypsubst ML structure could export its eq_var and triv_asm term inspection functions so blast would have a better idea what it would do (assuming blast can construct accurately what the subgoal passed would be). Blast has a different term structure with Skolems replacing Goal-Parameters etc. In the current architecture there seems to be no easy way to get a subgoal of the search back as an isabelle subgoal. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
Hi Thomas, Thomas Sewell wrote: It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines. There is still hope if we move the unrelated discussions to another thread... I have another small comment on the issue with "algebra": You were saying that the goals were solved in the presimplification phase together with clarify. Are you sure about this? I played a little with the theory, and it seemed to me that it is only solved using the fact "dvd_mult2", which is not used in the presimplification rules. Thus, clarify leaves behind an assumption which somehow confuses the following code. I am not sure what assumptions are made by the following code, but maybe it should be able to ignore additional assumptions...? Maybe Amine Chaieb can comment on this further, but it may take a while to get an answer... As you say, terminal methods that break with the patch are problematic, so we should try to understand this, even if we decide in the end that it is a problem of the algebra method. One more small thing: @@ -115,27 +116,55 @@ | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t then raise Match else false (*eliminates u*) - | (Free _, _) => if bnd orelse Logic.occs(t,u) orelse + | (Free f, _) => if bnd orelse Logic.occs(Free f,u) orelse novars andalso has_vars u then raise Match else true(*eliminates t*) - | (_, Free _) => if bnd orelse Logic.occs(u,t) orelse + | (_, Free f) => if bnd orelse Logic.occs(Free f,t) orelse novars andalso has_vars t then raise Match else false (*eliminates u*) | _ => raise Match; How is this change related to the rest? It seems to me that the only difference between (Free f) and t/u is only the possible eta contraction... So my question should rather be: Why was this correct before? Alex ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
