fibonacci functions

Stream: lean4

[Joseph O]

So i wrote a fibonacci function like this:

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n => fib (n-1) + fib (n-2)

and it didn't work because I had to prove termination. i then tried

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+1 => fib (n) + fib (n-1)

and the same thing happened, but this version worked:

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => fib (n+1) + fib n

I didnt have to prove any termination at all. So my question is, is this a bug or just how the core language works?

[Kevin Buzzard]

That's certainly not a bug. Do you know what 0-1 is? If so you can probably work out what's going on.

[Joseph O]

Fundamentally, I think i am just not supposed to subtract

[Henrik Böving]

The last version of your code is simply the only one that allows lean to automatically apply structural recursion since in every recursive call the parameter you are parsing is structually smaller than the one you got.

Now if you were to e.g. take your second version and apply termination by:

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+1 => fib (n) + fib (n-1)
termination_by fib n => n

Lean will complain that:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specity your own tactic for discharging this kind of goal
n : Nat
⊢ n - 1 < Nat.succ n

and you'd have to prove this by hand since lean cannot just automagically see whats going on.

[Joseph O]

Another solution is to mark it with partial, but that is generally not really ideal

[Henrik Böving]

That's not a solution to prove termination that's telling lean to ignore termination on this one

[Joseph O]

I mean not as a solution, but to ignore the termination errors.

[Leonardo de Moura]

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+1 =>
   have : n - 1 < n + 1 := Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.lt_succ_self ..) -- This auxiliary prop will be proved automatically in the future
   fib n + fib (n-1)

[Henrik Böving]

What does the .. syntax do? @Leonardo de Moura

[loki der quaeler]

I believe it's denoting that the arguments can be inferred - see the bottom of this page: https://leanprover.github.io/theorem_proving_in_lean4/interacting_with_lean.html

[Henrik Böving]

Ah so a multi _ alias I see

[Leonardo de Moura]

I think the .. notation + named arguments is also quite useful for writing patterns.

inductive Foo
  | mk₁ (x y z w : Nat)
  | mk₂ (x y z w : Nat)

def Foo.z : Foo → Nat
  | mk₁ (z := z) .. => z
  | mk₂ (z := z) .. => z

Foo.z will not break if we add new fields to the constructors.

[Kyle Miller]

Joseph O said:

So i wrote a fibonacci function like this:

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n => fib (n-1) + fib (n-2)

and it didn't work because I had to prove termination.

Just to mention what a problem is that prevents you from showing termination here, with match statements each pattern is independent: the third case doesn't "know" that n is neither 0 nor 1.

If match could somehow give you that information (maybe as n ≠ 0 ∧ n ≠ 1), then you'd be able to show the function terminates.

[Kyle Miller]

You could say the plus patterns (like n+2) are a way to avoid needing a fancy feature like that while still being relatively convenient.

[Mario Carneiro]

Note that lean 4 has that fancy feature, so potentially you could use it to prove the first one is terminating too

[Mario Carneiro]

I don't think there is syntax to expose the failing cases to the match expression itself though

[Leonardo de Moura]

If match could somehow give you that information (maybe as n ≠ 0 ∧ n ≠ 1), then you'd be able to show the function terminates.

We have support for this only when reasoning about code that uses match. The split tactic will add this kind of antecedent.

def foo : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n => n + 2

example : foo (n + 2) ≥ n + 4 := by
  unfold foo
  split
  trace_state -- In the third goal we have extra hypotheses that make sure the previous cases were not taken.
  case h_1 h => simp_arith at h
  case h_2 h => simp_arith at h
  case h_3 h _ _ _ => subst h; simp_arith

[Leonardo de Moura]

Mario Carneiro said:

I don't think there is syntax to expose the failing cases to the match expression itself though

Unfortunately, we don't. We only have support for this when reasoning about match expressions as in the example above.

[Joseph O]

Thanks for these great answers! :tada: :+1:

[Joseph O]

Not really related to the original question, but why is this not structural recursion

def List.unfoldr (f : β → Option (α × β)) (s : β) : List α :=
  match f s with
  | none => []
  | some (a, b') => a::(unfoldr f b')

nor this

