recursive definition in structure fields

Stream: lean4

[Jireh Loreaux]

I can't seem to make a recursive definition in a structure field. What is the syntax for making this work? I think in Lean 3 it was called _match.

theorem foo : ∀ n : Nat, 0 ≤ n
  | 0 => Nat.le_refl 0
  | n + 1 => Nat.le_trans (foo n) n.le_succ -- works

example : ∀ n : Nat, 0 ≤ n
  | 0 => Nat.le_refl 0
  | n + 1 => Nat.le_trans (_example n) n.le_succ -- works

structure Bar :=
  bar : ∀ n : Nat, 0 ≤ n

def myBar : Bar where
  bar
    | 0 => Nat.le_refl 0
    | n + 1 => Nat.le_trans (bar n) n.le_succ -- unknown identifier 'bar'

[Jireh Loreaux]

If I try Bar.bar it errors because it can't find an instance of the typeclass (which makes some sense).

[Eric Wieser]

I assume you can simplify this to the case of defining a structure value, eliminating typeclass search from the example?

[Jireh Loreaux]

Sure, edited

[Jireh Loreaux]

Using | n + 1 => Nat.le_trans (Bar.bar myBar n) n.le_succ leads to Lean complaining that it failed to show termination because structural recursion can't be used.

[František Silváši 🦉]

Maybe there's a more straightforward way but this works:

def myBar : Bar where
  bar := loop where
         loop | 0 => Nat.le_refl 0
              | n + 1 => Nat.le_trans (loop n) n.le_succ

(Alternatively, let rec instead of where.)

[Jireh Loreaux]

Thanks, yes, that works. I would still like to know if there is a built-in syntax which will make this work without a let binding.

[Henrik Böving]

Not to my knowledge sadly :(