Stream: new members

Topic: Christopher Hoskin

Christopher Hoskin (Dec 22 2020 at 16:36):

Hello, I'm a new member. I've recently started learning lean, and so far have mostly been able to solve my own problems. However, here is something that has me stumped:

import algebra.module.linear_map

universes u

variables {A : Type u} [add_comm_monoid A] [semimodule ℤ  A]

lemma test (T : linear_map ℤ A A)  (a  : A) : 2 • (T a) = T (2 • a)  :=
begin
rw T.map_smul 2 a,
end


Lean says rewrite tactic failed, did not find instance of the pattern in the target expression ⇑T (2 • a).

Why does this not work?

Christopher

Alex J. Best (Dec 22 2020 at 16:41):

When you write 2 lean treats it as the natural number 2, rather than the integer 2, which is ok as A is an add_comm_monoid, so multiplication by a nat is well defined even without the semimodule structure.

Alex J. Best (Dec 22 2020 at 16:41):

import algebra.module.linear_map

universes u

variables {A : Type u} [add_comm_monoid A] [semimodule ℤ  A]
set_option pp.all true
lemma test (T : linear_map ℤ A A)  (a  : A) : (2:ℤ) • (T a) = T ((2:ℤ) • a)  :=
begin
rw T.map_smul (2:ℤ) a,
end


Alex J. Best (Dec 22 2020 at 16:42):

If we use (2 : ℤ) instead everything works as expected

Alex J. Best (Dec 22 2020 at 16:43):

When you see something like rewrite tactic failed, did not find instance of the pattern in the target expression one debugging tool is to turn off all pretty printing (notation, implicit arguments etc) so you an see what lean thinks is really going on. Thats the line set_option pp.all true I added.

Alex J. Best (Dec 22 2020 at 16:44):

You'll see that everything is almost unreadable with pretty printing turned off but when two things look the same in the pretty printer (like integer 2 and natural number 2) this really helps you notice.

Alex J. Best (Dec 22 2020 at 16:45):

The original lemma you stated is still true of course, and simp proves it for you btw

Patrick Massot (Dec 22 2020 at 16:47):

Using pp.all true is the last desperate move to try though. Using widget inspection is much cheaper.

nat_vs_int.gif

Christopher Hoskin (Dec 22 2020 at 17:49):

Thanks - if this was a step in a longer proof, is there a way to cast to integers before doing the rewrite? A somewhat artificial example:

lemma test2 (T : linear_map ℤ A A)  (a : A) : T (a+a) = (2:ℤ) • T a :=
begin
rw ← two_nsmul,
rw_mod_cast T.map_smul 2 a,
end


I was hoping something like rw_mod_cast would work here, but it seems not.

Alex J. Best (Dec 22 2020 at 18:30):

I think simp alone worked for your first example, if you do squeeze_simp you can see what simp used to rewrite, it may be that map_smul just isnt the right lemma when naturals are involved

Christopher Hoskin (Dec 22 2020 at 19:02):

Thanks again. It looks like simp was using linear_map.map_smul_of_tower

lemma test (T : linear_map ℤ A A)  (a  : A) : 2 • (T a) = T (2 • a)  :=
begin
simp only [linear_map.map_smul_of_tower]
end


simp isn't able to convert the \N scalar product to the \Z one though:

lemma testn (T : linear_map ℤ A A)  (a  : A) : 2 • (T a) = T (a+a)  :=
begin
rw ← two_nsmul,
simp,
end


My work around is to introduce a new result two_gsmul  instead:

theorem two_gsmul (a : A) : 2 • a = a + a :=
@pow_two (multiplicative A) _ a

lemma test2 (T : linear_map ℤ A A)  (a : A) :  2 • (T a) = T (a+a) :=
begin
rw ← two_gsmul,
simp,
end


Christopher

Last updated: May 08 2021 at 18:17 UTC