refactor: make the algebra hierarchy use flat structures#3171
refactor: make the algebra hierarchy use flat structures#3171eric-wieser wants to merge 28 commits intomasterfrom
Conversation
|
👍 I think that's the best workaround to unblock the port for now. Can you try to add |
|
@gebner: I don't know how to make progress on this unfortunately. The error is which is caused by flat-inheriting the same default field twice. I would be happy to tell lean just to ignore the default value silently. |
|
@eric-wieser I've added a commit that works around that issue. |
|
|
||
| theorem lt_of_mul_lt_mul_of_nonpos_left (h : c * a < c * b) (hc : c ≤ 0) : b < a := | ||
| lt_of_mul_lt_mul_left (by rwa [neg_mul, neg_mul, neg_lt_neg_iff]) <| neg_nonneg.2 hc | ||
| lt_of_mul_lt_mul_left (by rwa [neg_mul, neg_mul, neg_lt_neg_iff]) <| (neg_nonneg (α := α)).2 hc |
Mathlib/Algebra/Field/Defs.lean
Outdated
| and can therefore be easily transported along ring isomorphisms. | ||
| Additionaly, this is useful when trying to prove that | ||
| a particular ring structure extends to a (semi)field. -/ | ||
| a particular ring structure extends FlatHack, to a (semi)field. -/ |
There was a problem hiding this comment.
Overzealous replace I think!
There was a problem hiding this comment.
@gebner, the failure is now happening in Qq in this file. Would you mind taking a look?
There was a problem hiding this comment.
Fixed. The function has both a LinearOrderedRing and a DivisionRing instance there, and we can't state that they commute because they're not comparable (I think). We really need a LinearOrderedDivisionRing class.
There was a problem hiding this comment.
Sorry, I got tricked by "warnings as errors". Now that I've turned that off, I actually get the error in this file.
I don't seem to be in a monad context, so I'm not sure how to use assumeInstancesCommute
There was a problem hiding this comment.
There's assumeInstancesCommute' for term mode. But it's the same situation as in the other function. We have a CommSemiring and a Ring instance, and there's no way to make them defeq.
There was a problem hiding this comment.
Presumably we can just override Qq's safety feature here and say "trust me, they're defeq"?
I assume that's what you did in the previous patch; I was struggling to get =Q to work here, but I didn't know about assumeInstancesCommute
There was a problem hiding this comment.
The thing is that there is no way to communicate to the lean elaborator that CommSemiring.toSemiring is defeq to Ring.toSemiring. (and that's what's failing here)
If we had for example a CommRing instance i and a CommSemiring instance j, then we could say that the j is defeq to CommRing.toCommSemiring by making j a let-binding. (Which is what =Q does.). In other words the =Q can only make comparable instances commute.
The only workaround I know here is to restate the hypothesis again with the right type.
There was a problem hiding this comment.
I've pushed what seems to be a workaround, though now lean is giving me a warning saying that my fix doesn't do anything!
|
Is this PR abandoned? I'm noticing it hasn't been touched for quite some time. One might as well close it if that is the case. |
|
Since leanprover/lean4#2074 is now resolved and flat structures are way out of the question now, I believe we can close this? Feel free to reopen if you disagree. |
By introducing a
FlatHackbase class and using it as the first parent of every algebra typeclass, it causes the typeclasses to all overlap and so we emulate flat structures.Most of the pain here comes from
to_additivenot generating any of the ancestor projections properly; this was already a bug present forn + 1parents, but now the1is taken upThis is one workaround for leanprover/lean4#2074: don't let the eta-diamonds appear in the first place.