# Zulip Chat Archive

## 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