Zulip Chat Archive

Stream: new members

Topic: extracting part of a recursive definition


Eric Wieser (Jun 17 2020 at 20:15):

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 (Jun 17 2020 at 20:17):

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

Jalex Stark (Jun 17 2020 at 20:22):

I recommend using finset.sum from algebra.big_operators

Eric Wieser (Jun 17 2020 at 20:23):

fsum is a contrived example here.

Eric Wieser (Jun 17 2020 at 20:23):

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 (Jun 17 2020 at 20:27):

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 (Jun 17 2020 at 20:29):

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

Eric Wieser (Jun 17 2020 at 20:29):

Indeed, that is my issue

Eric Wieser (Jun 17 2020 at 20:29):

And after that, I can just use rfl


Last updated: Dec 20 2023 at 11:08 UTC