Zulip Chat Archive

Stream: new members

Topic: How does `instantiate_vars` work?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 03 2020 at 08:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 03 2020 at 08:30):

#mwe?

view this post on Zulip 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]

view this post on Zulip Rob Lewis (Sep 03 2020 at 08:36):

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

view this post on Zulip Lucas Allen (Sep 03 2020 at 08:40):

open_pis might be what I want.

view this post on Zulip Lucas Allen (Sep 03 2020 at 08:40):

I'll check it out. Thanks.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 08 2021 at 10:12 UTC