-
Notifications
You must be signed in to change notification settings - Fork 350
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Meta.isDefEq failure #2461
Comments
It appears (to the untrained eye) that the transparency of |
I think it's worth emphasising that a solution to this would be especially valuable because of the frequent situations where we use |
Yes, |
Does |
Also, if you blindly make everything reducible, we get down to |
Then you didn't literally make everything reducible because |
Ha ha! Thanks. I don't think it has been mentioned above explicitly (but was emphasized in the Zulip topic that birthed this) but I thought reducibility for |
I think the answer is "essentially yes", in light of this library note. |
Which is to say, -- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra' {R S : Type} [CommSemiring R] [Semiring S] (i : R →+* S)
: Algebra R S where
smul c x := i c * x
toRingHom := i
-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra {R S : Type} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
i.toAlgebra' are breaking this rule and should be |
It's not enough; to make the mwe fail to fail, you also have to change -def RingHom.id (α : Type) [Semiring α] : α →+* α := { toFun := _root_.id .. }
+@[reducible] def RingHom.id (α : Type) [Semiring α] : α →+* α := { toFun := (·) .. } which is not a change we want to make |
Well that is problematic. Both simp and TC inference fundamentally depend on such typeclass diamonds being defeq under |
@kbuzzard, do you have a Zulip thread in mind that motivated this MWE? |
@eric-wieser Yes, see this message. You can see an example of this in Mathlib here: you can replace |
The issue has already been fixed in previous PRs. closes #2461
Prerequisites
Description
Meta.isDefEq
fails to deduce that two defeq terms are defeq, causingsimp
to fail.Steps to Reproduce
No doubt this can be minimised more, but
The relevant part of the
trace.Meta.isDefEq
output isand in particular the failure on line 3
[] ❌ Algebra.toSMul =?= bar ▼
is unexpected because the terms are defeq.Expected behavior: [What you expect to happen]
I would not expect that randomly adding a term to the local context would break a
simp
proof.Actual behavior: [What actually happens]
In the presence of
bar
,simp
now makes no progress.Reproduces how often: [What percentage of the time does it reproduce?]
100%
Versions
Lean (version 4.0.0-nightly-2023-08-19, commit 63d2bdd4908b, Release)
on UbuntuAdditional Information
There are workarounds, for example one can use
simp only [Pi.smul_apply _]
. But telling users to add_
s everywhere is not an ideal solution.The text was updated successfully, but these errors were encountered: