Zulip Chat Archive

Stream: new members

Topic: Christopher Hoskin


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Alex J. Best (Dec 22 2020 at 16:42):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 22 2020 at 16:49):

nat_vs_int.gif

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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