feat: update operation for FinFun (#470)

This PR adds `FinFun.update` and proves some basic results about the
functional interface and support of the resulting function.

---------

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: fmontesi

Cslib.lean

@@ -48,7 +48,9 @@ public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
-public import Cslib.Foundations.Data.FinFun
+public import Cslib.Foundations.Data.DecidableEqZero
+public import Cslib.Foundations.Data.FinFun.Basic
+public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs

Cslib/Foundations/Data/DecidableEqZero.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Init
+
+@[expose] public section
+
+namespace Cslib
+
+/-- Equality to `Zero` is decidable for all elements of a type (`α`). -/
+abbrev DecidableEqZero (α : Type*) [Zero α] := ∀ a : α, Decidable (a = 0)
+
+end Cslib

Cslib/Foundations/Data/FinFun.lean Cslib/Foundations/Data/FinFun/Basic.leanCslib/Foundations/Data/FinFun.lean renamed to Cslib/Foundations/Data/FinFun/Basic.lean

@@ -89,8 +89,7 @@ theorem fn_eq_eq [Zero β] {f g : α →₀ β} (h : f.fn = g.fn) : f = g :=
   ext (congrFun h)
 
 @[scoped grind =>]
-theorem congrFinFun [Zero β] {f g : α →₀ β} (h : f = g) (a : α) : f a = g a :=
-  by grind
+theorem congrFinFun [Zero β] {f g : α →₀ β} (h : f = g) (a : α) : f a = g a := by grind
 
 @[scoped grind =]
 theorem fromFun_eq [Zero β] [DecidableEq α] [∀ y : β, Decidable (y = 0)]

Cslib/Foundations/Data/FinFun/Update.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Data.FinFun.Basic
+public import Cslib.Foundations.Data.DecidableEqZero
+public import Mathlib.Data.Finset.SDiff
+
+@[expose] public section
+
+/-! # Update for finite functions
+
+This module defines the update operation for finite functions, that is, the equivalent of
+`Function.update` for `FinFun`.
+-/
+
+namespace Cslib.FinFun
+
+variable [Zero β] [DecidableEq α] [DecidableEqZero β]
+
+set_option linter.tacticAnalysis.verifyGrindOnly false in
+/-- `FinFun` equivalent of `Function.update`. -/
+def update (f : α →₀ β) (a : α) (b : β) : α →₀ β where
+  fn := Function.update f.fn a b
+  support := if b = 0 then f.support \ {a} else f.support ∪ {a}
+  mem_support_fn := by
+    by_cases b = 0
+    · grind only [= Finset.mem_sdiff, = Finset.mem_singleton, = Function.update, = mem_support_fn]
+    · grind
+
+/-- `FinFun.update` is consistent with `Function.update`. -/
+@[scoped grind =, simp]
+theorem update_coe (f : α →₀ β) : (f.update a b : α → β) = Function.update f a b := by
+  grind [update]
+
+/-- Conditional characterisation of the functional interface of `FinFun.update`. -/
+@[scoped grind =]
+theorem update_apply (f : α →₀ β) : ((f.update a' b) a) = if a = a' then b else f a := by
+  simp [Function.update_apply]
+
+/-- Conditional characterisation of the support of an updated `FinFun`. -/
+@[scoped grind =]
+theorem update_support (f : α →₀ β) :
+    (f.update a b).support = if b = 0 then f.support \ {a} else f.support ∪ {a} := by simp [update]
+
+/-- Updating a finite function on the same key is the same as doing the last update. -/
+@[scoped grind =, simp]
+theorem update_idem (f : α →₀ β) : (f.update a b).update a b' = f.update a b' := by grind
+
+/-- Updates on different keys commute. -/
+@[scoped grind =]
+theorem update_comm (f : α →₀ β) (h : a ≠ a') :
+    (f.update a b).update a' b' = (f.update a' b').update a b := by
+  grind only [←= ext, = update_apply]
+
+/-- Updates that do not change mappings are redundant. -/
+@[scoped grind =]
+theorem update_self (f : α →₀ β) : (f.update a (f a)) = f := by grind
+
+/-- Updating a function never grows its support more than adding the key. -/
+@[scoped grind .]
+theorem update_support_subseteq (f : α →₀ β) : (f.update a b).support ⊆ f.support ∪ {a} := by grind
+
+end Cslib.FinFun