backward.isDefEq.respectTransparency

Stream: general

[Weiyi Wang]

This looks like a new change in 4.29.0-rc1, and its behavior puzzles me... for example

import Mathlib

-- set_option backward.isDefEq.respectTransparency false -- uncomment this to remove error below

example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by simp --error
example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg] -- error
example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := sub_nonneg -- ok

What is going on here?

[Yury G. Kudryashov]

Can you minimize this example? FRO prefers to have bug reports that don't use Mathlib.

[Weiyi Wang]

Hmm not sure where to start... I think I'll need to extract the class hierarchy for AddGroup minimize there?

[Weiyi Wang]

A quick note, adding an explicit type parameter makes it work again

example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg (α := ℝ)]

[Weiyi Wang]

or even just one regular parameter also works

example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg (a := a)]

[Weiyi Wang]

@Yury G. Kudryashov Here is a Mathlib-less example

--set_option backward.isDefEq.respectTransparency false

class AddZero' (M : Type u_2) extends Zero M, Add M where

class AddMonoid' (M : Type u) extends Add M, AddZero' M where

instance : AddZero' Int where
instance : AddMonoid' Int where

theorem sub_nonneg' {α : Type u} [AddMonoid' α] [Sub α] [LE α] {a b : α} :
  0 ≤ a - b ↔ b ≤ a := sorry

example (a b : Int) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg'] -- error

I suspect it is the part where Add M appeared twice in the hierarchy that caused the problem. I extracted this structure from mathlib

[Yury G. Kudryashov]

@Kim Morrison WDYT?

[Jovan Gerbscheid]

Note that when using the set_option, the unification is solved because unification finds a stuck metavariable that it then decides to synthesize a value of:

[Meta.isDefEq.stuckMVar] found stuck MVar ?inst✝ : AddGroup ℝ
[Meta.synthInstance] ✅️ AddGroup ℝ ▶

And if you don't use the set_option, this doesn't happen.

[Jovan Gerbscheid]

Aha, I figured out a solution. If you write

set_option allowUnsafeReducibility true in
attribute [instance_reducible] Zero.zero

in your example, then it works.

[Jovan Gerbscheid]

What I don't understand here is why Zero.zero is not already instance_reducible. The point of instance_reducible transparency is so that instances and instance projections can be unfolded during instance unification (and this was the case before the new Lean version).

[Weiyi Wang]

There are other failures under the same change that we cna collect here like https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/fail.20to.20synth.20an.20easy.20instance/with/574495259

I also saw some different flavor of errors in my project. When I get time I can minimize them as well

[David Loeffler]

