is_left_id rw mystery

Stream: general

[Patrick Massot]

example (R : Type) (op nil a) [is_left_id R op nil] : op nil a = a := by rw is_left_id.left_id

errors with:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_1 ?m_2 ?m_3
state:
R : Type,
op : R → R → R,
nil : out_param.{1} R,
a : R,
_inst_2 : is_left_id.{0} R op nil
⊢ @eq.{1} R (op nil a) a

[Patrick Massot]

I know I could use is_left_id.left_id _ _ in place of the rw

[Patrick Massot]

But in my real use case I want to rewrite

[Patrick Massot]

(or simp would be even better)

[Kenny Lau]

example (R : Type) (op nil a) [is_left_id R op nil] : op nil a = a := by rw is_left_id.left_id op a

[Patrick Massot]

interesting

[Patrick Massot]

doesn't explain why unification fails though

[Kenny Lau]

probably because that is a higher-order unification

[Kenny Lau]

https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification

[Kenny Lau]

it is undecidable

[Patrick Massot]

Oh I think you're right

[Patrick Massot]

@Mario Carneiro is this part of why you don't believe in the new algebraic hierarchy? Or is it possible to recover a working simp lemma here?

[Mario Carneiro]

Yes, this is the main problem with the new alg hierarchy. To be fair to Leo, he's been aware of this problem since the start, and the algebra attribute is part of a plan to fix it, but it requires more lean support than it currently gets. It should be a part of lean 4

[Patrick Massot]

Ok, it makes sense. Do you agree that the new hierarchy seems more suitable if we want a big_op library that is really operator centric as in mathcomp?