How to control the terms unfolded by `#reduce`?

Stream: new members

[Qiyuan Zhao]

In the code below, my intention is to use #reduce to get rid of foo.match_1 and to expose the recursor of Thing. However, #reduce will also unfold List.map.

Is it possible for me to control the terms that will be affected by #reduce? In Coq, I can use Eval cbn delta [...] to control; I also wonder if there is anything similar in Lean.

Thanks!

-- Lean version for this: v4.8.0

inductive Thing where
  | aa : Thing
  | bb (a : List Nat) : Thing

def foo (t : Thing) :=
  match t with
  | .aa => []
  | .bb l => List.map (fun x => x + 1) l

#print foo
/-
output:

def foo : Thing → List Nat :=
fun t => foo.match_1 (fun t => List Nat) t (fun _ => List.nil) fun l => List.map (fun x => HAdd.hAdd x 1) l
-/

#reduce foo
/-
output:

fun t =>
  Thing.rec []
    (fun a =>
      (List.rec ⟨[], PUnit.unit⟩ (fun head tail tail_ih => ⟨head.succ :: tail_ih.1, ⟨tail_ih, PUnit.unit⟩⟩) a).1)
    t
-/

[Kyle Miller]

This sort of is what you're asking, but it makes use of the simp tactic rather than reduction.

import Mathlib

inductive Thing where
  | aa : Thing
  | bb (a : List Nat) : Thing

def foo (t : Thing) :=
  match t with
  | .aa => []
  | .bb l => List.map (fun x => x + 1) l

#simp only [foo] => fun t => foo t
/-
fun t ↦
  match t with
  | Thing.aa => []
  | Thing.bb l => List.map (fun x ↦ x + 1) l
-/

[Kyle Miller]

It would be possible to write your own #reduce (or #whnf) that only unfolds certain terms.