counting function

Stream: Is there code for X?

[Vladimir Goryachev]

A question inspired by discussion in General: is there a counting function which returns the n-th natural number satisfying predicate f?

[Ryan Lahfa]

AFAIK, there is nat.find which you would have to iterate, otherwise, if you had a bound on the n-th natural number, you could use find_greatest I suppose.

[Vladimir Goryachev]

Well, I am just thinking of creating a bounding function and a basic API to it as my first contribution to mathlib, and want to get sure I will not duplicate something already implemented.

[Kyle Miller]

If you can write (at least roughly) a type for the function you have in mind, you can get a more precise answer about what exists. (It's also good to run API ideas past the community anyway.)

[Eric Wieser]

I think this works:

import order.conditionally_complete_lattice

/-- `satisfied_by p i n c` states that there are `n` values less than or equal to `i` which satisfy `p`, and
that `p m` is satisfied iff`c`. -/
inductive satisfied_by (p : ℕ → Prop) : ℕ → ℕ → bool → Prop
| zero_pos (h : p 0) : satisfied_by 0 1 tt
| zero_neg (h : ¬p 0) : satisfied_by 0 0 ff
| succ_pos {i n : ℕ} {c : bool} (h : p i.succ) (hs : satisfied_by i n c) : satisfied_by i.succ n.succ tt
| succ_neg {i n : ℕ} {c : bool} (h : ¬p i.succ) (hs : satisfied_by i n c) : satisfied_by i.succ n ff

/-- a counting function which returns the `n`-th natural number satisfying predicate p -/
noncomputable def count (p : ℕ → Prop) (n : ℕ) : ℕ :=
⨅ i (h : satisfied_by p i n tt), i

[Johan Commelin]

So this returns 0 when no such n-th nat exists, right?

[Eric Wieser]

Yeah, I think so. There's probably a nicer way than using infi

[Eric Wieser]

Of course, you'll probably want to show that decidable_pred (λ (i : ℕ), satisfied_by p i n tt), which I think is true but is going to be a painful case-bash

[Eric Wieser]

Perhaps you can do it with fewer constructors

[Eric Rodriguez]

I don't think you need the bools at all?

[Alex J. Best]

I think a computable version that just assumes the set is infinite would be nice?

[Eric Wieser]

No, but I figured they'd make things easier later

[Eric Wieser]

The alternative would be to use satisfied_by p i n ∧ p i instead of satisfied_by p i n tt

[Eric Rodriguez]

if you're taking the infi can't we just use the smallest i with satisfied_by p i n?

[Eric Wieser]

Sure, i just thought that condition might come up in the computable version

[Eric Rodriguez]

ahh I think I get the motivation

[Eric Wieser]

I think this would be another option:

import order.conditionally_complete_lattice
import order.preorder_hom

open_locale classical

noncomputable def count (p : ℕ → Prop) (n : ℕ) : ℕ :=
if h : nonempty {f : ((<) : fin n.succ → fin n.succ → Prop) →r ((<) : ℕ → ℕ → Prop) // ∀ i, p (f i)}
    then h.some (fin.last n) else 0

[Floris van Doorn]

Or

-- import might need to be changed to `data.nat.lattice` in a more recent version of mathlib
import order.conditionally_complete_lattice

noncomputable def count (p : ℕ → Prop) : ℕ → ℕ
| n := Inf { i : ℕ | p i ∧ ∀ k < n, count k < i }

[Johan Commelin]

These are really nice. I especially like that the $\pi(n)$ is then simply count prime n.

[Kyle Miller]

A more restrictive but computable version:

import data.nat.parity
import data.nat.primes

def nth_with_aux {p : ℕ → Prop} [decidable_pred p] (h : ∀ (i : ℕ), ∃ (j : ℕ), i ≤ j ∧ p j) : ℕ → ℕ → ℕ → ℕ
| 0 i j := j
| (n+1) i j := let j := nat.find (h i)
               in nth_with_aux n j.succ j

-- maybe `find_nth` would be a more appropriate name
def nth_with {p : ℕ → Prop} [decidable_pred p] (h : ∀ (m : ℕ), ∃ (n : ℕ), m ≤ n ∧ p n) (n : ℕ) :=
nth_with_aux h n.succ 0 0

lemma inf_evens : ∀ (i : ℕ), ∃ (j : ℕ), i ≤ j ∧ even j :=
begin
  intro i,
  by_cases h : even i,
  refine ⟨i, rfl.ge, h⟩,
  use i + 1,
  simp [nat.even_succ.mpr h],
end

#eval [0,1,2,3].map (nth_with inf_evens)
-- [0, 2, 4, 6]

#eval [0,1,2,3,4].map (nth_with nat.exists_infinite_primes)
-- [2, 3, 5, 7, 11]

[Floris van Doorn]

Taking a step back, why are we calling this count? This is the "nth element satisfying p". We should have

import order.conditionally_complete_lattice
import set_theory.fincard

namespace nat

noncomputable def count (p : ℕ → Prop) (n : ℕ) : ℕ :=
nat.card { i : ℕ | i ≤ n ∧ p i }

noncomputable def nth (p : ℕ → Prop) : ℕ → ℕ
| n := Inf { i : ℕ | p i ∧ ∀ k < n, nth k < i }

end nat

[Kyle Miller]

With my example, if you import data.nat.primes too, you can do

#eval [0,1,2,3,4].map (nth_with nat.exists_infinite_primes)
-- [2, 3, 5, 7, 11]

[Eric Rodriguez]

i'm currently trying to make a decidable instance for Eric's definition, and just want to resetI all the time, e.g.:

instance {p : ℕ → Prop} {i n : ℕ} [∀ n, decidable (p n)] : decidable (satisfied_by p i n) :=
n.rec_on (if h : p 0
          then decidable.is_false (not_satisfied_of_zero h i)
          else
          @nat.rec_on (λ i, decidable (satisfied_by p i 0)) i (decidable.is_true (satisfied_by.zero_neg h))
          (λ i hi, @decidable.by_cases _ _ hi sorry sorry)
          )

this makes me feel that I'm doing it wrong; what's the "correct" way to make decidable instances?

[Yakov Pechersky]

eq compiler

[Vladimir Goryachev]

As another idea, could we first define the inverse of nth, (which is just number of elements satisfying p which are less than the given number), and then define nth as its inverse?

[Yaël Dillies]

Defining functions through inversion is usually a bad idea.

[Vladimir Goryachev]

Okay, thanks. As for the rubbish values: if there are only n numbers satisfying p, we could set nth p k = (nth p (k-1)) + 1 for n \le k, because this way we have the main theorems about nth (that it is injective, strictly monotone, and that k \le nth p k) without having to supply that there are infinitely many numbers satisfying p. Because otherwise it doesn't really matter what the rubbish values are, does it?

[Vladimir Goryachev]

(btw, how do I render \le correctly in the chat?)

[Ryan Lahfa]

(dollar dollar \leq dollar dollar)

[Scott Morrison]

Can anyone prove

lemma nth_count (p : ℕ → Prop) (n : ℕ) (h : p n) : nth p (count p n) = n := sorry

with @Floris van Doorn's definition above? It seems quite tricky!

[Scott Morrison]

If I can fill that in I have the pleasant fact:

noncomputable def set.infinite.order_iso_nat {s : set ℕ} (i : s.infinite) : s ≃o ℕ :=

[Yakov Pechersky]

Why isn't count just something like

def count (p : ℕ → Prop) [decidable_pred p] (n : ℕ) : ℕ :=
list.length ((list.range n).filter p)

[Scott Morrison]

I put my work so far on an API for count and nth in branch#count, in data.nat.count. Contributions welcome.

[Scott Morrison]

I'm perfectly happy with that definition as well.

[Scott Morrison]

But now I'm off to sleep.

[Yaël Dillies]

I'll have a go!

[Yaël Dillies]

Wait, your lemma is wrong, Scott. What if \not p n?

[Scott Morrison]

There's a hypothesis h : p n?

[Yaël Dillies]

Ah, of course.

[Yaël Dillies]

We should state that nth and count form a Galois connection, then p n tantamounts to n closed.

[Johan Commelin]

They are not just a Galois connection, they're inverses, right?

[Yaël Dillies]

Yes, but not between ℕ and ℕ.

[Johan Commelin]

good point

[Yaël Dillies]

Proved nth_count from the Galois connection and another sorry.

[Eric Rodriguez]

nth_count_gc doesn't seem to work for me @Yaël Dillies

[Yaël Dillies]

Yeah, the definition of count is probably off by one

[Eric Rodriguez]

i meant your proof, but I think it's pretty invariably flawed in general:

lemma nth_count_gc  : galois_connection (nth p) (count p) :=
begin
  refine λ a b, ⟨λ h, _, λ h, _⟩,
  sorry,
  cases a,
  /-
  case nat.zero
    p: ℕ → Prop
    b: ℕ
    h: 0 ≤ count p b

  ⊢ nth p 0 ≤ b
  -/
end

[Yaël Dillies]

Okay whoops, it's the other way around

[Eric Rodriguez]

sorry I didn't just fix it, don't have much of an intuition for galois connections yet

[Eric Rodriguez]

i've never seen them really described as a separate concept outside mathlib

[Eric Rodriguez]

i've pushed some proofs though

[Scott Morrison]

I'm confused by the state of the new commits. It looks like there are a bunch of lemmas proved as consequences of the incorrect statement about a galois connection.

[Scott Morrison]

After deleting those parts, the computable section has no content, besides a duplicate of count_eq_count_add_one in the noncomputable section.

[Scott Morrison]

so I think I'll just delete the computable section.

[Scott Morrison]

I've changed the definition of count to the computable version, and added a lemma

lemma count_eq_card (n : ℕ) : count p n = fintype.card { i : ℕ | i ≤ n ∧ p i } :=

for when the cardinality version is more useful.

[Scott Morrison]

I've pushed this now. (But @Eric Rodriguez and @Yaël Dillies, please do double check that I didn't remove something useful about galois connections.)

[Yaël Dillies]

What's true is galois_connection (count p) (nth p). All the results I had in the computable section can be turned around and it should be about as easy as before to get nth_count.

[Scott Morrison]

Surely you're assuming p is true infinitely often before there is a galois connection.

[Yaël Dillies]

Yep

[Yaël Dillies]

Ah, yes, you have some results unconditional on that.

[Scott Morrison]

In particular the lemma that I think is the "hard" one:

lemma nth_count (p : ℕ → Prop) (n : ℕ) (h : p n) : nth p (count p n) = n := sorry

doesn't depend on it being true infinitely often.

[Yaël Dillies]

Yeah, I understand your point now

[Scott Morrison]

There are some off by one errors that I think I've just fixed.

[Scott Morrison]

Argh, @Yaël Dillies, your last commit seems to be badly broken (8f3294ca76cf5c5b8d9d0f91fd4ba6eba031f4b7).

[Scott Morrison]

It has duplicated definitions, lots of errors, etc.

[Scott Morrison]

For now I've just reverted it, but hopefully you can recover your work from your commit.

[Vladimir Goryachev]

Wow, it is a weird feeling to say I want to work on a feature, and see so much work being already done on it : )
Anyway, the instructions say I should ask here for a permission to edit branches of mathlib. My GitHub username is SymmetryUnbroken

