has_coe_to_fun lemmas

Stream: general

[Andreas Swerdlow]

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]

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]

Chris says that this is hard in Lean 3.

[Kevin Buzzard]

@Chris Hughes