a bit of cleaning

theories/examples/delim_lang/hom.v

@@ -32,10 +32,7 @@ Section hom.
   Next Obligation.
     intros; simpl.
     simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - intros ???.
-      do 2 f_equiv.
-      intros ?; simpl.
-      solve_proper.
+    - solve_proper_please.
     - rewrite get_val_ITV.
       rewrite get_val_ITV.
       simpl.

theories/examples/delim_lang/interp.v

@@ -762,7 +762,7 @@ Section interp.
       trans (reify (gReifiers_sReifier rs)
                (APP_CONT_ (Next (interp_val v env))
                   fin kk)
-            (gState_recomp σr (sR_state (σ)))).
+            (gState_recomp σr (sR_state σ))).
       {
         repeat f_equiv. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl.
         rewrite !hom_vis. f_equiv. subst kk. rewrite ccompose_id_l. intro. simpl.

theories/examples/delim_lang/logrel.v

@@ -52,6 +52,15 @@ Section logrel.
   Solve All Obligations with solve_proper.
   Fail Next Obligation.
 
+  (** The configuration of the abstract machine (e, k, m) corresponds
+   to the "denotational configuration" tuple (t, κ, σ).
+
+   The meta-continuation is stored in the state and the top-level
+   current continuation is explicitly invoked.
+
+   At the top-level the refinement is explicitly about fully-evaluated
+   terms which compute to natural numbers. *)
+
   Definition obs_ref' {S : Set}
     (t : IT) (κ : HOM) (σ : stateF ♯ IT)
     (e : exprO S) (k : contO S) (m : mcontO S)
@@ -77,11 +86,8 @@ Section logrel.
                      -n> exprO S -n> contO S -n> mcontO S -n> iProp :=
     λne x y z a b c, obs_ref' x y z a b c.
   Solve All Obligations with try solve_proper.
-  Next Obligation.
-    intros.
-    intros ????????; simpl.
-    solve_proper.
-  Qed.
+  Next Obligation. solve_proper_please. Qed.
+
 
   Definition logrel_mcont' {S : Set}
     (P : ITV -n> valO S -n> iProp) (F : stateF ♯ IT) (m : mcontO S) :=
@@ -196,14 +202,7 @@ Section logrel.
                     -∗ ∀ F F', logrel_mcont δ F F'
                             -∗ obs_ref e E F e' E' F')%I.
   Solve All Obligations with try solve_proper.
-  Next Obligation.
-    intros; intros ????; simpl.
-    do 2 (f_equiv; intro; simpl).
-    f_equiv.
-    do 2 (f_equiv; intro; simpl).
-    f_equiv.
-    solve_proper.
-  Qed.
+  Next Obligation. solve_proper_please. Qed.
 
   Definition logrel {S : Set} (τ α β : ty) : IT -n> exprO S -n> iProp
     := logrel_expr (interp_ty τ) (interp_ty α) (interp_ty β).
@@ -219,7 +218,7 @@ Section logrel.
     (e' : exprO S)
     (τ α σ : ty) : iProp :=
     (□ ∀ γ (γ' : S [⇒] Empty_set), ssubst_valid Γ γ γ'
-          -∗ @logrel Empty_set τ α σ (e γ) (bind (F := expr) γ' e'))%I.
+          -∗ logrel τ α σ (e γ) (bind (F := expr) γ' e'))%I.
 
   Lemma compat_HOM_id {S : Set} P :
     ⊢ @logrel_ectx S P P HOM_id END.

theories/hom.v

@@ -4,12 +4,9 @@ Require Import Binding.Lib Binding.Set Binding.Env.
 Open Scope stdpp_scope.
 
 Section hom.
-  Context {sz : nat}.
-  Context {a : is_ctx_dep}.
   Context {A : ofe}.
   Context {CA : Cofe A}.
-  Context {rs : gReifiers a sz}.
-  Notation F := (gReifiers_ops rs).
+  Context {F : opsInterp}.
   Notation IT := (IT F A).
   Notation ITV := (ITV F A).