feat(RingTheory/MvPowerSeries/NoZeroDivisors): simplify the proof by adding two instances by AntoineChambert-Loir · Pull Request #36892 · leanprover-community/mathlib4

AntoineChambert-Loir · 2026-03-20T08:10:02Z

Clean up unwanted declarations regarding to well-orderings.

add exists_wellFoundedGTthat gives a linear ordering that satisfies WellFoundedGT
rename exists_wellOrder to exists_wellFoundedLT, deprecate the previous name, and add to_dual existing to relate the two functions.
add the instanceWellFoundedLT.wellOrderingRel suggested by @eric-wieser : WellOrderingRel.isWellOrder satisfies WellFoundedLT
adjust at a handful places, in particular in the proof of MvPowerSeries.NoZeroDivisors that the power series rings over a ring without zero divisors has no zero divisors, where the opposite of a “anti-well ordering” was needed.
delete LinearOrder.swap which abuses defeq (and was only used once for that proof).

Ref. #mathlib4 > help in RingTheory.MvPowerSeries.NeZeroDivisors

github-actions · 2026-03-20T08:11:11Z

PR summary b43655dfe2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ exists_wellFoundedGT
+ exists_wellFoundedLT

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

vihdzp · 2026-03-20T08:33:05Z

Can we add to_dual to both of these?

JovanGerb · 2026-03-20T09:31:47Z

Note that the dual instance gets different discrimination tree keys. The whole situation seems a bit dodgy

instance WellFoundedGT.swap {l : LinearOrder σ} [WellFoundedLT σ] :
    letI : LinearOrder σ := l.swap _; WellFoundedGT σ :=
  ‹WellFoundedLT σ›

instance WellFoundedLT.swap {l : LinearOrder σ} [WellFoundedGT σ] :
    letI : LinearOrder σ := l.swap _; WellFoundedLT σ :=
  ‹WellFoundedGT σ›

#discr_tree_key WellFoundedGT.swap -- IsWellFounded _ <other>
#discr_tree_key WellFoundedLT.swap -- IsWellFounded _ (@LT.lt _ _)

Recall that <other> means that it matches with any lambda expression.

mariainesdff · 2026-04-09T09:14:09Z

@eric-wieser, could you please have a look? This comes from the discussion in #mathlib4 > help in RingTheory.MvPowerSeries.NeZeroDivisors; it looks ok to me but I might be missing something.

JovanGerb · 2026-04-09T11:15:17Z

In my opinion, LinearOrder.swap should not exist in the first place. Could you instead refactor that proof to not use LinearOrder.swap, and then deprecate LinearOrder.swap? It is the only use of LinearOrder.swap

eric-wieser · 2026-04-09T14:06:55Z

Sorry for dropping the ball here; I had not thought to look at the discrimination trees, and indeed these seem like a mark against this strategy. I'll investigate a little more now.

JovanGerb · 2026-04-09T14:35:22Z

Note also that there does not exist anything similar to LinearOrder.swap for any other type class.

AntoineChambert-Loir · 2026-04-09T19:29:58Z

I will try to do as @JovanGerb requested. On the other hand, I would like to have a better understanding of the discussion — could you give me pointers to this question of discrimination trees, I'm ashamed to admit that I can't even parse Lean's output in Jovan's message.

vihdzp · 2026-04-10T01:05:35Z

Mathlib/SetTheory/Cardinal/Order.lean

