systemf mu

_CoqProject

@@ -49,6 +49,15 @@ theories/systemf/free_theorems.v
 theories/systemf/binary_logrel.v
 theories/systemf/existential_invariants.v
 
+# SystemF-Mu
+theories/systemf_mu/lang.v
+theories/systemf_mu/notation.v
+theories/systemf_mu/types.v
+theories/systemf_mu/tactics.v
+theories/systemf_mu/pure.v
+theories/systemf_mu/untyped_encoding.v
+
+
 
 # By removing the # below, you can add the exercise sheets to make
 # theories/warmup/sheet0.v

theories/systemf_mu/notation.v

+From semantics.systemf_mu Require Export lang.
+Set Default Proof Using "Type".
+
+
+(** Coercions to make programs easier to type. *)
+Coercion of_val : val >-> expr.
+Coercion LitInt : Z >-> base_lit.
+Coercion LitBool : bool >-> base_lit.
+Coercion App : expr >-> Funclass.
+Coercion Var : string >-> expr.
+
+(** Define some derived forms. *)
+Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
+
+(* No scope for the values, does not conflict and scope is often not inferred
+properly. *)
+Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
+Notation "# l" := (Lit l%Z%E%stdpp) (at level 8, format "# l") : expr_scope.
+
+(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
+    first. *)
+Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
+Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
+
+Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
+  (Match e0 x1%binder e1 x2%binder e2)
+  (e0, x1, e1, x2, e2 at level 200,
+   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
+Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
+  (Match e0 x2%binder e2 x1%binder e1)
+  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
+
+Notation "()" := LitUnit : val_scope.
+
+Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
+Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
+Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope.
+
+(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*)
+
+Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
+  (at level 200, e1, e2, e3 at level 200) : expr_scope.
+
+Notation "λ: x , e" := (Lam x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
+Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
+
+Notation "λ: x , e" := (LamV x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
+Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
+
+Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
+  (at level 200, x at level 1, e1, e2 at level 200,
+   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
+  (at level 100, e2 at level 200,
+   format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.
+
+
+Notation "'Λ' , e" := (TLam e%E)
+  (at level 200, e at level 200,
+    format "'[' 'Λ' , '/  ' e ']'") : expr_scope.
+Notation "'Λ' , e" := (TLamV e%E)
+  (at level 200, e at level 200,
+    format "'[' 'Λ' , '/  ' e ']'") : val_scope.
+
+(* the [e] always needs to be paranthesized, due to the level
+   (chosen to make this cooperate with the [App] coercion) *)
+Notation "e '<>'" := (TApp e%E)
+  (at level 10) : expr_scope.
+(*Check ((Λ, #4) <>)%E.*)
+(*Check (((λ: "x", "x") #5) <>)%E.*)
+
+Notation "'pack' e" := (Pack e%E)
+  (at level 200, e at level 200) : expr_scope.
+Notation "'pack' v" := (PackV v%V)
+  (at level 200, v at level 200) : val_scope.
+Notation "'unpack'  e1  'as'  x  'in'  e2" := (Unpack x%binder e1%E e2%E)
+  (at level 200, e1, e2 at level 200, x at level 1) : expr_scope.
+
+Notation "'roll'  e" := (Roll e%E)
+  (at level 200, e at level 200) : expr_scope.
+Notation "'roll'  v" := (RollV v%E)
+  (at level 200, v at level 200) : val_scope.
+Notation "'unroll'  e" := (Unroll e%E)
+  (at level 200, e at level 200) : expr_scope.

theories/systemf_mu/pure.v

+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import maps.
+From semantics.systemf_mu Require Import lang notation.
+
+Lemma contextual_ectx_step_case K e e' :
+  contextual_step (fill K e) e' →
+  (∃ e'', e' = fill K e'' ∧ contextual_step e e'') ∨ is_val e.
+Proof.
+  (* FIXME: exercise for you :) *)
+(*Qed.*)
+Admitted.
+
+(** ** Deterministic reduction *)
+
+Record det_step (e1 e2 : expr) := {
+  det_step_safe : reducible e1;
+  det_step_det e2' :
+    contextual_step e1 e2' → e2' = e2
+}.
+
+Record det_base_step (e1 e2 : expr) := {
+  det_base_step_safe : base_reducible e1;
+  det_base_step_det e2' :
+    base_step e1 e2' → e2' = e2
+}.
+
+Lemma det_base_step_det_step e1 e2 : det_base_step e1 e2 → det_step e1 e2.
+Proof.
+  intros [Hp1 Hp2]. split.
+  - destruct Hp1 as (e2' & ?).
+    eexists e2'. by apply base_contextual_step.
+  - intros e2' ?%base_reducible_contextual_step; [ | done]. by apply Hp2.
+Qed.
+
+(** *** Pure execution lemmas *)
+Local Ltac inv_step :=
+  repeat match goal with
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : base_step ?e ?e2 |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
+     and should thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+Local Ltac solve_exec_safe := intros; subst; eexists; econstructor; eauto.
+Local Ltac solve_exec_detdet := simpl; intros; inv_step; try done.
+Local Ltac solve_det_exec :=
+  subst; intros; apply det_base_step_det_step;
+    constructor; [solve_exec_safe | solve_exec_detdet].
+
+Lemma det_step_beta x e e2 :
+  is_val e2 →
+  det_step (App (@Lam x e) e2) (subst' x e2 e).
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_tbeta e :
+  det_step ((Λ, e) <>) e.
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_unpack e1 e2 x :
+  is_val e1 →
+  det_step (unpack (pack e1) as x in e2) (subst' x e1 e2).
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_unop op e v v' :
+  to_val e = Some v →
+  un_op_eval op v = Some v' →
+  det_step (UnOp op e) v'.
+Proof. solve_det_exec. by simplify_eq. Qed.
+
+Lemma det_step_binop op e1 v1 e2 v2 v' :
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  bin_op_eval op v1 v2 = Some v' →
+  det_step (BinOp op e1 e2) v'.
+Proof. solve_det_exec. by simplify_eq. Qed.
+
+Lemma det_step_if_true e1 e2 :
+  det_step (if: #true then e1 else e2) e1.
+Proof. solve_det_exec. Qed.
+Lemma det_step_if_false e1 e2 :
+  det_step (if: #false then e1 else e2) e2.
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_fst e1 e2 :
+  is_val e1 →
+  is_val e2 →
+  det_step (Fst (e1, e2)) e1.
+Proof. solve_det_exec. Qed.
+Lemma det_step_snd e1 e2 :
+  is_val e1 →
+  is_val e2 →
+  det_step (Snd (e1, e2)) e2.
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_casel e e1 e2 :
+  is_val e →
+  det_step (Case (InjL e) e1 e2) (e1 e).
+Proof. solve_det_exec. Qed.
+Lemma det_step_caser e e1 e2 :
+  is_val e →
+  det_step (Case (InjR e) e1 e2) (e2 e).
+Proof. solve_det_exec. Qed.
+
+Lemma det_step_unroll e :
+  is_val e →
+  det_step (unroll (roll e)) e.
+Proof. solve_det_exec. Qed.
+
+(** ** n-step reduction *)
+(** Reduce in n steps to an irreducible expression.
+    (this is ⇝^n from the lecture notes)
+ *)
+Definition red_nsteps (n : nat) (e e' : expr) := nsteps contextual_step n e e' ∧ irreducible e'.
+
+Lemma det_step_red e e' e'' n :
+  det_step e e' →
+  red_nsteps n e e'' →
+  1 ≤ n ∧ red_nsteps (n - 1) e' e''.
+Proof.
+  intros [Hprog Hstep] Hred.
+  inversion Hprog; subst.
+  destruct Hred as [Hred  Hirred].
+  destruct n as [ | n].
+  { inversion Hred; subst.
+    exfalso; eapply not_reducible; done.
+  }
+  inversion Hred; subst. simpl.
+  apply Hstep in H as ->. apply Hstep in H1 as ->.
+  split; first lia.
+  replace (n - 0) with n by lia. done.
+Qed.
+
+Lemma contextual_step_red_nsteps n e e' e'' :
+  contextual_step e e' →
+  red_nsteps n e' e'' →
+  red_nsteps (S n) e e''.
+Proof.
+  intros Hstep [Hsteps Hirred].
+  split; last done.
+  by econstructor.
+Qed.
+
+Lemma nsteps_val_inv n v e' :
+  red_nsteps n (of_val v) e' → n = 0 ∧ e' = of_val v.
+Proof.
+  intros [Hred Hirred]; cbn in *.
+  destruct n as [ | n].
+  - inversion Hred; subst. done.
+  - inversion Hred; subst. exfalso. eapply val_irreducible; last done.
+    rewrite to_of_val. eauto.
+Qed.
+
+Lemma nsteps_val_inv' n v e e' :
+  to_val e = Some v →
+  red_nsteps n e e' → n = 0 ∧ e' = of_val v.
+Proof. intros Ht. rewrite -(of_to_val _ _ Ht). apply nsteps_val_inv. Qed.
+
+Lemma red_nsteps_fill K k e e' :
+  red_nsteps k (fill K e) e' →
+  ∃ j e'', j ≤ k ∧
+    red_nsteps j e e'' ∧
+    red_nsteps (k - j) (fill K e'') e'.
+Proof.
+  (* FIXME: this is an exercise :) *)
+Admitted.
+
+
+(** Additionally useful stepping lemmas *)
+Lemma app_step_r (e1 e2 e2': expr) :
+  contextual_step e2 e2' → contextual_step (e1 e2) (e1 e2').
+Proof. by apply (fill_contextual_step [AppRCtx _]). Qed.
+
+Lemma app_step_l (e1 e1' e2: expr) :
+  contextual_step e1 e1' → is_val e2 → contextual_step (e1 e2) (e1' e2).
+Proof.
+  intros ? (v & Hv)%is_val_spec.
+  rewrite <-(of_to_val _ _ Hv).
+  by apply (fill_contextual_step [AppLCtx _]).
+Qed.
+
+Lemma app_step_beta (x: string) (e e': expr) :
+  is_val e' → is_closed [x] e → contextual_step ((λ: x, e) e') (lang.subst x e' e).
+Proof.
+  intros Hval Hclosed. eapply base_contextual_step, BetaS; eauto.
+Qed.
+
+Lemma unroll_roll_step (e: expr) :
+  is_val e → contextual_step (unroll (roll e)) e.
+Proof.
+  intros ?; by eapply base_contextual_step, UnrollS.
+Qed.
+
+
+Lemma fill_reducible K e :
+  reducible e → reducible (fill K e).
+Proof.
+  intros (e' & Hstep).
+  exists (fill K e'). eapply fill_contextual_step. done.
+Qed.
+
+Lemma reducible_contextual_step_case K e e' :
+  contextual_step (fill K e) (e') →
+  reducible e →
+  ∃ e'', e' = fill K e'' ∧ contextual_step e e''.
+Proof.
+  intros [ | Hval]%contextual_ectx_step_case Hred; first done.
+  exfalso. apply is_val_spec in Hval as (v & Hval).
+  apply reducible_not_val in Hred. congruence.
+Qed.
+
+(** Contextual lifting lemmas for deterministic reduction *)
+Tactic Notation "lift_det" uconstr(ctx) :=
+  intros;
+  let Hs := fresh in
+  match goal with
+  | H : det_step _ _ |- _ => destruct H as [? Hs]
+  end;
+  simplify_val; econstructor;
+  [intros; by eapply (fill_reducible ctx) |
+   intros ? (? & -> & ->%Hs)%(reducible_contextual_step_case ctx); done ].
+
+Lemma det_step_pair_r e1 e2 e2' :
+  det_step e2 e2' →
+  det_step (e1, e2)%E (e1, e2')%E.
+Proof. lift_det [PairRCtx _]. Qed.
+Lemma det_step_pair_l e1 e1' e2 :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (e1, e2)%E (e1', e2)%E.
+Proof. lift_det [PairLCtx _]. Qed.
+Lemma det_step_binop_r e1 e2 e2' op :
+  det_step e2 e2' →
+  det_step (BinOp op e1 e2)%E (BinOp op e1 e2')%E.
+Proof. lift_det [BinOpRCtx _ _]. Qed.
+Lemma det_step_binop_l e1 e1' e2 op :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (BinOp op e1 e2)%E (BinOp op e1' e2)%E.
+Proof. lift_det [BinOpLCtx _ _]. Qed.
+Lemma det_step_if e e' e1 e2 :
+  det_step e e' →
+  det_step (If e e1 e2)%E (If e' e1 e2)%E.
+Proof. lift_det [IfCtx _ _]. Qed.
+Lemma det_step_app_r e1 e2 e2' :
+  det_step e2 e2' →
+  det_step (App e1 e2)%E (App e1 e2')%E.
+Proof. lift_det [AppRCtx _]. Qed.
+Lemma det_step_app_l e1 e1' e2 :
+  is_val e2 →
+  det_step e1 e1' →
+  det_step (App e1 e2)%E (App e1' e2)%E.
+Proof. lift_det [AppLCtx _]. Qed.
+Lemma det_step_snd_lift e e' :
+  det_step e e' →
+  det_step (Snd e)%E (Snd e')%E.
+Proof. lift_det [SndCtx]. Qed.
+Lemma det_step_fst_lift e e' :
+  det_step e e' →
+  det_step (Fst e)%E (Fst e')%E.
+Proof. lift_det [FstCtx]. Qed.
+
+
+#[global]
+Hint Resolve app_step_r app_step_l app_step_beta unroll_roll_step : core.
+#[global]
+Hint Extern 1 (is_val _) => (simpl; fast_done) : core.
+#[global]
+Hint Immediate is_val_of_val : core.
+
+#[global]
+Hint Resolve det_step_beta det_step_tbeta det_step_unpack det_step_unop det_step_binop det_step_if_true det_step_if_false det_step_fst det_step_snd det_step_casel det_step_caser det_step_unroll : core.
+
+#[global]
+Hint Resolve det_step_pair_r det_step_pair_l det_step_binop_r det_step_binop_l det_step_if det_step_app_r det_step_app_l det_step_snd_lift det_step_fst_lift : core.
+
+#[global]
+Hint Constructors nsteps : core.
+
+#[global]
+Hint Extern 1 (is_val _) => simpl : core.
+
+(** Prove a single deterministic step using the lemmas we just proved *)
+Ltac do_det_step :=
+  match goal with
+  | |- nsteps det_step _ _ _ => econstructor 2; first do_det_step
+  | |- det_step _ _ => simpl; solve[eauto 10]
+  end.

theories/systemf_mu/tactics.v

+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export facts maps sets.
+From semantics.systemf_mu Require Export lang notation types.
+
+Ltac map_solver :=
+  repeat match goal with
+         | |-  (⤉ _) !! _ = Some _ =>
+             rewrite fmap_insert
+         | |- <[ ?p := _ ]> _ !! ?p = Some _ =>
+             apply lookup_insert
+         | |- <[ _ := _ ]> _ !! _ = Some _ =>
+             rewrite lookup_insert_ne; [ | congruence]
+         end.
+Ltac solve_typing :=
+  intros;
+  repeat match goal with
+  | |- TY _ ; _ ⊢ ?e : ?A => first [eassumption | econstructor]
+  (* heuristic to solve tapp goals where we need to pick the right type for the substitution *)
+  | |- TY _ ; _ ⊢ ?e <> : ?A => eapply typed_tapp'; [solve_typing | | asimpl; reflexivity]
+  | |- TY _ ; _ ⊢ Unroll ?e : ?A => eapply typed_unroll'; [solve_typing | asimpl; reflexivity]
+  | |- bin_op_typed _ _ _ _ => econstructor
+  | |- un_op_typed _ _ _ _ => econstructor
+  | |- type_wf _ ?e => assert_fails (is_evar e); eassumption
+  | |- type_wf _ ?e => assert_fails (is_evar e); econstructor
+  | |- type_wf _ (subst _ ?A) => eapply type_wf_subst; [ | intros; simpl]
+  | |- type_wf _ ?e => assert_fails (is_evar e); eapply type_wf_mono; [eassumption | lia]
+  (* conditions spawned by the tyvar case of [type_wf] *)
+  | |- _ < _ => lia
+  (* conditions spawned by the variable case *)
+  | |- _ !! _ = Some _ => map_solver
+  end.
+
+Tactic Notation "unify_type" uconstr(A) :=
+  match goal with
+  | |- TY ?n; ?Γ ⊢ ?e : ?B => unify A B
+  end.
+Tactic Notation "replace_type" uconstr(A) :=
+  match goal with
+  | |- TY ?n; ?Γ ⊢ ?e : ?B => replace B%ty with A%ty; cycle -1; first try by asimpl
+  end.
+
+
+Ltac simplify_list_elem :=
+  simpl;
+  repeat match goal with
+         | |- ?x ∈ ?y :: ?l => apply elem_of_cons; first [left; reflexivity | right]
+         | |- _ ∉ [] => apply not_elem_of_nil
+         | |- _ ∉ _ :: _ => apply not_elem_of_cons; split
+  end; try fast_done.
+Ltac simplify_list_subseteq :=
+  simpl;
+  repeat match goal with
+         | |- ?x :: _ ⊆ ?x :: _ => apply list_subseteq_cons_l
+         | |- ?x :: _ ⊆ _ => apply list_subseteq_cons_elem; first solve [simplify_list_elem]
+         | |- elements _ ⊆ elements _ => apply elements_subseteq; set_solver
+         | |- [] ⊆ _ => apply list_subseteq_nil
+         | |- ?x :b: _ ⊆ ?x :b: _ => apply list_subseteq_cons_binder
+         (* NOTE: this might make the goal unprovable *)
+         (*| |- elements _ ⊆ _ :: _ => apply list_subseteq_cons_r*)
+         end;
+  try fast_done.
+
+(* Try to solve [is_closed] goals using a number of heuristics (that shouldn't make the goal unprovable) *)
+Ltac simplify_closed :=
+  simpl; intros;
+  repeat match goal with
+  | |- closed _ _ => unfold closed; simpl
+  | |- Is_true (is_closed [] _) => first [assumption | done]
+  | |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[simplify_closed]
+  | |- Is_true (is_closed ?X ?v) => assert_fails (is_evar X); eapply is_closed_weaken
+  | |- Is_true (is_closed _ _) => eassumption
+  | |- Is_true (_ && true) => rewrite andb_true_r
+  | |- Is_true (true && _) => rewrite andb_true_l
+  | |- Is_true (?a && ?a) => rewrite andb_diag
+  | |- Is_true (_ && _)  => simpl; rewrite !andb_True; split_and!
+  | |- _ ⊆ ?A => match type of A with | list _ => simplify_list_subseteq end
+  | |- _ ∈ ?A => match type of A with | list _ => simplify_list_elem end
+  | |- _ ≠ _ => congruence
+  | H : closed _ _ |- _ => unfold closed in H; simpl in H
+  | H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
+  | H : _ ∧ _ |- _ => destruct H
+  | |- Is_true (bool_decide (_ ∈ _)) => apply bool_decide_pack; set_solver
+  end; try fast_done.

theories/systemf_mu/untyped_encoding.v

+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.systemf_mu Require Import lang notation types pure tactics.
+From Autosubst Require Import Autosubst.
+
+(** * Encoding of the untyped lambda calculus *)
+
+Definition D := (μ: #0 → #0)%ty.
+
+Definition lame (x : string) (e : expr) : val := RollV (λ: x, e).
+Definition appe (e1 e2 : expr) : expr := (unroll e1) e2.
+
+Lemma lame_typed n Γ x e :
+  TY n; (<[x := D]> Γ) ⊢ e : D →
+  TY n; Γ ⊢ lame x e : D.
+Proof. solve_typing. Qed.
+
+Lemma app_typed n Γ e1 e2 :
+  TY n; Γ ⊢ e1 : D →
+  TY n; Γ ⊢ e2 : D →
+  TY n; Γ ⊢ appe e1 e2 : D.
+Proof.
+  solve_typing.
+Qed.
+
+Lemma appe_step_l e1 e1' (v : val) :
+  contextual_step e1 e1' →
+  contextual_step (appe e1 v) (appe e1' v).
+Proof.
+  intros Hstep. unfold appe.
+  by eapply (fill_contextual_step [UnrollCtx; AppLCtx _]).
+Qed.
+
+Lemma appe_step_r e1 e2 e2' :
+  contextual_step e2 e2' →
+  contextual_step (appe e1 e2) (appe e1 e2').
+Proof.
+  intros Hstep. unfold appe.
+  by eapply (fill_contextual_step [AppRCtx _]).
+Qed.
+
+Lemma lame_step_beta x e (v : val) :
+  rtc contextual_step (appe (lame x e) v) (lang.subst x v e).
+Proof.
+  unfold appe, lame.
+  econstructor 2.
+  { eapply (fill_contextual_step [AppLCtx _]).
+    eapply base_contextual_step. by econstructor.
+  }
+  econstructor 2.
+  { eapply base_contextual_step. econstructor; eauto. }
+  reflexivity.
+Qed.
+
+(* Divergence *)
+Definition ω : expr :=
+  roll (λ: "x", (unroll "x") "x").
+
+Definition Ω := ((unroll ω) ω)%E.
+