I think there will be an announcement soon from the mathlib maintainers about this (there's been some discussion ongoing in the mathlib reviewers channel). I'm not a maintainer, but let me say that (a) the maintainers and the Lean core team are working urgently on this, and (b) your minimized example is very greatly appreciated by all involved.

[Eric Wieser]

Here's another mathlib-free failure adapted from my "Multiple-inheritance hazards in dependently-typed algebraic hierarchies" paper:

class add_monoid (α : Type) :=
(zero : α) (add : α → α → α)

class add_comm_monoid (α : Type) extends add_monoid α

class semiring (α : Type) extends add_comm_monoid α :=
(one : α) (mul : α → α → α)

attribute [instance 1000] semiring.toadd_comm_monoid

class add_group (α : Type) extends add_monoid α :=
(neg : α → α)

class add_comm_group (α : Type) extends add_group α, add_comm_monoid α

attribute [instance 10] add_comm_group.toadd_comm_monoid

class ring (α : Type) extends semiring α, add_comm_group α

attribute [instance 0] ring.toadd_comm_group

class module (α β : Type) [semiring α] [add_comm_monoid β] :=
(smul : α → β → β)

instance semiring.to_module (α) [semiring α] : module α α := { smul := semiring.mul }

theorem neg_smul {R M} [ring R] [add_comm_group M] [module R M] (r : R) (m : M) :
  module.smul (add_group.neg r) m = add_group.neg (module.smul r m) := sorry

-- fails
example {R} [iR : ring R] (r : R) (r' : R) :
    module.smul (add_group.neg r) r' = add_group.neg (module.smul r r') := by
  rw [neg_smul r r']

-- ok
set_option backward.isDefEq.respectTransparency false in
example {R} [iR : ring R] (r : R) (r' : R) :
    module.smul (add_group.neg r) r' = add_group.neg (module.smul r r') := by
  rw [neg_smul r r']

[David Loeffler]

Eric Wieser said:

Here's another mathlib-free failure adapted from my "Multiple-inheritance hazards in dependently-typed algebraic hierarchies" paper:

Is this "another example of the same failure", or "a different failure mode"? (Or is it hard to tell?)

[Eric Wieser]

I haven't had a chance to look in any detail, but my guess is that this is the same failure mode (failure to handle commuting typeclass diamonds, not structure eta)

[Eric Wieser]

(the adaptations above are just to switch to the new set_option and remove things that no longer fail)

[Eric Wieser]

David Loeffler said:

I think there will be an announcement soon from the mathlib maintainers about this

To this end, I would recommend not immediately resolving any non-trivial merge conflicts created by these new set_options, just in case we end up making a decision in a day or so that renders this unecessary.

[Jovan Gerbscheid]

I think I understand a bit better now what is going on in Weiyi Wang's example.

The unification algorithm decides whether to try to synthesize an instance metavariable by calling the function getStuckMVar?. This function searches for an instance metavariable in an expression by recursing into arguments of projection instances. In this case it is being called on Zero.zero, which contains a metavariable of type AddMonoid' Int. We want it to synthesize this metavariable with type class search, so that the unification can then succeed.

The reason why this worked originally is that unification would unfold Zero.zero into the projection .1, and the call getStuckMVar? on that. Since getStuckMVar? does recurse into all projections, it does find the metavariable that we want it to find. But now, since Zero.zero isn't unfolded, getStuckMVar? doesn't find the required metavariable.

[Violeta Hernández]

Just to be clear, this is a bug, right? Should we hold off on updating our projects until it's resolved?

[Sebastian Ullrich]

Violeta Hernández said:

Just to be clear, this is a bug, right?

Yes, there is a tentative fix at lean#12564

[Robin Arnez]

I also have a local "fix" which makes getStuckMVar? more correct (such that it can recurse more effectively and report things that actually block reduction) and also removes quite a few set_option backward.isDefEq.respectTransparency false ins but there's unfortunately many mathlib adaptations necessary (I'm not done lol). One of the common adaptations is what I've dubbed "CoeT explosion". Here's an example:

import Mathlib

variable (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (h : a < b)

set_option trace.Meta.isDefEq true in
#check inv_strictAntiOn ha hb h

inv_strictAntiOn receives as a first parameter ?a ∈ Set.Ioi 0 and we provide 0 < a. You might think here: Well it does the reduction and the unifies ?a := a and everything is fine but no! You can see two defeq failures!

[Meta.isDefEq] ❌️ ?m.15 ∈ Set.Ioi 0 =?= 0 < a ▶
[Meta.isDefEq] ❌️ 0 < a =?= ?m.15 ∈ Set.Ioi 0 ▶

turns out it reduces too much on the Real side and then doesn't know what to do with the < from the Set.Ioi anymore because it's too generic. Now you might ask yourself: Why does it work then? Well, "CoeT explosion" it is:

[Meta.isDefEq] 💥️ CoeT (0 < a) ha (?m.15 ∈ Set.Ioi 0) =?= CoeT ?m.17 ?m.18 ?m.17 ▼
  [] ✅️ 0 < a =?= ?m.17 ▶
  [] ✅️ ha =?= ?m.18 ▶
  [] 💥️ ?m.15 ∈ Set.Ioi 0 =?= 0 < a ▼
    [] 💥️ ?m.15 ∈ Set.Ioi 0 =?= 0 < a ▼
      [] ❌️ @Membership.mem =?= @LT.lt
      [onFailure] 💥️ ?m.15 ∈ Set.Ioi 0 =?= 0 < a ▼
        [stuckMVar] found stuck MVar ?m.15 : ?m.11

CoeT fails because of a stuckMVar (which we don't find with my patch) and thus the term elaboration gets delayed in a similar way to by exact. Thus, many fixes involved adding smileys or by exacts to influence elaboration order.

[Kim Morrison]

Violeta Hernández said:

Just to be clear, this is a bug, right? Should we hold off on updating our projects until it's resolved?

See the announcement post about v4.29.0-rc1.

[David Loeffler]

Eric Wieser said:

To this end, I would recommend not immediately resolving any non-trivial merge conflicts created by these new set_options, just in case we end up making a decision in a day or so that renders this unecessary.

Is this still the situation?

I have several PR's that have dropped off the review queue because they picked up conflicts with the isDefEq workarounds. I'm wondering how long I should wait before merging latest master into them.

[Kim Morrison]

I'm hoping to have an rc2 out later today, but I wouldn't expect any changes to respectTransparency on Mathlib master until at least tomorrow.

[Kim Morrison]

(And there will still be many even after the rc2, so I would advise getting on with life and doing the merge conflict resolutions!)

[Eric Wieser]

Do you agree with my claim that more than half of these are issues with the feature itself, rather than mathlib abusing type aliases?

[Eric Wieser]

(I would expect us to get in a lot of justified trouble in Category theory, but all the algebra-related stuff seems like it is not to blame)

[Kim Morrison]

Okay, we are on rc2 now. Looking forward to seeing #mwe's of remaining problems Mathlib is having.

[Kim Morrison]

Everyone is invited to continue investigating removing set_option backwards, and helping to construct concrete examples, without Mathlib imports, where it looks like further changes are required.

[Kim Morrison]

(I am running a script to see which set_option backwards can be removed without any changes, but I suspect that I got most of these already in the intervening nightly testings.)

[Kim Morrison]

Eric Wieser said:

Do you agree with my claim that more than half of these are issues with the feature itself, rather than mathlib abusing type aliases?

I'm not sure what "half of these" is referring to.

[Kim Morrison]

In particular, both Weiyi's and Eric's examples above work fine on rc2.

[Jeremy Tan]

This lemma in mathlib doesn't depend on anything else in mathlib:

universe u

theorem List.ofFn_get {α : Type u} : ∀ l : List α, ofFn (get l) = l
  | [] => rfl
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

It fails unless the respectTransparency option is false, and it fails even if the implicit argument (f := (a :: l).get) is provided to ofFn_succ.

[Jeremy Tan]

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ofFn (a :: l).get
in the target expression
  ofFn (a :: l).get = a :: l

[Jeremy Tan]

where the top ofFn (a :: l).get has type (upon hovering)

@ofFn α (l.length + 1) (a :: l).get : List α

and the bottom one has type

@ofFn α (a :: l).length (a :: l).get : List α

[Robin Arnez]

I feel like this is intentional? After all, (a :: l).length doesn't obviously look like _ + 1 so using this lemma there is technically defeq abuse; I guess that's one place where backward.isDefEq.respectTransparency actually makes sense to use.

[Jeremy Tan]

But we are trying to remove respectTransparency. The two terms are definitionally equal, so something must be done with rw

[Weiyi Wang]

If this is the intended new behavior, how would one fix the type mismatch in the expression? (A genuine question because I want to learn more technical skills in Lean)

[Christian Merten]

simp only [length_cons] fixes that (the whole goal is solved by simp, but that's not the point here I guess).

universe u

theorem List.ofFn_get {α : Type u} : ∀ l : List α, ofFn (get l) = l
  | [] => rfl
  | a :: l => by
    simp only [length_cons]
    rw [ofFn_succ]
    congr
    exact ofFn_get l

[Christian Merten]

Jeremy Tan said:

But we are trying to remove respectTransparency. The two terms are definitionally equal, so something must be done with rw

rw operates at reducible transparency and (a :: l).length is not reducibly def-eq to l.length + 1:

/--
error: Tactic `rfl` failed: The left-hand side
  (a :: l).length
is not definitionally equal to the right-hand side
  l.length + 1

α : Type u
l : List α
a : α
⊢ (a :: l).length = l.length + 1
-/
#guard_msgs in
example {α : Type u} (l : List α) (a : α) :
    (a :: l).length = l.length + 1 := by
  with_reducible rfl

[Weiyi Wang]

Ah, my mind overcomplicated it because I did not realize it was a mismatch in an implicit parameter. I thought it was a mismatch in a deeper type or something. Thanks!

[Jeremy Tan]

Christian Merten said:

rw operates at reducible transparency and (a :: l).length is not reducibly def-eq to l.length + 1:

So what should be the course of action taken with List.ofFn_get and respectTransparency?

[Christian Merten]

universe u

theorem List.ofFn_get {α : Type u} (l : List α) : ofFn (get l) = l := by
  induction l <;> simp

Or the old proof but by simp in the second branch of the pattern match.

[Jeremy Tan]

From a cursory playaround most of the cases of rw failing when respectTransparency is removed come from mismatching instances. For example, in powersetCard_empty_subsingleton:

lemma powersetCard_empty_subsingleton (n : ℕ) :
    (powersetCard n (∅ : Finset α) : Set <| Finset α).Subsingleton := by
  intro x mx y my
  simp_all only [SetLike.mem_coe]
  rw [mem_powersetCard] at mx my
  simp only [Set.Subsingleton, SetLike.mem_coe]

We have the error message

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Membership.mem (Finset ?m.20) (Finset (Finset ?m.20)) instMembership (powersetCard ?m.21 ?m.23) ?m.22
in the target expression
  @Membership.mem (Finset α) (Finset (Finset α)) SetLike.instMembership (powersetCard n ∅) x

How are we to fix these mismatching instances?

[Jeremy Tan]

(The original proof is simp [Set.Subsingleton, subset_empty])

[Jeremy Tan]

#35718 removes eight instances of the option. If you can remove some more, please add them as reviews to #35718

[Jeremy Tan]

If the instance mismatches indicate that our instance hierarchy is a mess, I don't know how we're going to fix that mess

[Eric Wieser]

Kim Morrison said:

I'm not sure what "half of these" is referring to.

"these" referred to backward.isDefEq.respectTransparency false lines.

[Matthew Jasper]

Reduced from https://github.com/leanprover-community/mathlib4/blob/0c08ce96d5d3380690ac7ca205fe21c06e049e3e/Mathlib/Algebra/AddConstMap/Basic.lean#L292

https://live.lean-lang.org/#codez=CYUwZgBA8gTqMBECuBDANhAFIRuAIC4IAVATwAcQIB9ASnyLIsvwF4AoCCbV1gYzRQDOAiAFliAQWDAsAcTolyVWgHcAFiBgh2EALbFKKKXTmAkwginz3AJYA7AQBcUNnhQDeuAgsYBfCAG1VOjFJaWwAXSCJI0xYeGR0Tlo8ZghVbgA3FBgrFAAjNApMOU8GJX9goxkw7hAADxQdUgK6TFswDQBJO0dnEHFhTArpGWpaFNabdpguhycXfqwhrFiNeIwR0ZYIXOJtZSt7VUpNYCQeK3yQAxtgSltZ3uEYMAwIAFo36ABpGvrG5oIEymMx68wGSw2ADo9AYjOM2p1unM+uCotIYnBVqh1qNqND9IZpMltrsOPtDscQKdzpdrrd7qCQE8XhwPhAAKIwGAAexgRBQPHsVh4EAABs80KKIGAUFYCsA8NxWEA

[Matthew Jasper]

https://live.lean-lang.org/#codez=CYUwZgBA8gTqMBECuBDANhAFIRuAIC4IAVATwAcQIB9ASnyLIsvwF4AoCCbV1gYzRQDOAiAFliAQWDAsAcTolyVWgHcAFiBgh2EFFLpzASYQRDx7n0HCRAewB2VgJbTMcggsa0QADwAuIG8EsJPTk1DS0OAC8NK30zfiEISWAASRsAN1l5BiUIL19/QKTjCFDNbXt0/QgjGTiLYxgrJFJZV2yaXJ8/ANFbB2kZABpEqVSM2tYKgW8UGx4KAG9cNsVKAF8IAG1VfUbmzgBdXaaWzFh4ZHROWjxmCFVuNJQYexQAIzQKZyzV2k2ZPYtGQHbheFAAW1InzomAqYA0qWms3m4mEzkBxmo1AAdN4rNY7I4IHdYTZ4TBETM5iBUbIMWc4BpLhgZFicXiCf0WBA3sRtMp7N5VJRNMAkDx7B8QJRZsBKFMqfNhDAwBgIABadXQADSoM8EKhFAIpPJlORNLRAJOmPZViSY2JWDhCJsSOptPR1oZF1QLLZuLto0qtx5fI4AqFIpAYolUpl/nlrsVIGVqo4mogAFEYI0YEQUDxvPYeBAAAYqtCliBgFD2T7APDcVhAA is slightly closer to the original

[Eric Wieser]

If you use #backticks those links are generated automatically

[Robin Arnez]

Matthew Jasper schrieb:

Reduced from https://github.com/leanprover-community/mathlib4/blob/0c08ce96d5d3380690ac7ca205fe21c06e049e3e/Mathlib/Algebra/AddConstMap/Basic.lean#L292

def OrderDual (α : Type _) : Type _ :=
  α

class MyAdd (G : Type _) where
  my_add : G → G → G

instance {α : Type _} [h : MyAdd α] : MyAdd (OrderDual α) := h

variable (G : Type _) [MyAdd G]

example : (inferInstanceAs (MyAdd G)) = (inferInstanceAs (MyAdd (OrderDual G))) := by
  with_reducible_and_instances rfl  -- OK

example : (inferInstanceAs (MyAdd G)).my_add = (inferInstanceAs (MyAdd (OrderDual G))).my_add := by
  with_reducible_and_instances rfl  -- Error Tactic `rfl` failed:

and

def OrderDual (α : Type _) : Type _ :=
  α

class MyAdd (G : Type _) where
  add : G → G → G

class Monoid (G : Type _) extends MyAdd G where
  zero : G

class AddInv (G : Type _) extends MyAdd G where
  inv : G → G

class Group (G: Type _) extends Monoid G, AddInv G

instance {α : Type _} [h : Group α] : Group (OrderDual α) := h

variable (G : Type _) [Group G]

example : (inferInstanceAs (Group G)).toMonoid = (inferInstanceAs (Group (OrderDual G))).toMonoid := by
  with_reducible_and_instances rfl  -- OK

example : (inferInstanceAs (Group G)).toAddInv = (inferInstanceAs (Group (OrderDual G))).toAddInv := by
  with_reducible_and_instances rfl  -- Error Tactic `rfl` failed:

(you can click the button in the top-right of the code blocks to go directly to live lean)

[Eric Wieser]

Those statements look type incorrect to me

[Matthew Jasper]

This is closer to what's in Mathlib:

def OrderDual (α : Type _) : Type _ :=
  α

class MyAdd (G : Type _) where
  add : G → G → G

class Monoid (G : Type _) extends MyAdd G where
  zero : G

class AddInv (G : Type _) extends MyAdd G where
  inv : G → G

class Group (G: Type _) extends Monoid G, AddInv G

instance {α : Type _} [h : Monoid α] : Monoid (OrderDual α) := h
instance {α : Type _} [h : AddInv α] : AddInv (OrderDual α) := h
instance {α : Type _} [h : Group α] : Group (OrderDual α) := h

variable (G : Type _) [Group G]

example : (inferInstanceAs (Monoid (OrderDual G))) = (inferInstanceAs (Group (OrderDual G))).toMonoid := by
  with_reducible_and_instances rfl  -- OK

example : (inferInstanceAs (AddInv (OrderDual G))) = (inferInstanceAs (Group (OrderDual G))).toAddInv := by
  with_reducible_and_instances rfl  -- Error Tactic `rfl` failed:

[Matthew Jasper]

I think that this can be fixed on the instance side

[Eric Wieser]

Yes, those instances are indeed slightly illegal, and it's fair game for Lean to tell us not to do what we do there

[Christian Merten]

On latest mathlib, with backward.isDefEq.respectTransparency true the following fails:

import Mathlib

example {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A]
    [Algebra S A] (f : R →+* S) :
    (Algebra.compHom A f).toModule = Module.compHom A f := by
  with_reducible_and_instances rfl

I am proposing a fix in #35739. Is this correct behaviour of the new mechanism and is this fix what we should be doing?

[Eric Wieser]

I think probably docs#SMul.comp should be marked instance_reducible oh, it's already reducible?

[Eric Wieser]

docs#Algebra.compHom should probably also switch from being an abbrev to @[instance_reducible] def, though this makes it less reducible not more reducible so would only help performance

[Christian Merten]

So __ := SMul.comp A f does not work, but __ := Module.compHom A f works, I believe. Let's wait for CI to confirm it.

[Weiyi Wang]

I'd like to test my projects against 4.29 rc2, but it looks like mathlib has not tagged a release yet. Should I expect that soon, or I need to rebuild mathlib on my own?

[Weiyi Wang]

Actually I am not exactly sure why the cache didn't work... my lake-manifest shows mathlib is on the latest commit 2d6247196524215d9beb18820e09d6bd5537bf8e, which should have built with rc2 tool chain https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain#L1. And obviously I have updated my toolchain to rc2 as well

[Matthew Jasper]

Is it expected that rw might now need more help inferring parameters? For example:

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
index ebc85333c27..7f1ffd32a6e 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@@ -487,13 +487,12 @@ theorem prod_extend_by_one [DecidableEq ι] (s : Finset ι) (f : ι → M) :
     ∏ i ∈ s, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i :=
   (prod_congr rfl) fun _i hi => if_pos hi

-set_option backward.isDefEq.respectTransparency false in
 /-- Also see `Finset.prod_ite_mem_eq` -/
 @[to_additive /-- Also see `Finset.sum_ite_mem_eq` -/]
 theorem prod_eq_prod_extend (f : s → M) : ∏ x, f x = ∏ x ∈ s, Subtype.val.extend f 1 x := by
   rw [univ_eq_attach, ← Finset.prod_attach s]
   congr with ⟨x, hx⟩
-  rw [Subtype.val_injective.extend_apply]
+  rw [Subtype.val_injective.extend_apply f 1 ⟨x, hx⟩]

 @[to_additive]
 theorem prod_bij_ne_one {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M}

[Weiyi Wang]

I have got some more examples of breakage. This one I believe already existed in rc1 and isn't fixed in rc2. I am currently just posting "reasonable use of Mathlib that breaks in my opinion", and haven't minimized it without mathlib yet. I can help minimize after collecting all the examples

1. SetLike.mem_coe / Multiset.mem_toFinset / Polynomial.mem_roots' doesn't trigger in simp Multiset.mem_toFinset simp_rw doesn't work (sometimes)

import Mathlib

--set_option backward.isDefEq.respectTransparency false

example (s : Multiset ℕ) (a : ℕ) (f : ℕ → ℕ) (h : a ∈ f '' s.toFinset) : ∃ x ∈ s, f x = a := by
  rw [Set.mem_image] at h
  simp_rw [SetLike.mem_coe] at h
  simp_rw [Multiset.mem_toFinset] at h -- error
  exact h

example (s : Multiset ℕ) (a : ℕ) (h : a ∈ s.toFinset) : a ∈ s := by
  simp_rw [Multiset.mem_toFinset] at h -- this is fine
  exact h

[Weiyi Wang]

hmm hold on, my original example of sub_nonneg is still broken?

2. Mathlib's sub_nonneg is still not very usable
This one is still not working

import Mathlib

-- set_option backward.isDefEq.respectTransparency false -- uncomment this to remove error below

example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by simp --error
example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg] -- error
example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := sub_nonneg -- ok

But my previous mathlib-free example does start working, so something in between is still broken...

--set_option backward.isDefEq.respectTransparency false

class AddZero' (M : Type u_2) extends Zero M, Add M where

class AddMonoid' (M : Type u) extends Add M, AddZero' M where

instance : AddZero' Int where
instance : AddMonoid' Int where

theorem sub_nonneg' {α : Type u} [AddMonoid' α] [Sub α] [LE α] {a b : α} :
  0 ≤ a - b ↔ b ≤ a := sorry

example (a b : Int) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg'] -- This one works now

[Matthew Jasper]

import Mathlib

example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg] -- error
example (a b : ℝ) : 0 ≤ a - b ↔ b ≤ a := by rw [sub_nonneg (a := a)] -- ok

[Weiyi Wang]

3. Submodule is not Free

import Mathlib

--set_option backward.isDefEq.respectTransparency false in
instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} : Module.Free ℝ l := inferInstance

-- It should go through this instance, but still error
--set_option backward.isDefEq.respectTransparency false in
instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} : Module.Free ℝ l := Module.Free.of_divisionRing ℝ l

