controlling names of bound variables in InfoView

Stream: new members

[Yannick Seurin]

Is there a way to control the naming of bound variables in InfoView? Say I have a long proof involving tsum's and I want to keep notation consistent through rewrites, what are the possible options? For example, consider:

import Mathlib

example (f : ℝ × ℝ → ENNReal) : ∑' (p : ℝ) (q : ℝ), f (p, q) = 1 := by
  rw [ENNReal.tsum_comm]
  change ∑' (q : ℝ) (p : ℝ), f (p, q) = 1
  sorry

The rewrite changes bound variables to a and b because that's what ENNReal.tsum_comm uses. Is there a simpler way to tell Lean to keep p and q than using change afterwards? I guess I could also do a calc proof but that's not very convenient either...

[Aaron Liu]

there's a gadget for this

[Aaron Liu]

docs#binderNameHint

[Yannick Seurin]

Thanks! The documentation is a bit cryptic to me though, and I couldn't find any example of how it should be used in Mathlib...

[Robin Arnez]

Yeah, it isn't used much because not many people know about it and it's a bit weird to use:

import Mathlib

theorem ENNReal.tsum_comm'.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β → ENNReal} :
    ∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), binderNameHint b (f a) (binderNameHint a f (f a b)) :=
  ENNReal.tsum_comm

example (f : ℝ × ℝ → ENNReal) : ∑' (p : ℝ) (q : ℝ), f (p, q) = 1 := by
  rw [ENNReal.tsum_comm']
  sorry

works here.

[Yannick Seurin]

Nice, thanks! It works, but not very convenient to do this manually for all theorems you'd want to use...

Out of curiosity, would it be complicated/impossible to make it the default behavior of InfoView? (I mean, having rewrites and simps keep the same bound variables appearing in InfoView rather than the ones used in the statement of the theorem passed to rw?)

[Jovan Gerbscheid]

Well, there is no way to really tell which bound variable turned into which bound variable. Hence why we have the binderNameHint to give a hint about this :)

[Mirek Olšák]

Really? I think there could be more effort to automatically keep the bound variable names when rw tries to match a theorem to the target.

[Jovan Gerbscheid]

Do you think there could be a way to automatically figure out where the binderNameHints are supposed to be?

[Mirek Olšák]

Of course it would be some heuristic that doesn't work in every case, but usually, you don't want to use the bound variable names from the theorem, and rather find them in the target expression.

[Mirek Olšák]

I can see two ideas for ENNReal.tsum_comm

1. Look at the matched expression, there we matched bound a in the theorem against p in the target, and b in the theorem against q in the target. So we can remember a => p, b => q, and use the same names for the other binders in the theorem using a, b.
2. We matched f to be applied to some bound variables. So if in the rhs expression, it is applied to bound variables again, we try to give them the same name.

[Mirek Olšák]

I guess I like the first option a little more, it feels more human in the sense that the author of the theorem can hint with equal names how the names are supposed to be rearranged.

[Robin Arnez]

I also thought about changing instantiateBetaRevRange. The idea is that if we infer the theorem type of ENNReal.tsum_comm, we'd have something like:

∑' (a : ℝ) (b : ℝ), (fun p q => f (p, q)) a b = ∑' (b : ℝ) (a : ℝ), (fun p q => f (p, q)) a b

But we automatically apply beta-reduction using instantiateBetaRevRange, so we get:

∑' (a : ℝ) (b : ℝ), f (a, b) = ∑' (b : ℝ) (a : ℝ), f (a, b)

But what if we remembered here that we beta-reduced fun p q => ... with bound variables a and b and then renamed a => p and b => q accordingly? Then we'd get:

∑' (p : ℝ) (q : ℝ), f (p, q) = ∑' (q : ℝ) (p : ℝ), f (p, q)

So the idea is that if every occurrence of such a beta-reduction with bound variables agrees on the binder name of the lambda, then we change the binder name. Just not sure how to best do this without sacrificing performance.

[Mirek Olšák]

That is what I meant with my suggestion no. 2, ,I know I was not very clear, thanks for making it clearer. What do you think about my suggestion no 1. that is:

After instantiating the theorem, the theorem is

∑' (a : ℝ) (b : ℝ), f (a, b) = ∑' (b : ℝ) (a : ℝ), f (a, b)

and the expression we are rewriting is

(∑' (p : ℝ) (q : ℝ), f (p, q))

from that, we can deduce that a should be renamed to p, and b to q in. Following this name rewrite also on the RHS, we obtain

 ∑' (q : ℝ) (p : ℝ), f (p, q)

[Robin Arnez]

Hmm I'm not sure how much sense it would make to implement the first option. Since we use reducible defeq to unify with the lhs we'd need to add something to defeq that records the names of the lhs and rhs. However, we usually skip a costly defeq if we have expressions a == b. But if we want to record names, we'd still need to recurse over the expression to figure out name correspondences (how deep, should we visit proof terms? Implicit arguments? Instance arguments?). Also since we use reducible defeq, what if we expose a binder by unfolding? Do we still count that as a binder to record if we find a correspondence? Also, on the right hand side, which binders should be replaced? What about proof terms, implicit arguments, etc.?

[Mirek Olšák]

I though rw uses syntactic equality. And I agree that visiting hidden (implicit & typeclass) arguments is not necessary.

[Mirek Olšák]

On the other hand, some other rewrite tactics expand more, and it should still work for them...

[Mirek Olšák]

So back to the option 2. Could it be done by adding the naming hints only to the relevant theorems as Jovan mentioned? By the way, this should be done in each direction separately, I see quite unfortunate that binderNameHint breaks rw [←ENNReal.tsum_comm']

[Robin Arnez]

Well, if we actually changed instantiateBetaRevRange, then, after instantiating, the theorem is

∑' (p : ℝ) (q : ℝ), f (p, q) = ∑' (q : ℝ) (p : ℝ), f (q, p)

so it'd work both ways.
Note: the interesting instantiation / instantiateBetaRevRange call here would be

∑' (a : ℝ) (b : ℝ), #0 a b = ∑' (b : ℝ) (a : ℝ), #0 b a

with #0 -> fun p q => f (p, q)