From db2d9d6bd8a4e79796047340eb915d1c5eaaf2ea Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 6 Dec 2017 17:51:30 +0100
Subject: [PATCH] Try on BI morphisms.

---
 theories/bi/derived_laws.v | 96 ++++++++++++++++++++++++++++++++++++++
 theories/bi/interface.v    | 19 ++++++++
 theories/bi/monpred.v      | 42 +++++++----------
 3 files changed, 131 insertions(+), 26 deletions(-)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index f8249ff54..996e434bf 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -2296,3 +2296,99 @@ To avoid that, we declare it using a [Hint Immediate], so that it will
 only be used at the leaves of the proof search tree, i.e. when the
 premise of the hint can be derived from just the current context. *)
 Hint Immediate bi.plain_persistent : typeclass_instances.
+
+(* BI morphisms *)
+Section bi_morphims.
+  Context `{@BiMorphism PROP1 PROP2 mor}.
+
+  Global Instance bi_mor_proper : Proper ((≡) ==> (≡)) mor.
+  Proof. apply (ne_proper _). Qed.
+  Global Instance bi_mor_mono_flip : Proper (flip (⊢) ==> flip (⊢)) mor.
+  Proof. solve_proper. Qed.
+
+  Lemma bi_mor_forall A Φ : mor (@bi_forall _ A Φ) ⊣⊢ (∀ x, mor (Φ x)).
+  Proof.
+    apply bi.equiv_spec; split; [|apply bi_mor_forall_2].
+    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
+  Qed.
+  Lemma bi_mor_exist A Φ : mor (@bi_exist _ A Φ) ⊣⊢ (∃ x, mor (Φ x)).
+  Proof.
+    apply bi.equiv_spec; split; [apply bi_mor_exist_1|].
+    apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
+  Qed.
+  Lemma bi_mor_and P Q : mor (P ∧ Q) ⊣⊢ mor P ∧ mor Q.
+  Proof. rewrite !bi.and_alt bi_mor_forall. by f_equiv=>-[]. Qed.
+  Lemma bi_mor_or P Q : mor (P ∨ Q) ⊣⊢ mor P ∨ mor Q.
+  Proof. rewrite !bi.or_alt bi_mor_exist. by f_equiv=>-[]. Qed.
+  Lemma bi_mor_impl P Q : mor (P → Q) ⊣⊢ (mor P → mor Q).
+  Proof.
+    apply bi.equiv_spec; split; [|apply bi_mor_impl_2].
+    apply bi.impl_intro_l. by rewrite -bi_mor_and bi.impl_elim_r.
+  Qed.
+  Lemma bi_mor_wand P Q : mor (P -∗ Q) ⊣⊢ (mor P -∗ mor Q).
+  Proof.
+    apply bi.equiv_spec; split; [|apply bi_mor_wand_2].
+    apply bi.wand_intro_l. by rewrite -bi_mor_sep bi.wand_elim_r.
+  Qed.
+  Lemma bi_mor_pure φ : mor ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+  Proof.
+    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_mor_exist.
+    do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
+    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?bi_mor_impl;
+      last apply bi.True_intro.
+    apply bi.impl_intro_l. by rewrite right_id.
+  Qed.
+  Lemma bi_mor_internal_eq (A : ofeT) (x y : A) : mor (x ≡ y) ⊣⊢ (x ≡ y).
+  Proof.
+    apply bi.equiv_spec; split; [apply bi_mor_internal_eq_1|].
+    rewrite (bi.internal_eq_rewrite x y (λ y, mor (x ≡ y)%I) _); [|solve_proper].
+    rewrite -(bi.internal_eq_refl True%I) bi_mor_pure.
+    eapply bi.impl_elim; [done|]. apply bi.True_intro.
+  Qed.
+  Lemma bi_mor_iff P Q : mor (P ↔ Q) ⊣⊢ (mor P ↔ mor Q).
+  Proof. by rewrite bi_mor_and !bi_mor_impl. Qed.
+  Lemma bi_mor_wand_iff P Q : mor (P ∗-∗ Q) ⊣⊢ (mor P ∗-∗ mor Q).
+  Proof. by rewrite bi_mor_and !bi_mor_wand. Qed.
+  Lemma bi_mor_affinely P : mor (bi_affinely P) ⊣⊢ bi_affinely (mor P).
+  Proof. by rewrite bi_mor_and bi_mor_emp. Qed.
+  Lemma bi_mor_absorbingly P : mor (bi_absorbingly P) ⊣⊢ bi_absorbingly (mor P).
+  Proof. by rewrite bi_mor_sep bi_mor_pure. Qed.
+  Lemma bi_mor_plainly_if P b :
+    mor (bi_plainly_if b P) ⊣⊢ bi_plainly_if b (mor P).
+  Proof. destruct b; auto using bi_mor_plainly. Qed.
+  Lemma bi_mor_persistently_if P b :
+    mor (bi_persistently_if b P) ⊣⊢ bi_persistently_if b (mor P).
+  Proof. destruct b; auto using bi_mor_persistently. Qed.
+  Lemma bi_mor_affinely_if P b :
+    mor (bi_affinely_if b P) ⊣⊢ bi_affinely_if b (mor P).
+  Proof. destruct b; simpl; auto using bi_mor_affinely. Qed.
+  Lemma bi_mor_hforall {As} (Φ : himpl As PROP1):
+    mor (bi_hforall Φ) ⊣⊢ bi_hforall (hcompose mor Φ).
+  Proof. induction As=>//. rewrite /= bi_mor_forall. by do 2 f_equiv. Qed.
+  Lemma bi_mor_hexist {As} (Φ : himpl As PROP1):
+    mor (bi_hexist Φ) ⊣⊢ bi_hexist (hcompose mor Φ).
+  Proof. induction As=>//. rewrite /= bi_mor_exist. by do 2 f_equiv. Qed.
+
+  Global Instance bi_mor_plain P : Plain P → Plain (mor P).
+  Proof. intros ?. by rewrite /Plain -bi_mor_plainly -plain. Qed.
+  Global Instance bi_mor_persistent P : Persistent P → Persistent (mor P).
+  Proof. intros ?. by rewrite /Persistent -bi_mor_persistently -persistent. Qed.
+  Global Instance bi_mor_affine P : Affine P → Affine (mor P).
+  Proof. intros ?. by rewrite /Affine (affine P) bi_mor_emp. Qed.
+  Global Instance bi_mor_absorbing P : Absorbing P → Absorbing (mor P).
+  Proof. intros ?. by rewrite /Absorbing -bi_mor_absorbingly absorbing. Qed.
+End bi_morphims.
+
+Section sbi_morphims.
+  Context `{@SbiMorphism PROP1 PROP2 mor}.
+
+  Lemma sbi_mor_laterN n P : mor (▷^n P) ⊣⊢ ▷^n (mor P).
+  Proof. induction n=>//=. rewrite sbi_mor_later. by f_equiv. Qed.
+  Lemma sbi_mor_except_0 P : mor (◇ P) ⊣⊢ ◇ (mor P).
+  Proof. by rewrite bi_mor_or sbi_mor_later bi_mor_pure. Qed.
+
+  Global Instance sbi_mor_timeless P : Timeless P → Timeless (mor P).
+  Proof.
+    intros ?. by rewrite /Timeless -sbi_mor_except_0 -sbi_mor_later timeless.
+  Qed.
+End sbi_morphims.
\ No newline at end of file
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 0105c21eb..7a1d2376a 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -337,6 +337,25 @@ Notation "⎡ P ⎤" := (bi_embedding P) : bi_scope.
 Instance: Params (@bi_embedding) 3.
 Typeclasses Opaque bi_embedding.
 