[Kyle Miller]

Scott Morrison said:

There are some off by one errors that I think I've just fixed.

list.range doesn't include the upper bound -- I think it needed the succ.

[Scott Morrison]

Sorry, just pushed again.

[Scott Morrison]

I had to revert out the broken commit before I could commit my fixes.

[Scott Morrison]

@Vladimir Goryachev, invitation sent.

[Kyle Miller]

(I'm hacking together count_set_fintype)

[Scott Morrison]

If several people are working on this branch, lets make sure we only commit things without red squiggles. :-)

[Scott Morrison]

@Kyle Miller, isn't count_set_fintype already done?

[Kyle Miller]

Sorry, miscopied. count_eq_card

[Scott Morrison]

Excellent, thanks!

[Yaël Dillies]

Kyle Miller said:

Scott Morrison said:

There are some off by one errors that I think I've just fixed.

list.range doesn't include the upper bound -- I think it needed the succ.

Ah yeah I was correcting that in my broken commit

[Vladimir Goryachev]

Why is count defined so that it includes the upper bound?

[Eric Rodriguez]

I think count_nth_of_le_card needs to be split into the finite and the infinite case for p, because nat.card p = 0 can mean two very different things

[Yaël Dillies]

Vladimir Goryachev said:

Why is count defined so that it includes the upper bound?

otherwise we don't have the Galois connection

[Eric Rodriguez]

Eric Rodriguez said:

I think count_nth_of_le_card needs to be split into the finite and the infinite case for p, because nat.card p = 0 can mean two very different things

or use the ordinal inequality used in nth_mem_of_le_card

[Vladimir Goryachev]

Yaël Dillies said:

Vladimir Goryachev said:

Why is count defined so that it includes the upper bound?

otherwise we don't have the Galois connection

In the sense of F(a) ≤ b if and only if a ≤ G(b)?

[Vladimir Goryachev]

Also, if I use "git pull origin count", I get the count file, but it has errors (red underscores), is it fine? Or am I getting the file the wrong way?

[Scott Morrison]

it currently has one red underline...

[Scott Morrison]

:-(

[Scott Morrison]

In count_nth_gc, that @Yaël Dillies just introduced.

[Yaël Dillies]

Vladimir Goryachev said:

In the sense of F(a) ≤ b if and only if a ≤ G(b)?

Yep, exactly

[Vladimir Goryachev]

Mine has 4 of them, starting with the definition of nth

[Scott Morrison]

That's a problem.

[Yaël Dillies]

Scott Morrison said:

In count_nth_gc, that Yaël Dillies just introduced.

Public shaming :stuck_out_tongue_closed_eyes:

[Scott Morrison]

:-)

[Eric Rodriguez]

did you get cache and restart the lean server?

[Eric Rodriguez]

@Vladimir Goryachev

[Scott Morrison]

there's no cache at the moment, I guess

[Yaël Dillies]

Probably not

[Vladimir Goryachev]

Eric Rodriguez said:

did you get cache and restart the lean server?

Is it described somewhere how to do it?

[Eric Rodriguez]

you can just get some from an old one with --rev because we're only touching the one file

[Scott Morrison]

If you:

git checkout master
leanproject up
git checkout count
git pull
leanproject build

[Scott Morrison]

and then restart VSCode, all should be good

[Scott Morrison]

leanproject up updates to the last commit, and then tries to download precompiles oleans for that commit. On master those are guaranteed to exist; on other branches they are about an hour or more behind.

[Scott Morrison]

So that recipe should pull the oleans for master, then switch to the current count branch, and recompiles anything that has changed relative to master (which should be only count.lean)

[Yaël Dillies]

Oh wait, I think we may need to not include the upper bound in count for the gc to work.

[Yaël Dillies]

Yup, count 0 should always be 0

[Yaël Dillies]

Do you mind if we do not include n in the definition of count?

[Vladimir Goryachev]

I think that not including the upper bound is the correct way.

[Scott Morrison]

