From fc717f6b9a19b24d2fbad6c18d186ff13a4317a2 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Fri, 26 Aug 2022 12:28:41 +0200
Subject: [PATCH] Add soundness lemma for envs_clear_intuitionistic

---
 iris/proofmode/environments.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 5f922b281..b728ad51d 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -738,6 +738,16 @@ Proof.
   - rewrite -persistent_and_sep_assoc left_id. done.
 Qed.
 
+Lemma envs_clear_intuitionistic_sound Δ :
+  of_envs Δ ⊢
+  env_and_persistently (env_intuitionistic Δ) ∗ of_envs (envs_clear_intuitionistic Δ).
+Proof.
+  rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
+  rewrite persistent_and_sep_1.
+  rewrite (pure_True); first by rewrite 2!left_id.
+  destruct Hwf. constructor; simpl; auto using Enil_wf.
+Qed.
+
 Lemma env_spatial_is_nil_intuitionistically Δ :
   env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
 Proof.
-- 
GitLab