Proving termination of a function that updates array

Stream: new members

[Muqsit Azeem]

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]

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

[loogle]

:search: Array.size_set

[Joachim Breitner]

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

[Joachim Breitner]

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]

Thank you, @Joachim Breitner ! It works.