Zulip Chat Archive

Stream: general

Topic: rw definition with parameter leads to weird state


Bolton Bailey (Sep 12 2021 at 13:13):

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 (Sep 12 2021 at 13:44):

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

Eric Rodriguez (Sep 12 2021 at 13:44):

what's your reason for doing this?

Mario Carneiro (Sep 12 2021 at 13:47):

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 (Sep 12 2021 at 13:49):

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 (Sep 12 2021 at 13:50):

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 (Sep 12 2021 at 14:00):

Another workaround is to use three_A A in tactics


Last updated: Dec 20 2023 at 11:08 UTC