## Stream: general

### Topic: counting function

#### Vladimir Goryachev (Oct 27 2021 at 07:03):

@Eric Wieser You have suggested renaming Inf_plus into Inf_add. What is your reasoning behind it?

#### Scott Morrison (Oct 27 2021 at 07:11):

Uniformity with the rest of the library. It may be worth reading #naming.

#### Vladimir Goryachev (Oct 27 2021 at 07:19):

Thanks, such a file was what I was looking for!

#### Vladimir Goryachev (Oct 27 2021 at 07:31):

Meanwhile, I have created a PR #10001 where I add two lemmas proved by refl to data/nat/basic

#### Vladimir Goryachev (Oct 27 2021 at 07:33):

(By the way, maybe we should move this conversation to general? It seems have grown out of scope of "Is there code for X" quite a while ago)

#### Vladimir Goryachev (Oct 27 2021 at 08:10):

I think I'll wait for #10001 to be accepted before making a PR about Inf_add.

#### Vladimir Goryachev (Oct 27 2021 at 08:47):

Next, I am looking into redefining of order_embedding_of_set and order_iso_of_nat in terms of nth. Currently, we have the proof that nth is the same as order_iso_of_nat. If we change the definition of order_iso_of_nat to be just nth, this prove would become the proof of the fact that order_iso_of_nat equals some scary arcane expression (which is currently the definition):

rel_iso.of_surjective (rel_embedding.order_embedding_of_lt_embedding
(rel_embedding.nat_lt (nat.subtype.of_nat s) (λ n, nat.subtype.lt_succ_self _)))
nat.subtype.of_nat_surjective


Do we want to have such a characterisation? Would it be useful for anything? Or was it used simply because there was nothing better to write instead?

#### Vladimir Goryachev (Oct 27 2021 at 19:14):

I think I'll wait for #10001 to be accepted before making a PR about Inf_add.

Yay, my first PR merged, even if a trivial one : )

I have made #10008

#### Kevin Buzzard (Oct 27 2021 at 19:20):

I felt just the same when my first PR, defining the complex numbers and proving they were a ring, was accepted :-)

#### Yaël Dillies (Oct 27 2021 at 19:35):

My very first PR was swapping two arguments on an obscure lemma for dot notation to work

#### Vladimir Goryachev (Oct 27 2021 at 19:45):

Ah, I have found the file, it is actually data/equiv/denumerable.

@Mario Carneiro , in this thread we have defined functions nth and count, same as your of_nat and to_fun_aux of data/equiv/denumerable (I could not find the functionality when I asked for it in the "Is there code for X" channel). However, here we have developed some of the basic results further, including counting elements of finite subsets of N. Could you please give your opinion on how we should integrate the things we have defined and proved into what you have defined and proved earlier? Thank you for your attention.

#### Mario Carneiro (Oct 27 2021 at 19:50):

The content of this thread is not quite the same as what denumerable does. denumerable is about coming up with some mapping to/from nat, but it is not an increasing function (necessarily), and indeed in most applications there is no notion of increasing since the source type has no ordering (besides the one it inherits from the bijection to nat). The nth and count functions are useful but probably wouldn't fit as a sub-part or application of denumerable. I think you should just make a new file data.nat.nth about this function.

#### Mario Carneiro (Oct 27 2021 at 19:52):

Oh, I see now what you mean about to_fun_aux. I guess the denumerable implementation for infinite sets is the same as your function

#### Mario Carneiro (Oct 27 2021 at 19:54):

I totally forgot that existed

#### Vladimir Goryachev (Oct 27 2021 at 19:55):

Yes, so in the comments to the PR it was advised to not have two distinct definitions implementing the same thing.

#### Mario Carneiro (Oct 27 2021 at 19:55):

The usual solution to that is to either relate them or use one in place of the other

#### Mario Carneiro (Oct 27 2021 at 19:55):

and prove the theorems in the union of both developments

#### Vladimir Goryachev (Oct 27 2021 at 20:07):

Do you have any opinion on whether should of_nat be redefined on terms of nth or vice versa?

#### Mario Carneiro (Oct 27 2021 at 20:18):

assuming you have looked at the proof of of_nat and mined the ideas from it, I think denumerable could just be referencing your version. I'm fairly sure that no one is using the denumerable instance for infinite sets, it was just proven to show that it's true

#### Vladimir Goryachev (Oct 27 2021 at 20:20):

Thank you! Then, I guess, I'll try to redefine of_nat in terms of nth.

#### Vladimir Goryachev (Oct 27 2021 at 20:31):

Well, I try to import count into denumerable, and I get an import cycle data.nat.count < set_theory.fincard < set_theory.cardinal < data.set.countable < data.equiv.list < data.equiv.denumerable < data.nat. count. Wow.

#### Mario Carneiro (Oct 27 2021 at 20:51):

why is fincard in the file?

#### Yaël Dillies (Oct 27 2021 at 21:36):

It's used to state lemmas for finite and infinite sets simultaneously by looking at its cardinal. I strongly voted against those because it's either finite or infinite here and nobody uses cardinals anyway.

#### Vladimir Goryachev (Oct 28 2021 at 06:37):

I'd side with Yaёl here. I think the cardinal lemmas didn't quite fit: set-theoretic cardinals should come after describing how to count, not in the same file. This was okay as it did not break anything, but now I think it is a legitimate reason to remove them. My default action would be to delete the lemmas, but anyone is free to move them to separate file like nat/count_cardinal or something.

But that would all come a bit further, as now I'd be focused at PR-ing simple lemmas which precede the count lemmas itself.

