Zulip Chat Archive
Stream: PR reviews
Topic: sublattice definition #7093
Matúš Behun (Apr 07 2021 at 20:33):
Anybody willing to look at talk about my PR? I am trying to define order/sublattice. I need at least some quick overview if structure is right and what else should I work on to be successful with merge.
Johan Commelin (Apr 07 2021 at 20:39):
@Matúš Behun welcome! (Note that there is a dedicated stream #PR reviews for discussion of specific PRs.)
Kevin Buzzard (Apr 07 2021 at 20:39):
Thanks for doing this! PR's have their own stream -- perhaps we should continue this conversation in #PR reviews .
Kevin Buzzard (Apr 07 2021 at 20:39):
heh :-)
Johan Commelin (Apr 07 2021 at 20:40):
First look: this looks pretty good, but there are some style issues.
Johan Commelin (Apr 07 2021 at 20:40):
@Matúš Behun please take a look at https://leanprover-community.github.io/contribute/style.html#structuring-definitions-and-theorems
Eric Wieser (Apr 07 2021 at 20:54):
A zulip admin can presumably move this thread?
Notification Bot (Apr 07 2021 at 21:38):
This topic was moved here from #new members > PR Sublattice by Mario Carneiro
Matúš Behun (Apr 07 2021 at 22:02):
@Eric Wieser Thank you for review, I would like to discuss it here and your comment regarding function.injective.lattice
Eric Wieser (Apr 07 2021 at 22:06):
I did a big refactor recently that removed a lot of duplication between subobjects, and introduced docs#set_like
Eric Wieser (Apr 07 2021 at 22:06):
I would guess you started your branch before that refactor
Matúš Behun (Apr 07 2021 at 22:07):
What I wanted to achieve is transformation of sublattice to lattice hence lattice beta. Also any comment regarding how to improve pr by adding theorems or instancing something would be appreciated.
Matúš Behun (Apr 07 2021 at 22:08):
Eric Wieser said:
I would guess you started your branch before that refactor
Yes
Eric Wieser (Apr 07 2021 at 22:11):
Your function.injective.lattice definition isn't useful because it takes a lattice over L, a function from \b to L, a bunch of proofs about that function... Only to ignore all those things and just produce the same lattice over L it started with!
Eric Wieser (Apr 07 2021 at 22:12):
Have a look at src#function.injective.mul_one_class for a very simple example of how that definition should actually look
Eric Wieser (Apr 07 2021 at 22:14):
Regarding set_like, you'll want to git fetch origin && git merge origin/master before you try to use it
Matúš Behun (Apr 07 2021 at 22:19):
okay thanks for the help
Matúš Behun (Apr 13 2021 at 22:05):
function.injective.sublattice - thanks for the example i changed it accordingly, of course i forgot to produce sublattice instead of lattice, still might ask around here how to finish this definition
Matúš Behun (Apr 13 2021 at 22:07):
regarding set_coe_sort I've changed all definitions to match new style
Eric Wieser (Apr 13 2021 at 22:25):
No, the result really should be lattice, just on the type at the other end of the injective function
Eric Wieser (Apr 13 2021 at 22:26):
Perhaps we already have that definition as docs#lattice.lift (to match docs#partial_order.lift)?
Last updated: Dec 20 2023 at 11:08 UTC