Weaken axioms for BI embeddings
The current axioms of a BI embedding are too strong; there are some BI embeddings for which the property ⎡ emp ⎤ ⊢ emp
does not hold. For example, consider (non-monotone) predicates M → sProp
where the canonical embedding is defined as ⎡P⎤ := λ _, P
.
In this MR I removed the violating axiom (i.e. turned the axiom ⎡emp⎤ ⊣⊢ emp
into emp ⊢ ⎡emp⎤
). Without this axiom, in order to prove:
Lemma embed_emp_valid (P : PROP1) : ⎡P⎤%I ↔ P.
I had to add bi_emp_valid ⎡P⎤ → bi_emp_valid P
as an axiom. Interestingly, using this axiom, one can prove Inj (⊢) (⊢) embed
.
There are also some other properties that no longer hold. I parametrized these by type classes:
Class BiEmbedEmp (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp;
}.
Class BiEmbedPlainly (PROP1 PROP2 : sbi)
`{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := {
embed_plainly_2 (P : PROP1) : ■ ⎡P⎤ ⊢ (⎡■ P⎤ : PROP2)
}.
@jjourdan can you review?