From 031c391455882431317a767d6653116cb27bea7a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 May 2018 17:15:36 +0200
Subject: [PATCH] provide big_op lemmas outside of bi module

There's a very low risk of these conflicting with Coq's standard library
---
 theories/bi/bi.v                 | 7 +++++++
 theories/program_logic/lifting.v | 2 +-
 theories/program_logic/ownp.v    | 4 ++--
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index b1d4c8a78..86a7c24b8 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -6,9 +6,16 @@ Module Import bi.
   Export bi.interface.bi.
   Export bi.derived_laws_bi.bi.
   Export bi.derived_laws_sbi.bi.
+  (* For better compatibility with some developments created during
+     gen_proofmode times, also provide bigops inside the bi
+     module. *)
   Export bi.big_op.bi.
 End bi.
 
+(* For better compatibility with pre-gen_proofmode-Iris, also provide
+   bigops outside of the bi module. *)
+Export bi.big_op.bi.
+
 (* Hint DB for the logic *)
 Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : BI.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index b014954d0..502a0ea45 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -104,7 +104,7 @@ Proof.
   iApply (wp_lift_pure_det_step with "[HWP]").
   - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
   - destruct s; naive_solver.
-  - by rewrite bi.big_sepL_nil right_id.
+  - by rewrite big_sepL_nil right_id.
 Qed.
 
 Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 538e82292..f3c368596 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -170,7 +170,7 @@ Section lifting.
     {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
   Proof.
     intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
-    rewrite bi.big_sepL_nil right_id. by apply bi.wand_intro_r.
+    rewrite big_sepL_nil right_id. by apply bi.wand_intro_r.
   Qed.
 
   Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
@@ -188,7 +188,7 @@ Section lifting.
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?bi.big_sepL_nil ?right_id; eauto.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End lifting.
 
-- 
GitLab