[Weiyi Wang]

4. Something about submodule used as a module is broken

import Mathlib

--set_option backward.isDefEq.respectTransparency false

example {V: Type} [AddCommGroup V] [Module ℝ V] (p : Submodule ℝ V) (hp : Module.finrank ℝ ↥p = 1) (d : ↥p) (hd : d ≠ 0) : ℝ ∙ d = ⊤ := by
  /-
  Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Eq ℕ (Module.finrank ?m.28 ↥p) 1
  in the target expression
  @Eq ℕ (Module.finrank ℝ ↥p) 1
  -/
  rw [finrank_eq_one_iff_of_nonzero d hd] at hp -- error
  exact hp

example {V: Type} [AddCommGroup V] [Module ℝ V] (p : Submodule ℝ V) (hp : Module.finrank ℝ ↥p = 1) (d : ↥p) (hd : d ≠ 0) : ℝ ∙ d = ⊤ := by
  let : Module ℝ p := inferInstance
  /-
  failed to synthesize instance of type class
  Module ℝ ↥p
  Even though I have just synthesized above
  -/
  rw [finrank_eq_one_iff_of_nonzero d hd (K := ℝ) (V := p) ] at hp
  exact hp

example {V : Type} [AddCommGroup V] [Module ℝ V] (hp : Module.finrank ℝ V = 1) (d : V) (hd : d ≠ 0) : ℝ ∙ d = ⊤ := by
  rw [finrank_eq_one_iff_of_nonzero d hd] at hp -- This one is fine
  exact hp

[Weiyi Wang]

5. fail to rewrite with Set.disjoint_singleton_right

import Mathlib

--set_option backward.isDefEq.respectTransparency false
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  /-
Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ?m.11) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot ?m.12
    {?m.13}
in the target expression
  @Disjoint (Set ℕ) ChainCompletePartialOrder.instOfCompleteLattice.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}
-/
  rw [Set.disjoint_singleton_right]
  exact ha

example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  /-
Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ℕ) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot s {a}
in the target expression
  @Disjoint (Set ℕ) ChainCompletePartialOrder.instOfCompleteLattice.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}
-/
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

[Weiyi Wang]

These are all breakage in one of my project. Meanwhile rc1->rc2 did fix 4 breakage, so still a great progress!

I have another project with even more problem, but that was written in my early days and is full of defeq abuse, so probably less valuable to investigate. Let me try working on minimizing these 5 examples instead

[Weiyi Wang]

(I am editing my post above with more minimized examples)

[Matthew Jasper]

1 might be that SetLike.instMembership and Finset.instMembership are not reducible def-eq

[Eric Wieser]

5 reproduces with just import Mathlib.Order.CompleteLattice.Defs

[Weiyi Wang]

Updated 1. with a more focused example. Indeed something about Multiset.mem_toFinset doesn't work well

[Eric Wieser]

5 looks most likely to be a lean issue to me

[Kim Morrison]

Eric Wieser said:

Kim Morrison said:

I'm not sure what "half of these" is referring to.

"these" referred to backward.isDefEq.respectTransparency false lines.

Obviously...? Which "half"?

[Kim Morrison]

Jeremy Tan said:

#35718 removes eight instances of the option. If you can remove some more, please add them as reviews to #35718

No need to add things, let's just have many PRs.

[Kim Morrison]

Weiyi Wang said:

I'd like to test my projects against 4.29 rc2, but it looks like mathlib has not tagged a release yet. Should I expect that soon, or I need to rebuild mathlib on my own?

The tag is in place now.

@Weiyi Wang, while I'm very pleased you're trying out v4.29.0-rc2 in your projects, since you've already given us some great feedback, I do just want to point out to any interested bystanders that the current general advice remains the same: downstream projects should delay bumping their Mathlib dependency to v4.29.0-rcK, unless they are consciously signing up to help resolve this defeq issues! :-)

[Jeremy Tan]

Yes, how do we solve these defeq issues?

[Jeremy Tan]

The more you suffix your messages with :-) the less people will be willing to help, IMO

[Kim Morrison]

It would be great to get a minimization of 5. above and the sub_nonneg issue. So far I think these are the most likely to indicate underlying problems in lean4, while most of the rest above look like defeq abuse at a quick look.

[Eric Wieser]

I think 4 might be symptomatic of a place where Lean is behaving correctly but there is no easy solution without redesigning the SetLike machinery, but I'd be hesitant to investigate it before solving 5

[Eric Wieser]

I meant "more than half of the additions of backwards compatibility flag set_options were the fault of Lean itself"

[Kim Morrison]

Yes, but that's rather unhelpful without pointing to which half you mean. :-)

[Jeremy Tan]

Which of my changes in #35718 are good to go for now?

[Kim Morrison]

re: 5, it's super useful if examples like this can be written as:

import Mathlib

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ?m.11) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot ?m.12
    {?m.13}
in the target expression
  @Disjoint (Set ℕ) ChainCompletePartialOrder.instOfCompleteLattice.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}

s : Set ℕ
a : ℕ
ha : a ∉ s
⊢ Disjoint s {a}
-/
#guard_msgs in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right]
  exact ha

set_option backward.isDefEq.respectTransparency false in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right]
  exact ha

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ℕ) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot s {a}
in the target expression
  @Disjoint (Set ℕ) ChainCompletePartialOrder.instOfCompleteLattice.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}

s : Set ℕ
a : ℕ
ha : a ∉ s
⊢ Disjoint s {a}
-/
#guard_msgs in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

set_option backward.isDefEq.respectTransparency false in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

(This is the "advanced" section of #mwe. The idea that we always use #guard_msgs to capture messages, and just repeat statements with and without options rather than having comments instructing the reader to do something. It's essential that examples are machine checkable so we can use lean-minimizer to reduce them.)

[Kim Morrison]

Oops, I forgot my own instructions: and further one should use set_option pp.mvars.anonymous true to make those #guard_msgs stable!

[Kim Morrison]

import Mathlib

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ?_) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot ?_ {?_}
in the target expression
  @Disjoint (Set ℕ) ChainCompletePartialOrder.instOfCompleteLattice.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}

s : Set ℕ
a : ℕ
ha : a ∉ s
⊢ Disjoint s {a}
-/
#guard_msgs in
set_option pp.mvars.anonymous false in
set_option backward.isDefEq.respectTransparency true in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right]
  exact ha

set_option backward.isDefEq.respectTransparency false in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right]
  exact ha

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ℕ) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot s {a}
in the target expression
  @Disjoint (Set ℕ) ChainCompletePartialOrder.instOfCompleteLattice.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}

s : Set ℕ
a : ℕ
ha : a ∉ s
⊢ Disjoint s {a}
-/
#guard_msgs in
set_option pp.mvars.anonymous false in
set_option backward.isDefEq.respectTransparency true in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

set_option backward.isDefEq.respectTransparency false in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

[Eric Wieser]

Kim Morrison said:

Yes, but that's rather unhelpful without pointing to which half you mean. :-)

My claim is "of the X set_options we added, I expect an unspecified >0.5x to become no-ops once the Lean issues in this thread are fixed", with the intended meaning "resolving conflicts will become twice as easy if you wait" and possibly "these local options are causing more harm in churn than benefit", though it's difficult for me to factor in the hidden cost of testing changes Lean if they were entirely removed on master, which I'm sure you have a clearer picture of

[Eric Wieser]

I could also see a strategy along the lines of "keep a random 5% of files with the new behavior enabled until we track down all the low hanging fruit", which would minimize the interference with open and new PRs, while still letting you track what breaks against the latest mathliv

[Kim Morrison]

@Weiyi Wang's example 5 allows reducing the imports to

module
import Mathlib.Data.Set.BooleanAlgebra
import Mathlib.Order.OmegaCompletePartialOrder

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ?_) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot ?_ {?_}
in the target expression
  @Disjoint (Set ℕ) CompleteLattice.instOmegaCompletePartialOrder.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}

s : Set ℕ
a : ℕ
ha : a ∉ s
⊢ Disjoint s {a}
-/
#guard_msgs in
set_option pp.mvars.anonymous false in
set_option backward.isDefEq.respectTransparency true in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right]
  exact ha

