Merge branch 'amin/logrel' into 'master'

Amin/logrel

Closes #2

See merge request FP/iris-examples!2

README.md

@@ -30,6 +30,19 @@ This repository contains the following case studies:
 
 * [barrier](theories/barrier): The implementation and proof of a barrier as
   described in "Higher-Order Ghost State" <http://doi.acm.org/10.1145/2818638>.
+* [logrel](theories/logrel): the following logical relations from the paper <http://doi.acm.org/10.1145/3093333.3009855>:
+  * STLC
+      * Unary logical relations proving type safety
+  * F_mu (System F with recursive types)
+      * Unary logical relations proving type safety
+  * F_mu_ref (System F with recursive types and references)
+      * Unary logical relations proving type safety
+	  * Binary logical relations for proving contextual refinements
+  * F_mu_ref_conc (System F with recursive types, references and concurrency)
+      * Unary logical relations proving type safety
+	  * Binary logical relations for proving contextual refinements
+	      * Proof of refinement for a pair of fine-grained/coarse-grained concurrent counter implementations
+		  * Proof of refinement for a pair of fine-grained/coarse-grained concurrent stack implementations
 
 ## For Developers: How to update the Iris dependency
 

_CoqProject

@@ -6,3 +6,45 @@ theories/barrier/barrier.v
 theories/barrier/protocol.v
 theories/barrier/example_client.v
 theories/barrier/example_joining_existentials.v
+
+theories/logrel/prelude/base.v
+theories/logrel/stlc/lang.v
+theories/logrel/stlc/typing.v
+theories/logrel/stlc/rules.v
+theories/logrel/stlc/logrel.v
+theories/logrel/stlc/fundamental.v
+theories/logrel/stlc/soundness.v
+theories/logrel/F_mu/lang.v
+theories/logrel/F_mu/typing.v
+theories/logrel/F_mu/rules.v
+theories/logrel/F_mu/logrel.v
+theories/logrel/F_mu/fundamental.v
+theories/logrel/F_mu/soundness.v
+theories/logrel/F_mu_ref/lang.v
+theories/logrel/F_mu_ref/typing.v
+theories/logrel/F_mu_ref/rules.v
+theories/logrel/F_mu_ref/rules_binary.v
+theories/logrel/F_mu_ref/logrel.v
+theories/logrel/F_mu_ref/logrel_binary.v
+theories/logrel/F_mu_ref/fundamental.v
+theories/logrel/F_mu_ref/fundamental_binary.v
+theories/logrel/F_mu_ref/soundness.v
+theories/logrel/F_mu_ref/context_refinement.v
+theories/logrel/F_mu_ref/soundness_binary.v
+theories/logrel/F_mu_ref_conc/lang.v
+theories/logrel/F_mu_ref_conc/rules.v
+theories/logrel/F_mu_ref_conc/typing.v
+theories/logrel/F_mu_ref_conc/logrel_unary.v
+theories/logrel/F_mu_ref_conc/fundamental_unary.v
+theories/logrel/F_mu_ref_conc/rules_binary.v
+theories/logrel/F_mu_ref_conc/logrel_binary.v
+theories/logrel/F_mu_ref_conc/fundamental_binary.v
+theories/logrel/F_mu_ref_conc/soundness_unary.v
+theories/logrel/F_mu_ref_conc/context_refinement.v
+theories/logrel/F_mu_ref_conc/soundness_binary.v
+theories/logrel/F_mu_ref_conc/examples/lock.v
+theories/logrel/F_mu_ref_conc/examples/counter.v
+theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
+theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
+theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
\ No newline at end of file

theories/logrel/F_mu/fundamental.v

