TL;DR: There is no logical reason I see that Lean can't do this. It just seems like it is not implemented (and possibly it will be implemented in the future as this comment on Zulip suggests). Nonetheless, you can directly construct this using induction (or the underlying rec operator). Moreover, since Lean is proof-irrelevant, there is no logical reason to give a proof via recursion, and in my opinion induction is always a better choice.
Mario's Carneiro's answer on Zulip from a month ago may give some light, so let me repeat it here (although I am not positive I understand it correctly):
Lean's equation compiler doesn't support direct structural recursion, which is paradoxical since it is the simplest kind of recursion.
Instead it currently supports the following two types of recursion:
- bounded recursion is like structural recursion except it also allows doing multiple layers of inductive constructors at once
- well founded recursion is where you recurse on a well founded type with a natural number measure function
Bounded recursion doesn't work for inductives in Prop, just inductive in Type u. Well founded recursion will attempt to do recursion on a natural number measure (or "height"). It might work on your toy example, but it is not powerful enough to proof that say Acc is well-founded.
A better option when using recursion to prove a Prop is just to use induction instead. In your toy example you could do:
inductive F : Prop where
| nil (n: Nat)
| fn (f: Nat → F)
theorem inc: F → F := by
intro t
induction t with
| nil n => exact F.nil (n+1)
| fn f f_ih => exact F.fn f_ih
Not only is this proof valid, but it is also a faithful representation of your recursive construction. The induction hypothesis f_ih : forall x : Nat, F is the inductive equivalent of the recursive step inc (f ...) in your structural recursion. The induction hypothesis is assuming that inc holds true for all the outputs of f: Nat -> F. (Notice both f_ih and lambda n, inc (f n) have type Nat -> F.)
Nonetheless, Lean is proof-irrelevant and the proof doesn't matter logically. This is even more reason to avoid recursive proofs of Props, when induction is a better choice.
Digging deeper, we can even give a convincing argument that this is the correct way to translate your recursive proofs to induction. If we print the inductive proof above we get:
theorem inc : F → F :=
fun t => F.rec (fun n => F.nil (n + 1)) (fun f ih => F.fn ih) t
Now, we can see that this exact definition when applied to the Type-valued F gives exactly the same result as your recursive formula:
inductive F where
| nil (n: Nat)
| fn (f: Nat → F)
def inc1: F → F
| F.nil n => F.nil (n+1)
| F.fn f => F.fn fun n => inc1 (f n)
def inc2 : F → F :=
fun t => F.rec (fun n => F.nil (n + 1)) (fun f ih => F.fn ih) t
-- check if they behave the same
variable (foo : Nat -> Nat -> Nat)
#reduce inc1 (F.fn (fun n => F.fn (fun m => F.nil (foo n m))))
-- F.fn fun n => F.fn fun n_1 => F.nil (Nat.succ (foo n n_1))
#reduce inc2 (F.fn (fun n => F.fn (fun m => F.nil (foo n m))))
-- F.fn fun n => F.fn fun n_1 => F.nil (Nat.succ (foo n n_1))
-- prove they are the same
theorem same_inc (t : F) : inc1 t = inc2 t := by
induction t with
| nil n => rfl
| fn f ih => calc
inc1 (F.fn f) = F.fn fun n => inc1 (f n) := rfl
_ = F.fn fun n => inc2 (f n) := by simp [ih]
_ = inc2 (F.fn f) := rfl
Finally, it should be noted that structural recursion seems to already be working for simpler inductive definitions in Prop:
inductive F : Prop where
| nil (n: Int)
| fn (f: F)
def inc: F → F
| F.nil n => F.nil (n+1)
| F.fn f => F.fn (inc f)
Indeed, it seems that parameters of the form (... -> F) in the inductive definition are what gives Lean 4 trouble.
def subtypeWellfounded {T: Type} (s: Set T) [wfr : WellFoundedRelation T] : WellFoundedRelation { t: T // t ∈ s } := invImage Subtype.val wfr$\endgroup$relOutdefinition, we have(relOut T s wfr.rel) = (@subtypeWellfounded T s wfr).reldefinitionally. $\endgroup$