Factor plainly out of main BI interface

The intention is to make the axioms compatible with plainly P r := forall s, P s in linear BIs. This is needed to obtain propositional extensionality.

We should not remove laws that no longer hold in the linear case. They still hold in the affine case, and @amintimany needs them, so we should have versions of them parameterized by BiAffine or something weaker.

Fair enough. However, with 1500 lines of derived laws, it is unclear which were shown "just because" and are actually needed.

Apart from those for the combined modality, all of them exist in Iris master, so they should be preserved.

All of them? Surely not plainly_and_emp_elim P : emp ∧ bi_plainly P ⊢ P. That's just silly to have in the presence of plainly_elim.

That's an expanded version of the combined modality :)

I know. And we don't have that any more. So it seems fine to drop that law.

Oh, also, I am aware that the notation could be used more consistently. We can do that when we know this actually works.

Yes, hence I said all of them, apart from those involving the combined modality (or emp for that matter) should be preserved.

But sure, let's first see whether this stuff actually works before restoring these laws.

With the newly added "or emp" clause, I find myself agreeing much more :)

E.g, Amin certainly doesn't need plainly_True_emp : bi_plainly True ⊣⊢ bi_plainly emp?

He does not.

added 1 commit

• 205285b9 - recover plainly_sep for affine BIs, and some other laws

Compare with previous version

I recovered what I removed from derived_laws.v.

But sure, let's first see whether this stuff actually works before restoring these laws.

Ack.

Btw, there is another law we could ask for: emp |- (plainly exists \pred) -> exists plainly pred. Using this, I think one could derive that affinely_plainly commutes with existentials.

Okay so here is the problem with tac_always_intros: With the proposed definition of ■, the intended behavior "make sure the affine-persistent context is all pure plain and clear the spatial context, then remove the ■ in the goal" is just wrong. We would then be proving the new goal with an empty spatial context; in particular, we would be proving the new goal with a context that entails emp. So instead of showing it for all resources, we only show it for emp.

My proposed fix is based on the observation that pure plain and affine are orthogonal in a linear setting. So what iAlways should do is remove everything non-pureplain from both contexts -- this could mean leaving this behind in the spatial context, as pure plain does not imply affine! (So, actually, we probably could allow a non-empty spatial context even for introducing persistent? Some persistent things may not be able to move to the affine-persistent context, after all.) Next, it moves everything from the affine-persistent context to the spatial context. Now we have an empty affine-persistent context and only pure plain things in the spatial context. Now we can remove the ■.

My proposed fix is based on the observation that pure and affine are orthogonal in a linear setting.

I am lost here, what does pure (=Coq pure?) have to do with this?

Sorry, I meant plain everywhere I said pure.

I do not understand why this is sound, when both contexts are empty, you cannot introduce ■ P.

Why not only allow one to introduce ■ P when P is absorbing?

when both contexts are empty, you cannot introduce ■ P.

What do you mean? You can introduce ■ when the affine-persistent context is empty and the spatial context is all plain. In that case, the context is [/\] nil /\ [*] \Gamma where everything in \Gamma is plain, so we can turn this into [/\] nil /\ [*] plainly \Gamma which implies plainly [*] \Gamma so we can introduce the goal.

Why not only allow one to introduce ■ P when P is absorbing?

That seems like a pretty arbitrary restriction.