Commenting tactic

Stream: lean4

[Patrick Massot]

I'm still doing meta-programming exercises with a view towards teaching. It would be nice to have tactics that react to the tactic state using some prerecorded reactions (stored in an environment extension say). The teacher would write somewhere

RegisterMessage exercise1 (n : Nat) (m : Nat) : n + m = m + n => "Congratulations on introducing variables"

and in the student would write

lemma exercise1 : ∀ n m : Nat, n + m = m + n := by
  comment -- Nothing happens
  intros k l
  comment -- triggers `logInfo "Congratulations on introducing variables"`

Ideally the comment tactic would be invoked automatically after each tactic invocation. I know how to register a simple environment extension, and I can parse the syntax of my RegisterMessage command. But then I'm stuck when I try to create a metavariable context that I could compare to the main goal in the comment tactic. Note that this comparison is also a non-trivial question since I don't want the order of declarations or the user facing names of free variables to be considered relevant. But this comparison question comes after understanding how to create a metavariable with a context outside of a proving context (I know this sentence isn't clear but I'm indeed confused about what needs to be done). I tried to read the definition of the def command but there are too many layers and too much generality and I got lost.

[Henrik Böving]

so basically you want to have a map from current tactic state => String (per theorem) and use the comment tactic to access that map and print a message about the current state if there is one registered yes?

[Patrick Massot]

Using strings would be easy but you would miss lots of cases. Notice that in my example I carefully chose stupid variable names in my intro line so that matching strings wouldn't work (the RegisterMessage command uses n and m but I introduce k and l).

[Henrik Böving]

No no I mean a map from the tactic state to strings (i.e. your messages) so that you can give it your current tactic state, it will try to look it up in said map and if it finds an entry print the string that is associated with the state.

[Patrick Massot]

Yes, except that, AFAIK there is no data structure called "tactic state". I'm stuck one creating such a synthetic tactic state in my RegisterMessage command.

[Henrik Böving]

Yes I'm talking about a logical concept such as a tactic state, although one could argue that a meta variable + its context essentially is the tactic state sind it consists of the free variables + the type of the meta variable.

Either way I do not know how to do this from the top of my head but iirc there were efforts to produce a tactic testing framework back in the ICERM22 after party right? They must have implemented a function that can compare tactic states already (since the test framework tests the tactic state before and after a tactic was run) so I would suggest you could try to look into how it was done there maybe.

[Patrick Massot]

Maybe I don't need to create such a synthetic tactic state, simply store the Syntax elements given to the registering command and then compare the actual tactic state to this data.

[Patrick Massot]

Henrik Böving said:

Yes I'm talking about a logical concept such as a tactic state, although one could argue that a meta variable + its context essentially is the tactic state sind it consists of the free variables + the type of the meta variable.

Do you know how to create such a pair "meta variable + its context" out of nowhere?

[Sebastian Ullrich]

I'm not sure you'll want to carry around a metavar context between commands. After elaborating the RegisterMessage arguments, you can pack them into an Expr as in ∀ (n : Nat) (m : Nat), n + m = m + n alongside the information that the first two binders are the context.

[Patrick Massot]

Oh that's clever. I thought about reverting all variables but I didn't want to loose the information about what was introduced.

[Sebastian Ullrich]

Lean does something like that in a lot of places internally :)

[Patrick Massot]

Are there any API functions supporting this?

[Sebastian Ullrich]

You'll want docs4#mkForallFVars and docs4#forallBoundedTelescope in the other direction

[Patrick Massot]

I returned to this idea but, unsurprisingly, I'm having issues. Reproducing is a bit painful because you need to create the environment extension in a different file. In order to reproduce that issue I don't know an easier solution than creating a lake project. You can do mkdir messages && cd messages && echo "leanprover/lean4:nightly-2022-08-06" > lean-toolchain && lake init messages && mkdir Messagesand create a file messages/Messages/EnvExtensions.lean containing

import Lean

open Lean

/-- A goal message is a string indexed by a level name, an expression and a number of necessary intros. -/
def GoalMessageEntry := Name × Expr × Nat × String

