Skip to content

Weaken axioms for BI embeddings

Robbert Krebbers requested to merge robbert/embed_emp into gen_proofmode

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?

Merge request reports