set_option backward.isDefEq.respectTransparency false in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right]
  exact ha

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  @Disjoint (Set ℕ) Set.instDistribLattice.toSemilatticeInf.toPartialOrder Set.instBoundedOrder.toOrderBot s {a}
in the target expression
  @Disjoint (Set ℕ) CompleteLattice.instOmegaCompletePartialOrder.toPartialOrder
    CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot s {a}

s : Set ℕ
a : ℕ
ha : a ∉ s
⊢ Disjoint s {a}
-/
#guard_msgs in
set_option pp.mvars.anonymous false in
set_option backward.isDefEq.respectTransparency true in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

set_option backward.isDefEq.respectTransparency false in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  rw [Set.disjoint_singleton_right (s := s) (a := a) (α := ℕ)]
  exact ha

[Kim Morrison]

(note the error messages are slightly different, but I think this is same issue)

[Kim Morrison]

Reducing the imports anywhere below

import Mathlib.Data.Set.BooleanAlgebra
import Mathlib.Order.OmegaCompletePartialOrder

causes the problem to go away.

[Kim Morrison]

The difference at the rw is that with respectTransparency false we get

oint ?m.12 {?m.13} ▼
  [] ✅️ s =?= ?m.12 ▶
  [] ✅️ {a} =?= {?m.13} ▶
  [] ✅️ Set ℕ =?= Set ℕ ▶
  [] ✅️ CompleteLattice.instOmegaCompletePartialOrder.toPartialOrder =?= Set.instDistribLattice.toSemilatticeInf.toPartialOrder ▶
  [] ✅️ CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot =?= Set.instBoundedOrder.toOrderBot ▼
    [] ✅️ CompleteBooleanAlgebra.toCompleteDistribLattice.toOrderBot =?= Set.instBoundedOrder.toOrderBot ▼
      [] ✅️ CompleteBooleanAlgebra.toCompleteDistribLattice.toBoundedOrder.2 =?= Set.instBoundedOrder.2 ▼
        [] ✅️ { toBot := Set.instBooleanAlgebra.toBot, bot_le := ⋯ } =?= { bot := ∅, bot_le := ⋯ } ▼
          [] ✅️ Set ℕ =?= Set ℕ
          [] ✅️ Set.instBooleanAlgebra.toLE =?= Set.instLE ▶
          [] ✅️ Set.instBooleanAlgebra.toBot =?= { bot := ∅ } ▼
            [] ✅️ Set.instBooleanAlgebra.6 =?= { bot := ∅ } ▼
              [] ✅️ inferInstance.toBot =?= { bot := ∅ } ▼
                [] ✅️ inferInstance.6 =?= { bot := ∅ } ▼
                  [] ✅️ Pi.instHeytingAlgebra.toBot =?= { bot := ∅ } ▼
                    [] ✅️ Pi.instHeytingAlgebra.toOrderBot.1 =?= { bot := ∅ } ▼
                      [] ✅️ Pi.instBotForall =?= { bot := ∅ } ▼
                        [] ✅️ { bot := fun x ↦ ⊥ } =?= { bot := ∅ } ▼
                          [] ✅️ fun x ↦ ⊥ =?= ∅ ▶
                          [] ✅️ (i : ℕ) → (fun a ↦ Prop) i =?= Set ℕ ▼
                            [] ✅️ (i : ℕ) → (fun a ↦ Prop) i =?= ℕ → Prop ▼
                              [] ✅️ ℕ =?= ℕ
                              [] ✅️ (fun a ↦ Prop) i =?= Prop ▼
                                [] ✅️ Prop =?= Prop

while with respectTransparency true we get

[Meta.isDefEq] ❌️ Disjoint s {a} =?= Disjoint ?m.12 {?m.13} ▼
  [] ✅️ s =?= ?m.12 ▶
  [] ✅️ {a} =?= {?m.13} ▶
  [] ✅️ Set ℕ =?= Set ℕ ▶
  [] ✅️ CompleteLattice.instOmegaCompletePartialOrder.toPartialOrder =?= Set.instDistribLattice.toSemilatticeInf.toPartialOrder ▶
  [] ❌️ CompleteBooleanAlgebra.toCompleteDistribLattice.toHeytingAlgebra.toOrderBot =?= Set.instBoundedOrder.toOrderBot ▼
    [] ❌️ CompleteBooleanAlgebra.toCompleteDistribLattice.toOrderBot =?= Set.instBoundedOrder.toOrderBot ▼
      [] ❌️ CompleteBooleanAlgebra.toCompleteDistribLattice.toBoundedOrder.2 =?= Set.instBoundedOrder.2 ▼
        [] ❌️ { toBot := Set.instBooleanAlgebra.toBot, bot_le := ⋯ } =?= { bot := ∅, bot_le := ⋯ } ▼
          [] ✅️ Set ℕ =?= Set ℕ
          [] ✅️ Set.instBooleanAlgebra.toLE =?= Set.instLE ▶
          [] ❌️ Set.instBooleanAlgebra.toBot =?= { bot := ∅ } ▼
            [] ❌️ Set.instBooleanAlgebra.6 =?= { bot := ∅ } ▼
              [] ❌️ inferInstance.toBot =?= { bot := ∅ } ▼
                [] ❌️ inferInstance.6 =?= { bot := ∅ } ▼
                  [] ❌️ Pi.instHeytingAlgebra.toBot =?= { bot := ∅ } ▼
                    [] ❌️ Pi.instHeytingAlgebra.toOrderBot.1 =?= { bot := ∅ } ▼
                      [] ❌️ Pi.instBotForall =?= { bot := ∅ } ▼
                        [] ❌️ { bot := fun x ↦ ⊥ } =?= { bot := ∅ } ▼
                          [] ✅️ fun x ↦ ⊥ =?= ∅ ▶
                          [] ❌️ (i : ℕ) → (fun a ↦ Prop) i =?= Set ℕ ▼
                            [onFailure] ❌️ (i : ℕ) → (fun a ↦ Prop) i =?= Set ℕ
                          [onFailure] ❌️ { bot := fun x ↦ ⊥ } =?= { bot := ∅ }
                          [onFailure] ❌️ { bot := fun x ↦ ⊥ } =?= { bot := ∅ }
          [onFailure] ❌️ { toBot := Set.instBooleanAlgebra.toBot, bot_le := ⋯ } =?= { bot := ∅, bot_le := ⋯ }
          [onFailure] ❌️ { toBot := Set.instBooleanAlgebra.toBot, bot_le := ⋯ } =?= { bot := ∅, bot_le := ⋯ }
  [onFailure] ❌️ Disjoint s {a} =?= Disjoint ?m.12 {?m.13}
  [onFailure] ❌️ Disjoint s {a} =?= Disjoint ?m.12 {?m.13}

[Yury G. Kudryashov]

Does it mean that Set should become a structure?

[Kim Morrison]

I think it means:

universe u
unif_hint set_hint (α β : Type u) where
  α ≟ β ⊢
  ((i : α) → Prop) ≟ Set β

[Kim Morrison]

this at least solves the problem locally.

[Kim Morrison]

But that is just a first guess, we need to explore a bit here.

[Kim Morrison]

(and there may still need to be a lean fix here)

[Kim Morrison]

Yury G. Kudryashov said:

Does it mean that Set should become a structure?

But replacing "it" with "type hygiene", I think I might agree with your statement! :-)

[Eric Wieser]

I think this indicates we should pull the lattice structure through setOf?

[Kim Morrison]

set_option allowUnsafeReducibility true in
attribute [implicit_reducible] Set

also solves the problem here.

[Eric Wieser]

My provisional apologies for declaring this one as probably Lean's fault

[Kim Morrison]

Just for clarity, I am at this point satisfied that this issue is on the Mathlib side, and will hope that someone here can try out adding setOf in the right places?

[Kim Morrison]

I am going to assume that this issue will come up again and again, and try to write a tactic combinator that runs something under trace.Meta.isDefEq, with and without respectTransparency, and gives a useful diff.

[Kim Morrison]

(I think this is more effective use of my time than the actual Mathlib fixes for now.)

[Weiyi Wang]

3 and 4 look like the same kind of the problem. For some reason, Module instance provided by docs#Submodule.module is not found
For example, if I do

import Mathlib

set_option trace.Meta.synthInstance true

--set_option backward.isDefEq.respectTransparency false in
instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} : Module.Free ℝ l := Module.Free.of_divisionRing ℝ l

This gives

[Meta.synthInstance] ✅️ DivisionRing ℝ ▶
[Meta.synthInstance] ✅️ AddCommGroup ↥l ▶
[Meta.synthInstance] ❌️ Module ℝ ↥l ▼
  [] new goal Module ℝ ↥l ▶
  [] ❌️ apply inst✝ to Module ℝ ↥l ▶
  [] ❌️ apply @Submodule.module to Module ℝ ↥l ▼
    [tryResolve] ❌️ Module ℝ ↥l ≟ Module ?m.13 ↥?m.18

But with old behavior, it is

[Meta.synthInstance] ✅️ DivisionRing ℝ ▶
[Meta.synthInstance] ✅️ AddCommGroup ↥l ▶
[Meta.synthInstance] ✅️ Module ℝ ↥l ▼
  [] new goal Module ℝ ↥l ▶
  [] ❌️ apply inst✝ to Module ℝ ↥l ▶
  [] ✅️ apply @Submodule.module to Module ℝ ↥l ▼
    [tryResolve] ✅️ Module ℝ ↥l ≟ Module ℝ ↥l
    [answer] ✅️ Module ℝ ↥l
  [] result l.module

[Weiyi Wang]

On the line [tryResolve] ❌️ Module ℝ ↥l ≟ Module ?m.13 ↥?m.18,
the full type on the left is @Module ℝ (↥l) DivisionRing.toDivisionSemiring.toSemiring l.addCommGroup.toAddCommMonoid
the full type on the right is @Module ?m.13 ↥?m.19 ?m.20 (Submodule.addCommMonoid ?m.19) : Type (max ?u.1820 ?u.1822)

[Kim Morrison]

import Mathlib.Data.Set.BooleanAlgebra
import Mathlib.Order.OmegaCompletePartialOrder
import Mathlib.Tactic.CheckDefEqAbuse

/--
warning: check_defeq_abuse: tactic fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
The following isDefEq checks are the root causes of the failure:
  ❌️ (i : ℕ) → (fun a => Prop) i =?= Set ℕ
-/
#guard_msgs in
example (s : Set ℕ) (a : ℕ) (ha : a ∉ s) : Disjoint s {a} := by
  check_defeq_abuse rw [Set.disjoint_singleton_right]
  exact ha

/-- info: check_defeq_abuse: tactic succeeds with `backward.isDefEq.respectTransparency true`. No abuse detected. -/
#guard_msgs in
example (a b : ℕ) (h : a = b) : a = b := by
  check_defeq_abuse rw [h]