No objection from me. All I care about is the last statement in the file, which I need for something else. :-)

[Yaël Dillies]

Oh please, I look away 5min and here are 11 commits waiting to be pulled :rofl:

[Scott Morrison]

I merged master, so Vladimir could retrieve oleans.

[Scott Morrison]

sorry

[Kyle Miller]

The prime-counting function traditionally includes the upper bound -- why is it the correct way not to include it?

[Vladimir Goryachev]

Scott Morrison said:

If you:

git checkout master
leanproject up
git checkout count
git pull
leanproject build

I tried to do it, didn't help. The Inf in the def nth gets the red line.

[Scott Morrison]

What is the error message?

[Scott Morrison]

Did you get any errors from leanproject up?

[Vladimir Goryachev]

failed to synthesize type class instance for
p : ℕ → Prop,
_inst_1 : decidable_pred p,
nth : ℕ → ℕ,
n : ℕ
⊢ has_Inf ℕ

[Scott Morrison]

Weird. What do you get from lean --version?

[Vladimir Goryachev]

Lean (version 3.27.0, commit de35266fe596, Release)

[Vladimir Goryachev]

leanproject up gave no error messages, just said it found some local oleans

[Scott Morrison]

Did you install elan? It seems you might have installed a fixed version of Lean, which won't work. You need elan, which will look at the repository you are working in and pick the right version automatically.

[Scott Morrison]

oh! I now get the same error message...

[Scott Morrison]

Sorry. :-)

[Eric Rodriguez]

regardless of whether you get the same error, that's definitely the wrong version of lean ;b

[Scott Morrison]

Yes, so you should still sort of out the lean version.

[Scott Morrison]

But the has_Inf error I've fixed (by adding an import --- when I updated to master, someone must have removed a transitive import in the meantime, so we weren't importing data.nat.lattice anymore...)

[Eric Rodriguez]

ahh, #8708

[Vladimir Goryachev]

Thanks, that error message disappeared!

[Vladimir Goryachev]

And I have elan 0.11.0 (b25724876 2021-03-09)

[Eric Rodriguez]

wait, did you run lean --version from the mathlib directory?

[Eric Rodriguez]

or somewhere else?

[Vladimir Goryachev]

I don't remember, probably from the root. Anyway, I ran elan update, and I now have lean version 3.32.1 (though elan update had errors while self-updating)

[Eric Rodriguez]

because the thing is that lean is a smart executable and can execute different versions depending on where you are

[Eric Rodriguez]

so it really does matter in which directory you run it

[Vladimir Goryachev]

Okay, thanks! I think that is now sorted out.

[Scott Morrison]

I'm off for the evening, good luck everyone. :-)

[Kyle Miller]

(I accidentally just pushed without making sure there were no errors after dealing with a merge conflict...)

(never mind, it's all fine)

[Yaël Dillies]

Where is this gone?

lemma count_succ_eq_succ_count {n : ℕ} (h : p n) :
  count p (n + 1) = count p n + 1 :=

[Yaël Dillies]

There was a proof and I can't find it anymore.

[Yaël Dillies]

Ah, found it!

[Vladimir Goryachev]

If I want to add a change, do I just git push origin count?

[Yaël Dillies]

Yes

[Kyle Miller]

@Yaël Dillies What's going on down here?

image.png

[Yaël Dillies]

Whoops, that's unwanted. Delete the second one.

[Yaël Dillies]

I'm in orange bar hell :slight_frown:

[Eric Rodriguez]

leanproject get-cache --rev=f36c98e877dd86af12606a and a restart server always fixes my orange bar hell :)

[Kyle Miller]

there seem to be some errors in the current commit -- i'm going through and fixing them and will be pushing in a moment

[Kyle Miller]

ok, they're fixed

[Vladimir Goryachev]

As far as I understand, the line lemma nth_count (n : ℕ) (h : p n) : nth p (count p n - 1) = n should not have "- 1" in it. I have tried to push this tiny change. Did it work?

[Kyle Miller]

@Vladimir Goryachev It looks like you just merged the remote branch and pushed your merge commit

[Kyle Miller]

(and I just pushed my own merge commits)

[Vladimir Goryachev]

What does it mean? Or maybe I could read about it somewhere?

[Vladimir Goryachev]

I am just really new to github

[Kyle Miller]

It doesn't include the removal of the "- 1"

[Kyle Miller]

What are you using for git?

[Vladimir Goryachev]

"What" in what sense? I just type "git push origin count" in the terminal.

[Kyle Miller]

There are many interfaces -- GitHub has a graphical application you can use, for instance. I personally use magit in Emacs, though sometimes I do a command in the terminal

[Kyle Miller]

Have you become acquainted with "git status" yet? it shows you the files that you have changed locally. To create a commit, you can use git add ...filenames and then git commit -m "short message". At this point, you want to git pull origin count to merge any changes others have made (and then possibly deal with merge conflicts...), and then git push origin count.

[Kyle Miller]

but for a colleague who was new to git this summer, I set him up with GitHub Desktop, which seemed to work well.

To learn more than you need to know about git, there's the Pro Git book

[Vladimir Goryachev]

Thanks! It seems it worked. And I will look into those resources.

[Kyle Miller]

We can confirm it worked: https://github.com/leanprover-community/mathlib/commit/0c0484d9e67eef92e3d1f074adab91efbcb527b6

[Vladimir Goryachev]

Great, thank you!

[Vladimir Goryachev]

