Zulip Chat Archive

I am definitely not an expert, but when I see declarations doing so much I tend to ask myself if I can break it into smaller pieces that are easier to understand and review. Could not be the case tho!

Eric Wieser (Dec 16 2021 at 15:25):

I guess a PR would be useful to tell apart what's new and what's Yael and Bhavik's existing code

Huỳnh Trần Khanh (Dec 16 2021 at 15:28):

https://github.com/leanprover-community/mathlib/pull/10846

Julian Külshammer (Dec 16 2021 at 15:33):

Another common thing is that if you do two rw in a row, they should be written in one line as rw [lem1, lem2].

Julian Külshammer (Dec 16 2021 at 15:36):

And sometimes you do two casesright after each other, which can probably be put in one line using rcases.

Jireh Loreaux (Dec 16 2021 at 16:01):

@Huỳnh Trần Khanh: just FYI, in Zulip, #10846 becomes #10846.

Eric Wieser (Dec 16 2021 at 16:09):

I added some comments - thanks for adding the {}s, they already make it way more readable than it was

Huỳnh Trần Khanh (Dec 17 2021 at 03:48):

thank you for your suggestions! i fixed all the issues you mentioned :octopus: #10846

Huỳnh Trần Khanh (Dec 17 2021 at 03:49):

oh wait. i still need to use rcases. back to work :joy:

Huỳnh Trần Khanh (Dec 17 2021 at 03:55):

done :raised_hands:

Huỳnh Trần Khanh (Dec 17 2021 at 04:01):

today i learned that this community becomes 10000000000x more helpful when i contribute to mathlib :joy:

Arthur Paulino (Dec 17 2021 at 04:30):

@Huỳnh Trần Khanh you can remove the label awating-author and add the label awating-review if the PR is ready again

Eric Wieser (Dec 18 2021 at 10:02):

It looks like you've PR'd from your personal repo, which is an easy mistake to make since how that's how most github projects operate. I've granted you write access to non-master branches so that you can push to a branch like huynhtrankhanh/stars-and-bars in the shared repo instead. See the comment on the PR

Huỳnh Trần Khanh (Dec 19 2021 at 13:40):

i'm back :heart: ok so i'll make another PR to provide instances and add some functions for sym. but i have some questions:

Can you extract everything to the right of sum.inr to a new definition, sym2.erase?

is there a way to do this elegantly? i'm afraid there isn't. this is because the length of the returned sym depends on whether the to be erased element is in the input sym or not. should i take a hypothesis stating that the element to be erased is a member of the original sym?

I would rather write it like def encode {k : ℕ} (x : sym (option α) k.succ) : sym α k.succ ⊕ sym (option α) k :=

well, you are not the first to come up with this idea. this is part of my proof sketch. however i decided against using this type signature because i assumed that the proof would be quite cantankerous... and at the end of the day i would still need to map the type back to fin n anyway, otherwise there is no way i can define the two multichoose functions... the proof strategy would be quite different i'm afraid

i will address other comments in a new PR. thanks!

Yaël Dillies (Dec 19 2021 at 13:42):

Then I encourage you to try the foreseen cantakerous proof. I promise it's not that bad, and you might even enjoy it.

Eric Wieser (Dec 19 2021 at 13:47):

Yes, I'm suggesting erase (s : sym α n.succ) (a : α) (ha : a ∈ s) : sym α n

Eric Wieser (Dec 19 2021 at 13:47):

Since that's the version it seems you actually use

Huỳnh Trần Khanh (Dec 24 2021 at 12:07):

i made a new PR!!! #11032

Huỳnh Trần Khanh (Dec 24 2021 at 12:09):

this time i do things very properly :joy: i hope someone will review and merge my PR :joy:

Johan Commelin (Dec 24 2021 at 12:28):

@Huỳnh Trần Khanh I've left a first set of comments. Main remark: use more explicit variables when writing instances.

Eric Wieser (Dec 24 2021 at 12:29):

Thanks, that PR looks great! Some of the proofs look a little strangely written, but the statements largely look good

Huỳnh Trần Khanh (Dec 25 2021 at 04:40):

i've made the necessary changes and the PR is now ready for review again :laughing:

Johan Commelin (Dec 25 2021 at 05:39):

@Huỳnh Trần Khanh I left another review.

Huỳnh Trần Khanh (Dec 25 2021 at 10:11):

