Is `simp_wf` harmless?

Stream: lean4

[Heather Macbeth]

I'd like to propose that decreasing_by build in an application of the simp_wf tactic by default. (This is one of the innards of decreasing_tactic.). It makes the infoview a lot clearer. Here's an example:

def gcd : Nat → Nat → Nat
  | a, 0 => a
  | a, b + 1 => gcd (b + 1) (a % (b + 1))
termination_by gcd a b => b

Compare the goal state for the following two partially-set-up termination proofs (in each case with the cursor right before the sorry):

decreasing_by sorry
/-
a b : Nat
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => snd) instWellFoundedRelation).1 { fst := b + 1, snd := a % (b + 1) }
  { fst := a, snd := Nat.succ b }
-/

and

decreasing_by simp_wf ; sorry
/-
a b : Nat
⊢ a % (b + 1) < Nat.succ b
-/

The latter is much more informative.

[Heather Macbeth]

It seems to me that the only reason not to do this would be if there are examples of termination proofs which this simp_wf would make fail. Does anyone have such an example or is the simp_wf indeed harmless?

[Heather Macbeth]

Alternatively: is it possible to write my own syntax custom_decreasing_by which does this? I got as far in the source as the place where decreasing_by is defined as a leading_parser but I'm not sure how to write a variant.

[Alex Keizer]

Heather Macbeth said:

Alternatively: is it possible to write my own syntax custom_decreasing_by which does this? I got as far in the source as the place where decreasing_by is defined as a leading_parser but I'm not sure how to write a variant.

You should have a look at the elaborator for declaration, that is where the decreasing_by is used. So you'd have to create new parser for def, like

def custom_def            := leading_parser
  "custom_def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> customTerminationSuffix

Where customTerminationSuffix is a version of the terminationSuffix parser that uses custom_decreasing_by.
(You might be able to reuse the def keyword here, instead of custom_def; I'm not 100% sure, though, so I just picked a different command to be safe)

Then, you have to write an elaborator for custom_def. We can look at the standard declaration elaborator for inspiration.

-- from Lean.Elab.Declaration

def getTerminationHints (stx : Syntax) : TerminationHints :=
  let decl := stx[1]
  let k := decl.getKind
  if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
    let args := decl.getArgs
    { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
  else
    {}

@[builtin_command_elab declaration]
def elabDeclaration : CommandElab := fun stx => do
  match (← liftMacroM <| expandDeclNamespace? stx) with
  | some (ns, newStx) => do
    let ns := mkIdentFrom stx ns
    let newStx ← `(namespace $ns $(⟨newStx⟩) end $ns)
    withMacroExpansion stx newStx <| elabCommand newStx
  | none => do
    let decl     := stx[1]
    let declKind := decl.getKind
    if declKind == ``Lean.Parser.Command.«axiom» then
      let modifiers ← elabModifiers stx[0]
      elabAxiom modifiers decl
    else if declKind == ``Lean.Parser.Command.«inductive» then
      let modifiers ← elabModifiers stx[0]
      elabInductive modifiers decl
    else if declKind == ``Lean.Parser.Command.classInductive then
      let modifiers ← elabModifiers stx[0]
      elabClassInductive modifiers decl
    else if declKind == ``Lean.Parser.Command.«structure» then
      let modifiers ← elabModifiers stx[0]
      elabStructure modifiers decl
    else if isDefLike decl then
      elabMutualDef #[stx] (getTerminationHints stx)
    else
      throwError "unexpected declaration"

You only care about defs, so the key line there is

      elabMutualDef #[stx] (getTerminationHints stx)

You can define a new version of getTerminationHints that inserts the call to simp_wf where you want it.
With that, you define the elaborator for custom_def

@[command_elab custom_def]
def elabCustomDef : CommandElab := fun stx => do
  match (← liftMacroM <| expandDeclNamespace? stx) with
  | some (ns, newStx) => do
    let ns := mkIdentFrom stx ns
    let newStx ← `(namespace $ns $(⟨newStx⟩) end $ns)
    withMacroExpansion stx newStx <| elabCommand newStx
  | none => do
    elabMutualDef #[stx] (getCustomTerminationHints stx)

I hope that helps! Feel free to ask for more clarification if the code is not clear

[Mario Carneiro]

There is no need to override decreasing_by (which is not extensible). You can instead override decreasing_tactic (which is extensible)

[Mario Carneiro]

note that decreasing_tactic calls decreasing_with which starts with a call to simp_wf

[Heather Macbeth]

@Alex Keizer Thanks! I learned a lot from your explanation, but I think if the scale of change needed is not just custom_decreasing_by but also custom_def then it's not worth it for me.

@Mario Carneiro I'm not sure I follow, can you explain? Note that I'm specifically interested in what is displayed in the goal state in the place marked with *****

def gcd : Nat → Nat → Nat
  | a, 0 => a
  | a, b + 1 => gcd (b + 1) (a % (b + 1))
termination_by gcd a b => b
decreasing_by ***** sorry

At that point, decreasing_tactic does not seem to be relevant? IIUC decreasing_tactic is only called as a finishing tactic if the decreasing_by line is missing. I'm proposing effectively that one of the innards of decreasing_tactic, namely simp_wf, be called as a cleanup tactic as part of a decreasing_by line.