Can I try a tactic during elaboration?

Stream: lean4

[Thomas Murrills]

For what I'm working on, I'd like to attempt a user-provided autoparam during elaboration, and if it fails, create a nicely-named goal. I'm not sure if this is actually possible during elaboration, as I'm not sure exactly when tactics are run.

If it's not possible, I'd maybe like to "add onto" the tactic at the expression level somehow (not the syntax level). Currently the code elaborates `(by $tacticSyntax), then uses the resulting expression. If I could build on that resulting expression appropriately, I'd be good—but I'm not sure how this would work, or what I should use.

An expression version of things like first and refine might be useful, as would the ability to combine tactics at the expression level.

Or, if I could at least refer to some hole via syntax with a particular identity, e.g. `(by first | $tacticSyntax | refine $hole) where I know that hole's mvarId (and could then assign it to what I want later), that would be useful too.

Any pointers are appreciated! :)

[Mario Carneiro]

at the expression level, you can do try ... catch to catch failure and let s <- saveState; ... ; s.restore to undo any modifications caused by the tactic. These can be used separately or together, and I think there is also an or-else combinator <|> which you can use to do the same thing as the first syntax

[Thomas Murrills]

hmm, when I say at the expression level, I mean directly building Exprs that correspond to (elaborated) tactics. this seems like what I'd write if I were writing a tactic directly, as opposed to building expressions. how do you turn these into Exprs? (or am I missing something obvious)

[Thomas Murrills]

ooh, actually your and Gabriel Ebner's comments in existsi for already elaborated Expr might cover what I need! That's what I was grasping for with "if I could at least refer to some hole via syntax with a particular identity" in the last part. I'll try doing something like that and seeing what happens.

[Moritz Doll]

I had the same question with zify and I am starting to wonder whether one possible answer to this general problem is 'create several helper-tactics and make your high level tactic a macro'?

[Thomas Murrills]

I’m having a little trouble using tactics during elaboration because of their relationship with metavariables. Metavariables created during the course of elaboration via mkFreshExprMVar are able to be assigned, e.g. by isDefEq in rfl, in contrast to metavariables that appeared directly in top-level syntax. Here, rfl is trying to prove something like ?x = ?y, and is unfortunately succeeding. (tracing isDefEq confirms that it regards the metavariables as assignable during elaboration.)

I thought this might be due to the metavariable context depth, and tried solving it by using withNewMCtxDepth do before by, but that doesn’t end well.

Is this actually a depth issue? Or can something else affect assignability?

Additional context: the code proceeds by extracting the tactic syntax, then:

...
let val ← elabTermEnsuringType (←`(by $tacticSyntax)) d
-- val is then used somewhere within the final expression
...

[Thomas Murrills]

I could potentially make these metavariables synthetic opaque, but I’m guessing then I’d have to somehow turn them back at the end after running the tactic (as these metavariables are going to go on to become goals), and I’m not totally sure how to do that either.

I guess if I could mimic the way that metavariables appearing in top-level syntax don’t get assigned, that would be best.

[Thomas Murrills]

Here's a minimal working example of the problem. Note that by rfl unifies ?x and ?y and leaves us with only one case, y, when I would hope for two cases and a tactic failure.

def frefl (x y : Nat) : (x = y) → Unit := fun _ => ()

elab "tryRfl" : term => do
  match (← inferType (← mkConst ``frefl)) with
  | .forallE _ a (.forallE _ b (.forallE _ c _ _) _) _ =>
    let x ← mkFreshExprMVar a .synthetic `x
    let y ← mkFreshExprMVar b .synthetic `y
    let c := c.instantiate #[y, x]
    mkAppM ``frefl #[x, y, ← elabTermEnsuringType (←`(by rfl)) c]
  | _ => unreachable!

example := by refine tryRfl; case y => exact 0

Contrast with using explicit metavariables in syntax:

example := by refine frefl ?x ?y (by rfl)
-- tactic 'rfl' failed, equality lhs ?x is not definitionally equal to rhs ?y ⊢ @Eq.{1} Nat ?x ?y

What's causing the difference here?

[Mario Carneiro]

Thomas Murrills said:

I could potentially make these metavariables synthetic opaque, but I’m guessing then I’d have to somehow turn them back at the end after running the tactic (as these metavariables are going to go on to become goals), and I’m not totally sure how to do that either.

Metavariables that are going to be goals should generally be synthetic-opaque, unless you are okay with them being solved en passant

[Mario Carneiro]

to change the kind of a metavariable, you can always make a new one with a different kind and assign the old one to it

[Mario Carneiro]

(for that specific modification I think you can just update the metavar context, but that technique works in general)

[Thomas Murrills]

ooh, ok, great! I had somehow acquired the belief that that shouldn’t be the case and didn’t realize it. 🙃 (I think I had just gotten a vague impression from the metaprogramming book saying “most goals are synthetic” or something and not talking about opaque ones much, but now that I look closely, i think one of the examples uses a syntheticOpaque metavariable as a goal without comment…!)

[Mario Carneiro]

Also, for "what's causing the difference here", ?x is concrete syntax for synthetic opaque metavariables

[Thomas Murrills]

That would do it! Lol

[Mario Carneiro]

syntheticOpaque means "this will be assigned by a tactic, not by unification"

[Thomas Murrills]

Ah, ok. So when the metaprogramming book talks about synthetic metavariables, they don’t just mean synthetic metavariables—they also mean syntheticOpaque? I’m guessing the opacity is independent info from the SyntheticMVarKind info that the book talks about, then…!

[Thomas Murrills]

Actually, wait. Are opaque synthetic mvars only tactic-solvable re: their SyntheticMVarKind? (Or is your comment more of a heuristic, because, well, nothing else is probably going to assign them?)

[Mario Carneiro]

synthetic opaque mvars cannot be assigned by the usual methods. (rfl : ?_ = ?_) does not typecheck

[Mario Carneiro]

synthetic mvars are used by typeclass inference, they are fairly rare otherwise. They are discouraged from solving by unification, in the sense that if you have a defeq ?m1 =?= ?m2 where ?m1 is natural and ?m2 is synthetic, then ?m1 := ?m2 is preferred over ?m2 := ?m1.

[Jannis Limperg]

In the book, I discuss mvar kinds under isDefEq: natural = isDefEq is free to assign it; synthetic = isDefEq can assign it but avoids it if possible; synthetic opaque = isDefEq never assigns it. That's correct, right? Are any functions besides isDefEq affected by the mvar kinds (except, of course, all the functions that call isDefEq)?

[Mario Carneiro]

there are lots of places the check is used (search for isReadOnlyOrSyntheticOpaque), but they are all morally equivalent to isDefEq or trying to predict whether it will work

[Jannis Limperg]

Okay thanks, then the text is morally correct.