+
 variable (α) in
 /-- The **well-ordering theorem** (or **Zermelo's theorem**): every type has a well-order -/
 theorem exists_wellOrder : ∃ (_ : LinearOrder α), WellFoundedLT α := by


Perhaps this should be renamed exists_wellFoundedLT? And perhaps we can generate the other one via to_dual? (or at least tag it with to_dual existing)

About the renaming, I'm OK for that, it's only used four or five times. But WellFoundedLT doesn't impose LinearOrder, so I'm not sure that the name will truly reflect what is done. (And the remark applies to the new version exists_wellFoundedLT). Give a firm order and I'll do it.

I do not understand the remark about to_dual, because at that point, one has no LinearOrder on the type.

The previous name is even worse imo since we don't have anything called WellOrder (save for an auxiliary structure in the definition of ordinals, which this is not about). If you think this should reference linearOrder then why not exists_linearOrder_wellFoundedLT? Though this feels a bit verbose and I still prefer exists_wellFoundedLT.

Maybe this change can be split out of the PR? Seems like the stuff with LinearOrder.swap is a bit controversial, and the new WellFoundedGT theorem seems like a good, orthogonal change.

I do not understand the remark about to_dual, because at that point, one has no LinearOrder on the type.

Does to_dual existing not work regardless?

Maybe @AntoineChambert-Loir is not familiar with the @[to_dual] attribute for generating dual versions of declarations?

Indeed, I hadn't understood that it was similar to @[to_additive], I confused it with something applied to OrderDual.
Now, to_dual doesn't work, but to_dual existing worked. I also renamed the thing.

JovanGerb · 2026-04-11T16:02:03Z

As far as I know, there isn't really a comprehensive writeup of what discrimination trees do in Lean. I should maybe write some :).

In short a discrimination tree is a data structure for storing and looking up expression patterns. The is used in simp and in type class search in order to get a list of candidate simp lemmas or candidate instances. Each simp lemma/instance is stored in the discrimination tree using a list of discrimination tree keys. It's helpful to know what the keys for a specific lemma/instance are, because if the keys are wrong/too specific, it may not get found. And on the other hand if the keys are too general, then it will be found too often, which is bad for performance.

JovanGerb · 2026-04-11T16:05:39Z

But I think the discrimination tree keys aren't the main reason why I didn't like the instance. Rather, I had a problem with the swapping of the order in the funny LinearOrder instance. Instead, using OrderDual would be the right approach for that.

AntoineChambert-Loir · 2026-04-11T16:09:51Z

I don't see how to use OrderDual for that. You can impose an well ordering (wellFoundedLT) on OrderDual α, but that won't give you anything on α itself…

JovanGerb · 2026-04-11T16:45:12Z

Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

+    let : LinearOrder σ := (exists_wellFoundedGT σ).choose
+    have : WellFoundedGT σ := (exists_wellFoundedGT σ).choose_spec


Rather than using choose and choose_spec, you should be able to use rcases, right?

Yes. Is it better?

JovanGerb · 2026-04-11T16:48:30Z

but that won't give you anything on α itself…

Well, OrderDual α is definitionally equal to α, so if you are happy abusing this defeq, then you can do it. This trick is used widely in Mathlib, though there are now people saying that this kind of defeq abuse is actually a bad idea.

AntoineChambert-Loir · 2026-04-11T17:15:52Z

Wouldn't it be tantamount to the proof to which the first round of review objected!

AntoineChambert-Loir · 2026-04-12T08:12:08Z

This PR is only 16 lines, I rewrote the description and it looks fairly coherent to me. May I beg you not to ask me to split into two or three tiny parts?

JovanGerb · 2026-04-12T08:13:18Z

Mathlib/SetTheory/Cardinal/Order.lean

  ⟨⟨WellOrderingRel, inferInstance⟩⟩

+/-- This instance is about `WellOrderingRel.isWellOrder.linearOrder`. -/
+instance WellFoundedLT.wellOrderingRel :


Do we need this instance in this PR? I would be against adding it.

This is the other one suggested by Eric. The (initial) point was to remove the defeq abuses related to LinearOrder.swap, maybe that one is no more necessary.

I'm commenting it out, and if that compiles, which it should, I'll remove it.

(This PR started doing something, and made something else, probably cleaner, maybe that's the joy of collaborative work!)

…hlib4 into ACL-EWInstances

add two instances

06159c4

grunweg added the t-ring-theory Ring theory label Mar 30, 2026

mathlib-triage bot assigned mariainesdff Apr 1, 2026

mariainesdff assigned eric-wieser Apr 9, 2026

AntoineChambert-Loir added 3 commits April 9, 2026 21:39

Merge branch 'master' into ACL-EWInstances

b7d95be

avoid LinearOrder.swap

9f6b3fe

add deprecation and remove bad instance

f2abb54

vihdzp reviewed Apr 10, 2026

View reviewed changes

JovanGerb reviewed Apr 11, 2026

View reviewed changes

AntoineChambert-Loir added 2 commits April 11, 2026 19:19

use rcases instead of choose/choose_spec

9597e6f

use to_dual existing and rename and deprecate

2185a3f

JovanGerb reviewed Apr 12, 2026

View reviewed changes

AntoineChambert-Loir added 4 commits April 12, 2026 10:25

comment out instance

880810e

Merge branch 'master' into ACL-EWInstances

5658c7a

delete instance

b1432ac

Merge branch 'ACL-EWInstances' of github.com:AntoineChambert-Loir/mat…

aab8b93

…hlib4 into ACL-EWInstances

		let : LinearOrder σ := (exists_wellFoundedGT σ).choose
		have : WellFoundedGT σ := (exists_wellFoundedGT σ).choose_spec

Conversation

AntoineChambert-Loir commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b43655dfe2

Import changes for modified files

Declarations diff

Uh oh!

vihdzp commented Mar 20, 2026

Uh oh!

JovanGerb commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mariainesdff commented Apr 9, 2026

Uh oh!

JovanGerb commented Apr 9, 2026

Uh oh!

eric-wieser commented Apr 9, 2026

Uh oh!

JovanGerb commented Apr 9, 2026

Uh oh!

AntoineChambert-Loir commented Apr 9, 2026

Uh oh!

vihdzp Apr 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JovanGerb commented Apr 11, 2026

Uh oh!

JovanGerb commented Apr 11, 2026

Uh oh!

AntoineChambert-Loir commented Apr 11, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JovanGerb commented Apr 11, 2026

Uh oh!

AntoineChambert-Loir commented Apr 11, 2026

Uh oh!

AntoineChambert-Loir commented Apr 12, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

AntoineChambert-Loir commented Mar 20, 2026 •

edited

Loading

github-actions bot commented Mar 20, 2026 •

edited

Loading

JovanGerb commented Mar 20, 2026 •

edited

Loading

vihdzp Apr 10, 2026 •

edited

Loading