+Class BiMorphism {PROP1 PROP2 : bi} (mor : PROP1 → PROP2) := {
+  bi_mor_ne :> NonExpansive mor;
+  bi_mor_mono :> Proper ((⊢) ==> (⊢)) mor;
+  bi_mor_emp : mor emp ⊣⊢ emp;
+  bi_mor_impl_2 P Q : (mor P → mor Q)%I ⊢ mor (P → Q)%I;
+  bi_mor_forall_2 A Φ : (∀ x, mor (Φ x)) ⊢ mor (@bi_forall _ A Φ);
+  bi_mor_exist_1 A Φ : mor (@bi_exist _ A Φ) ⊢ ∃ x, mor (Φ x);
+  bi_mor_internal_eq_1 (A : ofeT) (x y : A) : mor (x ≡ y) ⊢ (x ≡ y);
+  bi_mor_sep P Q : mor (P ∗ Q) ⊣⊢ (mor P ∗ mor Q);
+  bi_mor_wand_2 P Q : (mor P -∗ mor Q) ⊢ mor (P -∗ Q);
+  bi_mor_plainly P : mor (bi_plainly P) ⊣⊢ bi_plainly (mor P);
+  bi_mor_persistently P : mor (bi_persistently P) ⊣⊢ bi_persistently (mor P)
+}.
+
+Class SbiMorphism {PROP1 PROP2 : sbi} (mor : PROP1 → PROP2) := {
+  sbi_mor_bi_mor :> BiMorphism mor;
+  sbi_mor_later P : mor (▷ P) ⊣⊢ ▷ mor P
+}.
+
 Module bi.
 Section bi_laws.
 Context {PROP : bi}.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index b98c092bb..c1a63ebd0 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -372,19 +372,6 @@ Global Instance monPred_car_mono_flip :
   Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) (@monPred_car I PROP).
 Proof. solve_proper. Qed.
 
