simplifying `let (a,b) := (x,y); f a b`

Stream: lean4

[Tomas Skrivan]

I would like simp to turn let (a,b) := (x,y); f a b into let a := x; let b := y; f a b.

Right now, simp simplifies let (a,b) := (x,y); f a b to f x y even with zeta := false. If you set iota := false then it does not get simplified at all.

These kind of simplifications are done in simproc Lean.Meta.Simp.simpMatch so it seems to me I should turn off iota and provide custom version of simpMatch.

Any tips how should I go about this?

Few examples of what I would like to have

let (a,b) := (x,y); f a b          ==>    let a := x; let b := y; f a b
let (a,b,c) := (x,yz); f a b c     ==>    let a := x; let bc := yz; let b := bc.1; let c := bc.2; f a b c

How would I go about writing such match reduction?