(I've pushed one more change to remove the error in the last definition)

[Kyle Miller]

If you look at the end of https://github.com/leanprover-community/mathlib/compare/count, you can see two commits that you created. The first contains your change, with respect to what you thought was the current version of the repositiory, and the second is a "merge commit" that joins together two histories: your local one and the remote (GitHub) one. Earlier you had pushed a merge with no changes.

[Vladimir Goryachev]

Thanks!

[Kyle Miller]

I don't know if I'd ever seen it on the GitHub website, but other tools can show you how the various histories intertwine -- which commits refer to which commits.

In this one, time goes upwards:

image.png

[Scott Morrison]

Vladimir Goryachev said:

As far as I understand, the line lemma nth_count (n : ℕ) (h : p n) : nth p (count p n - 1) = n should not have "- 1" in it. I have tried to push this tiny change. Did it work?

I think the -1 is correct: remember that nth is zero-indexed!

[Vladimir Goryachev]

well, say p is always true, n = 1. Then count p 1-1 = count p 0 = 0, nth p 0 = 0 rather than 1. So -1 breaks things.

[Scott Morrison]

Oh, we changed to counting in {0,...,n-1}! Sorry, my mistake.

[Yaël Dillies]

GC, GC, GC!

[Yaël Dillies]

I completed the count_succ lemmas to try an induction, if that sparks ideas.

[Kyle Miller]

Make sure to check what's in a commit before pushing it. This one introduced duplicate lemmas (and for some reason replaced the count_succ proofs that I had fixed earlier). This one deletes my proof of exists_gt_of_infinite, causing Eric to reprove it later.

[Kyle Miller]

There are bound to be merge issues with so many people editing the same small file simultaneously, which means extra diligence needed :smile:

[Eric Rodriguez]

aah the lemma was right there why did I go round loops to prove the same thing LOL

[Yaël Dillies]

But I do check the diff before merging :big_frown: It must be lying a bit.

[Scott Morrison]

When I'm working on a branch that others are working on actively, sometimes I will do some work without committing, then run git stash, git pull, git stash apply. It's hard to go wrong this way.

[Scott Morrison]

I just made some good progress on branch#count. In particular, the main statement I want

def set.infinite.order_iso_nat {s : set ℕ} (i : s.infinite) : s ≃o ℕ := ...

still has a bunch of sorries, but they all seem very doable! Again if anyone wants to help fill in a few please do so.

[Scott Morrison]

The route I found does _not_ go via building the galois connection, so I took the liberty of moving everything off the direct route to order_iso_nat below it.

[Scott Morrison]

In fact, I think the galois connection is consequence of order_iso_nat and nth_count without too much difficulty.

[Vladimir Goryachev]

Hello! I did some work towards the galois connection. I would appreciate some feedback, as this is my first attempt to push some code, rather that delete a -1.

[Vladimir Goryachev]

Also, I feel that nth_count_le would be useful in the galois connection proof, so I moved it upwards

[Vladimir Goryachev]

Also, could someone explain me why can't the first sorry in count_nth_gc be simply closed by exact hc? The goal and the hc statement look identical to me.

[Ruben Van de Velde]

You can try convert hc and see what it leaves as goals

[Vladimir Goryachev]

Thanks. It leaves nothing at all!

[Vladimir Goryachev]

I feel bewildered about that.

[Vladimir Goryachev]

I have pushed convert hc and closed this sorry.

[Anne Baanen]

Vladimir Goryachev said:

Thanks. It leaves nothing at all!

That means the difference is too big for the unifier to figure out, but just small enough for convert (really congr) to figure out, so it's probably some term in a subsingleton type. From looking at the code, it might be a clash between open_locale classical and variable [decidable_pred p]: classical.decidable p is not definitially equal to any instance argument, but decidable has a subsingleton instance that congr can use.

[Eric Rodriguez]

take care with the merge in the future - I think you merged the wrong way round, so the merge commit made a weird diff

[Eric Rodriguez]

also when you split into subgoals, it's in mathlib style to always brace around it - it makes the code a lot more readable

[Eric Rodriguez]

but otherwise this is very good, thanks!

[Vladimir Goryachev]

Thanks. Where can I see that the diff is weird?

[Eric Rodriguez]

@Scott Morrison whilst looking for some other stuff, I found docs#nat.subtype.order_iso_of_nat; is this good enough for what you needed it? (not to discourage you from working on this branch too ;b)

[Eric Rodriguez]

https://github.com/leanprover-community/mathlib/commit/baf6d178760376981c38c2bfb286562f105d560e @Vladimir Goryachev

[Vladimir Goryachev]

Thanks, will be more careful.

[Scott Morrison]

@Eric Rodriguez that's perfect! I should try library_search more often. :-)

[Scott Morrison]

I suspect we can relate that existing order iso to count and nth, and this will be helpful for building the galois connection.

[Vladimir Goryachev]

Finished the proof of the Galois connection (modulo the lemmas it uses)

[Vladimir Goryachev]

By the way, is it possible and/or useful to create notation p[m] =nth p m? It is potentially easier to read (e.g nat.prime[m] makes a lot of sense for me).

[Scott Morrison]

It's possible, but I'm always inclined to be very cautious introducing new notation.

[Scott Morrison]

And certainly anything involving square brackets is dangerously prone to clashing with other notations.

[Eric Rodriguez]

I think we should definitely use a lot more use of localised notation, though; I think it's a great shame the amount of long function names we end up using often

[Eric Rodriguez]

Especially with the open scoped stuff in Lean4

[Vladimir Goryachev]

Okay. Also, should one place a space after a \<- ? The styleguide doesn't say anything about it, but there are such spaces in the examples there.

[Scott Morrison]

The style guide is silent on that, and both seem acceptable.

[Eric Rodriguez]

same as the style guide on ending commas, which I'm glad we won't have to deal with in Lean4 because there's huge variances on what's what

[Anne Baanen]

I searched for all lines containing simp or rw and counted how many ←s there were with and without a space: about 3100 without a space and 7400 with a space.

[Vladimir Goryachev]

Thanks.

[Vladimir Goryachev]

I did some work on nth_succ_of_zero, and I hope it is in the right direction. The goal there was of type Inf ... = Inf ... + 1, and it looked like if I manage to put this + 1 inside the Inf, the sets will become equal. So I wrote a lemma (yet without proof) that Inf {m : ℕ | p m} + n = max (Inf {m : ℕ | p (m - n)}) n, which I could not find in the file with Infs, applied it, and began to iron out the edge cases where the right Inf is zero.

[Eric Rodriguez]

are you sure Inf_plus is the right way to do this? On your second by_cases, we'd need p 1, which I don't think we either have nor could figure out (remember, ∀ x, 0 - x = 0)

[Vladimir Goryachev]

We have p 1, it is called hp

[Vladimir Goryachev]

It seems to me this approach would work, but I am not sure this is the right way.

[Vladimir Goryachev]

Also, it can be the case that the better form of Inf_plus is lemma Inf_plus {n: ℕ} {p: set ℕ} (h: 0 < Inf {m : ℕ | p m}) : Inf {m : ℕ | p m} + n = Inf {m : ℕ | p (m - n)}

[Vladimir Goryachev]

(Because it is stronger)

[Eric Rodriguez]

you get p 1 from h0 which needs p 1 in and of itself

[Eric Rodriguez]

like to actually be proved

[Vladimir Goryachev]

h0 is getting Inf = 0 from (not 0 < Inf), this should be closed trivially.

[Vladimir Goryachev]

I can commit it in a few minutes

[Vladimir Goryachev]

Done. Also have changed Inf_plus statement.

[Vladimir Goryachev]

I have just proved Inf_plus, but I see something was done on it 7 minutes ago.

[Vladimir Goryachev]

So I guess if I push my proof now, this would cause a merge problem, wouldn't it?

[Scott Morrison]

You won't be able to push unless you first merge the remote changes.

[Scott Morrison]

Start with git pull and hope for the best!

[Vladimir Goryachev]

Okay. I pushed my proof, putting it into lemma Inf_plus', because I felt uncomfortable deleting the existing beginning of a proof.

[Eric Rodriguez]

don't worry about it, a full proof is better than my half-baked attempt at one :b

[Vladimir Goryachev]

I have proved count_nth_of_infinite. I think basically same proof would work for bounded cardinalities, and then we would be able use it all over, as having one-sided inverse is neat.

[Vladimir Goryachev]

I would be thankful if someone filled up count_eq_card_finset, which is basically expressing count in terms of finset.card - it should be trivial, but I have not learned to work with cardinalities different from finset yet.

[Kyle Miller]

I'll take a look

[Kyle Miller]

You were right about triviality, the proof ended up being rfl :smile:

[Kyle Miller]

I had a longer proof that ended with the refl tactic, and I kept deleting lines until nothing was left.

[Vladimir Goryachev]

Thanks! Trivial indeed : )

[Eric Rodriguez]

i'm surprised it's rfl, I thought finset was some level of list quotients and proofs with quotients couldn't be rfl

[Eric Rodriguez]

that's nice

[Kyle Miller]

@Eric Rodriguez Here's what's going on: a finset is a nodup multiset, and a multiset is the quotient of list by list.perm. The definition of finset.card is multiset.card of its multiset, and the definition of multiset.card is the list.length of a representative list (using quot.lift for well-definedness). Similarly, both finset.range and finset.filter are defined in terms of list.range and list.filter, in that the latter functions are by definition the list representatives for the finsets.

A key fact is that Lean has the following reduction rule (where reduction is what underlies what it means for things to be defeq):

quot.lift f p (quot.mk a) ~~> f a

So, for example,

(finset.range 37).card ~~> quot.lift list.length _ (quot.mk (list.range 37))
                       ~~> list.length (list.range 37)

We can see this in action for count_eq_card_finset using #reduce:

