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