[Kim Morrison]

I'll make a PR shortly!

[Kim Morrison]

#35750

[Weiyi Wang]

Weiyi Wang said:

On the line [tryResolve] ❌️ Module ℝ ↥l ≟ Module ?m.13 ↥?m.18,
the full type on the left is @Module ℝ (↥l) DivisionRing.toDivisionSemiring.toSemiring l.addCommGroup.toAddCommMonoid
the full type on the right is @Module ?m.13 ↥?m.19 ?m.20 (Submodule.addCommMonoid ?m.19) : Type (max ?u.1820 ?u.1822)

In comparison, the full type for the happy case is

[tryResolve] ✅️ Module ℝ ↥l ≟ Module ℝ ↥l
left: @Module ℝ (↥l) DivisionRing.toDivisionSemiring.toSemiring l.addCommGroup.toAddCommMonoid
right: @Module ℝ (↥l) Real.semiring l.addCommMonoid

So I guess Semiring parameter and/or the AddCommMonoid are considered defeq abuse?

[Kim Morrison]

Well, somewhere in there there is some def being using that needs an @[implicit_reducible] attribute.

[Yury G. Kudryashov]

Do you mean @[instance_reducible]?

[Kim Morrison]

Oh, sorry, it has been renamed in rc2, although instance_reducible is still available as a synonym (not yet deprecated, oops).

[Yury G. Kudryashov]

Thanks, I've missed that.

[Yury G. Kudryashov]

BTW, could you please have a look at #35286? I've moved stuff that changes more than defeq abuse to #35351

[Johan Commelin]

Borsed #35351

[Johan Commelin]

#35286 looks good to me

[Kim Morrison]

Kim Morrison said:

#35750

I'm adding some more features, including a command mode that helps with instance and variables problems. But I have to stop for this evening, so I'll mark the PR as draft until I get back to it.

[Kim Morrison]

In the meantime, in would be incredibly useful to have Mathlib free minimizations of the Set/Lattice problem, and the Module problem, so that we can leave these in place as test cases for #check_defeq_abuse even once the current underlying problems are solved.

[Weiyi Wang]

(I am slowly learning reading the trace...)
The defeq failure of 3./4. happens at the AddCommGroup / AddCommMonoid part
(l : Submodule ℝ V in the following)

        [] ❌️ l.addCommGroup.toAddCommMonoid =?= l.addCommMonoid ▼
          [] ❌️ { toAddMonoid := l.addCommGroup.toAddMonoid, add_comm := ⋯ } =?= l.addCommMonoid ▼
            [] ❌️ { toAddMonoid := l.addCommGroup.toAddMonoid, add_comm := ⋯ } =?= l.toAddCommMonoid ▼
              [] ❌️ { toAddMonoid := l.addCommGroup.toAddMonoid, add_comm := ⋯ } =?= AddSubmonoidClass.toAddCommMonoid l.toAddSubmonoid ▼
                [] ❌️ { toAddMonoid := l.addCommGroup.toAddMonoid,
                      add_comm :=
                        ⋯ } =?= { toAddMonoid := AddSubmonoidClass.toAddMonoid l.toAddSubmonoid, add_comm := ⋯ } ▼
                  [] ✅️ ↥l =?= ↥l.toAddSubmonoid ▶
                  [] ❌️ l.addCommGroup.toAddMonoid =?= AddSubmonoidClass.toAddMonoid l.toAddSubmonoid ▼
                    [] ❌️ AddSubmonoidClass.toAddMonoid l.toAddSubgroup =?= AddSubmonoidClass.toAddMonoid l.toAddSubmonoid ▼
                      [] ❌️ l.toAddSubgroup =?= l.toAddSubmonoid ▶
                      [] ❌️ { toAddSemigroup := AddMemClass.toAddSemigroup l.toAddSubgroup, toZero := ZeroMemClass.zero l.toAddSubgroup,
                            zero_add := ⋯, add_zero := ⋯, nsmul := fun n x => n • x, nsmul_zero := ⋯,
                            nsmul_succ :=
                              ⋯ } =?= { toAddSemigroup := AddMemClass.toAddSemigroup l.toAddSubmonoid,
                            toZero := ZeroMemClass.zero l.toAddSubmonoid, zero_add := ⋯, add_zero := ⋯,
                            nsmul := fun n x => n • x, nsmul_zero := ⋯, nsmul_succ := ⋯ } ▶
                  [onFailure] ❌️ { toAddMonoid := l.addCommGroup.toAddMonoid,
                        add_comm :=
                          ⋯ } =?= { toAddMonoid := AddSubmonoidClass.toAddMonoid l.toAddSubmonoid, add_comm := ⋯ }
                  [onFailure] ❌️ { toAddMonoid := l.addCommGroup.toAddMonoid,
                        add_comm :=
                          ⋯ } =?= { toAddMonoid := AddSubmonoidClass.toAddMonoid l.toAddSubmonoid, add_comm := ⋯ }

[Weiyi Wang]

It looks like also a SetLike behavior difference after all?

error case:
                        [] ❌️ fun n x => n • x =?= fun n x => n • x ▼
                          [] ✅️ ℕ =?= ℕ
                          [] ❌️ ↥l.toAddSubgroup =?= ↥l.toAddSubmonoid ▼
                            [] ❌️ fun x => x ∈ l.toAddSubgroup =?= fun x => x ∈ l.toAddSubmonoid ▼
                              [] ✅️ V =?= V
                              [] ❌️ x ∈ l.toAddSubgroup =?= x ∈ l.toAddSubmonoid ▼
                                [] ❌️ l.toAddSubgroup =?= l.toAddSubmonoid
                                [onFailure] ❌️ x ∈ l.toAddSubgroup =?= x ∈ l.toAddSubmonoid
                                [] ❌️ x ∈ ↑l.toAddSubgroup =?= x ∈ ↑l.toAddSubmonoid ▼
                                  [] ❌️ ↑l.toAddSubgroup =?= ↑l.toAddSubmonoid ▼
                                    [] ❌️ l.toAddSubgroup =?= l.toAddSubmonoid
                                    [onFailure] ❌️ ↑l.toAddSubgroup =?= ↑l.toAddSubmonoid
                                    [] ❌️ l.toAddSubgroup.carrier =?= l.carrier ▼
                                      [] ❌️ l.toAddSubgroup.toAddSubsemigroup.1 =?= l.toAddSubsemigroup.1 ▼
                                        [] ❌️ l.toAddSubgroup.toAddSubsemigroup =?= l.toAddSubsemigroup ▼
                                          [] ❌️ l.toAddSubgroup.toAddSubmonoid.1 =?= l.toAddSubmonoid.1 ▼
                                            [] ❌️ l.toAddSubgroup.toAddSubmonoid =?= l.toAddSubmonoid ▼
                                              [] ❌️ l.toAddSubgroup.1 =?= l.1 ▼
                                                [onFailure] ❌️ l.toAddSubgroup.1 =?= l.1

happy case:
                        [] ✅️ fun n x => n • x =?= fun n x => n • x ▼
                          [] ✅️ ℕ =?= ℕ
                          [] ✅️ ↥l.toAddSubgroup =?= ↥l.toAddSubmonoid ▼
                            [] ✅️ fun x => x ∈ l.toAddSubgroup =?= fun x => x ∈ l.toAddSubmonoid ▼
                              [] ✅️ V =?= V
                              [] ✅️ x ∈ l.toAddSubgroup =?= x ∈ l.toAddSubmonoid ▼
                                [] ✅️ SetLike.instMembership.1 l.toAddSubgroup x =?= SetLike.instMembership.1 l.toAddSubmonoid x ▼
                                  [] ✅️ x ∈ ↑l.toAddSubgroup =?= x ∈ ↑l.toAddSubmonoid ▼
                                    [] ✅️ Set.instMembership.1 (↑l.toAddSubgroup) x =?= Set.instMembership.1 (↑l.toAddSubmonoid) x ▼
                                      [] ✅️ (↑l.toAddSubgroup).Mem x =?= (↑l.toAddSubmonoid).Mem x ▼
                                        [] ✅️ ↑l.toAddSubgroup x =?= ↑l.toAddSubmonoid x ▼
                                          [] ✅️ AddSubgroup.instSetLike.1 l.toAddSubgroup x =?= AddSubmonoid.instSetLike.1 l.toAddSubmonoid x ▼
                                            [] ✅️ l.toAddSubgroup.carrier x =?= l.carrier x ▼
                                              [] ✅️ l.toAddSubgroup.toAddSubsemigroup.1 x =?= l.toAddSubsemigroup.1 x ▼
                                                [] ✅️ l.toAddSubgroup.toAddSubsemigroup.1 =?= l.toAddSubsemigroup.1 ▼
                                                  [] ✅️ l.toAddSubgroup.toAddSubsemigroup =?= l.toAddSubsemigroup ▼
                                                    [] ✅️ l.toAddSubgroup.toAddSubmonoid.1 =?= l.toAddSubmonoid.1 ▼
                                                      [] ✅️ l.toAddSubgroup.toAddSubmonoid =?= l.toAddSubmonoid ▼
                                                        [] ✅️ l.toAddSubgroup.1 =?= l.1 ▼
                                                          [] ✅️ l.toAddSubmonoid =?= l.1 ▼
                                                            [] ✅️ l.1 =?= l.1
                                                [] ✅️ x =?= x

[Yury G. Kudryashov]

I've created a branch with structure Set, then cherry-picked some of fixes to uncovered defeq abuses to #35752 UPD: I'm fixing compile errors

[Yury G. Kudryashov]

#35752 builds locally

[Kim Morrison]

The Module failures above are correctly detected by #defeq_abuse, which says:

/-
warning: #defeq_abuse: command fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
The following synthesis applications fail due to transparency:
  ❌️ apply @Submodule.module to Module ℝ ↥_fvar.1076
    ❌️ l.toAddSubgroup =?= l.1
    ❌️ l.toAddSubgroup =?= l.toAddSubmonoid
    ❌️ l.toAddSubgroup.1 =?= l.1
    ❌️ ↑l.toAddSubgroup =?= ↑l.toAddSubmonoid
-/
#guard_msgs (drop warning) in
set_option pp.all true in
#defeq_abuse in
instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} :
    Module.Free ℝ l := Module.Free.of_divisionRing ℝ l

and indeed putting @[implicit_reducible] on Submodule.toAddSubgroup resolves the problem.

[Kim Morrison]

Is there some way we can identify quickly all of these "pseudo parents" in mathlib, and put @[implicit_reducible] on them all?

[Kim Morrison]

I guess we want a metaprogram that finds all def toX : <a class>?

[Matthew Jasper]

Somewhat reduced version of 2.

import Mathlib.Algebra.Order.Group.Unbundled.Basic
import Mathlib.Algebra.Order.Group.Int

theorem result.{u} : ∀ {α : Type u} [inst : AddGroup α] (a : α),
  0 = a ↔ a = a + a := sorry

