From e0d0f8dd8d543f40a710f5cb4c531d046c1035a9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Feb 2016 23:33:52 +0100
Subject: [PATCH] Restraint instance search for global functors.

Also, give all these global functors the suffix GF to avoid shadowing
such as we had with authF.

And add some type annotations for clarity.
---
 barrier/barrier.v               |  2 +-
 barrier/client.v                |  2 +-
 heap_lang/heap.v                |  8 +++---
 heap_lang/tests.v               |  2 +-
 program_logic/auth.v            | 10 +++-----
 program_logic/ghost_ownership.v | 43 ++++++++++++++++++---------------
 program_logic/saved_prop.v      | 10 +++-----
 program_logic/sts.v             |  9 +++----
 8 files changed, 43 insertions(+), 43 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 0dbf4b8f1..97efedbb5 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -125,7 +125,7 @@ End barrier_proto.
 Import barrier_proto.
 
 (* The functors we need. *)
-Definition barrierFs := stsF sts `::` agreeF `::` pnil.
+Definition barrierGFs := stsGF sts `::` agreeF `::` pnil.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/barrier/client.v b/barrier/client.v
index 29bd737be..47bf44ebd 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -26,7 +26,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := heapF .:: barrierFs .++ endF.
+  Definition Σ : iFunctorG := heapGF .:: barrierGFs .++ endGF.
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2a32e5ffc..7e517f24b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -7,8 +7,8 @@ Import uPred.
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
    predicates over finmaps instead of just ownP. *)
 
-Definition heapRA := mapRA loc (exclRA (leibnizC val)).
-Definition heapF := authF heapRA.
+Definition heapRA : cmraT := mapRA loc (exclRA (leibnizC val)).
+Definition heapGF : iFunctor := authGF heapRA.
 
 Class heapG Σ := HeapG {
   heap_inG : inG heap_lang Σ (authRA heapRA);
@@ -21,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl.
 Definition of_heap : heapRA → state := omap (maybe Excl).
 
 Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
-  auth_own heap_name ({[ l := Excl v ]} : heapRA).
+  auth_own heap_name {[ l := Excl v ]}.
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).
 Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
@@ -104,7 +104,7 @@ Section heap.
     P ⊑ || Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
-    trans (|={E}=> auth_own heap_name (∅ : heapRA) ★ P)%I.
+    trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
     { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 0f8467db5..71a7f35af 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -76,7 +76,7 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := heapF .:: endF.
+  Definition Σ : iFunctorG := heapGF .:: endGF.
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 2e7f75d70..d056d51cc 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -9,12 +9,10 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_timeless (a : A) :> Timeless a;
 }.
 
-(* TODO: This shadows algebra.auth.authF. *)
-Definition authF (A : cmraT) := constF (authRA A).
-
-Instance authG_inGF (A : cmraT) `{CMRAIdentity A} `{∀ a : A, Timeless a}
-         `{inGF Λ Σ (authF A)} : authG Λ Σ A.
-Proof. split; try apply _. move:(@inGF_inG Λ Σ (authF A)). auto. Qed.
+Definition authGF (A : cmraT) : iFunctor := constF (authRA A).
+Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
+  `{CMRAIdentity A, ∀ a : A, Timeless a} : authG Λ Σ A.
+Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Section definitions.
   Context `{authG Λ Σ A} (γ : gname).
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index b42995bf0..d66734f70 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -28,6 +28,30 @@ Typeclasses Opaque to_globalF own.
 Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
 Notation iFunctorG := (gid → iFunctor).
 
+(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
+   the functor breaks badly because Coq is unable to infer the correct
+   typeclasses, it does not unfold the functor. *)
+Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
+  inGF_id : gid;
+  inGF_prf : F = Σ inGF_id;
+}.
+(* Avoid eager type class search: this line ensures that type class search
+is only triggered if the first two arguments of inGF do not contain evars. Since
+instance search for [inGF] is restrained, instances should always have [inGF] as
+their first argument to avoid loops. For example, the instances [authGF_inGF]
+and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
+Hint Mode inGF + + - : typeclass_instances.
+
+Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
+Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
+Instance inGF_here {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
+Proof. by exists 0. Qed.
+Instance inGF_further {Λ Σ} (F F': iFunctor) : inGF Λ Σ F → inGF Λ (F' .:: Σ) F.
+Proof. intros [i ?]. by exists (S i). Qed.
+
+Definition endGF : iFunctorG := const (constF unitRA).
+
+(** Properties about ghost ownership *)
 Section global.
 Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
@@ -145,22 +169,3 @@ Proof.
   apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
 Qed.
 End global.
-
-(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
-   the functor breaks badly because Coq is unable to infer the correct
-   typeclasses, it does not unfold the functor. *)
-Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
-  inGF_id : gid;
-  inGF_prf : F = Σ inGF_id;
-}.
-
-Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
-Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.
-
-Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
-Proof. exists 0. done. Qed.
-
-Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
-Proof. exists (S inGF_id). apply inGF_prf. Qed.
-
-Definition endF : gid → iFunctor := const (constF unitRA).
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 6ab24d612..1d17c0906 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -6,7 +6,7 @@ Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
 Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
-Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed.
+Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
@@ -18,11 +18,9 @@ Section saved_prop.
   Implicit Types P Q : iPropG Λ Σ.
   Implicit Types γ : gname.
 
-  Global Instance : ∀ P, AlwaysStable (saved_prop_own γ P).
-  Proof.
-    intros. rewrite /AlwaysStable /saved_prop_own.
-    rewrite always_own; done.
-  Qed.
+  Global Instance saved_prop_always_stable γ P :
+    AlwaysStable (saved_prop_own γ P).
+  Proof. by rewrite /AlwaysStable /saved_prop_own always_own. Qed.
 
   Lemma saved_prop_alloc_strong N P (G : gset gname) :
     True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ P).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index b53c7dcb2..e118a20b1 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -8,11 +8,10 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 }.
 Coercion sts_inG : stsG >-> inG.
 
-Definition stsF (sts : stsT) := constF (stsRA sts).
-
-Instance stsG_inGF sts `{Inhabited (sts.state sts)}
-         `{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts.
-Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed.
+Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
+Instance stsGF_inGF sts `{inGF Λ Σ (stsGF sts)}
+  `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
+Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Section definitions.
   Context `{i : stsG Λ Σ sts} (γ : gname).
-- 
GitLab