Zulip Chat Archive

Stream: maths

Topic: how to use the pow_add theorem


Truong Nguyen (Sep 02 2018 at 19:10):

Dear Alls,
The pow_add theorem is as follow:

#check pow_add
pow_add : ∀ (a : ?M_1) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n

By why can't I prove the consequence theorem:

theorem th01 (a: ℕ ): ∀ m n:ℕ, a ^ (m + n) = (a ^ m) * (a ^ n) :=
begin
rw pow_add (a:ℕ)
end

Here is the error that I got:

rewrite tactic failed, did not find instance of the pattern in the target expression
a ^ (?m_1 + ?m_2)
Thank you,

Kenny Lau (Sep 02 2018 at 19:13):

(deleted)

Chris Hughes (Sep 02 2018 at 19:14):

It's because you need to use nat.pow_add

Kenny Lau (Sep 02 2018 at 19:15):

because the ^ are different

Mario Carneiro (Sep 02 2018 at 19:15):

nat has a different instance for the power function, so it has its own theorems to go with it, like nat.pow_add

Chris Hughes (Sep 02 2018 at 19:15):

This is a very annoying feature of current lean. There are two definitions of pow on the naturals.

Mario Carneiro (Sep 02 2018 at 19:16):

If nat.pow_add was not proven, you could also use by simpa using pow_add a to prove it

Truong Nguyen (Sep 02 2018 at 19:21):

Dear Mario,
can you be more specific, what is by simpa using pow_add a.

Truong Nguyen (Sep 02 2018 at 19:24):

I changed to this:

theorem th01 (a: ℕ ): ∀ m n:ℕ, a ^ (m + n) = (a ^ m) * (a ^ n) :=
begin
rw [nat.pow_add (a:ℕ )]
end

But, it did not work neither.

Mario Carneiro (Sep 02 2018 at 19:26):

import algebra.group_power

theorem th01 (a m n : ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
by simpa using pow_add a m n

Mario Carneiro (Sep 02 2018 at 19:27):

theorem th01 (a m n : ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
by rw nat.pow_add

Mario Carneiro (Sep 02 2018 at 19:27):

theorem th01 (a m n : ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
nat.pow_add _ _ _

Mario Carneiro (Sep 02 2018 at 19:28):

note that you need to have all the variables left of the colon for rw to work here

Truong Nguyen (Sep 02 2018 at 19:55):

Oh, great
Do you know how can I find the tutorial of using "simpa".

I have the following issue as well. I think it can be done in similar way.

How to use the theorem:
#check cardinal.mul_power
cardinal.mul_power : (?M_1 * ?M_2) ^ ?M_3 = ?M_1 ^ ?M_3 * ?M_2 ^ ?M_3

To prove that:
theorem th07 (a b n: \N): (a * b)^n = a ^n*b^n.

Mario Carneiro (Sep 02 2018 at 20:00):

That is an unrelated use of power; although it is possible it would be a weird way to prove that theorem for natural numbers

Mario Carneiro (Sep 02 2018 at 20:01):

the theorem itself is nat.mul_pow

Truong Nguyen (Sep 02 2018 at 20:04):

when I run the command:
#check nat.mul_pow

it gave me nothing.

Patrick Massot (Sep 02 2018 at 20:10):

you need to import https://github.com/leanprover/mathlib/blob/dd0c0aeefcaf6a438ab4273d7a1f42e1b8225847/data/nat/basic.lean

Patrick Massot (Sep 02 2018 at 20:11):

import data.nat.basic

Truong Nguyen (Sep 03 2018 at 16:22):

Hello,
do you know where can I find the tutorial of using "simpa".

Patrick Massot (Sep 03 2018 at 16:23):

I think we don't have anything better than https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#simpa

Truong Nguyen (Sep 03 2018 at 17:17):

Oh, thank you


Last updated: Dec 20 2023 at 11:08 UTC