Merge branch 'ci/robbert/canonical_language' into 'master'

Use solely canonical structures for language hierarchy.

See merge request FP/iris-coq!90

CHANGELOG.md

@@ -76,6 +76,11 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Define the generic `fill` operation of the `ectxi_language` construct in terms
   of a left fold instead of a right fold. This gives rise to more definitional
   equalities.
+* The language hierarchy (`language`, `ectx_language`, `ectxi_language`) is now
+  fully formalized using canonical structures instead of using a mixture of
+  type classes and canonical structures. Also, it now uses explicit mixins. The
+  file `program_logic/ectxi_language` contains some documentation on how to
+  setup Iris for your language.
 * Improved big operators:
   + They are no longer tied to cameras, but work on any monoid
   + The version of big operations over lists was redefined so that it enjoys

theories/heap_lang/lang.v

@@ -374,7 +374,7 @@ Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
 Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
-Lemma val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
 Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
@@ -467,20 +467,18 @@ Lemma subst_rec_ne' f y e x es :
   (x ≠ f ∨ f = BAnon) → (x ≠ y ∨ y = BAnon) →
   subst' x es (Rec f y e) = Rec f y (subst' x es e).
 Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
+
+Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+Proof.
+  split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
+    fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+Qed.
 End heap_lang.
 
 (** Language *)
-Program Instance heap_ectxi_lang :
-  EctxiLanguage
-    (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
-  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
-|}.
-Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
-  heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
-  heap_lang.head_ctx_step_val.
-
-Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
+Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
+Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
+Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.

theories/heap_lang/lifting.v

@@ -61,16 +61,6 @@ Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
 Implicit Types σ : state.
 
