has_coe

Stream: new members

[Alex Zhang]

Why does #check reports the errorinvalid field notation, function 'has_coe.coe' does not have explicit argument with type (has_coe ...)?

import data.matrix.basic
namespace matrix
variables {α I J : Type*} [fintype I] [fintype J] [non_unital_non_assoc_semiring α]
instance to_mul_vec : has_coe (matrix I J α) ((J → α) → (I → α)) :=
⟨λ M v, M.mul_vec v⟩
variable (A : matrix I J α)
#check matrix.to_mul_vec.coe A
end matrix

[Alex Zhang]

Btw, #check matrix.to_mul_vec.coe gives has_coe.coe : matrix ?M_1 ?M_2 ?M_5 → (?M_2 → ?M_5) → ?M_1 → ?M_5.

[Mario Carneiro]

has_coe.coe is usually written \u, why are you using projection notation for it?

[Mario Carneiro]

it has an argument of type has_coe but it's a typeclass argument, so it isn't supposed to work with projection notation. (It does in some circumstances due to a bug that no one has cared to fix.)

[Alex Zhang]

Mario Carneiro said:

has_coe.coe is usually written \u, why are you using projection notation for it?

Because I am not sure how to properly use \u in this case. I would like #check ↑A to print ↑A : (J → α) → I → α but it prints ↑A : ?M_1. @Mario Carneiro

[Mario Carneiro]

it needs to know what it is coercing to as well. #check (↑A : (J → α) → I → α ) should work

[Mario Carneiro]

I think in this example it would be better to have a coe_fun instance instead, so that you can write A v for mul_vec

[Alex Zhang]

(deleted)

[Alex Zhang]

Mario Carneiro said:

it needs to know what it is coercing to as well. #check (↑A : (J → α) → I → α ) should work

Yeah, Mario. I know this should work. I was using the projection notation for another reason.

[Mario Carneiro]

if you are just exploring and noticed the oddity with matrix.to_mul_vec.coe, that's just a bug

[Alex Zhang]

import data.matrix.basic
namespace matrix
variables {α I J : Type*} [fintype I] [fintype J] [non_unital_non_assoc_semiring α]
instance to_mul_vec : has_coe (matrix I J α) ((J → α) → (I → α)) :=
⟨λ M v, M.mul_vec v⟩
instance to_vec_mul : has_coe (matrix I J α) ((I → α) → (J → α)) :=
⟨λ M v, M.vec_mul v⟩
variable (A : matrix I I α)
#check (↑A : (I → α) → (I → α))
end matrix

[Alex Zhang]

In the above case, if I use \u, I think I am unable to pick which one of to_mul_vec to_vec_mul I am using. That is the other reason I was not using \u before.

[Mario Carneiro]

yeah that looks like a bad notation

[Mario Carneiro]

I would do something like A *> v and v <* A

[Alex Zhang]

@Mario Carneiro Mario, do you have a way to pick a particular coercion?
I don't quite understand your last reply, could you please give more explanation?

[Alex Zhang]

btw, #check A.to_mul_vec.coe also reports an error.

[Mario Carneiro]

The notation is ambiguous about a mathematically relevant distinction, so even if lean worked perfectly here I wouldn't recommend it

[Mario Carneiro]

you shouldn't use A v to mean both A*v and v*A

[Eric Wieser]

Because if you did, it would be ambiguous when I = J

[Mario Carneiro]

even if one of them is type incorrect and so lean knows what you are talking about, readers will be confused

[Eric Wieser]

Not just readers, people trying to prove things about your definition will get ambiguous goal states they have to hover over to interpret.

[Alex Zhang]

Mario Carneiro said:

I would do something like A *> v and v <* A

As I noticed \u A and A v are ambiguous in the (A : matrix I I α) case , I attempted to use the dot notation. Then Mario pointed out to me that there is a bug.
*> and <* have already been used to mean has_seq_right and has_seq_left(, of which I don't quite understand the purpose).
What I am not sure is if you mean to use has_seq_right and has_seq_left or just overload of notations?

[Eric Wieser]

Have you considered A • v as a spelling?

[Eric Wieser]

Oh, I guess that only works for square matrices

[Alex Zhang]

No. • is used for scalar multiplication. I am not sophisticated in playing around with abused notations.

[Eric Wieser]

I'd argue that for square matrices A • v is actually the right syntax, since it satisfies module (matrix n n R) (n → R). Lean 4's heterogenous multiplication would help a lot here

[Alex Zhang]

Maybe this is a little bit far away from my original question. As #check (↑A : (I → α) → (I → α)) is ambiguous, is there a way to invoke to_mul_vec or to_vec_mul manually?

[Eric Wieser]

Yes, you can use @has_coe.coe _ _ to_vec_mul A

[Eric Wieser]

But this is an #xy problem, if your notation is ambiguous then you shouldn't have defined it in the first place.

[Alex Zhang]

Thanks and good point! I was exploiting things in Lean.