#reduce λ (n : ℕ), finset.card (finset.filter p (finset.range n))
-- λ (n : ℕ), (filter p (range_core n nil)).length

[Kyle Miller]

Another example of something involving quotients that's intentionally defeq to something more basic is the edge set for simple graphs. It's convenient how ⟦(v, w)⟧ ∈ G.edge_set is by definition G.adj v w.

[Vladimir Goryachev]

The main problem in the case of finite p was that we didn't have prove that the set over which we take Inf is nonempty (unlike in the infinite case, where it is easily infinite). Now I have proved lemma nth_mem_of_le_card_aux, which computes the cardilities of those sets, allowing to prove them to be nonempty.

[Vladimir Goryachev]

(Renamed the lemma, and proved a slightly stronger lemma nth_set_card)

[Vladimir Goryachev]

And now I have proved p(nth p n) in the finite case.

[Vladimir Goryachev]

I have proved nth_count. Again, I haven't deleted the existing unfinished proof, and added my proof as nth_count' instead. Please tell me if it is fine to remove the unfinished proof.

[Johan Commelin]

Usually replacing an unfinished proof by a complete proof is fine. And if the old proof exists in the git history, then people can dig it up there if they want/need it.

[Kyle Miller]

I'm going through things right now, by the way @Vladimir Goryachev. I'll delete the old proof.

[Kyle Miller]

@Vladimir Goryachev I've pushed my changes and am done for now. I tried simplifying proofs, and hopefully I succeed in not obfuscating them.

[Vladimir Goryachev]

@Kyle Miller Thanks! I do hope I will learn to write those shorter proofs at some point.

[Vladimir Goryachev]

I have proved count_nth_le. I think it means that the galois connection theorem is now proved completely (without sorries all the way down). I think I will try look at the latest edits Kyle Miller has made to the file and try to edit my last proof accordingly.

[Kyle Miller]

@Vladimir Goryachev A way you can check is to use the #print axioms count_nth_gc command. If it's sorry-free, it won't print [sorry], and I can confirm it doesn't.

[Vladimir Goryachev]

@Kyle Miller I have finally looked into your edits. I understood that I should use squeeze_simp rather than simp, and I have changed it in my latest commit. Could you maybe give some other general advise on how to write proofs so that they do not require cleaning up, please?

[Kyle Miller]

It's probably better not to worry too much about it while doing the hard part of actually finishing the proofs in the first place. Later on, you can go in with your sandpaper to give the proof a nicer finish.

I think mainly what helped were the refine, convert and convert_to tactics, and also noticing when small arguments could be passed directly to a lemma in an apply. What could also help is studying what is going on overall in a theorem, to try to make things that would be defined with a have be automatically generated as a subgoal.

For example, in nth_count_eq_Inf, I notice

        apply count_strict_mono,
        { exact hp, },
        { exact ha, },

Looking at the type of count_strict_mono, we see it takes the predicate p along with two proofs. So, we can simplify this to

        exact count_strict_mono _ hp ha,

(I used an underscore since it can figure out p, but you could also write p in its place. Doesn't matter either way.)

[Kyle Miller]

Or, consider the large-scale structure of the proof:

lemma nth_count_eq_Inf {n : ℕ} : nth p (count p n) = Inf {i : ℕ | p i ∧ n ≤ i} :=
begin
  rw nth,
  have h: {i : ℕ | p i ∧ ∀ (k : ℕ), k < count p n → nth p k < i} = {i : ℕ | p i ∧ n ≤ i},
  { ... },
  rw h,
end

After rw nth, the left-hand side becomes Inf, and h is for rewriting its set. Instead, you can do

lemma nth_count_eq_Inf {n : ℕ} : nth p (count p n) = Inf {i : ℕ | p i ∧ n ≤ i} :=
begin
  rw nth,
  congr' 1,
  ...
end

since congr' 1 will create the exact hypothesis you've written for have h. I find it easier to follow in this form since there isn't this lone rw h at the very end.

[Ruben Van de Velde]

Or

lemma nth_count_eq_Inf {n : ℕ} : nth p (count p n) = Inf {i : ℕ | p i ∧ n ≤ i} :=
begin
  rw nth,
  suffices h : {i : ℕ | p i ∧ ∀ (k : ℕ), k < count p n → nth p k < i} = {i : ℕ | p i ∧ n ≤ i},
  { rw h },
  ...
end

[Kyle Miller]

Another pattern: rather than

    apply lt_of_lt_of_le,
    swap,
    { exact hn,},

you can use refine like so:

    refine lt_of_lt_of_le _ hn,

I think this makes it clearer that the intent is, that the rest of the proof is to fill in the less-than part of this transitivity proof.

[Kyle Miller]

After some transformations like these, it ended up in this form:

lemma nth_count_eq_Inf {n : ℕ} : nth p (count p n) = Inf {i : ℕ | p i ∧ n ≤ i} :=
begin
  rw nth,
  congr' 1,
  ext a,
  simp only [set.mem_set_of_eq, and.congr_right_iff],
  intro hp,
  split,
  { intro h,
    by_contra ha,
    push_neg at ha,
    have hn : nth p (count p a) < a := h _ (count_strict_mono _ hp ha),
    rwa [nth_count p hp, lt_self_iff_false] at hn, },
  { intros hn k hk,
    refine lt_of_lt_of_le _ hn,
    apply (count_monotone p).reflect_lt,
    convert hk,
    obtain (hfi|hfi) := em (set.finite p),
    { rw count_nth_of_lt_card_finite _ hfi,
      apply lt_trans hk,
      apply lt_of_le_of_lt,
      { exact count_monotone _ hn, },
      { exact count_lt_card p hfi hp, }, },
    { apply count_nth_of_infinite p hfi, }, },
end

I find it to be relatively easy to follow this kind of proof with the infoview, but these things are a matter of taste.

(I didn't commit this change)

[Vladimir Goryachev]

Thank you very much for your advise! So, do you say that I should first finish the file, so that no sorries are left, and only then begin refactoring?

[Vladimir Goryachev]

And I commited the little changes, in line with your recommendations.

[Vladimir Goryachev]

Do we still have a need for nth_succ_of_zero? I think it is easy to prove now, but it seems like an auxiliary lemma which I have bypassed by using other proofs. Do you consider it still relevant?

[Scott Morrison]

I think it can be dropped.

[Scott Morrison]

Something that will be essential for PRing this material is connecting it with what is already in docs#nat.subtype.order_iso_of_nat.

[Scott Morrison]

(and higher up in that file)

[Scott Morrison]

Sorry, wrong link

[Scott Morrison]

I meant docs#nat.subtype.of_nat

[Scott Morrison]

at the least we need lemmas relating this to nth.

[Scott Morrison]

possibly we should redefine it in terms of nth.

[Vladimir Goryachev]

Thanks. I will look into it - I'm still unsure how to work with those types of objects though.

[Vladimir Goryachev]

Also - can anyone help me with why in the nth_lt_of_lt_count proof the line "apply lt_of_count_lt" (now the only line commented out) does not work, and how to fix it?

[Vladimir Goryachev]

I want to finish the last couple of lemmas in the end of the file first, and then I'll think about nat subtypes.

[Vladimir Goryachev]

I have finished the proof of nth_lt_of_lt_count. I have removed the lemma nth_le_of_le_count, as it is wrong: even though 2 \le count nat.prime 4, we do not have nth nat.prime 2 \le 4.

[Yaël Dillies]

It sounds like it was the wrong way around. le_nth_of_count_le should be correct instead.

[Yaël Dillies]

and similarly lt_nth_of_count_lt should be wrong.

[Yaël Dillies]

I love Galois connections :heart_eyes:

[Vladimir Goryachev]

Yeah, sure, le_nth_of_count_le is now trivial. Done it!

[Yaël Dillies]

If you want to turn iff into one way implications, you can use alias iff_theorem ↔ name_of_the_first_imp name_of_the_second_imp.

[Vladimir Goryachev]

I could not actually do it, as the Galois connection lemma uses assumptions that p is infinite, but those lemmas do not.

[Yaël Dillies]

Well one of them must use it. You can place an _ instead of the lemma you don't want alias to generate.

[Vladimir Goryachev]

No, those lemmas are equivalent, as they are just contrapositions of each other. And none of them assume infinitude of p.

[Yaël Dillies]

Neither of the ← and → implications need p infinite, but ↔ does? Is it really what you mean?

[Vladimir Goryachev]

No. I mean that one of -> and <- is not implemented, and we have a -> b and ~b -> ~a instead.

[Vladimir Goryachev]

I have proved the lemma nth_nonzero_of_ge_nonzero and removed another lemma which seemed like a leftover of a no longer relevant proof by induction. Now the only sorry left is to prove nth_eq_order_iso_of_nat.

[Yaël Dillies]

Ah yes, that's different indeed. Good work by the way!

[Vladimir Goryachev]

I have finished the proof of nth_eq_order_iso_of_nat!

[Vladimir Goryachev]

@Scott Morrison you were particularly interested in that.

[Vladimir Goryachev]

Also, this means that no sorries are currently left in the count file!

[Vladimir Goryachev]

So I would like to ask everyone's advise on what to do next. I have seen the idea that PRs should be kept fairly small and manageable, so I would be inclined to polish up the existing lemmas, rearrange them and PR the file. But I am new to mathlib development, and so I am not sure how things are done here.

[Yaël Dillies]

I'm willing to go through the file, fix lemma names if needed and such... if you want.

[Yaël Dillies]

I very much love file restructuring :heart_eyes:

[Vladimir Goryachev]

Oh, you are definitely welcome!

[Vladimir Goryachev]

I usually prefer writing new code to restructuring the old one : )

[Eric Rodriguez]

OK, so I've pushed some changes; mostly golfing (-200 lines or so!) to the file. I think most changes should be done by now! I also fixed (hopefully) all linting issues. I'd appreciate if one of you could check the file (especially the names of stuff, @Yaël Dillies your skills would be appreciated :]) but I think we should PR this sooner rather than later so that stuff doesn't bitrot

