mk_local_const : name -> pexpr?

Stream: general

[Zesen Qian]

Is there such a function that give a pexpr of local constant from the variable name? I can just call expr.local_const, but the constructor is kind of complex and not so much documentation, also I don't think it's the way to go.

[Mario Carneiro]

There is mk_const, but one way or another you have to decide what to do about universe variables

[Zesen Qian]

sorry, what's the difference between const and local_const? also, I'm trying to work without the tactic monad.

[Mario Carneiro]

const is a global constant, which is declared by a def or theorem or axiom, like nat or nat.succ or nat.succ_pos

[Mario Carneiro]

local_const is a "local constant" which is probably less than helpful but you would usually think of it as a variable. These are the variables that appear in the context during a tactic proof, left of the turnstile

[Zesen Qian]

ahh I see.

[Zesen Qian]

yeah, so I guess I'm trying to create a reference to local constant, from a string.

[Mario Carneiro]

This is in contrast to var which is a de bruijn variable, which are variables which are currently bound in a binder in a term

[Zesen Qian]

I can create name by mk_simple_name, but from that to expr I don't know.

[Mario Carneiro]

You can't make a local constant from a string without the local context

[Mario Carneiro]

that is what enables name resolution

[Zesen Qian]

ok, so I need to be in a tactic.

[Zesen Qian]

monad.

[Mario Carneiro]

right

[Mario Carneiro]

you want get_local I think

[Zesen Qian]

yes, I saw that.

[Zesen Qian]

and I was wondering why it's implemented in VM, if it can be implemented natively.

[Zesen Qian]

and now I know why.

[Mario Carneiro]

You need that local context information to find out the unique name and type given the pp name

[Mario Carneiro]

this is what the tactic_state provides

[Zesen Qian]

ok. question: can I make a elet, getting a local_const, and pass it to the rest of the function, without access tactic state?

[Mario Carneiro]

Possibly, what are the inputs? You need a variable, a type, a value and a body

[Zesen Qian]

I want to construct a proof, which start with let v = ..., and I hope to get a expr refering to this v, and pass it to the rest of the proof generation.

[Zesen Qian]

is that viable?

[Mario Carneiro]

There are two ways you could proceed: you could construct the body containing v as a local_const, and then abstract it when you are finished, or you could construct it with v already abstracted, meaning you refer to it only as var 0

[Mario Carneiro]

Lean is mostly geared toward constructing terms the first way, particularly if you intend for the expression to be constructed partially using tactics, with a metavariable in the middle etc. Most tactics only work on "closed terms", meaning that var is not allowed

[Mario Carneiro]

But if you can construct the entire expr in one go with no intervention then the second approach is possible

[Zesen Qian]

thanks, I'll try

[Zesen Qian]

very much appreciated.

[Sebastian Ullrich]

Please also note https://github.com/leanprover/lean/issues/1921#issuecomment-363028776. This distinction between "pure" and "tactic" local constants will likely vanish in Lean 4. As well as the name "local constant".

[Simon Hudon]

Do you mean that this kind of type won't leak through into the Lean code?