From 0d2b923c1f76f57b24f3d48b9563146f2ac4873b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Oct 2020 14:27:53 +0200
Subject: [PATCH] move remaining validI lemmas also to algebra.v

---
 theories/base_logic/algebra.v | 17 +++++++++++++----
 theories/base_logic/bi.v      |  7 -------
 theories/base_logic/upred.v   |  9 ---------
 3 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 9e2758efd..21d496480 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -8,6 +8,15 @@ From iris Require Import options.
 Section upred.
 Context {M : ucmraT}.
 
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢@{uPredI M} ✓ x.1 ∧ ✓ x.2.
+Proof. by uPred.unseal. Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  ✓ mx ⊣⊢@{uPredI M} match mx with Some x => ✓ x | None => True : uPred M end.
+Proof. uPred.unseal. by destruct mx. Qed.
+Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) :
+  ✓ g ⊣⊢@{uPredI M} ∀ i, ✓ g i.
+Proof. by uPred.unseal. Qed.
+
 Section gmap_ofe.
   Context `{Countable K} {A : ofeT}.
   Implicit Types m : gmap K A.
@@ -26,10 +35,10 @@ Section gmap_cmra.
   Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢@{uPredI M} ✓ x.
   Proof.
     rewrite gmap_validI. apply: anti_symm.
-    - rewrite (bi.forall_elim i) lookup_singleton uPred.option_validI. done.
+    - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
     - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-      + rewrite lookup_singleton uPred.option_validI. done.
-      + rewrite lookup_singleton_ne // uPred.option_validI.
+      + rewrite lookup_singleton option_validI. done.
+      + rewrite lookup_singleton_ne // option_validI.
         apply bi.True_intro.
   Qed.
 End gmap_cmra.
@@ -241,7 +250,7 @@ Section gmap_view.
       ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
     rewrite /gmap_view_frag -view_frag_op view_frag_validI.
-    rewrite singleton_op singleton_validI -pair_op uPred.prod_validI /=.
+    rewrite singleton_op singleton_validI -pair_op prod_validI /=.
     apply bi.and_mono; first done.
     rewrite agree_validI agree_equivI. done.
   Qed.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 8f86b9c02..fa2327ae6 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -215,15 +215,8 @@ Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
 Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. exact: uPred_primitive.prod_validI. Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. exact: uPred_primitive.option_validI. Qed.
 Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. exact: uPred_primitive.discrete_valid. Qed.
-Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
 
 (** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 2c628c6c4..b3e6fb96c 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -863,18 +863,9 @@ Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
 
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. by unseal. Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. unseal. by destruct mx. Qed.
-
 Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 
-Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. by unseal. Qed.
-
 (** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
-- 
GitLab