Zulip Chat Archive

Stream: general

Topic: matrix add_comm_monoid issue


view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 12 2021 at 08:36):

I haven't investigated yet.

view this post on Zulip 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
  matrix.add_comm_monoid
inferred
  matrix.add_comm_monoid

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 12 2021 at 08:39):

Never mind, I'm stupid :face_palm:

view this post on Zulip Johan Commelin (Apr 12 2021 at 08:39):

reindex_linear_equiv obviously needs semiring

view this post on Zulip Johan Commelin (Apr 12 2021 at 08:39):

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

view this post on Zulip Johan Commelin (Apr 12 2021 at 08:40):

It should have yelled at me in 0.1ms

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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
[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

Last updated: May 14 2021 at 13:24 UTC