mathlib
mathlib copied to clipboard
leanprover-community
Tactic to transfer theorems / definitions using an equivalence.
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 be by 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 and e.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).
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 transfer tactic that Johannes wrote a long time ago. Here's an example in mathlib where it transfers theorems between ℤ and znum (an isomorphic copy of ℤ).
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 transfer that @gebner mentions is indeed quite ad hoc: https://github.com/leanprover-community/mathlib/blob/master/src/data/num/lemmas.lean#L955
There is also: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/transfer.lean I have no experience with this tactic.
I've done a bunch of work towards this, so far appearing in #2246 (an equiv_rw tactic) and #2251 (a transport tactic).
Can it do all the transfers in data/equiv/transfer_instance? Does it produce the same definitional equalities?
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.)