/--
error: `simp` made no progress
-/
#guard_msgs in
theorem t1 (a : ℤ) : 0 = a ↔ a = a + a := by simp only [result]
/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 = ?a
in the target expression
  0 = a ↔ a = a + a

a : ℤ
⊢ 0 = a ↔ a = a + a
-/
#guard_msgs in
example (a : ℤ) : 0 = a ↔ a = a + a := by rw [result]

/--
error: typeclass instance problem is stuck
  AddGroup ?_

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `AddGroup` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs in
set_option pp.mvars.anonymous false in
example (a : ℤ) : 0 = a ↔ a = a + a := by
  with_reducible_and_instances exact result _

example (a : ℤ) : 0 = a ↔ a = a + a := by simp only [result a]
example (a : ℤ) : 0 = a ↔ a = a + a := by rw [result a]
example (a : ℤ) : 0 = a ↔ a = a + a := by exact result _

[Kim Morrison]

Kim Morrison said:

indeed putting @[implicit_reducible] on Submodule.toAddSubgroup resolves the problem.

#35761.

I'm also running scripts/rm_set_option.py on that PR, and it is deleting many set_option backward from across Mathlib. (About 100 removed so far.)

[Kim Morrison]

Kim Morrison said:

In the meantime, in would be incredibly useful to have Mathlib free minimizations of the Set/Lattice problem, and the Module problem, so that we can leave these in place as test cases for #check_defeq_abuse even once the current underlying problems are solved.

Claude and I have found Mathlib free minimization of these two problems, and installed them as test cases in th #defeq_abuse tactic, at #35750.

This tactic seems really useful, and is a lovely example of Claude writing a metaprogram! It understood perfectly how to simultaneously read a Meta.isDefEq and Meta.synthInstance trace log, and reports the failing isDefEq checks immediately prior to the first divergence between the synthInstance traces with/without respectTransparency. This would have been a nightmare to do by hand, particularly because the logs are not very well structured objects, and we find ourselves string matching on emojis to find our way through them.

[Kim Morrison]

Matthew Jasper said:

Somewhat reduced version of 2.

import Mathlib.Algebra.Order.Group.Unbundled.Basic
import Mathlib.Algebra.Order.Group.Int

theorem result.{u} : ∀ {α : Type u} [inst : AddGroup α] (a : α),
  0 = a ↔ a = a + a := sorry

/--
error: `simp` made no progress
-/
#guard_msgs in
theorem t1 (a : ℤ) : 0 = a ↔ a = a + a := by simp only [result]
/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 = ?a
in the target expression
  0 = a ↔ a = a + a

a : ℤ
⊢ 0 = a ↔ a = a + a
-/
#guard_msgs in
example (a : ℤ) : 0 = a ↔ a = a + a := by rw [result]

/--
error: typeclass instance problem is stuck
  AddGroup ?_

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `AddGroup` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs in
set_option pp.mvars.anonymous false in
example (a : ℤ) : 0 = a ↔ a = a + a := by
  with_reducible_and_instances exact result _

example (a : ℤ) : 0 = a ↔ a = a + a := by simp only [result a]
example (a : ℤ) : 0 = a ↔ a = a + a := by rw [result a]
example (a : ℤ) : 0 = a ↔ a = a + a := by exact result _

Thanks Jasper, this example is a good one. I'm not sure what the fix is yet! It comes down to a defeq failure between 0 from Zero.zero and 0 from Int.oftNat.

[Kim Morrison]

Kim Morrison said:

I guess we want a metaprogram that finds all def toX : <a class>?

https://gist.github.com/kim-em/8f01bafd5e19c0d45c9e878a4c1deae5

Spot checking, to me these all look like they need @[implicit_reducible]. But I haven't checked them all.

It's probably simplest to do this check as a PR...?

[Kim Morrison]

#35765

[Kim Morrison]

I'll have CI check that doesn't break anything, then measure how many set_option backward we can remove.

[Robin Arnez]

I wonder if it makes sense to add a new transparency setting specifically for instance synthesis. It seems to me like implicit_reducible is not really suited for instance synthesis. For example, do we really want to allow Nat.add a b =?= a + b during instance synthesis? While unifying implicit arguments? Sure. But when unifying instance types? I don't really think so. I'd argue that instance synthesis should really use something that can do a bit more than reducible but maybe not unfold all instances (especially not those that involve defeq abuse). That would also allow being a bit more aggressive with @[implicit_reducible], tagging Matrix, OrderDual, Set, setOf, etc. as @[implicit_reducible] without fearing that instances will be mixed up between them. In particular, we'd ideally ensure that all instances typecheck under @[implicit_reducible] (modulo proofs).

[Kim Morrison]

Kim Morrison said:

Kim Morrison said:

indeed putting @[implicit_reducible] on Submodule.toAddSubgroup resolves the problem.

#35761.

I'm also running scripts/rm_set_option.py on that PR, and it is deleting many set_option backward from across Mathlib. (About 100 removed so far.)

This removes over 600 of the set_option backward, so I think we can say this is a good change! The run isn't quite finished, so I'll commit it tomorrow with the remainder.

[Patrick Massot]

Kim Morrison said:

This tactic seems really useful, and is a lovely example of Claude writing a metaprogram! It understood perfectly how to simultaneously read a Meta.isDefEq and Meta.synthInstance trace log, and reports the failing isDefEq checks immediately prior to the first divergence between the synthInstance traces with/without respectTransparency. This would have been a nightmare to do by hand, particularly because the logs are not very well structured objects, and we find ourselves string matching on emojis to find our way through them.

This sounds like one more great example of AI enshittification: instead of working on fixing the actual issue of logs not being very well structured, you avoid the issue and push technical debt down the road.

[Weiyi Wang]

I disagree with the assertion that the log is not well structured. I was learning to read it for the first time last night and was able to grasp the idea of it quickly. The real problem that blocked my initial investigation was 1. didn't know the option to turn on trace log (documentation issue) 2. had to manually compare the before/after log (which the new script is resolving)

[Matthew Jasper]

Matthew Jasper said:

Somewhat reduced version of 2.

-- cut

With all of the dependencies removed:

class Zo (α : Type _) where
  zo : α

class Num (α : Type _) (n : Nat) where
  fromNat : α

class Gr (α : Type _) extends Zo α where
  add : α → α → α
  inv : α → α

class Sm (α : Type _) extends Zo α where
  inv : α → α

instance {α} [h: Gr α] : Sm α := { h with }

instance : Zo Int where
  zo := 0

instance {n} : Num Int n where
  fromNat := Int.ofNat n

instance {α} [Zo α] : Num α 0 where
  fromNat := Zo.zo

instance : Gr Int where
  add a b := a + b
  inv a := -a

theorem zo_eq_iff {α} [Gr α] (a : α) : Num.fromNat 0 = a ↔ a = Gr.add a a := sorry

