How does `instantiate_vars` work?

Stream: new members

[Lucas Allen]

Hola, in expr.lean there is the instantiate_vars meta constant. The docs say

/-- ``instantiate_vars `(#0 #1 #2) [x,y,z] = `(%%x %%y %%z)`` -/

However, when I try

variables x y z : expr
#eval instantiate_vars `(#0 #1 #2) [x,y,z]

I get a red squiggle under the #0 and the error, "don't know how to synthesize placeholder
context". How do I get this to work?

[Lucas Allen]

If I try

variables x y z : expr
#eval instantiate_vars `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) [x,y]

I get the error "cannot evaluate function: 0 arguments given but expected 2." I don't understand what's happening.

[Reid Barton]

What exactly are you trying to do? Something like your last example?

[Reid Barton]

`(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) is an expr.pi, whose body is another expr.pi, whose body is some other expression we'll call e. If you called instantiate_vars e [x,y] then you'd get an expression with x and y substituted for a and b, not sure in what order.

[Lucas Allen]

Yeah, basically given an expr I want to determine whether one of the leading expr.pi's is a proposition. So for the example `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) I'd want false for the first two expr.pi's and true for the last two. But when I try infer_type it tells me to replace the variables with local constants.

[Lucas Allen]

I tried

meta def remove_pis : expr → expr
| (expr.pi var_name bi αₙ b) := remove_pis b
| e := e

#eval trace (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))

Which gives me "#3 ↔ #2", then

#eval instantiate_vars (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))) [x,y]

gives me a red squiggle under the #eval and the error "cannot evaluate function: 0 arguments given but expected 2". I don't understand what this means and how to fix it.

[Reid Barton]

#mwe?

[Lucas Allen]

open tactic
open expr

meta def remove_pis : expr → expr
| (expr.pi var_name bi αₙ b) := remove_pis b
| e := e

#eval trace (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))
#eval instantiate_vars (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))) [x,y]

[Rob Lewis]

You're probably looking for https://leanprover-community.github.io/mathlib_docs/tactic/binder_matching.html

[Lucas Allen]

open_pis might be what I want.

[Lucas Allen]

I'll check it out. Thanks.

[Mario Carneiro]

The notation #0 is sometimes used in the documentation to denote expr.var 0, but there is no concrete syntax for this that the parser will accept

[Lucas Allen]

I think I forgot the variables in the MWE.

open tactic
open expr

meta def remove_pis : expr → expr
| (expr.pi var_name bi αₙ b) := remove_pis b
| e := e

variables x y z : expr
#eval trace (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))
#eval instantiate_vars (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))) [x,y]

I feel bad about that.

[Lucas Allen]

Mario Carneiro said:

The notation #0 is sometimes used in the documentation to denote expr.var 0, but there is no concrete syntax for this that the parser will accept

Ok, so it's not possible to get the example in the docs to work.