barrier: strive for consistency between barrierGF and the inGF assumptions;...

barrier: strive for consistency between barrierGF and the inGF assumptions; also change some instance names

barrier/barrier.v

@@ -125,14 +125,14 @@ End barrier_proto.
 Import barrier_proto.
 
 (* The functors we need. *)
-Definition barrierGFs : iFunctors := [stsGF sts; agreeF].
+Definition barrierGF : iFunctors := [stsGF sts; agreeF].
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
   Context {Σ : iFunctorG} (N : namespace).
   Context `{heapG Σ} (heapN : namespace).
-  Context `{stsG heap_lang Σ sts}.
-  Context `{savedPropG heap_lang Σ}.
+  (* These are exactly the elements of barrierGF *)
+  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
 
   Local Hint Immediate i_states_closed low_states_closed : sts.
   Local Hint Resolve signal_step wait_step split_step : sts.

barrier/client.v

@@ -26,7 +26,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := #[ heapGF ; barrierGFs ].
+  Definition Σ : iFunctorG := #[ heapGF ; barrierGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.

program_logic/saved_prop.v

@@ -5,7 +5,7 @@ Import uPred.
 Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
-Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
+Instance inGF_savedPropG `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
 Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ}

program_logic/sts.v

@@ -9,7 +9,7 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 Coercion sts_inG : stsG >-> inG.
 
 Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
-Instance stsGF_inGF sts `{inGF Λ Σ (stsGF sts)}
+Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
 Proof. split; try apply _. apply: inGF_inG. Qed.