From 6bbcc096ead9b31f5ed54e6fef7cdfaf7475fbc5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Jul 2021 10:06:05 +0200
Subject: [PATCH] Improve coding style.

---
 iris/bi/embedding.v | 129 ++++++++++++++++++--------------------------
 1 file changed, 51 insertions(+), 78 deletions(-)

diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index eefa04b6e..8a7e39e58 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -311,95 +311,68 @@ Section embed.
   End plainly.
 End embed.
 
-(** Transitive embedding: this constructs an embedding of [PROP1] into [PROP3]
-  by combining the embeddings of [PROP1] into [PROP2] and [PROP2] into [PROP3].
-  Note that declaring these instances globally can make TC search ambiguous or
-  diverging. These are only defined so that a user can conveniently use them to
-  manually combine embeddings. *)
-Section transitive_embedding.
-  Context `{BE1: BiEmbed PROP1 PROP2} `{BE2: BiEmbed PROP2 PROP3}.
-
-  Local Instance embed_embed : Embed PROP1 PROP3 :=
-    λ P, embed (embed P).
-
-  Local Ltac unfold_embed := rewrite /embed /bi_embed_embed /= /embed_embed /=.
+(* Not defined using an ordinary [Instance] because the default
+[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
+search for the other premises fail. See the proof of [monPred_objectively_plain]
+for an example where it would fail with a regular [Instance].*)
+Global Hint Extern 4 (Plain _) =>
+  notypeclasses refine (embed_plain _ _) : typeclass_instances.
 
-  Local Instance embed_embed_mono :
-    Proper ((⊢) ==> (⊢)) (@embed PROP1 PROP3 _).
-  Proof. intros ?? PQ. unfold_embed. by rewrite PQ. Qed.
+(** Transitive embedding: this constructs an embedding of [PROP1] into [PROP3]
+by combining the embeddings of [PROP1] into [PROP2] and [PROP2] into [PROP3].
+Note that declaring these instances globally can make TC search ambiguous or
+diverging. These are only defined so that a user can conveniently use them to
+manually combine embeddings. *)
+Section embed_embed.
+  Context `{BiEmbed PROP1 PROP2, BiEmbed PROP2 PROP3}.
 
-  Local Instance embed_embed_ne : NonExpansive (@embed PROP1 PROP3 _).
-  Proof. unfold_embed. solve_proper. Qed.
+  Local Instance embed_embed : Embed PROP1 PROP3 := λ P, ⎡ ⎡ P ⎤ ⎤%I.
 
-  Definition embed_embedding_mixin :
-    BiEmbedMixin PROP1 PROP3 embed_embed.
+  Lemma embed_embedding_mixin : BiEmbedMixin PROP1 PROP3 embed_embed.
   Proof.
-    split; try apply _; unfold_embed.
-    - intros P. rewrite embed_emp_valid. by apply BE1.
-    - intros PROP' IN P Q. rewrite embed_interal_inj; by apply BE1.
-    - rewrite -bi_embed_mixin_emp_2; [|apply BE1]. apply BE2.
-    - intros P Q. rewrite -embed_impl. apply embed_mono, BE1.
-    - intros A Φ. rewrite -embed_forall. apply embed_mono, BE1.
-    - intros A Φ. rewrite -embed_exist. apply embed_mono, BE1.
-    - intros P Q. rewrite -embed_sep. apply embed_proper, BE1.
-    - intros P Q. rewrite -embed_wand. apply embed_mono, BE1.
-    - intros P. rewrite -embed_persistently. apply embed_proper, BE1.
+    split; unfold embed, embed_embed.
+    - solve_proper.
+    - solve_proper.
+    - intros P. by rewrite !embed_emp_valid.
+    - intros PROP' ? P Q. by rewrite !embed_interal_inj.
+    - by rewrite -!embed_emp_2.
+    - intros P Q. by rewrite -!embed_impl.
+    - intros A Φ. by rewrite -!embed_forall.
+    - intros A Φ. by rewrite -!embed_exist.
+    - intros P Q. by rewrite -!embed_sep.
+    - intros P Q. by rewrite -!embed_wand.
+    - intros P. by rewrite -!embed_persistently.
   Qed.
-
   Local Instance embed_bi_embed : BiEmbed PROP1 PROP3 :=
     {| bi_embed_mixin := embed_embedding_mixin |}.
 
-  Definition embed_embed_emp
-    `{@BiEmbedEmp _ _ BE1} `{@BiEmbedEmp _ _ BE2} :
+  Lemma embed_embed_alt (P : PROP1) : ⎡ P ⎤ ⊣⊢@{PROP3} ⎡ ⎡ P ⎤ ⎤.
+  Proof. done. Qed.
+
+  Lemma embed_embed_emp :
+    BiEmbedEmp PROP1 PROP2 → BiEmbedEmp PROP2 PROP3 →
     BiEmbedEmp PROP1 PROP3.
-  Proof.
-    rewrite /BiEmbedEmp. unfold_embed.
-    rewrite -embed_emp. apply embed_mono. by apply embed_emp_1.
-  Qed.
-  Definition embed_embed_later
-    `{@BiEmbedLater _ _ BE1} `{@BiEmbedLater _ _ BE2} :
+  Proof. rewrite /BiEmbedEmp !embed_embed_alt. by intros -> ->. Qed.
+  Lemma embed_embed_later :
+    BiEmbedLater PROP1 PROP2 → BiEmbedLater PROP2 PROP3 →
     BiEmbedLater PROP1 PROP3.
-  Proof.
-    rewrite /BiEmbedLater => P. unfold_embed.
-    rewrite -embed_later. apply embed_proper. by apply embed_later.
-  Qed.
-  Definition embed_embed_internal_eq
-    `{BiInternalEq PROP1} `{BiInternalEq PROP2} `{BiInternalEq PROP3}
-    `{@BiEmbedInternalEq _ _ BE1 _ _} `{@BiEmbedInternalEq _ _ BE2 _ _} :
+  Proof. intros ?? P. by rewrite !embed_embed_alt !embed_later. Qed.
+  Lemma embed_embed_internal_eq
+      `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiInternalEq PROP3} :
+    BiEmbedInternalEq PROP1 PROP2 → BiEmbedInternalEq PROP2 PROP3 →
     BiEmbedInternalEq PROP1 PROP3.
-  Proof.
-    rewrite /BiEmbedInternalEq => ???. unfold_embed.
-    rewrite -embed_internal_eq. apply embed_mono. by apply embed_internal_eq_1.
-  Qed.
-  Definition embed_embed_bupd
-    `{BiBUpd PROP1} `{BiBUpd PROP2} `{BiBUpd PROP3}
-    `{@BiEmbedBUpd _ _ BE1 _ _} `{@BiEmbedBUpd _ _ BE2 _ _} :
+  Proof. intros ?? A x y. by rewrite !embed_embed_alt !embed_internal_eq. Qed.
+  Lemma embed_embed_bupd `{!BiBUpd PROP1, !BiBUpd PROP2, !BiBUpd PROP3} :
+    BiEmbedBUpd PROP1 PROP2 → BiEmbedBUpd PROP2 PROP3 →
     BiEmbedBUpd PROP1 PROP3.
-  Proof.
-    rewrite /BiEmbedBUpd => P. unfold_embed.
-    rewrite -embed_bupd. apply embed_proper. by apply embed_bupd.
-  Qed.
-  Definition embed_embed_fupd
-    `{BiFUpd PROP1} `{BiFUpd PROP2} `{BiFUpd PROP3}
-    `{@BiEmbedFUpd _ _ BE1 _ _} `{@BiEmbedFUpd _ _ BE2 _ _} :
+  Proof. intros ?? P. by rewrite !embed_embed_alt !embed_bupd. Qed.
+  Lemma embed_embed_fupd `{!BiFUpd PROP1, !BiFUpd PROP2, !BiFUpd PROP3} :
+    BiEmbedFUpd PROP1 PROP2 → BiEmbedFUpd PROP2 PROP3 →
     BiEmbedFUpd PROP1 PROP3.
-  Proof.
-    rewrite /BiEmbedFUpd => ?? P. unfold_embed.
-    rewrite -embed_fupd. apply embed_proper. by apply embed_fupd.
-  Qed.
-  Definition embed_embed_plainly
-    `{BiPlainly PROP1} `{BiPlainly PROP2} `{BiPlainly PROP3}
-    `{@BiEmbedPlainly _ _ BE1 _ _} `{@BiEmbedPlainly _ _ BE2 _ _} :
+  Proof. intros ?? E1 E2 P. by rewrite !embed_embed_alt !embed_fupd. Qed.
+  Lemma embed_embed_plainly
+      `{!BiPlainly PROP1, !BiPlainly PROP2, !BiPlainly PROP3} :
+    BiEmbedPlainly PROP1 PROP2 → BiEmbedPlainly PROP2 PROP3 →
     BiEmbedPlainly PROP1 PROP3.
-  Proof.
-    rewrite /BiEmbedPlainly => P. unfold_embed.
-    rewrite -embed_plainly. apply embed_proper. by apply embed_plainly.
-  Qed.
-End transitive_embedding.
-
-(* Not defined using an ordinary [Instance] because the default
-[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
-search for the other premises fail. See the proof of [monPred_objectively_plain]
-for an example where it would fail with a regular [Instance].*)
-Global Hint Extern 4 (Plain _) =>
-  notypeclasses refine (embed_plain _ _) : typeclass_instances.
+  Proof. intros ?? P. by rewrite !embed_embed_alt !embed_plainly. Qed.
+End embed_embed.
-- 
GitLab