New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Tactic to transfer theorems / definitions using an equivalence. #1868
Comments
Related: #408 |
Also related: @CohenCyril spent a couple of intense weeks on the problem (his repo). It is not an easy problem and we'll have to be patient. |
Since I didn't see this mentioned either here or at #408, there's the |
It was mentioned in the conversation earlier. I think the consensus was that this machinery is too ad hoc and not very extendible. I don't personally have experience with it but that's what I got from the conversation. @CohenCyril on the other hand is formalizing a theory of parametricity to base transport on which promises to be more principled and more solid. |
Note that the |
@johoelzl Could you please explain what does |
Can it do all the transfers in |
Oh, I didn't even realise that file existed. Yes, I will certainly aspire to automate everything there away. (And hopefully synthesize lots of missing lemmas about these transferred instances.) |
It would be nice to have a tactic that can transfer definitions and / or theorems through equivalences. E.g., all theorems in the upper half of
data/equiv/algebra
should beby equiv_transfer e
.In its simplest form it should assume that there is no structure on the target type, and transfer everything from the source type. I.e., it should analyze the requested type, and substitute
e
,e.symm
,e.apply_symm_apply
ande.symm_apply_apply
as needed.A more advanced version should be able to work with a target type that already has some structure but this structure agrees with that on the source type (e.g.,
e (a * b) = e a * e b
), and the lemmas that prove these equalities either have predictable names, or are given as arguments to the tactic.With the second type of tactic, it would be easy to define new types that are mathematically equivalent to old ones but provide better performance (more precisely, to prove theorems about these types).
The text was updated successfully, but these errors were encountered: