From 186ffb077fcd3a83f0c6d80ec11e539027fd77b3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Feb 2018 14:39:25 +0100
Subject: [PATCH] a BI is affine iff True |- emp
---
theories/bi/derived_laws.v | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index ec6c8d78a..c0aa5b1ff 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -673,6 +673,15 @@ Proof. apply (anti_symm _); auto using True_sep_2. Qed.
Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P.
Proof. by rewrite comm True_sep. Qed.
+Lemma True_emp_iff_BiAffine :
+ BiAffine PROP ↔ (True ⊢ emp).
+Proof.
+ split.
+ - intros ?. exact: affine.
+ - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp.
+ exact: True_intro.
+Qed.
+
Section bi_affine.
Context `{BiAffine PROP}.
--
GitLab