solution for exercises 06

theories/type_systems/systemf_mu/exercises06_sol.v

@@ -0,0 +1,375 @@
+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.ts.systemf_mu Require Import lang notation types pure tactics logrel.
+From Autosubst Require Import Autosubst.
+
+(** * Exercise Sheet 6 *)
+
+Notation sub := lang.subst.
+
+Implicit Types
+  (e : expr)
+  (v : val)
+  (A B : type)
+.
+
+(** ** Exercise 5: Keep Rollin' *)
+(** This exercise is slightly tricky.
+  We strongly recommend you to first work on the other exercises.
+  You may use the results from this exercise, in particular the fixpoint combinator and its typing, in other exercises, however (which is why it comes first in this Coq file).
+ *)
+Section recursion_combinator.
+  Variable (f x: string). (* the template of the recursive function *)
+  Hypothesis (Hfx: f ≠ x).
+
+  (** Recursion Combinator *)
+  (* First, setup a definition [Rec] satisfying the reduction lemmas below. *)
+
+  (** You may find an auxiliary definition [rec_body] helpful *)
+  Definition rec_body (t: expr) : expr :=
+    roll (λ: f x, t (λ: x, (unroll f) f x) x).
+
+  Definition Rec (t: expr): val :=
+    λ: x, (unroll (rec_body t)) (rec_body t) x.
+
+  Lemma closed_rec_body t :
+    is_closed [] t → is_closed [] (rec_body t).
+  Proof. simplify_closed. Qed.
+  Lemma closed_Rec t :
+    is_closed [] t → is_closed [] (Rec t).
+  Proof. simplify_closed. Qed.
+  Lemma is_val_Rec t:
+    is_val (Rec t).
+  Proof. done. Qed.
+
+  Lemma rec_body_subst_x e t:
+    (sub x e (rec_body t))%E = rec_body t.
+  Proof.
+    simpl. destruct decide; try naive_solver.
+    destruct decide; naive_solver.
+  Qed.
+
+  Lemma rec_body_subst_f e t:
+    (sub f e (rec_body t))%E = rec_body t.
+  Proof.
+    simpl. destruct decide; naive_solver.
+  Qed.
+
+   Lemma Rec_red (t e: expr):
+    is_val e →
+    is_val t →
+    is_closed [] e →
+    is_closed [] t →
+    rtc contextual_step ((Rec t) e) (t (Rec t) e).
+  Proof.
+    intros Hval1 Hval2 Hcl1 Hcl2. do 4 try econstructor 2.
+    - rewrite /Rec. eapply app_step_beta; first eauto.
+      simplify_closed.
+    - cbn -[rec_body]. rewrite rec_body_subst_x.
+      destruct decide; try naive_solver.
+      simpl. eapply app_step_l; last eauto.
+      eapply app_step_l; last done.
+      eapply unroll_roll_step; done.
+    - eapply app_step_l; last eauto.
+      eapply app_step_beta; first done.
+      simplify_closed.
+    - simpl.
+      rewrite decide_False; last congruence.
+      rewrite decide_False; last congruence.
+      rewrite decide_True; last done.
+      rewrite !decide_False; last done.
+      eapply app_step_beta; [eauto|].
+      simplify_closed.
+    - cbn -[rec_body].
+      rewrite (subst_is_closed_nil _ f); last done.
+      rewrite (subst_is_closed_nil _ x); last done.
+      destruct decide; try naive_solver.
+      destruct decide; naive_solver.
+  Qed.
+
+  Lemma rec_body_typing n Γ (A B: type) t :
+    Γ !! x = None →
+    Γ !! f = None →
+    type_wf n A →
+    type_wf n B →
+    TY n; Γ ⊢ t : ((A → B) → (A → B)) →
+    TY n; Γ ⊢ rec_body t : (μ: #0 → rename (+1) A → rename (+1) B).
+  Proof.
+    intros Hx Hf Hwf1 Hwf2 Hty.
+    rewrite /rec_body. econstructor; asimpl.
+    solve_typing.
+    eapply typed_weakening; eauto.
+    etrans; first eapply insert_subseteq; first done.
+    eapply insert_subseteq; rewrite lookup_insert_ne //=.
+  Qed.
+
+  Lemma Rec_typing n Γ A B t:
+    type_wf n A →
+    type_wf n B →
+    Γ !! x = None →
+    Γ !! f = None →
+    TY n; Γ ⊢ t : ((A → B) → (A → B)) →
+    TY n; Γ ⊢ (Rec t) : (A → B).
+  Proof.
+    intros Hwf1 Hwf2 Hx Hf Ht. econstructor; last done.
+    econstructor; last first.
+    { econstructor. rewrite lookup_insert //=. }
+    econstructor; first eapply typed_unroll'.
+    - eapply typed_weakening with (Γ := Γ); eauto; last by eapply insert_subseteq.
+      eapply rec_body_typing with (A := A) (B := B); eauto.
+    - simpl. f_equal. f_equal; by asimpl.
+    - eapply typed_weakening with (Γ := Γ); eauto; last by eapply insert_subseteq.
+      eapply rec_body_typing; eauto.
+  Qed.
+
+End recursion_combinator.
+
+Definition Fix (f x: string) (e: expr) : val := (Rec f x (Lam f%string (Lam x%string e))).
+(** We "seal" the definition to make it opaque to the [solve_typing] tactic.
+  We do not want [solve_typing] to unfold the definition, instead, we should manually
+  apply the typing rule below.
+
+  You do not need to understand this in detail -- the only thing of relevance is that
+  you can use the equality [Fix_eq] to unfold the definition of [Fix].
+*)
+Definition Fix_aux : seal (Fix). Proof. by eexists. Qed.
+Definition Fix' := Fix_aux.(unseal).
+Lemma Fix_eq : Fix' = Fix.
+Proof. rewrite -Fix_aux.(seal_eq) //. Qed.
+Arguments Fix' _ _ _ : simpl never.
+
+(* the actual fixpoint combinator *)
+Notation "'fix:' f x := e" := (Fix' f x e)%E
+  (at level 200, f, x at level 1, e at level 200,
+   format "'[' 'fix:'  f  x   :=  '/  ' e ']'") : val_scope.
+Notation "'fix:' f x := e" := (Fix' f x e)%E
+  (at level 200, f, x at level 1, e at level 200,
+   format "'[' 'fix:'  f  x   :=  '/  ' e ']'") : expr_scope.
+
+
+Lemma fix_red (f x: string) (e e': expr):
+  is_closed [x; f] e →
+  is_closed [] e' →
+  is_val e' →
+  f ≠ x →
+  rtc contextual_step ((fix: f x := e) e')%V (sub x e' (sub f (fix: f x := e)%V e)).
+Proof.
+  intros He Hval. etransitivity; [|econstructor 2]; [| |econstructor 2].
+  - rewrite Fix_eq /Fix. eapply Rec_red; simpl; eauto.
+  - eapply app_step_l; last done.
+    eapply app_step_beta; last done.
+    done.
+  - simpl. rewrite decide_False; last congruence.
+    eapply app_step_beta; first done.
+    eapply is_closed_subst.
+    { apply closed_Rec; done. }
+    eapply is_closed_weaken; eauto. set_solver.
+  - rewrite Fix_eq; done.
+Qed.
+
+Lemma fix_typing n Γ (f x: string) (A B: type) (e: expr):
+  type_wf n A →
+  type_wf n B →
+  f ≠ x →
+  TY n; <[x := A]> (<[f := (A → B)%ty]> Γ) ⊢ e : B →
+  TY n; Γ ⊢ (fix: f x := e) : (A → B).
+Proof.
+  intros Hwf1 Hwf2 Hfx He.
+  rewrite Fix_eq /Fix.
+  eapply typed_weakening with (Γ := delete x (delete f Γ)); eauto; last first.
+  { etrans; eapply delete_subseteq. }
+  eapply Rec_typing; eauto.
+  - eapply lookup_delete.
+  - rewrite lookup_delete_ne //=. eapply lookup_delete.
+  - econstructor; last eauto.
+    econstructor; last eauto.
+    rewrite -delete_insert_ne //=.
+    rewrite !insert_delete_insert. done.
+Qed.
+
+(** ** Exercise 1: Encode arithmetic expressions *)
+
+Definition aexpr : type := μ: (Int + (#0 × #0)) + (#0 × #0).
+
+Definition num_val (v : val) : val := RollV (InjLV $ InjLV v).
+Definition num_expr (e : expr) : expr := Roll (InjL $ InjL e).
+
+Definition plus_val (v1 v2 : val) : val := RollV (InjLV $ InjRV (v1, v2)).
+Definition plus_expr (e1 e2 : expr) : expr := Roll (InjL $ InjR (e1, e2)).
+
+Definition mul_val (v1 v2 : val) : val := RollV (InjRV (v1, v2)).
+Definition mul_expr (e1 e2 : expr) : expr := Roll (InjR (e1, e2)).
+
+Lemma num_expr_typed n Γ e :
+  TY n; Γ ⊢ e : Int →
+  TY n; Γ ⊢ num_expr e : aexpr.
+Proof.
+  intros. solve_typing.
+  Qed.
+
+Lemma plus_expr_typed n Γ e1 e2 :
+  TY n; Γ ⊢ e1 : aexpr →
+  TY n; Γ ⊢ e2 : aexpr →
+  TY n; Γ ⊢ plus_expr e1 e2 : aexpr.
+Proof.
+  
+  intros; solve_typing.
+Qed.
+
+Lemma mul_expr_typed n Γ e1 e2 :
+  TY n; Γ ⊢ e1 : aexpr →
+  TY n; Γ ⊢ e2 : aexpr →
+  TY n; Γ ⊢ mul_expr e1 e2 : aexpr.
+Proof.
+  
+  intros; solve_typing.
+Qed.
+
+Definition eval_aexpr : val :=
+  fix: "rec" "e" := match: unroll "e" with
+           InjL "e'" =>
+              match: "e'" with
+                InjL "n" => "n"
+              | InjR "es" => "rec" (Fst "es") + "rec" (Snd "es")
+              end
+           | InjR "es" => "rec" (Fst "es") * "rec" (Snd "es")
+            end.
+
+Lemma eval_aexpr_typed Γ n :
+  TY n; Γ ⊢ eval_aexpr : (aexpr → Int).
+Proof.
+  unfold eval_aexpr.
+  apply fix_typing; solve_typing.
+  done.
+Qed.
+
+
+(** Exercise 3: Lists *)
+
+Definition list_t (A : type) : type :=
+  ∃: (#0 (* mynil *)
+    × (A.[ren (+1)] → #0 → #0) (* mycons *)
+    × (∀: #1 → #0 → (A.[ren (+2)] → #1 → #0) → #0)) (* mylistcase *)
+  .
+
+Definition mylist_impl : val :=
+  
+  pack ((#0, #()),        (* mynil *)
+        (λ: "a" "l", (#1 + Fst "l", ("a", Snd "l"))),   (* mycons *)
+        (Λ, λ: "l" "n" "c",
+          if: Fst "l" = #0 then "n" else "c" (Fst (Snd "l")) (Fst "l" - #1, Snd (Snd "l")))) (* mycase *).
+
+(** We define a recursive representation predicate for lists.
+  This is a common pattern: we specify the shape of lists in our language in terms of lists at the meta-level (i.e., in Coq).
+*)
+Fixpoint represents_list_rec (l : list val) (v : val) :=
+  match l with
+  | [] => v = #()
+  | h :: l' => ∃ v' : val, v = (h, v')%V ∧ represents_list_rec l' v'
+  end.
+(* A full list also needs to store the length, otherwise we'd have no way of knowing
+  when a list ends (we can't analyze whether a term is () or a pair from inside the language) *)
+Definition represents_list (l : list val) (v : val) :=
+  ∃ (n : Z) (v' : val), n = length l ∧ v = (#n, v')%V ∧
+  represents_list_rec l v'.
+
+Lemma mylist_impl_sem_typed A :
+  type_wf 0 A →
+  ∀ k, 𝒱 (list_t A) δ_any k mylist_impl.
+Proof.
+  intros Hwf k.
+  unfold list_t.
+  simp type_interp.
+  eexists _. split; first done.
+  pose_sem_type (λ k' (v : val), ∃ l : list val, represents_list l v ∧ Forall (fun v => 𝒱 A δ_any k' v) l) as τ.
+  {
+    intros k' v (l & Hrep & Hl).
+    destruct Hrep as (n & v' & -> & -> & Hrep). simplify_closed.
+    induction l as [ | h l IH] in v', Hrep, Hl |-*; simpl in Hrep.
+    - rewrite Hrep. done.
+    - destruct Hrep as (v'' & -> & Hrep).
+      simplify_closed.
+      + eapply Forall_inv in Hl. eapply val_rel_is_closed in Hl. done.
+      + eapply IH; first done. eapply Forall_inv_tail in Hl. done.
+  }
+  {
+    intros k' k'' v (l & Hrep & Hl) Hle.
+    exists l. split; first done.
+    eapply Forall_impl; first done.
+    intros v'. by eapply val_rel_mono.
+  }
+  exists τ.
+  simp type_interp. eexists _, _. split; first done. split;
+    [ simp type_interp; eexists _, _; split; first done; split | ].
+  - simp type_interp. simpl. exists []. split; last done.
+    eexists _, _; simpl; split; first done. done.
+  - simp type_interp. eexists _, _. split; first done. split; first done.
+    intros v2 k' Hk' Hv2. simpl. eapply (sem_val_expr_rel _ _ _ (LamV _ _)).
+    simp type_interp. eexists _, _. split; first done.
+    specialize (val_rel_is_closed _ _ _ _ Hv2) as ?.
+    split; first by simplify_closed.
+
+    intros v3 k'2 Hk'2 Hv3.
+    simpl. rewrite subst_is_closed_nil; last done.
+    simp type_interp in Hv3. destruct Hv3 as (l & (len & hv & -> & -> & Hv3) & Hl).
+    simpl.
+
+    eapply expr_det_steps_closure.
+    { repeat do_det_step. constructor. }
+    eapply (sem_val_expr_rel _ _ _ (PairV _ (PairV _ _))).
+    simp type_interp. simpl.
+    exists (v2 :: l). split.
+    { simpl. eexists _, (v2, hv)%V. split; first done.
+      simpl. split. { f_equal. f_equal. f_equal. lia. }
+      eexists _; done.
+    }
+    econstructor.
+    { eapply sem_val_rel_cons; eapply val_rel_mono; last done. lia. }
+    eapply Forall_impl; first done.
+    intros v' Hv'. eapply val_rel_mono; last apply Hv'. lia.
+  - simp type_interp. eexists; split; first done. split; first done.
+    intros τ'. eapply (sem_val_expr_rel _ _ _ (LamV _ _)).
+    simp type_interp. eexists _, _. split; first done. split; first done.
+    intros v2 k' Hk' Hv2. simpl.
+    eapply (sem_val_expr_rel _ _ _ (LamV _ _)).
+    simp type_interp. eexists _, _. split; first done.
+    specialize (val_rel_is_closed _ _ _ _ Hv2) as ?.
+    split; first by simplify_closed.
+    intros v3 k'2 Hk'2 Hv3. simpl.
+    rewrite subst_is_closed_nil; last done.
+    eapply (sem_val_expr_rel _ _ _ (LamV _ _)).
+    simp type_interp. eexists _, _. split; first done.
+    specialize (val_rel_is_closed _ _ _ _ Hv3) as ?.
+    split; first by simplify_closed.
+    intros v4 k'3 Hk'3 Hv4. simpl.
+    rewrite !subst_is_closed_nil; [ | done..].
+
+    simp type_interp in Hv2. simpl in Hv2. destruct Hv2 as (l & (len & vl & -> & -> & Hl) & Hlf).
+    simpl.
+
+    destruct l as [ | h l].
+    + eapply expr_det_steps_closure.
+      { repeat do_det_step. econstructor. }
+      eapply sem_val_expr_rel.
+      eapply val_rel_mono; last done. lia.
+    + simpl in Hl. destruct Hl as (vl' & -> & Hl).
+      eapply expr_det_steps_closure.
+      { repeat do_det_step. econstructor. }
+      replace (S (length l) - 1)%Z with (Z.of_nat $ length l) by lia.
+      eapply semantic_app.
+      { eapply semantic_app.
+        { eapply sem_val_expr_rel.
+          eapply val_rel_mono; last done. lia.
+        }
+        apply Forall_inv in Hlf.
+        eapply sem_val_expr_rel, val_rel_mono.
+        2: { eapply sem_val_rel_cons in Hlf. erewrite sem_val_rel_cons in Hlf. asimpl in Hlf. apply Hlf. }
+        lia.
+      }
+
+      eapply (sem_val_expr_rel _ _ _ (PairV (LitV _) _)). simp type_interp. simpl. exists l. split.
+      { eexists _, _. done. }
+      eapply Forall_inv_tail.
+      eapply Forall_impl; first done.
+      intros v' Hv'. eapply val_rel_mono; last apply Hv'. lia.
+Qed.

theories/type_systems/systemf_mu/pure_sol.v

@@ -0,0 +1,310 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import maps.
+From semantics.ts.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.
+  destruct (to_val e) as [ v | ] eqn:Hv.
+  { intros _. right. apply is_val_spec. eauto. }
+  intros Hcontextual. left.
+  inversion Hcontextual as [K' e1' e2' Heq1 Heq2 Hstep]; subst.
+  eapply step_by_val in Heq1 as (K'' & ->); [ | done | done].
+  rewrite <-fill_comp.
+  eexists _. split; [done | ].
+  rewrite <-fill_comp in Hcontextual.
+  apply contextual_step_ectx_inv in Hcontextual; done.
+Qed.
+
+(** ** 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.
+  intros [Hsteps Hirred].
+  induction k as [ | k IH] in e, e', Hsteps, Hirred |-*.
+  - inversion Hsteps; subst.
+    exists 0, e. split_and!; [done | split | ].
+    + constructor.
+    + by eapply irreducible_fill.
+    + done.
+  - inversion Hsteps as [ | n e1 e2 e3 Hstep Hsteps' Heq1 Heq2 Heq3]. subst.
+    destruct (contextual_ectx_step_case _ _ _ Hstep) as [(e'' & -> & Hstep') | Hv].
+    + apply IH in Hsteps' as (j & e3 & ? & Hsteps' & Hsteps''); last done.
+      eexists (S j), _. split_and!; [lia | | done].
+      eapply contextual_step_red_nsteps; done.
+    + exists 0, e. split_and!; [ lia | | ].
+      * split; [constructor | ].
+        apply val_irreducible. by apply is_val_spec.
+      * simpl. by eapply contextual_step_red_nsteps.
+Qed.
+
+
+(** 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.