fully reduce type

Stream: general

[Mirek Olšák]

In a lecture, I would like to show an example of the type

import Mathlib

def iteratePow (n : ℕ) : Type :=
  match n with
  | 0 => ℕ
  | k+1 => (iteratePow k) → Prop

to give an idea of how easily a large type can be build. However, I would also like to show how this actually evaluates. Naturally #eval doesn't work. I hoped #reduce could do it but it refuses to reduce the term fully, leaving some mess of Nat.rec

#eval iteratePow 3 -- error
#reduce (types := true) iteratePow 3 -- mess

The best I have come up with so far is

#simp [iteratePow] => iteratePow 3 -- ((ℕ → Prop) → Prop) → Prop

but it is quite high level, and somewhat inaccurate description of what is happening when Lean accepts say

example : iteratePow 1 := fun n : Nat ↦ n > 5

Is there any way of actually reducing the expression iteratePow 3? Say in tactic mode? Or using meta-code if there is no better option?

[Jovan Gerbscheid]

Huh, that's wierd, looking at the implementation of docs#Lean.Meta.reduce, we see that it doesn't actually reduce in the domain of a forall. I'm afraid you'll have to implement your own version, and you can copy-paste docs#Lean.Elab.Command.elabReduce

[Mirek Olšák]

If I need modify the code Meta.reduce for this, what is the correct way of reducing type in a LocalDecl?

[Jovan Gerbscheid]

Here's a neat way to implement a fully reducing version of reduce:

import Lean

open Lean Meta Elab Command

def fullReduce (e : Expr) : MetaM Expr := do
  transform e (pre := fun e ↦ return .continue (← whnf e))

-- copied elaborator for `#reduce` command
@[command_elab Lean.reduceCmd] def elabReduce : CommandElab
  | `(#reduce%$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
      -- Users might be testing out buggy elaborators. Let's typecheck before proceeding:
      withRef tk <| Meta.check e
      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.set `smartUnfolding false }) do
        let e ← withTransparency (mode := TransparencyMode.all) <| fullReduce e
        logInfoAt tk e

def iteratePow (n : Nat) : Type :=
  match n with
  | 0 => Nat
  | k+1 => (iteratePow k) → Prop

#reduce iteratePow 3 -- expected result

[Mirek Olšák]

Thanks, the transform might be not super-efficient but completely sufficient for my needs. I also simplified the elab part, and call it #full_reduce, in my materials.