Failure with `can_lift`

Stream: general

[Yury G. Kudryashov]

The following #mwe fails:

import data.option.basic
import algebra.group.with_one
import tactic.lift

variables {α : Type*}
@[to_additive]
instance with_one.can_lift : can_lift (with_one α) α :=
{ coe := coe,
  cond := λ a, a ≠ 1,
  prf := λ a ha, let ⟨b, hb⟩ := with_one.ne_one_iff_exists.1 ha in ⟨b, hb.symm⟩ }

namespace with_zero

instance [group α] : group_with_zero (with_zero α) :=
{ inv_zero := inv_zero,
  mul_inv_cancel := by { intros a ha, lift a to α using ha },
  .. with_zero.monoid_with_zero, .. with_zero.has_inv, .. with_zero.nontrivial
}

end with_zero

[Yury G. Kudryashov]

Here is the error:

16:39: invalid simplification lemma 'with_zero.can_lift' (use command 'set_option trace.simp_lemmas true' for more details)
state:
α : Type u_1,
_inst_1 : group α,
a : with_zero α,
ha : a ≠ 0
⊢ a * a⁻¹ = 1

[Yury G. Kudryashov]

@Mario Carneiro ?

[Yury G. Kudryashov]

@Floris van Doorn ?

[Mario Carneiro]

This appears to be an interaction with the @[to_additive] attribute

[Mario Carneiro]

the lift tactic tries to use simp to rewrite with the equation lemma for with_zero.can_lift but @[to_additive] doesn't create one

[Mario Carneiro]

it works fine if you write the zero version manually:

instance with_one.can_lift : can_lift (with_one α) α :=
{ coe := coe,
  cond := λ a, a ≠ 1,
  prf := λ a ha, let ⟨b, hb⟩ := with_one.ne_one_iff_exists.1 ha in ⟨b, hb.symm⟩ }

instance with_zero.can_lift : can_lift (with_zero α) α :=
{ coe := coe,
  cond := λ a, a ≠ 0,
  prf := λ a ha, let ⟨b, hb⟩ := with_zero.ne_zero_iff_exists.1 ha in ⟨b, hb.symm⟩ }
attribute [to_additive] with_one.can_lift

[Yury G. Kudryashov]

Thank you

[Yury G. Kudryashov]

@Gabriel Ebner Do we have an API to actually add these lemmas in @[to_additive]?

[Yury G. Kudryashov]

It seems that I add these lemmas but Lean doesn't know that they're special.

[Mario Carneiro]

I think there is an API for setting the equation lemmas?

[Mario Carneiro]

environment.add_eqn_lemma