Mathlib bump

Stream: Polynomial Freiman-Ruzsa conjecture

[Scott Morrison]

I reduced the changes to the lake-manifest.json in https://github.com/teorth/pfr/pull/129/files (no functional change from my original PR, just making sure json blocks aren't unnecessarily reordered).

It compiles fine with lake build. Is there anything else to be concerned about? (If so, how about we check it in CI? :-)

[Terence Tao]

Scott Morrison said:

I reduced the changes to the lake-manifest.json in https://github.com/teorth/pfr/pull/129/files (no functional change from my original PR, just making sure json blocks aren't unnecessarily reordered).

It compiles fine with lake build. Is there anything else to be concerned about? (If so, how about we check it in CI? :-)

Hmm, as with previous bumps it caused my local version of Lean to recompile all of Mathlib, but that's fine. (I understand that I could presumably save the hour or two of building by doing lake cache get or something, but I'm not touching Lean any time soon, so I'm happy to just let it run. Still, I'm glad we waited until the project got over the finish line before approving the Mathlib rollover.)

[Yaël Dillies]

Now that we're reaching the "upstreaming" part of the project, please everyone expect mathlib bumps to become quite frequent!

[Yaël Dillies]

I would like to remind you that whenever you pull a bump PR to your local copy, you should run lake exe cache get right after. Importantly, do not click Rebuild imports or Refresh file dependencies or Restart file until you've run lake exe cache get.

[Kevin Buzzard]

So "before you upgrade, close VS Code, and don't open it again until after lake exe cache get". I usually type lake build as well before opening VS Code.

[Eric Wieser]

I don't think closing vscode is necessary any more

[Eric Wieser]

You just have to not click the popup that says "restart file" until you are actually ready to run Lean against your cache

[Adam Topaz]

crtl+shift+x is probably my most frequently used shortcut nowadays

[Kevin Buzzard]

For me closing and opening VS Code is cheap. I do it every time I fiddle on command line. Looking forward to a world where I never have to touch command line...

[Eric Rodriguez]

Developer: reload window is closing vscode but faster :)

[Eric Wieser]

Not clicking "restart file" is (in this case) "Developer: reload window" but faster :)

[Scott Morrison]

@Kevin Buzzard, what are the major things you're still doing on the command line?

• Restart file (via ctrl-shift-x) deals with out of date imports
• Under the \forall menu, selecting "Project Actions" then "Fetch Mathlib Build Cache" achieves the same as lake exe cache get
• "Developer: reload window" resolves many "how did I get into this weird state" problems.

If you're keen on a future of not needing the command line, I'd recommend you try using these as much as possible, and report back where the pain points are, or conditions when you still need the command line.

[Scott Morrison]

