Zulip Chat Archive

Stream: general

Topic: Failure with `can_lift`


Yury G. Kudryashov (Sep 26 2020 at 18:21):

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 (Sep 26 2020 at 18:23):

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 (Sep 26 2020 at 19:37):

@Mario Carneiro ?

Yury G. Kudryashov (Sep 26 2020 at 19:37):

@Floris van Doorn ?

Mario Carneiro (Sep 26 2020 at 19:45):

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

Mario Carneiro (Sep 26 2020 at 19:45):

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 (Sep 26 2020 at 19:46):

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 (Sep 26 2020 at 19:50):

Thank you

Yury G. Kudryashov (Sep 26 2020 at 19:55):

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

Yury G. Kudryashov (Sep 26 2020 at 19:56):

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

Mario Carneiro (Sep 26 2020 at 19:59):

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

Mario Carneiro (Sep 26 2020 at 19:59):

environment.add_eqn_lemma


Last updated: Dec 20 2023 at 11:08 UTC