Zulip Chat Archive

Stream: PR reviews

Topic: sublattice definition #7093


view this post on Zulip 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.

#7093

view this post on Zulip 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.)

view this post on Zulip 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 .

view this post on Zulip Kevin Buzzard (Apr 07 2021 at 20:39):

heh :-)

view this post on Zulip Johan Commelin (Apr 07 2021 at 20:40):

First look: this looks pretty good, but there are some style issues.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 07 2021 at 20:54):

A zulip admin can presumably move this thread?

view this post on Zulip Notification Bot (Apr 07 2021 at 21:38):

This topic was moved here from #new members > PR Sublattice by Mario Carneiro

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 07 2021 at 22:06):

I would guess you started your branch before that refactor

view this post on Zulip 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.

view this post on Zulip Matúš Behun (Apr 07 2021 at 22:08):

Eric Wieser said:

I would guess you started your branch before that refactor

Yes

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Matúš Behun (Apr 07 2021 at 22:19):

okay thanks for the help

view this post on Zulip 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

view this post on Zulip Matúš Behun (Apr 13 2021 at 22:07):

regarding set_coe_sort I've changed all definitions to match new style

view this post on Zulip 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

view this post on Zulip 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: May 09 2021 at 14:10 UTC