Add notations for `<affine> ⌜ ⌝` and friends.
This MR adds the following notations:

⌜⌜ φ ⌝⌝
for<affine> ⌜ φ ⌝

⎡⎡ P ⎤⎤
for<affine> ⎡ P ⎤

x ≡≡ y
for<affine> (x ≡ y)

x ≼≼ y
for<affine> (x ≼ y)
So the idea is: doubling the symbol makes it affine. This should also scale to ✓✓ x := <affine> (✓ x)
, once we have ✓
for any SBI.
I think this is a more feasible alternative to earlier discussions where we planned to make the ordinary notations the affine ones, because:
 Most users of Iris don't use linear BIs, so the alternative would be an invasive change, whereas the current MR is trivial.
 Many lemmas don't hold for the affine version. For example
f ≡ g ⊣⊢ ∀ x, f x ≡ g x
does not hold for≡≡
. So if the affine version is the default, we need to duplicate all our lemmas, similar to how we have duplicated all lemmas for<pers>
and□
. This sounds like too much work for too little gain. In proofs with the present MR, you would typically move the affine version into the persistent context, thus stripping the affine modality, allowing you to use the lemmas for the nonaffine version.  Some lemmas would need absorbing modalities for the affine versions. For example
own γ x ⊢ ✓ x
would not hold in an affine BI if✓
where affine. (This example only applies once we have a generalown
and✓
, there might be other examples in our current codebase already).  We support instances of
Embed
where⎡ P ⎤
is affine and where it is not, so having<affine> ⎡ _ ⎤
as the default would not be desired. For example, the embedding ofiProp
intoironProp
is not affine, so you often want to use⎡⎡ P ⎤⎤
. However, ifBiEmbedEmp
holds, you want to use⎡ P ⎤
(without affine modality), so that⎡ P ⎤
is affine ifP
is affine.
TODO: Since there are not many uses of these new notations, we should add some tests. In particular, we should test that ⎡ ⎡ P ⎤ ⎤
is not pretty printed as ⎡⎡ P ⎤⎤
.
Edited by Robbert Krebbers