/--
error: typeclass instance problem is stuck
  Gr ?m.10

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Gr` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs in
example (a : Int) : Num.fromNat 0 = a ↔ a = Gr.add a a := by
  with_reducible_and_instances exact zo_eq_iff _

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  Num.fromNat 0 = ?a
in the target expression
  Num.fromNat 0 = a ↔ a = Gr.add a a

a : Int
⊢ Num.fromNat 0 = a ↔ a = Gr.add a a
-/
#guard_msgs in
example (a : Int) : Num.fromNat 0 = a ↔ a = Gr.add a a := by rw [zo_eq_iff]

example (a : Int) : Num.fromNat 0 = a ↔ a = Gr.add a a := by
  with_reducible_and_instances exact zo_eq_iff a

example (a : Int) : Num.fromNat 0 = a ↔ a = Gr.add a a := by rw [zo_eq_iff a]

[Violeta Hernández]

Weiyi Wang ha dicho:

I disagree with the assertion that the log is not well structured. I was learning to read it for the first time last night and was able to grasp the idea of it quickly. The real problem that blocked my initial investigation was 1. didn't know the option to turn on trace log (documentation issue) 2. had to manually compare the before/after log (which the new script is resolving)

Maybe the correct claim is that the log is well-structured for humans but badly structured for our meta code?

[Chris Henson]

Violeta Hernández said:

Maybe the correct claim is that the log is well-structured for humans but badly structured for our meta code?

Yes, though I feel like this was clear from the context of discussing a tactic.

[Weiyi Wang]

Maybe it is because of my background, I didn't consider "structured log for machine" as a practical thing (I had this impression way before AI entered the picture) as I deal with unstructured log for job everyday

[Weiyi Wang]

The logic behind that is "you have log because you expect the unexpected. If you somehow can make it structured to capture all information, then it is expected information and it shouldn't be log in the first place"

[Yury G. Kudryashov]

#35780 is ready for review (drop Membership on Finset).

[Eric Wieser]

Should Membership.mem instead be made instance_reducible?

[Yury G. Kudryashov]

Why? Other SetLike types don't have Membership instances

[Kim Morrison]

Patrick Massot said:

This sounds like one more great example of AI enshittification: instead of working on fixing the actual issue of logs not being very well structured, you avoid the issue and push technical debt down the road.

@Patrick Massot, you are inappropriately jumping to conclusions here. Of course this discovery --- that it's hard to programmatically process these logs --- has bumped the priority of better trace logs, and I'm already thinking about it. That will of course take much longer to get right than a diagnostic script to help fix urgently problems in Mathlib, and it would be stupid to wait on better structured trace logs to get #defeq_abuse into users' hands.

[Kim Morrison]

chore: mark Submodule.toAddSubgroup @[implicit_reducible] #35761

Is ready to go. It removes ~700 occasions where we currently need set_option backward.isDefEq.respectTransparency. It then --- mysteriously --- requires three of these added in the test cases. But I think this is an improvement, and we'll of course investigate those additions later.

[Kim Morrison]

Kim Morrison said:

Kim Morrison said:

I guess we want a metaprogram that finds all def toX : <a class>?

https://gist.github.com/kim-em/8f01bafd5e19c0d45c9e878a4c1deae5

Spot checking, to me these all look like they need @[implicit_reducible]. But I haven't checked them all.

It's probably simplest to do this check as a PR...?

I tried this, and somewhat mysteriously, despite adding implicit_reducible on Submodule.toAddCommGroup allowing us to remove ~700 set_option backwards, none of the other toX : <class> definitions receiving a implicit_reducible seem to make any difference! :woman_shrugging:

I'm pretty surprised by this.

[Eric Wieser]

Kim Morrison said:

I guess we want a metaprogram that finds all def toX : <a class>?

I'm confused by this claim, docs#AddSubgroup is not a class

[Jeremy Tan]

I am really surprised that Massot, who once suspended me for talking trash in this Zulip, now does it himself

[Kim Morrison]

oh! I was confused. So indeed the def toX : <a class> was the wrong thing entirely.

[Kim Morrison]

Is there a pattern we should be looking for to automate the success of #35761?

[Jeremy Tan]

Kim Morrison said:

Is there a pattern we should be looking for to automate the success of #35761?

Run your new command on everything, log the results and analyse them

[Kim Morrison]

Jeremy Tan said:

I am really surprised that Massot, who once suspended me for talking trash in this Zulip, now does it himself

AI enshittification is a real thing, and a real thing to guard against. I'm glad Patrick raised the issue, because if we're failing somewhere to guard against it, it should be pointed out. But this wasn't such a place. :-)

[Jeremy Tan]

BTW I'm trying myself adding to Data.Set.Defs

unif_hint (α β : Type u) where
  α ≟ β ⊢ ((i : α) → Prop) ≟ Set β

and running rm_set_option.py. It has removed 65 set_options so far

[Jeremy Tan]

unif_hint has no documentation

[Yury G. Kudryashov]

I don't think that we should normalize defeq abuse instead of getting rid of it.

[Kim Morrison]

Agreed, let's only use unif_hint "in desperation".

[Jeremy Tan]

But it still points out where specific types of defeq abuses are

[Jeremy Tan]

(deleted)

[Kim Morrison]

Patrick Massot said:

This sounds like one more great example of AI enshittification: instead of working on fixing the actual issue of logs not being very well structured, you avoid the issue and push technical debt down the road.

@Patrick Massot, please see

feat: add structured TraceResult to TraceData lean#12698
feat: add Meta.synthInstance.apply trace class lean#12699

[Kim Morrison]

So far I am not finding a solution to Jasper's example besides

unif_hint (α : Type _) (n : ℕ) (inst₁ : OfNat α n) (inst₂ : OfNat α n) where ⊢
    @OfNat.ofNat α n inst₁ ≟ @OfNat.ofNat α n inst₂

which I don't think it insane, despite mere minutes ago saying that I wanted to avoid unif_hint where possible.

We could restrict this to just n=0 (possibly also n=1) since these problems are all about Zero/One.

[Eric Wieser]

What does that hint mean? I'm not a huge fan of declaring unif_hint the solution before it has any docstring explaining how to use it!

[Eric Wieser]

This is a long thread; could you link back to the example you're referring to?

[Kim Morrison]

The best summary is maybe actually the test cases for #35750.

[Matthew Jasper]

#general > backward.isDefEq.respectTransparency @ 💬 , #general > backward.isDefEq.respectTransparency @ 💬 and #general > backward.isDefEq.respectTransparency @ 💬

[Jeremy Tan]

I found a possible bug in your #defeq_abuse, at Multiset.noncommFoldr_coe. If I set set_option backward.isDefEq.respectTransparency true in on it, it errors, but running #defeq_abuse in on it gives

#defeq_abuse: command succeeds with `backward.isDefEq.respectTransparency true`. No abuse detected.

[Jeremy Tan]

image.png
image.png

[Kim Morrison]

Jeremy Tan said:

I found a possible bug in your #defeq_abuse, at Multiset.noncommFoldr_coe

Thanks, taking a look now.

[Kim Morrison]

I just want to summarize the state of things here, please let me know if we're missing anything.

• Yury's PR "chore: reduce defeq abuse #35286" is awaiting-author after some review comments from Kevin
• "chore(scripts): make rm_set_option cache opt-in via --resume #35763" is a usability improvement waiting for review
• "chore: mark Submodule.toAddSubgroup @[reducible] #35761" has gone through some review, is being benchmarked, but hopefully can be merged soon
• "feat(Tactic): add #defeq_abuse tactic combinator #35750" needs review. I've tried to factor out the general code, and it will be improved by the lean PRs lean#12698 and lean#12699 but those will take a while to land. This contains test cases showing #defeq_abuse works on most of the examples above.
• We don't have ideas for @Matthew Jasper's example except trying a unif_hint, and we need to try that out to see what else it breaks.
• Jeremy has identified a potential problem with #defeq_abuse that I will look into.
• I would love others to try out #defeq_abuse and start solving problems it reports / telling me how it goes wrong.
• At present we don't have any concrete cases where a lean4 fix is required, except possibly the OfNat issue.

[Kim Morrison]

@Jovan Gerbscheid and @Thomas Murrills, if either of you could be tempted into looking at #35750 that would be super helpful. This tool doesn't need to be perfect, it just needs to get us through this respectTransparency refactor. But I'd like to get it into master asap so people can start working on the backlog.

[Jeremy Tan]

Further possible false negatives for #defeq_abuse you may want to look into: Equiv.piFinsetUnion_left, Equiv.piFinsetUnion_right, Finset.disjoint_coe

[Robin Carlier]

Aobout unification hints to remove some of those set_option, they were also mentioned here (and the discussion contains interesting explanations of how unif_hint works and what it does) in the context of trying to find how we should approach category theory in mathlib with this new behavior of transparency.

[Kim Morrison]

Thanks @Jeremy Tan for your report about #defeq_abuse not detecting problems in Finset.disjoint_coe, etc.

It was a subtle problem -- the command needs to turn off Elab.async, or the global set_option backward false option leaks through.

It is fixed now on #35750, so I would love to have more people test it out / review it / merge it.

[Kim Morrison]

Monoid.toOne doesn't have implicit_reducible. This seems likely to be a Lean bug, requiring a rc3.

[Christian Merten]

Kim Morrison said:

I just want to summarize the state of things here, please let me know if we're missing anything.

Do you have an answer for this question I asked above?
Christian Merten said:

On latest mathlib, with backward.isDefEq.respectTransparency true the following fails:

import Mathlib

example {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A]
    [Algebra S A] (f : R →+* S) :
    (Algebra.compHom A f).toModule = Module.compHom A f := by
  with_reducible_and_instances rfl

I am proposing a fix in #35739. Is this correct behaviour of the new mechanism and is this fix what we should be doing?

[Robin Arnez]

Kim Morrison schrieb:

unif_hint (α : Type _) (n : ℕ) (inst₁ : OfNat α n) (inst₂ : OfNat α n) where ⊢
    @OfNat.ofNat α n inst₁ ≟ @OfNat.ofNat α n inst₂

Please no, I don't want to get kernel errors like this one:

unif_hint (α : Type _) (n : Nat) (inst₁ : OfNat α n) (inst₂ : OfNat α n) where ⊢
    @OfNat.ofNat α n inst₁ ≟ @OfNat.ofNat α n inst₂

/--
error: (kernel) declaration type mismatch, '_example' has type
  OfNat.ofNat 0 = OfNat.ofNat 0
but it is expected to have type
  OfNat.ofNat 0 = OfNat.ofNat 0
-/
#guard_msgs in
example : @OfNat.ofNat Int 0 _ = @OfNat.ofNat Int 0 ⟨3⟩ := by
  with_reducible eq_refl

We should probably fix lean4#8982 before we consider adding unification hints.

[Kim Morrison]

Kim Morrison said:

Monoid.toOne doesn't have implicit_reducible. This seems likely to be a Lean bug, requiring a rc3.

lean#12701 I think will fix this, but I don't want to merge yet as I don't have the #mwe I want...

[Matthew Jasper]

I think that the OfNat issues come down to this:

class Zero' (α : Type _) where
  zero : α

@[reducible]
def rid (h: Zero' α) : Zero' α := h

instance instZoInt : Zero' Int where
  zero := 0

theorem zero_rfl {α} [h : Zero' α] : (rid h).zero = (rid h).zero := rfl

set_option pp.mvars.anonymous false in
/--
error: typeclass instance problem is stuck
  Zero' ?_

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Zero'` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs in
example : (0 : Int) = 0 := by
  with_reducible_and_instances exact zero_rfl

example : (0 : Int) = 0 := by
  exact zero_rfl

[Eric Wieser]

Kim Morrison said:

lean#12701 I think will fix this,

I'm a little puzzled by the big picture here; am I right in saying that structure parents are _more_ reducible than instance parents (assuming reducible is "more reducible" than implicit_reducible? Is this deliberate?

[Robin Arnez]

Sure, since we bump the transparency to implicit_reducible for class projections, we need to make sure that you can't reduce them under reducible, otherwise we get the following transitivity failure:
(myInstance ..).projection =?= (MyClass.mk ... xyz ...).projection =?= xyz
but not (myInstance ..).projection =?= xyz under reducible transparency

[Eric Wieser]

and "bump the transparency" means "make less transparent"?

[Robin Arnez]

Bump the transparency in the sense of use a transparency of implicit_reducible or higher (i.e. or default / all if you already have it)

[Eric Wieser]

Does higher mean "more transparent" or "less transparent"?

[Robin Arnez]

Higher meaning being able to unfold more

[Arend Mellendijk]

Here's an issue I ran into in #34734 where a coersion between two structures no longer works. It concerns two types that each take a Lean.Level as an implicit parameter, which came up in the context of Qq annotations. The issue seems to be that Lean.Level.zero, Lean.levelZero and Lean.Level.ofNat (nat_lit 0) are not defeq at reducible transparency.

Here's a Mathlib- and Qq-free minimization:

import Lean

open Lean

structure A {u : Level} where
structure B {u : Level} where

instance testCoersion (u : Level) : Coe (B (u := u)) (A (u := u)) where
  coe x := ⟨⟩

def b : B (u := Lean.Level.zero) := ⟨⟩

set_option trace.Meta.isDefEq true
set_option trace.Meta.synthInstance true

/- The coersion fails. It succeeds if you uncomment the set_option.  -/
-- set_option backward.isDefEq.respectTransparency false in
#check show A (u := 0) from b

A snippet from the defeq trace shows Level.ofNat 0 =?= Level.zero fails

  [] ❌️ apply testCoersion to Coe B A ▼
    [tryResolve] ❌️ Coe B A ≟ Coe B A ▼
      [isDefEq] ❌️ Coe B A =?= Coe B A ▼
        [] ✅️ B =?= B ▶
        [] ❌️ A =?= A ▼
          [] ❌️ 0 =?= Level.zero ▼
            [] ❌️ Level.ofNat 0 =?= Level.zero ▼
              [onFailure] ❌️ Level.ofNat 0 =?= Level.zero

And indeed adding the following lines makes the coersion work again.

set_option allowUnsafeReducibility true
attribute [local reducible] Lean.levelZero Lean.Level.ofNat

Should those definitions be reducible? Or is there an important reason they're not?

I suppose I'll note this issue is not strictly caused by the new changes: if you make u explicit, you'll get the same error on Mathlib stable. I just hadn't noticed this because of the old behaviour around implicit parameters.

[Eric Wieser]

Should docs#Lean.levelZero just be deleted?

[Eric Wieser]

The whole section of constructor duplicates around it seem pretty pointless to me

[Arend Mellendijk]

I admit I had the same thought, but I'm not familiar enough with the internals of Lean to make that call

[Jovan Gerbscheid]

The original reason for these duplicate constructors, I think, is that the computed field feature didn't exists yet in its current form. So you really had to use these alternative constructors to make sure the computed field was set correctly. Reacall that e.g. Lean.Expr has 64 bits of additional information, 32 of which are just a hash, and some of the other bits are used to store e.g. Expr.hasFVar.

[Eric Wieser]

Indeed, Level.data is such a computed field

