Zulip Chat Archive

Stream: general

@[to_additive left_add_coset]
def left_coset [has_mul α] (a : α) (s : set α) : set α := (λ x, a * x) '' s

Kenny Lau (May 19 2020 at 20:06):

should this be a new definition with attribute [to_additive left_add_coset] left_coset afterwards?

Kenny Lau (May 19 2020 at 20:06):

because currently the additive version cannot be unfolded

Kenny Lau (May 19 2020 at 20:09):

import group_theory.coset

universe u

variables {G : Type u} [group G] (x : G) (s : set G)

lemma test1 : left_coset x s = left_coset x s ∧ 0 = 0 :=
by unfold left_coset -- (λ (x_1 : G), x * x_1) '' s = (λ (x_1 : G), x * x_1) '' s ∧ 0 = 0

variables {A : Type u} [add_group A] (y : A) (t : set A)

lemma test2 : left_add_coset y t = left_add_coset y t ∧ 0 = 0 :=
by unfold left_add_coset -- unfold tactic failed, left_add_coset does not have equational lemmas nor is a projection

Kenny Lau (May 19 2020 at 20:09):

or have we collectively decided that this isn't important?

Reid Barton (May 19 2020 at 20:10):

Maybe it's a bug that to_additive didn't copy the equational lemma? I don't know.

Kenny Lau (May 19 2020 at 20:11):

#print prefix left_coset
#print prefix left_add_coset

left_coset : Π {α : Type u_1} [_inst_1 : has_mul α], α → set α → set α
left_coset.equations._eqn_1 : ∀ {α : Type u_1} [_inst_1 : has_mul α] (a : α) (s : set α), left_coset a s = (λ (x : α), a * x) '' s

left_add_coset : Π {α : Type u_1} [_inst_1 : has_add α], α → set α → set α
left_add_coset.equations._eqn_1 : ∀ {α : Type u_1} [_inst_1 : has_add α] (a : α) (s : set α), left_add_coset a s = (λ (x : α), a + x) '' s

Kenny Lau (May 19 2020 at 20:11):

I think I've been told before that there is no way to make Lean recognize this as an equational lemma

Kenny Lau (May 19 2020 at 20:11):

because something something unsafe

Reid Barton (May 19 2020 at 20:15):

would it try to rename _eqn_1 to _eqn_0

Reid Barton (May 19 2020 at 20:16):

Oh, are you saying you can't just randomly create lemmas and then mark them as equational lemmas for an unrelated definition? That sounds fair

Mario Carneiro (May 19 2020 at 20:16):

When to_additive was written, there was no way to get at the eqn_lemmas data structure in lean. I'm not sure if that has since changed, but it is not sufficient that the theorem itself be transferred

Mario Carneiro (May 19 2020 at 20:17):

I don't think it's about something something unsafe but rather something something core is frozen

Kevin Buzzard (May 19 2020 at 20:28):

Fortunately I think it only renames one to zero

Kenny Lau (May 19 2020 at 20:30):

so my question is that, given the current situation, whether we should instead write:

def left_coset [has_mul α] (a : α) (s : set α) : set α := (λ x, a * x) '' s
def left_add_coset [has_add α] (a : α) (s : set α) : set α := (λ x, a + x) '' s
attribute [to_additive left_add_coset] left_coset

Kenny Lau (May 19 2020 at 20:30):

because that's what I'm doing with my next PR

Kenny Lau (May 19 2020 at 20:30):

which will feature a cleanup of algebra/free.lean

Kevin Buzzard (May 19 2020 at 20:31):

@Yury G. Kudryashov and @Amelia Livingston will know the ins and outs of to_additive.

Yury G. Kudryashov (May 19 2020 at 20:57):

Currently to_additive copies lemmas like _eqn* so that if you write another proof for multiplicative version, then to_additive can transfer this proof. @Gabriel Ebner can we tell Lean that these new lemmas are eqn_lemmas?

Gabriel Ebner (May 19 2020 at 21:37):

lean#254 I have no idea if we already copy/generate the sunfold lemmas, please check this. Otherwise there will be troubles when you copy definitions using pattern matching.

Kenny Lau (May 19 2020 at 21:53):

def foo : ℕ → ℕ
| 0 := 1
| (n+1) := match n with 0 := 2 | _ := 1 end

lemma foo.faux_eqn (n) : foo n = 42 := sorry

open tactic
run_cmd do
e ← get_env,
trace $ e.get_eqn_lemmas_for ``foo,
trace $ e.get_ext_eqn_lemmas_for ``foo,
set_env $ e.add_eqn_lemma ``foo.faux_eqn

#eval do
e ← get_env,
trace $ e.get_eqn_lemmas_for ``foo,
trace $ e.get_ext_eqn_lemmas_for ``foo

-- success: we've taught lean a new and exciting simp lemma!
example : ∀ n, foo n = 42 := by simp [foo]