docstrings added, you can review the PR again

Huỳnh Trần Khanh (Dec 26 2021 at 04:48):

I just fixed stuff :joy: I don't know how to do the docstring thing though, please review my PR again

Arthur Paulino (Dec 26 2021 at 13:17):

Huỳnh Trần Khanh said:

I just fixed stuff :joy: I don't know how to do the docstring thing though, please review my PR again

On the PR page, if you to the bottom and check the box with the tests, you'll notice this line with a red mark indicating failure:
continuous integration / Lint mathlib (push) Failing after 40m — Lint mathlib Details
Then you can click on Details and check what broke

Arthur Paulino (Dec 26 2021 at 13:19):

In this case, it's because you added a definition of sym.map and didn't add a docstring for it

Huỳnh Trần Khanh (Dec 27 2021 at 10:43):

yayy!!! my PR looks very ready to merge :joy: can anyone run bors r+ :heart_eyes: or tell me if there's anything I need to fix :grinning:

Huỳnh Trần Khanh (Dec 29 2021 at 06:27):

#10846 someone please review :tada: :joy:

Johan Commelin (Dec 29 2021 at 06:34):

@Huỳnh Trần Khanh You should label the PR with awaiting-review. That way you can make it show up on the #queue

Yaël Dillies (Dec 30 2021 at 08:22):

I just opened #11142, which should hopefully generalize the approach (from fintypes to finsets). Hence I suggest putting it as a dependency of #10846.

Huỳnh Trần Khanh (Dec 30 2021 at 15:12):

sorry I couldn't get fin.cast_pred to work. anyway if anyone has any suggestions please let me know #10846

Huỳnh Trần Khanh (Dec 30 2021 at 15:27):

but I think I have a question :smiley: I don't quite understand what #11142 does really... does it mean I have to ~~rewrite my PR~~? that is, do I have to use finset in my proof now? and I can't have my straightforward proof based on equinumerosity?

Kyle Miller (Dec 30 2021 at 15:35):

I like this finset.sym2, but I'm not sure it's better to base stars-and-bars on it (or if it is better, I'm not sure it's necessary to rewrite the PR to use it right now). I think this is a case where manipulating types directly gives a more direct proof, vs manipulating finsets in types. It's probably fairly easy to get the finset version of the theorem from the type version.

Huỳnh Trần Khanh (Dec 30 2021 at 16:23):

i'd say that it would be silly to base my PR off of #11142 because the proof would become... more convoluted? and my proof is as straightforward as it gets :joy: i believe equinumerosity is the most natural approach to prove stars and bars, even stars and bars isn't as natural as my approach :joy:

Huỳnh Trần Khanh (Dec 30 2021 at 16:33):

this is my opinion, and of course you might disagree but i believe my opinion is pretty reasonable: we should get my PR merged without changing the overall proof strategy or generalizing stuff :joy: building an API for data.sym is reasonable, and i think there might be some lean idioms that i missed. also the names don't really follow mathlib conventions so maybe you should tell me how to fix those names too. but i don't think the proof strategy should be changed for the time being

Kyle Miller (Dec 30 2021 at 16:46):

I think it's nice having combinatorial proofs where we encode algebraic expressions of numbers as algebraic expressions of types, with equalities being equivalences, ideally in a way where these equivalences are useful functions in their own right.

I'd like it more if our equivalences used "generic" types, like sums, products, and option. (option I think we can agree ought to be the standard combinatorial encoding of "add one.") Right now the equivalent definition uses special properties of fin, and I think everything will end up being cleaner if we use Yael's earlier suggestion of sym (option α) k.succ ≃ sym α k.succ ⊕ sym (option α) k.

I'm happy to go through and switch things over to this if you want any help @Huỳnh Trần Khanh.

Kyle Miller (Dec 30 2021 at 16:48):

(I want to be mindful of the fact that it's not that fun being part of a long and drawn-out PR process, so I don't want to ask you to do more work for this to get it in.)

Yaël Dillies (Dec 30 2021 at 16:59):

I have the same feeling that the way you attacked things won't translate that well from types to finsets. The sym2 stars and bars, however, went unscathed.

Yaël Dillies (Dec 30 2021 at 17:04):

