print discrimination tree keys

Stream: batteries

[Matthew Ballard]

Do we have a command to print discrimination keys? I've been using the following based on @Tomas Skrivan

import Lean

open Lean Meta

def discrKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
  let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
  let type ← whnfR type
  match type.eq? with
  | some (_, lhs, _) => DiscrTree.mkPath lhs simpDtConfig
  | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"

open Elab Term
elab "#discr_tree_key" t:term : command => do
  Command.liftTermElabM <| do
    let e ← elabTerm t none
    IO.println ((← discrKey e).map fun key => key.format)

open Elab Term
elab "#discr_tree_key" id:ident : command => do
  Command.liftTermElabM <| do
    let info ← getConstInfo id.getId
    IO.println ((← discrKey info.type).map fun key => key.format)

open Tactic in
elab "discr_tree_key" : tactic => do
  let e ← getMainGoal
  let keys ← discrKey (← e.getType)
  logInfo s!"{keys.map fun key => key.format}"

[Matthew Ballard]

If not, is this something desired in batteries? I know that incoming core changes will avoid mapping over format.

[Kyle Miller]

lean4#4208 is what you mean by that last sentence, right? That discriminations tree keys will have a nice pretty printer?

[Kim Morrison]

I would be very happy to have this in batteries, and even happier to have it in Lean itself. This is super useful for diagnosing problems.

Putting it in Lean requires jumping through an extra hoop to set up built-in syntax. If someone could even do that, amazing, but I'm also happy to modify a PR that just contains the non-built-in setup.

[Tomas Skrivan]

It would be also useful to have an option for simp that:

• prints out the discrimination tree key when simp searches for candidate theorems to apply
• prints out discrimination tree key of lhs when you mark theorem with simp attribute

[Kim Morrison]

These are probably best done via issues rather than PRs. (But yes, both of these are needed.)

[Matthew Ballard]

Right now I can't use one of my 4 local copies of mathlib because I just keep that code sitting in an open buffer so I would be happy to use this again.

What is the hoop to set up built-in syntax?

[Matthew Ballard]

If we are listing desirable things for the future, the generated keys for instances is also useful to know on occasion.

[Kim Morrison]

You just need to define the syntax in the appropriate file, using Init/Tactics.lean, and then use the @[builtin_command_elab] attribute when you set up the implementation. For the commands discussed above, I don't think any update-stage0 shenanigans would be required.

[Matthew Ballard]

Can I be lazy and ask you to point me to your favorite example?

[Matthew Ballard]

It's ok to say no :)

[Matthew Ballard]

Ok, nevermind. I stopped being lazy

[Kim Morrison]

Maybe

@[builtin_command_elab guardCmd]
def evalGuardCmd : Lean.Elab.Command.CommandElab
  | `(command| #guard $e:term) => Lean.Elab.Command.liftTermElabM do
    let e ← Term.elabTermEnsuringType e (mkConst ``Bool)
    Term.synthesizeSyntheticMVarsNoPostponing
    let e ← instantiateMVars e
    let mvars ← getMVars e
    if mvars.isEmpty then
      let v ← unsafe evalExpr Bool (mkConst ``Bool) e
      unless v do
        throwError "expression{indentExpr e}\ndid not evaluate to `true`"
    else
      _ ← Term.logUnassignedUsingErrorInfos mvars
  | _ => throwUnsupportedSyntax

from src/Lean/Elab/Tactic/Guard.lean, and syntax (name := guardCmd) "#guard " term : command in src/Init/Guard.lean.

[Kim Morrison]

The point is that even though the implementation of #guard is not in the prelude, after rebuilding stage0 you nevertheless get to use it in the prelude. (The magic of bootstrapping.)

[Matthew Ballard]

@Kim Morrison Sorry for the delay lean#4447. Draft form because I’m sure you’ll have some good examples to add to the test file.

[Matthew Ballard]

@Tomas Skrivan I listed you as an author (and of course misspelled your name :man_facepalming: ) Let me know your thoughts.

[Tomas Skrivan]

Looks good to me. I'm just wondering if the tactic should fail if you provide term that is not of the form _ = _ (current behavior) or it should print a key of the whole expression. You might want to use it to debug typeclass synthesis too where you do not have expression of the form _ = _. Also a special support for _ ↔ _ might be desirable. But it is plenty useful in the form it is already, so these are just suggestions for potential improvements.