def List.unfoldlAux (f : β → Option (α × β)) (s : β) (acc : List α) : List α :=
  match f s with
  | none => acc
  | some (a, a') => unfoldlAux f a' (a::acc)

and how can i make it structural

[Joseph O]

i could just mark them with partial and leave it like that, as these functions are for personal use, but why may they never terminate?

[Arthur Paulino]

It's not clear to me why f s can eventually be none (I'm guessing that's when you want your functions to terminate)

[Mario Carneiro]

To answer the question "why is it not structural recursion": A structural recursion begins by matching on one of the function arguments, and then calling the function only on the values coming out of that match. Here you are matching on f s, which is not a function argument, and you are calling yourself recursively on b' which is not a value coming from a match on said function argument

[Mario Carneiro]

As arthur says, not only is this not structurally recursive, it's not well founded recursive either, and you can in fact make it loop by passing the function (\lam a, some (0, a)) for f

[Joseph O]

Mario Carneiro said:

As arthur says, not only is this not structurally recursive, it's not well founded recursive either, and you can in fact make it loop by passing the function (\lam a, some (0, a)) for f

but what can i do to match on the argument?

[Joseph O]

it wouldnt help

[Joseph O]

I feel like for my purpose just marking it with partial would suffice

[Joseph O]

but for the future, how would the structural recursive version look like?

[Arthur Paulino]

Wanna describe the problem you're trying to solve verbally on another thread to clear out the #xy noise? I suspect you'll need to rethink the whole solution design because your function can indeed loop forever for some functions f (e.g. with Mario's example).

[Mauricio Collares]

unfoldr is a useful function in general, but I guess in Lean it should return something like docs#stream instead of a List

[Leonardo de Moura]

Joseph O said:

but for the future, how would the structural recursive version look like?

As @Mario Carneiro pointed out your function does not terminate in general. You can change the signature a bit, and ask the user to show that the new b is "smaller". Here are some examples

def List.unfoldr {α β : Type u} [sz : SizeOf β] (f : (b : β) → Option (α × { b' : β // sizeOf b' < sizeOf b})) (b : β) : List α :=
  match f b with
  | none => []
  | some (a, ⟨b', h⟩) => a :: unfoldr f b'

def tst1 (n : Nat) : List Nat :=
  List.unfoldr (b := n) fun
    | 0 => none
    | b+1 => some (3*n - b*2, ⟨b, by simp_arith⟩)

#eval tst1 10

def tst2 (n : Nat) : List Nat :=
  -- Similar example where we provide our custom `SizeOf` instance
  List.unfoldr (sz := ⟨fun b => n - b⟩) (b := 0) fun b =>
    if h : b < n then
      some (b*2, ⟨b+1, by decreasing_tactic⟩)
    else
      none

#eval tst2 10

-- More general (and less convenient to use) version that can take an arbitrary well-founded relation.
def List.unfoldr' {α β : Type u} [w : WellFoundedRelation β] (f : (b : β) → Option (α × { b' : β // w.rel b' b})) (b : β) : List α :=
  match f b with
  | none => []
  | some (a, ⟨b', h⟩) => a :: unfoldr' f b'
termination_by unfoldr' b => b

-- We need the `master` branch to test the following example

def tst3 (n : Nat) : List Nat :=
  List.unfoldr' (b := n) fun
    | 0 => none
    | b+1 => some (3*n - b*2, ⟨b, by decreasing_tactic⟩)

#eval tst3 10

def tst4 (n : Nat) : List Nat :=
  List.unfoldr' (w := invImage (fun b => n - b) inferInstance) (b := 0) fun b =>
    if h : b < n then
      some (2*b, ⟨b+1, by decreasing_tactic⟩)
    else
      none

#eval tst4 10

[Leonardo de Moura]

If the angle brackets bother you, you can define a macro. Example:

notation "#(" a ")" => ⟨a, by decreasing_tactic⟩

def tst3 (n : Nat) : List Nat :=
  List.unfoldr' (b := n) fun
    | 0 => none
    | b+1 => some (3*n - b*2, #(b))

#eval tst3 10

[Siddhartha Gadgil]

Thanks for the very helpful explanations and the updated docs. Can someone confirm my understanding of all the cases?

• To prove termination, we need a well-founded relation and a proof that the argument is decreasing for recursive calls (where decrease is with respect to the given relation).
• If there is no termination_by, a well-founded relation is derived (if possible) by implicit resolution on the arguments of the function. It is an error if the typeclass resolution fails.
• If termination_by is specified, it maps the arguments of the function to a type α and implicit resolution looks for a well-founded relation on α (which we may view as giving a pull-back relation on the original arguments). Again it is an error if the implicit resolution fails, but this time for α .
• In either case, we have to show that arguments for recursive calls are decreasing with respect to the well-founded relation. By default this is done using the decreasing_tactic, with an error if this fails and decreasing_by is not specified. One can instead use decreasing_by to specify the tactic.
• A useful trick to make things elegant is to note that decreasing_tactic includes assumption, so one can include a have statement that proves arguments are decreasing, and this gets picked up by assumption. This is especially useful if we have multiple recursive calls, since the appropriate have can be added just before each call (this is helpful to lean and to the reader).

Thanks.

[Joseph O]

this one doesnt terminate:

def List.unfoldr {α β : Type u} [sz : SizeOf β] (f : (b : β) → Option (α × { b' : β // sizeOf b' < sizeOf b})) (b : β) : List α :=
  match f b with
  | none => []
  | some (a, ⟨b', h⟩) => a :: unfoldr f b'
``` just saying

[Joseph O]

and the second version has a type mismatch image.png

[Leonardo de Moura]

@Joseph O You need the Lean 4 master branch.
Note that this examples are now in our CI :)

[Sebastian Ullrich]

(also please don't quote entire (long) comments)

[Joseph O]

Sebastian Ullrich said:

(also please don't quote entire (long) comments)

Ah sorry

[Joseph O]

How do i get the master branch? Do i have to clone from source then?

[Arthur Paulino]

I usually wait for the next nightly release

[Joseph O]

Yeah I would do that. Why do the examples @Leonardo de Moura posted not work on the current nightly version? Was something added?

[Leonardo de Moura]

Joseph O said:

How do i get the master branch? Do i have to clone from source then?

Yes, this is an option, but the repo is quite big. Another option is to press the green "Code" button at GitHub, and select "Download Zip". The zip file includes just the master branch. The current nightly build is good enough for part of the examples.

[Leonardo de Moura]

Joseph O said:

Yeah I would do that. Why do the examples Leonardo de Moura posted not work on the current nightly version? Was something added?

The current nightly build is missing this commit https://github.com/leanprover/lean4/commit/619186b2a839ebd191257d78595d240e8eab47d7

[Leonardo de Moura]

It will probably be there tomorrow.

[Leonardo de Moura]

Without this commit, code generation will fail in the example that uses invImage.

[Joseph O]

ok well thank you

[Sebastian Ullrich]

Perhaps we should postpone the nightly cut-off time by a few hours so it's night for both of us :grinning:

[Sebastian Ullrich]

8AM CET/11PM PT sounds reasonable enough? Now I just need to find out the server timezones of GitHub and of the new bot

[Leonardo de Moura]

@Siddhartha Gadgil Thanks for writing the summary. I included it in "Theorem Proving in Lean 4"

[Joseph O]

What does sizeOf do in your function @Leonardo de Moura ?

[Leonardo de Moura]

sizeOf is an auxiliary function we use to prove termination. It has type:

{α : Sort u} → [SizeOf α] → α → Nat

When we declare a new inductive type or structure, Lean automatically generates a SizeOf instance for this type and equation theorems. For example, here are the theorems generated for Lists.

#check @List.nil.sizeOf_spec
--  ∀ {α : Type u} [inst : SizeOf α], sizeOf [] = 1
#check @List.cons.sizeOf_spec
-- ∀ {α : Type u} [SizeOf α] (head : α) (tail : List α), sizeOf (head :: tail) = 1 + sizeOf head + sizeOf tail

The decreasing_tactic uses these theorems when proving termination.
For Nat, the SizeOf instance is just the identity function.
The short answer is: SizeOfalready exists and was a convenient way of making List.unfoldr work for different types.

In the List.unfoldr example, Lean shows termination using the decreasing_tactic, this tactic succeeds because it also uses the assumption tactic, and we have h : sizeOf b' < sizeOf b in the context. In tst1, when our function returns a new b, we also show sizeOf b < sizeOf (b+1) using simpArith.

[Joseph O]

What syntatic sugar are you using in tst1? Also, i really need to read TPIL4

[Joseph O]

Or else im never going to be able to prove termination of my functions

[Leonardo de Moura]

Are you referring to ⟨b, by simp_arith⟩? This is the anonymous constructor notation. We can use it for types that have only one constructor. In this case, it expands to Subtype.mk b (by simp_arith)
You can view a subtype as a pair: the element b, and a proof that sizeof b < sizeof (b+1). The proof is being constructed by the tactic by simp_arith.

[Joseph O]

I was actually referring to

fun
    | 0 => none
    | b+1 => some (3*n - b*2, ⟨b, by simp_arith⟩)

i shouldve explained myself better, sorry

[Leonardo de Moura]

This is sugar for

fun x => match x with
    | 0 => none
    | b+1 => some (3*n - b*2, ⟨b, by simp_arith⟩)

[Joseph O]

ah, like the function keyword in OCaml.