rw definition with parameter leads to weird state

Stream: general

[Bolton Bailey]

Hey, here's an mwe. I would like Lean to think of A as a natural fixed parameter throughout the file, and three_A as another natural which depends on A, rather than as a function which can be applied to other values like B. Is there some way to get the rewrite in h2 and the goal to not happen?

import data.nat.basic

section my_section

parameter (A : ℕ)

def three_A := 3 * A

example (B : ℕ) (h1 : 3 * A = 0) (h2 : 3 * B = 0) :
  3 * B = 0
:=
begin
  rw <-three_A at *,
end

end my_section

[Eric Rodriguez]

oh god, the hack that rw does isn't nice

[Eric Rodriguez]

what's your reason for doing this?

[Mario Carneiro]

Unfortunately parameters don't work in tactic blocks. It should work if you introduce them like let three_A := three_A in begin ... outside the tactic block

[Bolton Bailey]

Eric Rodriguez said:

what's your reason for doing this?

One reason is simply that the expression 3 * A is large in my code and I'd like to look at something more simple. Another reason (and I'm not sure this is right so please tell me if I'm wrong) is that I do a lot of simplification of expressions with 3 * A by expressions with 3 * A, and I was hoping it might run faster if it didn't have to match the whole complicated 3 * A expression, it would make the code faster.

[Bolton Bailey]

Mario Carneiro said:

Unfortunately parameters don't work in tactic blocks. It should work if you introduce them like let three_A := three_A in begin ... outside the tactic block

Thanks, I'll try this

[Mario Carneiro]

Another workaround is to use three_A A in tactics