#### Vladimir Goryachev (Oct 29 2021 at 07:44):

For PR #10008, I was advised to make some changes, and made them now. Is it true that to ask for a review again, I simply need to add "awaiting review" label, and it will get reviewed (at some point)?

Yep

Thanks!

#### Johan Commelin (Oct 29 2021 at 07:58):

@Vladimir Goryachev If you make sure your PR ends up on #queue than it has a very high chance of getting reviewed (-;
That list is made up of PRs that have the awaiting review label, are not blocked by other PRs, don't have merge conflicts, are not waiting for a CI run, etc... (see the filters at the top of the list).

#### Johan Commelin (Oct 29 2021 at 08:01):

I left a few more stylistic comments.

#### Vladimir Goryachev (Oct 29 2021 at 09:58):

Thanks, changes pushed!
I hope to get used to placing spaces before colons soon, it just felt weird, kind of like placing spaces before commas : )

#### Vladimir Goryachev (Nov 08 2021 at 14:34):

@Yaël Dillies , I am trying to implement the changes you propose for the Inf_add lemma, but Lean says that it does not know what is le_cInf in the proof of Inf_add'. How do I fix this?

#### Yaël Dillies (Nov 08 2021 at 14:35):

That's weird... Try to see whether you indeed import order.conditionally_complete_lattice because that's where it is: https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html#le_cInf

#### Vladimir Goryachev (Nov 08 2021 at 14:42):

Ah, sorry, it actually knows what it is, it has some other problem...

#### Vladimir Goryachev (Nov 08 2021 at 14:45):

type mismatch, term
le_of_not_lt ?m_5
has type
?m_3 ≤ ?m_4
but is expected to have type
?m_2 ≤ b


and

type mismatch, term
le_cInf ?m_5 ?m_6
has type
?m_3 ≤ Inf ?m_4
but is expected to have type
n ≤ Inf {m : ℕ | p (m - n)}


#### Yaël Dillies (Nov 08 2021 at 14:46):

And that's what you get with my suggestion and no other modification?

#### Vladimir Goryachev (Nov 08 2021 at 14:47):

Let me recheck it quickly

#### Vladimir Goryachev (Nov 08 2021 at 14:56):

Yes, if I do no other modification and paste your code into nat/lattice, deleting my previous proofs of Inf_add and Inf_add', I get this error messages.

#### Vladimir Goryachev (Nov 08 2021 at 14:58):

I think I see what the second error message is saying though - it is expected to say something about nat.Inf, but the lemma speaks about general Inf instead. I have had this appearing before, and had to type nat.Inf in proofs manually. Here, however, there is no nat version of le_cInf, and I can not do that.

#### Yaël Dillies (Nov 08 2021 at 15:03):

nat.Inf is a cInf (through docs#nat.conditionally_complete_linear_order_bot)

#### Vladimir Goryachev (Nov 08 2021 at 15:08):

Well, I don't know, it was just a hypothesis for what's wrong...

#### Vladimir Goryachev (Nov 08 2021 at 15:13):

If I place apply le_cInf before this refine, the error message is just

invalid apply tactic, failed to unify
n ≤ Inf {m : ℕ | p (m - n)}
with
?m_3 ≤ Inf ?m_4


#### Vladimir Goryachev (Nov 08 2021 at 15:19):

The proof works on your computer though, right?

#### Yaël Dillies (Nov 08 2021 at 15:24):

It worked on Gitpod.

#### Vladimir Goryachev (Nov 08 2021 at 15:27):

Okay... Should I just press "commit suggestion" in github, and see if it compiles there?

Yeah, probably

#### Yaël Dillies (Nov 08 2021 at 15:28):

If it fails, I'll fix it.

Thank you. Done!

#### Yaël Dillies (Nov 08 2021 at 15:30):

ALso, I can PR the few nat.find lemmas I came up with separately if you want.

#### Vladimir Goryachev (Nov 08 2021 at 15:31):

I am fine both ways here.

#### Vladimir Goryachev (Nov 09 2021 at 08:10):

@Yaël Dillies , it did not compile on the server, got the error message I was speaking about.

#### Yaël Dillies (Nov 09 2021 at 08:11):

Will look into that

#### Vladimir Goryachev (Nov 09 2021 at 18:41):

I also have a question about the lemma list.range_add. It is stated about list.range, but the list.range file prompts to do any math about ranges with list.Ico instead. So, shouldn't this lemma be stated about Ico instead, as well as the lemmas multiset.range_addand finset.range_add?

#### Vladimir Goryachev (Nov 10 2021 at 15:34):

So anyway, I have changed the coed for Inf_add' into something that compiles.

#### Vladimir Goryachev (Nov 10 2021 at 15:35):

I have another question. How do I change a name of a lemma in mathlib in a way that changes the name everywhere where it is used?

#### Eric Rodriguez (Nov 10 2021 at 15:37):

egergious use of ctrl+f :) ctrl+shift+f usually works in vscode

#### Yaël Dillies (Nov 10 2021 at 15:44):

Ah! I was fixing it just now!

#### Vladimir Goryachev (Nov 10 2021 at 15:48):

I would still be grateful for a more eloquent proof than mine : )

#### Vladimir Goryachev (Nov 10 2021 at 15:49):

@Eric Rodriguez Will it work for all of mathlib though, or for the current file only?

#### Yaël Dillies (Nov 10 2021 at 15:53):

The problem was just that the instance was defined below. I moved the lemma and now it's fine.

#### Vladimir Goryachev (Nov 10 2021 at 15:56):

I see! Thank you very much.

Last updated: Dec 20 2023 at 11:08 UTC