Nested Function.update on Fin k

Stream: Is there code for X?

[chris477]

In my proofs, I have a lot of of expressions of the form

Function.update
  (Function.update
    (Function.update f
    a x)
  b y)
c z

(often nested much deeper), where f : Fin k → α, k : ℕ. The lemmas I want to prove usually in the end simplify to equality of permutations of such update structures or equality of update structures with some if-then-else expressions strewn at different places. Sometimes it happens that (in the example above) a = c, i.e. the innermost update is redundant.

Using simp and grind together with split_ifs often solves the goal, but not always and I'm wondering if there is some other data structure I could use here. I also tried adding a lemma that "sorts" the updates (because adjacent redundant updates are eliminated by simp), but usually the <-requirement is not automatically established, but even if it is, it takes a long time (both via simp and via grind).

Any help is greatly appreciated!

[Violeta Hernández]

I'd also recommend aesop for goals like these.

[Violeta Hernández]

Not sure if there's much to be done, most things on Function.update are necessarily very case-heavy arguments that one just handwaves in pen and paper maths.

[Ruben Van de Velde]

Maybe a simproc could help with this in the case where you've got a sequence of update calls and you can combine multiple non-adjacent calls

[chris477]

Ah, these are good ideas! Will look into writing a simproc to sort, followed by aesop!