[Robin Arnez]

I wonder if we should eventually deprecate them, since we don't need them anymore

[Robin Arnez]

but well, let's maybe not talk about that in this thread

[Kim Morrison]

Thanks, @Arend Mellendijk, for those.

It's super (extra!) helpful if #mwe's use #guard_msgs to display the behaviour and the way it changes, e.g. as

import Lean

open Lean

structure A {u : Level} where
structure B {u : Level} where

instance testCoersion (u : Level) : Coe (B (u := u)) (A (u := u)) where
  coe x := ⟨⟩

def b : B (u := Lean.Level.zero) := ⟨⟩

/- The coersion fails. It succeeds if you uncomment the set_option.  -/
/--
error: Type mismatch
  b
has type
  B
but is expected to have type
  A
---
info: have this := sorry;
this : A
-/
#guard_msgs in
#check show A (u := 0) from b

/--
info: have this := { };
this : A
-/
#guard_msgs in
set_option backward.isDefEq.respectTransparency false in
#check show A (u := 0) from b

set_option trace.Meta.isDefEq true
set_option trace.Meta.synthInstance true

-- [] ❌️ apply testCoersion to Coe B A ▼
--   [tryResolve] ❌️ Coe B A ≟ Coe B A ▼
--     [isDefEq] ❌️ Coe B A =?= Coe B A ▼
--       [] ✅️ B =?= B ▶
--       [] ❌️ A =?= A ▼
--         [] ❌️ 0 =?= Level.zero ▼
--           [] ❌️ Level.ofNat 0 =?= Level.zero ▼
--             [onFailure] ❌️ Level.ofNat 0 =?= Level.zero
#check show A (u := 0) from b

[Kim Morrison]

I would really really love to see #35750 merged asap. With this, we don't need to muck about reading the trace messages ourselves, we just get immediately:

/--
warning: #defeq_abuse: command fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
The following synthesis applications fail due to transparency:
  ❌️ apply testCoersion to Coe B A
    ❌️ Level.ofNat 0 =?= Level.zero
---
info: have this := { };
this : A
-/
#guard_msgs in
#defeq_abuse in
#check show A (u := 0) from b

[Kim Morrison]

I'm trying out

set_option allowUnsafeReducibility true in
attribute [implicit_reducible] Lean.levelZero Lean.Level.ofNat

in lean4#12719 and #35832.

[Jeremy Tan]

Kim Morrison said:

I would really really love to see #35750 merged asap

Since you're a maintainer and you really want this in, why don't you just merge it yourself (after getting #35833 in)?

[Jovan Gerbscheid]

From my understanding, a non-trivial PR created by a maintainer needs to be approved by a different maintainer.

[Thomas Murrills]

#35750 is pretty bulky, in part because Claude has no qualms about repeating itself. :) This really obscures the logic and makes it difficult to review. I’ve taken a first pass at cleaning up the first half of it at #35833 so we can better see what’s going on in the code, shaving ~60 lines off of the main file.

I think if we reviewed this as an ordinary meta PR, even a high-value one, we’d be reviewing it for a little while.

But maybe we shouldn’t review it as an ordinary meta PR. Meta PRs that contribute features which are intended to be user-facing should be carefully reviewed for proper behavior and maintainability, but “providing users with a new feature” doesn’t seem to me the motivating factor for this PR.

The motivating factor is getting us through this breakage, and that has a different set of needs and constraints than an ordinary meta feature: very high value if some version of it is available now, without terrible consequences if it doesn’t work quite correctly or can’t be maintained in its current form (since its use is so restricted and single-purpose).

I think there’s an argument for viewing this as something like an “adaptation tool”. It’s technical debt, but it helps Kim get their urgent work done, so this might be a time when it makes sense to take on technical debt.

To make sure we’re clear to users about these different standards, we plaster neon signs in the module docs and hovers about how this is currently intended only for this sole purpose, may undergo breaking syntax and behavior changes in the future, and may not work as advertised. Then we clean it up after it’s in.

I don’t like technical debt, but given the circumstances, I think it wouldn’t be an unreasonable course of action.

[Yury G. Kudryashov]

If we're going this way, then I suggest making as much as possible private as a way to say "this may break at any time" without relying on a human reading a docstring. I'm not sure how much must stay public for the tactic to be usable.

[Violeta Hernández]

I would love to have any sort of tool to diagnose this error, instead of randomly flailing around in the dark adding set_option. Anything is better than nothing.

[Kim Morrison]

Yes, sorry, I should have talked about this above. In particular this is purely a diagnostic tool, which will never see a #defeq_abuse call committed to a branch or master outside the test file.

So for review we need to check that it does not "launch the nukes" in some annoying way, and we need some basic behavioural tests: is this more often than not a time saver to diagnose problems?

[Eric Wieser]

I think there's also an element of deciding what our maintainence plan is if it breaks in a lean update; but I guess the answer is "that will almost certainly become Kim's problem"?

[Kim Morrison]

lean#12701 seems to result in the addition of 100 new set_option backward and the removal of another 400. So... net positive! And it seems more principled to have the grandparent projections have the same reducibility as normal structure projections (I am not attempting yet to get consistency here for mixed class/structure inheritance. My mind boggles, but we will have to return to this.) So it will land in an rc3, which unfortunately I won't be able to get to Mathlib until Monday.

[Eric Wieser]

I am not attempting yet to get consistency here for mixed class/structure inheritance

Perhaps the easy answer here is to lint against this in mathlib in the first place

[Eric Wieser]

I guess the main thing this would break is Algebra which we would have to write as algebraMap.toFun := instead of toFun := or similar

[Kim Morrison]

Eric Wieser said:

I think there's also an element of deciding what our maintainence plan is if it breaks in a lean update; but I guess the answer is "that will almost certainly become Kim's problem"?

The backup plan being "Now that we are on Lean v4.67.0, Mathlib is so immaculately careful about defeq abuse, that this legacy tool can simply be deleted!"... :-)

[Thomas Murrills]

Kim Morrison said:

In particular this is purely a diagnostic tool, which will never see a #defeq_abuse call committed to a branch or master outside the test file.

Just to make clear my reviewing/maintaining thoughts here:

Even if no invocation of a diagnostic tool is ever committed to a branch or master, the tool still becomes part of the user interface surface, and people form expectations about it and how it works (without committing it anywhere).

So, to respect those expectations and keep the user interface surface stable, an ordinary contribution of a diagnostic tool would still need to at least try to avoid breaking changes (e.g. settle on good syntax), be reviewed to behave correctly/meet current expectations, and have maintainable-enough code to preserve those expectations through time.

But since this is no ordinary diagnostic tool...we "get to" avoid all that for now with some disclaimers :)

[Eric Wieser]

Kim Morrison said:

"Now that we are on Lean v4.67.0, Mathlib is so immaculately careful about defeq abuse, that this legacy tool can simply be deleted!"... :-)

I would be extremely surprised if the code remains unbroken for ~40 releases!

[Johan Commelin]

What about creating a new package in the Mathlib4 repo, next to Mathlib, Archive, etc...
We call it MathlibNightlyDevTools.
It is imported in the root of Mathlib by default, but we lint against any of those tools/commands/decls actually appearing in Mathlib.
The review of new tools can follow the standards that Thomas outlined above.
And there is a very clear communication that "if this code breaks during updates, we might just delete it... we don't promise any polish, or maintenance, or whatever"

[Thomas Murrills]

Kim Morrison said:

So for review [...] we need some basic behavioural tests: is this more often than not a time saver to diagnose problems?

The endorsement from @Violeta Hernández seems to suggest "yes". :) Given that we are including disclaimers, I am tempted to say we should experiment with this in the field! :)

[Violeta Hernández]

I haven't actually experimented with this new tool. But given that I just had to add 100 of these set_options to my own repo, I'm certainly excited to try it out.

[Thomas Murrills]

I've made a final bare-bones review PR to the branch adding disclaimers, making some functionality private (and changing one private thing to public, but I believe the organization is better that way): #35843.

[Thomas Murrills]

If there are no objections here shortly I'll maintainer delegate the PR. (Or a maintainer can leapfrog me. :) ) I've maintainer delegated the PR. I think it would be great to get MathlibNightlyDevTools going, and move this there...but after it's merged, given that the point of this unorthodoxy is the time sensitivity :)

[Anne Baanen]

Delegated! :peace_sign:

[Matthew Jasper]

I've finished looking at the ofNat issues. The bug here is that class projections are semireducible and are special cased in the compiler to act like they're implicit_reducible, but it's not handled correctly everywhere. Specifically, getStuckMVar? is not normalizing the instance parameter to the projection function, even though it does so for actual projections. I think that there's two possible solutions: first, getStuckMVar?could be made consistent between projections and class projection functions:

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index d05e0e694a..ba7959297b 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -350,3 +350,3 @@ mutual
             if let some major := args[projInfo.numParams]? then
-              if let some mvarId ← getStuckMVar? major then
+              if let some mvarId ← getStuckMVar? (← whnf major) then
                 return mvarId

Alternatively, class projection functions could be made implicit_reducible. This appears to work and should also allow removing unfoldProjInstWhenInstances? but I wasn't able to test that because it seems that the build process doesn't recompile Init with the new compiler.

Note that lean#12701 is also required to fix the original Mathlib examples.

[Robin Carlier]

So, if class projections are semireducible, and semireducible Type-valued definitions are bad, should be avoided etc., is the design of docs#Quiver bad? Is the following "defeq abuse"?

import Mathlib.Combinatorics.Quiver.Basic
opaque V : Type
structure V.Hom (_ : V) (_ : V) where of : Nat
instance : Quiver V where Hom := V.Hom
-- is using `f.of` for `f : Quiver.Hom x y` abuse?
example {x y : V} (f : x ⟶ y) : Nat := f.of

I am of course asking because this kind of things is everywhere in Mathlib: morphisms in categories are almost always structures on which we use the field projections on terms of type _ ⟶ _.
If this is abuse, what could be fixes that do not involve refactoring the entirety of category theory? Marking Quiver.Hom as implicit_reducible?

[Eric Wieser]

I think we tried making Quiver.Hom reducible in the past, and it didn't work because not every instance used that structure pattern

[Yury G. Kudryashov]

I would appreciate a review of #35795 (reduce defeq about Set)

[Robin Carlier]

Eric Wieser said in #general > backward.isDefEq.respectTransparency:

I think we tried making Quiver.Hom reducible in the past, and it didn't work because not every instance used that structure pattern

Is this saying that we should be refactoring these instance to make sure their Hom is always a structure (maybe with just one field)?
What would be other unwanted consequences of marking it implicit_reducible?

[Yury G. Kudryashov]

The next batch about Set defeq abuse: #35885 (probably, I haven't cherry-picked all the relevant parts of the diff; I'll do it in the morning)

[Eric Wieser]

Robin Carlier said:

Is this saying that we should be refactoring these instance to make sure their Hom is always a structure (maybe with just one field)?

Yes, and I think this is already a refactor we've been slowly executing