Christopher Hoskin

Stream: new members

[Christopher Hoskin]

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]

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]

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]

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

[Alex J. Best]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

nat_vs_int.gif

[Christopher Hoskin]

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]

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]

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