## Stream: new members

### Topic: Simple termination proofs

#### Christoph M. Wintersteiger (Apr 21 2022 at 16:10):

Total noob to Lean and Zulip, so bear with me! I'm toying with the idea of writing verified/verifiable programs with Lean (mainly for personal projects for now) and I've hit an issue that tells me that I don't fully understand how Lean handles termination_by.

Two versions of a trivial loop:

def sum (i:Nat) (n:Nat) : Nat :=
if i < n then
1 + (sum (i + 1) n)
else
0
termination_by sum i n => n - i


and the same with reversed order of branches:

def sum2 (i:Nat) (n:Nat) : Nat :=
if i >= n then
0
else (
-- have _ := n - (i + 1) < n - i
1 + (sum2 (i + 1) n)
)
termination_by sum2 i n => n - i


Where the first one verifies just fine, but the second one doesn't (with or without the have clause). In general, can I infer that Lean prefers the recursion first and the base cases second, or is that just an artefact of heuristics which may change at any time? I imagine there's a way to solve this problem by adding a different have clause, or by specifying a tactic via decreasing_by, but I haven't explored that yet.

#### Eric Wieser (Apr 21 2022 at 17:06):

That have doesn't mean what you think it does

#### Eric Wieser (Apr 21 2022 at 17:06):

It says "I have a statement, it's n - (i + 1) < n - i"

#### Eric Wieser (Apr 21 2022 at 17:06):

But termination wants to you to say "I have a proof of n - (i + 1) < n - i, it's ..."

#### Eric Wieser (Apr 21 2022 at 17:07):

I would guess have : i < n := sorry, is sufficient to make the recursion happy

#### Kyle Miller (Apr 21 2022 at 17:15):

Here's the right notation for have:

def sum2 (i:Nat) (n:Nat) : Nat :=
if h : i >= n then
0
else (
have : n - (i + 1) < n - i := by
-- use h to prove this
sorry
1 + (sum2 (i + 1) n)
)
termination_by sum2 i n => n - i


I also added in a dependent if since you'll need that fact to prove what's needed.

#### Christoph M. Wintersteiger (Apr 21 2022 at 17:16):

Eric Wieser said:

I would guess have : i < n := sorry, is sufficient to make the recursion happy

Thanks Eric, that changes everything! I thought the _ : is just a label for the have statement. Back to reading the manual!

#### Jireh Loreaux (Apr 21 2022 at 17:18):

the syntax is: have <label> : <type> := <term>

#### Jireh Loreaux (Apr 21 2022 at 17:19):

(there are other syntax options available too)

#### Kyle Miller (Apr 21 2022 at 17:19):

If you had written have _ : n - (i + 1) < n - i := sorry it would have been fine, note that the := comes after the type/proposition, not before

Last updated: Dec 20 2023 at 11:08 UTC