bad coercion

Stream: general

[Chris Hughes]

Would this function be a bad coercion? Do I have to use has_coe_t or something for this?

def to_matrix [has_one R] [has_zero R] (f : pequiv m n) : matrix m n R
| i j := if j ∈ f i then 1 else 0

[Kenny Lau]

why don't you use projection

[Chris Hughes]

I do, but then I write .to_matrix everywhere, and everything is long and unreadable.

[Joe Hendrix]

Can you make it a definition and add local instances where you find yourself frequently writing to_matrix? The main question I have with coercision instances is whether you always want them to spread to modules that import the module that are in even indirectly.

[Chris Hughes]

The difficulty with that is I need all the theorems to be stated with whichever one I'm using.

[Joe Hendrix]

That's true, but you could still define the coe_t, just not make it an instance.

What I had in mind was something like

def to_mat_coe : coe_t (pequiv m n) (matrix m n R) := <to_matrix>
local [instance] to_mat_coe

Then other modules that want the coercions just write local [instance] to_mat_coe.

Note that the above syntax may not be exactly right, it's been a while since I used Lean 3.

[Mario Carneiro]

That will create a bunch of theorems of the form @coe _ _ (to_mat_coe) foo = bar, which will not be usable after the coercion goes away

[Mario Carneiro]

This can't be a coe because R is an out parameter