Hanno Becker (Mar 07 2023 at 07:16): Hanno Becker (Mar 07 2023 at 07:16):Hi! (How) Is it possible to register a conversion with the simplifier (similar to a simproc), so that it is automatically tried as part of simp?
Manuel Eberl (Mar 07 2023 at 08:52):No, you're going to have to wrap it in a simproc. That's not very hard to do; simprocs are more general than conversions.
Hanno Becker (Mar 07 2023 at 09:09):So I'd just give a trivial pattern to the simproc so the conversion starts out with the full goal?
Manuel Eberl (Mar 07 2023 at 09:19):Ah, I see, I hadn't thought of that. Usually you do target a rather specific term structure when you do this sort of thing.
You can of course just register your simproc with a pattern like x, but it will be called on every single subterm of your term, i.e. quadratically often (in terms of your proof state size). If you do this, you ought to make sure your simproc fails fast when it fails. And even then there might be some performance impact. For a small closed-off development this may be fine, but if your development is something that may be imported by others it would be prudent not to enable this simproc by default.
There is another possibility that is not quite as nice but might have less overhead, namely to register a looper instead of a simproc. Off the top of my head, a looper is called when the simplifier has tried everything else, the goal is not solved and it does not change anymore either. The looper gets to see the entire goal (not just a subterm) and can do to it whatever it wants. In particular, it could apply a conversion to the entire goal (or parts of it).
Not sure which is better for your use case.
Hanno Becker (Mar 07 2023 at 09:21):Wow, thanks. I had never heard of loopers, but that seems like the right thing here -- I want the conversion to be called on the _entire_ subgoal only, as it needs to selectively apply different simplifications for assumptions and conclusions, and in the conclusion there are further refinements
Hanno Becker (Mar 07 2023 at 09:22):Can you point me to a minimal example of how to use loopers?
Manuel Eberl (Mar 07 2023 at 09:25):Yeah this is pretty arcane Isabelle lore. Not many people know about it these days, I think. The only looper that I am aware of is the one that does case splitting.
Manuel Eberl (Mar 07 2023 at 09:29):You can just grep the AFP or the distribution for addloop, but I don't think there are very many helpful examples. The splitter is in ~~/src/Provers/splitter.ML.
Manuel Eberl (Mar 07 2023 at 09:33):I looked through my extensive collection of half-finished gadgets and found the following experimental code for normalisation of commutative monoid expressions. It registers a looper in order to get to see the entire proof state and then applies a targeted rewrite step. Definitely not a minimal example, but probably one of the few actual uses of a custom looper.
Manuel Eberl (Mar 07 2023 at 09:43):Just another thought, do remember that the goal will always be of type prop, so if you want to match only the goal, you could also do a simproc that matches on the pattern p :: prop or, in HOL, Trueprop p.
The main problem there is that you basically have no way to distinguish whether the thing you get to see is the goal or a premise. If you just do Trueprop p you only get the assumptions and premises; if you match on p :: prop you will also get terms of the form asm1 ⟹ asm2 ⟹ goal.
Hanno Becker (Mar 07 2023 at 09:56):I see... perhaps I should abandon the idea of integrating said simplification into simp, and just wrap it in a separate tactic. At the least, one can give a name to (simp | conv_based_tactic)+ if that happens to be invoked many times.
Hanno Becker (Mar 07 2023 at 09:57):Thank you @Manuel Eberl !
Last updated: Dec 07 2024 at 16:22 UTC