Zulip Chat Archive

Stream: new members

Topic: proving a + a = 2* a


view this post on Zulip Atze van der Ploeg (Jan 11 2019 at 10:53):

I'm trying to prove the shocking lemma ∀ n : ℕ, n + n = 2*n , how do i tell lean to unfold the definition of *?

view this post on Zulip Kenny Lau (Jan 11 2019 at 10:59):

you don't; you just tell Lean what you want it to unfold to

view this post on Zulip Chris Hughes (Jan 11 2019 at 10:59):

There's a lemma nat.mul_succ

view this post on Zulip Rob Lewis (Jan 11 2019 at 11:00):

You can use simp only [(*)]. This will unfold the notation, then you'll have to deal with the definition nat.mul.

view this post on Zulip Chris Hughes (Jan 11 2019 at 11:00):

Sorry, nat.succ_mul

view this post on Zulip Rob Lewis (Jan 11 2019 at 11:00):

You can unfold that with the same method, or unfold nat.mul, but since it's defined by recursion on n, you'll have to use induction first.

view this post on Zulip Chris Hughes (Jan 11 2019 at 11:01):

You can't actually unfold multiplication in this scenario, since it's defined by recursion on the second argument.

view this post on Zulip Kenny Lau (Jan 11 2019 at 11:01):

well I imagined he would do induction on n

view this post on Zulip Atze van der Ploeg (Jan 11 2019 at 12:05):

Thanks, nat.succ_mul works fine, or using mul_comm but this requires me to know that nat.mul is defined by recursively on the second argument.

view this post on Zulip Kevin Buzzard (Jan 11 2019 at 12:23):

You can just use the 'ring' tactic if you don't care about what the low level proof looks like

view this post on Zulip Mark Dickinson (Jan 11 2019 at 18:40):

There's also two_mul in the standard library:

two_mul :  {α : Type u_1} [_inst_1 : semiring α] (n : α), 2 * n = n + n

Last updated: May 13 2021 at 18:26 UTC