[Yaël Dillies]

Let me have another look!

[Yaël Dillies]

I must say I see absolutely no point in using cardinal. This to me seems like a pretty artificial way to unify the cases where p is true finitely vs infinitely often.

[Yaël Dillies]

count_succ' is a too specialized case of count_add {a b : ℕ} : count p (a + b) = count p a + count (λ k, p (a + k)) b. I'm trying to prove that now.

[Yaël Dillies]

Done!

[Eric Rodriguez]

how come you localised the instance?

[Yaël Dillies]

Isn't it a pretty peculiar use-case? We're providing a fintype instance for the coercion to Sort of a sep of the set of naturals strictly less than n.

[Eric Rodriguez]

I feel like it's not going to hurt anyone to have it around, either

[Yaël Dillies]

Would it make sense to feed in (set_of p).infinite through TC inference?

[Eric Rodriguez]

hmm, I feel like there's some good reason why infinite isn't a class already though

[Yaël Dillies]

Yeah sure. I meant to use fact

[Eric Rodriguez]

no strong feelings either way there

[Scott Morrison]

I would avoid writing things using fact unless it really makes life fundamentally easier at the point of use.

[Kyle Miller]

I'm pretty sure count_set.fintype should be an instance, but generalized a bit. This could go in data.set.finite:

instance set.finite.fintype_pred_sep {α : Type*} (p : α → Prop) [fintype {x | p x}]
  (q : α → Prop) [decidable_pred q] :
  fintype {x | p x ∧ q x} :=
by apply set.fintype_sep {x | p x}

-- Now it's automatic:
def count_set.fintype (p : ℕ → Prop) [decidable_pred p] (n : ℕ) : fintype {i | i < n ∧ p i} :=
infer_instance

[Kyle Miller]

@Yaël Dillies I see you changed (set_of p).finite back to set.finite p. The issue is that p is not a set, so set.finite p is "wrong".

[Yaël Dillies]

I am pretty sure it has already been used like that in mathlib... There's not even any coercion as set is a type synonym.

[Kevin Buzzard]

yeah but it's breaking the abstraction barrier

[Kevin Buzzard]

Maybe someone decides to make set irreducible one day and then your code breaks.

[Kyle Miller]

It's breaking the abstraction barrier. I carefully went through everything in this a while back to make sure whenever a predicate is used as a set, it's cast using set_of.

[Yaël Dillies]

Oh well, sorry about that.

[Kyle Miller]

What's wrong with cardinals? I'm just going to record the deleted lemmas here in case @Scott Morrison has any comment, since he added originally them I believe.

lemma count_nth_of_lt_card (n : ℕ) (w : (n : cardinal) < cardinal.mk (set_of p)) :
  count p (nth p n) = n

lemma nth_mem_of_lt_card (n : ℕ) (w : (n : cardinal) < cardinal.mk (set_of p)) : p (nth p n)

Also, did this one go somewhere, or is it a trivial consequence of other lemmas so was deleted?

lemma nth_nonzero_of_ge_nonzero (h : ¬p 0) (a k : ℕ) (ha: a ≤ k) (h : nth p k ≠ 0) :
  nth p a ≠ 0

[Yaël Dillies]

It's now nth_zero_of_nth_zero.

[Yaël Dillies]

The only thing you're doing with cardinals is checking the finite case, and the omega case. There's nothing more happening with them and, as expected, they aren't used by anything else.

[Kyle Miller]

Yaël Dillies said:

they aren't used by anything else.

Let's delete the whole file then, since none of it's being used elsewhere :smile: (I know that's not fair, since we know one of the theorems has use in another project.)

It's possible they have limited future utility -- just wanted to make sure Scott had a chance to notice their departure.

[Kyle Miller]

It looks like there's an accidental battle between rw and simp in the git history. I think rw has won this match :checkered_flag:

instance count_set_fintype (n : ℕ) : fintype {i | i < n ∧ p i} :=
fintype.of_finset ((finset.range n).filter p)
  (λ x, by rw [mem_filter, mem_range, set.mem_set_of_eq])

--> two days ago

instance count_set_fintype (n : ℕ) : fintype {i | i < n ∧ p i} :=
fintype.of_finset ((finset.range n).filter p) (by simp)

--> yesterday

def count_set.fintype (n : ℕ) : fintype {i | i < n ∧ p i} :=
fintype.of_finset ((finset.range n).filter p)
  (λ x, by rw [mem_filter, mem_range, set.mem_set_of_eq])

[Yaël Dillies]

Whooops. The fervent partisan of "A simp should not replace less than two full lines of rw" is me.

[Scott Morrison]

My take on the simp vs rw "war" is that replacing simp with rw is nice for explicitness and speed --- but this shouldn't come at the cost of really polishing and perfecting the simp set, if only for downstream users.

[Scott Morrison]

I'm happy with the deleted lemmas staying deleted.

[Eric Wieser]

Regarding a lemma upthread; note that sep (docs#has_sep) refers to {x ∈ s | p x} not {x | p x}

[Eric Rodriguez]

do you still think that lemma has the right name?

[Eric Wieser]

No, fintype_pred_sep should probably be called fintype_setof_and_right

[Vladimir Goryachev]

I did the PR! I hope I followed the conventions correctly : )

[Eric Rodriguez]

#9457!

[Scott Morrison]

Could you update the top post of the PR to include coauthor information? Format is:
Co-authored-by: Name Name <email@address.com>
(don't worry to much about getting the emails right; you could try pulling them off here)

[Vladimir Goryachev]

So, I finally got my computer back, and hope to continue working on this PR.

[Vladimir Goryachev]

@Scott Morrison, I have updated the top post of the PR as you have asked.

[Vladimir Goryachev]

When I try to open the count file in VS code, it underlines literally everything with red, saying that there is not enough memory. Am I the only one to have this problem? Could any other changes to mathlib have broken something here?

[Johan Commelin]

@Vladimir Goryachev (1) How much memory do you have? (2) Did you git pull and leanproject get-cache recently?

[Vladimir Goryachev]

1) Which memory exactly? Where do I look it up?
2) I have deleted and redownloaded the mathlib_count branch half an hour ago, so I hope it would solve any such problems.

