From 77dafe708dea6cfa1aceb3d51ad23969877a3ca7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Nov 2017 11:17:04 +0100
Subject: [PATCH] Import uPred proofmode class instances when importing
 base_logic.

---
 _CoqProject                                   |   1 -
 theories/base_logic/base_logic.v              | 130 +++++++++++++++++
 .../base_logic/lib/fancy_updates_from_vs.v    |   2 +-
 theories/base_logic/lib/gen_heap.v            |   1 -
 theories/base_logic/lib/wsat.v                |   1 -
 theories/base_logic/proofmode.v               | 132 ------------------
 theories/tests/proofmode_iris.v               |   2 +-
 7 files changed, 132 insertions(+), 137 deletions(-)
 delete mode 100644 theories/base_logic/proofmode.v

diff --git a/_CoqProject b/_CoqProject
index 928dd91a6..8e8bfadfa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,7 +39,6 @@ theories/base_logic/base_logic.v
 theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/deprecated.v
-theories/base_logic/proofmode.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 96b4ce2d9..a4d718524 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,5 +1,7 @@
 From iris.base_logic Require Export derived.
 From iris.bi Require Export bi.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 Module Import uPred.
@@ -16,3 +18,131 @@ Hint Resolve persistently_mono : I.
 Hint Resolve sep_mono : I. (* sep_elim_l' sep_elim_r'  *)
 Hint Immediate True_intro False_elim : I.
 Hint Immediate iff_refl internal_eq_refl : I.
