general lemma that a fixpoint is Persistent/Absorbing/Affine

Something got me thinking about when an internally defined fixpoint is persistent, and this is the result of that -- there is a general principle that looks roughly like what I expected, but it needs BiAffine and I don't quite know why. Also it would seem like this should not just work for Persistent but for all sorts of things. And I cannot quite figure out what to do with greatest fixpoints since we cannot do coinduction since there is this □ modality blocking the goal...

Is this of any use? I am also okay with just throwing it away.

Robbert has then strengthened the lemmas and also added some for Absorbing and Affine.

assigned to @jung

Also it would seem like this should not just work for Persistent but for all sorts of things.

Also for Timeless? (I once thought I needed that, and failed to prove that.)

FWIW these principles tend to not be obvious, so it's nice if they're already available :-). I don't currently have a strong usecase, but dot-iris uses persistence of a pure total wp defined using least fixpoints (tho it can use a simpler proof).

unassigned @jung

added 2 commits

• f4545892 - Fix some very long lines.
• ac867ab3 - Add lemmas for affine/absorbing/and strong variants for persistent.

Compare with previous version

added 15 commits

• ac867ab3...297fa447 - 13 commits from branch master
• 944d62c9 - general lemma that a fixpoint is Persistent
• 39b728f9 - Add lemmas for affine/absorbing/and strong variants for persistent.

Compare with previous version

changed title from general lemma that a fixpoint is Persistent to general lemma that a fixpoint is Persistent/Absorbing/Affine

changed the description

added 1 commit

• 627177b3 - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

resolved all threads

LGTM. Do you want to mention this is the changelog? Seems like a neat new set of lemmas.

Sounds good to mention in the changelog.

added 10 commits

• 627177b3...2f866db4 - 6 commits from branch master
• a52b29fc - general lemma that a fixpoint is Persistent
• c5d09720 - Add lemmas for affine/absorbing/and strong variants for persistent.
• 2056ec6f - Apply 2 suggestion(s) to 1 file(s)
• 449ced9b - changelog

Compare with previous version

All right, good to go then?