+From iris_examples.logrel.F_mu Require Export logrel.
+From iris.program_logic Require Import lifting.
+From iris.proofmode Require Import tactics.
+From iris_examples.logrel.F_mu Require Import rules.
+From iris.base_logic Require Export big_op.
+
+Definition log_typed `{irisG F_mu_lang Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs,
+  env_Persistent Δ →
+  ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
+Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
+
+Section fundamental.
+  Context `{irisG F_mu_lang Σ}.
+
+  Notation D := (valC -n> iProp Σ).
+
+  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
+    iApply (wp_bind (fill[ctx]));
+    iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
+    iIntros (v) Hv.
+
+  Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ.
+  Proof.
+    induction 1; iIntros (Δ vs HΔ) "#HΓ"; cbn.
+    - (* var *)
+      iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
+      rewrite /env_subst. simplify_option_eq. by iApply wp_value.
+    - (* unit *) by iApply wp_value.
+    - (* pair *)
+      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHtyped1.
+      smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
+      iApply wp_value; eauto 10.
+    - (* fst *)
+      smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
+      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
+      simpl. iApply wp_pure_step_later; auto. by iApply wp_value.
+    - (* snd *)
+      smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
+      iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
+      simpl. iApply wp_pure_step_later; eauto. by iApply wp_value.
+    - (* injl *)
+      smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
+      iApply wp_value; eauto.
+    - (* injr *)
+      smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn.
+      iApply wp_value; eauto.
+    - (* case *)
+      smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn.
+      iDestruct (interp_env_length with "HΓ") as %?.
+      iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as (w) "[% Hw]"; simplify_eq/=.
+      + iApply wp_pure_step_later; auto; asimpl. iNext.
+        erewrite typed_subst_head_simpl by naive_solver.
+        iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+      + iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
+        erewrite typed_subst_head_simpl by naive_solver.
+        iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
+    - (* lam *)
+      iApply wp_value; simpl; iAlways; iIntros (w) "#Hw".
+      iDestruct (interp_env_length with "HΓ") as %?.
+      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
+      asimpl. erewrite typed_subst_head_simpl by naive_solver.
+      iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
+    - (* app *)
+      smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
+      smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
+      iApply wp_mono; [|iApply "Hv"]; auto.
+    - (* TLam *)
+      iApply wp_value; simpl.
+      iAlways; iIntros (τi) "%". iApply wp_pure_step_later; auto. iNext.
+      iApply IHtyped. by iApply interp_env_ren.
+    - (* TApp *)
+      smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
+      iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|].
+      iIntros (w) "?". by rewrite interp_subst.
+    - (* Fold *)
+      smart_wp_bind FoldCtx v "#Hv" IHtyped; cbn. iApply wp_value.
+      rewrite /= -interp_subst fixpoint_unfold /=.
+      iAlways; eauto.
+    - (* Unfold *)
+      iApply (wp_bind (fill [UnfoldCtx]));
+        iApply wp_wand_l; iSplitL; [|iApply IHtyped; trivial].
+      iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
+      change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl.
+      iDestruct "Hv" as (w) "#[% Hw]"; subst; simpl.
+      iApply wp_pure_step_later; auto. iApply wp_value; iNext.
+      by rewrite -interp_subst.
+  Qed.
+End fundamental.

theories/logrel/F_mu/lang.v

