instantiate_nth_var

Stream: general

[Alex J. Best]

I'm really surprised by the following behavior of docs#expr.instantiate_nth_var

run_cmd (do l ← (`(∀ l m t: ℕ, (l < t → 0 < t)) : expr).match_pi,
  let body := l.2.2.2,
  trace body,
  trace $ body.instantiate_nth_var 2 `(7),
  trace $ body.instantiate_nth_var 0 `(7),
  return () )

is this a bug, or am I just confused by the doc string "instantiate_nth_var n a b takes the nth de-Bruijn variable in a and replaces each occurrence with b.", I would have thought that nth de-Bruijn variable means the variable of index n, but does it instead mean nth starting from the minimal index in the expr?

[Alex J. Best]

Actually I'm confused why the variable prints as #2 at all, maybe that is the bug here?

[Floris van Doorn]

This is normal behavior for de Bruijn variables.
With de Bruijn variables, #n refers to the n-th quantification encapsulating it (counting from inside-out). So #0 refers to the innermost quantifier, etc.
An example can be illuminating here. The formula

∀ x, ∀ y, x = y → ∀ z, x + z = y + z

could be written using de Bruijn variables as

∀ _, ∀ _, #1 = #0 → ∀ _, #2 + #0 = #1 + #0

Note that the first x represented as #1 and the second x as #2, since there's an extra quantifier around it.

[Floris van Doorn]

So body.instantiate_nth_var 0 replaces the first (zeroth?) de Bruijn variable that is not captured by any quantifiers. Since the #2 is inside the scope of two quantifiers, it is considered to be the first free variable, and so is replaced by body.instantiate_nth_var 0.

[Alex J. Best]

Thanks Floris!

[Patrick Massot]

I think I already understood de Bruijn indices before, but this example is definitely the clearest explanation I've ever seen!

[Patrick Massot]

I'm sure that guy even knows how to pronounce de Bruijn for real!

[Alex J. Best]

Ok, my original bug was something else actually which still confuses me, if I replace de Bruijn variables with other de Bruijn variables I see different behavior:

run_cmd (do l ← (`(∀ l m t: ℕ, (l < t → 0 < t)):expr).match_pi,
  let body := l.2.2.2,
  trace body, -- ℕ → ∀ (t : ℕ), #2 < t → 0 < t
  trace $ body.instantiate_vars (list.repeat (expr.var 0) 3), -- ℕ → ∀ (t : ℕ), #2 < t → 0 < t
  trace $ body.instantiate_nth_var 0 (expr.var 0), --ℕ → ∀ (t : ℕ), #2 < t → 0 < t
  return () )

is the lesson here that I just shouldn't do such a weird thing? Or is there a mechanic here I can still understand to do what I'm trying.

[Floris van Doorn]

Probably these operations increase the free de Bruijn variables in the expression you're substituting in (i.e. expr.var 0) as well whenever you enter a quantifier (so that the free de Bruijn variables stay free in the substituted expression).
This is usually what you want. If it didn't do that, let's consider my above example formula, with one fewer quantifier:

∀ _, #1 = #0 → ∀ _, #2 + #0 = #1 + #2

Now there is one free variable (occurring twice), and suppose I syntactically replaced both those occurrences by #1. Then in the first occurrence this #1 would stay a free variable, but in the second occurrence it would become a bound variable. This is usually not what you want.

This smells like there is some #xy going on here.
However, docs#expr.replace might be able to help you here, since there nat argument supplies in how many quantifiers you are (so I suspect that function will not automatically increase free de Bruijn variables).

[Alex J. Best]

Yes this makes sense, and you are right there is definitely some #xy here, I can work around this to do what I want (thanks for reminding me about replace though, that might be a better way). I just wanted to try and understand this behavior, what you've said makes a lot of sense though, thanks :smile:

[Rob Lewis]

@Alex J. Best are you sure you want to be manipulating free variables? For anything that isn't performance critical, https://leanprover-community.github.io/mathlib_docs/tactic/binder_matching.html is usually way easier to use.

[Alex J. Best]

Well for what I wanted to do I didn't mind so much which order the binders came in, so I was just trying to replace them all with the same thing, so I could see if they were equal up to reordering of binders, I couldn't find a name for this concept, I'm also not sure its particularly sensible! But it would be fairly performance critical I think