upstream things

We have a bunch of things that should be upstreamed. @simonspies @msammler @lgaeher if you remember anything else you proved here that should be in Iris/std++, please add that to the list. :)

• all/most things in https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulang/base.v @jung (remainder blocked on iris#429)
• some tweak to the fixpoint construction in https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/logic/fixpoints.v (recursive calls are non-expansive; stronger coinduction principle) @lgaeher iris!725 (merged)
• the things at the top of https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulation/slsls.v @robbertkrebbers
  • curry/uncurry
  • NonExpansive3/NonExpansive4
• https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/simulation/relations.v @jung
• IntoIH instance @robbertkrebbers iris#430 (closed)
• theories/stacked_borrows/logical_state.v: lookup_difference_is_Some, lookup_union_is_Some, lookup_union_Some_l' might be worth upstreaming (stdpp!315 (merged))
• https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/adequacy.v#L9 @jung stdpp!318 (merged)
• https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/helpers.v#L151
• https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/steps_opt.v#L1138 @jung stdpp!319 (merged)
• https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/wf.v#L6 @jung
• https://gitlab.mpi-sws.org/iris/simuliris/-/blob/master/theories/stacked_borrows/parallel_subst.v#L187 (should probably become something general for foldl over associative/commutative [is one of them enough?] operations)