Algebra.Order.Hom.Ring #1482

Stream: mathlib4

[Lukas Miaskiwskyi]

Corresponding PR: mathlib4#1482

The refl attribute on the reflfor OrderRingIsos is giving me trouble:

@[refl] attribute only applies to lemmas proving x ∼ x, got (α : Type u_1) →
  [inst : Mul α] → [inst_1 : Add α] → [inst_2 : LE α] → α ≃+*o α

I was thinking the issue is with the instances, but the refl in Algebra.Ring.Equiv looks fairly similar, and its refl tag gives no complaints:

RingEquiv.refl.{u_1} (R : Type u_1) [inst✝ : Mul R] [inst✝¹ : Add R] : R ≃+* R

Any thoughts? Why is the above refl not recognized as x ~ x?

[Matthew Ballard]

I get similar complaints in !4#1287 for self-equivalences of categories.

[Matthew Ballard]

The cited issue was "fixed" by reordering the parameters of the class. It look like let .app (.app rel lhs) rhs := targetTy | fail here takes the first two parameters? This also affects @[trans]

[Lukas Miaskiwskyi]

Returning to this to report that this is still an issue. But I guess it is still not a github-issue, so I'll try to make it one. Thanks for sharing your fix, @Matthew Ballard , but in this particular case I don't see what I could reorder, the first two arguments of OrderRingIso are already the "correct" ones:

structure OrderRingIso (α : Type _) (β : Type _) [Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β] extends
  α ≃+* β

[Lukas Miaskiwskyi]

Hahaha, actually: Reordering the instances after the first two arguments, from

[Mul α] [Add α] [LE α] [Mul β] [Add β] [LE β]

to

[Mul α] [Mul β] [Add α] [Add β] [LE α] [LE β]

fixes things. I'll still open an issue, since reordering arguments (even if they are instances or otherwise implicit) seems like a devious thing to do while porting, with implicit arguments being accessed through @theorem often enough.

[Lukas Miaskiwskyi]

Issue: https://github.com/leanprover-community/mathlib4/issues/2505

[Matthew Ballard]

I think the better workaround is to build the the instance by hand, remove the the tag, and leave a note