Intended way to add local declaration to local context

Stream: metaprogramming / tactics

[Bhavik Mehta]

In my tactic, I'd like to add a have statement, which in my understanding means adding something to the LocalContext. Poking around that API, I see docs#Lean.LocalContext.addDecl, but this isn't meant to be used directly. I also see that I can do evalTactic (← (tactic| have ...))`, but this feels too high-level to be the right solution. What's the intended API / method for this?

[Mario Carneiro]

docs#Lean.MVarId.intro1P probably

[Mario Carneiro]

see also docs#Mathlib.Tactic.haveLetCore

[Thomas Murrills]

I think you might be looking for docs#Lean.MVarId.assertHypotheses and friends!

[Mario Carneiro]

and docs#Lean.MVarId.assert

[Bhavik Mehta]

I don't think intro1P is what I'm looking for, but the other three suggestions look very helpful. What's the distinction between haveLetCore and assert(Hypotheses)?

[Mario Carneiro]

haveLetCore is halfway to a tactic frontend, notice that it takes Syntax arguments

[Mario Carneiro]

docs#Lean.MVarId.note is also basically have, using its ancient name

[Bhavik Mehta]

(deleted)

[Thomas Murrills]

Mario Carneiro said:

docs#Lean.MVarID.note is also basically have, using its ancient name

Ohh, I was wondering about that!

[Mario Carneiro]

once upon a time note was the tactic and have was the term. We're talking lean 3.1 or so

[Bhavik Mehta]

note seems to do what I want, thank you! (Although it's slightly confusing to me that I'm changing the mvar, and I don't know what the first argument it returns is...)

[Mario Carneiro]

most "MetaM tactics" take and return an MVarId

[Mario Carneiro]

that's basically your current goal state

[Mario Carneiro]

you thread it around explicitly, and the number of MVarIds you get back is the number of subgoals

[Bhavik Mehta]

Ah, including the local context. So the idea is that I'm meant to pass around this MVarId (presumably with the same name), and rewrite over the old ones? Isn't this exactly what a state monad is meant to handle for me?

[Mario Carneiro]

note returns an FVarId as well (which exists in the returned MVarId goal state), which refers to the hypothesis you've just created

[Mario Carneiro]

Bhavik Mehta said:

Ah, including the local context. So the idea is that I'm meant to pass around this MVarId (presumably with the same name), and rewrite over the old ones? Isn't this exactly what a state monad is meant to handle for me?

Yes, that state monad is called TacticM

[Mario Carneiro]

but what you lose with that monad is type soundness wrt subgoals as I mentioned. You can't tell the difference between a tactic that solves the goal and one which operates on two goals and produces three subgoals, they all have the same type

[Bhavik Mehta]

Right okay, this is why the input type of docs#Lean.Elab.Tactic.liftMetaFinishingTactic is what it is

[Mario Carneiro]

and you are never really sure whether you even have a main goal

[Mario Carneiro]

which impacts how type checking works since every expression has to elaborate in the context of the appropriate goal

[Bhavik Mehta]

I think I see, so the state monad I wanted does exist but it's more precise in some sense to handle these things by hand

[Mario Carneiro]

same thing with FVarIds, the local context is stored in the state but you want to hold on to FVarIds as "handles" to them so that you don't get confused and have to go find them again by name and worry about shadowing and not finding the right one later etc

[Bhavik Mehta]

Just to be clear, the local context is stored in the state of MetaM (which I presume is some ReaderT/StateT/IO stack), or in the state of TacticM? edit, just found the answer to this in the metaprogramming book, it's in the state of MetaM

[Mario Carneiro]

The local context is in the read only state of MetaM

[Mario Carneiro]

this is why anything that changes the local context will be in a callback shape

[Bhavik Mehta]

Am I to read that as docs#ReaderT.adapt, or something else? I don't quite see the callback shape in docs#Lean.MVarId.note, unless it's the MVarId passing (and even then I don't really see how that's a callback shape)

[Mario Carneiro]

ah, good point

[Mario Carneiro]

I believe it actually isn't changing the local context (it can't), which means you probably have to do mvar.withContext immediately after the note call on the mvar you get back if you want to make use of the fvarid and generally do things in the new context

[Mario Carneiro]

and docs#Lean.MVarId.withContext is hopefully more obviously in a callback shape

[Bhavik Mehta]

I think this makes sense, thanks!