Zulip Chat Archive

Stream: new members

Topic: Proving function defined via well founded recursion

erd1 (Sep 16 2021 at 07:03):

Hi, I've just started learning lean, and started trying random things, but I can't seem to make the following code work, can someone please help me?

open nat

def f :   
| 0 := 0
| (succ n) :=
  have succ n / 2 < succ n, from sorry,
  f (succ n / 2)

lemma lem : f 0 = 0 := rfl

The type checker throws an "type mismatch" error at the lemma below.
Confusingly, this snippet type-checks at https://leanprover.github.io/live/latest/
but not at https://leanprover-community.github.io/lean-web-editor
and I'm quite baffled right now.

Last updated: Dec 20 2023 at 11:08 UTC