Slow Chinese remainder theorem

Stream: mathlib4

[Patrick Massot]

I'm preparing some teaching/demo and decided to do something other than real analysis (next week I need to introduce a bunch of young algebraic geometer to Lean). After a lot of thinking about what would be a simple algebra theorem that everybody likes, I settled on the Chinese remainder theorem. So my target was to prepare a Lean file with a proof outline and sorries. I went to mathlib4 and was shocked to see the length of https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/RingTheory/Ideal/Quotient.lean#L375-L440. The docstring says /-- Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/ so I thought: "let's see if Bourbaki can cut this in half". And indeed they can. But elaboration is slow. Does anyone understand why coprime_infᵢ_of_coprime is so slow in the code below:

import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Ideal.Operations

namespace PiNotation
open Lean.Parser Term
open Lean.PrettyPrinter.Delaborator

@[scoped term_parser]
def piNotation := leading_parser:leadPrec
  unicodeSymbol "Π" "Pi" >>
  many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >>
  optType >> ", " >> termParser

@[scoped macro PiNotation.piNotation] def replacePiNotation : Lean.Macro
  | .node info _ args => return .node info ``Lean.Parser.Term.forall args
  | _ => Lean.Macro.throwUnsupported

@[scoped delab forallE]
def delabPi : Delab := do
  let stx ← delabForall
  let stx : Term ←
    match stx with
    | `($group:bracketedBinder → $body) => `(Π $group:bracketedBinder, $body)
    | _ => pure stx
  match stx with
  | `(Π $group, Π $groups*, $body) => `(Π $group $groups*, $body)
  | _ => pure stx

end PiNotation


open PiNotation BigOperators

lemma Finset.sum_univ_eq_single {β : Type u} {α : Type v} [Fintype α] [AddCommMonoid β] {f : α → β} (a : α)
    (h : ∀ b,  b ≠ a → f b = 0) : ∑ x, f x = f a := by
  rw [Finset.sum_eq_single]
  · tauto
  · exact λ ha ↦ (ha <| Finset.mem_univ a).elim

section chinese
namespace Ideal
variable [CommRing R] {ι : Type _}

lemma Ideal.add_eq_one_iff {I J : Ideal R} : I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1 := by
  rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]

def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) (by
    intro r hr
    rw [Submodule.mem_infᵢ] at hr
    ext i
    exact Quotient.eq_zero_iff_mem.2 (hr i))

lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
  chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Quotient.mk (I i) x :=
rfl

lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
  chineseMap I (Quotient.mk _ x) i = Quotient.mk (I i) x :=
rfl

lemma chineseMap_injective (I : ι → Ideal R) : Function.Injective (chineseMap I) := by
  rintro ⟨x⟩ ⟨y⟩ hxy
  apply  Quotient.eq.2
  apply  (Submodule.mem_infᵢ _).2
  intro i
  apply Quotient.eq.1
  change chineseMap I (Quot.mk _ x) i = chineseMap I (Quot.mk _ y) i
  rw [hxy]

