Simple termination proofs

Stream: new members

[Christoph M. Wintersteiger]

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]

That have doesn't mean what you think it does

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Kyle Miller]

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]

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]

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

[Jireh Loreaux]

(there are other syntax options available too)

[Kyle Miller]

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