[Johan Commelin]

But did you run leanproject get-cache?

[Vladimir Goryachev]

I have right now, it Failed to fetch cached oleans

[Yaël Dillies]

Update elan. It now gives you the name of the commit you can try.

[Johan Commelin]

Did you mean "Update leanproject"?

[Yaël Dillies]

Eh yes

[Vladimir Goryachev]

Saying leanproject update (while inside mathlib_count folder) also results in Failed to fetch cached oleans

[Vladimir Goryachev]

So can I assume that only have this problem?

[Johan Commelin]

I think you need pip install -U mathlibtools to update leanproject

[Kevin Buzzard]

This problem can be fixed, your issue is that your computer doesn't want to compile all of Lean's maths library but there is a way of getting it to download compiled files which will solve the memory errors

[Vladimir Goryachev]

If I download the master branch, it compiles just fine. If I download the count branch, it has memory problems. So I would think that my problems have to do something not with leanproject nor with the memory of my computer, but with something in the count branch.

[Vladimir Goryachev]

That's why I ask if anyone has the same problems with this branch.

[Johan Commelin]

The count branch is probably quite a bit older than current master. So the olean files don't match.

[Johan Commelin]

What is the exact branch name? I'll try.

[Vladimir Goryachev]

@Johan Commelin, count

[Johan Commelin]

@Vladimir Goryachev which file should I open?

[Yaël Dillies]

data.nat.count

[Vladimir Goryachev]

data/nat/count

[Johan Commelin]

Works flawlessly for me

[Johan Commelin]

Here is what I did:

git checkout count
git pull
leanproject get-cache

[Johan Commelin]

After that, I opened mathlib in VScode, and opened data/nat/count.

[Johan Commelin]

There were orange bars for 2-3 seconds, that's it.

[Vladimir Goryachev]

Thanks! I still have the problem, I'll try to figure something out.

[Alex J. Best]

Do you have any other (modified) files open in vscode

[Scott Morrison]

What was the output from leanproject get-cache?

[Vladimir Goryachev]

@Alex J. Best, no

[Vladimir Goryachev]

@Scott Morrison, now it says something that includes

There are multiple viable caches from parent commits:
ee74b6717
e61584d59

[Alex J. Best]

Try leanproject get-cache --fallback=download-all

[Vladimir Goryachev]

Screenshot-from-2021-10-19-23-41-38.png

[Vladimir Goryachev]

@Alex J. Best, what you have said did download something, but it did not solve the problem with memory

[Alex J. Best]

Did you restart the lean server after the download?

[Scott Morrison]

What was the output from leanproject get-cache --fallback=download-all?

[Vladimir Goryachev]

Screenshot-from-2021-10-19-23-50-27.png

[Vladimir Goryachev]

I have reinstalled mathlib_count again, and did this thing, here is what I got. The memory problem persists.

[Vladimir Goryachev]

How do I uninstall Lean, if I'd like to try it out?

[Scott Morrison]

How did you install elan? If you installed it via the shell script, you can rm -rf ~/.elan.

[Scott Morrison]

How are you opening your .lean file? You're opening the mathlib folder in VSCode, not some subfolder, right?

[Vladimir Goryachev]

Yes, mathlib folder.

[Vladimir Goryachev]

Trying to reinstall elan did not help.

[Kevin Buzzard]

Just to be clear, the oleans you should be getting are from commit ee74b67171.

[Kevin Buzzard]

I can confirm that data.nat.count works fine for me on the count branch with those oleans. What is the output of leanproject --version? If it's not 1.1.0 you could try updating.

[Kevin Buzzard]

Vladimir Goryachev said:

Saying leanproject update (while inside mathlib_count folder) also results in Failed to fetch cached oleans

This shouldn't happen. Is your local copy of count equal with the version on github? Did you try

git checkout count
git pull
leanproject get-cache

? What does git status look like after these commands? Does get-cache get the oleans for ee74b67171?

[Vladimir Goryachev]

@Kevin Buzzard are you sure it is ee74b67171? I have ee74b6717.

[Vladimir Goryachev]

version of leanproject is 1.1.0, version of lean is 3.33.0

[Vladimir Goryachev]

I have tried the three lines, though I have to use git pull origin count, as otherwise it does not understand where to pull from.

[Kyle Miller]

Vladimir Goryachev said:

are you sure it is ee74b67171? I have ee74b6717.

A slightly confusing thing about git: a full commit id is 40 characters, but git will report an unambiguous prefix given all the other commits in the repository. These two likely refer to the same thing.

[Vladimir Goryachev]

if I specify leanproject get-cache --rev ee74b6717, it says that it applies cash and deletes two zombies.

[Vladimir Goryachev]

git status returns

On branch count
nothing to commit, working tree clean

[Scott Morrison]

After you've run leanproject get-cache, you should be able to run leanpkg build and have it return quickly (<20s). Could you confirm that? Or is it recompiling, even on the command line?

[Kyle Miller]

