Proving fonction is decreasing

Stream: general

[Alice Laroche]

Lets say i have defined a function that's not trivially decreasing. For the sake of argument, the 3n + 1 function.

def collatz : ℕ -> ℕ -> ℕ
| flight_time 1 := flight_time
| flight_time n := if n % 2 = 0
                   then collatz (flight_time + 1) (n / 2)
                   else collatz (flight_time + 1) (3 * n + 1)

Lean will obviously say it failed to prove the function is decreasing. How can i give such a proof ?

[Alex J. Best]

If you can come up with a well founded relation for your function then you can do it with the using_well_founded keyword.
You can find many examples in mathlib, but here is a made up one, saying how this would look for collatz is of course way harder than the question here

import tactic
def ex : ℕ -> ℕ -> ℕ
| flight_time 0 := flight_time
| flight_time (n+1) :=
if h : n % 2 = 0 then
  have 2 * (n + 2) - ((n + 2) % 2) < 2 * (n + 1) - ((n + 1) % 2) := by simp [h]; sorry, -- showing that the function defined below is decreasing
  ex (flight_time + 1) (n + 2)
else
  have 2 * (n / 2) - ((n / 2) % 2) < 2 * (n + 1) - ((n + 1) % 2) := sorry,
 ex (flight_time + 1) (n / 2)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ ⟨i, n⟩, 2 * n - n % 2)⟩],-- specifying that given i the flight time and n the second argument, that 2 * n - n % 2 is decreasing
  dec_tac := `[assumption] } -- this is the default I believe, it says to try and fill in proofs that the relationg is decreasing using the assumption tactic, this means that we can just add the have's above to provide proofs, a tactic that can prove your goals above automatically is also possible here if there is one

this is the simplest possibility for a well founded relation, we give a map to the naturals and show it decreases with every recursive call, more complicated things are also possible.

P.s. I have no idea if the goals here are provable, but hopefully the structure is clear

[Alice Laroche]

Is there a way to use a mapping to transfinite ? I can easily define a function like

def size' : my_type -> ℕ := sorry
def size'' : my_type -> ℕ := sorry

def size : my_type -> transfinite
| val := (size' val) * ω + (size'' val)

Were size always decrease, but i don't think i can if i limit myself to naturals

[Reid Barton]

You could use ordinal, but in this case it should be enough to use docs#prod.lex_wf

[Mario Carneiro]

Note that the collatz function as written is definitely not well founded, as it diverges at 0

[Mario Carneiro]

If you special case 0 to make it terminate, then it becomes an open problem. In either case you aren't going to convince lean that this function terminates. But as long as there is a proof that the function terminates, even if it has a very high transfinite order type, it should be possible to construct the function in lean, either by induction on a suitable inductive type, or using the using_well_founded mechanism to supply an inductive with even higher order type (like ordinal).

[Alice Laroche]

The collatz function was just an exemple, I don't plan to solve it huhu

[Kevin Buzzard]

The problem might even be undecidable -- Conway's FRACTRAN is a generalisation of collatz and deciding whether a FRACTRAN program terminates is undecidable