/-- Environment extension supporting goal driven messages. -/
initialize goalMessageExt : SimplePersistentEnvExtension GoalMessageEntry (Array GoalMessageEntry) ←
  registerSimplePersistentEnvExtension {
    name := `goal_message
    addEntryFn := Array.push
    addImportedFn := Array.concatMap id
  }

and a file messages/Messages/Issue.lean containing:

import Lean

import Messages.EnvExtensions

set_option autoImplicit false

open Lean Meta Elab Command Term

declare_syntax_cat mydecl
syntax "(" ident ":" term ")" : mydecl

def getIdent : TSyntax `mydecl → Ident
| `(mydecl| ($n:ident : $_t:term)) => n
| _ => default

def getType : TSyntax `mydecl → Term
| `(mydecl| ($_n:ident : $t:term)) => t
| _ => default

def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
| [] => return s


def mkGoalExpr (e : Expr) : List (Name × Expr) → Expr
| (n, t)::tail => .forallE n t (mkGoalExpr e tail) BinderInfo.default
| [] => e


elab "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
  let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList
  let g ← liftTermElabM none $ elabTerm g none
  modifyEnv (goalMessageExt.addEntry · ((← getCurrNamespace), g, decls.size, msg.getString))


Message (n : Nat) (m : Nat) : n + m = m + n => "Well done!"


open  Tactic

/-- Get the list of free variables occuring in the expression (with repetitions). -/
def Lean.Expr.getFVars : Expr → List FVarId
| .app fn arg => (getFVars fn) ++ (getFVars arg)
| .fvar Id => [Id]
| .lam _ bt body .. => getFVars bt ++ getFVars body
| .forallE _ bt body .. => getFVars bt ++ getFVars body
| .letE _ t v b .. => getFVars t ++ getFVars v ++ getFVars b
| .mdata _ e => getFVars e
| .proj _ _ e => getFVars e
| _ => []


/-- Returns the type of the goal after reverting all free variables in the order
where they appear in the goal type. -/
def normalizedRevertExpr (goal : MVarId) : MetaM Expr := do
  let (_, new) ← goal.revert (← goal.getType).getFVars.toArray true
  return (← new.getType)

elab "comment" : tactic => do
  let tgt ← getMainGoal
  let tgt_ctx_size := (← tgt.getDecl).lctx.size
  let normalized_tgt ← normalizedRevertExpr tgt
  for (_name, msg_goal, nb, d) in goalMessageExt.getEntries (← getEnv) do
    let msg_mvar ← mkFreshExprMVar msg_goal MetavarKind.syntheticOpaque
    let (_, msg_mvar) ← msg_mvar.mvarId!.introNP nb
    let msg_ctx_size := (← msg_mvar.getDecl).lctx.size
    if tgt_ctx_size ≠ msg_ctx_size then continue
    let normalized_msg ← normalizedRevertExpr msg_mvar
    if (← isDefEq normalized_tgt normalized_msg) then logInfo d

example : ∀ n m : Nat, n + m = m + n := by
  comment
  intros n m
  revert n
  revert m
  intros m n
  comment
  rw [Nat.add_comm]

[Patrick Massot]

Recall the goal is to be able to recognize a tactic state even if the free variables are permuted in the context. In the example above, the goal is to recognize the context n m : Nat ⊢ n + m = m + n even if it appears as m n : Nat ⊢ n + m = m + n (note the free variables order). The comparison should also discard free variable names differences, so k l : Nat ⊢ k + l = l + k should match as well. My idea to compare to such contexts is to list all free variables in the target expression, here n + m = m + n and revert all those variables in the order they appear then I test whether the resulting goals are defeq. In the above code I first do a cheap check comparing the context sizes to fail the comparison early in case they don't match.

[Patrick Massot]

It sort of works except that all those manipulation actually alter the goal and the above example has an error on the last line saying there is no remaining goal to solve.

[Patrick Massot]

Note that I'm interested in both a fix to my code and a completely different much better way to achieve my goal.

[Mario Carneiro]

the easy fix to the fact that your manipulations alter the goal is to roll back the state once you're done

[Mario Carneiro]

wrap the whole thing in withoutModifyingState

[Patrick Massot]

Do you mean

elab "comment" : tactic => do
withoutModifyingState do
  let tgt ← getMainGoal
  let tgt_ctx_size := (← tgt.getDecl).lctx.size
  let normalized_tgt ← normalizedRevertExpr tgt
  for (_name, msg_goal, nb, d) in goalMessageExt.getEntries (← getEnv) do
    let msg_mvar ← mkFreshExprMVar msg_goal MetavarKind.syntheticOpaque
    let (_, msg_mvar) ← msg_mvar.mvarId!.introNP nb
    let msg_ctx_size := (← msg_mvar.getDecl).lctx.size
    if tgt_ctx_size ≠ msg_ctx_size then continue
    let normalized_msg ← normalizedRevertExpr msg_mvar
    if (← isDefEq normalized_tgt normalized_msg) then logInfo d

This indeed suppresses the error message but it also suppresses the success message :sad:

[Mario Carneiro]

You can have the body return the list of messages you want to report, and then do them outside the withoutModifyingState. Alternatively, you could try using saveState and restore directly

[Mario Carneiro]

elab "comment" : tactic => do
  let s ← saveState
  let tgt ← getMainGoal
  let tgt_ctx_size := (← tgt.getDecl).lctx.size
  let normalized_tgt ← normalizedRevertExpr tgt
  let mut messages := #[]
  for (_name, msg_goal, nb, d) in goalMessageExt.getEntries (← getEnv) do
    let msg_mvar ← mkFreshExprMVar msg_goal MetavarKind.syntheticOpaque
    let (_, msg_mvar) ← msg_mvar.mvarId!.introNP nb
    let msg_ctx_size := (← msg_mvar.getDecl).lctx.size
    if tgt_ctx_size ≠ msg_ctx_size then continue
    let normalized_msg ← normalizedRevertExpr msg_mvar
    if (← isDefEq normalized_tgt normalized_msg) then
      messages := messages.push d
  s.restore
  for d in messages do logInfo d

I'm not sure why s.restore is backtracking the trace state; the documentation says it shouldn't

[Sebastian Ullrich]

Diagnostic messages are not part of the trace state, if you mean that

[Patrick Massot]

Thank you very much Mario! Do you have other comment about my approach? Do you see a better way to do it? I know I should store a normalized version in the environment extension instead of recomputing it endlessly, but I didn't want to optimize this before having a working version.

[Patrick Massot]

Actually precomputing the normalized expression is not as easy as I thought because there is no MonadLiftT MetaM CommandElabM.

[Patrick Massot]

I still have issues navigating the monads of meta-programming in Lean 4. Do we have a cheat-sheet displaying all relations between them? I mean both extension relations and lifting capabilities.

[Patrick Massot]

There must be a way to go from CommandElabM Unit to MetaM since declaration commands can state and prove theorems.

[Henrik Böving]

Its not as easy as you think though, CommandElabM has no direct way to execute a MetaM computation since it can only access an Environment and doesn't have all the other stuff MetaM needs included. The MetaM executing elaborators basically create new either empty or customly filled states and contexts for the MetaM monad.

Since it is not entirely obvious what these initial states and contexts should be though (at least not generally for all use cases) these MonadLift instances do not exist.

You can see this yourself if you go through the definitions of the monad stack, a CommandElabM does not have all the info a MetaM needs

[Patrick Massot]

I understand that, but the def and theorem commands somehow do this, right?

[Patrick Massot]

I guess we're back to the question that started this thread: how to create an artificial context for a goal outside a proving context?

[Sebastian Ullrich]

MetaM.run' defaults to an empty local and mvar context, which I assume is what you want in this case. Then you're in CoreM, which you can lift with Command.liftCoreM.

[Leonardo de Moura]

@Patrick Massot
The def and theorem commands are implemented using
runTermElabM. I added documentation and examples for liftTermElabM and runTermElabM:
https://github.com/leanprover/lean4/commit/e236eeba870c64178805c2d5a4d6727f9b329fcb

[Leonardo de Moura]

Here is where runTermElabM is used to implement def and theorem:
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/MutualDef.lean#L876

[Leonardo de Moura]

BTW, I will remove the unnecessary declName? parameter. New commit coming soon.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/413db56b89459d7328cee7abd669f9b99e7f4b37

[Patrick Massot]

Thank you very much for all this!

[Patrick Massot]

I can confirm that liftTermElab works for me.

[Mario Carneiro]

Would it be an option to make it a liftM instance now? Or is that being deliberately avoided because of the dummy state issues

[Leonardo de Moura]

@Mario Carneiro I think it is problematic because

• The lift is not a cheap operation
• It matters where the lift is inserted. Example:

import Lean

open Lean Meta Elab Command Term

def ex1 : CommandElabM Expr := liftTermElabM do
  let x ← mkFreshTypeMVar
  inferType x

def ex2 : CommandElabM Expr := do
  let x ← liftTermElabM <| mkFreshTypeMVar
  liftTermElabM <| inferType x

#eval ex1 -- Ok
#eval ex2 -- Error unknown metavariable

[Mario Carneiro]

does liftM prefer the second interpretation? (EDIT: yes)

[Mario Carneiro]

The names liftTermElabM and runTermElabM are not very clearly different though. I wouldn't be able to guess which is which without looking them up

[Leonardo de Moura]

Mario Carneiro said:

The names liftTermElabM and runTermElabM are not very clearly different though. I wouldn't be able to guess which is which without looking them up

We now have the docstrings :)

[Leonardo de Moura]

liftTermElabM has (now) the same signature of other liftM methods.

[Mario Carneiro]

How about runTermElabMWithContext?

[Mario Carneiro]

and renaming liftTermElabM to runTermElabM

[Leonardo de Moura]

I didn't like the new names :big_smile:

[Mario Carneiro]

Although the signature of liftTermElabM is like other liftMs, I am convinced by your argument that it's not really a lift

[Mario Carneiro]

especially liftTermElabM (a >> b) != liftTermElabM a >> liftTermElabM b