A bit of cleanup

theories/typing/contextual_refinement.v

@@ -239,7 +239,7 @@ Inductive typed_ctx: ctx → stringmap type → type → stringmap type → type
      typed_ctx (k :: K) Γ1 τ1 Γ3 τ3.
 
 (* Observable types are, at the moment, exactly the types which support equality. *)
-Definition ObsType : type → Prop := EqType.
+Definition ObsType : type → Prop := λ τ, EqType τ ∧ UnboxedType τ.
 
 Definition ctx_refines (Γ : stringmap type)
     (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ v τ',
@@ -311,20 +311,6 @@ Definition ctx_refines_alt (Γ : stringmap type)
   rtc erased_step ([fill_ctx K e], σ₀) (of_val v1 :: thp, σ₁) →
   ∃ thp' σ₁' v2, rtc erased_step ([fill_ctx K e'], σ₀) (of_val v2 :: thp', σ₁').
 
-(* Lemma erased_step_ectx (e e' : expr) tp' σ σ' K : *)
-(*   erased_step ([e], σ) (e' :: tp', σ') → *)
-(*   erased_step ([fill K e], σ) (fill K e' :: tp', σ'). *)
-(* Proof. *)
-(*   intros [κ Hst]. inversion Hst; simplify_eq/=. *)
-(*   symmetry in H. apply app_singleton in H. *)
-(*   assert (t1 = [] ∧ e1 = e ∧ t2 = []) as (->&->&->). *)
-(*   { naive_solver. } *)
-(*   assert (e2 = e' ∧ tp' = efs) as [-> ->]. *)
-(*   { naive_solver. } *)
-(*   eapply fill_prim_step in H1. simpl in H1. *)
-(*   econstructor. eapply step_atomic with (t1 := []); eauto. *)
-(* Qed. *)
-
 (* Helper lemmas *)
 Lemma erased_step_ectx (e e' : expr) tp tp' σ σ' K :
   erased_step (e :: tp, σ) (e' :: tp', σ') →
@@ -340,14 +326,6 @@ Proof.
   + rewrite app_comm_cons. reflexivity.
 Qed.
 
-
-Local Definition ffill (K : list ectx_item) :
-  (list expr * state) → (list expr * state) :=
-  fun x => match x with
-           | (e :: tp, σ) => (fill K e :: tp, σ)
-           | ([], σ) => ([], σ)
-           end.
-
 Lemma erased_step_nonempty  (tp : list expr) σ tp' σ'  :
   erased_step (tp, σ) (tp', σ') → tp' ≠ [].
 Proof.
@@ -366,6 +344,14 @@ Proof.
     intros ? ?%erased_step_nonempty. naive_solver.
 Qed.
 
+
+Local Definition ffill (K : list ectx_item) :
+  (list expr * state) → (list expr * state) :=
+  fun x => match x with
+           | (e :: tp, σ) => (fill K e :: tp, σ)
+           | ([], σ) => ([], σ)
+           end.
+
 Lemma rtc_erased_step_ectx (e e' : expr) tp tp' σ σ' K :
   rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
   rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
@@ -434,6 +420,7 @@ Proof.
   fold ρ1 ρ2. intros Hρ.
   change σ1 with ρ1.2. eapply nice_ctx_lemma; eauto.
 Qed.
+(*/Helper lemmas*)
 
 Lemma ctx_refines_impl_alt Γ e1 e2 τ :
   (Γ ⊨ e1 ≤ctx≤ e2 : τ) →

theories/typing/types.v

@@ -18,7 +18,7 @@ Inductive type :=
   | TExists : {bind 1 of type} → type
   | TRef : type → type.
 
-(** Which types support equality testing *)
+(** Types which support direct equality test (which coincides with ctx equiv) *)
 Inductive EqType : type → Prop :=
   | EqTUnit : EqType TUnit
   | EqTNat : EqType TNat