Reduction of types in lambda and forall bindings

Stream: lean4

[Yann Herklotz]

reduce does not reduce the types of lambda and forall bindings, only the final expressions. For example:

#reduce (proofs := true) (types := true) 1 + 1 = 2 → True
-- ==> 1 + 1= 2 → True

This seems to be a design decision, because the implementation for reduction of foralls and lambdas first abstracts these away, reduces, and then reconstructs the forall (GitHub link to implementation: src/Lean/Meta/Reduce.lean#L40):

| Expr.forallE ..    => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)

I was wondering what the main downsides would be if one allowed reduction of types in the binders, maybe with an optional flag that enables it, like the reduction of proofs and types?

I do agree that it could be quite expensive, but are there other reasons one may never actually want this?

We sometimes have hypotheses that quantify over quite large types because they are generated by a function, but they usually can be reduced into a small concrete type if this function is given concrete values. So to make it easier to look at the context, we would like to reduce all of these expressions, which might appear in binders in hypotheses.

I have implemented a version of reduce which does exactly this, adding an option called skipArgs which will skip the reduction of binders, I'll post the implementation below.

[Yann Herklotz]

import Lean

open Lean Expr Meta

partial def reallyReduce (e : Expr) (explicitOnly skipTypes skipProofs skipArgs := true) : MetaM Expr :=
  let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr :=
    checkCache e fun _ => Core.withIncRecDepth do
      if (← (pure skipTypes <&&> isType e)) then
        return e
      else if (← (pure skipProofs <&&> isProof e)) then
        return e
      else
        let e ← whnf e
        match e with
        | Expr.app .. =>
          let f     ← visit e.getAppFn
          let nargs := e.getAppNumArgs
          let finfo ← getFunInfoNArgs f nargs
          let mut args  := e.getAppArgs
          for i in [:args.size] do
            if i < finfo.paramInfo.size then
              let info := finfo.paramInfo[i]!
              if !explicitOnly || info.isExplicit then
                args ← args.modifyM i visit
            else
              args ← args.modifyM i visit
          if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then
            return mkRawNatLit (args[0]!.rawNatLit?.get! + 1)
          else
            return mkAppN f args
        | Expr.lam ..        => lambdaTelescope e fun xs b => do
          if skipArgs then mkLambdaFVars xs (← visit b)
          else
            let ctx ← getLCtx
            let ctx' ← xs.foldlM (fun ctx' e => do
              let e' ← visit (ctx'.getFVar! e).type
              return ctx'.modifyLocalDecl e.fvarId! fun l => l.setType e') ctx
            withLCtx ctx' #[] do mkLambdaFVars xs (← visit b)
        | Expr.forallE ..    => forallTelescope e fun xs b => do
          if skipArgs then mkForallFVars xs (← visit b)
          else
            let ctx ← getLCtx
            let ctx' ← xs.foldlM (fun ctx' e => do
              let e' ← visit (ctx'.getFVar! e).type
              return ctx'.modifyLocalDecl e.fvarId! fun l => l.setType e') ctx
            withLCtx ctx' #[] do mkForallFVars xs (← visit b)
        | Expr.proj n i s .. => return mkProj n i (← visit s)
        | _                  => return e
  visit e |>.run

def reallyReduceAll (e : Expr) : MetaM Expr :=
  reallyReduce e false false false

syntax (name := reallyReduceCmd) "#reallyReduce " term : command

open Elab Command in
@[command_elab reallyReduceCmd] def elabReallyReduce : CommandElab
  | `(#reallyReduce%$tk $term) => go tk term
  | _ => throwUnsupportedSyntax
where
  go (tk : Syntax) (term : Syntax) : CommandElabM Unit :=
    withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
      let e ← Term.elabTerm term none
      Term.synthesizeSyntheticMVarsNoPostponing
      let e ← Term.levelMVarToParam (← instantiateMVars e)
      -- TODO: add options or notation for setting the following parameters
      withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
        let e ← withTransparency (mode := TransparencyMode.all) <| reallyReduce e false false false false
        logInfoAt tk e

#reduce (proofs := true) (types := true) 1 + 1 = 2 → True
#reallyReduce 1 + 1 = 2 → True