## Stream: general

#### Johan Commelin (Apr 12 2021 at 08:35):

From LTE

import linear_algebra.matrix

namespace matrix
open equiv

variables {m n R : Type*} [fintype m] [fintype n]
variables [semiring R] -- change to [add_comm_monoid R] to get failure
variables (M : matrix m n R)

lemma reindex_linear_equiv_sum_empty_symm :
(reindex_linear_equiv (sum_empty _) (sum_empty _)).symm M = from_blocks M 0 0 0 :=
begin
ext (i|i) (j|j),
{ simp only [sum_empty_apply_inl, reindex_linear_equiv_symm_apply, from_blocks_apply₁₁] },
{ cases j },
{ cases i }
end

end matrix


#### Johan Commelin (Apr 12 2021 at 08:36):

I haven't investigated yet.

#### Johan Commelin (Apr 12 2021 at 08:36):

After ~10 secs I get an error on the .symm saying

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
inferred


#### Anne Baanen (Apr 12 2021 at 08:37):

My first idea is decidable_eq issues, but I guess semiring R would have those, not add_comm_monoid.

#### Johan Commelin (Apr 12 2021 at 08:39):

Never mind, I'm stupid :face_palm:

#### Johan Commelin (Apr 12 2021 at 08:39):

reindex_linear_equiv obviously needs semiring

#### Johan Commelin (Apr 12 2021 at 08:39):

It's just that Lean is bad at letting me know this

#### Johan Commelin (Apr 12 2021 at 08:40):

It should have yelled at me in 0.1ms

#### Anne Baanen (Apr 12 2021 at 08:44):

Well, how would it know from (reindex_linear_equiv (sum_empty _) (sum_empty _)).symm that the instance it needs is semiring R? So only if the unification succeeds, it can start giving "missing instance" errors.

#### Johan Commelin (Apr 12 2021 at 08:45):

I'm sure there is an explanation :smiley: But I still want it to yell at me faster :stuck_out_tongue_wink:

#### Anne Baanen (Apr 12 2021 at 08:51):

Yeah, it looks like the unifier is climbing up the entire inheritance hierarchy on both sides of matrix.add_comm_monoid =?= matrix.add_comm_monoid, hoping to find an instance where the add and zero happen to coincide. There should be a better way to do that.

#### Anne Baanen (Apr 12 2021 at 08:58):

It also keeps doing these kinds of weird loops, "let's check that semiring.to_add_comm_monoid =?= __inst_3 by checking the add and zero fields coincide. well, how do we get the add and zero fields to coincide? because semiring.to_add_comm_monoid =?= __inst_3. well, I guess we were already checking that, so never mind" (repeat for each add field in each ancestor of semiring and each ancestor of add_comm_monoid)

[type_context.is_def_eq_detail] [10]: (λ (i : n), semiring.to_add_comm_monoid R) i =?= (λ (i : n), _inst_3) i
zero := add_comm_monoid.zero ((λ (i : n), _inst_3) i),