seeing inferred arguments for a theorem application

Stream: new members

[Rado Kirov]

When I write something like rw [add_comm] Lean implicitly infers the two arguments {a b} for add_comm and then applies the rewrite a + b = b + a for some a and b. Is there a way to see in the InfoView or other tool, what the inferred a and b precisely are. Kind hoped hovering over add_comm would do that, but it doesn't seem too.

I know that, of course, I can work those backwards from the resulting rewrite in the local goals, but it require a bit of extra work from me (imagine the theorem being {a b}: <some messy expression with a b> applied to an <even messier expression that contains the theorems messy subexpression>).

[Ruben Van de Velde]

If you put show_term before rw, you can probably find the answer in there

[Alfredo Moreira-Rosa]

Indeed, but it's really ugly. Would be nice if LSP could show what it inferred.
Another way i use sometimes is make the rw fail to show what it infers since error message show it.

[Rado Kirov]

That's great, didn't know about it! A bit more involved than hovering over, but good enough for now.

Also the simple

import Mathlib

example (x y: Nat) : x + y = y + x := by
  rw [add_comm]

turns into

example (x y: Nat) : x + y = y + x := by
  exact Eq.mpr (id (congrArg (fun _a => _a = y + x) (add_comm x y))) (Eq.refl (y + x))

wowza :) I expected add_comm x y only

[Damiano Testa]

It is not just add_comm, since rw "navigates" to the locations in the expression that should be changed. This is what the congrArg does.

[Damiano Testa]

In particular, rw is changing just the LHS, it is not unifying the whole goal with an application of the lemma.

[Eric Paul]

Just for fun, this shows the instantiated version of the theorem when you hover, although you lose the old hover. I could just logInfo the instantiated version but I wouldn't want the blue squiggles under everything.

The new version is rw' with your example at the bottom:

I just changed one line but had to copy everything over

import Lean
import Mathlib

namespace Rw
open Lean Meta Elab Tactic Parser Tactic
syntax (name := rewriteSeq') "rewrite'" optConfig rwRuleSeq (location)? : tactic

/--
`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
-/
macro (name := rwSeq') "rw' " c:optConfig s:rwRuleSeq l:(location)? : tactic =>
  match s with
  | `(rwRuleSeq| [$rs,*]%$rbrak) =>
    -- We show the `rfl` state on `]`
    `(tactic| (rewrite' $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
  | _ => Macro.throwUnsupported


/--
Runs `Lean.MVarId.rewrite`, and also handles filtering out the old metavariables in the rewrite result.
This should be used from within `withSynthesize`.
Use `finishElabRewrite` once elaboration is complete to make final updates to `RewriteResult`.
-/
def elabRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax)
    (symm : Bool := false) (config := { : Rewrite.Config }) : TacticM RewriteResult := do
  let mvarCounterSaved := (← getMCtx).mvarCounter
  let thm ← withEnableInfoTree false <| elabTerm stx none true
  if thm.hasSyntheticSorry then
    throwAbortTactic
  unless ← occursCheck mvarId thm do
    throwErrorAt stx "Occurs check failed: Expression{indentExpr thm}\ncontains the goal {Expr.mvar mvarId}"
  let r ← mvarId.rewrite e thm symm (config := config)
  discard <| Lean.Elab.Term.addTermInfo stx r.eqProof.getAppArgs.back!
  let mctx ← getMCtx
  let mvarIds := r.mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved

  return { r with mvarIds }

/--
Makes new goals be synthetic opaque, to be done once elaboration of the rewrite theorem is complete.

Workaround note: we are only doing this for proof goals, not data goals,
since there are many downstream cases of tactic proofs that later assign data goals by unification.
-/
def finishElabRewrite (r : RewriteResult) : MetaM RewriteResult := do
  let mvarIds ← r.mvarIds.filterM (not <$> ·.isAssigned)
  mvarIds.forM fun newMVarId => newMVarId.withContext do
    if ← Meta.isProp (← newMVarId.getType) then
      newMVarId.setKind .syntheticOpaque
  return { r with mvarIds }

def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
  let r ← Term.withSynthesize <| withMainContext do
    elabRewrite (← getMainGoal) (← getMainTarget) stx symm (config := config)
  let r ← finishElabRewrite r
  let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
  replaceMainGoal (mvarId' :: r.mvarIds)

def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) :
    TacticM Unit := withMainContext do
  -- Note: we cannot execute `replaceLocalDecl` inside `Term.withSynthesize`.
  -- See issues #2711 and #2727.
  let rwResult ← Term.withSynthesize <| withMainContext do
    let localDecl ← fvarId.getDecl
    elabRewrite (← getMainGoal) localDecl.type stx symm (config := config)
  let rwResult ← finishElabRewrite rwResult
  let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
  replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)

def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
  let lbrak := rwRulesSeqStx[0]
  let rules := rwRulesSeqStx[1].getArgs
  -- show initial state up to (incl.) `[`
  withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
  let numRules := (rules.size + 1) / 2
  for i in *...numRules do
    let rule := rules[i * 2]!
    let sep  := rules.getD (i * 2 + 1) Syntax.missing
    -- show rule state up to (incl.) next `,`
    withTacticInfoContext (mkNullNode #[rule, sep]) do
      -- show errors on rule
      withRef rule do
        let symm := !rule[0].isNone
        let term := rule[1]
        let processId (id : Syntax) : TacticM Unit := do
          -- See if we can interpret `id` as a hypothesis first.
          if (← withMainContext <| Term.isLocalIdent? id).isSome then
            x symm term
          else
            -- Try to get equation theorems for `id`.
            let declName ← try realizeGlobalConstNoOverload id catch _ => return (← x symm term)
            let some eqThms ← getEqnsFor? declName | x symm term
            let hint := if eqThms.size = 1 then m!"" else
              .hint' m!"Try rewriting with `{Name.str declName unfoldThmSuffix}`"
            let rec go : List Name →  TacticM Unit
              | [] => throwError m!"Failed to rewrite using equation theorems for `{.ofConstName declName}`" ++ hint
              | eqThm::eqThms => (x symm (mkCIdentFrom id eqThm)) <|> go eqThms
            discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
            go eqThms.toList
        match term with
        | `($id:ident)  => processId id
        | `(@$id:ident) => processId id
        | _ => x symm term

@[tactic rewriteSeq'] def evalRewriteSeq : Tactic := fun stx => do
  let cfg ← elabRewriteConfig stx[1]
  let loc   := expandOptLocation stx[3]
  withRWRulesSeq stx[0] stx[2] fun symm term => do
    withLocation loc
      (rewriteLocalDecl term symm · cfg)
      (rewriteTarget term symm cfg)
      (throwTacticEx `rewrite · "Did not find an occurrence of the pattern in the current goal")
end Rw

example (x y: Nat) : x + y = y + x := by
  rw' [add_comm]

[Eric Paul]

Learning that one could modify hover info like this was cool so I wrote a tiny blog post about it