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

Stream: new members

[Rémy Degenne]

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]

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

[Rémy Degenne]

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]

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

[Rémy Degenne]

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]

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]

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]

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]

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]

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]

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]

mathematicians are scared of \lam ;-)

[Reid Barton]

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]

well I'll try to come up with a MWE

[Reid Barton]

Maybe the issue is somewhere in the form of hypotheses_f

[Rémy Degenne]

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.