counting function

Stream: general

[Vladimir Goryachev]

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

[Scott Morrison]

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

[Vladimir Goryachev]

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

[Vladimir Goryachev]

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

[Vladimir Goryachev]

(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]

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

[Vladimir Goryachev]

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]

Vladimir Goryachev said:

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]

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

[Yaël Dillies]

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

[Vladimir Goryachev]

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]

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]

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]

I totally forgot that existed

[Vladimir Goryachev]

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

[Mario Carneiro]

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

[Mario Carneiro]

and prove the theorems in the union of both developments

[Vladimir Goryachev]

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

[Mario Carneiro]

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]

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

[Vladimir Goryachev]

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]

why is fincard in the file?

[Yaël Dillies]

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]

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]

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)?

[Ruben Van de Velde]

Yep

[Vladimir Goryachev]

Thanks!

[Johan Commelin]

@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]

I left a few more stylistic comments.

[Vladimir Goryachev]

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]

@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]

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]

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

[Vladimir Goryachev]

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]

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

[Vladimir Goryachev]

Let me recheck it quickly

[Vladimir Goryachev]

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]

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]

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

[Vladimir Goryachev]

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

[Vladimir Goryachev]

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]

The proof works on your computer though, right?

[Yaël Dillies]

It worked on Gitpod.

[Vladimir Goryachev]

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

[Yaël Dillies]

Yeah, probably

[Yaël Dillies]

If it fails, I'll fix it.

[Vladimir Goryachev]

Thank you. Done!

[Yaël Dillies]

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

[Vladimir Goryachev]

I am fine both ways here.

[Vladimir Goryachev]

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

[Yaël Dillies]

Will look into that

[Vladimir Goryachev]

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]

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

[Vladimir Goryachev]

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]

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

[Yaël Dillies]

Ah! I was fixing it just now!

[Vladimir Goryachev]

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

[Vladimir Goryachev]

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

[Yaël Dillies]

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

[Vladimir Goryachev]

I see! Thank you very much.