One way finset.sym could help is if it were inductively defined in such a way that every sym is added exactly once, in which case the inductive definition turns into an inductive relation on its card. I wrote #11142 with the idea that the definition might change in mind, by making sure most of the API wasn't directly using the definition but instead going through finset.mem_sym_iff, which is the main theorem.

Eric Rodriguez (Dec 30 2021 at 17:07):

this is what I did for card_embedding; there's a bunch of equivs which basically underscore the proof (and option used for add_one!)

Eric Rodriguez (Dec 30 2021 at 17:08):

(and the end proof looked like file#data/fintype/card_embedding

Kyle Miller (Dec 30 2021 at 17:09):

@Eric Rodriguez Just to clarify, what's "this"? (I'm assuming it's what I mentioned about equivalences, but just want to be sure since there are a couple things under discussion.)

Eric Rodriguez (Dec 30 2021 at 17:11):

Kyle Miller said:

I think it's nice having combinatorial proofs where we encode algebraic expressions of numbers as algebraic expressions of types, with equalities being equivalences, ideally in a way where these equivalences are useful functions in their own right.

I'd like it more if our equivalences used "generic" types, like sums, products, and option. (option I think we can agree ought to be the standard combinatorial encoding of "add one.") Right now the equivalent definition uses special properties of fin, and I think everything will end up being cleaner if we use Yael's earlier suggestion of sym (option α) k.succ ≃ sym α k.succ ⊕ sym (option α) k.

I'm happy to go through and switch things over to this if you want any help Huỳnh Trần Khanh.

Huỳnh Trần Khanh (Dec 31 2021 at 03:47):

i made a new PR from a branch on mathlib. you, as in everyone with write access can commit anything you want now :joy: #11162

feel free to do crazy stuff

Yaël Dillies (Dec 31 2021 at 09:33):

I'm trying the option α stuff out.

Yaël Dillies (Dec 31 2021 at 09:59):

What you were missing to make that work was

def attach (s : sym α n) : sym {a // a ∈ s} n

Yaël Dillies (Dec 31 2021 at 12:51):

Okay, I got it working, with many more sym lemmas.

Kyle Miller (Dec 31 2021 at 13:16):

@Yaël Dillies Oh, I was working on that, too, and I also implemented attach. That's what my offer to @Huỳnh Trần Khanh was supposed to mean and the :thumbs_up:, but I should have been more explicit I guess.

Yaël Dillies (Dec 31 2021 at 13:17):

Ah yeah, sorry. I did say I was working on it 3 hours ago.

Kyle Miller (Dec 31 2021 at 13:19):

I mean I was working on it yesterday (and I just woke up in this timezone)

Yaël Dillies (Dec 31 2021 at 13:20):

Oh whoops

Kyle Miller (Dec 31 2021 at 13:20):

Oh well, I'll just merge in some of the additional things I have.

Kyle Miller (Dec 31 2021 at 17:07):

Ok, merged. @Yaël Dillies I reorganized the new lemmas you wrote and put them in data/sym/basic, and other than that I don't think I modified them other than renaming map_attach_val to attach_map_coe. There's a section unused in data/sym/card with a few things that weren't used in the argument (and which I didn't want to find proper homes for to avoid recompilation).

@Huỳnh Trần Khanh I changed the design slightly. I consolidated the multichoose* functions to a single one:

def multichoose (n k : ℕ) := (n + k - 1).choose k

and I filled in the proof for

lemma multichoose_eq (α : Type*) [hα : fintype α] (k : ℕ) [fintype (sym α k)] :
  multichoose (card α) k = card (sym α k)

I figured card (sym α k) is a short enough name for itself.

Kyle Miller (Dec 31 2021 at 17:14):

(@Yaël Dillies That was a good change to sym.cons to help unstick simplifications.)

Yaël Dillies (Dec 31 2021 at 17:31):

Btw I meant to replace multichoose by nat. asc_fac or something

Kyle Miller (Dec 31 2021 at 17:36):

Whatever it's called, putting it into the nat is a good idea. nat.multichoose seems fine to me, and it seems like a relatively common name.

Where's the name nat.asc_fac coming from?

Yaël Dillies (Dec 31 2021 at 18:20):

Sorry, was on my phone. I meant docs#nat.asc_factorial

Kyle Miller (Dec 31 2021 at 18:35):

Oh, I see, makes sense.

Last updated: Dec 20 2023 at 11:08 UTC