+
+(* Setup of the proof mode *)
+Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
+
+Section class_instances.
+Context {M : ucmraT}.
+Implicit Types P Q R : uPred M.
+
+Global Instance from_assumption_bupd p P Q :
+  FromAssumption p P Q → FromAssumption p P (|==> Q).
+Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
+
+Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
+  @IntoPure (uPredI M) (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|==> P) φ.
+Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
+
+Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
+  @FromPure (uPredI M) (✓ a) (✓ a).
+Proof.
+  rewrite /FromPure. eapply bi.pure_elim; [done|]=> ?.
+  rewrite -cmra_valid_intro //. by apply pure_intro.
+Qed.
+
+Global Instance into_wand_bupd p q R P Q :
+  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
+Proof.
+  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
+  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
+Qed.
+
+Global Instance into_wand_bupd_persistent p q R P Q :
+  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
+Proof.
+  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
+  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
+Qed.
+
+Global Instance into_wand_bupd_args p q R P Q :
+  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
+Proof.
+  rewrite /IntoWand' /IntoWand /= => ->.
+  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
+Qed.
+
+(* FromOp *)
+(* TODO: Worst case there could be a lot of backtracking on these instances,
+try to refactor. *)
+Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance is_op_pair_core_id_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
+  CoreId  a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
+Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
+Global Instance is_op_pair_core_id_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
+  CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
+Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
+
+Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
+  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
+an [â‹…]. *)
+Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
+Proof. done. Qed.
+
+Global Instance from_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 →
+  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
+  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
+  destruct H; by rewrite persistent_and_sep.
+Qed.
+
+Global Instance into_and_ownM p (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
+Qed.
+
+Global Instance into_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
+
+Global Instance from_sep_bupd P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
+Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
+
+Global Instance from_or_bupd P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
+Proof.
+  rewrite /FromOr=><-.
+  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
+Qed.
+
+Global Instance from_exist_bupd {A} P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
+Proof.
+  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+Qed.
+
+Global Instance from_modal_bupd P : FromModal (|==> P) P.
+Proof. apply bupd_intro. Qed.
+
+Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
+Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+
+Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
+
+Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+
+Global Instance is_except_0_bupd P : IsExcept0 P → IsExcept0 (|==> P).
+Proof.
+  rewrite /IsExcept0=> HP.
+  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
+Qed.
+
+Global Instance frame_bupd p R P Q : Frame p R P Q → Frame p R (|==> P) (|==> Q).
+Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
+End class_instances.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index b77f45beb..f8e87f2f8 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -1,7 +1,7 @@
 (* This file shows that the fancy update can be encoded in terms of the
 view shift, and that the laws of the fancy update can be derived from the
 laws of the view shift. *)
-From iris.base_logic Require Import proofmode.
+From iris.base_logic Require Export base_logic.
 From iris.proofmode Require Import tactics.
 From stdpp Require Export coPset.
 Set Default Proof Using "Type*".
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index a0ac009cf..c80b066b0 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,5 +1,4 @@
 From iris.algebra Require Import auth gmap frac agree.
-From iris.base_logic Require Import proofmode.
 From iris.base_logic.lib Require Export own.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 9171275fa..5ac4139ae 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -2,7 +2,6 @@ From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import proofmode.
 Set Default Proof Using "Type".
 
 Module invG.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
deleted file mode 100644
index dc86a510c..000000000
--- a/theories/base_logic/proofmode.v
+++ /dev/null
@@ -1,132 +0,0 @@
-From iris.base_logic Require Export base_logic.
-From iris.proofmode Require Export tactics.
-From iris.algebra Require Import proofmode_classes.
-Import uPred.
-Import bi.
-
-Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
-
-Section class_instances.
-Context {M : ucmraT}.
-Implicit Types P Q R : uPred M.
-
-Global Instance from_assumption_bupd p P Q :
-  FromAssumption p P Q → FromAssumption p P (|==> Q).
-Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
-
-Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
-  @IntoPure (uPredI M) (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
-
-Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|==> P) φ.
-Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
-
-Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
-  @FromPure (uPredI M) (✓ a) (✓ a).
-Proof.
-  rewrite /FromPure. eapply bi.pure_elim; [done|]=> ?.
-  rewrite -cmra_valid_intro //. by apply pure_intro.
-Qed.
-
-Global Instance into_wand_bupd p q R P Q :
-  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
-Proof.
-  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
-Qed.
-
-Global Instance into_wand_bupd_persistent p q R P Q :
-  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
-Proof.
-  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
-  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
-Qed.
-
-Global Instance into_wand_bupd_args p q R P Q :
-  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
-Proof.
-  rewrite /IntoWand' /IntoWand /= => ->.
-  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
-Qed.
-
-(* FromOp *)
-(* TODO: Worst case there could be a lot of backtracking on these instances,
-try to refactor. *)
-Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
-Proof. by constructor. Qed.
-Global Instance is_op_pair_core_id_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
-  CoreId  a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
-Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-Global Instance is_op_pair_core_id_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
-  CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
-Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-
-Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
-  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
-Proof. by constructor. Qed.
-(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
-an [â‹…]. *)
-Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
-Proof. done. Qed.
-
-Global Instance from_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
-Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
-  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
-  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H; by rewrite persistent_and_sep.
-Qed.
-
-Global Instance into_and_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
-Qed.
-
-Global Instance into_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
-
-Global Instance from_sep_bupd P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
-Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
-
-Global Instance from_or_bupd P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
-Proof.
-  rewrite /FromOr=><-.
-  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
-Qed.
-
-Global Instance from_exist_bupd {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
-
-Global Instance from_modal_bupd P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
-
-Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
-Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
-
-Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-
-Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
-
-Global Instance is_except_0_bupd P : IsExcept0 P → IsExcept0 (|==> P).
-Proof.
-  rewrite /IsExcept0=> HP.
-  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
-Qed.
-
-Global Instance frame_bupd p R P Q : Frame p R P Q → Frame p R (|==> P) (|==> Q).
-Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
-End class_instances.
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index bcae3c9be..ec136a553 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import proofmode lib.invariants.
+From iris.base_logic Require Import base_logic lib.invariants.
 
 Section base_logic_tests.
   Context {M : ucmraT}.
-- 
GitLab