Zulip Chat Archive

Stream: new members

Topic: replace (f x) by ((\lam x, f x) x)

Rémy Degenne (Nov 18 2020 at 13:21):

Is there a way that does not involve change to replace f x by (\lam x, f x) x in the goal? The change command causes a deterministic timeout. The reason I want to do that is to use rw to replace f by something else.

Shing Tak Lam (Nov 18 2020 at 13:28):

Does change f x with (λ x, f x) x work?

Rémy Degenne (Nov 18 2020 at 13:29):

I does, thanks. I did not know that I could use change like that. I used it only to change the whole goal.

Rémy Degenne (Nov 18 2020 at 13:33):

correction : it worked for one of the two functions I wanted to replace. The second one still causes a timeout.

Rémy Degenne (Nov 18 2020 at 13:47):

Well it is possible that the timeout was caused by another change further down that was rendered invalid by my modifications, so ignore that. My experience with change so far is that when it does not succeed, its most common failure state is to cause a timeout.

Reid Barton (Nov 18 2020 at 13:49):

change needs to check that the new thing is definitionally equal to the old one, and when it isn't definitionally equal there might be a lot of unfolding of definitions that can be done before it gives up.

Kevin Buzzard (Nov 18 2020 at 14:54):

Note also that unless you are doing something like rewriting, you might not need to change anything. Why do you want to change f x into the "more complicated" lambda term?

Reid Barton (Nov 18 2020 at 14:56):

The original message says "to use rw" but I'm sill a little confused why it's needed unless the lemma in question explicitly has the form (\lam x, f x) = ..., which seems unusual

Rémy Degenne (Nov 18 2020 at 15:04):

my lemma has the form f = \lam x, ..., valid for functions f:alpha -> ennreal under some hypotheses and I have a goal of the form f x * g x = ... for some functions f and g. I wanted to do rw lemma_name hypotheses_f to replace f, then rw lemma_name hypotheses_g to replace g. But that does not work. If I replace f x by (\lam x, f x) x, it does.

Kevin Buzzard (Nov 18 2020 at 15:05):

Why not make x an additional input and make your lemma f x = ...? This would be more like the standard mathlib style I guess.

Rémy Degenne (Nov 18 2020 at 15:09):

yes I can also do that. It looked more natural to me to write that the function itself was equal to another function, but if coding in mathlib is easier with the f x = ... formulation, that is the way I will write it from now on.

Kevin Buzzard (Nov 18 2020 at 15:09):

mathematicians are scared of \lam ;-)

Reid Barton (Nov 18 2020 at 15:09):

But also if you're rewriting in the forward direction then I don't see why you wouldn't be able to just rewrite f without turning it into a lambda first.

Rémy Degenne (Nov 18 2020 at 15:10):

well I'll try to come up with a MWE

Reid Barton (Nov 18 2020 at 15:10):

Maybe the issue is somewhere in the form of hypotheses_f

Rémy Degenne (Nov 18 2020 at 15:20):

I think you are right : there are some coercions in the hypotheses that could perhaps make it guess the wrong function, and when I give the function explicitly to the lemma instead of it being inferred, there is no issue any more.
I don't really understand why the change with the lambda worked, but I definitely need to fix that ambiguous lemma.

Last updated: Dec 20 2023 at 11:08 UTC