+From iris.program_logic Require Export language ectx_language ectxi_language.
+From iris_examples.logrel.prelude Require Export base.
+
+Module F_mu.
+  Inductive expr :=
+  | Var (x : var)
+  | Lam (e : {bind 1 of expr})
+  | App (e1 e2 : expr)
+  (* Unit *)
+  | Unit
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
+  (* Recursive Types *)
+  | Fold (e : expr)
+  | Unfold (e : expr)
+  (* Polymorphic Types *)
+  | TLam (e : expr)
+  | TApp (e : expr).
+
+  Instance Ids_expr : Ids expr. derive. Defined.
+  Instance Rename_expr : Rename expr. derive. Defined.
+  Instance Subst_expr : Subst expr. derive. Defined.
+  Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
+
+  Inductive val :=
+  | LamV (e : {bind 1 of expr})
+  | TLamV (e : {bind 1 of expr})
+  | UnitV
+  | PairV (v1 v2 : val)
+  | InjLV (v : val)
+  | InjRV (v : val)
+  | FoldV (v : val).
+
+  Fixpoint of_val (v : val) : expr :=
+    match v with
+    | LamV e => Lam e
+    | TLamV e => TLam e
+    | UnitV => Unit
+    | PairV v1 v2 => Pair (of_val v1) (of_val v2)
+    | InjLV v => InjL (of_val v)
+    | InjRV v => InjR (of_val v)
+    | FoldV v => Fold (of_val v)
+    end.
+  Notation "# v" := (of_val v) (at level 20).
+
+  Fixpoint to_val (e : expr) : option val :=
+    match e with
+    | Lam e => Some (LamV e)
+    | TLam e => Some (TLamV e)
+    | Unit => Some UnitV
+    | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
+    | InjL e => InjLV <$> to_val e
+    | InjR e => InjRV <$> to_val e
+    | Fold e => v ← to_val e; Some (FoldV v)
+    | _ => None
+    end.
+
+  (** Evaluation contexts *)
+  Inductive ectx_item :=
+  | AppLCtx (e2 : expr)
+  | AppRCtx (v1 : val)
+  | TAppCtx
+  | PairLCtx (e2 : expr)
+  | PairRCtx (v1 : val)
+  | FstCtx
+  | SndCtx
+  | InjLCtx
+  | InjRCtx
+  | CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
+  | FoldCtx
+  | UnfoldCtx.
+
+  Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
+    match Ki with
+    | AppLCtx e2 => App e e2
+    | AppRCtx v1 => App (of_val v1) e
+    | TAppCtx => TApp e
+    | PairLCtx e2 => Pair e e2
+    | PairRCtx v1 => Pair (of_val v1) e
+    | FstCtx => Fst e
+    | SndCtx => Snd e
+    | InjLCtx => InjL e
+    | InjRCtx => InjR e
+    | CaseCtx e1 e2 => Case e e1 e2
+    | FoldCtx => Fold e
+    | UnfoldCtx => Unfold e
+    end.
+
+  Definition state : Type := ().
+
+  Inductive head_step : expr → state → expr → state → list expr → Prop :=
+  (* β *)
+  | BetaS e1 e2 v2 σ :
+      to_val e2 = Some v2 →
+      head_step (App (Lam e1) e2) σ e1.[e2/] σ []
+  (* Products *)
+  | FstS e1 v1 e2 v2 σ :
+      to_val e1 = Some v1 → to_val e2 = Some v2 →
+      head_step (Fst (Pair e1 e2)) σ e1 σ []
+  | SndS e1 v1 e2 v2 σ :
+      to_val e1 = Some v1 → to_val e2 = Some v2 →
+      head_step (Snd (Pair e1 e2)) σ e2 σ []
+  (* Sums *)
+  | CaseLS e0 v0 e1 e2 σ :
+      to_val e0 = Some v0 →
+      head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ []
+  | CaseRS e0 v0 e1 e2 σ :
+      to_val e0 = Some v0 →
+      head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ []
+  (* Recursive Types *)
+  | Unfold_Fold e v σ :
+      to_val e = Some v →
+      head_step (Unfold (Fold e)) σ e σ []
+  (* Polymorphic Types *)
+  | TBeta e σ :
+      head_step (TApp (TLam e)) σ e σ [].
+
+  (** Basic properties about the language *)
+  Lemma to_of_val v : to_val (of_val v) = Some v.
+  Proof. by induction v; simplify_option_eq. Qed.
+
+  Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+  Proof.
+    revert v; induction e; intros; simplify_option_eq; auto with f_equal.
+  Qed.
+
+  Instance of_val_inj : Inj (=) (=) of_val.
+  Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+
+  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.
+
+  Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+  Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.
+
+  Lemma val_stuck e1 σ1 e2 σ2 ef :
+    head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+  Proof. destruct 1; naive_solver. Qed.
+
+  Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
+    head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
+  Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. 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.
+    destruct Ki1, Ki2; intros; try discriminate; simplify_eq;
+    repeat match goal with
+           | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
+           end; auto.
+  Qed.
+
+  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 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.
+
+  Canonical Structure stateC := leibnizC state.
+  Canonical Structure valC := leibnizC val.
+  Canonical Structure exprC := leibnizC expr.
+End F_mu.
+
+(** Language *)
+Canonical Structure F_mu_ectxi_lang := EctxiLanguage F_mu.lang_mixin.
+Canonical Structure F_mu_ectx_lang := EctxLanguageOfEctxi F_mu_ectxi_lang.
+Canonical Structure F_mu_lang := LanguageOfEctx F_mu_ectx_lang.
+
+Export F_mu.
+
+Hint Extern 20 (PureExec _ _ _) => progress simpl : typeclass_instances.
+
+Hint Extern 5 (IntoVal _ _) => eapply to_of_val : typeclass_instances.
+Hint Extern 10 (IntoVal _ _) =>
+  rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
+
+Hint Extern 5 (AsVal _) => eexists; eapply to_of_val : typeclass_instances.
+Hint Extern 10 (AsVal _) =>
+  eexists; rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
\ No newline at end of file

