[Merged by Bors] - chore: mark Submodule.toAddSubgroup @[reducible]

[kim-em]

This PR marks Submodule.toAddSubgroup as @[reducible], matching the reducibility that a real structure parent projection would have (Lean marks structure parent projections [reducible]). This resolves backward.isDefEq.respectTransparency failures where Lean needs to see that s.toAddSubgroup.toAddSubmonoid = s.toAddSubmonoid.

The motivating example is:

instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} :
    Module.Free ℝ l := Module.Free.of_divisionRing ℝ l

which fails with backward.isDefEq.respectTransparency because synthesis of Module ℝ ↥l needs Submodule.module, whose AddCommMonoid comes through toAddSubgroup (a virtual parent), while the Module prerequisite expects AddCommMonoid from toAddSubmonoid (a real projection). Lean must unfold toAddSubgroup to see these agree, but as a plain def it was [semireducible] and invisible at instance transparency.

See #general > backward.isDefEq.respectTransparency and the synthetic test case in #35750.

[github-actions]

PR summary 9b1001cbdb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (25.25, 0.54)

Current number	Change	Type
11071	-790	backward.isDefEq
47	-22	backward.whnf

Current commit 416e79d87c
Reference commit 9b1001cbdb

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

Commit Verification Summary

Warning

Some verifications failed. See details below.

Commits to Review (2)

• ccede82: chore: mark Submodule.toAddSubgroup implicit_reducible
• e586b7a: let's just do one thing at a time

View PR diff

\u274c Automated commits (1) - 0/1 verified

Commit	Command	Status
46fccb0	x: scripts/rm_set_option.py	❌ Command failed with exit code 1

---

Generated by commit verification CI

[eric-wieser]

Can you explain what the repro for this was and why it is a good idea in the PR description?

[kim-em]

Can you explain what the repro for this was and why it is a good idea in the PR description?

I would really prefer not to. It is explained in the Zulip threads.

[eric-wieser]

My reading of that thread is "we should do this because it makes the error go away", I don't see any strong claim that this is actually the direction we want to go in or why. If you intend to make that claim, then the PR description is the place to put it.

[urkud]

Submodule.toAddSubgroup is not a structural projection, but it is used to construct some instances (e.g., AddCommGroup). My guess is that without this attribute, Lean fails to see that s.toAddSubgroup.toAddSubmonoid = s.toAddSubmonoid.

[eric-wieser]

Is every extends parent of a structure marked as implicit_reducible by default, which justifies doing this for pseudo-parents?

I'd assumed that was only true of classes.

[kim-em]

Is every extends parent of a structure marked as implicit_reducible by default, which justifies doing this for pseudo-parents?

I'd assumed that was only true of classes.

https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Structure.lean#L114C1-L116C49

Structure parents are reducible:

import Lean

-- Plain structures
structure Foo where
  x : Nat

structure Bar extends Foo where
  y : Nat

-- Classes
class Baz where
  z : Nat

class Qux extends Baz where
  w : Nat

-- Class extending a structure
class Quux extends Foo where
  v : Nat

-- Structure extending a class
structure Corge extends Baz where
  u : Nat

open Lean in
/-- info: Bar.toFoo (structure extends structure): Lean.ReducibilityStatus.reducible
---
info: Qux.toBaz (class extends class): Lean.ReducibilityStatus.implicitReducible
---
info: Quux.toFoo (class extends structure): Lean.ReducibilityStatus.semireducible
---
info: Corge.toBaz (structure extends class): Lean.ReducibilityStatus.reducible
-/
#guard_msgs in
#eval show CoreM Unit from do
  let env ← getEnv
  let check (name : Name) (desc : String) : CoreM Unit := do
    let status := getReducibilityStatusCore env name
    logInfo m!"{name} ({desc}): {repr status}"
  check `Bar.toFoo "structure extends structure"
  check `Qux.toBaz "class extends class"
  check `Quux.toFoo "class extends structure"
  check `Corge.toBaz "structure extends class"

This really needs to be in reference manual rather than digging through the code to understand. :-(

[kim-em]

So maybe the right fix here is actually @[reducible] not @[implicit_reducible].

[eric-wieser]

That seems like the right conclusion to me, thanks for the test-case.

[eric-wieser]

Do we want to encourage abbrev instead of reducible for such cases?

[eric-wieser]

!bench

[leanprover-radar]

Benchmark results for 52f499c against 02dfd80 are in! @eric-wieser

• 🟥 main exited with code 1

No significant changes detected.

[eric-wieser]

This seems a little asymmetric with toAddSubmonoid_inj, which is allowed by simp. I suppose if it were a "real" projection though (with overlapping base classes) we'd have the same behavior, so fixing the asymmetry is out of scope.

[fpvandoorn]

This seems unobjectionable to me. This also fits within the scope of the library note reducible non-instances. Feel free to treat this as a bors d+ if the bench looks ok.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[eric-wieser]

This also fits within the scope of the library note reducible non-instances.

Does it? That note is for things whose type is a class, am which AddSubgroup is not.

I'm not opposed to the PR, but this isn't the first time this confusion has come up in discussion about it

[fpvandoorn]

Does it? That note is for things whose type is a class, am which AddSubgroup is not.

I'm not opposed to the PR, but this isn't the first time this confusion has come up in discussion about it

Oops, my bad. You're right. It still seems fine, though.

[kim-em]

!bench

[leanprover-radar]

Benchmark results for 416e79d against 9b1001c are in! @kim-em

• 🟥 build//instructions: +5.3G (+0.00%)

No significant changes detected.

[kim-em]

I'm taking Floris' message about as now a bors d+, since the benchmark was fine.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job