(this is saying the command-line-free future might already be here... in my demo talk on tuesday I installed Lean during the talk, and didn't touch a command line.)

[Yaël Dillies]

Heads up that I just bumped mathlib an hour ago.

[Yaël Dillies]

And bumped again just now.

[Terence Tao]

Yaël Dillies said:

And bumped again just now.

Just a headsup: as part of the entropy refactoring I've had to add lemmas to PFR/Mathlib/MeasureTheory/Integral/Bochner.lean , PFR/Mathlib/MeasureTheory/Integral/Lebesgue.lean ,
PFR/Mathlib/MeasureTheory/Measure/Dirac.lean , PFR/Mathlib/MeasureTheory/Measure/NullMeasurable.lean , and PFR/Mathlib/Probability/Kernel/Disintegration.lean (mostly along the lines of replacing finiteness hypotheses with countability hypotheses).

[Terence Tao]

Oof, I just discovered that updating Mathlib at the main branch causes other branches to want to update too. Now Lean is rebuilding Mathlib in the entropy refactoring branch, I hope this doesn't break too many more things

[Eric Wieser]

If you switch branch between different mathlib versions, you need to run lake exe cache get again

[Eric Wieser]

(it should use an offline cache if you were previously working on that version, but you still have to tell it to copy the files from the cache)

[Terence Tao]

Is there a way to merge changes in the main branch with changes in a refactoring branch without pushing those changes back into the main branch?

[Eric Wieser]

From the refactor branch, you can git merge the_main_branch

[Eric Wieser]

(which may be either main or master for your project, I don't know which)

[Terence Tao]

The refactor branch is currently building Mathlib files (554/1698 so far). Would it be safe to cancel this, close VSCode, run lake exe cache get and git merge master, and reopen VSCode?

[Yaël Dillies]

Yes, absolutely.

[Yaël Dillies]

Except you should git merge master then run lake exe cache get.

[Terence Tao]

Also: if I have checked out the refactor branch in VScode and then close VScode and open up a separate command line, will git still know that I am in that branch?

[Eric Wieser]

The knowledge about which branch you are in is stored in the filesystem (in the .git folder)

[Terence Tao]

ok. Trying it now :fingers_crossed:

[Terence Tao]

Oh crap there are merge conflicts

[Yaël Dillies]

Sorry :frown:

[Mauricio Collares]

git push will still sync your most recent commits (pre merge) with GitHub in case you haven't done so already

[Mauricio Collares]

Seems like the newest commit is quite recent, though

[Terence Tao]

Ugh Measure.lean is going to be a mess for a while now

[Mauricio Collares]

You can also git merge --abort if you'd rather undo it all and deal with it later

[Mauricio Collares]

(you'll lose any merging work you might have done, though)

[Terence Tao]

Actually it only created three errors in the file, hopefully I can fix them all manually.

[Terence Tao]

I was expecting an ocean of red

[Terence Tao]

Have to attend to other things right now, but hopefully this was only a speed bump.

[Terence Tao]

OK Measure.lean is repaired. Refactoring is back on track!

[Yaël Dillies]

Bumped again!

[Yaël Dillies]

A pretty big bump today, with 10 files gone.

[Yaël Dillies]

I started a bump, but got stuck on the huge statements in WeakPFR. My progress is on branch bump, if people want to have a look.

[Terence Tao]

Yaël Dillies said:

I started a bump, but got stuck on the huge statements in WeakPFR. My progress is on branch bump, if people want to have a look.

Yeah, the proofs I just put in there are a bit of a mess, I was not prepared for just how complicated it would be in particular to formalize the single line "Without loss of generality we can assume that $A$ and $B$ are not both inside (possibly distinct) cosets of the same subgroup of ${\mathbb Z}^d$, or we just replace
with that subgroup." in the blueprint, which expanded to well over 200 lines of code. Let me know if there is anything specific you could use help on.

It did occur to me that bundling together a lot of the hypotheses into a single structure would be cleaner, visually at least; in particular having something like

structure UniformVar {G: Type u} [MeasurableSpace G]  (A: Set G) :=
  finite: Set.Finite A
  nonempty: Nonempty A
  Ω: Type u
  hΩ: MeasureSpace Ω
  hμ: IsProbabilityMeasure (ℙ:Measure Ω)
  X: Ω → G
  uniform: IsUniform A X ℙ
  measurable: Measurable X
  range: FiniteRange X

would shorten the very long statements in weakPFR (and could also retroactively be used in PFR), though given the principle of "if it ain't broke, don't fix it", perhaps this is only worth doing if the alternative is causing actual pain (e.g., in making the bump harder).

[Terence Tao]

Actually on further investigation it appears that trying to bundle classes inside a structure messes up instance inference, and so could cause more problems than it solves.

[Yaël Dillies]

It kinda is broke right now :sweat_smile: Certainly if we want to PR PFR to mathlib, we'll have to clean this up one way or another.

[Terence Tao]

well one could always jettison weakPFR from any mathlib PR to resolve this specific issue (I doubt it would see all that many usecases in Mathlib, whereas the core PFR theorem might conceivably have an application).

[Terence Tao]

Another possible refactor is to introduce a variant Ruzsa distance dᵤ[A # B], defined to equal d[UA # UB] where UA, UB are uniform random variables on A, B (chosen arbitrarily, because the choice does not matter), and set up some basic API for this distance (for instance, it is preserved by injective homomorphisms and by shifting by constants). Then one doesn't have to explicitly carry the uniform random variables and their supporting structures throughout the argument (and particularly throughout the inductive part of weakPFR). It could also simplify PFR itself a little bit (though it's much less of an issue there because one is not performing induction), and also removes a minor universe issue (I had to suddenly care about which universe everything belonged to in order to perform induction). I could try developing this approach if you think it is worthwhile, though of course I don't want to interfere with your bump.

[Rémy Degenne]

Terence Tao said:

It did occur to me that bundling together a lot of the hypotheses into a single structure would be cleaner, visually at least; in particular having something like

structure UniformVar {G: Type u} [MeasurableSpace G]  (A: Set G) :=
  finite: Set.Finite A
  nonempty: Nonempty A
  Ω: Type u
  hΩ: MeasureSpace Ω
  hμ: IsProbabilityMeasure (ℙ:Measure Ω)
  X: Ω → G
  uniform: IsUniform A X ℙ
  measurable: Measurable X
  range: FiniteRange X

would shorten the very long statements in weakPFR (and could also retroactively be used in PFR), though given the principle of "if it ain't broke, don't fix it", perhaps this is only worth doing if the alternative is causing actual pain (e.g., in making the bump harder).

A general thought I have about the code in the PFR project, which I think applies here, is that often the code is written about random variables but should be about measures. Very often we care only about the law of the variables, and because we talk about random variables we need Ω and a Measurable X assumption which we have to carry along. All the entropy and Ruzsa distance definitions are more naturally written about measures; at several steps of the blueprint there are remarks stating that random variables need not be defined on the same space and as far as I can tell it's because only their laws matter... In some places we even explicitly change the domain of the random variables even though that domain should not matter.

I was thinking about trying to refactor the code to use less random variables and see how simpler it can get, but that's a lot of refactoring and I am only midly curious.

For similar reasons, I think that a definition of a Ruzsa distance between sets equal to the distance between uniform measures is a good idea: if the choice of measure don't matter, let's not introduce the measure and work as much as possible with the sets only.

[Terence Tao]

Good point. In particular we should define the uniform probability measure Measure.uniform A of a finite non-empty subset A of an ambient (MeasurableSingletonClass) space G, and use the measure-theoretic version of Ruzsa distance to define dᵤ[A # B]. I had in mind a much more complicated definition involving exists_isUniform_measureSpace (and the axiom of choice) that would have been considerably worse to work with. (EDIT: once one had Measure.uniform, one could refactor the IsUniform API accordingly.)

The one nice thing about working with random variables instead of measures is that algebraic facts about (deterministic) variables in the range space carry over quite painlessly to the random variables. For instance, if G is an elementary abelian 2-group, we have x+y=x-y for all x y: G, and hence we pretty much automatically have X+Y=X-Y for all X Y: Ω → G as well. Admittedly it's not that much harder to show that μXY.map (fun x ↦ x.1 + x.2) = μXY.map (fun x ↦ x.1 - x.2) (where μXY is the joint distribution of X and Y, which for instance might be μX.prod μY if X, Y are independent) but it's visually and conceptually harder to follow arguments structured in that fashion.

I think I will create a separate file to try to set up uniform measures and Ruzsa distance between sets, but not touch the main project files such as weakPFR.lean for now, just to see how it would work.

[Terence Tao]

Ah, I remember now what the main advantage of the random variable formalism is: one can introduce new random variables that are independent of previous variables, but all facts already proven about the previous random variables carry over because the hypotheses (such as independence) are probabilistic hypotheses that don't require a specific sample space. If one worked only with distributions, then every time one wanted to introduce a new random variable, one would have to replace the previous joint distribution with a product of that measure with the new distribution, and make sure that all previously established facts about the prior distribution lift to the new one. For instance, if one already had some inequalities concerning independent random variables X and Y, and some inequalities concerning independent random variables Y and Z, and now wanted to combine these inequalities to form a more complex inequality relating jointly independent variables X, Y, and Z, then a number of lifting arguments would have to be made before the inequalities could be combined if one was working in a purely distribution-based formalism. In our current framework we rely in the various independent_copies lemmas to do all this lifting at the very beginning of the argument instead of in the middle. Potentially a refactor would still be cleaner though.

[Terence Tao]

OK, I now have an API for uniform probability measures, and a set-based Ruzsa distance at https://github.com/teorth/pfr/blob/master/PFR/ForMathlib/Entropy/RuzsaSetDist.lean . (Because the existing Ruzsa distance API is more developed for random variables than for measures, the proofs here largely go through the random variable formalism, but in principle it could all be refactored eventually.) I can start converting the relevant portions of weakPFR (and PFR) to this API, but I don't want to interfere with @Yaël Dillies 's bump. Yael, how would you like to proceed here?

[Terence Tao]

p.s. for some reason the blueprint did not build in the most recent commits, despite no change to the source files. https://github.com/teorth/pfr/actions/runs/7375198307/job/20066472325

[Yaël Dillies]

I spent an awful lot of time on WeakPFR but not very productively. Most of my bump is before WeakPFR, so I suggest you streamline whatever you can, and once this is in a better state I redo my bump by cherry-picking changes from the bump branch.

[Rémy Degenne]

Terence Tao said:

p.s. for some reason the blueprint did not build in the most recent commits, despite no change to the source files. https://github.com/teorth/pfr/actions/runs/7375198307/job/20066472325

I have the same new error for the CLT blueprint: https://github.com/RemyDegenne/CLT/actions/runs/7376451454/job/20069248540
I don't know how to fix it yet.

[Terence Tao]

OK, Weak PFR is now refactored using distance between sets. I guess for sake of consistency I'll do PFR next.

[Terence Tao]

Oh, wait, PFR actually uses the random variable formalism much more deeply than weak PFR. It ain't broke, so I think I'll just leave it as is.

[Yaël Dillies]

The cache for mathlib is currently broken, so I will restrain from bumping until it is fixed.

[Mario Carneiro]

you can probably bump to v2024

[Yaël Dillies]

Yes but I wanted to bump to https://github.com/leanprover-community/mathlib4/commit/0d6117a47dd8f9fe074025146a29b195bf0230f1 :sad:

[Yaël Dillies]

@Bhavik Mehta is now done with BSG! However his proof uses APAP, my discrete Fourier analysis library.

[Yaël Dillies]

This means we need to make PFR depend on APAP. Since APAP uses a more recent mathlib than PFR, we must complete pfr#171 before I can add APAP as a dependency and complete all the tasks currently the blueprint.

[Yaël Dillies]

I must focus on my studies for the coming two months. I am therefore asking you whether you would have time to take over pfr#171. It shouldn't be terribly hard.

[Mauricio Collares]

I did start updating it, but there was some breakage with Nonempty/Set.Nonempty I couldn't fix in WeakPFR.lean

[Yaël Dillies]

Sorry, do you mean you started bumping mathlib again (as in not on branch bump from pfr#171)?

[Mauricio Collares]

No, on top of pfr#171

[Yaël Dillies]

Don't worry too much about bumping to the latest mathlib. I will be able to do that quickly once pfr#171 is in.

[Mauricio Collares]

PRd the version with Nonempty issues as https://github.com/teorth/pfr/pull/183

[Yaël Dillies]

(The linkifier currently doesn't work. I've been fixing my links manually)

[Mauricio Collares]

The errors in ApproxHomPFR.lean are new and I think I can fix them. The Nonempty ones in WeakPFR.lean look trickier.

[Yaël Dillies]

In WeakPFR, it's a matter of replacing hs : Nonempty s by hs : s.Nonempty and add have := hs.to_subtype wherever needed.

[Mauricio Collares]

I probably made more of a mess than needed, but it builds now

[Sébastien Gouëzel]

@Yaël Dillies , is https://github.com/teorth/pfr/pull/171 good to go, or should we bump it to another version of mathlib to make sure it becomes compatible with APAP?

[Yaël Dillies]

Send it as soon as it passes CI!

[Sébastien Gouëzel]

It does already pass CI, doesn't it?

[Yaël Dillies]

Ah I didn't notice! Merged

[Yaël Dillies]

I am now waiting for @Bhavik Mehta to put the BSG code in LeanAPAP. Then I will add LeanAPAP as a dependency to PFR and the graph will be fully green!

[Terence Tao]

Is anyone else getting build errors post-bump, starting with PFR.Mathlib.Probability.Kernel.MeasureCompProd.lean (where it complains that prod_apply is not a function?, and also giving several errors such as "'ProbabilityTheory.kernel.prod_const' has already been declared"). Possibly I have the wrong cache or something, since the CI seems to be working fine.

[Rémy Degenne]

kernel.prod_const was added to Mathlib yesterday, along most of the content of the file MeasureCompProd. If the Mathlib version you have is younger than that, those errors are expected and most of MeasureCompProd should simply be deleted.
I can help clean up. Does the problem happen on master?

[Rémy Degenne]

I am bumping mathlib now. PR coming soon.

[Rémy Degenne]

https://github.com/teorth/pfr/pull/184

[Mauricio Collares]

@Rémy Degenne Can you use scripts/update_mathlib.sh to update the lake manifest? This ensures doc-gen dependencies are added to the manifest properly (otherwise master CI will break once the PR is merged).

[Mauricio Collares]

Or just run lake -R -Kenv=dev update, that should be enough too

[Rémy Degenne]

I used the lake command you wrote and pushed to the PR branch. Is it good now?

[Mauricio Collares]

I think so. Thank you!

[Terence Tao]

Somehow I still haven't mastered the workflow of updating the cache and Lean is currently rebuilding Mathlib from scratch, but hopefully everything is fixed now, will let you know in an hour or two once mathlib builds. (For some reason, once I start accidentally initiate the mathlib build process, VSCode is determined to see it to the end, no matter how many times I restart, fetch the cache, etc., afterwards.)

[Sébastien Gouëzel]

Normally, quitting VSCode and then doing

lake clean
lake exe cache get!

should get you a working mathlib. Deleting the .lake directory may also help.

[Sébastien Gouëzel]

But of course, it's computer science, so utterly unpredictable :-)

[Terence Tao]

Sébastien Gouëzel said:

lake clean

error: permission denied (error code: 13)
file: .\.lake\build\lib

[Sébastien Gouëzel]

Wow, pretty unusual. I would just wipe out .lake completely.

[Terence Tao]

Oh wait, one has to do this in the mathlib directory rather than the root directory?

[Sébastien Gouëzel]

In the root directory.

[Terence Tao]

lake clean works in the mathlib directory.

[Sébastien Gouëzel]

You should never try to touch the mathlib directory: since you're not working on mathlib, it's just a version that has been downloaded for you by lake, and it's just lake's business.

[Sébastien Gouëzel]

I just tried it on my computer: I have checked out latest PFR master, and then

PS C:\Users\sgouezel_A\Desktop\pfr> lake clean
info: mathlib: updating repository '.\.lake/packages\mathlib' to revision 'b075cdd0e6ad8b5a3295e7484b2ae59e9b2ec2a7'
info: std: updating repository '.\.lake/packages\std' to revision '1d85fd7db28700b28043d6370dd1ebc426de4d5d'
info: Qq: updating repository '.\.lake/packages\Qq' to revision '1c88406514a636d241903e2e288d21dc6d861e01'
info: aesop: updating repository '.\.lake/packages\aesop' to revision '2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70'
info: proofwidgets: updating repository '.\.lake/packages\proofwidgets' to revision '8dd18350791c85c0fc9adbd6254c94a81d260d35'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '.\.lake/packages\importGraph'
PS C:\Users\sgouezel_A\Desktop\pfr> lake exe cache get
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
Attempting to download 4133 file(s)
Downloaded: 4133 file(s) [attempted 4133/4133 = 100%] (100% success)
Decompressing 4133 file(s)
unpacked in 7080 ms
PS C:\Users\sgouezel_A\Desktop\pfr> lake build
[426/847] Building PFR.ForMathlib.Pair
[844/847] Building PFR.Mathlib.GroupTheory.Subgroup.Pointwise
[1140/1236] Building PFR.Tactic.Finiteness.Attr
[1219/1276] Building PFR.Mathlib.Algebra.GroupWithZero.Units.Lemmas
[1250/1276] Building PFR.Mathlib.MeasureTheory.Measure.NullMeasurable
[1349/1657] Building PFR.Mathlib.Data.Fintype.Card
[1422/1704] Building PFR.Mathlib.MeasureTheory.Integral.Lebesgue
[1466/1864] Building PFR.Mathlib.Data.Set.Image
[1467/1864] Building PFR.Mathlib.Data.Fin.Basic
[1468/1864] Building PFR.Mathlib.Data.Fintype.Lattice
[1469/1864] Building PFR.Mathlib.Data.Finset.Sigma
...

only builds PFR files.

[Rémy Degenne]

the "permission denied" error sometimes happen to me when VSCode is open and I try to use lake. It happened earlier today when I was trying to bump mathlib. It goes away when I close VSCode.

[Sébastien Gouëzel]

Yes, all these commands should be used when VSCode is closed and no compilation is going on.

[Terence Tao]

OK, that works, thanks. Saving these instructions the next time I need to rebuild from scratch.

[Yaël Dillies]

The bump to 4.6.0-rc1 has caused rpow_simp to break. I just spent an hour wading through the changelogs but I didn't figure out how to fix it :sad: @Scott Morrison, do you have advice here?

[Yaël Dillies]

See PFR/Tactic/RpowSimp in https://github.com/teorth/pfr/commit/5e621b7cb6ad405f52d334cd87591eb076b982ec

[Mario Carneiro]

broke how?

[Mario Carneiro]

the build itself broke for a silly reason (missing include)

[Yaël Dillies]

The simp internals changed with the introduction of simprocs (at least that's what I gathered)

[Mario Carneiro]

okay, again broke how?

[Mario Carneiro]

what line is failing with what error

[Yaël Dillies]

def rewrite (parent : Expr) (root := true) : M Simp.Result := fun nctx rctx s ↦
  let pre e :=
    try
      guard <| root || parent != e -- recursion guard
      let e ← withReducible <| whnf e
      guard e.isApp -- all interesting ring expressions are applications
      guard <| ← isDefEq (← inferType e) q(ℝ)
      let ⟨a, _, pa⟩ ← eval e rctx s
      let r ← nctx.simp { expr := a, proof? := pa }
      if ← withReducible <| isDefEq r.expr e then return .done { expr := r.expr }
      pure (.done r)
    catch _ =>
      pure <| Simp.Step.visit { expr := e }
  let post := (Simp.postDefault · fun _ ↦ none)
  (·.1) <$> Simp.main parent nctx.ctx (methods := { pre, post })

is failing with

RPowSimp.lean:197:14
type mismatch
  nctx.simp { expr := a, proof? := some pa, dischargeDepth := 0, cache := true }
has type
  SimpM Simp.Result : Type
but is expected to have type
  MetaM ?m.34878 : Type
RPowSimp.lean:198:36
invalid field notation, type is not of the form (C ...) where C is a constant
  r
has type
  ?m.34867
RPowSimp.lean:198:57
invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  ?m.35661
RPowSimp.lean:199:12
invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  ?m.35773
RPowSimp.lean:202:34
application type mismatch
  Simp.postDefault x✝ fun x ↦ none
argument
  fun x ↦ none
has type
  (x : ?m.30870) → Option (?m.30874 x) : Sort (max ?u.30869 (?u.30872 + 1))
but is expected to have type
  Expr : Type
RPowSimp.lean:203:50
overloaded, errors
  failed to synthesize instance
    Singleton (Simp.SimprocsArray → SimpM Simp.Step) Simp.Methods

  203:57 type mismatch
    post
  has type
    Simp.SimprocsArray → SimpM Simp.Step : Type
  but is expected to have type
    Simp.Simproc : Type

[Mario Carneiro]

RpowSimp is a copy paste job of RingNF. The corresponding code in RingNF has changed like so:

   fun nctx rctx s ↦ do
-    let pre e :=
+    let pre : Simp.Simproc := fun e =>
       try
         guard <| root || parent != e -- recursion guard
         let e ← withReducible <| whnf e
         guard e.isApp -- all interesting ring expressions are applications
         let ⟨u, α, e⟩ ← inferTypeQ' e
         let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type u))
         let c ← mkCache sα
         let ⟨a, _, pa⟩ ← match ← isAtomOrDerivable sα c e rctx s with
         | none => eval sα c e rctx s -- `none` indicates that `eval` will find something algebraic.
         | some none => failure -- No point rewriting atoms
         | some (some r) => pure r -- Nothing algebraic for `eval` to use, but `norm_num` simplifies.
         let r ← nctx.simp { expr := a, proof? := pa }
         if ← withReducible <| isDefEq r.expr e then return .done { expr := r.expr }
         pure (.done r)
-      catch _ => pure <| .visit { expr := e }
-    let post := (Simp.postDefault · fun _ ↦ none)
+      catch _ => pure <| .continue
+    let post := Simp.postDefault #[]
     (·.1) <$> Simp.main parent nctx.ctx (methods := { pre, post })

[Patrick Massot]

We really need to get rpow_simp to Mathlib. Users of PFR should not have to handle this.

[llllvvuu]

So I've almost fixed the build (@Mario Carneiro 's diff above worked) on my branch:

https://github.com/teorth/pfr/pull/185

I'm getting a weird unrelated error in the fixed ApproxHomPFR.lean . I get spammed with "don't know how to synthesize placeholder" on every line (there are no placeholders), but if I put a sorry at the end of the proof, it says "no goals to be solved", indicating that the proof is done (and I can step through and get the goal states fine)

[Kim Morrison]

CI is saying ./.lake/packages/LeanAPAP/././LeanAPAP/Mathlib/Tactic/Positivity.lean:18:6: warning: declaration uses 'sorry', so I'd look there first!

[llllvvuu]

(deleted)

[llllvvuu]

ah never mind, it was my mistake: it turns out the error message was correct and I'd made a typo which I didn't realize because the error message showed up on every line. Fixed now

[llllvvuu]

Also thank you @Yaël Dillies for the last green bubble!

Screenshot-2024-02-09-at-11.25.30PM.png

[Yaël Dillies]

Nice! I wasn't sure whether it would be sorry-free since I've sorried many stupid things in LeanAPAP (things that are easier to fix in mathlib than to work around, like NNRat.cast)

[Yaël Dillies]

Scott Morrison said:

CI is saying ./.lake/packages/LeanAPAP/././LeanAPAP/Mathlib/Tactic/Positivity.lean:18:6: warning: declaration uses 'sorry', so I'd look there first!

This is a remnant of the switch to Lean 4. There are still a few positivity extensions that haven't been fixed.

[Terence Tao]

llllvvuu said:

Also thank you Yaël Dillies for the last green bubble!

Screenshot-2024-02-09-at-11.25.30PM.png

Thanks for getting things over the finish line! Very happy to see this project reach a satisfactory conclusion. (I guess there could still be some Mathlib migration to do, though...)

[Yaël Dillies]

... yes. https://teorth.github.io/pfr/ still lists a lot of files that would be easy to PR to mathlib. However, the meat of the project is still stuck on entropy, which itself is stuck on Rémy being very busy right now.

[Yaël Dillies]

I am personally only mildly busy with Part III at the moment, so it's very possible I'll PR some of the aforementioned files. That will wait a bit though, because I've just started the fierce battle against the import hierarchy to define NNRat.cast (see #10392), which I need for LeanAPAP.

[Rémy Degenne]

There is an issue for the transfer of most probability results to Mathlib: many things use a disintegration property of Markov kernels, which in the project has been proved only for countable spaces (pfr#ProbabilityTheory.kernel.condKernel).
In Mathlib I think we should add that property in the more general case that either the domain is countable or the first space of the codomain is standard Borel. That's why I paused transferring to Mathlib: I want to do that properly first. I have around 1500 lines of code towards that result, which is 95% done. However as Yaël wrote I have little time to finish it right now.

[Rémy Degenne]

The result is #10603 . This is an enormous PR (+4,558 −1,631): I am cutting it into more reviewable pieces.

[Yaël Dillies]

Excited!!

[Yaël Dillies]

Btw I didn't mention it here, but I bumped Mathlib again this week. There was quite a lot of breakage due to syntax changes. But the next bump should be easy

[Rémy Degenne]

condKernel is now in Mathlib! Thanks @Sébastien Gouëzel for the reviews!
Sometime in the next two weeks I'll bump Mathlib and modify the PFR code to use the new condKernel. Then I'll resume the transfer of PFR results to Mathlib.

[Rémy Degenne]

I bumped Mathlib and opened a PR: https://github.com/teorth/pfr/pull/188
That was not fun. Many things broke, mainly due to a change in simp. And since we never enforced code quality requirements like replacing non-terminal simp by simp only, a few proofs were tricky to fix.

There are 3 sorry left and any help is welcome.

[Sébastien Gouëzel]

I'm looking at the sorrys.

[Sébastien Gouëzel]

Sorrys fixed at https://github.com/RemyDegenne/pfr/pull/1 (I don't have writing rights either on PFR or your fork, so I have PRed to your fork and you will need to merge it before this shows up in the PR on the main repo, if I understand correctly).

[Rémy Degenne]

Thanks! I merged the changes and the bump PR is ready.

[Yaël Dillies]

Thanks! Merged

[Yaël Dillies]

You beat me to it by a few hours because, as you must have noticed, I just bumped LeanAPAP and was about to bump PFR as well

[Rémy Degenne]

I noticed nothing :)
Well I saw that LeanAPAP was updated at some point because a file did not exist anymore, but I had no idea of the date at which that happened.

[Yaël Dillies]

Ah the file disappearing was a few days ago

[Pietro Monticone]

Our recent Mathlib PR #12918, which adds the lemma IdentDistrib.inv, has been merged (thanks @Jason KY. and @Rémy Degenne ).

Would it be advisable to bump Mathlib so that we can remove this lemma from the PFR/MoreRuzsaDist.lean file in our draft?

[Yaël Dillies]

It's definitely possible, but note that we first need to bump APAP

[Yaël Dillies]

Bumped, but note that there is no IdentDistrib.inv in PFR. Did you confuse with iIndepFun.inv?

[Yaël Dillies]

Oh I see, it's in your draft PR

[Yaël Dillies]

Also I will note that ./scripts/mk_all.sh wasn't run since PFR.MultiTauFunctional was added, meaning that the build succeeded even though the file was completely broken.

[Yaël Dillies]

I commented out chunks of it to get the build succeeded and since it seems to so far be mostly a copy-paste of the binary tau functional

[Terence Tao]

Yaël Dillies said:

I commented out chunks of it to get the build succeeded and since it seems to so far be mostly a copy-paste of the binary tau functional

Thanks. I will try to fix up that file later - we're a long way from getting to that part of the formalization currently - but for now definitely just comment out anything problematic. (I had wondered why there weren't any errors reported regarding that file, I had thought I had just been extremely lucky getting the syntax right the first time around.)

[Terence Tao]

There seems to be some minor simp issue in PFR.Mathlib.Probability.Independence.Basic that came up during the bump. https://github.com/teorth/pfr/actions/runs/9105173824/job/25030314036

[Johan Commelin]

@Terence Tao I think there is a simp? [lem1, lem2] says ... line which needs to be updated.
This says tactic combinator is an attempt at caching a fast version of a slower tactic. Locally only the fast simp only runs, but in CI we check that the output of the slow tactic matches the fast version. We keep the slow simp? in the code to communicate intent and (hopefully) increase readability.

[Rémy Degenne]

The drawback of simp? says ... is that it is very brittle: they frequently break after mathlib updates because simp uses a slightly different set of lemmas and the ... part changes.

[Yaël Dillies]

Yes, I will remove all the says in PFR later today, unless Terry beats me to it

[Johan Commelin]

Yep, I think says is an interesting experiment, but not a resounding success.

[Johan Commelin]

It would be good if we could come up with a better version of the says idea.

[Pietro Monticone]

Opened PFR#197 to remove the single says we've found in the whole repo.

[Terence Tao]

I'm no longer able to rebuild Mathlib. The build reports issues in some seemingly random files:

1929/1929] Building PFR.ForMathlib.Entropy.RuzsaDist
Some build steps logged failures:
- Building Mathlib.Algebra.Group.Opposite
- Building Mathlib.Order.BooleanAlgebra
- Building Mathlib.Algebra.Order.Monoid.Canonical.Defs
- Building Mathlib.Algebra.Ring.Commute
- Building Mathlib.Data.Int.Units
- Building Mathlib.Algebra.Regular.Basic
error: build failed

For instance,

[435/1929] Building Mathlib.Algebra.Group.Opposite
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake/packages\LeanAPAP\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false .\.\.lake/packages\mathlib\.\.\Mathlib\Algebra\Group\Opposite.lean -R .\.\.lake/packages\mathlib\.\. -o .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Algebra\Group\Opposite.olean -i .\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Algebra\Group\Opposite.ilean -c .\.\.lake/packages\mathlib\.lake\build\ir\Mathlib\Algebra\Group\Opposite.c --json
info: stderr:
failed to write '.\.\.lake/packages\mathlib\.lake\build\lib\Mathlib\Algebra\Group\Opposite.olean': 13 Permission denied
error: Lean exited with code 1

Trying to fetch the Mathlib build cache creates similar errors, though now reported in different files:

Some build steps logged failures:
- Compiling Cache.Main
- Compiling Cache.IO
- Compiling Cache.Hashing
- Compiling Cache.Requests
error: build failed
=> Operation failed. Exit code: 1.

I have no idea what is going on here...

[Yaël Dillies]

What if you nuke .lake and try lake exe cache get again?

[Terence Tao]

Same error:

info: LeanAPAP: cloning https://github.com/YaelDillies/LeanAPAP.git to '.\.\.lake/packages\LeanAPAP'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.\.lake/packages\mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '.\.\.lake/packages\Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '.\.\.lake/packages\aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.\.lake/packages\proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '.\.\.lake/packages\Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '.\.\.lake/packages\importGraph'
[6/10] Compiling Cache.Main
trace: .> c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe' exited with code 1
[7/10] Compiling Cache.IO
trace: .> c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe' exited with code 1
[8/10] Compiling Cache.Hashing
trace: .> c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe' exited with code 1
[9/10] Compiling Cache.Requests
trace: .> c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.8.0-rc1\bin\leanc.exe' exited with code 1
Some build steps logged failures:
- Compiling Cache.Main
- Compiling Cache.IO
- Compiling Cache.Hashing
- Compiling Cache.Requests
error: build failed

[Yaël Dillies]

I can't reproduce. I suspect your local state is messed up. Can you do at least one of the following?

1. elan toolchain uninstall leanprover/lean4:v4.8.0-rc1, elan toolchain install leanprover/lean4:v4.8.0-rc1, lake exe cache get!. Keep on going even if the first command fails.
2. Go to https://www.gitpod.io/#https://github.com/teorth/pfr and try again in the gitpod container.

[Pietro Monticone]

We have just:

1. deleted the local repository
2. cloned the repo again
3. lake exe cache get!
4. lake build

and we didn't encounter any error / build failure.

[Yaël Dillies]

That doesn't do anything about the toolchain, which I suspect is what's going wrong for Terry. Kim Morrison accidentally misrolled 4.8.0-rc1, so now everyone is having slight issues with that specific toolchain. Hopefully we'll all be on rc2 in a matter of days.

[Terence Tao]

Yaël Dillies said:

1. elan toolchain uninstall leanprover/lean4:v4.8.0-rc1, elan toolchain install leanprover/lean4:v4.8.0-rc1, lake exe cache get!. Keep on going even if the first command fails.

This worked, thanks!

[Pietro Monticone]

Our recent Mathlib PR #13125, which adds the lemma indepFun_of_identDistrib_pair (solving this topic), has been merged.

Once we bump Mathlib we will have to remove this lemma from the PFR/MoreRuzsaDist.lean file (see related code).

[Yaël Dillies]

FYI I will do that bump (for both APAP and PFR) when Mathlib goes to 4.9.0-rc1... which should be in a week roughly?

[Yaël Dillies]

I bumped APAP early to get rid of dissociation (#10555). However we can't bump PFR just yet because @Yury G. Kudryashov generalised docs#MeasureTheory.ae in a way that breaks its use with a FiniteMeasure.

[Yaël Dillies]

Discussion about the ae issue: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ae.20of.20a.20finite.20measure

[Yaël Dillies]

One cheap solution if we really want to get the bump through is to create a new notation f =ᵐᶠ[μ] g defined as f =ᵐ[(μ : Measure Ω)] g. But that's a hack and I would rather solve the root issue.

[Yaël Dillies]

@Sébastien Gouëzel's recent upstreaming of Measure.real (:tada:) is leaving us with a lot of work on the bump. I have spent a lot of time today on it, and now I can't dedicate any more time to it. If someone is willing to fix the remaining errors, I have opened teorth/pfr#239.

[Michael Rothgang]

Aside: the linkifier for PFR points to github.com/leanprover-community/PFR, but should point to teorth/PFR. CC @Bryan Gin-ge Chen as I know you have updated this in the past

[Bryan Gin-ge Chen]

It seems we have a lower-case pfr linkifier which points to the pfr docs: pfr#PFR_conjecture. If necessary, I can add the upper-case version to point to the github repo, but it seems confusing so I'd prefer if there was some confirmation that this is desired first.

[Terence Tao]

Is there some web page or source code that has an updated list of all the linkifiers? That may be the most stable long-term solution. This particular project is now very low activity and probably won't make much use of these tools going forward.

[Mario Carneiro]

https://leanprover.zulipchat.com/#organization/linkifier-settings

[Sébastien Gouëzel]

@Yaël Dillies , some little progress in https://github.com/teorth/pfr/pull/240

[Kevin Buzzard]

Mario Carneiro said:

https://leanprover.zulipchat.com/#organization/linkifier-settings

Wooa we have O(100) of them!

[Michael Rothgang]

TIL there was a stale linkifier: bikeshedding thoughts welcome!

[Bryan Gin-ge Chen]

I didn't realize everyone could see that page! (Maybe we should make #linkifiers?)