reduction of dependent return type

Stream: lean4

[Sébastien Michelland]

I'm trying to map a symbolic type to a Lean type and define a default value through a function, but I often run into instances where the unification algorithm does not reduce the eval function in each branch. Here is a MWE:

inductive T :=
  | int : Int -> T
  | tuple : List T -> T

def T.eval: T → Type
  | T.int _ => Int
  | T.tuple [] => Unit
  | T.tuple (τ::_) => τ.eval

def T.default (τ: T): τ.eval :=
  match τ with
  | T.int _ => (0:Int)
  | T.tuple [] => ()
  | T.tuple (τ::l) => τ.default

For instance I get an error on (0:Int) saying it expects an eval (int x✝). I'm not sure what influences this result; removing the parameter to T.int, getting rid of T.tuple, or returning Int rather than τ.eval for the third matching case of T.eval all cause this error to go away on the first case.

I'd think there is some function attribute to indicate that T.eval should be reduced, but neither @[simp] or @[reducible] work. The best I can get currently is with @[simp], by replacing the terms with cast (by simp) _, but it's inconvenient.

[Leonardo de Moura]

The problem is that T is a nested inductive datatype, and in the current implementation, every recursive function defined on this kind of type uses well-founded recursion. You can use

#print T.eval

to see how T.eval was compiled before being sent to the kernel.
Moreover, well-founded recursion requires theorems to be unfolded to reduce, and by default, the Lean elaborator does not unfold theorems.
The current workaround is to define T.eval using the primitive T.rec recursor. It is painful, but it is doable for a simple function like T.eval. In the future, we want to be able to show definitions such as T.eval terminate using T.rec instead of well-founded recursion, but it will not happen in the near future. Here is your example with T.rec

inductive T :=
  | int : Int -> T
  | tuple : List T -> T

def T.eval (t : T) : Type :=
  @T.rec
    (motive_1 := fun _ => Type)
    (motive_2 := fun _ => Type)
    (fun _ => Int)
    (fun _ ih => ih)
    Unit
    (fun _ _ ih₁ ih₂ => ih₁)
    t

def T.default (τ: T): τ.eval :=
  match τ with
  | T.int _ => (0:Int)
  | T.tuple [] => ()
  | T.tuple (τ::l) => τ.default

[Leonardo de Moura]

I pushed your example to our test suite as a reminder that we need to add support for nested and mutual inductive types to the structural recursion module.
https://github.com/leanprover/lean4/blob/master/tests/lean/run/nestedInductiveRecType.lean

[Leonardo de Moura]

BTW, file above also uses the recursor T.rec_1that takes List T as a major premise. We need it if want eval to return a Prod for T.tuple.