HOL-Theorem-Prover
Consider implicational rewriting tactics
https://github.com/aravantv/HOL4-impconv
Also, the current implementation of HINT_EXISTS_TAC in HOL4 is somewhat broken, and I think fixed up in the above.
Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
I'd be happy to see this code integrated if you think it's useful. (You've tried using it.)
I tried, but without a huge amount of success. I think it may either still contain bugs or I was using it incorrectly. I'd need to put more time in, but ideally the author could do the integration as a pull request along with a small example theory showing it works... I'll ask.
I only had a brief look at the description. As it looks to me, there are a lot of connections of this library with the existing consequence conversions and quantifier heuristics libraries. Depending on how much work it is to fix HINT_EXISTS_TAC, it might be worth implementing it using the quantifier heuristics library. It should be straight-forward using unjustified guesses. In fact, if I understand the documentation of HINT_EXISTS_TAC correctly, the existing quantifier parameter conj_lift_qp already leads to similar (if a bit more general) behaviour.
For what it's worth there is also something like HINT_EXISTS_TAC in CakeML's "miscLib" (https://github.com/xrchz/vml/blob/master/miscLib.sml) called "match_exists_tac".
If both of them can be implemented using quantifier heuristics technology maybe that's the right way to go, at least for HINT_EXISTS_TAC.
I believe "match_exists_tac" is tricky, since it can instantiate multiple variables at the same time. It is a big short-comming of the quantifier heuristics library that this cannot be done easily. However, perhaps "QUANT_TAC" might be sufficient in some cases? It is more convenient than "EXISTS_TAC", but has the same main problem: instantiations have to be given explicitly :-(
Hi all,
- to answer a personal message of Ramana: no I have not made any progress on this tactic, unfortunately I am now working in a completely different field and have very few time to update this (it does not mean that I am not interested though; just that I don't have a lot of resources to allocate to that)
- however, I can fix things on my side if you can provide me with some broken use cases.
- I unfortunately really don't have a lot of time to work on a use case library... I have one with the HOL Light version of the tactics but it relies on Harison's vector library which I don't think is available in HOL4? If I'm wrong it might be easy to adapt this example library to HOL4 too...
- regarding HINT_EXISTS_TAC in particular, it would indeed be better to integrate the one in the new library, which normally should work much better (again based on my rudimentary tries, and on the assumption that it works just like it works in the HOL Light version)
- to answer Thomas: yes the background library that I developped (namely "implicational conversions") is I think indeed very close to the consequence conversions (that I think you developped (?) ); therefore it would be a pity not to adapt the implicational rewriting tactic to your conversions; however I really cannot spend myself the time required to 1. understand how your conversions work, 2. adapt my library to them, 3. test that this adaptation would work correctly
- I don't know the quantifier guess library well enough to be able to say how useful it would be in this context
- in particular, regarding conj_lift_qp, I don't really know how useful it would be; it depends which strategy we can lift using this function: if some "existential" guess can be used that matches HINT_EXISTS_TAC behavior then yes, but I've no idea about this
- match_exists_tac looks indeed very similar to HINT_EXISTS_TAC, except that HINT_EXISTS_TAC looks not just at the first conjunct, but all of them, possibly also instantiating several different quantifiers at the same time based on different atoms (not sure how useful it is in practice though); also HINT_EXISTS_TAC is able (if I remember right) to instantiate only partially a set of quantifiers, e.g., if some guesses based on the atoms are found for some existential quantifiers, but not all of them it will still manage to instantiate those that it can.
- I think QUANT_TAC is not the way to go with HINT_EXISTS_TAC since not having to give the explicit instantiation is the whole objective of HINT_EXISTS_TAC :-(
More details regarding the quantifier guess library, I think I remember when starting working on HINT_EXISTS_TAC about 2yrs ago and discussing it on the hol-info mailing list, that Thomas already advised having a look at the quantifier guess library to implement this. Now, even though I don't remember why precisely, I remember that I had a look back then, but could not find a relevant way to make use of it. Maybe this conclusion was due to my lack of understanding, maybe this conclusion would also be different now that it seems it has been updated.