Zulip Chat Archive

Stream: general

Topic: has_coe_to_fun lemmas

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 09:01):

Chris says that this is hard in Lean 3.

view this post on Zulip Kevin Buzzard (Jul 12 2019 at 09:01):

@Chris Hughes

Last updated: May 14 2021 at 06:16 UTC