Zulip Chat Archive

Stream: new members

Topic: rewriting and let


Robin Carlier (Jun 25 2021 at 18:56):

Hi ! stupid question, but is there a way to rewrite some equality that I defined using let? Say I have a goal foo = blah, and I do let bar := blah before_hand, how do I rewrite my goal as foo = bar?

Robin Carlier (Jun 25 2021 at 18:57):

I tried to just rw bar but Lean did not like it.

Ruben Van de Velde (Jun 25 2021 at 18:58):

change would work

Damiano Testa (Jun 25 2021 at 18:59):

I think that set [...] with h, instead of let, will produce a hypothesis h that you can use for rw.

Ruben Van de Velde (Jun 25 2021 at 18:59):

Alternatively, if you use set bar := blah with hbar,, you can use rw ←hbar,

Robin Carlier (Jun 25 2021 at 19:02):

Nice! So set works just like let? In practice, is it better to avoid let?

Ruben Van de Velde (Jun 25 2021 at 19:05):

I personally tend to avoid let, but I don't think that's mathlib policy, at least

Eric Rodriguez (Jun 25 2021 at 19:23):

I also tend to avoid let because of the aforementioned finickyness, but also simp_rw and simp only work to rewrite them

Robin Carlier (Jun 25 2021 at 19:30):

Thank you! I have a last silly question: is there a canonical syntax for turning an hypothesis of the form f = g where f and g are functions into an hypothesis of the form f x = g x (given some xin the domain of course)?

Eric Rodriguez (Jun 25 2021 at 19:31):

congr_fun?

Eric Rodriguez (Jun 25 2021 at 19:32):

(docs#congr_fun)

Robin Carlier (Jun 25 2021 at 19:35):

So something like have neq_hyp := congr_fun ...?

Robin Carlier (Jun 25 2021 at 19:35):

It works but I was just wondering if there was a way to make it directly act on my f = g hypothesis rather than adding a new one.

Eric Rodriguez (Jun 25 2021 at 19:36):

I mean, if it's a goal state you can just rw it at the goal

Eric Rodriguez (Jun 25 2021 at 19:37):

you could also do rw function.funext_iff at h, specialize h x, but at that point you may just write replace h := congr_fun h x

Robin Carlier (Jun 25 2021 at 19:38):

Oh, I was not aware of the replacesyntax! Looks like what I want!


Last updated: Dec 20 2023 at 11:08 UTC