## Stream: new members

### Topic: How does instantiate_vars work?

#### Lucas Allen (Sep 03 2020 at 07:34):

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 (Sep 03 2020 at 07:44):

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 (Sep 03 2020 at 08:18):

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

#### Reid Barton (Sep 03 2020 at 08:20):

(∀ {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 (Sep 03 2020 at 08:27):

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 (Sep 03 2020 at 08:29):

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.

#mwe?

#### Lucas Allen (Sep 03 2020 at 08:30):

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 (Sep 03 2020 at 08:36):

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

#### Lucas Allen (Sep 03 2020 at 08:40):

open_pis might be what I want.

#### Lucas Allen (Sep 03 2020 at 08:40):

I'll check it out. Thanks.

#### Mario Carneiro (Sep 03 2020 at 13:44):

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 (Sep 03 2020 at 21:32):

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]