Expose atomic lifetimes in the API, end many in a single step

Review changes
Download
Patches
Plain diff

Merged Expose atomic lifetimes in the API, end many in a single step

ivanbakel/lambda-rust:atomic_lft_promotion into master

Overview 10
Commits 4
Pipelines 0
Changes 16

Merged Isaac van Bakel requested to merge ivanbakel/lambda-rust:atomic_lft_promotion into master 10 months ago

Overview 10
Commits 4
Pipelines 0
Changes 16

This turns out to be useful for my borrow-checker proofs, which require the ability to mass-end lifetimes to model loan termination without generating an inordinate number of laters.

This extracts the proof that atomic lifetimes can end from lft_create_strong as a standalone lemma, and then proves a stronger version of that lemma that terminates arbitrarily many atomic lifetimes at the same time (which is allowed because they don't overlap.) In fact, I think this generalises to being allowed to terminate any number of lifetimes at in the same step, but that requires some more set/multiset theory to prove, I think.

To prove this, I require a few data structure lemmas which I am trying to upstream. Two are going into iris!1049 (merged). The gset_to_map mass-update lemma is harder to generalise - I thought about including it upstream, but it's rather specific here and it doesn't seem to have a nice "kernel" to extract out that would keep the proof burden in these changes small.