-Global Instance monPred_ipure_ne :
-  NonExpansive (@bi_embedding PROP (monPred I PROP) _).
-Proof. unseal. by split. Qed.
-Global Instance monPred_ipure_proper :
-  Proper ((≡) ==> (≡)) (@bi_embedding PROP (monPred I PROP) _).
-Proof. apply (ne_proper _). Qed.
-Global Instance monPred_ipure_mono :
-  Proper ((⊢) ==> (⊢)) (@bi_embedding PROP (monPred I PROP) _).
-Proof. unseal. by split. Qed.
-Global Instance monPred_ipure_mono_flip :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_embedding PROP (monPred I PROP) _).
-Proof. solve_proper. Qed.
-
 Global Instance monPred_in_proper (R : relation I) :
   Proper (R ==> R ==> iff) (⊑) → Reflexive R →
   Proper (R ==> (≡)) (@monPred_in I PROP).
@@ -443,19 +430,6 @@ Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
 Global Instance monPred_car_affine P i : Affine P → Affine (P i).
 Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
 
-Global Instance monPred_ipure_plain (P : PROP) :
-  Plain P → @Plain (monPredI I PROP) ⎡P⎤%I.
-Proof. split => ? /=. unseal. apply bi.forall_intro=>?. apply (plain _). Qed.
-Global Instance monPred_ipure_persistent (P : PROP) :
-  Persistent P → @Persistent (monPredI I PROP) ⎡P⎤%I.
-Proof. split => ? /=. unseal. exact: H. Qed.
-Global Instance monPred_ipure_absorbing (P : PROP) :
-  Absorbing P → @Absorbing (monPredI I PROP) ⎡P⎤%I.
-Proof. unfold Absorbing. split => ? /=. by unseal. Qed.
-Global Instance monPred_ipure_affine (P : PROP) :
-  Affine P → @Affine (monPredI I PROP) ⎡P⎤%I.
-Proof. unfold Affine. split => ? /=. by unseal. Qed.
-
 (* Note that monPred_in is *not* Plain, because it does depend on the
    index. *)
 Global Instance monPred_in_persistent V :
@@ -489,6 +463,18 @@ Proof.
   move=> []. unfold Affine. unseal=>Hp. split => ?.
   by apply affine, bi.forall_affine.
 Qed.
+
+Global Instance monPred_ipure_bi_mor :
+  @BiMorphism PROP (monPredI I PROP) bi_embedding.
+Proof.
+  split; try apply _; unseal; try done.
+  - split=>? /=.
+    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+  - split=>? /=.
+    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+  - intros ?. split => ? /=. apply bi.equiv_spec; split.
+    by apply bi.forall_intro. by rewrite bi.forall_elim.
+Qed.
 End bi_facts.
 
 Section sbi_facts.
@@ -509,4 +495,8 @@ Proof.
   move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
   by apply timeless, bi.forall_timeless.
 Qed.
+
+Global Instance monPred_ipure_sbi_mor :
+  @SbiMorphism PROP (monPredSI I PROP) bi_embedding.
+Proof. split; try apply _. by unseal. Qed.
 End sbi_facts.
-- 
GitLab