Zulip Chat Archive

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.

Reid Barton (Sep 03 2020 at 08:30):

#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]

I feel bad about that.

Lucas Allen (Sep 03 2020 at 21:33):

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.


Last updated: Dec 20 2023 at 11:08 UTC