(I should also say that it doesn't hurt to give more of the commit id: leanproject get-cache --rev ee74b67171b26da3fa6f3a8b4af5ea2d7b333137 is the full form, based on the commits I see here. I clicked on the first one and looked at the url.)

[Vladimir Goryachev]

@Scott Morrison It is recompiling on the command line.

[Scott Morrison]

That is ... weird. Can you show us the output of leanproject get-cache --rev ee74b6717, and the output of git status?

[Kevin Buzzard]

Have you made local changes? If you pull and push does anything happen? This is difficult to debug because it's working for everyone else

[Vladimir Goryachev]

@Scott Morrison Screenshot-from-2021-10-21-03-35-36.png

[Scott Morrison]

and now leanpkg build?

[Vladimir Goryachev]

Does not intend to stop. Screenshot-from-2021-10-21-03-40-04.png

[Scott Morrison]

Okay, somehow you have got a bad local cache. Let's force it to pull a new one.

[Vladimir Goryachev]

How do I do it? And should I let this thing run to completion, or terminate it?

[Scott Morrison]

no ,kill it

[Scott Morrison]

I'm just checking locally for you

[Yakov Pechersky]

To me that looks like some core Lean file got changed. Uninstalling and reinstalling elan might not have done anything because it might not have cleaned out the existing core lean files. And when you reinstalled it, it was happy to use the files that already existed.

[Scott Morrison]

Try

rm ~/.mathlib/ee74b67171b26da3fa6f3a8b4af5ea2d7b333137.tar.xz
leanproject get-cache
leanpkg build

[Scott Morrison]

If that still fails, we'll need to work out how to more thoroughly clean your system.

[Bryan Gin-ge Chen]

Yakov Pechersky said:

To me that looks like some core Lean file got changed. Uninstalling and reinstalling elan might not have done anything because it might not have cleaned out the existing core lean files. And when you reinstalled it, it was happy to use the files that already existed.

I think there was a change to elan a while back that made core Lean files read-only (though that's certainly still a possibility).

[Vladimir Goryachev]

It failed. Is there a way to delete everything connected to Lean completely, to reinstall it again?

[Scott Morrison]

It can depend a bit on what installation method you used, but deleting ~/.mathlib and ~/.elan is a good start.

[Scott Morrison]

If after that lean fails at the command line, you're probably good to start over again.

[Vladimir Goryachev]

@Scott Morrison Did not help.
Also, is it expected behavior that if I take the master branch, and slightly edit data.nat.basic (e.g. add an additional enter), then most other files in nat (e.g. data.nat.lattice) do not recompile in time and get this "excessive memory consumption"?

[Vladimir Goryachev]

Also, in the general branch, there was a discussion that elan broke two days ago, right before I tried to get back to lean. Could it be relevant?

[Vladimir Goryachev]

And, do I understand my situation correctly? Mathlib takes long to compile. So there exist those olean files, which are proofs that indicate that the files are checked and are true. This count branch has inserted a couple of trivial lines in data.nat.basic, so it requires to recompile almost all the mathlib from scratch, as everything depends on nat.basic. Everyone else can simply download oleans for the count branch, but my computer does not see them for some reason. Is this correct?

[Johan Commelin]

That sounds like a correct summary to me.

[Vladimir Goryachev]

I set it to compile from the command line. I'll see how it goes.

[Vladimir Goryachev]

It is compiling. The nat files now became workable with, as their yellow stripes disappear quickly. However, the compiler showed me an error message while compiling (and then continued on). It said that it does not know the identifier sub_lt_iff_right, which is used in the lemma Inf_plus. I have googled it and only found tsub_lt_iff_right. Where is sub_lt_iff_right? Also, if I enter VS Code, it also underscore this identifier with red and says that it is unknown.

[Vladimir Goryachev]

Also, when compiling other files, the compiler sometimes warns me that data.nat.lattice uses sorry. There is no sorry there, so I guess it just says it because there is a mistake in the data.nat.lattice (the one about sub_lt_iff_right)

[Yaël Dillies]

sub_lt_iff_right (and a bucnh of other lemmas) has been renamed to tsub_lt_iff_right recently by Floris.

[Vladimir Goryachev]

Then how do Johan Commelin and Kevin Buzzard say the branch compiles just fine??

[Yaël Dillies]

You must have taken cache from master.

[Yaël Dillies]

Just merge now and everything will be alright.

[Vladimir Goryachev]

What exactly do you mean by merge here?

[Kyle Miller]

What does git rev-parse HEAD say? This will get the actual commit ID you're working with, and it would be good to check. (It ought to say ee74b67171b26da3fa6f3a8b4af5ea2d7b333137)

[Kyle Miller]

One other thing I might suggest is leanproject clean to delete all the oleans from the project and then leanproject get-cache.

Given your trouble with tsub_..., the following seems unlikely to help, but you might also check what the modified times are for a lean file and its corresponding olean. If your system clock is incorrect, potentially the lean file might appear to be newer than its olean. (I believe Lean uses modified times for olean invalidation.)

[Kyle Miller]

(I know someone who for awhile had his system clock set incorrectly by a few years, and his e-mails from the future would sit at the tops of our inboxes...)

[Vladimir Goryachev]

Everyone, thank you for your help, I figured out what happened! I am illiterate with git, so when I have read in "How to contribute to mathlib" guide that one should use leanproject get -b mathlib:shiny_lemma to contribute, I decided that this must be the default way of downloading branches. So to get the count branch, I was just saying leanproject get -b mathlib:count, followed by git pull origin count. This used to work when data.nat.basic was not altered, but it stopped to work after it was altered, as everything had to be recompiled. Now I have googled around, learned of the wonderful checkout functionality of git, and now it works and I have no problems.

So, maybe that piece of documentation should be rewritten? As people whose interest is primarily in pure mathematics are a meaningful portion of potential new contributours, I guess I am not the only one for whom it was the first time working with git. So I think instructions on how to contribute should be mindful of such people.

[Kyle Miller]

I've accidentally used -b before and been confused, too. leanproject get mathlib:count downloads the actual count branch. The -b option is just for creating new branches.

What your sequence of commands does is (1) download the master branch with its oleans, (2) create a new local branch based on that one with a name derived from mathlib:count, (3) try to merge in the origin/count branch. This leaves you in a state where you have oleans for master, and files that are some mixture of master and count (depending on how the merge went). If you then went ahead and followed the suggestion to do leanproject get-cache --rev ee74b6717 then you'd have really the wrong oleans (since they'd be for the original count branch), so no wonder Lean was trying to compile everything from scratch!

[Vladimir Goryachev]

Yeah, I understand now. In fact, I have done leanproject get-cache --rev ee74b6717, and it did download some oleans, but they (logically) did not help.

[Scott Morrison]

It's always complicated to provide "easy" tools like leanproject, but without obscuring what's going on underneath (e.g. with git). :-(

[Scott Morrison]

If you have a suggested sentence or two that we could add to the docs to that would have saved you, please propose them and we can think about incorporating them!

[Johan Commelin]

@Vladimir Goryachev Wow, that was a nasty trap. I'm very glad that you figured it out.

[Vladimir Goryachev]

Thanks!
As for changes I would propose for "How to contribute to mathlib":

• Move the part (6) upwards: it describes things which happen before opening a PR.
• Add a few words about git, e.g.

As with most projects stored on github, mathlib exists as a collection of copies, called branches. The main copy, called master, is the version which is shown to the world, and so must not include any half-finished work. So, all the other branches exist exactly for that purpose: to store various work in progress. When you complete the changes in a branch, you merge that branch with the master, making your results available to the world.

Note that while you can edit secondary branches freely, merging with the master requires approval from more experienced contributor, as described in the section "Lifecycle of a PR".

• And finally, I would add to the point 6 the following. "The simplest way to start making changes is to create your own branch. To do it, <here go the first two bullet points of the point 6>. However, if you want to get an existing branch, for example to help someone else with their changes, or to get a branch you have been working on on another computer, be sure to use <git checkout? leanproject get without -b? I am still not sure what is the community-approved way is> instead.

• (I'd also fix the typo "steps for for sharing")

[Vladimir Goryachev]

As for working on the PR.
Maybe the simplest thing would be to separate the things which are preliminary to nth and count, and PR them separately. I mean changes to data.nat.basic and data.nat.lattice, as well as lemmas list.range_add, multiset.range_add and finset.range_add (which I believe should be moved to their respective files).

The harder thing would be to redefine nat.subtype.order_iso_of_nat in terms of nth, and make the count file its dependency. Does anyone have objections to the fact that it should be done?

[Eric Wieser]

PRing lemmas deep down in the heirarchy separately is always a good idea, especially if the stuff built on top of them isn't ready yet

[Vladimir Goryachev]

OK. Should I create a separate branch for each of those changes?

[Yaël Dillies]

For each related set of changes, yes.

[Scott Morrison]

I've made a PR updating the advice for pull requests, at https://github.com/leanprover-community/leanprover-community.github.io/pull/212. Improvements welcome --- please just push changes directly, you don't need to check with me. :-)

[Johan Commelin]

@Vladimir Goryachev Would you mind reviewing :this: ?

[Vladimir Goryachev]

Thank you, this is much more clear now! The instructions look much more complete, and I think I would have much easier time if I had them available. However, I am to unproficient with the said tools to review on how optimal the proposed solutions are.

[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.