release exercise 06

_CoqProject

@@ -51,6 +51,16 @@ theories/type_systems/systemf/binary_logrel.v
 theories/type_systems/systemf/binary_logrel_sol.v
 theories/type_systems/systemf/existential_invariants.v
 
+# SystemF-Mu
+theories/type_systems/systemf_mu/lang.v
+theories/type_systems/systemf_mu/notation.v
+theories/type_systems/systemf_mu/types.v
+theories/type_systems/systemf_mu/tactics.v
+theories/type_systems/systemf_mu/pure.v
+theories/type_systems/systemf_mu/untyped_encoding.v
+theories/type_systems/systemf_mu/parallel_subst.v
+theories/type_systems/systemf_mu/logrel.v
+
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
 #theories/type_systems/warmup/warmup_sol.v
@@ -66,3 +76,4 @@ theories/type_systems/systemf/existential_invariants.v
 #theories/type_systems/systemf/exercises04_sol.v
 #theories/type_systems/systemf/exercises05.v
 #theories/type_systems/systemf/exercises05_sol.v
+#theories/type_systems/systemf_mu/exercises06.v

theories/type_systems/systemf_mu/exercises06.v

@@ -0,0 +1,202 @@
+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, #0). (* TODO *)
+
+  Definition Rec (t: expr): val :=
+    λ: x, rec_body t. (* TODO *)
+
+  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_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.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  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.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  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.
+    (* TODO: exercise *)
+  Admitted.
+
+
+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.
+  (* TODO: exercise *)
+Admitted.
+
+
+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.
+  (* TODO: exercise *)
+Admitted.
+
+
+(** ** Exercise 1: Encode arithmetic expressions *)
+
+Definition aexpr : type := #0 (* TODO *).
+
+Definition num_val (v : val) : val := #0 (* TODO *).
+Definition num_expr (e : expr) : expr := #0 (* TODO *).
+
+Definition plus_val (v1 v2 : val) : val := #0 (* TODO *).
+Definition plus_expr (e1 e2 : expr) : expr := #0 (* TODO *).
+
+Definition mul_val (v1 v2 : val) : val := #0 (* TODO *).
+Definition mul_expr (e1 e2 : expr) : expr := #0 (* TODO *).
+
+Lemma num_expr_typed n Γ e :
+  TY n; Γ ⊢ e : Int →
+  TY n; Γ ⊢ num_expr e : aexpr.
+Proof.
+  intros. solve_typing.
+  (* TODO: exercise *)
+Admitted.
+
+
+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.*)
+  (* TODO: exercise *)
+Admitted.
+
+
+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.*)
+  (* TODO: exercise *)
+Admitted.
+
+
+Definition eval_aexpr : val :=
+  #0. (* TODO *)
+
+Lemma eval_aexpr_typed Γ n :
+  TY n; Γ ⊢ eval_aexpr : (aexpr → Int).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** 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 :=
+  #0 (* TODO *)
+  .
+
+
+
+Lemma mylist_impl_sem_typed A :
+  type_wf 0 A →
+  ∀ k, 𝒱 (list_t A) δ_any k mylist_impl.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+

theories/type_systems/systemf_mu/lang.v