lemma coprime_infᵢ_of_coprime {I : Ideal R} {J : ι → Ideal R} {s : Finset ι} (hf : ∀ j ∈ s, I + J j = 1) : I + (⨅ j ∈ s, J j) = 1 := by
  classical
  revert hf
  let P : Finset ι → Prop := λ s ↦ (∀ (j : ι), j ∈ s → I + J j = 1) → (I + ⨅ j ∈ s, J j) = 1
  apply @Finset.induction_on _ P _ s
  · intro _
    simp only [Finset.not_mem_empty, not_false_eq_true, infᵢ_neg, infᵢ_top, Submodule.add_eq_sup, ge_iff_le,
               top_le_iff, le_top, sup_of_le_right, one_eq_top]
  · intros i s _hi hs h
    rw [Finset.infᵢ_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := (⨅ j ∈ s, J j)
    have : I + K = 1 := hs fun j hj ↦ h j (Finset.mem_insert_of_mem hj)
    calc
      1 = I + K := this.symm
      _ = I + K*(I + J i) := by rw [h i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i := by ring
      _ ≤ I + K ⊓ J i := add_le_add mul_le_left mul_le_inf

lemma chineseMap_surjective_aux [Fintype ι] {I : ι → Ideal R} (hI : ∀ i j, i ≠ j → I i + I j = 1) (i : ι) :
    ∃ e : R, Quotient.mk (I i) e = 1 ∧ ∀ j, j ≠ i → Quotient.mk (I j) e = 0 := by
  classical
  have key : ∀ j ∈ Finset.erase Finset.univ i, I i + I j = 1 := by
    intros j hj
    apply hI
    simpa [ne_comm] using hj
  rcases Ideal.add_eq_one_iff.mp (coprime_infᵢ_of_coprime key) with ⟨u, hu, e, he, hue⟩
  refine ⟨e, ?_, ?_⟩
  · simp [eq_sub_of_add_eq' hue, map_sub, Ideal.Quotient.eq_zero_iff_mem.mpr hu]
    rfl
  · intros j hj
    apply Ideal.Quotient.eq_zero_iff_mem.mpr
    simp at he
    tauto

lemma chineseMap_surjective [Fintype ι] {I : ι → Ideal R} (hI : ∀ i j, i ≠ j → I i + I j = 1) :
    Function.Surjective (chineseMap I) := by
  intro g
  let f := fun i ↦ Quotient.out' (g i)
  choose e he using chineseMap_surjective_aux hI
  use Quotient.mk _ (∑ i, f i*e i)
  ext i
  rw [chineseMap_mk', map_sum, Finset.sum_univ_eq_single i]
  · simp [(he i).1]
    exact Quotient.out_eq' _
  · intros j hj
    simp [(he j).2 i hj.symm]

noncomputable def chineseIso [Fintype ι] (I : ι → Ideal R) (hI : ∀ i j, i ≠ j → I i + I j = 1) :
   (R ⧸ ⨅ i, I i) ≃+* Π i, R ⧸ I i :=
{ Equiv.ofBijective _ ⟨chineseMap_injective I, chineseMap_surjective hI⟩, chineseMap I with }


end Ideal
end chinese

[Patrick Massot]

Note the beginning of the file is Kyle's Pi notation from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Add.20pi.20notation.20back.20.3F/near/355787931

[Patrick Massot]

Note also the line simp only [Finset.not_mem_empty, not_false_eq_true, infᵢ_neg, infᵢ_top, Submodule.add_eq_sup, ge_iff_le, top_le_iff, le_top, sup_of_le_right, one_eq_top] is me desperately trying to make things faster. This should be simp

[Patrick Massot]

On the math side, to be totally fair, this isn't exactly how this proof is written in Bourbaki. Bourbaki is a bit shy when it comes to using the SemiRing structure on Ideal R and they use elements of R instead of the neat

    calc
      1 = I + K := this.symm
      _ = I + K*(I + J i) := by rw [h i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i := by ring
      _ ≤ I + K ⊓ J i := add_le_add mul_le_left mul_le_inf

[Patrick Massot]

But of course they don't assume any commutativity, I did it only because we don't have a nice theory of ring quotients in the non-commutative case.

[Kevin Buzzard]

It's just the usual problem:

        [] [3.441595s] ✅ instHAdd =?= instHAdd ▼
          [] [0.000000s] ✅ Ideal R =?= Ideal R
          [] [3.441552s] ✅ Distrib.toAdd =?= AddZeroClass.toAdd ▼
            [] [3.441306s] ✅ NonUnitalNonAssocSemiring.toDistrib.2 =?= AddMonoid.toAddZeroClass.2 ▼
              [] [3.441276s] ✅ AddSemigroup.toAdd =?= AddSemigroup.toAdd ▼
                [] [0.000000s] ✅ Ideal R =?= Ideal R
                [] [0.000001s] ✅ OrderedAddCommMonoid (Ideal R) =?= OrderedAddCommMonoid (Ideal R)
                [] [3.441196s] ✅ AddMonoid.toAddSemigroup =?= AddMonoid.toAddSemigroup ▼
                  [] [3.441171s] ✅ AddCommMonoid.toAddMonoid.1 =?= AddCommMonoid.toAddMonoid.1 ▼
                    [] [3.440987s] ✅ AddMonoid.toAddSemigroup =?= AddSemigroup.mk (_ : ∀ (a b c : Submodule R R), a + b + c = a + (b + c)) ▼
                      [] [3.440971s] ✅ AddCommMonoid.toAddMonoid.1 =?= AddSemigroup.mk (_ : ∀ (a b c : Submodule R R), a + b + c = a + (b + c)) ▼
                        [] [3.440939s] ✅ AddSemigroup.mk
                              (_ :
                                ∀ (x x_1 x_2 : Submodule R R),
                                  x ⊔ x_1 ⊔ x_2 =
                                    x ⊔
                                      (x_1 ⊔
                                        x_2)) =?= AddSemigroup.mk
                              (_ : ∀ (a b c : Submodule R R), a + b + c = a + (b + c)) ▼
                          [] [2.729004s] ✅ Submodule.pointwiseAddCommMonoid.proof_1 =?= Submodule.instCanonicallyOrderedAddMonoidSubmodule.proof_1 ▼
                            [] [2.728993s] ✅ ∀ (x x_1 x_2 : Submodule R R),
                                  x ⊔ x_1 ⊔ x_2 = x ⊔ (x_1 ⊔ x_2) =?= ∀ (a b c : Submodule R R), a + b + c = a + (b + c) ▶

etc etc, the typeclass inference system is checking that zillions of proofs are defeq to other proofs of the same theorem.

[Kevin Buzzard]

Here's the profiler output:

typeclass inference of HAdd took 327ms
typeclass inference of HAdd took 322ms
typeclass inference of OfNat took 313ms
typeclass inference of HAdd took 334ms
typeclass inference of HAdd took 267ms
typeclass inference of HAdd took 265ms
typeclass inference of OfNat took 256ms
typeclass inference of HAdd took 229ms
typeclass inference of OrderTop took 371ms
typeclass inference of OrderTop took 127ms
simp took 3.1s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 386ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 167ms
typeclass inference of HAdd took 257ms
typeclass inference of HAdd took 258ms
typeclass inference of OfNat took 232ms
typeclass inference of HAdd took 251ms
typeclass inference of HAdd took 252ms
typeclass inference of HAdd took 247ms
typeclass inference of HAdd took 227ms
typeclass inference of HAdd took 227ms
typeclass inference of HAdd took 250ms
typeclass inference of Add took 248ms
typeclass inference of CovariantClass took 8.38s
typeclass inference of CovariantClass took 5.2s
typeclass inference of MulOneClass took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 178ms
typeclass inference of CharZero took 1.02s
typeclass inference of AddMonoidWithOne took 140ms
ring took 257ms
tactic execution of calcTactic took 1.45s

I think CovariantClass is Gabriel's least favourite typeclass.

[Kevin Buzzard]

Switching eta experiment on creates a huge new problem:

typeclass inference of CharZero took 12s
typeclass inference of CharZero took 11.5s
typeclass inference of CharZero took 11.3s
typeclass inference of CharZero took 11.5s
typeclass inference of CharZero took 11.5s
typeclass inference of CharZero took 11.6s
typeclass inference of CharZero took 13.8s
typeclass inference of CharZero took 12.8s
typeclass inference of CharZero took 13.2s

which is interesting

[Kevin Buzzard]

On the reenableeta branch the simp only call breaks but if you just change it back to simp then the entire file compiles very quickly, all issues are gone.

[Patrick Massot]

Thanks a lot for investigating this Kevin!

[Patrick Massot]

Is the reenableeta usable for all purposes?

[Mauricio Collares]

There's a rebased reenableeta-230503 branch (!4#3780) too

[Patrick Massot]

Does anyone has instruction on how to use that reenableeta in a project? Say I want to run a Lean tutorial nextweek using a project depending on !4#3780. What is the procedure? What should I write in the lakefile.lean and lean-toolchain of my project?

[Matthew Ballard]

gebner/lean4:reenableeta-230411 is the toolchain I think

[Matthew Ballard]

But you might have to spend a little time rectifying the desired files in mathlib with it

[Patrick Massot]

My understanding is that the PR I linked does the rectifying for me

[Matthew Ballard]

Indeed!

[Matthew Ballard]

Ok. I am way behind the times. semorrison/lean4:reenableeta230503 for the toolchain and

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "45c211377067ed816d18ce60a1c06688dbfb1e4e"

seem to be working for me

[Matthew Ballard]

I have to build everything though

[Patrick Massot]

Thank you very much for investigating this. I'll try here.

[Patrick Massot]

I give up, I can't get anything to build with this branch.

[Kevin Buzzard]

I just merged that branch with SG_test3 (to do some unrelated experiment) and the resulting thing compiled fine for me.

[Patrick Massot]

For instance I get an error at the very end of Data.Quot

[Patrick Massot]

I'll try to build mathlib directly rather than as a dependency of my project

[Kevin Buzzard]

Oh! I was using mathlib4's origin/reenableeta-230503

[Patrick Massot]

I can't say I master the mysteries of updating the dependencies of a project using lake.

[Kevin Buzzard]

Yeah I wasn't doing that at all, I was entirely within mathlib just switching between different branches, merging and compiling manually.

[Patrick Massot]

Ok, I can see lake didn't even manage to git pull mathlib correctly.

[Matthew Ballard]

import Lake
open Lake DSL

package «test» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "45c211377067ed816d18ce60a1c06688dbfb1e4e"

@[default_target]
lean_lib «Test» {
  -- add any library configuration options here
}

is the full contents of my lakefile.lean

[Patrick Massot]

That require line is not enough for lake to use the correct commit from mathlib

[Matthew Ballard]

I seem to be building something with the semorrison/lean4:reenableeta230503 toolchain

[Patrick Massot]

I'll try a different random combination of lake update, lake exe cache get and lake build. I miss leanproject up so much...

[Patrick Massot]

It works!

[Matthew Ballard]

I ran

• lake update
• lake exe cache get! (failed silently)
• lake build (multiple times for some reason)

[Patrick Massot]

Thanks everybody. I'll try to use that. Next step will be to to bring in the linarith PRs in this branch

[Kevin Buzzard]

I like the fact that lake is much quicker to type than leanproject though :-)

[Scott Morrison]

I delegated the cancel_denoms PR, hopefully that helps.

[Scott Morrison]

I need to lint !4#3780, but may not have an opportunity for 48 hours.

[Scott Morrison]

I think it lints now, and has been bumped again to master.