The current axioms of BI imply emp ≡ True
As the subject states, the current axiomatization of the plainly modality implies emp ≡ True.
In particular, the guilty parties are the axioms prop_ext
and plainly_emp_intro
.
I am not sure whose axioms they are, but I hope either @robbertkrebbers or @jjourdan knows the history.
I believe this must be an error, since otherwise there is no point in having emp
.
From iris.bi Require Import interface.
Import bi.
Section bi_emp.
Context {PROP : bi}.
Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
Lemma bar: emp ⊢ (True → emp) ∧ (emp → True).
Proof.
apply and_intro.
- apply impl_intro_r, and_elim_l.
- apply impl_intro_r, pure_intro; exact I.
Qed.
Lemma baz: True ⊢ ((True : PROP) ≡ emp).
Proof.
transitivity (bi_plainly (emp : PROP))%I; first apply plainly_emp_intro.
transitivity (bi_plainly ((True → emp : PROP) ∧ (emp → True))%I).
{ apply plainly_mono, bar. }
apply prop_ext.
Qed.
End bi_emp.