Zulip Chat Archive

Stream: general

Topic: has_coe_to_fun lemmas


Andreas Swerdlow (Jun 24 2019 at 13:04):

I'm working on bilinear forms (link: https://github.com/leanprover-community/mathlib/blob/inner_product_spaces/src/linear_algebra/bilinear_form.lean) and would like to use has_coe_to_fun for notation. However, I run into issues when trying to apply lemmas for structures that extend bilin_form, for example refl_bilin_form. Do I need to copy and paste every lemma for each new structure? I have found one workaround which is to give a coercion from refl_bilin_form to bilin_form, but this requires the use of coe_fn_coe_base before rw works.

Kevin Buzzard (Jun 27 2019 at 17:50):

Andreas has just explained his question to me in a lot more detail. He has made a structure called bilinear forms, with a coe to fun. His simp lemmas for bilinear forms are all written in terms of this coercion (so they're statements about \u b with b the bilinear form). He now wants to make symmetric bilinear forms and so he extended the structure and now he can't use any of his simp lemmas. How should he be doing this? I suggested making an is_symmetric predicate on bilinear forms instead, so then the symmetric bilinear forms would be a subtype rather than a new structure. Are there other better ways to do this?

Kevin Buzzard (Jul 12 2019 at 09:01):

Chris says that this is hard in Lean 3.

Kevin Buzzard (Jul 12 2019 at 09:01):

@Chris Hughes


Last updated: Dec 20 2023 at 11:08 UTC