Port iAccu

[MackieLoeffel]

See Iris Rocq documentation at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md

[ayhon]

Is this sort of tactic even needed? I don't think evars are used as much in Lean as in Rocq

[MackieLoeffel]

This tactic is only very rarely used, even in Rocq, but then it can be very useful. I for example use it a bunch of times in DimSum: https://gitlab.mpi-sws.org/search?search=iaccu&nav_source=navbar&project_id=1744&group_id=1795&search_code=true&repository_ref=master

I don't think there is a difference between Rocq and Lean here, so it would be useful to have the tactic in Lean as well. (And it should be quite easy to implement I hope.)