@@ -0,0 +1,729 @@
+From stdpp Require Export binders strings.
+From iris.prelude Require Import options.
+From semantics.lib Require Export maps.
+
+Declare Scope expr_scope.
+Declare Scope val_scope.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+
+(** Expressions and vals. *)
+Inductive base_lit : Set :=
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
+Inductive un_op : Set :=
+  | NegOp | MinusUnOp.
+Inductive bin_op : Set :=
+  | PlusOp | MinusOp | MultOp (* Arithmetic *)
+  | LtOp | LeOp | EqOp. (* Comparison *)
+
+
+Inductive expr :=
+  | Lit (l : base_lit)
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Lam (x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | UnOp (op : un_op) (e : expr)
+  | BinOp (op : bin_op) (e1 e2 : expr)
+  | If (e0 e1 e2 : expr)
+  (* Polymorphism *)
+  | TApp (e : expr)
+  | TLam (e : expr)
+  | Pack (e : expr)
+  | Unpack (x : binder) (e1 e2 : expr)
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr)
+  (* Isorecursive types *)
+  | Roll (e : expr)
+  | Unroll (e : expr)
+.
+
+Bind Scope expr_scope with expr.
+
+Inductive val :=
+  | LitV (l : base_lit)
+  | LamV (x : binder) (e : expr)
+  | TLamV (e : expr)
+  | PackV (v : val)
+  | PairV (v1 v2 : val)
+  | InjLV (v : val)
+  | InjRV (v : val)
+  | RollV (v : val)
+.
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+  match v with
+  | LitV l => Lit l
+  | LamV x e => Lam x e
+  | TLamV e => TLam e
+  | PackV v => Pack (of_val v)
+  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
+  | InjLV v => InjL (of_val v)
+  | InjRV v => InjR (of_val v)
+  | RollV v => Roll (of_val v)
+  end.
+
+Fixpoint to_val (e : expr) : option val :=
+  match e with
+  | Lit l => Some $ LitV l
+  | Lam x e => Some (LamV x e)
+  | TLam e => Some (TLamV e)
+  | Pack e =>
+     to_val e ≫= (λ v, Some $ PackV v)
+  | Pair e1 e2 =>
+    to_val e1 ≫= (λ v1, to_val e2 ≫= (λ v2, Some $ PairV v1 v2))
+  | InjL e => to_val e ≫= (λ v, Some $ InjLV v)
+  | InjR e => to_val e ≫= (λ v, Some $ InjRV v)
+  | Roll e => to_val e ≫= (λ v, Some $ RollV v)
+  | _ => None
+  end.
+
+(** Equality and other typeclass stuff *)
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof.
+  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
+Qed.
+
+Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+Proof.
+  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
+Qed.
+
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
+
+(** structural computational version *)
+Fixpoint is_val (e : expr) : Prop :=
+  match e with
+  | Lit l => True
+  | Lam x e => True
+  | TLam e => True
+  | Pack e => is_val e
+  | Pair e1 e2 => is_val e1 ∧ is_val e2
+  | InjL e => is_val e
+  | InjR e => is_val e
+  | Roll e => is_val e
+  | _ => False
+  end.
+Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
+Proof.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try naive_solver.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - rewrite IH. intros (v & ->). eauto.
+Qed.
+
+Global Instance base_lit_eq_dec : EqDecision base_lit.
+Proof. solve_decision. Defined.
+Global Instance un_op_eq_dec : EqDecision un_op.
+Proof. solve_decision. Defined.
+Global Instance bin_op_eq_dec : EqDecision bin_op.
+Proof. solve_decision. Defined.
+
+
+(** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Lit _ => e
+  | Var y => if decide (x = y) then es else Var y
+  | Lam y e =>
+      Lam y $ if decide (BNamed x = y) then e else subst x es e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | TApp e => TApp (subst x es e)
+  | TLam e => TLam (subst x es e)
+  | Pack e => Pack (subst x es e)
+  | Unpack y e1 e2 => Unpack y (subst x es e1) (if decide (BNamed x = y) then e2 else subst x es e2)
+  | UnOp op e => UnOp op (subst x es e)
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
+  | Roll e => Roll (subst x es e)
+  | Unroll e => Unroll (subst x es e)
+  end.
+
+Definition subst' (mx : binder) (es : expr) : expr → expr :=
+  match mx with BNamed x => subst x es | BAnon => id end.
+
+(** The stepping relation *)
+Definition un_op_eval (op : un_op) (v : val) : option val :=
+  match op, v with
+  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
+  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
+  | _, _ => None
+  end.
+
+Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
+  match op with
+  | PlusOp => Some $ LitInt (n1 + n2)
+  | MinusOp => Some $ LitInt (n1 - n2)
+  | MultOp => Some $ LitInt (n1 * n2)
+  | LtOp => Some $ LitBool (bool_decide (n1 < n2))
+  | LeOp => Some $ LitBool (bool_decide (n1 ≤ n2))
+  | EqOp => Some $ LitBool (bool_decide (n1 = n2))
+  end%Z.
+
+Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
+  match v1, v2 with
+  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
+  | _, _ => None
+  end.
+
+Inductive base_step : expr → expr → Prop :=
+  | BetaS x e1 e2 e' :
+     is_val e2 →
+     e' = subst' x e2 e1 →
+     base_step (App (Lam x e1) e2) e'
+  | TBetaS e1 :
+      base_step (TApp (TLam e1)) e1
+  | UnpackS e1 e2 e' x :
+      is_val e1 →
+      e' = subst' x e1 e2 →
+      base_step (Unpack x (Pack e1) e2) e'
+  | UnOpS op e v v' :
+     to_val e = Some v →
+     un_op_eval op v = Some v' →
+     base_step (UnOp op e) (of_val v')
+  | BinOpS op e1 v1 e2 v2 v' :
+     to_val e1 = Some v1 →
+     to_val e2 = Some v2 →
+     bin_op_eval op v1 v2 = Some v' →
+     base_step (BinOp op e1 e2) (of_val v')
+  | IfTrueS e1 e2 :
+     base_step (If (Lit $ LitBool true) e1 e2) e1
+  | IfFalseS e1 e2 :
+     base_step (If (Lit $ LitBool false) e1 e2) e2
+  | FstS e1 e2 :
+     is_val e1 →
+     is_val e2 →
+     base_step (Fst (Pair e1 e2)) e1
+  | SndS e1 e2 :
+     is_val e1 →
+     is_val e2 →
+     base_step (Snd (Pair e1 e2)) e2
+  | CaseLS e e1 e2 :
+     is_val e →
+     base_step (Case (InjL e) e1 e2) (App e1 e)
+  | CaseRS e e1 e2 :
+     is_val e →
+     base_step (Case (InjR e) e1 e2) (App e2 e)
+  | UnrollS e :
+      is_val e →
+      base_step (Unroll (Roll e)) e
+.
+
+(* Misc *)
+Lemma is_val_of_val v : is_val (of_val v).
+Proof. apply is_val_spec. rewrite to_of_val. eauto. Qed.
+
+(** If [e1] makes a base step to a value under some state [σ1] then any base
+ step from [e1] under any other state [σ1'] must necessarily be to a value. *)
+Lemma base_step_to_val e1 e2 e2' :
+  base_step e1 e2 →
+  base_step e1 e2' → is_Some (to_val e2) → is_Some (to_val e2').
+Proof. destruct 1; inversion 1; naive_solver. Qed.
+
+(** We define evaluation contexts *)
+(** In contrast to before, we formalize contexts differently in a non-recursive way.
+  Evaluation contexts are now lists of evaluation context items, and we specify how to
+  plug these items together when filling the context.
+  For instance:
+   - HoleCtx becomes [], the empty list of context items
+   - e1 ●  becomes [AppRCtx e1]
+   - e1 (● + v2) becomes [PlusLCtx v2; AppRCtx e1]
+ *)
+Inductive ectx_item :=
+  | AppLCtx (v2 : val)
+  | AppRCtx (e1 : expr)
+  | TAppCtx
+  | PackCtx
+  | UnpackCtx (x : binder) (e2 : expr)
+  | UnOpCtx (op : un_op)
+  | BinOpLCtx (op : bin_op) (v2 : val)
+  | BinOpRCtx (op : bin_op) (e1 : expr)
+  | IfCtx (e1 e2 : expr)
+  | PairLCtx (v2 : val)
+  | PairRCtx (e1 : expr)
+  | FstCtx
+  | SndCtx
+  | InjLCtx
+  | InjRCtx
+  | CaseCtx (e1 : expr) (e2 : expr)
+  | UnrollCtx
+  | RollCtx
+.
+
+Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
+  match Ki with
+  | AppLCtx v2 => App e (of_val v2)
+  | AppRCtx e1 => App e1 e
+  | TAppCtx => TApp e
+  | PackCtx => Pack e
+  | UnpackCtx x e2 => Unpack x e e2
+  | UnOpCtx op => UnOp op e
+  | BinOpLCtx op v2 => BinOp op e (of_val v2)
+  | BinOpRCtx op e1 => BinOp op e1 e
+  | IfCtx e1 e2 => If e e1 e2
+  | PairLCtx v2 => Pair e (of_val v2)
+  | PairRCtx e1 => Pair e1 e
+  | FstCtx => Fst e
+  | SndCtx => Snd e
+  | InjLCtx => InjL e
+  | InjRCtx => InjR e
+  | CaseCtx e1 e2 => Case e e1 e2
+  | UnrollCtx => Unroll e
+  | RollCtx => Roll e
+  end.
+(* The main [fill] operation is defined below. *)
+
+(** Basic properties about the language *)
+Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
+
+Lemma fill_item_val Ki e :
+  is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
+
+Lemma val_base_stuck e1 e2 : base_step e1 e2 → to_val e1 = None.
+Proof. destruct 1; naive_solver. Qed.
+
+Lemma of_val_lit v l :
+  of_val v = (Lit l) → v = LitV l.
+Proof. destruct v; simpl; inversion 1; done. Qed.
+Lemma of_val_pair_inv (v v1 v2 : val) :
+  of_val v = Pair (of_val v1) (of_val v2) → v = PairV v1 v2.
+Proof.
+  destruct v; simpl; inversion 1.
+  apply of_val_inj in H1. apply of_val_inj in H2. subst; done.
+Qed.
+Lemma of_val_injl_inv (v v' : val) :
+  of_val v = InjL (of_val v') → v = InjLV v'.
+Proof.
+  destruct v; simpl; inversion 1.
+  apply of_val_inj in H1. subst; done.
+Qed.
+Lemma of_val_injr_inv (v v' : val) :
+  of_val v = InjR (of_val v') → v = InjRV v'.
+Proof.
+  destruct v; simpl; inversion 1.
+  apply of_val_inj in H1. subst; done.
+Qed.
+Ltac simplify_val :=
+  repeat match goal with
+  | H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
+  | H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
+  | H: to_val ?e = ?v |- _ => is_var e; specialize (of_to_val _ _ H); intros <-; clear H
+  | H: of_val ?v = Lit ?l |- _ => is_var v; specialize (of_val_lit _ _ H); intros ->; clear H
+  | |- context[to_val (of_val ?e)] => rewrite to_of_val
+  end.
+
+Lemma base_ectxi_step_val Ki e e2 :
+  base_step (fill_item Ki e) e2 → is_Some (to_val e).
+Proof.
+  revert e2. induction Ki; inversion_clear 1; simplify_option_eq; simplify_val; 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.
+  revert Ki1. induction Ki2; intros Ki1; induction Ki1; try naive_solver eauto with f_equal.
+  all: intros ?? Heq; injection Heq; intros ??; simplify_eq; simplify_val; naive_solver.
+Qed.
+
+Section contexts.
+  Notation ectx := (list ectx_item).
+  Definition empty_ectx : ectx := [].
+  Definition comp_ectx : ectx → ectx → ectx := flip (++).
+
+  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.
+  Lemma fill_empty e : fill empty_ectx e = e.
+  Proof. done. Qed.
+  Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+  Proof. unfold fill, comp_ectx; simpl. by rewrite foldl_app. Qed.
+  Global Instance fill_inj K : Inj (=) (=) (fill K).
+  Proof. induction K as [|Ki K IH]; unfold Inj; naive_solver. Qed.
+
+  Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+  Proof.
+    induction K as [|Ki K IH] in e |-*; [ done |]. by intros ?%IH%fill_item_val.
+  Qed.
+  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.
+
+End contexts.
+
+(** Contextual steps *)
+Inductive contextual_step (e1 : expr) (e2 : expr) : Prop :=
+  Ectx_step K e1' e2' :
+    e1 = fill K e1' → e2 = fill K e2' →
+    base_step e1' e2' → contextual_step e1 e2.
+
+
+Lemma base_contextual_step e1 e2 :
+  base_step e1 e2 → contextual_step e1 e2.
+Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
+
+Lemma fill_contextual_step K e1 e2 :
+  contextual_step e1 e2 → contextual_step (fill K e1) (fill K e2).
+Proof.
+  destruct 1 as [K' e1' e2' -> ->].
+  rewrite !fill_comp. by econstructor.
+Qed.
+
+(** *** closedness *)
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ X)
+  | Lam x e => is_closed (x :b: X) e
+  | Unpack x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
+  | Lit _ => true
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | TApp e | TLam e | Pack e | Roll e | Unroll e => is_closed X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 => is_closed X e1 && is_closed X e2
+  |  If e0 e1 e2 | Case e0 e1 e2 =>
+   is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+
+(** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
+Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+Proof. unfold closed. apply _. Qed.
+#[export] Instance closed_dec X e : Decision (closed X e).
+Proof. unfold closed. apply _. Defined.
+
+(** closed expressions *)
+Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
+Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
+
+Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
+Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
+
+Lemma is_closed_subst X e x es :
+  is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
+Proof.
+  intros ?.
+  induction e in X |-*; simpl; intros ?; destruct_and?; split_and?; simplify_option_eq;
+    try match goal with
+    | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
+    end; eauto using is_closed_weaken with set_solver.
+Qed.
+Lemma is_closed_do_subst' X e x es :
+  is_closed [] es → is_closed (x :b: X) e → is_closed X (subst' x es e).
+Proof. destruct x; eauto using is_closed_subst. Qed.
+
+Lemma closed_is_closed X e :
+  is_closed X e = true ↔ closed X e.
+Proof.
+  unfold closed. split.
+  - apply Is_true_eq_left.
+  - apply Is_true_eq_true.
+Qed.
+
+(** Substitution lemmas *)
+Lemma subst_is_closed X e x es : is_closed X e → x ∉ X → subst x es e = e.
+Proof.
+  induction e in X |-*; simpl; rewrite ?bool_decide_spec, ?andb_True; intros ??;
+    repeat case_decide; simplify_eq; simpl; f_equal; intuition eauto with set_solver.
+Qed.
+
+Lemma subst_is_closed_nil e x es : is_closed [] e → subst x es e = e.
+Proof. intros. apply subst_is_closed with []; set_solver. Qed.
+Lemma subst'_is_closed_nil e x es : is_closed [] e → subst' x es e = e.
+Proof. intros. destruct x as [ | x]. { done. } by apply subst_is_closed_nil. Qed.
+
+(** ** More on the contextual semantics *)
+
+Definition base_reducible (e : expr) :=
+  ∃ e', base_step e e'.
+Definition base_irreducible (e : expr) :=
+  ∀ e', ¬base_step e e'.
+Definition base_stuck (e : expr) :=
+  to_val e = None ∧ base_irreducible e.
+
+(** Given a base redex [e1_redex] somewhere in a term, and another
+    decomposition of the same term into [fill K' e1'] such that [e1'] is not
+    a value, then the base redex context is [e1']'s context [K'] filled with
+    another context [K''].  In particular, this implies [e1 = fill K''
+    e1_redex] by [fill_inj], i.e., [e1]' contains the base redex.)
+ *)
+Lemma step_by_val K' K_redex e1' e1_redex e2 :
+    fill K' e1' = fill K_redex e1_redex →
+    to_val e1' = None →
+    base_step e1_redex e2 →
+    ∃ K'', K_redex = comp_ectx K' K''.
+Proof.
+  rename K' into K. rename K_redex into K'.
+  rename e1' into e1. rename e1_redex into e1'.
+  intros Hfill Hred Hstep; revert K' Hfill.
+  induction K as [|Ki K IH] using rev_ind; simpl; intros K' Hfill; eauto using app_nil_r.
+  destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
+  { rewrite fill_app in Hstep. apply base_ectxi_step_val in Hstep.
+    apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
+  rewrite !fill_app in Hfill; simpl in Hfill.
+  assert (Ki = Ki') as ->.
+  { eapply fill_item_no_val_inj, Hfill.
+    - by apply fill_not_val.
+    - apply fill_not_val. eauto using val_base_stuck.
+  }
+  simplify_eq. destruct (IH K') as [K'' ->]; auto.
+  exists K''. unfold comp_ectx; simpl. rewrite assoc; [done |]. apply _.
+Qed.
+
+(** If [fill K e] takes a base step, then either [e] is a value or [K] is
+    the empty evaluation context. In other words, if [e] is not a value
+    wrapping it in a context does not add new base redex positions. *)
+Lemma base_ectx_step_val K e e2 :
+  base_step (fill K e) e2 → is_Some (to_val e) ∨ K = empty_ectx.
+Proof.
+  destruct K as [|Ki K _] using rev_ind; simpl; [by auto|].
+  rewrite fill_app; simpl.
+  intros ?%base_ectxi_step_val; eauto using fill_val.
+Qed.
+
+(** If a [contextual_step] preserving a surrounding context [K] happens,
+   the reduction happens entirely below the context. *)
+Lemma contextual_step_ectx_inv K e e' :
+  to_val e = None →
+  contextual_step (fill K e) (fill K e') →
+  contextual_step e e'.
+Proof.
+  intros ? Hcontextual.
+  inversion Hcontextual; subst.
+  eapply step_by_val in H as (K'' & Heq); [ | done | done].
+  subst K0.
+  rewrite <-fill_comp in H1. rewrite <-fill_comp in H0.
+  apply fill_inj in H1. apply fill_inj in H0. subst.
+  econstructor; done.
+Qed.
+
+Lemma base_reducible_contextual_step_ectx K e1 e2 :
+  base_reducible e1 →
+  contextual_step (fill K e1) e2 →
+  ∃ e2', e2 = fill K e2' ∧ base_step e1 e2'.
+Proof.
+  intros (e2''&HhstepK) [K' e1' e2' HKe1 -> Hstep].
+  edestruct (step_by_val K) as [K'' ?];
+    eauto using val_base_stuck; simplify_eq/=.
+  rewrite <-fill_comp in HKe1; simplify_eq.
+  exists (fill K'' e2'). rewrite fill_comp; split; [done | ].
+  apply base_ectx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
+  { apply val_base_stuck in Hstep; simplify_eq. }
+  by rewrite !fill_empty.
+Qed.
+
+Lemma base_reducible_contextual_step e1 e2 :
+  base_reducible e1 →
+  contextual_step e1 e2 →
+  base_step e1 e2.
+Proof.
+  intros.
+  edestruct (base_reducible_contextual_step_ectx empty_ectx) as (?&?&?);
+    rewrite ?fill_empty; eauto.
+  by simplify_eq; rewrite fill_empty.
+Qed.
+
+(** *** Reducibility *)
+Definition reducible (e : expr) :=
+    ∃ e', contextual_step e e'.
+Definition irreducible (e : expr) :=
+  ∀ e', ¬contextual_step e e'.
+Definition stuck (e : expr) :=
+  to_val e = None ∧ irreducible e.
+Definition not_stuck (e : expr) :=
+  is_Some (to_val e) ∨ reducible e.
+
+Lemma base_step_not_stuck e e' : base_step e e' → not_stuck e.
+Proof. unfold not_stuck, reducible; simpl. eauto 10 using base_contextual_step. Qed.
+
+Lemma val_stuck e e' : contextual_step e e' → to_val e = None.
+Proof.
+  intros [??? -> -> ?%val_base_stuck].
+  apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
+Qed.
+Lemma not_reducible e : ¬reducible e ↔ irreducible e.
+Proof. unfold reducible, irreducible. naive_solver. Qed.
+Lemma reducible_not_val e : reducible e → to_val e = None.
+Proof. intros (?&?). eauto using val_stuck. Qed.
+Lemma val_irreducible e : is_Some (to_val e) → irreducible e.
+Proof. intros [??] ? ?%val_stuck. by destruct (to_val e). Qed.
+
+Lemma irreducible_fill K e :
+  irreducible (fill K e) → irreducible e.
+Proof.
+  intros Hirred e' Hstep.
+  eapply Hirred. by apply fill_contextual_step.
+Qed.
+
+Lemma base_reducible_reducible e :
+  base_reducible e → reducible e.
+Proof. intros (e' & Hhead). exists e'. by apply base_contextual_step. Qed.
+
+
+(* we derive a few lemmas about contextual steps *)
+Lemma contextual_step_app_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (App e1 e2) (App e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [AppLCtx _]).
+Qed.
+
+Lemma contextual_step_app_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (App e1 e2) (App e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [AppRCtx e1]).
+Qed.
+
+Lemma contextual_step_tapp e e':
+  contextual_step e e' →
+  contextual_step (TApp e) (TApp e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [TAppCtx]).
+Qed.
+
+Lemma contextual_step_pack e e':
+  contextual_step e e' →
+  contextual_step (Pack e) (Pack e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [PackCtx]).
+Qed.
+
+Lemma contextual_step_unpack x e e' e2:
+  contextual_step e e' →
+  contextual_step (Unpack x e e2) (Unpack x e' e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [UnpackCtx x e2]).
+Qed.
+
+Lemma contextual_step_unop op e e':
+  contextual_step e e' →
+  contextual_step (UnOp op e) (UnOp op e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [UnOpCtx op]).
+Qed.
+
+Lemma contextual_step_binop_l op e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (BinOp op e1 e2) (BinOp op e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [BinOpLCtx op v]).
+Qed.
+
+Lemma contextual_step_binop_r op e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (BinOp op e1 e2) (BinOp op e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [BinOpRCtx op e1]).
+Qed.
+
+Lemma contextual_step_if e e' e1 e2:
+  contextual_step e e' →
+  contextual_step (If e e1 e2) (If e' e1 e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [IfCtx e1 e2]).
+Qed.
+
+Lemma contextual_step_pair_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Pair e1 e2) (Pair e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step [PairLCtx v]).
+Qed.
+
+Lemma contextual_step_pair_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Pair e1 e2) (Pair e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [PairRCtx e1]).
+Qed.
+
+
+Lemma contextual_step_fst e e':
+  contextual_step e e' →
+  contextual_step (Fst e) (Fst e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [FstCtx]).
+Qed.
+
+Lemma contextual_step_snd e e':
+  contextual_step e e' →
+  contextual_step (Snd e) (Snd e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [SndCtx]).
+Qed.
+
+Lemma contextual_step_injl e e':
+  contextual_step e e' →
+  contextual_step (InjL e) (InjL e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [InjLCtx]).
+Qed.
+
+Lemma contextual_step_injr e e':
+  contextual_step e e' →
+  contextual_step (InjR e) (InjR e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [InjRCtx]).
+Qed.
+
+Lemma contextual_step_case e e' e1 e2:
+  contextual_step e e' →
+  contextual_step (Case e e1 e2) (Case e' e1 e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step [CaseCtx e1 e2]).
+Qed.
+
+Lemma contextual_step_roll e e':
+  contextual_step e e' →
+  contextual_step (Roll e) (Roll e').
+Proof. by apply (fill_contextual_step [RollCtx]). Qed.
+
+Lemma contextual_step_unroll e e':
+  contextual_step e e' → contextual_step (Unroll e) (Unroll e').
+Proof. by apply (fill_contextual_step [UnrollCtx]). Qed.
+
+
+#[export]
+Hint Resolve
+  contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
+  contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
+  contextual_step_pack contextual_step_pair_l contextual_step_pair_r contextual_step_snd contextual_step_tapp
+  contextual_step_tapp contextual_step_unop contextual_step_unpack contextual_step_roll contextual_step_unroll : core.
+

theories/type_systems/systemf_mu/notation.v

@@ -0,0 +1,97 @@
+From semantics.ts.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/type_systems/systemf_mu/parallel_subst.v

@@ -0,0 +1,275 @@
+From stdpp Require Import prelude.
+From iris Require Import prelude.
+From semantics.lib Require Import facts maps.
+From semantics.ts.systemf_mu Require Import lang.
+
+Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
+  match e with
+  | Lit l => Lit l
+  | Var y => match xs !! y with Some es => es | _ =>  Var y end
+  | App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
+  | Lam x e => Lam x (subst_map (binder_delete x xs) e)
+  | UnOp op e => UnOp op (subst_map xs e)
+  | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
+  | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
+  | TApp e => TApp (subst_map xs e)
+  | TLam e => TLam (subst_map xs e)
+  | Pack e => Pack (subst_map xs e)
+  | Unpack x e1 e2 => Unpack x (subst_map xs e1) (subst_map (binder_delete x xs) e2)
+  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
+  | Fst e => Fst (subst_map xs e)
+  | Snd e => Snd (subst_map xs e)
+  | InjL e => InjL (subst_map xs e)
+  | InjR e => InjR (subst_map xs e)
+  | Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2)
+  | Roll e => Roll (subst_map xs e)
+  | Unroll e => Unroll (subst_map xs e)
+  end.
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  all: destruct x; simpl; [done | by rewrite !delete_empty..].
+Qed.
+
+Lemma subst_map_is_closed X e xs :
+  is_closed X e →
+  (∀ x : string, x ∈ dom xs → x ∉ X) →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed Hd.
+  induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* Var *)
+    apply bool_decide_spec in Hclosed.
+    assert (xs !! x = None) as ->; last done.
+    destruct (xs !! x) as [s | ] eqn:Helem; last done.
+    exfalso; eapply Hd; last apply Hclosed.
+    apply elem_of_dom; eauto.
+  }
+  { (* lambdas *)
+    erewrite IHe; [done | done |].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  8: { (* Unpack *)
+    erewrite IHe1; [ | done | done].
+    erewrite IHe2; [ done | done | ].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+       | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
+       end; done.
+Qed.
+
+Lemma subst_map_subst map x (e e' : expr) :
+  is_closed [] e' →
+  subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
+Proof.
+  intros He'.
+  revert x map; induction e; intros xx map; simpl;
+  try (f_equal; eauto).
+  - case_decide.
+    + simplify_eq/=. rewrite lookup_insert.
+      rewrite (subst_map_is_closed []); [done | apply He' | ].
+      intros ? ?. apply not_elem_of_nil.
+    + rewrite lookup_insert_ne; done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+Qed.
+
+Definition subst_is_closed (X : list string) (map : gmap string expr) :=
+  ∀ x e, map !! x = Some e → closed X e.
+Lemma subst_is_closed_subseteq X map1 map2 :
+  map1 ⊆ map2 → subst_is_closed X map2 → subst_is_closed X map1.
+Proof.
+  intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
+Qed.
+
+Lemma subst_subst_map x es map e :
+  subst_is_closed [] map →
+  subst x es (subst_map (delete x map) e) =
+  subst_map (<[x:=es]>map) e.
+Proof.
+  revert map es x; induction e; intros map v0 xx Hclosed; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (_ !! x) as [rr|] eqn:Helem.
+      * apply Hclosed in Helem.
+        by apply subst_is_closed_nil.
+      * simpl. rewrite decide_False //.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe2.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+Qed.
+
+Lemma subst'_subst_map b (es : expr) map e :
+  subst_is_closed [] map →
+  subst' b es (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b es map) e.
+Proof.
+  destruct b; first done.
+  apply subst_subst_map.
+Qed.
+
+Lemma closed_subst_weaken e map X Y :
+  subst_is_closed [] map →
+  (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
+  closed X e →
+  closed Y (subst_map map e).
+Proof.
+  induction e in X, Y, map |-*; rewrite /closed; simpl; intros Hmclosed Hsub Hcl; first done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* vars *)
+    destruct (map !! x) as [es | ] eqn:Heq.
+    + apply is_closed_weaken_nil. by eapply Hmclosed.
+    + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
+      by apply not_elem_of_dom.
+  }
+  { (* lambdas *)
+    eapply IHe; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  8: { (* unpack *)
+    apply andb_True; split; first naive_solver.
+    eapply IHe2; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+         | |- Is_true (_ && _) => apply andb_True; split
+              end.
+  all: naive_solver.
+Qed.
+
+Lemma subst_is_closed_weaken X1 X2 θ :
+  subst_is_closed X1 θ →
+  X1 ⊆ X2 →
+  subst_is_closed X2 θ.
+Proof.
+  intros Hcl Hincl x e Hlook.
+  eapply is_closed_weaken; last done.
+  by eapply Hcl.
+Qed.
+
+Lemma subst_is_closed_weaken_nil X θ :
+  subst_is_closed [] θ →
+  subst_is_closed X θ.
+Proof.
+  intros; eapply subst_is_closed_weaken; first done.
+  apply list_subseteq_nil.
+Qed.
+
+Lemma subst_is_closed_insert X e f θ :
+  is_closed X e →
+  subst_is_closed X (delete f θ) →
+  subst_is_closed X (<[f := e]> θ).
+Proof.
+  intros Hcl Hcl' x e'.
+  destruct (decide (x = f)) as [<- | ?].
+  - rewrite lookup_insert. intros [= <-]. done.
+  - rewrite lookup_insert_ne; last done.
+    intros Hlook. eapply Hcl'.
+    rewrite lookup_delete_ne; done.
+Qed.
+
+(* NOTE: this is a simplified version of the tactic in tactics.v which
+  suffice for this proof *)
+Ltac simplify_closed :=
+  repeat match goal with
+  | |- closed _ _ => unfold closed; simpl
+  | |- Is_true (_ && _)  => simpl; rewrite !andb_True; split_and!
+  | H : closed _ _ |- _ => unfold closed in H; simpl in H
+  | H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
+  | H : _ ∧ _ |- _ => destruct H
+  end.
+
+Lemma is_closed_subst_map X θ e :
+  subst_is_closed X θ →
+  closed (X ++ elements (dom θ)) e →
+  closed X (subst_map θ e).
+Proof.
+  induction e in X, θ |-*; eauto.
+  all: try solve [intros; simplify_closed; naive_solver].
+  - unfold subst_map.
+    destruct (θ !! x) eqn:Heq.
+    + intros Hcl _. eapply Hcl; done.
+    + intros _ Hcl.
+      apply closed_is_closed in Hcl.
+      apply bool_decide_eq_true in Hcl.
+      apply elem_of_app in Hcl.
+      destruct Hcl as [ | H].
+      * apply closed_is_closed. by apply bool_decide_eq_true.
+      * apply elem_of_elements in H.
+        by apply not_elem_of_dom in Heq.
+  - intros. simplify_closed.
+    eapply IHe.
+    + destruct x as [ | x]; simpl; first done.
+      intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
+      eapply is_closed_weaken; first done.
+      by apply list_subseteq_cons_r.
+    + eapply is_closed_weaken; first done.
+      simpl. destruct x as [ | x]; first done; simpl.
+      apply list_subseteq_cons_l.
+      apply stdpp.sets.elem_of_subseteq.
+      intros y; simpl. rewrite elem_of_cons !elem_of_app.
+      intros [ | Helem]; first naive_solver.
+      destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
+      right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
+      apply elem_of_elements in Helem; done.
+  - intros. simplify_closed. { naive_solver. }
+    (* same proof as for lambda *)
+    eapply IHe2.
+    + destruct x as [ | x]; simpl; first done.
+      intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
+      eapply is_closed_weaken; first done.
+      by apply list_subseteq_cons_r.
+    + eapply is_closed_weaken; first done.
+      simpl. destruct x as [ | x]; first done; simpl.
+      apply list_subseteq_cons_l.
+      apply stdpp.sets.elem_of_subseteq.
+      intros y; simpl. rewrite elem_of_cons !elem_of_app.
+      intros [ | Helem]; first naive_solver.
+      destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
+      right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
+      apply elem_of_elements in Helem; done.
+Qed.

theories/type_systems/systemf_mu/pure.v

@@ -0,0 +1,289 @@
+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.
+  (* TODO: exercise *)
+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.
+  (* TODO: 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/type_systems/systemf_mu/tactics.v

@@ -0,0 +1,84 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export facts maps sets.
+From semantics.ts.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/type_systems/systemf_mu/untyped_encoding.v

@@ -0,0 +1,80 @@
+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.
+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.
+
+Lemma Ω_loops:
+  tc contextual_step Ω Ω.
+Proof.
+  econstructor 2; [|econstructor 1].
+  - rewrite /Ω /ω. eauto.
+  - rewrite /Ω. eauto.
+Qed.
+
+Lemma ω_typed :
+  TY 0; ∅ ⊢ ω : D.
+Proof.
+  solve_typing.
+Qed.
+
+Lemma Ω_typed : TY 0; ∅ ⊢ Ω : D.
+Proof.
+  rewrite /Ω. econstructor.
+  - eapply typed_unroll'; eauto using ω_typed.
+  - eapply ω_typed.
+Qed.