Zulip Chat Archive
Stream: general
Topic: transfer between isomorphic types
Alexander Bentkamp (Apr 02 2019 at 18:02):
Is there a way to transfer theorems between two isomorphic types (semi-)automatically? For example using transfer? @Johannes Hölzl ?
In my case, I have row vectors (1xn matrices) and column vectors (nx1 matrices). Whether this makes sense or not is surely also up for discussion and you can tell me your opinion if you like.
Anyhow, I'd like to prove lemmas only for one of them and transfer them to the other via a bijection.
Johan Commelin (Apr 02 2019 at 18:02):
Search for transfer in this chat...
Johan Commelin (Apr 02 2019 at 18:02):
Or transport
Johan Commelin (Apr 02 2019 at 18:03):
You will find lots of requests, headaches, pain, confusion
Johan Commelin (Apr 02 2019 at 18:03):
Mathematicians think its trivial, computer scientists think not.
Johan Commelin (Apr 02 2019 at 18:03):
People are trying to build things. Little progress so far.
Johan Commelin (Apr 02 2019 at 18:03):
The transfer tactic exists. But there is no infrastructure.
Alexander Bentkamp (Apr 02 2019 at 18:05):
Oh, right, I should have searched in the chat earlier. Thanks :-)
Johan Commelin (Apr 02 2019 at 18:06):
No worries! The more people are interested in this thing, the higher the chances we get a solution soon.
Johan Commelin (Apr 02 2019 at 18:07):
You are working in the Lean Forward project, right?
Johan Commelin (Apr 02 2019 at 18:08):
Having a powerful and easy-to-use transfer/transport system is a core feature if mathematicians are to use theorem provers...
Alexander Bentkamp (Apr 02 2019 at 18:08):
I am actually part of the Matryoshka project, but I am also working in Amsterdam.
Alexander Bentkamp (Apr 02 2019 at 18:08):
yes, that would be definitely good to have
Simon Hudon (Apr 02 2019 at 18:09):
That's a pretty realistic looking hologram that you sent to Pittsburgh!
Johan Commelin (Apr 02 2019 at 18:09):
Aah, too bad. I was thinking I could suggest you a topic :stuck_out_tongue_wink:
Alexander Bentkamp (Apr 02 2019 at 18:35):
But it seems to work pretty well for has_add and has_mul, right?
Kevin Buzzard (Apr 02 2019 at 18:44):
It's not perfect
Kevin Buzzard (Apr 02 2019 at 18:44):
But it's much better than nothing
Kevin Buzzard (Apr 02 2019 at 18:45):
It's also used for integers somehow
Kevin Buzzard (Apr 02 2019 at 18:45):
Relating them to pairs of naturals
Patrick Massot (Apr 02 2019 at 18:46):
I think this is no longer true
Patrick Massot (Apr 02 2019 at 18:46):
since Lean 3.4.2
Simon Hudon (Apr 02 2019 at 18:49):
I thought they only moved that construction from core to mathlib
Patrick Massot (Apr 02 2019 at 18:49):
No, int is in core
Patrick Massot (Apr 02 2019 at 18:50):
https://github.com/leanprover/lean/commit/95fa4cfb0a8774570d67bb231c1ab088a94e12bb
Patrick Massot (Apr 02 2019 at 18:51):
So transfer is now in mathlib, and is no longer used to build int
Last updated: Dec 20 2023 at 11:08 UTC