Zulip Chat Archive

In terms of splitting or porting? For splitting I think the answer is no, as I already split the low-hanging thousands of lines from it in the past. #18345 splits out the last 50 or so lines in an easy way, but for the same reason would be easy to forward-port later

Johan Commelin (Feb 01 2023 at 12:07):

@Calvin Lee fyi, I just pushed some fixes

Calvin Lee (Feb 01 2023 at 12:11):

yep me too, I don't think we're working on anything conflicting, but I'm happy to stop if it makes things easier

Johan Commelin (Feb 01 2023 at 12:13):

No, please go ahead

Calvin Lee (Feb 01 2023 at 12:50):

Having a typeclass resolution issue on line 339, it works with set_option synthInstance.maxHeartbeats 500000
trace: https://paste.sr.ht/~pounce/59cd529832fc534a3ad60449274b671dc28e078c

Kevin Buzzard (Feb 01 2023 at 15:29):

 [tryResolve] [7.132600s] ❌ Ring (Module.End R { x // x ∈ N }) ≟ Ring (Module.End ?m.179306 ?m.179307) ▼
      [] [0.104616s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.096173s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.096049s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.096203s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.099098s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106227s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103798s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106911s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.109596s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106846s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.104730s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103525s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103775s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.102245s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.107397s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.108276s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.104062s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097365s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097216s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097538s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.095381s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.098824s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.101104s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106123s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.110068s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.105849s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106301s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.104094s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.102728s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.106125s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.104456s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103311s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.112193s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.110938s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097567s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.095208s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.099329s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103886s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.111523s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.098682s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.094006s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.113392s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097390s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.098329s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.095917s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.094190s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.092369s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.096521s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.105390s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097593s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.096123s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.094200s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097183s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.098124s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.126267s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.095530s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.095839s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.099397s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.094540s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.097697s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.099212s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.101507s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.099770s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.099125s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.095121s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.098686s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.102678s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.103136s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.102466s] ❌ AddCommGroup { x // x ∈ N } ▶
      [] [0.094496s] ❌ AddCommGroup { x // x ∈ N } ▶

Kevin Buzzard (Feb 01 2023 at 15:35):

Might be this https://github.com/leanprover/lean4/issues/2055 ?

Kevin Buzzard (Feb 01 2023 at 15:36):

Only 70 failures as opposed to the 300+ in that example, but they each take 0.1 seconds.

Jireh Loreaux (Feb 01 2023 at 15:37):

That's weird

Kevin Buzzard (Feb 01 2023 at 16:23):

Here's the behaviour on master:

import Mathlib.Algebra.Module.Submodule.Lattice


-- default maximum heartbeats = 20000


--set_option profiler true
set_option synthInstance.maxHeartbeats 120000 -- 100000 (five times the default) is not enough
--set_option trace.Meta.synthInstance true

example {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
{N : Submodule R M} {g : Module.End R N} (n : ℕ) : g ^ n = 0 := sorry

Lukas Miaskiwskyi (Feb 03 2023 at 19:32):

About an interesting porting note in the file (after line 1048):

section AddCommGroup

variable [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M)

variable [AddCommGroup M₂] [Module R M₂]
--Porting note: Why doesn't inferInstance work here?
example : AddCommGroup (M →ₗ[R] M₂) := LinearMap.addCommGroup

Replacing [Ring R] with [Semiring R] makes inferInstance work in the given example, so inferInstance seems unable to make use of the fact that Ring extends Semiring here. I don't know how to remedy this, but if someone has ideas, I believe this would solve quite a lot of issues in the file.

Eric Wieser (Feb 03 2023 at 19:41):

This sounds like it's caused by new structures to me

Eric Wieser (Feb 03 2023 at 19:42):

We had this problem a few times in mathlib3 too around normed_space (which is a new-style structure)

Eric Wieser (Feb 03 2023 at 19:42):

See for instance docs#normed_algebra.to_normed_space'

Kevin Buzzard (Feb 03 2023 at 20:43):

Are new structures the cause of some of the typeclass inference issues we're seeing in the port?

Eric Wieser (Feb 03 2023 at 20:52):

My speculation is yes, but maybe that's based on a lean3-centric model. It would be possible to test the theory by removing any uses of extends in the algebraic heirarchy and manually copying fields instead, but that's not a very pleasant thing to try or place to end up at

Calvin Lee (Feb 04 2023 at 03:05):

we've made it to under 100 errors! image.png
most of these are instance failures for linear maps—from what I can tell.

Johan Commelin (Feb 06 2023 at 14:15):

I just made a copy of this branch LinAlgBas-bump which merges !4#2105 into it. That branch now has no red errors anymore.

Johan Commelin (Feb 06 2023 at 14:16):

I also cherry-picked all fixes into the original branch.

Kevin Buzzard (Feb 06 2023 at 14:49):

Oh that's great news! So the bump is definitely solving problems as well as causing exciting new problems

Calvin Lee (Feb 10 2023 at 18:37):

this issue seems to persist after bumping to 4.0.0-nightly-2023-02-10, however (!4#2178)

Johan Commelin (Feb 10 2023 at 19:01):

Right, because the relevant PR to Lean 4 was reverted. Since it caused massive slowdowns in linarith (amongst other problems)

Pol'tta / Miyahara Kō (Feb 12 2023 at 07:02):

As a temporary remedy, this command removes all red errors.

attribute [-instance] Ring.toNonAssocRing

Pol'tta / Miyahara Kō (Feb 12 2023 at 08:02):

This theorem is not simp-normal form in Lean 3 and Lean 4, but this doesn't get lint in Lean 3.
Should we remain nolint simpNF? Or erase simp?

-- Mathlib\LinearAlgebra\Basic.lean L2513
@[simp, nolint simpNF]
theorem mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    refine' ⟨e.symm x, hx, by simp⟩
#align submodule.mem_map_equiv Submodule.mem_map_equiv

Johan Commelin (Feb 12 2023 at 08:09):

I think: leave it like this, but add a porting note with your remark.

Kevin Buzzard (Feb 12 2023 at 09:15):

Could it be that many of the non structure projection "short cut" instances which were helping in lean 3 are hindering in Lean 4?

Eric Wieser (Feb 12 2023 at 10:16):

Pol'tta / Kô Miyahara said:

This theorem is not simp-normal form in Lean 3 and Lean 4, but this doesn't get lint in Lean 3.
Should we remain nolint simpNF? Or erase simp?

What is the simp normal form in lean 3?

Pol'tta / Miyahara Kō (Feb 12 2023 at 11:08):

-- src/linear_algebra/basic.lean L2005
@[simp] lemma mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔
  e.symm x ∈ p :=
begin
  rw submodule.mem_map, split,
  { rintros ⟨y, hy, hx⟩, simp [←hx, hy], },
  { intros hx, refine ⟨e.symm x, hx, by simp⟩, },
end

example {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔
  e.symm x ∈ p :=
begin
  simp [-mem_map_equiv],
  -- (∃ (y : M), y ∈ p ∧ ⇑e y = x) ↔ ⇑(e.symm) x ∈ p
  sorry
end

This is the same in Lean 4.

Eric Wieser (Feb 12 2023 at 11:10):

The solution is lean4 is to increase the priority I think

Eric Wieser (Feb 12 2023 at 11:11):

Does simp use the new lemma in lean 4, or end up in that lean 3 goal state?

Pol'tta / Miyahara Kō (Feb 12 2023 at 11:22):

This ends up in the lean 3 goal state.

-- Mathlib/LinearAlgebra/Basic.lean L2513
-- Porting note: This theorem is not simp-normal form in Lean 3 and Lean 4, but this got no lint
-- in Lean 3.
@[simp, nolint simpNF]
theorem mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    refine' ⟨e.symm x, hx, by simp⟩
#align submodule.mem_map_equiv Submodule.mem_map_equiv

example {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  simp [-mem_map_equiv]
  -- (∃ y, y ∈ p ∧ ↑e y = x) ↔ ↑(LinearEquiv.symm e) x ∈ p
  sorry

#exit

Eric Wieser (Feb 12 2023 at 11:36):

I mean simp instead of simp [-mem_map_equiv]

Pol'tta / Miyahara Kō (Feb 12 2023 at 11:42):

Even using simp, the result is the same.

-- Mathlib/LinearAlgebra/Basic.lean L2513
-- Porting note: This theorem is not simp-normal form in Lean 3 and Lean 4, but this got no lint
-- in Lean 3.
@[simp, nolint simpNF]
theorem mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    refine' ⟨e.symm x, hx, by simp⟩
#align submodule.mem_map_equiv Submodule.mem_map_equiv

example {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  simp
  -- (∃ y, y ∈ p ∧ ↑e y = x) ↔ ↑(LinearEquiv.symm e) x ∈ p
  sorry

#exit

Pol'tta / Miyahara Kō (Feb 12 2023 at 11:49):

However, @[simp high] solved this.

-- Mathlib/LinearAlgebra/Basic.lean L2513
-- Porting note: This theorem is not simp-normal form in Lean 3 and Lean 4, but this got no lint
-- in Lean 3.
@[simp high, nolint simpNF]
theorem mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    refine' ⟨e.symm x, hx, by simp⟩
#align submodule.mem_map_equiv Submodule.mem_map_equiv

example {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  simp
  -- No goals

#exit

Pol'tta / Miyahara Kō (Feb 12 2023 at 11:51):

I commited this change (with erasing nolint simpNF). Thank you!

Eric Wieser (Feb 12 2023 at 12:02):

Does that match the Lean3 behavior now, or does lean3 also need a higher priority?

Pol'tta / Miyahara Kō (Feb 12 2023 at 12:14):

That match the Lean3 behavior.

-- src/linear_algebra/basic.lean L2005
@[simp] lemma mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔
  e.symm x ∈ p :=
begin
  rw submodule.mem_map, split,
  { rintros ⟨y, hy, hx⟩, simp [←hx, hy], },
  { intros hx, refine ⟨e.symm x, hx, by simp⟩, },
end

example {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔
  e.symm x ∈ p :=
begin
  simp,
  -- goals accomplished 🎉
end

Pol'tta / Miyahara Kō (Feb 13 2023 at 02:56):

I think this problem is caused because the type class synthesizer fails to unify diamond inheritances.

import Mathlib.Algebra.BigOperators.Pi
import Mathlib.Algebra.Module.Hom
import Mathlib.Algebra.Module.Prod
import Mathlib.Algebra.Module.Submodule.Lattice
import Mathlib.Algebra.Module.LinearMap
import Mathlib.Data.Dfinsupp.Basic
import Mathlib.Data.Finsupp.Basic

variable {R M₁ M₂ : Type _} [iᵣ : Ring R] [iₘ₁ : AddCommGroup M₁] [iᵣₘ₁ : Module R M₁]
variable [iₘ₂ : AddCommGroup M₂] [iᵣₘ₂ : Module R M₂]

example : AddCommGroup (M₁ →ₗ[R] M₂) := inferInstance
-- failed to synthesize instance
--   AddCommGroup (M₁ →ₗ[R] M₂)

In the above example, originally, this instance should be matched.

instance LinearMap.addCommGroup {R₁ R₂ N₁ N₂ : Type _}
  [jᵣ₁ : Semiring R₁] [jᵣ₂ : Semiring R₂] [jₙ₁ : AddCommMonoid N₁] [jₙ₂ : AddCommGroup N₂]
  [jᵣₙ₁ : Module R₁ N₁] [jᵣₙ₂ : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : AddCommGroup (N₁ →ₛₗ[σ₁₂] N₂)

However, the synthesizer considers these are not def-eq.

AddCommGroup (M₁ →ₗ[R] M₂) =?= AddCommGroup (?N₁ →ₛₗ[?σ₁₂] ?N₂)
-- explicit
AddCommGroup
  (@LinearMap R R
    (@Ring.toSemiring R iᵣ)
    (@Ring.toSemiring R iᵣ)
    (@RingHom.id R (@NonAssocRing.toNonAssocSemiring R
      (@Ring.toNonAssocRing R iᵣ)))
    M₁ M₂
    (@AddCommGroup.toAddCommMonoid M₁ iₘ₁)
    (@AddCommGroup.toAddCommMonoid M₂ iₘ₂)
    iᵣₘ₁ iᵣₘ₂)
  =?=
AddCommGroup
  (@LinearMap ?R₁ ?R₂
    ?jᵣ₁
    ?jᵣ₂
    ?σ₁₂
    ?N₁ ?N₂
    ?jₙ₁
    (@AddCommGroup.toAddCommMonoid ?N₂ ?jₙ₂)
    ?jᵣₙ₁ ?jᵣₙ₂)

The most obstacles to unify these is this.

@RingHom.id R (@NonAssocRing.toNonAssocSemiring R
  (@Ring.toNonAssocRing R iᵣ))
  =?=
?σ₁₂

The key is these types.

@RingHom R R
  (@NonAssocRing.toNonAssocSemiring R
    (@Ring.toNonAssocRing R iᵣ))
  (@NonAssocRing.toNonAssocSemiring R
    (@Ring.toNonAssocRing R iᵣ))
  =?=
@RingHom ?N₁ ?N₂
  (@Semiring.toNonAssocSemiring ?R₁ ?jᵣ₁)
  (@Semiring.toNonAssocSemiring ?R₂ ?jᵣ₂)

The instances of NonAssocSemiring on LHS is derived from NonAssocRing, in contrast LHS, the instances of NonAssocSemiring on RHS is derived from Semiring.
I think this difference is the cause of red errors on LinearAlgebra/Basic, but I have no idea to fix this without disabling Ring.toNonAssocRing.

Kevin Buzzard (Feb 13 2023 at 05:40):

Is this related to lean4#2074 ?

Pol'tta / Miyahara Kō (Feb 13 2023 at 06:06):

I think it is related.

Johan Commelin (Feb 13 2023 at 06:07):

@Pol'tta / Kô Miyahara Thank you so much for this fix! I kicked the PR on the queue

Johan Commelin (Feb 13 2023 at 06:07):

We'll have to find a long-term solution later. But at least this way the port is unblocked again!

Last updated: Dec 20 2023 at 11:08 UTC