From df837b9d3d4e5fe4a7466f2886463cd7380b65f3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Oct 2017 20:46:11 +0200
Subject: [PATCH] Proof mode instances for the plain modality.

---
 theories/proofmode/class_instances.v | 42 ++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index a55899d06..beb49c8a0 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -19,6 +19,9 @@ Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 
+Global Instance from_assumption_plainly_l p P Q :
+  FromAssumption p P Q → FromAssumption p (☃ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite plainly_elim. Qed.
 Global Instance from_assumption_always_l p P Q :
   FromAssumption p P Q → FromAssumption p (□ P) Q.
 Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
@@ -48,6 +51,8 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
+Global Instance into_pure_plainly P φ : IntoPure P φ → IntoPure (☃ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite plainly_pure. Qed.
 Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
 
@@ -97,6 +102,8 @@ Proof.
   rewrite -cmra_valid_intro //. auto with I.
 Qed.
 
+Global Instance from_pure_plainly P φ : FromPure P φ → FromPure (☃ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
 Global Instance from_pure_always P φ : FromPure P φ → FromPure (□ P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite always_pure. Qed.
 Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
@@ -258,6 +265,9 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
   FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
 Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
+Global Instance from_later_plainly n P Q :
+  FromLaterN n P Q → FromLaterN n (☃ P) (☃ Q).
+Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
 Global Instance from_later_always n P Q :
   FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
 Proof. by rewrite /FromLaterN -always_laterN=> ->. Qed.
@@ -310,6 +320,9 @@ Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
 Global Instance into_wand_forall {A} p (Φ : A → uPred M) P Q x :
   IntoWand p (Φ x) P Q → IntoWand p (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
+Global Instance into_wand_plainly p R P Q :
+  IntoWand p R P Q → IntoWand p (☃ R) P Q.
+Proof. rewrite /IntoWand=> ->. by rewrite plainly_elim. Qed.
 Global Instance into_wand_always p R P Q :
   IntoWand p R P Q → IntoWand p (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
@@ -347,6 +360,12 @@ Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
 
 Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
+Global Instance from_and_plainly p P Q1 Q2 :
+  FromAnd false P Q1 Q2 → FromAnd p (☃ P) (☃ Q1) (☃ Q2).
+Proof.
+  intros. apply mk_from_and_and.
+  by rewrite plainly_and_sep_l' -plainly_sep -(from_and _ P).
+Qed.
 Global Instance from_and_always p P Q1 Q2 :
   FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
@@ -438,6 +457,11 @@ Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. apply mk_into_and_sep. by rewrite pure_and always_and_sep_r. Qed.
+Global Instance into_and_plainly p P Q1 Q2 :
+  IntoAnd true P Q1 Q2 → IntoAnd p (☃ P) (☃ Q1) (☃ Q2).
+Proof.
+  rewrite /IntoAnd=>->. destruct p; by rewrite ?plainly_and always_and_sep_r.
+Qed.
 Global Instance into_and_always p P Q1 Q2 :
   IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
 Proof.
@@ -623,6 +647,9 @@ Global Instance from_or_bupd P Q1 Q2 :
 Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
 Global Instance from_or_pure φ ψ : @FromOr M ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /FromOr pure_or. Qed.
+Global Instance from_or_plainly P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (☃ P) (☃ Q1) (☃ Q2).
+Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
 Global Instance from_or_always P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
@@ -641,6 +668,9 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
 Proof. done. Qed.
 Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoOr pure_or. Qed.
+Global Instance into_or_plainly P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (☃ P) (☃ Q1) (☃ Q2).
+Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
 Global Instance into_or_always P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
@@ -665,6 +695,9 @@ Qed.
 Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
+Global Instance from_exist_plainly {A} P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (☃ P) (λ a, ☃ (Φ a))%I.
+Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
 Global Instance from_exist_always {A} P (Φ : A → uPred M) :
   FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite always_exist. Qed.
@@ -688,6 +721,9 @@ Proof. done. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
+Global Instance into_exist_plainly {A} P (Φ : A → uPred M) :
+  IntoExist P Φ → IntoExist (☃ P) (λ a, ☃ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_exist_always {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
@@ -704,6 +740,9 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → uPred M) : IntoForall (∀ a, Φ a) Φ.
 Proof. done. Qed.
+Global Instance into_forall_plainly {A} P (Φ : A → uPred M) :
+  IntoForall P Φ → IntoForall (☃ P) (λ a, ☃ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance into_forall_always {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
@@ -729,6 +768,9 @@ Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
 
+Global Instance elim_modal_plainly P Q : ElimModal (☃ P) P Q Q.
+Proof. intros. by rewrite /ElimModal plainly_elim wand_elim_r. Qed.
+
 Global Instance elim_modal_always P Q : ElimModal (â–¡ P) P Q Q.
 Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.
 
-- 
GitLab