Difficulty working with coe

Stream: new members

[Eric Wieser]

I have in my proof a definition instance has_coe (r : ℤ) : has_coe (A r) G := { coe := to_fun }. However, for ar : A r, when I swap out (to_fun ar : G) in my lemmas for (ar : G), I can't work out how to unfold coe in my proofs.

The full code is self-contained, and at https://github.com/pygae/lean-ga/pull/5/files#. I've added some comments on the lines where coe is causing me difficulty.

Feedback would be very appreciated, and thanks all for all the help so far.

[Mario Carneiro]

That coe is a bad instance

[Eric Wieser]

How so?

[Mario Carneiro]

because neither A r nor G have any interesting structure to key on

[Eric Wieser]

Is it generally true that type-classes should never provide coe?

[Mario Carneiro]

When lean goes looking for a coe the right argument is unbound, so it's trying to see what A r can coerce to

[Mario Carneiro]

It can depend on typeclasses on A r but not on A and certainly not on G

[Mario Carneiro]

However, you can use a notation to avoid mentioning A r and G in the section

[Eric Wieser]

Presumably it does find my coe though, since the lemma statements are valid if I make the change - it's just my proofs which suffer

[Eric Wieser]

Local notation did the trick, thanks! (done in https://github.com/pygae/lean-ga/commit/9643c01d7f7a69da952ffeaccad6b6dca55b4cd6)

To make coe simplify, I had to add lemma coe_def {r : ℤ} (v : A r) : (v : G) = to_fun v := rfl

[Eric Wieser]

Is there any way to take existing notation and bind the inferred arguments without repeating the symbols and precedence?