Local bindings as syntactic abbreviations

Stream: lean4

[Raghuram]

inductive Tree (α : Type u) : Type u where
| node : α → Option (Tree α) → Option (Tree α) → Tree α

-- Just noticed I don't need to open `some`; no idea why
open Option (none)

def Tree.rec' {motive : Tree α → _}
        (base : (a:α) → motive (node a none none))
        (left : (a:α) → (l:Tree α) → motive l → motive (node a l none))
        (right : (a:α) → (r:Tree α) → motive r → motive (node a none r))
        (both : (a:α) → (l r : Tree α) → motive l → motive r → motive (node a l r))
    : (tree : Tree α) → motive tree
| node a none none         => base a
| node a (some l) none     => left a l (rec'' l)
| node a none (some r)     => right a r (rec'' r)
| node a (some l) (some r) => both a l r (rec'' l) (rec'' r)
where rec'' := rec' base left right both

This doesn't work with Lean complaining about failing to show termination. Normally that's reasonable, but here all applications of rec'' are just applications of rec' to subtrees, i.e. if rec'' was instead treated as an abbreviation and substituted wherever it appears, this would just be structural recursion.

Is there any way to achieve such an effect and avoiding writing out rec' base left right both every time?

[Raghuram]

Indeed, Theorem Proving in Lean 4 seems to be saying that letdoes this, but that doesn't work here:

...
def Tree.rec' ...
    (tree : Tree α) : motive tree :=
let rec'' := rec' base left right both
match tree with
| node a none none         => base a
| node a (some l) none     => left a l (rec'' l)
| node a none (some r)     => right a r (rec'' r)
| node a (some l) (some r) => both a l r (rec'' l) (rec'' r)

still complains about failing to show termination.

[Mario Carneiro]

Raghuram said:

-- Just noticed I don't need to open `some`; no idea why
open Option (none)

You don't need to open either none or some because these are both exported in the global namespace

[Mario Carneiro]

If the where was abbreviating something more complicated the answer might be different, but in this case there is a simpler alternative which is to use variable instead of binders left of the colon; these don't appear in the function call in recursive occurrences

[Mario Carneiro]

variable {motive : Tree α → _}
  (base : (a:α) → motive (node a none none))
  (left : (a:α) → (l:Tree α) → motive l → motive (node a l none))
  (right : (a:α) → (r:Tree α) → motive r → motive (node a none r))
  (both : (a:α) → (l r : Tree α) → motive l → motive r → motive (node a l r)) in
def Tree.rec' : (tree : Tree α) → motive tree
| node a none none         => base a
| node a (some l) none     => left a l (rec' l)
| node a none (some r)     => right a r (rec' r)
| node a (some l) (some r) => both a l r (rec' l) (rec' r)