matrix add_comm_monoid issue

Stream: general

[Johan Commelin]

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]

I haven't investigated yet.

[Johan Commelin]

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
  matrix.add_comm_monoid
inferred
  matrix.add_comm_monoid

[Anne Baanen]

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

[Johan Commelin]

Never mind, I'm stupid :face_palm:

[Johan Commelin]

reindex_linear_equiv obviously needs semiring

[Johan Commelin]

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

[Johan Commelin]

It should have yelled at me in 0.1ms

[Anne Baanen]

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]

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

[Anne Baanen]

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]

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
[type_context.is_def_eq_detail] unfold left&right: add_comm_monoid.to_add_monoid
[type_context.is_def_eq_detail] [10]: {add := add_comm_monoid.add ((λ (i : n), semiring.to_add_comm_monoid R) i),
 add_assoc := _,
 zero := add_comm_monoid.zero ((λ (i : n), semiring.to_add_comm_monoid R) i),
 zero_add := _,
 add_zero := _} =?= {add := add_comm_monoid.add ((λ (i : n), _inst_3) i),
 add_assoc := _,
 zero := add_comm_monoid.zero ((λ (i : n), _inst_3) i),
 zero_add := _,
 add_zero := _}
[type_context.is_def_eq_detail] [11]: add_comm_monoid.add =?= add_comm_monoid.add
[type_context.is_def_eq_detail] [12]: (λ (i : n), semiring.to_add_comm_monoid R) i =?= (λ (i : n), _inst_3) i
[type_context.is_def_eq_detail] after whnf_core: semiring.to_add_comm_monoid R =?= _inst_3
[type_context.is_def_eq_detail] unfold left: semiring.to_add_comm_monoid
[type_context.is_def_eq_detail] [13]: {add := semiring.add ?m_1, add_assoc := _, zero := semiring.zero ?m_1, zero_add := _, add_zero := _, add_comm := _} =?= _inst_3
[type_context.is_def_eq_detail] on failure: {add := semiring.add ?m_1, add_assoc := _, zero := semiring.zero ?m_1, zero_add := _, add_zero := _, add_comm := _} =?= _inst_3
[type_context.is_def_eq_detail] [12]: semiring.add =?= add_comm_monoid.add
[type_context.is_def_eq_detail] [13]: semiring.add =?= add_comm_monoid.add
[type_context.is_def_eq_detail] on failure: semiring.add =?= add_comm_monoid.add