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
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.
So I'd just give a trivial pattern to the simproc so the conversion starts out with the full goal?
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.
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
Can you point me to a minimal example of how to use loopers?
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.
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
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.
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,
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.
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.
Thank you @Manuel Eberl !
Last updated: Dec 07 2023 at 12:30 UTC