Q: Nat.any vs Nat.anyTR

Stream: lean4

[Yuri de Wit]

I see two versions of Nat.any: one that is tail recursive and one that isn't.

@[specialize] def any (f : Nat → Bool) : Nat → Bool
  | 0      => false
  | succ n => any f n || f n

@[inline] def anyTR (f : Nat → Bool) (n : Nat) : Bool :=
  let rec @[specialize] loop : Nat → Bool
    | 0      => false
    | succ m => f (n - succ m) || loop m
  loop n

Curious: what is the reason to keep the non-tail recursive version?

[Yuri de Wit]

[Compiler.result] size: 9
    def Nat.any f x.1 : Bool :=
      cases x.1 : Bool
      | Nat.zero =>
        let _x.2 := false;
        return _x.2
      | Nat.succ n.3 =>
        let _x.4 := Nat.any f n.3;
        cases _x.4 : Bool
        | Bool.false =>
          let _x.5 := f n.3;
          return _x.5
        | Bool.true =>
          return _x.4

I guess we should also share the f n computation.

[Yuri de Wit]

Just for a bit of context, I am querying LCNF to find recursive declarations that are not tail recursive.

[Mario Carneiro]

We could just mark the non-TR version as noncomputable here to prevent the compiler from generating the code, but there is nothing on the definition of any itself that makes it clear that it is being replaced, like implemented_by, so this might cause problems for the noncomputable checker

[Wojciech Nawrocki]

To the original question "what is the reason to keep the non-tail recursive version", I am assuming, as in other cases such as map and mapTR, it is that the straightforward version is easier to reason about as a mathematical model (maybe not soo much in this particular case but in general it's definitely true).