Re: [isabelle-dev] Safe approach to hypothesis substitution
On 08/23/2010 12:30 PM, Thomas Sewell wrote: Hello again isabelle-dev. I should clear up some confusion that may have been caused by my mail. I was trying to avoid repeating all that had been said on this issue, and it seems I left out some that hadn't been said as well. This approach avoids ever deleting an equality on a Free variable during a 'safe' reasoning step. It will substitute with that equality but keep it in place. This is a significant change to the intermediate state of some tactic scripts, thus the incompatibilities, especially on induction. It is somewhat surprising there aren't more such incompatibilities. There's no truly safe way to delete an equality on a Free variable without inspecting the whole context. Naive questions: * why is inspecting the whole context infeasible? * why can't we just collect (and cache?) the Frees occuring in assumptions managed by assumption.ML and never delete equalities involving them? Since equalities are not deleted, care must be taken to avoid an infinite loop in which a substitution is repeatedly attempted. This is the reason for the uniqueness check - if x appears only in 'x = expr' then there is no more substitution to be done. Some subtleties were discovered experimentally: - 'x = y' should not be substituted if either x or y is unique, or else we enter a loop substituting x - y - x - 'expr = x' needs to be reoriented when it is substituted, or else hypsubst and simp will loop doing opposite substitutions. - 'x = y' is OK to substitute if y is a unique free and x is a non-unique Bound. This is what is meant by a 'useful' substitution in the comment. Other equalities, which would cause a no-effect or cyclic substitution, are referred to as trivial (abbreviated triv) in this code. The language should probably be cleanup up to use a consistent set of names. Sounds complicated, but cool. You adapted blast_hyp_subst_tac in that way too, right? The subtlety here is that blast tries to approximate the effect of that tactic in the search and has accuracy problems even now. The more complicated the substitution criterion, the more weirdness is induced here. With the current situation before the patch, the accuracy problems can be fully repaired it seems; what works best for blast is a simple criterion of substitutability which is decidable from the hyp (and possibly information that stays constant in the whole search) only. Let me address Alex's detailed comments: 1. In the HOL sources the algebra method is used to solve two problems about parity essentially by accident. No Groebner bases were involved, but the surrouding logic, which appeals to clarify_tac and a custom simpset, happened to solve the goal. With this change the simplified goal had an extra quantifier in it. Note that with this change terminal tactics operating in 'unsafe' mode - fast, best, etc - will call thin_triv_tac via Context_Rules and behave similarly to before. It is terminal tactics which take safe steps - like algebra - that are most likely to break. 2. Yes, count vars is a bit strange, as it will consider (%f. f) (%x. x) to contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp, which it gets right. Yours, Thomas. ___ 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 Tue, 24 Aug 2010, Andreas Schropp wrote: Naive questions: * why is inspecting the whole context infeasible? * why can't we just collect (and cache?) the Frees occuring in assumptions managed by assumption.ML and never delete equalities involving them? Assumptions belong to the foundation layer, i.e. they are conceptionally somehow accidental, even hidden. This is also the reason why using the old prems abbreviation is a bad thing: you can never be sure what it will contain, because Isar language elements are entitled to extend the hypothetical context as required internally, e.g. as done by 'obtain', but not by 'have'. Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. Anyway, I would prefer if the non-local behaviour of hyp_subst could be repaired without too many additional complications, i.e. by using the visible goal that it is offered in a sensible way. There are some further problems of hyp_subst that maybe Stefan Berghofer still recalls. We have been standing there many times before, but never managed to improve it without too much effort, or breaking too many existing proof scripts. The real trouble only starts when trying the main portion of existing applications, and also doing some performance measurements ... 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/24/2010 06:35 PM, Makarius wrote: On Tue, 24 Aug 2010, Andreas Schropp wrote: Naive questions: * why is inspecting the whole context infeasible? * why can't we just collect (and cache?) the Frees occuring in assumptions managed by assumption.ML and never delete equalities involving them? Assumptions belong to the foundation layer, i.e. they are conceptionally somehow accidental, even hidden. Why is the safeness of this equality-elimination not a property only dependent on the foundation layer? Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. I don't get this response: if a Free x is not mentioned in any assumes, the elimination of a hyp x=t can not affect provability of the goal, because any deductions involving x can be done with an arbitrary term of the same type (esp. t) instead, right? Anyway, I would prefer if the non-local behaviour of hyp_subst could be repaired without too many additional complications, i.e. by using the visible goal that it is offered in a sensible way. There are some further problems of hyp_subst that maybe Stefan Berghofer still recalls. We have been standing there many times before, but never managed to improve it without too much effort, or breaking too many existing proof scripts. The real trouble only starts when trying the main portion of existing applications, and also doing some performance measurements ... 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
Hi Thomas, Thomas Sewell wrote: I should clear up some confusion that may have been caused by my mail. I was trying to avoid repeating all that had been said on this issue, and it seems I left out some that hadn't been said as well. This approach avoids ever deleting an equality on a Free variable during a 'safe' reasoning step. It will substitute with that equality but keep it in place. Thanks for the clarification. I think I understand better now. Note that with this change terminal tactics operating in 'unsafe' mode - fast, best, etc - will call thin_triv_tac via Context_Rules and behave similarly to before. similarly? :-))) What different behaviour could occur? 2. Yes, count vars is a bit strange, as it will consider (%f. f) (%x. x) to contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp, which it gets right. So it's probably just the name that confused me... Best, Alex ___ 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
Andreas Schropp wrote: On 08/24/2010 06:35 PM, Makarius wrote: Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. I don't get this response: if a Free x is not mentioned in any assumes, the elimination of a hyp x=t can not affect provability of the goal, because any deductions involving x can be done with an arbitrary term of the same type (esp. t) instead, right? The safety concerns discussed here are not the only relevant design principle. If a method would peek at the assumtions in a context, you would get a different behaviour of lemma fixes x shows A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method Safe or not, this is obviously undesirable. Alex ___ 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/24/2010 07:51 PM, Alexander Krauss wrote: Andreas Schropp wrote: On 08/24/2010 06:35 PM, Makarius wrote: Just like global types/consts/defs, local fixes/assumes merely generate an infinite collection of consequences. The latter is what you are working with conceptually, but it is not practical. So the system provides further slots to declare certain consequences of a context to certain tools: simp, intro, elim etc. I don't get this response: if a Free x is not mentioned in any assumes, the elimination of a hyp x=t can not affect provability of the goal, because any deductions involving x can be done with an arbitrary term of the same type (esp. t) instead, right? The safety concerns discussed here are not the only relevant design principle. If a method would peek at the assumtions in a context, you would get a different behaviour of I am just talking about tracking Frees occuring in any assumptions, no general peeking at assumptions. But I get your point. And actually any tactic can peek at the assumptions, via examination of the hyps of the goal-state, so this is at best an unenforcable design consideration and nothing really changes by making this functionality available from assumption.ML. The more practical justification (opposed to the theoretical justification, which I alluded to above) of doing this in the context of equality-elimination might be that most of our tools are based on unification. So they should be closed under substitutions, meaning that if they can prove P, they can prove any well-typed substitutions of Frees and Vars in P? lemma fixes x shows A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method Safe or not, this is obviously undesirable. Well yes, but users have to be aware of the difference between an assume (extending the context) and an explicit goal assumption (not extending the context) anyway. Otherwise things like lemma x=t == t=x x=x proof - assume x=t thus t=x by (rule sym) show x=x by (rule refl) qed should work too without bracing or reording. Alex ___ 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/24/2010 09:13 PM, Andreas Schropp wrote: On 08/24/2010 07:51 PM, Alexander Krauss wrote: lemma fixes x shows A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method Safe or not, this is obviously undesirable. BTW: if you want to be even more conservative you take both fixes and assumes into account (are the Frees in assumes always guaranteed to be fixed?) when approximating safeness of equality-elimination. Then you would have to compare e.g. lemma shows !! x. A x == B x apply method and lemma fixes x assumes a: A x shows B x apply (insert a) apply method to observe the difference. Is that better or worse? ^^ ___ 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/24/2010 10:51 PM, Makarius wrote: On Tue, 24 Aug 2010, Andreas Schropp wrote: And actually any tactic can peek at the assumptions, via examination of the hyps of the goal-state A tactic must never peek at the hyps field of the goal state, and it must never peek at the main goal being proved. See also section 3.2 in the Isabelle/Isar implementation manual for some further well-formedness conditions that cannot be enforced by the ML type discipline. Section 3.2 only lists the following The main well-formedness conditions for proper tactics are summarized as follows. · General tactic failure is indicated by an empty result, only serious faults may produce an exception. · The main conclusion must not be changed, apart from instantiating schematic variables. · A tactic operates either uniformly on all subgoals, or specifically on a selected subgoal (without bumping into unrelated subgoals). · Range errors in subgoal addressing produce an empty result. Can someone provide a full list? Is everybody respecting all of them? I don't even know them ... BTW: this email asks a lot of questions about conformity to seemingly undocumented design principles. Please don't mistake that for aggressiveness or something. ^^ The LCF type discipline of the kernel prevents proving wrong results, but it does not prevent breaking tools, or violating higher structuring principles. What are those higher structuring principles? What does violation of them imply? One very important one is independence on logical details of the derivation of previous results. This forbids any tools using proof terms, e.g. Extraction, AWE, unoverloading, HOL-ZF. What is the motivation behind our proof terms if it is considered a well-formedness violation to use them? E.g. tools need to work uniformly for assumptions or derived facts, fixed parameters or locally defined entities. This means I should not do a case distinction based on if something is an assumption etc? That sounds reasonable, but why is it important? Logically an assumption is quite different from a derived fact: introducing an assumption weakens your results, whereas introducing a derived fact never does. Why do we try to blur the line here? What does this say about our equality-elimination criterion, which wants to check if there are any assumptions involving a Free? For historical reasons one can also have Frees that are not fixed in the context, or hyps that are not assumed. So is that a higher structuring principle? Can you list some more with motivations behind them? A good sanity check of some idea that involves the proof context is to see how it interacts either with 'have' or 'obtain' in Isar. I.e. the following should be conservative additions to the proof situation: have P x sorry This doesn't change the assumptions, so no interaction with that equality-elimination safeness approximation idea? or obtain P x sorry This adds the assumption P x, so hyps x=t are not eliminated, which may be more conservative than we need it to be, if there is no further assumption on x (but how realistic is that?). What is obtain without a where clause good for? It looks like a complicated way to write a have P x. The behaviour wrt obtain x where P x is right: this adds fix x assume P x, so hyps x=t are not eliminated, which is correct because we don't know P t so the elimination would loose information. These are just necessariy conditions on structural integrity wrt. the context, not sufficient ones. And are there sufficient ones? Is structural integrity of contexts important for that equality-elimination safeness approximation idea? Where is structural integrity of contexts used and established? You mentioned above that For historical reasons one can also have Frees that are not fixed in the context, or hyps that are not assumed., so this is not part of structural integrity for contexts? ___ 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
It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines. 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. 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. 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). To respond to Makarius' comment that the real trouble only starts when trying the main portion of existing applications, and also doing some performance measurements ...: I've run the simplest performance measurement I can: rebuilding HOL and HOL-ex. On my desktop machine at home: Pre-patch: Finished HOL (0:11:32 elapsed time, 0:11:30 cpu time, factor 0.99) With patch: Finished HOL (0:11:37 elapsed time, 0:11:33 cpu time, factor 0.99) On my desktop machine at work: Pre-patch: Finished HOL (0:07:24 elapsed time, 0:07:22 cpu time, factor 0.99) Finished HOL-ex (0:15:25 elapsed time, 0:15:21 cpu time, factor 0.99) With patch: Finished HOL (0:07:41 elapsed time, 0:07:41 cpu time, factor 1.00) Finished HOL-ex (0:15:30 elapsed time, 0:15:23 cpu time, factor 0.99) In both cases parallel features are off (ISABELLE_USEDIR_OPTIONS=-q 0 -M 1). Obviously this is only the beginning of the story. As I mentioned before there are some obvious performance improvements that can be made to the tactic itself, which I avoided for the sake of clarity. Whether the additional assumptions are slowing down other tactics is hard to tell. With regard to running a broader set of existing applications: I was hoping to get some agreement as to whether this is a desirable approach or not before investing much more time in repairing proof scripts. I've set the standard isabelle make -k test test running, which may produce interesting results but will more likely tell us that many proofs are broken in trivial ways. 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