theories/logrel/F_mu/logrel.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris_examples.logrel.F_mu Require Export lang typing.
+From iris.algebra Require Import list.
+From iris.base_logic Require Import big_op.
+Import uPred.
+
+(** interp : is a unary logical relation. *)
+Section logrel.
+  Context `{irisG F_mu_lang Σ}.
+  Notation D := (valC -n> iProp Σ).
+  Implicit Types τi : D.
+  Implicit Types Δ : listC D.
+  Implicit Types interp : listC D → D.
+
+  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
+    from_option id (cconst True)%I (Δ !! x).
+  Solve Obligations with solve_proper_alt.
+
+  Definition interp_unit : listC D -n> D := λne Δ w, (⌜w = UnitV⌝)%I.
+
+  Program Definition interp_prod
+      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+    (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I.
+  Solve Obligations with repeat intros ?; simpl; solve_proper.
+
+  Program Definition interp_sum
+      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+    ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I.
+  Solve Obligations with repeat intros ?; simpl; solve_proper.
+
+  Program Definition interp_arrow
+      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
+    (□ ∀ v, interp1 Δ v → WP App (# w) (# v) {{ interp2 Δ }})%I.
+  Solve Obligations with repeat intros ?; simpl; solve_proper.
+
+  Program Definition interp_forall
+      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
+    (□ ∀ τi : D,
+      ⌜∀ v, Persistent (τi v)⌝ → WP TApp (# w) {{ interp (τi :: Δ) }})%I.
+  Solve Obligations with repeat intros ?; simpl; solve_proper.
+
+  Definition interp_rec1
+      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
+    (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I.
+
+  Global Instance interp_rec1_contractive
+    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
+  Proof. by solve_contractive. Qed.
+
+  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
+    fixpoint (interp_rec1 interp Δ).
+  Next Obligation.
+    intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
+  Qed.
+
+  Fixpoint interp (τ : type) : listC D -n> D :=
+    match τ return _ with
+    | TUnit => interp_unit
+    | TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
+    | TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2)
+    | TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
+    | TVar x => ctx_lookup x
+    | TForall τ' => interp_forall (interp τ')
+    | TRec τ' => interp_rec (interp τ')
+    end%I.
+  Notation "⟦ τ ⟧" := (interp τ).
+
+  Definition interp_env (Γ : list type)
+      (Δ : listC D) (vs : list val) : iProp Σ :=
+    (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
+  Notation "⟦ Γ ⟧*" := (interp_env Γ).
+
+  Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
+    WP e {{ ⟦ τ ⟧ Δ }}%I.
+
+  Class env_Persistent Δ :=
+    ctx_persistent : Forall (λ τi, ∀ v, Persistent (τi v)) Δ.
+  Global Instance ctx_persistent_nil : env_Persistent [].
+  Proof. by constructor. Qed.
+  Global Instance ctx_persistent_cons τi Δ :
+    (∀ v, Persistent (τi v)) → env_Persistent Δ → env_Persistent (τi :: Δ).
+  Proof. by constructor. Qed.
+  Global Instance ctx_persistent_lookup Δ x v :
+    env_Persistent Δ → Persistent (ctx_lookup x Δ v).
+  Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
+  Global Instance interp_persistent τ Δ v :
+    env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v) := _.
+  Proof.
+    revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
+    rewrite /Persistent /interp_rec fixpoint_unfold /interp_rec1 /=.
+    by apply persistently_intro'.
+  Qed.
+  Global Instance interp_env_base_persistent Δ Γ vs :
+  env_Persistent Δ → TCForall Persistent (zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs).
+  Proof.
+    intros HΔ. revert vs.
+    induction Γ => vs; simpl; destruct vs; constructor; apply _.
+  Qed.
+  Global Instance interp_env_persistent Γ Δ vs :
+    env_Persistent Δ → Persistent (⟦ Γ ⟧* Δ vs) := _.
+
+  Lemma interp_weaken Δ1 Π Δ2 τ :
+    ⟦ τ.[upn (length Δ1) (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2)
+    ≡ ⟦ τ ⟧ (Δ1 ++ Δ2).
+  Proof.
+    revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
+    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
+    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
+    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
+    - apply fixpoint_proper=> τi w /=.
+      properness; auto. apply (IHτ (_ :: _)).
+    - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
+      { by rewrite !lookup_app_l. }
+      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
+    - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
+  Qed.
+
+  Lemma interp_subst_up Δ1 Δ2 τ τ' :
+    ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2)
+    ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
+  Proof.
+    revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl.
+    - done.
+    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
+    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
+    - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
+    - apply fixpoint_proper=> τi w /=.
+      properness; auto. apply (IHτ (_ :: _)).
+    - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
+      { by rewrite !lookup_app_l. }
+      rewrite !lookup_app_r; [|lia ..].
+      destruct (x - length Δ1) as [|n] eqn:?; simpl.
+      { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
+      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. 
+    - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
+  Qed.
+
+  Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
+  Proof. apply (interp_subst_up []). Qed.
+
+  Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ ⌜length Γ = length vs⌝.
+  Proof. by iIntros "[% ?]". Qed.
+
+  Lemma interp_env_Some_l Δ Γ vs x τ :
+    Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, ⌜vs !! x = Some v⌝ ∧ ⟦ τ ⟧ Δ v.
+  Proof.
+    iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
+    destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
+    { by rewrite -Hlen; apply lookup_lt_Some with τ. }
+    iExists v; iSplit. done. iApply (big_sepL_elem_of with "HΓ").
+    apply elem_of_list_lookup_2 with x.
+    rewrite lookup_zip_with; by simplify_option_eq.
+  Qed.
+
+  Lemma interp_env_nil Δ : (⟦ [] ⟧* Δ [])%I.
+  Proof. iSplit; rewrite ?zip_with_nil_r; auto. Qed.
+  Lemma interp_env_cons Δ Γ vs τ v :
+    ⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
+  Proof.
+    rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜(_ = _)⌝%I) -assoc.
+    by apply sep_proper; [apply pure_proper; omega|].
+  Qed.
+
+  Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
+    ⟦ subst (ren (+1)) <$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs.
+  Proof.
+    apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
+    revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
+    apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
+  Qed.
+End logrel.
+
+Notation "⟦ τ ⟧" := (interp τ).
+Notation "⟦ τ ⟧ₑ" := (interp_expr τ).
+Notation "⟦ Γ ⟧*" := (interp_env Γ).

theories/logrel/F_mu/rules.v

+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ectx_lifting.
+From iris_examples.logrel.F_mu Require Export lang.
+From stdpp Require Import fin_maps.
+
+Section lang_rules.
+  Context `{irisG F_mu_lang Σ}.
+  Implicit Types e : expr.
+
+  Ltac inv_head_step :=
+    repeat match goal with
+    | H : to_val _ = Some _ |- _ => apply of_to_val in H
+    | H : head_step ?e _ _ _ _ |- _ =>
+       try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
+       and can thus better be avoided. *)
+       inversion H; subst; clear H
+    end.
+
+  Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+
+  Local Hint Constructors head_step.
+  Local Hint Resolve to_of_val.
+
+  Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
+  Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
+  Local Ltac solve_pure_exec :=
+    unfold IntoVal, AsVal in *; subst;
+    repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
+    apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+
+  Global Instance pure_lam e1 e2 `{!AsVal e2} :
+    PureExec True (App (Lam e1) e2) e1.[e2 /].
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_tlam e : PureExec True (TApp (TLam e)) e.
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_fold e `{!AsVal e}:
+    PureExec True (Unfold (Fold e)) e.
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_fst e1 e2 `{!AsVal e1, !AsVal e2} :
+    PureExec True (Fst (Pair e1 e2)) e1.
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_snd e1 e2 `{!AsVal e1, !AsVal e2} :
+    PureExec True (Snd (Pair e1 e2)) e2.
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_case_inl e0 e1 e2 `{!AsVal e0}:
+    PureExec True (Case (InjL e0) e1 e2) e1.[e0/].
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_case_inr e0 e1 e2 `{!AsVal e0}:
+    PureExec True (Case (InjR e0) e1 e2) e2.[e0/].
+  Proof. solve_pure_exec. Qed.
+
+End lang_rules.