Zulip Chat Archive
Stream: mathlib4
Topic: !4#2868
Jeremy Tan (Mar 15 2023 at 14:55):
!4#2868 perhaps someone could fix the remaining errors in this?
Jeremy Tan (Mar 15 2023 at 14:56):
Lines 113/114 in particular look like a place where the way simp works in mathlib 3 is too cryptic
Ruben Van de Velde (Mar 15 2023 at 15:08):
That was a weird one. It builds, but you'll need to fix some C's and X's in the names
Jeremy Tan (Mar 15 2023 at 15:15):
hmm... yeah
Jeremy Tan (Mar 16 2023 at 02:23):
@Eric Wieser the problem is that op_apply_apply appears only in one place in the mathlib3 code – the very file I'm trying to port – and has no declared lean4 equivalent. Can you search for its equivalent?
simp only [opRingEquiv, RingEquiv.trans_apply, /-RingEquiv.op_apply_apply,-/
RingEquiv.toAddEquiv_eq_coe, AddEquiv.mulOp_apply, AddEquiv.coe_trans,
opAddEquiv_apply, RingEquiv.coe_toAddEquiv, opAddEquiv_symm_apply, Function.comp_apply,
unop_op, toFinsuppIso_apply, toFinsupp_monomial, AddMonoidAlgebra.opRingEquiv_single,
toFinsuppIso_symm_apply, ofFinsupp_single]
Kyle Miller (Mar 16 2023 at 02:25):
docs#ring_equiv.op_apply_apply is generated by the @[simps] attribute on this definition
Jeremy Tan (Mar 16 2023 at 02:27):
how do you search for that?
Kyle Miller (Mar 16 2023 at 02:28):
I used the mathlib3 documentation's search in the upper right corner
Kyle Miller (Mar 16 2023 at 02:30):
There's some way to get @[simps] to explain what it defines. Maybe @[simps?]? You might try doing that to the corresponding mathlib4 definition to see what it might be naming this lemma.
Kyle Miller (Mar 16 2023 at 02:32):
@[simps] is a fairly complicated metaprogram that Floris develops to generate useful boilerplate simp lemmas, and it has some differences between the mathlib3 and mathlib4 versions (though I don't know how they work well enough to say what they are)
Jeremy Tan (Mar 16 2023 at 02:33):
@[simps?] shows 4 lemmas but none match exactly mathlib3 ring_equiv.op_apply.apply
Jeremy Tan (Mar 16 2023 at 02:37):
The closest one is RingEquiv.op_apply_apply_unop but its definition is
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β] (f : α ≃+* β)
(a : αᵐᵒᵖ), (↑(↑RingEquiv.op f) a).unop = ↑f a.unop
whereas the mathlib3 version is
[simps] > adding projection ring_equiv.op_apply_apply:
> ∀ {α : Type u_1} {β : Type u_2} [_inst_1 : has_add α] [_inst_2 : has_mul α] [_inst_3 : has_add β]
[_inst_4 : has_mul β] (f : α ≃+* β) (ᾰ : αᵐᵒᵖ),
⇑(⇑ring_equiv.op f) ᾰ = (⇑add_equiv.mul_op f.to_add_equiv).to_fun ᾰ
Kyle Miller (Mar 16 2023 at 02:41):
Maybe I'll ping @Floris van Doorn about it. Either there's some configuration we're supposed to do to get @[simps] to generate the right thing, or it's an interesting new test case for the implementation. (For Floris: it's for a (α ≃+* β) ≃ (αᵐᵒᵖ ≃+* βᵐᵒᵖ), and the fields are structures themselves, so maybe simps isn't looking at expanding them?)
Kyle Miller (Mar 16 2023 at 02:42):
@Jeremy Tan Could you give a link to the mathlib4 version? If it's in a PR, a link to a line in a commit maybe?
Jeremy Tan (Mar 16 2023 at 02:45):
Jeremy Tan (Mar 16 2023 at 02:49):
@Yury G. Kudryashov see my comment on the PR
Jeremy Tan (Mar 16 2023 at 03:05):
nevermind, I got the squeezed proof from simp? in Lean 4
Floris van Doorn (Mar 16 2023 at 11:07):
The difference in the lemmas is because docs#mul_opposite is a definition but docs4#MulOpposite is a structure.
Floris van Doorn (Mar 16 2023 at 11:09):
If you want the old lemma, you can do something like @[simps (config := { notRecursive := [`MulOpposite] })].
Floris van Doorn (Mar 16 2023 at 12:58):
You can also experiment with adding `MulOpposite here to do this by default. That might be useful for other definitions in Lean 3 that got turned into structures in Lean 4.
Adam Topaz (Mar 16 2023 at 13:54):
Is docs4#Opposite a structure as well? (No)
Adam Topaz (Mar 16 2023 at 13:55):
Why did we make this change in lean4?
Floris van Doorn (Mar 16 2023 at 13:56):
Adam Topaz (Mar 16 2023 at 13:58):
Just to clarify, I think making it a structure is good for various reasons. I'm just curious why we didn't do it for docs4#Opposite as well.
Last updated: Dec 20 2023 at 11:08 UTC