RFC: a trace variant of the tactic `trivial`, aka `trivial?`

Stream: lean4

[Yongshun Ye]

It's a common topic that something in math can be trivial for one person but not for another. Especially for beginners, understanding why/how something is trivial is important. Lean's trivial tactic delegates to 6 other tactics as I see from the source code. So I think it would make Lean more friendly especially to new users by adding a trace variant trivial?, which suggests the underlying tactic used, just like simp?, apply?, etc. If OK, I am happy take on the implementation of this and submit a PR.

[Robin Arnez]

Actually, why not expand all macros?

import Lean

def cleanMacroScopes (stx : Lean.Syntax) : Lean.Syntax :=
  match stx with
  | .ident info raw val pre => .ident info raw val.eraseMacroScopes pre
  | .node info kind args =>
    if kind = ``Lean.Parser.Tactic.withAnnotateState then
      if h : args.size > 2 then
        cleanMacroScopes args[2]
      else
        stx
    else
      .node info kind (args.map cleanMacroScopes)
  | stx => stx

def null : Lean.Parser.Parser := Lean.Parser.many Lean.Parser.commandParser

open Lean Syntax MonadTraverser Parser PrettyPrinter Formatter in
@[formatter null]
def null.formatter : Lean.PrettyPrinter.Formatter := do
  let stx ← getCur
  ppDedent.formatter do
    visitArgs $ stx.getArgs.size.forM fun i _ => do
      if i > 0 then
        ppLine.formatter
        ppLine.formatter
      commandParser.formatter

open Lean Parser PrettyPrinter Parenthesizer in
@[parenthesizer null]
def null.parenthesizer : Lean.PrettyPrinter.Parenthesizer :=
  many.parenthesizer commandParser.parenthesizer

open Lean Meta Elab Tactic in
partial def addMacroExpandSuggestions (tree : InfoTree) (ctx : ContextInfo) : MetaM Unit := do
  match tree with
  | .context pctx tree =>
    addMacroExpandSuggestions tree ((pctx.mergeIntoOuter? (some ctx)).getD ctx)
  | .hole _ => pure ()
  | .node info children =>
    match info with
    | .ofTacticInfo tac =>
      let elabName := tac.elaborator
      let some _ := info.range? |
        children.forM (addMacroExpandSuggestions · ctx)
      let some elabDecl := ctx.env.findConstVal? elabName |
        children.forM (addMacroExpandSuggestions · ctx)
      if elabDecl.type.isConstOf ``Macro then
        if h : children.size = 1 then
          let inner := children[0]
          if let .node innerInfo _ := inner then
            TryThis.addSuggestion tac.stx (⟨cleanMacroScopes innerInfo.stx⟩ : Syntax.Tactic)
            return
      children.forM (addMacroExpandSuggestions · ctx)
    | .ofMacroExpansionInfo mac =>
      if mac.stx.isOfKind ``Parser.Term.paren then
        children.forM (addMacroExpandSuggestions · ctx)
      else
        let some _ := info.range? | children.forM (addMacroExpandSuggestions · ctx)
        TryThis.addSuggestion mac.stx (⟨cleanMacroScopes mac.output⟩ : Syntax.Term)
    | _ => children.forM (addMacroExpandSuggestions · ctx)

open Lean Elab Term in
def getContextInfo : TermElabM ContextInfo :=
  return {
    env := ← getEnv
    fileMap := ← getFileMap
    ngen := ← getNGen
    openDecls := ← getOpenDecls
    mctx := ← getMCtx
    options := ← getOptions
    currNamespace := ← getCurrNamespace
    parentDecl? := ← Term.getDeclName?
  }

open Lean Meta Elab Tactic in
elab "macro_expand?" s:tacticSeq : tactic => do
  evalTacticSeq s
  let trees := (← getInfoState).substituteLazy.get.trees
  let context : ContextInfo ← getContextInfo
  for tree in trees do
    addMacroExpandSuggestions tree context

open Lean Meta Elab Term in
elab "macro_expand% " stx:term : term => do
  let expr ← elabTerm stx ‹_›
  let trees := (← getInfoState).substituteLazy.get.trees
  let context : ContextInfo ← getContextInfo
  for tree in trees do
    addMacroExpandSuggestions tree context
  return expr

open Lean Meta Elab Command in
elab "#macro_expand " "in " stx:command : command => do
  let expr ← elabCommand stx
  let trees := (← getInfoState).substituteLazy.get.trees
  liftTermElabM <| do
    let context : ContextInfo ← getContextInfo
    for tree in trees do
      addMacroExpandSuggestions tree context
    return expr

[Robin Arnez]

This is quite fun to play around with (just put #macro_expand in above your command of choice)

[Kyle Miller]

@Yongshun Shreck Ye If you "go to definition" on a use of trivial, it should go to the macro rule that applied.

[Yongshun Ye]

@Kyle Miller Thanks. It's good to know.

[Yongshun Ye]

@Robin Arnez Yeah this does look like a more general and well-rounded approach.