Find better name for "emp |- P"

Currently, emp |- P is called bi_valid P and is used as a coercion from PROP to Prop. This turns out to be the right definition for the coercion (i.e., (l |-> v -* l |->{0.5} v * l |->{0.5} v)%I is provable), but the name is dubious: Usually, validity is defined as True |- P. Let's try to find a better name.

Quoting @amintimany from !122 (merged):

AFAIK validity is a model property and not a logic property. That is, valid(P) if for any interpretation I in the model I ⊧ P. The property that we usually write True ⊢ P is called provability in this terminology. Also, in this setting soundness is usually formulated as: for all P, provable(P) then valid(P).

I agree with @jung that provability is usually defined with True. However, I am not convinced if it should be the case for (linear) separation logic. One important property of provable propositions is that if P is provable then P ∧ Q ⊣⊢ Q for any Q. For separation logic I would argue that we want for a provable P to have P ∗ Q ⊣⊢ Q and indeed, correct me if I am wrong, with the emp definition of provability we get P ∗ Q ⊣⊢ Q ⊣⊢ P ∧ Q as provability implies persistence. So I am gravitating towards the emp definition of provability.

and my response:

However, at the same time this actually loses the property that for provable P, we have P ∧ Q ⊣⊢ Q for any Q. IOW, we have two notions of provability ("intuitionistic" and "spatial", or so), and two corresponding universal properties, relating them to our two notions of conjunction.

So, I propose to call this bi_spat_valid or bi_spatially_valid (it's a coercion, so a long name shouldn't be a problem), or bi_emp_valid.

mentioned in merge request !122 (merged)

[stuff about valid versus provable] ... That is, valid(P) if for any interpretation I in the model I ⊧ P.

We have shallow embeddings, so this is actually exactly what Iris' valid says.

Iris is clearly a shallow embedding, but is the generalized proofmode fundamentally restricted to shallow embeddings? I am speculating, but could one somehow instantiate it with a deep embedding formalized using some form of HOAS?

So, I propose to call this bi_spat_valid or bi_spatially_valid (it's a coercion, so a long name shouldn't be a problem), or bi_emp_valid.

bi_emp_valid sounds most appealing to me. Yet some other alternatives: bi_svalid or bi_evalid.

The thing that I don't quite like about it is that even in the affine setting you something end up writing it.

Iris is clearly a shallow embedding, but is the generalized proofmode fundamentally restricted to shallow embeddings? I am speculating, but could one somehow instantiate it with a deep embedding formalized using some form of HOAS?

Well, we certainly require binders to be handled "semantically". Deeply embedded logics with syntactic binders cannot satisfy our embedding. AFAIK doing HOAS in Coq requires some form of intentional function space; us using the normal function space for the quantifiers seems to exclude that -- so I'd be surprised if that was possible. But I don't know.

You can do HOAS like syntactic stuff, but it will break when you use higher-order quantification:

Inductive prop :=
  | PForall : forall A, (A -> prop) -> prop
  | PTrue : prop.

Check (PForall prop (fun P : prop => P)).

Note sure if one could sensibly instantiate the proof mode with such a logic.

Okay so I suggest we use bi_emp_valid. @jjourdan ?

Good for me.

Fine. Please do not rename anything until we're done with the other renaming.

Sure. I can do this, just tell me when.

mentioned in merge request !131 (merged)

Fixed by https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/131

closed

added T-proofmode label