-(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
-Proof. exact: wp_ectx_bind. Qed.
-
-Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
-     WP fill_item Ki e @ E {{ Φ }}.
-Proof. exact: weakestpre.wp_bind. Qed.
-
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e Φ :
   ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.

theories/heap_lang/proofmode.v

@@ -13,8 +13,7 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
-  rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
-  by rewrite -ectx_lifting.wp_ectx_bind_inv.
+  rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv.
 Qed.
 
 Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
@@ -55,7 +54,7 @@ Tactic Notation "wp_match" := wp_case; wp_let.
 Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
+Proof. rewrite /envs_entails=> ->. by apply: wp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with

theories/program_logic/ectx_language.v

@@ -4,9 +4,51 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
-   inference to use a keys. *)
-Class EctxLanguage (expr val ectx state : Type) := {
+(* TAKE CARE: When you define an [ectxLanguage] canonical structure for your
+language, you need to also define a corresponding [language] canonical
+structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
+file for doing that. *)
+
+Section ectx_language_mixin.
+  Context {expr val ectx state : Type}.
+  Context (of_val : val → expr).
+  Context (to_val : expr → option val).
+  Context (empty_ectx : ectx).
+  Context (comp_ectx : ectx → ectx → ectx).
+  Context (fill : ectx → expr → expr).
+  Context (head_step : expr → state → expr → state → list expr → Prop).
+
+  Record EctxLanguageMixin := {
+    mixin_to_of_val v : to_val (of_val v) = Some v;
+    mixin_of_to_val e v : to_val e = Some v → of_val v = e;
+    mixin_val_head_stuck e1 σ1 e2 σ2 efs :
+      head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
+
+    mixin_fill_empty e : fill empty_ectx e = e;
+    mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
+    mixin_fill_inj K : Inj (=) (=) (fill K);
+    mixin_fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e);
+
+    (* There are a whole lot of sensible axioms (like associativity, and left and
+    right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
+    positivity suffices. *)
+    mixin_ectx_positive K1 K2 :
+      comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
+
+    mixin_step_by_val K K' e1 e1' σ1 e2 σ2 efs :
+      fill K e1 = fill K' e1' →
+      to_val e1 = None →
+      head_step e1' σ1 e2 σ2 efs →
+      ∃ K'', K' = comp_ectx K K'';
+  }.
+End ectx_language_mixin.
+
+Structure ectxLanguage := EctxLanguage {
+  expr : Type;
+  val : Type;
+  ectx : Type;
+  state : Type;
+
   of_val : val → expr;
   to_val : expr → option val;
   empty_ectx : ectx;
@@ -14,61 +56,58 @@ Class EctxLanguage (expr val ectx state : Type) := {
   fill : ectx → expr → expr;
   head_step : expr → state → expr → state → list expr → Prop;
 
-  to_of_val v : to_val (of_val v) = Some v;
-  of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
-
-  fill_empty e : fill empty_ectx e = e;
-  fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
-  fill_inj K :> Inj (=) (=) (fill K);
-  fill_not_val K e : to_val e = None → to_val (fill K e) = None;
-
-  (* There are a whole lot of sensible axioms (like associativity, and left and
-  right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
-  positivity suffices. *)
-  ectx_positive K1 K2 :
-    comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
-
-  step_by_val K K' e1 e1' σ1 e2 σ2 efs :
-    fill K e1 = fill K' e1' →
-    to_val e1 = None →
-    head_step e1' σ1 e2 σ2 efs →
-    exists K'', K' = comp_ectx K K'';
+  ectx_language_mixin :
+    EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
 }.
 
-Arguments of_val {_ _ _ _ _} _%V.
-Arguments to_val {_ _ _ _ _} _%E.
-Arguments empty_ectx {_ _ _ _ _}.
-Arguments comp_ectx {_ _ _ _ _} _ _.
-Arguments fill {_ _ _ _ _} _ _%E.
-Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
-
-Arguments to_of_val {_ _ _ _ _} _.
-Arguments of_to_val {_ _ _ _ _} _ _ _.
-Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
-Arguments fill_empty {_ _ _ _ _} _.
-Arguments fill_comp {_ _ _ _ _} _ _ _.
-Arguments fill_not_val {_ _ _ _ _} _ _ _.
-Arguments ectx_positive {_ _ _ _ _} _ _ _.
-Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
+Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _} _.
+Arguments of_val {_} _%V.
+Arguments to_val {_} _%E.
+Arguments empty_ectx {_}.
+Arguments comp_ectx {_} _ _.
+Arguments fill {_} _ _%E.
+Arguments head_step {_} _%E _ _%E _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
-  Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-  Implicit Types (e : expr) (K : ectx).
+  Context {Λ : ectxLanguage}.
+  Implicit Types v : val Λ.
+  Implicit Types e : expr Λ.
+  Implicit Types K : ectx Λ.
+
+  (* Only project stuff out of the mixin that is not also in language *)
+  Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+  Proof. apply ectx_language_mixin. Qed.
+  Lemma fill_empty e : fill empty_ectx e = e.
+  Proof. apply ectx_language_mixin. Qed.
+  Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+  Proof. apply ectx_language_mixin. Qed.
+  Global Instance fill_inj K : Inj (=) (=) (fill K).
+  Proof. apply ectx_language_mixin. Qed.
+  Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+  Proof. apply ectx_language_mixin. Qed.
+  Lemma ectx_positive K1 K2 :
+    comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx.
+  Proof. apply ectx_language_mixin. Qed.
+  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
+    fill K e1 = fill K' e1' →
+    to_val e1 = None →
+    head_step e1' σ1 e2 σ2 efs →
+    ∃ K'', K' = comp_ectx K K''.
+  Proof. apply ectx_language_mixin. Qed.
 
-  Definition head_reducible (e : expr) (σ : state) :=
+  Definition head_reducible (e : expr Λ) (σ : state Λ) :=
     ∃ e' σ' efs, head_step e σ e' σ' efs.
-  Definition head_irreducible (e : expr) (σ : state) :=
+  Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
-  Definition sub_redexes_are_values (e : expr) :=
+  Definition sub_redexes_are_values (e : expr Λ) :=
     ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
 
-  Inductive prim_step (e1 : expr) (σ1 : state)
-      (e2 : expr) (σ2 : state) (efs : list expr) : Prop :=
+  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ)
+      (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
     Ectx_step K e1' e2' :
       e1 = fill K e1' → e2 = fill K e2' →
       head_step e1' σ1 e2' σ2 efs → prim_step e1 σ1 e2 σ2 efs.
@@ -77,19 +116,21 @@ Section ectx_language.
     head_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs.
   Proof. econstructor; eauto. Qed.
 
-  Lemma val_prim_stuck e1 σ1 e2 σ2 efs :
-    prim_step e1 σ1 e2 σ2 efs → to_val e1 = None.
-  Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
+  Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
+  Proof.
+    split.
+    - apply ectx_language_mixin.
+    - apply ectx_language_mixin.
+    - intros ????? [??? -> -> ?%val_head_stuck].
+      apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
+  Qed.
 
-  Canonical Structure ectx_lang : language := {|
-    language.expr := expr; language.val := val; language.state := state;
-    language.of_val := of_val; language.to_val := to_val;
-    language.prim_step := prim_step;
-    language.to_of_val := to_of_val; language.of_to_val := of_to_val;
-    language.val_stuck := val_prim_stuck;
-  |}.
+  Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
 
   (* Some lemmas about this language *)
+  Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
+  Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
+
   Lemma head_prim_step e1 σ1 e2 σ2 efs :
     head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
   Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
@@ -108,7 +149,7 @@ Section ectx_language.
     reducible e σ → sub_redexes_are_values e → head_reducible e σ.
   Proof.
     intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
-    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
     rewrite fill_empty /head_reducible; eauto.
   Qed.
   Lemma prim_head_irreducible e σ :
@@ -123,7 +164,7 @@ Section ectx_language.
     Atomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
-    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+    assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
@@ -135,14 +176,14 @@ Section ectx_language.
     intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
     destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' efs'')
       as [K' [-> _]%symmetry%ectx_positive];
-      eauto using fill_empty, fill_not_val, val_stuck.
+      eauto using fill_empty, fill_not_val, val_head_stuck.
     by rewrite !fill_empty.
   Qed.
 
   (* Every evaluation context is a context. *)
-  Global Instance ectx_lang_ctx K : LanguageCtx ectx_lang (fill K).
+  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
   Proof.
-    split.
+    split; simpl.
     - eauto using fill_not_val.
     - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
       by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
@@ -166,4 +207,10 @@ Section ectx_language.
   Qed.
 End ectx_language.
 
-Arguments ectx_lang _ {_ _ _ _}.
+Arguments ectx_lang : clear implicits.
+Coercion ectx_lang : ectxLanguage >-> language.
+
+Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
+  let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
+  @Language E V St of_val to_val _
+    (@ectx_lang_mixin (@EctxLanguage E V C St of_val to_val empty comp fill head mix)).

theories/program_logic/ectx_lifting.v

@@ -4,22 +4,13 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section wp.
-Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
+Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types P : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types v : val.
-Implicit Types e : expr.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
 Hint Resolve head_prim_reducible head_reducible_prim_step.
 
-Lemma wp_ectx_bind {E Φ} K e :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
-Proof. apply: weakestpre.wp_bind. Qed.
-
-Lemma wp_ectx_bind_inv {E Φ} K e :
-  WP fill K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
-Proof. apply: weakestpre.wp_bind_inv. Qed.
-
 Lemma wp_lift_head_step {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗

theories/program_logic/ectxi_language.v

@@ -4,92 +4,130 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language ectx_language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
-   inference to use a keys. *)
-Class EctxiLanguage (expr val ectx_item state : Type) := {
+(* TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
+language, you need to also define a corresponding [language] and [ectxLanguage]
+canonical structure for canonical structure inference to work properly. You
+should use the coercion [EctxLanguageOfEctxi] and [LanguageOfEctx] for that, and
+not [ectxi_lang] and [ectxi_lang_ectx], otherwise the canonical projections will
+not point to the right terms.
+
+A full concrete example of setting up your language can be found in [heap_lang].
+Below you can find the relevant parts:
+
+  Module heap_lang.
+    (* Your language definition *)
+
+    Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+    Proof. (* ... *) Qed.
+  End heap_lang.
+
+  Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
+  Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
+  Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
+*)
+
+Section ectxi_language_mixin.
+  Context {expr val ectx_item state : Type}.
+  Context (of_val : val → expr).
+  Context (to_val : expr → option val).
+  Context (fill_item : ectx_item → expr → expr).
+  Context (head_step : expr → state → expr → state → list expr → Prop).
+
+  Record EctxiLanguageMixin := {
+    mixin_to_of_val v : to_val (of_val v) = Some v;
+    mixin_of_to_val e v : to_val e = Some v → of_val v = e;
+    mixin_val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
+
+    mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
+    mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
+    mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+      to_val e1 = None → to_val e2 = None →
+      fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
+
+    mixin_head_ctx_step_val Ki e σ1 e2 σ2 efs :
+      head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e);
+  }.
+End ectxi_language_mixin.
+
+Structure ectxiLanguage := EctxiLanguage {
+  expr : Type;
+  val : Type;
+  ectx_item : Type;
+  state : Type;
+
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
   head_step : expr → state → expr → state → list expr → Prop;
 
-  to_of_val v : to_val (of_val v) = Some v;
-  of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
-
-  fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
-  fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
-  fill_item_no_val_inj Ki1 Ki2 e1 e2 :
-    to_val e1 = None → to_val e2 = None →
-    fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
-
-  head_ctx_step_val Ki e σ1 e2 σ2 efs :
-    head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e);
+  ectxi_language_mixin :
+    EctxiLanguageMixin of_val to_val fill_item head_step
 }.
 
-Arguments of_val {_ _ _ _ _} _%V.
-Arguments to_val {_ _ _ _ _} _%E.
-Arguments fill_item {_ _ _ _ _} _ _%E.
-Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
-
-Arguments to_of_val {_ _ _ _ _} _.
-Arguments of_to_val {_ _ _ _ _} _ _ _.
-Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
-Arguments fill_item_val {_ _ _ _ _} _ _ _.
-Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
+Arguments EctxiLanguage {_ _ _ _ _ _ _ _} _.
+Arguments of_val {_} _%V.
+Arguments to_val {_} _%E.
+Arguments fill_item {_} _ _%E.
+Arguments head_step {_} _%E _ _%E _ _.
 
 Section ectxi_language.
-  Context {expr val ectx_item state}
-          {Λ : EctxiLanguage expr val ectx_item state}.
-  Implicit Types (e : expr) (Ki : ectx_item).
-  Notation ectx := (list ectx_item).
+  Context {Λ : ectxiLanguage}.
+  Implicit Types (e : expr Λ) (Ki : ectx_item Λ).
+  Notation ectx := (list (ectx_item Λ)).
+
+  (* Only project stuff out of the mixin that is not also in ectxLanguage *)
+  Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+  Proof. apply ectxi_language_mixin. Qed.
+  Lemma fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+  Proof. apply ectxi_language_mixin. Qed.
+  Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+    to_val e1 = None → to_val e2 = None →
+    fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
+  Proof. apply ectxi_language_mixin. Qed.
+  Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
+    head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e).
+  Proof. apply ectxi_language_mixin. Qed.
 
-  Definition fill (K : ectx) (e : expr) : expr := foldl (flip fill_item) e K.
+  Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
 
   Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
   Proof. apply foldl_app. Qed.
 
-  Instance fill_inj K : Inj (=) (=) (fill K).
-  Proof. induction K as [|Ki K IH]; rewrite /Inj; naive_solver. Qed.
-
-  Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+  Definition ectxi_lang_ectx_mixin :
+    EctxLanguageMixin of_val to_val [] (flip (++)) fill head_step.
   Proof.
-    revert e.
-    induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val.
+    assert (fill_val : ∀ K e, is_Some (to_val (fill K e)) → is_Some (to_val e)).
+    { intros K. induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val. }
+    assert (fill_not_val : ∀ K e, to_val e = None → to_val (fill K e) = None).
+    { intros K e. rewrite !eq_None_not_Some. eauto. }
+    split.
+    - apply ectxi_language_mixin.
+    - apply ectxi_language_mixin.
+    - apply ectxi_language_mixin.
+    - done.
+    - intros K1 K2 e. by rewrite /fill /= foldl_app.
+    - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
+    - done.
+    - by intros [] [].
+    - intros K K' e1 e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
+      induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
+      destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
+      { rewrite fill_app in Hstep. apply head_ctx_step_val in Hstep.
+        apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
+      rewrite !fill_app /= in Hfill.
+      assert (Ki = Ki') as ->.
+      { eapply fill_item_no_val_inj, Hfill; eauto using val_head_stuck.
+        apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
+      simplify_eq. destruct (IH K') as [K'' ->]; auto.
+      exists K''. by rewrite assoc.
   Qed.
 
+  Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
+  Canonical Structure ectxi_lang := LanguageOfEctx ectxi_lang_ectx.
+
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
 
-  (* When something does a step, and another decomposition of the same expression
-  has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
-  other words, [e] also contains the reducible expression *)
-  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
-    fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 efs →
-    exists K'', K' = K'' ++ K. (* K `prefix_of` K' *)
-  Proof.
-    intros Hfill Hred Hstep; revert K' Hfill.
-    induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
-    destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
-    { rewrite fill_app in Hstep.
-      exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
-        eauto using fill_not_val, head_ctx_step_val. }
-    rewrite !fill_app /= in Hfill.
-    assert (Ki = Ki') as ->
-      by eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
-    simplify_eq. destruct (IH K') as [K'' ->]; auto.