Zulip Chat Archive

Stream: new members

Topic: Proving termination of a function that updates array


Muqsit Azeem (Feb 05 2024 at 16:02):

I have the following functions.. Lean requires a proof of termination for set_elements and failed to synthesize one.

def set_elements (arr : Array Nat) (index : Nat) : Array Nat :=
  if h: index < arr.size then
    let idx : Fin arr.size := index, h
    set_elements (arr.set! idx 1) (idx + 1)
  else
    arr

def set_one (arr : Array Nat) : Array Nat :=
  set_elements arr 0

So I am using

termination_by _ => arr.size - index

However, as the arr is changed in every recursive call, this is not enough.
So, I proved the following and try to use this property to argue for the termination:

theorem array_size_same_after_set (arr : Array Nat) (index : Fin arr.size) (val : Nat): (arr.set index val).size = arr.size := by
  unfold Array.set
  unfold Fin.val
  unfold List.set
  split
  case h_1 _ =>
    simp_all
    unfold Array.size
    rename_i heq1
    rename_i heq2
    rw [heq2]
    unfold List.length
    split
    case h_1 =>
      simp
    case h_2 =>
      simp
  case h_2 =>
    simp
    unfold Array.size
    rename_i heq1; rename_i heq2
    rw [heq2]
    unfold List.length
    split
    case h_1 =>
      simp
    case h_2 =>
      simp

  case h_3 _ =>
    simp
    unfold Array.size
    rename_i h
    rw [h]
    rfl

here is my attempt to use the property of array_size_same_after_set.

decreasing_by
  let idx : Fin arr.size := index, h
  have size_unchanged : (arr.set idx 1).size = arr.size := array_size_same_after_set arr idx 1

However, I do not understand how to proceed to complete the termination proof.

Joachim Breitner (Feb 05 2024 at 17:08):

@loogle Array.size (Array.set _ _ _) = _

loogle (Feb 05 2024 at 17:08):

:search: Array.size_set

Joachim Breitner (Feb 05 2024 at 17:10):

Your code uses Array.set!, but your lemma is about Array.set. Maybe that is the issue? Why not use Array.set?

Joachim Breitner (Feb 05 2024 at 17:13):

This works:

import Std

def set_elements (arr : Array Nat) (index : Nat) : Array Nat :=
  if h: index < arr.size then
    let idx : Fin arr.size := index, h
    set_elements (arr.set idx 1) (idx + 1)
  else
    arr
termination_by arr.size - index
decreasing_by simp_wf; omega

It does not work with Array.set!, because the API for Array.set! is unfortunately incomplete.
Note that simp_wf happens to apply Array.size_set already (although I think that’s not actually desirable and would prefer to have to write simp separately).
In a future version of lean, omega will be part of the default termination check and this might all work out of the box.

Muqsit Azeem (Feb 05 2024 at 19:23):

Thank you, @Joachim Breitner ! It works.


Last updated: May 02 2025 at 03:31 UTC