Sums in recursively defined functions on the natural numbers

Stream: lean4

[Thomas Preu]

I am trying to understand the faculties and limitations of Lean in defining functions on the natural numbers recursively. Is it possible to sum over values of all smaller arguments in defining the function?

Here are some naive attempts with a toy example as an MWE. They yield an error "fail to show termination".

import Mathlib.Tactic.Ring
import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Fin

#eval ∑ i in Finset.range 5, i

--does not work - Lean4 cannot establish termination of recursion ahead.
def frec1 : Nat → Nat
  | Nat.zero   => 1
  | Nat.succ n => ∑ i in Finset.range (Nat.succ n), (frec1 i)
#eval frec1 5

--does not work - Lean4 cannot establish termination of recursion ahead.
def frec2 : Nat → Nat
  | Nat.zero   => 1
  | Nat.succ n => (List.range (Nat.succ n)).map frec2 |>.foldl (· + ·) 0
#eval frec2 5

def frec3 : Nat → Nat
  | Nat.zero   => 1
  | Nat.succ n => frec3 n + frec3 n
--work around: first frec3 n means ∑ᵢ<ₙ (frec3 i) and second frec3 n stands for itself.
--this requires some rewriting on the part of the user, unsatisfactory.
#eval frec3 5

Does anyone know how to achieve this without resorting to work arounds as indicated above?

Remark: I have Lean 4.5 installed, which might be outdated and the libraries might have changed names.

[Robin Arnez]

You can use:

def frec : Nat → Nat
  | 0 => 1
  | n => ∑ i : Fin n, frec i

[Kenny Lau]

@Thomas Preu this is because when you have i in Finset.range (Nat.succ n), in the context of the application frec1 i, Lean only knows that i is a natural number

[Kenny Lau]

summing over Fin n as instructed above allows you to carry the proof of i < n

[Kenny Lau]

Finset.range (Nat.succ n) returns a term of Finset (Nat), and the summation syntax sums over a function on Nat when you have Finset Nat

[Thomas Preu]

Thanks for the help and the explanation, now it works.

[Thomas Preu]

@Kenny Lau Interestingly enough the standalone sum does not work like this.

-- works
#eval ∑ i in Finset.range 5, i
-- yields error "failed to synthesize AddCommMonoid (Fin 5)"
#eval ∑ i : Fin 5, i

Do you have an explanation for that?

[Kenny Lau]

@Thomas Preu if you just type i it interprets it as a term of Fin 5, which has no addition defined

[Kenny Lau]

but in the code above frec forces it to be coerced to Nat

[Thomas Preu]

Now it works:

#eval ∑ i : Fin 5, (↑i : Nat)

[Kenny Lau]

lean tip: basically don't ever type the uparrow, it only confuses you

[Thomas Preu]

OK, so this works better:

#eval ∑ i : Fin 5, (i : Nat)

[Ruben Van de Velde]

Kenny Lau said:

lean tip: basically don't ever type the uparrow, it only confuses you

I don't agree with this tip - sometimes you need to specify exactly where the coercion goes, e.g. (<arrow>(a+b) : Int)

[Kenny Lau]

but that isn't simp NF

[Kenny Lau]

i think it's better to drill into people the idea that the simp NF is ↑a + ↑b not ↑(a+b)

[Ruben Van de Velde]

I don't see how your comment is relevant

[Kenny Lau]

if we tell people that the idiomatic way is (term : expected type), then they will type (a + b : Int) and see ↑a + ↑b, which is the correct simpNF

[Chris Henson]

Kenny Lau said:

if we tell people that the idiomatic way is (term : expected type), then they will type (a + b : Int) and see ↑a + ↑b, which is the correct simpNF

In general, is this considered the preferred way for users to discover simp normal forms? Is there documentation that recommends this?

[Kenny Lau]

well all of the map_add lemmas look like f(a+b) = f a + f b

[Thomas Preu]

What I, as a beginner, take from this:

1. The ↑ specifies the exact subterm that is supposed to be coerced.
2. Lean output features them by default if coercions occur.
3. Usually when coercions are not automatically inferred by Lean, type annotation like (... : type) is sufficient, ↑ is not necessary, ↑ is considered obfuscating to human readers and should therefore be omitted.
4. Sometimes however, type annotation is not enough and then an additional ↑ clarifies the place of coercion.

Did I get this right from your discussion? Did I miss something?

[Kenny Lau]

that's what i think anyway

[Aaron Liu]

One more thing - the default coercion is "no coercion", so if you don't specify what to coerce to then even if you put a ↑ if you haven't disallowed "no coercion" as an option then that's what will happen.

[Robin Arnez]

I prefer something like ((a + b : Nat) : Int) for this kind of coercion -- it's a bit clearer and the elaborator can't really do anything wrong