## Stream: new members

### Topic: Inferring associativity of composition

#### Yakov Pechersky (Jun 17 2020 at 18:34):

I'm trying to understand how instances are inferred for composition of functions or linear maps. Why does the first example work, but the second one fails?

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables {n : Type*} [fintype n] [decidable_eq n] {R : Type*} [field R]

-- works
example (A : matrix n n R) (B : matrix n n R) (C : matrix n n R) :
(A.to_lin.comp (B.to_lin.comp C.to_lin)) = ((A.to_lin.comp B.to_lin).comp C.to_lin) :=
(is_associative.assoc _ _ _).symm

-- does not work, cannot find instance for is_associative
example (A : matrix n n R) (B : matrix n n R) (C : matrix n n R) :
(A.to_lin.comp (B.to_lin.comp C.to_lin)) = ((A.to_lin.comp B.to_lin).comp C.to_lin) :=
begin
rw @is_associative.assoc _ linear_map.comp (by apply_instance) _ _ _,
sorry,
end


#### Anne Baanen (Jun 18 2020 at 09:48):

From set_option trace.class_instances true, we can see that it derives is_associative from the monoid instance on linear_map, but that only works for specific linear maps, from a semimodule M to M itself. In the first example, the expected type gives the elaborator enough information to finish the typeclass search. Passing the term as an argument to rw doesn't give it an expected type, so there are not enough constraints to find the monoid instance. If you help the typeclass search by writing rw @is_associative.assoc (linear_map R (n → R) (n → R)) linear_map.comp (by apply_instance), it does have enough information to succeed.

Last updated: Dec 20 2023 at 11:08 UTC