extracting part of a recursive definition

Stream: new members

[Eric Wieser]

I'm trying to prove the seemingly definitionally-true statement below, but I can't make any progress.
Essentially, I want to extract the update rule from nat.rec_on.

def fsum : (ℕ → ℕ) → ℕ → ℕ :=
  λ f n, nat.rec_on n (f 0) (λ n' ihn', f (nat.succ n') + ihn')

theorem fsum_succ (f : ℕ → ℕ) (n : ℕ) : fsum f n.succ = fsum f n + f (nat.succ n) := sorry

Am I missing an obvious trick here?

[Eric Wieser]

Nevermind, library_search solved if for me (usually it consumes too much memory for me)

[Jalex Stark]

I recommend using finset.sum from algebra.big_operators

[Eric Wieser]

fsum is a contrived example here.

[Eric Wieser]

But is there an easy way to pull out the recursive definition of a function without repeating it in a theorem as I do above?

[Jalex Stark]

import data.nat.basic
import tactic

def fsum : (ℕ → ℕ) → ℕ → ℕ :=
  λ f n, nat.rec_on n (f 0) (λ n' ihn', f (nat.succ n') + ihn')

theorem fsum_succ (f : ℕ → ℕ) (n : ℕ) : fsum f n.succ = fsum f n + f (nat.succ n) :=
begin
  conv_lhs { rw fsum },
  dsimp, ring,
end

[Patrick Massot]

Eric, I think your problem is addition is not written in the same order in your definition and your theorem.

[Eric Wieser]

Indeed, that is my issue

[Eric Wieser]

And after that, I can just use rfl