From 4f600972e53c737727a43711bf48c7547b971b7c Mon Sep 17 00:00:00 2001 From: Benjamin Peters Date: Thu, 7 Dec 2023 14:45:52 +0100 Subject: [PATCH] release exercise 07 --- _CoqProject | 14 + .../type_systems/systemf_mu_state/execution.v | 450 +++++ .../systemf_mu_state/exercises07.v | 127 ++ theories/type_systems/systemf_mu_state/lang.v | 858 ++++++++ .../type_systems/systemf_mu_state/locations.v | 46 + .../type_systems/systemf_mu_state/logrel.v | 1738 +++++++++++++++++ .../type_systems/systemf_mu_state/notation.v | 113 ++ .../systemf_mu_state/parallel_subst.v | 279 +++ .../type_systems/systemf_mu_state/tactics.v | 91 + .../type_systems/systemf_mu_state/types.v | 1326 +++++++++++++ 10 files changed, 5042 insertions(+) create mode 100644 theories/type_systems/systemf_mu_state/execution.v create mode 100644 theories/type_systems/systemf_mu_state/exercises07.v create mode 100644 theories/type_systems/systemf_mu_state/lang.v create mode 100644 theories/type_systems/systemf_mu_state/locations.v create mode 100644 theories/type_systems/systemf_mu_state/logrel.v create mode 100644 theories/type_systems/systemf_mu_state/notation.v create mode 100644 theories/type_systems/systemf_mu_state/parallel_subst.v create mode 100644 theories/type_systems/systemf_mu_state/tactics.v create mode 100644 theories/type_systems/systemf_mu_state/types.v diff --git a/_CoqProject b/_CoqProject index c4576c1..e621d45 100644 --- a/_CoqProject +++ b/_CoqProject @@ -57,9 +57,21 @@ 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/pure_sol.v theories/type_systems/systemf_mu/untyped_encoding.v theories/type_systems/systemf_mu/parallel_subst.v theories/type_systems/systemf_mu/logrel.v +theories/type_systems/systemf_mu/logrel_sol.v + +# SystemF + Mu + State +theories/type_systems/systemf_mu_state/locations.v +theories/type_systems/systemf_mu_state/lang.v +theories/type_systems/systemf_mu_state/notation.v +theories/type_systems/systemf_mu_state/types.v +theories/type_systems/systemf_mu_state/tactics.v +theories/type_systems/systemf_mu_state/execution.v +theories/type_systems/systemf_mu_state/parallel_subst.v +theories/type_systems/systemf_mu_state/logrel.v # By removing the # below, you can add the exercise sheets to make #theories/type_systems/warmup/warmup.v @@ -77,3 +89,5 @@ theories/type_systems/systemf_mu/logrel.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_sol.v +#theories/type_systems/systemf_mu_state/exercises07.v diff --git a/theories/type_systems/systemf_mu_state/execution.v b/theories/type_systems/systemf_mu_state/execution.v new file mode 100644 index 0000000..d63a9da --- /dev/null +++ b/theories/type_systems/systemf_mu_state/execution.v @@ -0,0 +1,450 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.systemf_mu_state Require Import lang notation. +(* TODO: everywhere replace the metavar σ for heaps with h *) + +(** ** Deterministic reduction *) + +Record det_step (e1 : expr) (e2 : expr) := { + det_step_safe h : reducible e1 h; + det_step_det e2' h h' : + contextual_step (e1, h) (e2', h') → e2' = e2 ∧ h' = h +}. + +Record det_base_step (e1 e2 : expr) := { + det_base_step_safe h : base_reducible e1 h; + det_base_step_det e2' h h' : + base_step (e1, h) (e2', h') → e2' = e2 ∧ h' = h +}. + +Lemma det_base_step_det_step e1 e2 : det_base_step e1 e2 → det_step e1 e2. +Proof. + intros [Hp1 Hp2]. split. + - intros h. destruct (Hp1 h) as (e2' & h' & ?). + eexists e2', h'. by apply base_contextual_step. + - intros e2' h h' ?%base_reducible_contextual_step; [ | done]. by eapply 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, ?σ2) |- _ => + 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 h e' h' := nsteps contextual_step n (e, h) (e', h') ∧ irreducible e' h'. + +Lemma det_step_red e e' e'' h h'' n : + det_step e e' → + red_nsteps n e h e'' h'' → + 1 ≤ n ∧ red_nsteps (n - 1) e' h e'' h''. +Proof. + intros [Hprog Hstep] Hred. + specialize (Hprog h). + destruct Hred as [Hred Hirred]. + destruct n as [ | n]. + { inversion Hred; subst. + exfalso; eapply not_reducible; done. + } + inversion Hred as [ | ??[e1 h1]? Hstep0]; subst. simpl. + apply Hstep in Hstep0 as [<- <-]. + split; first lia. + replace (n - 0) with n by lia. done. +Qed. + +Lemma contextual_step_red_nsteps n e e' e'' h h' h'': + contextual_step (e, h) (e', h') → + red_nsteps n e' h' e'' h'' → + red_nsteps (S n) e h e'' h''. +Proof. + intros Hstep [Hsteps Hirred]. + split; last done. + by econstructor. +Qed. + +Lemma nsteps_val_inv n v e' h h' : + red_nsteps n (of_val v) h e' h' → n = 0 ∧ e' = of_val v ∧ h' = h. +Proof. + intros [Hred Hirred]; cbn in *. + destruct n as [ | n]. + - inversion Hred; subst. done. + - inversion Hred as [ | ??[e1 h1]]; subst. exfalso. eapply val_irreducible; last done. + rewrite to_of_val. eauto. +Qed. + +Lemma nsteps_val_inv' n v e e' h h' : + to_val e = Some v → + red_nsteps n e h e' h' → n = 0 ∧ e' = of_val v ∧ h' = h. +Proof. intros Ht. rewrite -(of_to_val _ _ Ht). apply nsteps_val_inv. Qed. + +Lemma red_nsteps_fill K k e e' h h' : + red_nsteps k (fill K e) h e' h' → + ∃ j e'' h'', j ≤ k ∧ + red_nsteps j e h e'' h'' ∧ + red_nsteps (k - j) (fill K e'') h'' e' h'. +Proof. + intros [Hsteps Hirred]. + induction k as [ | k IH] in e, e', h, h', Hsteps, Hirred |-*. + - inversion Hsteps; subst. + exists 0, e, h'. split_and!; [done | split | ]. + + constructor. + + by eapply irreducible_fill. + + done. + - inversion Hsteps as [ | n [e1 h1] [e2 h2] [e3 h3] Hstep Hsteps' Heq1 Heq2 Heq3]. subst. + destruct (contextual_ectx_step_case _ _ _ _ _ Hstep) as [(e'' & -> & Hstep') | Hv]. + + apply IH in Hsteps' as (j & e3 & h3 & ? & Hsteps' & Hsteps''); last done. + eexists (S j), _, _. split_and!; [lia | | done ]. + eapply contextual_step_red_nsteps; done. + + exists 0, e, h. split_and!; [ lia | | ]. + * split; [constructor | ]. + apply val_irreducible. by apply is_val_spec. + * simpl. by eapply contextual_step_red_nsteps. +Qed. + +(** * Heap execution lemmas *) +Lemma new_step_inv v e e' σ σ' : + to_val e = Some v → + base_step (New e, σ) (e', σ') → + ∃ l, e' = (Lit $ LitLoc l) ∧ σ' = init_heap l 1 v σ ∧ σ !! l = None. +Proof. + intros <-%of_to_val. + inversion 1; subst. + rewrite to_of_val in H5. injection H5 as [= ->]. + eauto. +Qed. + +Lemma new_nsteps_inv n v e e' σ σ' : + to_val e = Some v → + red_nsteps n (New e) σ e' σ' → + (n = 1 ∧ base_step (New e, σ) (e', σ')). +Proof. + intros <-%of_to_val [Hsteps Hirred%not_reducible]. + inversion Hsteps; subst. + - exfalso; apply Hirred. eapply base_reducible_reducible. eexists _, _. eapply new_fresh. + - destruct y. + eapply base_reducible_contextual_step in H. + 2: { eexists _, _. apply new_fresh. } + inversion H0; subst. + { eauto. } + eapply new_step_inv in H; last apply to_of_val. + destruct H as (l & -> & -> & ?). + destruct y. apply val_stuck in H1. done. +Qed. + +Lemma load_step_inv e v σ e' σ' : + to_val e = Some v → + base_step (Load e, σ) (e', σ') → + ∃ (l : loc) v', v = #l ∧ σ !! l = Some v' ∧ e' = of_val v' ∧ σ' = σ. +Proof. + intros <-%of_to_val. + inversion 1; subst. + symmetry in H0. apply of_val_lit in H0 as ->. + eauto 8. +Qed. + +Definition sub_redexes_are_values (e : expr) := + ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx. + +Lemma contextual_base_reducible e σ : + reducible e σ → sub_redexes_are_values e → base_reducible e σ. +Proof. + intros (e' & σ' & Hstep) ?. inversion Hstep; subst. + assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck. + rewrite fill_empty /base_reducible; eauto. +Qed. + + +Ltac solve_sub_redexes_are_values := + let K := fresh "K" in + let e' := fresh "e'" in + let Heq := fresh "Heq" in + let Hv := fresh "Hv" in + let IH := fresh "IH" in + let Ki := fresh "Ki" in + let Ki' := fresh "Ki'" in + intros K e' Heq Hv; + destruct K as [ | Ki K]; first (done); + exfalso; induction K as [ | Ki' K IH] in e', Ki, Hv, Heq |-*; + [destruct Ki; inversion Heq; subst; simplify_val; cbn in *; congruence + | eapply IH; first (by rewrite Heq); + apply fill_item_no_val; done]. + +Lemma load_nsteps_inv n v e e' σ σ' : + to_val e = Some v → + red_nsteps n (Load e) σ e' σ' → + (n = 0 ∧ σ' = σ ∧ e' = Load e ∧ ¬ reducible (Load e) σ) ∨ + (n = 1 ∧ base_step (Load e, σ) (e', σ')). +Proof. + intros <-%of_to_val [Hsteps Hirred%not_reducible]. + inversion Hsteps; subst. + - by left. + - right. destruct y. + eapply base_reducible_contextual_step in H. + 2: { eapply contextual_base_reducible; [eexists _, _; done | solve_sub_redexes_are_values]. } + inversion H0; subst. + { eauto. } + eapply load_step_inv in H as (l & ? & -> & ? & -> & ->); last apply to_of_val. + destruct y. apply val_stuck in H1. simplify_val. done. +Qed. + +(** useful derived lemma when we know upfront that l satisfies some invariant [P] *) +Lemma load_nsteps_inv' n l e e' σ σ' (P : val → Prop) : + to_val e = Some (LitV $ LitLoc l) → + (∃ v', σ !! l = Some v' ∧ P v') → + red_nsteps n (Load e) σ e' σ' → + ∃ v' : val, n = 1 ∧ e' = v' ∧ σ' = σ ∧ σ !! l = Some v' ∧ P v'. +Proof. + intros <-%of_to_val (v' & Hlook & HP) Hred. + eapply load_nsteps_inv in Hred; last done. + destruct Hred as [(-> & -> & -> & Hnred) | (-> & Hstep)]. + - exfalso; eapply Hnred. eexists v', _. + eapply base_contextual_step. econstructor. done. + - exists v'. split; first done. + eapply load_step_inv in Hstep; last done. + destruct Hstep as (l' & v'' & [= <-] & ? & -> & ->). + split; first by simplify_option_eq. + split; last done. econstructor; done. +Qed. + +Lemma store_step_inv v1 v2 σ e' σ' : + base_step (Store (of_val v1) (of_val v2), σ) (e', σ') → + ∃ (l : loc) v', v1 = #l ∧ σ !! l = Some v' ∧ e' = Lit LitUnit ∧ σ' = <[l := v2]> σ. +Proof. + inversion 1; subst. + symmetry in H0. apply of_val_lit in H0 as ->. + simplify_val. simplify_option_eq. + eauto 8. +Qed. + +Lemma store_nsteps_inv n v1 v2 e' σ σ' : + red_nsteps n (Store (of_val v1) (of_val v2)) σ e' σ' → + (n = 0 ∧ σ' = σ ∧ e' = Store (of_val v1) (of_val v2) ∧ ¬ reducible (Store (of_val v1) (of_val v2)) σ) ∨ + (n = 1 ∧ base_step (Store (of_val v1) (of_val v2), σ) (e', σ')). +Proof. + intros [Hsteps Hirred%not_reducible]. + inversion Hsteps; subst. + - by left. + - right. destruct y. + eapply base_reducible_contextual_step in H. + 2: { eapply contextual_base_reducible; [eexists _, _; done | solve_sub_redexes_are_values]. } + inversion H0; subst. + { eauto. } + apply store_step_inv in H as (l & ? & -> & ? & -> & ->). + destruct y. apply val_stuck in H1. simplify_val. done. +Qed. + +Lemma store_nsteps_inv' n e1 e2 v0 v l e' σ σ' : + to_val e1 = Some (LitV $ LitLoc l) → + to_val e2 = Some v → + σ !! l = Some v0 → + red_nsteps n (Store e1 e2) σ e' σ' → + n = 1 ∧ e' = Lit $ LitUnit ∧ σ' = <[l := v ]> σ. +Proof. + intros <-%of_to_val <-%of_to_val Hlook Hred%store_nsteps_inv. + destruct Hred as [(-> & -> & -> & Hnred) | (-> & Hb)]. + - exfalso; eapply Hnred. + eexists #(), _. + eapply base_contextual_step. econstructor; [done | apply to_of_val ]. + - eapply store_step_inv in Hb. destruct Hb as (l' & v' & [= <-] & Hlook' & -> & ->). + simplify_option_eq. done. +Qed. + +(** Additionally useful stepping lemmas *) +Lemma app_step_r (e1 e2 e2': expr) h h' : + contextual_step (e2, h) (e2', h') → contextual_step (e1 e2, h) (e1 e2', h'). +Proof. by apply (fill_contextual_step [AppRCtx _]). Qed. + +Lemma app_step_l (e1 e1' e2: expr) h h' : + contextual_step (e1, h) (e1', h') → is_val e2 → contextual_step (e1 e2, h) (e1' e2, h'). +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) h : + is_val e' → is_closed [x] e → contextual_step ((λ: x, e)%E e', h) (lang.subst x e' e, h). +Proof. + intros Hval Hclosed. eapply base_contextual_step, BetaS; eauto. +Qed. + +Lemma unroll_roll_step (e: expr) h : + is_val e → contextual_step ((unroll (roll e))%E, h) (e, h). +Proof. + intros ?; by eapply base_contextual_step, UnrollS. +Qed. + +Lemma fill_reducible K e h : + reducible e h → reducible (fill K e) h. +Proof. + intros (e' & h' & Hstep). + exists (fill K e'), h'. eapply fill_contextual_step. done. +Qed. + +Lemma reducible_contextual_step_case K e e' h1 h2 : + contextual_step (fill K e, h1) (e', h2) → + reducible e h1 → + ∃ e'', e' = fill K e'' ∧ contextual_step (e, h1) (e'', h2). +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. +Lemma det_step_store_r e1 e2 e2' : + det_step e2 e2' → + det_step (Store e1 e2)%E (Store e1 e2')%E. +Proof. lift_det [StoreRCtx _]. Qed. +Lemma det_step_store_l e1 e1' e2 : + is_val e2 → + det_step e1 e1' → + det_step (Store e1 e2)%E (Store e1' e2)%E. +Proof. lift_det [StoreLCtx _]. 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 det_step_store_l det_step_store_r : core. + +#[global] +Hint Constructors nsteps : core. + +#[global] +Hint Extern 1 (is_val _) => simpl : core. + +Ltac do_det_step := + match goal with + | |- nsteps det_step _ _ _ => econstructor 2; first do_det_step + | |- det_step _ _ => simpl; solve[eauto 10] + end. diff --git a/theories/type_systems/systemf_mu_state/exercises07.v b/theories/type_systems/systemf_mu_state/exercises07.v new file mode 100644 index 0000000..59c2d19 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/exercises07.v @@ -0,0 +1,127 @@ +From iris Require Import prelude. +From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst tactics execution. + +(** * Exercise Sheet 7 *) + +(** Exercise 1: Stack (LN Exercise 45) *) +(* We use lists to model our stack *) +Section lists. + Context (A : type). + Definition list_type : type := + μ: Unit + (A.[ren (+1)] × #0). + + Definition nil_val : val := + RollV (InjLV (LitV LitUnit)). + Definition cons_val (v : val) (xs : val) : val := + RollV (InjRV (v, xs)). + Definition cons_expr (v : expr) (xs : expr) : expr := + roll (InjR (v, xs)). + + Definition list_case : val := + Λ, λ: "l" "n" "hf", match: unroll "l" with InjL <> => "n" | InjR "h" => "hf" (Fst "h") (Snd "h") end. + + Lemma nil_val_typed Σ n Γ : + type_wf n A → + TY Σ; n; Γ ⊢ nil_val : list_type. + Proof. + intros. solve_typing. + Qed. + + Lemma cons_val_typed Σ n Γ (v xs : val) : + type_wf n A → + TY Σ; n; Γ ⊢ v : A → + TY Σ; n; Γ ⊢ xs : list_type → + TY Σ; n; Γ ⊢ cons_val v xs : list_type. + Proof. + intros. simpl. solve_typing. + Qed. + + Lemma cons_expr_typed Σ n Γ (x xs : expr) : + type_wf n A → + TY Σ; n; Γ ⊢ x : A → + TY Σ; n; Γ ⊢ xs : list_type → + TY Σ; n; Γ ⊢ cons_expr x xs : list_type. + Proof. + intros. simpl. solve_typing. + Qed. + + Lemma list_case_typed Σ n Γ : + type_wf n A → + TY Σ; n; Γ ⊢ list_case : (∀: list_type.[ren (+1)] → #0 → (A.[ren(+1)] → list_type.[ren (+1)] → #0) → #0). + Proof. + intros. simpl. solve_typing. + Qed. +End lists. + +(* The stack interface *) +Definition stack_t A : type := + ∃: ((Unit → #0) (* new *) + × (#0 → A.[ren (+1)] → Unit) (* push *) + × (#0 → Unit + A.[ren (+1)])) (* pop *) + . + +(** We assume an abstract implementation of lists (an example implementation is provided above) *) +Definition list_t (A : type) : type := + ∃: (#0 (* mynil *) + × (A.[ren (+1)] → #0 → #0) (* mycons *) + × (∀: #1 → #0 → (A.[ren (+2)] → #1 → #0) → #0)) (* mylistcase *) + . + +Definition mystack : val := + (* define your stack implementation, assuming "lc" is a list implementation *) + λ: "lc", #0. (* FIXME *) + + +Definition make_mystack : val := + Λ, λ: "lc", + unpack "lc" as "lc" in + #0. (* FIXME *) + +Lemma make_mystack_typed Σ n Γ : + TY Σ; n; Γ ⊢ make_mystack : (∀: list_t #0 → stack_t #0). +Proof. + repeat solve_typing_fast. +Admitted. + + +(** Exercise 2 (LN Exercise 46): Obfuscated code *) +Definition obf_expr : expr := + let: "x" := new (λ: "x", "x" + "x") in + let: "f" := (λ: "g", let: "f" := !"x" in "x" <- "g";; "f" #11) in + "f" (λ: "x", "f" (λ: <>, "x")) + "f" (λ: "x", "x" + #9). + +(* The following contextual lifting lemma will be helpful *) +Lemma rtc_contextual_step_fill K e e' h h' : + rtc contextual_step (e, h) (e', h') → + rtc contextual_step (fill K e, h) (fill K e', h'). +Proof. + remember (e, h) as a eqn:Heqa. remember (e', h') as b eqn:Heqb. + induction 1 as [ | ? c ? Hstep ? IH] in e', h', e, h, Heqa, Heqb |-*; subst. + - simplify_eq. done. + - destruct c as (e1, h1). + econstructor 2. + + apply fill_contextual_step. apply Hstep. + + apply IH; done. +Qed. + +(* You may use the [new_fresh] and [init_heap_singleton] lemmas to allocate locations *) + +Lemma obf_expr_eval : + ∃ h', rtc contextual_step (obf_expr, ∅) (of_val #0 (* FIXME: what is the result? *), h'). +Proof. + eexists. unfold obf_expr. + (* TODO: exercise *) +Admitted. + + + +(** Exercise 4 (LN Exercise 48): Fibonacci *) + + +Definition fibonacci : val := #0. (* FIXME *) + +Lemma fibonacci_typed Σ n Γ : + TY Σ; n; Γ ⊢ fibonacci : (Int → Int). +Proof. + repeat solve_typing_fast. +Admitted. diff --git a/theories/type_systems/systemf_mu_state/lang.v b/theories/type_systems/systemf_mu_state/lang.v new file mode 100644 index 0000000..fc0a055 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/lang.v @@ -0,0 +1,858 @@ +From iris.prelude Require Import prelude. +From stdpp Require Export binders strings. +From semantics.ts.systemf_mu_state Require Export locations. +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 | LitLoc (l : loc). +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) + (* State *) + | Load (e : expr) + | Store (e1 e2 : expr) + | New (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) + | Load e => Load (subst x es e) + | Store e1 e2 => Store (subst x es e1) (subst x es e2) + | New e => New (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. + +Definition heap := gmap loc val. +Fixpoint heap_array (l : loc) (vs : list val) : heap := + match vs with + | [] => ∅ + | v :: vs' => {[l := v]} ∪ heap_array (l +ₗ 1) vs' + end. + +Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}. +Proof. by rewrite /heap_array right_id. Qed. + +Lemma heap_array_lookup l vs w k : + heap_array l vs !! k = Some w ↔ + ∃ j, (0 ≤ j)%Z ∧ k = l +ₗ j ∧ vs !! (Z.to_nat j) = Some w. +Proof. + revert k l; induction vs as [|v' vs IH]=> l' l /=. + { rewrite lookup_empty. naive_solver lia. } + rewrite -insert_union_singleton_l lookup_insert_Some IH. split. + - intros [[-> ?] | (Hl & j & ? & -> & ?)]. + { eexists 0. rewrite loc_add_0. naive_solver lia. } + eexists (1 + j)%Z. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; eauto with lia. + - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=. + { rewrite loc_add_0. eauto. } + right. split. + { rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. } + assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj. + { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. } + rewrite Hj /= in Hil. + eexists (j - 1)%Z. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l. + auto with lia. +Qed. + +Lemma heap_array_map_disjoint (h : heap) (l : loc) (vs : list val) : + (∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) → + (heap_array l vs) ##ₘ h. +Proof. + intros Hdisj. apply map_disjoint_spec=> l' v1 v2. + intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup. + move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj. +Qed. + +Definition init_heap (l : loc) (n : Z) (v : val) (σ : heap) : heap := + heap_array l (replicate (Z.to_nat n) v) ∪ σ. + +Lemma init_heap_singleton l v σ : + init_heap l 1 v σ = <[l:=v]> σ. +Proof. + rewrite /init_heap /=. + rewrite right_id insert_union_singleton_l. done. +Qed. + +Inductive base_step : expr * heap → expr * heap → 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, σ) + | NewS e v σ l : + σ !! l = None → + to_val e = Some v → + base_step (New e, σ) (Lit $ LitLoc l, init_heap l 1 v σ) + | LoadS l v σ : + σ !! l = Some v → + base_step (Load (Lit $ LitLoc l), σ) (of_val v, σ) + | StoreS l v w e2 σ : + σ !! l = Some v → + to_val e2 = Some w → + base_step (Store (Lit $ LitLoc l) e2, σ) + (Lit LitUnit, <[l:=w]> σ) +. + +(* 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' σ1 σ2 σ2' : + base_step (e1, σ1) (e2, σ2) → + base_step (e1, σ1) (e2', σ2') → is_Some (to_val e2) → is_Some (to_val e2'). +Proof. inversion 1; inversion 1; naive_solver. Qed. + +Lemma new_fresh v σ : + let l := fresh_locs (dom σ) in + base_step (New (of_val v), σ) (Lit $ LitLoc l, init_heap l 1 v σ). +Proof. + intros. + apply NewS. + - apply (not_elem_of_dom). + rewrite -(loc_add_0 l). + by apply fresh_locs_fresh. + - rewrite to_of_val. eauto. +Qed. + +(** We define evaluation contexts *) +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 + | LoadCtx + | StoreRCtx (e1 : expr) + | StoreLCtx (v2 : val) + | NewCtx +. + +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 + | LoadCtx => Load e + | StoreRCtx e1 => Store e1 e + | StoreLCtx v2 => Store e (of_val v2) + | NewCtx => New e + end. + +(** 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 fill_item_no_val Ki e : + to_val e = None → to_val (fill_item Ki e) = None. +Proof. + intros Hn. destruct (to_val (fill_item _ _ )) eqn:Heq; last done. + edestruct (fill_item_val Ki e) as (? & ?); last simplify_eq. + eauto. +Qed. + +Lemma val_base_stuck e1 e2 σ1 σ2 : base_step (e1, σ1) (e2, σ2) → to_val e1 = None. +Proof. inversion 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 σ1 σ2 : + base_step (fill_item Ki e, σ1) (e2, σ2) → 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 : expr * heap → expr * heap → Prop := + Ectx_step K e1 e2 σ1 σ2 e1' e2' : + e1 = fill K e1' → e2 = fill K e2' → + base_step (e1', σ1) (e2', σ2) → contextual_step (e1, σ1) (e2, σ2). + + +Lemma base_contextual_step e1 e2 σ1 σ2 : + base_step (e1, σ1) (e2, σ2) → contextual_step (e1, σ1) (e2, σ2). +Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed. + +Lemma fill_contextual_step K e1 e2 σ1 σ2 : + contextual_step (e1, σ1) (e2, σ2) → contextual_step (fill K e1, σ1) (fill K e2, σ2). +Proof. + inversion 1; subst. + 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 | Load e | New e=> is_closed X e + | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store 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 σ1 σ2 : + fill K' e1' = fill K_redex e1_redex → + to_val e1' = None → + base_step (e1_redex, σ1) (e2, σ2) → + ∃ 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. +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 σ1 σ2 : + base_step (fill K e, σ1) (e2, σ2) → 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' σ1 σ2 : + to_val e = None → + contextual_step (fill K e, σ1) (fill K e', σ2) → + contextual_step (e, σ1) (e', σ2). +Proof. + intros ? Hcontextual. + inversion Hcontextual as [??????? Heq1 Heq2 ?]; subst. + eapply step_by_val in H as (K'' & Heq); [ | done | done]. + subst K0. + rewrite <-fill_comp in Heq1. rewrite <-fill_comp in Heq2. + apply fill_inj in Heq1. apply fill_inj in Heq2. subst. + econstructor; done. +Qed. + +Lemma contextual_ectx_step_case K e e' σ1 σ2 : + contextual_step (fill K e, σ1) (e', σ2) → + (∃ e'', e' = fill K e'' ∧ contextual_step (e, σ1) (e'', σ2)) ∨ 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. + +Lemma base_reducible_contextual_step_ectx K e1 e2 σ1 σ2 : + base_reducible e1 σ1 → + contextual_step (fill K e1, σ1) (e2, σ2) → + ∃ e2', e2 = fill K e2' ∧ base_step (e1, σ1) (e2', σ2). +Proof. + intros (e2''&σ2'' & HhstepK) Hctx. + inversion Hctx as [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 σ1 σ2 : + base_reducible e1 σ1 → + contextual_step (e1, σ1) (e2, σ2) → + base_step (e1, σ1) (e2, σ2). +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. + inversion 1 as [??????? -> -> ?%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 σ1 σ2 : + is_val e2 → + contextual_step (e1, σ1) (e1', σ2) → + contextual_step (App e1 e2, σ1) (App e1' e2, σ2). +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' σ1 σ2 : + contextual_step (e2, σ1) (e2', σ2) → + contextual_step (App e1 e2, σ1) (App e1 e2', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [AppRCtx e1]). +Qed. + +Lemma contextual_step_tapp e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (TApp e, σ1) (TApp e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [TAppCtx]). +Qed. + +Lemma contextual_step_pack e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Pack e, σ1) (Pack e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [PackCtx]). +Qed. + +Lemma contextual_step_unpack x e e' e2 σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Unpack x e e2, σ1) (Unpack x e' e2, σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [UnpackCtx x e2]). +Qed. + +Lemma contextual_step_unop op e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (UnOp op e, σ1) (UnOp op e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [UnOpCtx op]). +Qed. + +Lemma contextual_step_binop_l op e1 e1' e2 σ1 σ2 : + is_val e2 → + contextual_step (e1, σ1) (e1', σ2) → + contextual_step (BinOp op e1 e2, σ1) (BinOp op e1' e2, σ2). +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' σ1 σ2 : + contextual_step (e2, σ1) (e2', σ2) → + contextual_step (BinOp op e1 e2, σ1) (BinOp op e1 e2', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [BinOpRCtx op e1]). +Qed. + +Lemma contextual_step_if e e' e1 e2 σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (If e e1 e2, σ1) (If e' e1 e2, σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [IfCtx e1 e2]). +Qed. + +Lemma contextual_step_pair_l e1 e1' e2 σ1 σ2 : + is_val e2 → + contextual_step (e1, σ1) (e1', σ2) → + contextual_step (Pair e1 e2, σ1) (Pair e1' e2, σ2). +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' σ1 σ2 : + contextual_step (e2, σ1) (e2', σ2) → + contextual_step (Pair e1 e2, σ1) (Pair e1 e2', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [PairRCtx e1]). +Qed. + + +Lemma contextual_step_fst e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Fst e, σ1) (Fst e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [FstCtx]). +Qed. + +Lemma contextual_step_snd e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Snd e, σ1) (Snd e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [SndCtx]). +Qed. + +Lemma contextual_step_injl e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (InjL e, σ1) (InjL e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [InjLCtx]). +Qed. + +Lemma contextual_step_injr e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (InjR e, σ1) (InjR e', σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [InjRCtx]). +Qed. + +Lemma contextual_step_case e e' e1 e2 σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Case e e1 e2, σ1) (Case e' e1 e2, σ2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step [CaseCtx e1 e2]). +Qed. + +Lemma contextual_step_roll e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Roll e, σ1) (Roll e', σ2). +Proof. by apply (fill_contextual_step [RollCtx]). Qed. + +Lemma contextual_step_unroll e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Unroll e, σ1) (Unroll e', σ2). +Proof. by apply (fill_contextual_step [UnrollCtx]). Qed. + +Lemma contextual_step_new e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (New e, σ1) (New e', σ2). +Proof. by apply (fill_contextual_step [NewCtx]). Qed. + +Lemma contextual_step_load e e' σ1 σ2 : + contextual_step (e, σ1) (e', σ2) → + contextual_step (Load e, σ1) (Load e', σ2). +Proof. by apply (fill_contextual_step [LoadCtx]). Qed. + +Lemma contextual_step_store_r e1 e2 e2' σ1 σ2 : + contextual_step (e2, σ1) (e2', σ2) → + contextual_step (Store e1 e2, σ1) (Store e1 e2', σ2). +Proof. by apply (fill_contextual_step [StoreRCtx _]). Qed. + +Lemma contextual_step_store_l e1 e1' e2 σ1 σ2 : + is_val e2 → + contextual_step (e1, σ1) (e1', σ2) → + contextual_step (Store e1 e2, σ1) (Store e1' e2, σ2). +Proof. + intros [v <-%of_to_val]%is_val_spec Hcontextual. + by eapply (fill_contextual_step [StoreLCtx _]). +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 + contextual_step_new contextual_step_load contextual_step_store_r contextual_step_store_l : core. diff --git a/theories/type_systems/systemf_mu_state/locations.v b/theories/type_systems/systemf_mu_state/locations.v new file mode 100644 index 0000000..f3dda15 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/locations.v @@ -0,0 +1,46 @@ +From stdpp Require Import countable numbers gmap. + +Record loc := Loc { loc_car : Z }. + +Add Printing Constructor loc. + +Global Instance loc_eq_decision : EqDecision loc. +Proof. solve_decision. Defined. + +Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}. + +Global Instance loc_countable : Countable loc. +Proof. by apply (inj_countable' loc_car Loc); intros []. Defined. + +Global Program Instance loc_infinite : Infinite loc := + inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _. +Next Obligation. done. Qed. + +Definition loc_add (l : loc) (off : Z) : loc := + {| loc_car := loc_car l + off|}. + +Notation "l +ₗ off" := + (loc_add l off) (at level 50, left associativity) : stdpp_scope. + +Lemma loc_add_assoc l i j : l +ₗ i +ₗ j = l +ₗ (i + j). +Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed. + +Lemma loc_add_0 l : l +ₗ 0 = l. +Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed. + +Global Instance loc_add_inj l : Inj eq eq (loc_add l). +Proof. destruct l; unfold Inj, loc_add; simpl; intros; simplify_eq; lia. Qed. + +Definition fresh_locs (ls : gset loc) : loc := + {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}. + +Lemma fresh_locs_fresh ls i : + (0 ≤ i)%Z → fresh_locs ls +ₗ i ∉ ls. +Proof. + intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls) + i)%Z. + { intros help Hf%help. simpl in *. lia. } + apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)%Z)); + set_solver by eauto with lia. +Qed. + +Global Opaque fresh_locs. diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v new file mode 100644 index 0000000..52e0286 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/logrel.v @@ -0,0 +1,1738 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.lib Require Export facts maps. +From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst execution. +From Equations Require Export Equations. +From Autosubst Require Export Autosubst. + +(** * Logical relation for SystemF + recursive types *) + +(** ** First-order typing for heaps *) +(* We have to explicitly specify the type of first-order types here. + + One alternative approach would be to just require first-orderness in the ref case of the logrel, + but this breaks the boring lemma about moving substitution: (A.[σ]) might be first-order + even if A is not (because it contains a type variable), so we fail to prove the equivalence. + Explicitly defining fotypes in this way prevents type substitution from going below Ref entirely, + which fixes this problem. +*) + +Inductive fotype : Type := + | FOInt + | FOBool + | FOUnit + | FOProd (A B : fotype) + | FOSum (A B : fotype). + +Inductive type : Type := + (** [var] is the type of variables of Autosubst -- it unfolds to [nat] *) + | TVar : var → type + | Int + | Bool + | Unit + (** The [{bind 1 of type}] tells Autosubst to put a De Bruijn binder here *) + | TForall : {bind 1 of type} → type + | TExists : {bind 1 of type} → type + | Fun (A B : type) + | Prod (A B : type) + | Sum (A B : type) + | TMu : {bind 1 of type} → type + | Ref (a : fotype) +. + +Fixpoint of_fotype (a : fotype) : type := + match a with + | FOInt => Int + | FOBool => Bool + | FOUnit => Unit + | FOProd a b => Prod (of_fotype a) (of_fotype b) + | FOSum a b => Sum (of_fotype a) (of_fotype b) + end. +Coercion of_fotype : fotype >-> type. + +(** Autosubst instances. + This lets Autosubst do its magic and derive all the substitution functions, etc. + *) +#[export] Instance Ids_type : Ids type. derive. Defined. +#[export] Instance Rename_type : Rename type. derive. Defined. +#[export] Instance Subst_type : Subst type. derive. Defined. +#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed. + +Definition typing_context := gmap string type. +Implicit Types + (Γ : typing_context) + (v : val) + (e : expr) + (A B : type) + (* we use lower-case letters for first-order types *) + (a : fotype) +. + +Declare Scope FType_scope. +Delimit Scope FType_scope with ty. +Bind Scope FType_scope with type. +Notation "# x" := (TVar x) : FType_scope. +Infix "→" := Fun : FType_scope. +Notation "(→)" := Fun (only parsing) : FType_scope. +Notation "∀: τ" := + (TForall τ%ty) + (at level 100, τ at level 200) : FType_scope. +Notation "∃: τ" := + (TExists τ%ty) + (at level 100, τ at level 200) : FType_scope. +Infix "×" := Prod (at level 70) : FType_scope. +Notation "(×)" := Prod (only parsing) : FType_scope. +Infix "+" := Sum : FType_scope. +Notation "(+)" := Sum (only parsing) : FType_scope. +Notation "μ: A" := + (TMu A%ty) + (at level 100, A at level 200) : FType_scope. + +Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ"). + +Implicit Types + (α : var) +. +Inductive type_wf : nat → type → Prop := + | type_wf_TVar m n: + m < n → + type_wf n (TVar m) + | type_wf_Int n: type_wf n Int + | type_wf_Bool n : type_wf n Bool + | type_wf_Unit n : type_wf n Unit + | type_wf_TForall n A : + type_wf (S n) A → + type_wf n (TForall A) + | type_wf_TExists n A : + type_wf (S n) A → + type_wf n (TExists A) + | type_wf_Fun n A B: + type_wf n A → + type_wf n B → + type_wf n (Fun A B) + | type_wf_Prod n A B : + type_wf n A → + type_wf n B → + type_wf n (Prod A B) + | type_wf_Sum n A B : + type_wf n A → + type_wf n B → + type_wf n (Sum A B) + | type_wf_mu n A : + type_wf (S n) A → + type_wf n (μ: A) + | type_wf_ref n a : + type_wf n (Ref a). +#[export] Hint Constructors type_wf : core. + +Inductive bin_op_typed : bin_op → type → type → type → Prop := + | plus_op_typed : bin_op_typed PlusOp Int Int Int + | minus_op_typed : bin_op_typed MinusOp Int Int Int + | mul_op_typed : bin_op_typed MultOp Int Int Int + | lt_op_typed : bin_op_typed LtOp Int Int Bool + | le_op_typed : bin_op_typed LeOp Int Int Bool + | eq_op_typed : bin_op_typed EqOp Int Int Bool. +#[export] Hint Constructors bin_op_typed : core. + +Inductive un_op_typed : un_op → type → type → Prop := + | neg_op_typed : un_op_typed NegOp Bool Bool + | minus_un_op_typed : un_op_typed MinusUnOp Int Int. + +Reserved Notation "'TY' Δ ; Γ ⊢ e : A" (at level 74, e, A at next level). +Inductive syn_typed : nat → typing_context → expr → type → Prop := + | typed_var n Γ x A : + Γ !! x = Some A → + TY n; Γ ⊢ (Var x) : A + | typed_lam n Γ x e A B : + TY n ; (<[ x := A]> Γ) ⊢ e : B → + type_wf n A → + TY n; Γ ⊢ (Lam (BNamed x) e) : (A → B) + | typed_lam_anon n Γ e A B : + TY n ; Γ ⊢ e : B → + type_wf n A → + TY n; Γ ⊢ (Lam BAnon e) : (A → B) + | typed_tlam n Γ e A : + (* we need to shift the context up as we descend under a binder *) + TY S n; (⤉ Γ) ⊢ e : A → + TY n; Γ ⊢ (Λ, e) : (∀: A) + | typed_tapp n Γ A B e : + TY n; Γ ⊢ e : (∀: A) → + type_wf n B → + (* A.[B/] is the notation for Autosubst's substitution operation that + replaces variable 0 by [B] *) + TY n; Γ ⊢ (e <>) : (A.[B/]) + | typed_pack n Γ A B e : + type_wf n B → + type_wf (S n) A → + TY n; Γ ⊢ e : (A.[B/]) → + TY n; Γ ⊢ (pack e) : (∃: A) + | typed_unpack n Γ A B e e' x : + type_wf n B → (* we should not leak the existential! *) + TY n; Γ ⊢ e : (∃: A) → + (* As we descend under a type variable binder for the typing of [e'], + we need to shift the indices in [Γ] and [B] up by one. + On the other hand, [A] is already defined under this binder, so we need not shift it. + *) + TY (S n); (<[x := A]>(⤉Γ)) ⊢ e' : (B.[ren (+1)]) → + TY n; Γ ⊢ (unpack e as BNamed x in e') : B + | typed_int n Γ z : TY n; Γ ⊢ (Lit $ LitInt z) : Int + | typed_bool n Γ b : TY n; Γ ⊢ (Lit $ LitBool b) : Bool + | typed_unit n Γ : TY n; Γ ⊢ (Lit $ LitUnit) : Unit + | typed_if n Γ e0 e1 e2 A : + TY n; Γ ⊢ e0 : Bool → + TY n; Γ ⊢ e1 : A → + TY n; Γ ⊢ e2 : A → + TY n; Γ ⊢ If e0 e1 e2 : A + | typed_app n Γ e1 e2 A B : + TY n; Γ ⊢ e1 : (A → B) → + TY n; Γ ⊢ e2 : A → + TY n; Γ ⊢ (e1 e2)%E : B + | typed_binop n Γ e1 e2 op A B C : + bin_op_typed op A B C → + TY n; Γ ⊢ e1 : A → + TY n; Γ ⊢ e2 : B → + TY n; Γ ⊢ BinOp op e1 e2 : C + | typed_unop n Γ e op A B : + un_op_typed op A B → + TY n; Γ ⊢ e : A → + TY n; Γ ⊢ UnOp op e : B + | typed_pair n Γ e1 e2 A B : + TY n; Γ ⊢ e1 : A → + TY n; Γ ⊢ e2 : B → + TY n; Γ ⊢ (e1, e2) : A × B + | typed_fst n Γ e A B : + TY n; Γ ⊢ e : A × B → + TY n; Γ ⊢ Fst e : A + | typed_snd n Γ e A B : + TY n; Γ ⊢ e : A × B → + TY n; Γ ⊢ Snd e : B + | typed_injl n Γ e A B : + type_wf n B → + TY n; Γ ⊢ e : A → + TY n; Γ ⊢ InjL e : A + B + | typed_injr n Γ e A B : + type_wf n A → + TY n; Γ ⊢ e : B → + TY n; Γ ⊢ InjR e : A + B + | typed_case n Γ e e1 e2 A B C : + TY n; Γ ⊢ e : B + C → + TY n; Γ ⊢ e1 : (B → A) → + TY n; Γ ⊢ e2 : (C → A) → + TY n; Γ ⊢ Case e e1 e2 : A + | typed_roll n Γ e A : + TY n; Γ ⊢ e : (A.[(μ: A)/]) → + TY n; Γ ⊢ (roll e) : (μ: A) + | typed_unroll n Γ e A : + TY n; Γ ⊢ e : (μ: A) → + TY n; Γ ⊢ (unroll e) : (A.[(μ: A)/]) + (** Typing rules for state *) + (* We use lower-case letters, which imposes the requirement to use first-order types. + (The coercion [of_fotype] does a lot of work here.) *) + | typed_load n Γ e a : + TY n; Γ ⊢ e : (Ref a) → + TY n; Γ ⊢ !e : a + | typed_store n Γ e1 e2 a : + TY n; Γ ⊢ e1 : (Ref a) → + TY n; Γ ⊢ e2 : a → + TY n; Γ ⊢ (e1 <- e2) : Unit + | typed_new n Γ e a : + TY n; Γ ⊢ e : a → + TY n; Γ ⊢ (new e) : Ref a +where "'TY' Δ ; Γ ⊢ e : A" := (syn_typed Δ Γ e%E A%ty). +#[export] Hint Constructors syn_typed : core. + +Lemma syn_typed_closed Δ Γ e A X : + TY Δ; Γ ⊢ e : A → + (∀ x, x ∈ dom Γ → x ∈ X) → + is_closed X e. +Proof. + induction 1 as [ | ??????? IH | | n Γ e A H IH | | | n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done. + { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. } + { (* lam *) apply IH. + intros y. rewrite elem_of_dom lookup_insert_is_Some. + intros [<- | [? Hy]]; first by apply elem_of_cons; eauto. + apply elem_of_cons. right. eapply Hx. by apply elem_of_dom. + } + { (* anon lam *) naive_solver. } + { (* tlam *) + eapply IH. intros x Hel. apply Hx. + by rewrite dom_fmap in Hel. + } + 3: { (* unpack *) + apply andb_True; split. + - apply IH1. apply Hx. + - apply IH2. intros y. rewrite elem_of_dom lookup_insert_is_Some. + intros [<- | [? Hy]]; first by apply elem_of_cons; eauto. + apply elem_of_cons. right. eapply Hx. + apply elem_of_dom. revert Hy. rewrite lookup_fmap fmap_is_Some. done. + } + (* everything else *) + all: repeat match goal with + | |- Is_true (_ && _) => apply andb_True; split + end. + all: try naive_solver. +Qed. + +Goal TY 0; ∅ ⊢ (λ: "x", #1 + "x") : (Int → Int). +Proof. eauto. Qed. +Goal TY 0; ∅ ⊢ (Λ, λ: "x", "x") : (∀: #0 → #0). +Proof. eauto 8. Qed. +Goal TY 0; ∅ ⊢ (new #42 <- #1337) : Unit. +Proof. eapply (typed_store _ _ _ _ FOInt); eauto. Qed. + +(** ** Worlds *) +(** We represent heap invariants as predicates on heaps, + and worlds as lists of such invariants. + *) +Definition heap_inv := heap → Prop. +Definition world := list heap_inv. +Implicit Types (W : world) (INV : heap_inv). +(** [W'] extends [W] if [W] is a suffix of [W'] *) +Definition wext W W' := suffix W W'. +Notation "W' ⊒ W" := (wext W W') (at level 40). +#[export] Instance wext_preorder : PreOrder wext. +Proof. apply _. Qed. + +(** Satisfaction is defined straightforwardly by recursion. + We use map difference ∖ that computes the difference of two maps + based on the domain. + *) +Fixpoint wsat W σ := + match W with + | INV :: W' => + ∃ σ0, INV σ0 ∧ σ0 ⊆ σ ∧ wsat W' (σ ∖ σ0) + | [] => True + end. + +Lemma wsat_mono σ σ' W : + σ ⊆ σ' → + wsat W σ → wsat W σ'. +Proof. + induction W as [ | INV W' IH] in σ, σ' |-*; first done. + simpl. intros Hincl (σ0 & Hinv & Hincl' & Hsat). + exists σ0; split; first done. split; first by etrans. + eapply IH; last done. + by apply map_difference_mono. +Qed. + +Lemma wsat_wext W W' σ : + W' ⊒ W → + wsat W' σ → + wsat W σ. +Proof. + intros (L & ->). induction L as [ | INV L' IH] in σ |-*; first done. + simpl. intros (σ0 & Hinv & Hincl & ?%IH). eapply wsat_mono; last done. + by apply map_subseteq_difference_l. +Qed. + +Lemma wsat_lookup W σ i P : + wsat W σ → W !! i = Some P → + ∃ σ0, σ0 ⊆ σ ∧ P σ0. +Proof. + induction W as [ | INV W IH] in i, σ |-*; first done. + simpl. intros (σ0 & HINV & Hincl & Hsat). + destruct i as [ | i]; simpl. + - intros [= ->]. eauto. + - intros Hlook. destruct (IH _ _ Hsat Hlook) as (σ1 & ? & ?). + exists σ1; split; last done. etrans; eauto. + by apply map_subseteq_difference_l. +Qed. + +Lemma wext_lookup W' W i INV : + W' ⊒ W → W !! i = Some INV → ∃ i', W' !! i' = Some INV. +Proof. + unfold wext. + intros Hincl Hlook. + destruct Hincl as (W''& ->). + exists (length W'' + i). + rewrite lookup_app_r; last lia. + by rewrite Nat.add_comm Nat.add_sub. +Qed. + +Lemma wsat_merge σ1 σ2 W1 W2 : + σ1 ##ₘ σ2 → + wsat W1 σ1 → + wsat W2 σ2 → + wsat (W1 ++ W2) (σ1 ∪ σ2). +Proof. + intros Hdisj. induction W1 as [ | INV W1 IH] in W2, σ1, σ2, Hdisj |-*. + - simpl. intros _ Hs. eapply wsat_mono; last done. by apply map_union_subseteq_r. + - simpl. intros (σ0 & Hinv & Hincl & Hsat1) Hsat2. + exists σ0. split_and!; [ done | | ]. + + by apply map_union_subseteq_l'. + + rewrite map_difference_union'; last done. + assert ((σ2 ∖ σ0) = σ2) as H. + { symmetry; apply map_disjoint_difference. + symmetry. eapply map_disjoint_weaken_l; done. + } + rewrite H. + apply IH; [ | done..]. + eapply map_disjoint_weaken_l; first done. by apply map_subseteq_difference_l. +Qed. + +(** Assuming that we have found a heap invariant [P] talking about [l] and that is invariant wrt the concrete value, we can update [l]. + *) +Lemma wsat_update W σ i (l : loc) (v : val) (P : heap_inv) : + wsat W σ → W !! i = Some P → + (∀ σ : heap, P σ → is_Some (σ !! l) ∧ P (<[l := v]> σ)) → + wsat W (<[l := v]> σ). +Proof. + induction W as [ | INV W IH] in i, σ |-*; first done. + destruct i as [ | i]. + - intros (σ0 & HINV & Hincl & Hsat). + intros [= ->] Hupd. eexists. split_and!; [eapply Hupd, HINV | | ]. + + by apply insert_mono. + + apply Hupd in HINV as [[v0 Hs] _]. eapply wsat_mono; last apply Hsat. + rewrite (difference_insert _ _ _ _ _ v0). rewrite insert_id; done. + - intros Hsat Hlook Hupd. + destruct Hsat as (σ0 & HINV & Hincl & Hsat). simpl in *. + specialize (wsat_lookup _ _ _ _ Hsat Hlook) as (σ1 & Hincl' & [Hs ?]%Hupd). + specialize (IH _ _ Hsat Hlook Hupd). + assert (σ0 !! l = None) as H0l. + { eapply lookup_weaken_is_Some in Hincl'; last done. + apply lookup_difference_is_Some in Hincl'. apply Hincl'. + } + exists σ0. split_and!; [ done | | ]. + + etrans; first by eapply (insert_subseteq _ l v). + by apply insert_mono. + + assert (<[l:=v]> σ ∖ σ0 = <[l:=v]> (σ ∖ σ0)) as ->; last done. + symmetry. apply insert_difference'. done. +Qed. + +(** ** Definition of the logrel *) + +(** A semantic type consists of a value-predicate parameterized over a step-index and a world, + a proof of closedness, and a proof of downwards-closure wrt step-indices, + and a proof of upwards-closure wrt world extension. + *) +Record sem_type := mk_ST { + sem_type_car :> nat → world → val → Prop; + sem_type_closed_val k W v : sem_type_car k W v → is_closed [] (of_val v); + sem_type_mono : ∀ k k' W v, sem_type_car k W v → k' ≤ k → sem_type_car k' W v; + sem_type_mono_world : ∀ k W W' v, sem_type_car k W v → W' ⊒ W → sem_type_car k W' v + }. + +(** Two tactics we will use later on. + [pose_sem_type P as N] defines a semantic type at name [N] with the value predicate [P]. + *) +(* slightly complicated formulation to make the proof term [p] opaque and prevent it from polluting the context *) +Tactic Notation "pose_sem_type" uconstr(P) "as" ident(N) := + let p := fresh "__p" in + let p2 := fresh "__p2" in + let p3 := fresh "__p3" in + unshelve refine ((λ p p2 p3, let N := (mk_ST P p p2 p3) in _) _ _ _); first (simpl in p, p2, p3); cycle 1. +Tactic Notation "specialize_sem_type" constr(S) "with" uconstr(P) "as" ident(N) := + pose_sem_type P as N; last specialize (S N). + +(** We represent type variable assignments [δ] as functions [f] into semantic types. + The variable [#n] (in De Bruijn representation) is mapped to [f n]. + *) +Definition tyvar_interp := var → sem_type. +Implicit Types + (δ : tyvar_interp) + (τ : sem_type) +. + +(** + In Coq, we need to make argument why the logical relation is well-defined precise: + (for Coq, that means: we need to show that the recursion is terminating). + + To make this formal, we define a well-founded relation that allows to either decrease the step-index, the type, or switch from the expression case to the value case for recursive calls. + We define size measures for for all three of these things, and then combine them into a big lexicographic ordering [term_rel]. + + Adding in state does not provide much of a complication, _as long as we only consider first-order state_. + (higher-order state makes the argument quite a bit more difficult, since worlds then also need to be step-indexed). + *) +Equations type_size (A : type) : nat := + type_size Int := 1; + type_size Bool := 1; + type_size Unit := 1; + type_size (A → B) := type_size A + type_size B + 1; + type_size (#α) := 1; + type_size (∀: A) := type_size A + 2; + type_size (∃: A) := type_size A + 2; + type_size (A × B) := type_size A + type_size B + 1; + type_size (A + B) := max (type_size A) (type_size B) + 1; + type_size (μ: A) := type_size A + 2; + type_size (Ref A) := 2 +. +(* [ltof A R] defines a well-founded measure on type [A] by using a mapping [R] from [A] to [nat] + (it lifts the < relation on natural numbers to [A]) *) +Definition type_lt := ltof type type_size. +#[local] Instance type_lt_wf : WellFounded type_lt. +Proof. apply well_founded_ltof. Qed. + +Inductive type_case : Set := + | expr_case | val_case. +Definition type_case_size (c : type_case) : nat := + match c with | expr_case => 1 | val_case => 0 end. +Definition type_case_lt := ltof type_case type_case_size. +#[local] Instance type_case_lt_wf : WellFounded type_case_lt. +Proof. apply well_founded_ltof. Qed. + +Definition term_rel := Subterm.lexprod nat (type * type_case) lt (Subterm.lexprod type type_case type_lt type_case_lt). +#[local] Instance term_rel_wf : WellFounded term_rel. apply _. Qed. + +(** *** The logical relation *) +(** Since the relation is step-indexed now, and the argument that the case for recursive types is well-formed + fundamentally requires decreasing the step-index, we also need to convince Equations that this definition is well-formed! + We do this by providing a well-founded termination relation [term_rel] that decreases for each recursive call. + *) +Equations type_interp (c : type_case) (t : type) δ (k : nat) (W : world) (v : match c with val_case => val | expr_case => expr end) : Prop + by wf (k, (t, c)) term_rel := { + + type_interp val_case Int δ k W v => + ∃ z : Z, v = #z ; + type_interp val_case Bool δ k W v => + ∃ b : bool, v = #b ; + type_interp val_case Unit δ k W v => + v = #LitUnit ; + type_interp val_case (A × B) δ k W v => + ∃ v1 v2 : val, v = (v1, v2)%V ∧ type_interp val_case A δ k W v1 ∧ type_interp val_case B δ k W v2; + type_interp val_case (A + B) δ k W v => + (∃ v' : val, v = InjLV v' ∧ type_interp val_case A δ k W v') ∨ + (∃ v' : val, v = InjRV v' ∧ type_interp val_case B δ k W v'); + + type_interp val_case (A → B) δ k W v => + ∃ x e, v = LamV x e ∧ is_closed (x :b: nil) e ∧ + (* Slightly weird formulation: for down-closure, we want to quantify over all k' ≤ k -- + but with that formulation, the termination checker will not be able to see that k' will really be smaller! + Thus, we quantify over the difference kd and subtract *) + ∀ v' kd W', W' ⊒ W → + type_interp val_case A δ (k - kd) W' v' → + type_interp expr_case B δ (k - kd) W' (subst' x (of_val v') e); + type_interp val_case (#α) δ k W v => + (δ α).(sem_type_car) k W v; + type_interp val_case (∀: A) δ k W v => + ∃ e, v = TLamV e ∧ is_closed [] e ∧ + ∀ τ, type_interp expr_case A (τ .: δ) k W e; + type_interp val_case (∃: A) δ k W v => + ∃ v', v = PackV v' ∧ + ∃ τ : sem_type, type_interp val_case A (τ .: δ) k W v'; + (** Defined with two cases: ordinarily, we might require [k > 0] in the body as a guard for the recursive call, + but this does not count as a proper guard for termination for Coq -- therefore we handle the 0-case separately. + *) + type_interp val_case (μ: A) δ (S k) W v => + ∃ v', v = (roll v')%V ∧ is_closed [] v' ∧ ∀ kd, type_interp val_case (A.[μ: A/]%ty) δ (k - kd) W v'; + type_interp val_case (μ: A) δ 0 W v => + ∃ v', v = (roll v')%V ∧ is_closed [] v'; + (** The reference case *) + type_interp val_case (Ref a) δ k W v => + ∃ (l : loc), v = LitV $ LitLoc l ∧ ∃ i INV, W !! i = Some INV ∧ + INV = (λ σ', ∃ v, σ' = <[ l := v ]> ∅ ∧ TY 0; ∅ ⊢ (of_val v) : a); + + type_interp expr_case t δ k W e => + ∀ e' h h' W' n, W' ⊒ W → wsat W' h → n < k → red_nsteps n e h e' h' → ∃ v W'', to_val e' = Some v ∧ + W'' ⊒ W' ∧ wsat W'' h' ∧ type_interp val_case t δ (k - n) W'' v +}. + +(** Proving that the arguments are decreasing for recursive calls is a bit more messy now, but it's mostly systematic. + Therefore we provide a simple automation tactic that will also become useful a few times below. +*) +Ltac dsimpl := + repeat match goal with + | |- term_rel (?k, _) (?k, _) => + (* step-index is not decreasing, go right *) + right + | |- term_rel (?k1, _) (?k2, _) => + (* use [lia] to decide where to go *) + destruct (decide (k1 < k2)) as [ ? | ?]; [left; lia | assert (k1 = k2) as -> by lia; right] + | |- Subterm.lexprod type type_case _ _ (?t, _) (?t, _) => + (* type is not decreasing, go right *) + right + | |- Subterm.lexprod type type_case _ _ (_, ?a) (_, ?a) => + (* type case is not decreasing, go left *) + left + | |- term_rel (_, _) (_, _) => + (* branch non-deterministically and try to solve the remaining goal *) + first [left; solve [dsimpl] | right; solve [dsimpl]] + | |- Subterm.lexprod type type_case _ _ _ _ => + (* branch non-deterministically *) + first [left; solve [dsimpl] | right; solve [dsimpl]] + | _ => + (* try to solve a leaf, i.e. a [type_lt], [type_case_lt] or [lt] goal *) + unfold type_case_lt, type_lt, ltof; simp type_size; simpl; try lia + end. +(** The tactic solves all of Equations' obligations for showing that the argument decreases. *) +Solve Obligations with (intros; dsimpl). + +(** *** Value relation and expression relation *) +Definition sem_val_rel A δ k W v := type_interp val_case A δ k W v. +Definition sem_expr_rel A δ k W e := type_interp expr_case A δ k W e. + +Notation 𝒱 := (type_interp val_case). +Notation ℰ := (type_interp expr_case). + +Lemma val_rel_is_closed v δ k W A: + 𝒱 A δ k W v → is_closed [] (of_val v). +Proof. + induction A as [ | | | | | A IHA | | A IH1 B IH2 | A IH1 B IH2 | A IHA | A] in k, v, δ |-*; simp type_interp. + - by eapply sem_type_closed_val. + - intros [z ->]. done. + - intros [b ->]. done. + - intros ->. done. + - intros (e & -> & ? & _). done. + - intros (v' & -> & (τ & Hinterp)). simpl. by eapply IHA. + - intros (x & e & -> & ? & _). done. + - intros (v1 & v2 & -> & ? & ?). simpl; apply andb_True; split; eauto. + - intros [(v' & -> & ?) | (v' & -> & ?)]; simpl; eauto. + - destruct k; simp type_interp. + + intros (v' & -> & ?); done. + + intros (v' & -> & ? & Ha); done. + - intros (l & -> & _). done. +Qed. + +(** Downwards closure wrt step-index *) +Lemma type_interp_mono : ∀ '(k, (A, c)) δ W k' x, k' ≤ k → type_interp c A δ k W x → type_interp c A δ k' W x. +Proof. + eapply (well_founded_ind (R := term_rel) term_rel_wf). + intros (k & A & []) IH δ W k'. + { (* expression rel *) + intros e Hk He. simp type_interp in He. simp type_interp. intros e' h h' W' n Hincl Hsat Hn Hred. + destruct (He e' h h' W' n ltac:(done) ltac:(done) ltac:(lia) Hred) as (v & W'' & Hval & Hincl' & Hsat' & Hv). + exists v, W''. split; first done. + split_and!; [done.. | ]. + eapply (IH (k-n, (A, val_case))); [ | lia | done]. + (* show that the induction is decreasing *) + dsimpl. + } + intros v Hk Hv. + destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simp type_interp; simp type_interp in Hv. + - (* var case *) + by eapply sem_type_mono. + - (* universal case *) + destruct Hv as (e & -> & ? & Hv). + exists e. split_and!; [done.. | ]. intros τ. + eapply (IH (k, (A, expr_case))); [ dsimpl | done | done]. + - (* existential case *) + destruct Hv as (v' & -> & (τ & Hv)). exists v'. split; first done. + exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..]. + - (* fun case *) + destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ]. + intros v' kd W' Hv' Hincl. + (* slightly tricky due to the contravariant recursive occurrence *) + set (kd' := k - k'). + specialize (Hv v' (kd + kd')). + replace (k - (kd + kd')) with (k' - kd) in Hv by lia. + eapply (IH (k' - kd, (B, expr_case))); [ | lia | by eapply Hv]. + destruct (decide (k' - kd < k)) as [ ? | ?]; first (left; lia). + assert (k' - kd = k) as -> by lia. dsimpl. + - (* pair case *) + destruct Hv as (v1 & v2 & -> & Hv1 & Hv2). + exists v1, v2. split_and!; first done. + all: eapply (IH (k, (_, _))); [ dsimpl | done..]. + - (* sum case *) + destruct Hv as [(v' & -> & Hv) | (v' & -> & Hv)]; [ left | right]. + all: exists v'; split; first done. + all: eapply (IH (k, (_, _))); [ dsimpl | done..]. + - (* rec case *) + destruct k; simp type_interp in Hv. + { assert (k' = 0) as -> by lia. simp type_interp. } + destruct Hv as (v' & -> & ? & Hv). + destruct k' as [ | k']; simp type_interp. + { eauto. } + exists v'. split_and!; [ done.. | ]. + intros kd. + (* here we crucially use that we can decrease the index *) + eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | lia | done]. + left. lia. +Qed. + +(** We can now derive the two desired lemmas *) +Lemma val_rel_mono_idx A δ k k' W v : k' ≤ k → 𝒱 A δ k W v → 𝒱 A δ k' W v. +Proof. apply (type_interp_mono (k, (A, val_case))). Qed. +Lemma expr_rel_mono_idx A δ k k' W e : k' ≤ k → ℰ A δ k W e → ℰ A δ k' W e. +Proof. apply (type_interp_mono (k, (A, expr_case))). Qed. + +(** Up-closure wrt worlds *) +Lemma type_interp_mono_world : ∀ '(k, (A, c)) δ W W' x, W' ⊒ W → type_interp c A δ k W x → type_interp c A δ k W' x. +Proof. + eapply (well_founded_ind (R := term_rel) term_rel_wf). + intros (k & A & []) IH δ W W'. + { (* expression rel *) + intros e HW He. simp type_interp in He. simp type_interp. intros e' h h' W'' n Hincl Hsat Hn Hred. + destruct (He e' h h' W'' n ltac:(etrans; done) ltac:(done) ltac:(lia) Hred) as (v & W''' & Hval & Hincl' & Hsat' & Hv). + exists v, W'''. split; first done. + split_and!; [done.. | ]. + eapply (IH (k-n, (A, val_case))); [ | | apply Hv]. + - dsimpl. + - done. + } + intros v HW Hv. + destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simp type_interp; simp type_interp in Hv. + - (* var case *) + by eapply sem_type_mono_world. + - (* universal case *) + destruct Hv as (e & -> & ? & Hv). + exists e. split_and!; [done.. | ]. intros τ. + eapply (IH (k, (A, expr_case))); [ dsimpl | done | done]. + - (* existential case *) + destruct Hv as (v' & -> & (τ & Hv)). exists v'. split; first done. + exists τ. eapply (IH (k, (A, _))); [ dsimpl | done..]. + - (* fun case *) + destruct Hv as (x & e & -> & ? & Hv). exists x, e. split_and!; [done..| ]. + intros v' kd W'' Hincl Hv'. + specialize (Hv v' kd W''). + eapply (IH (k - kd, (B, expr_case))); [ dsimpl | | eapply Hv]. + + done. + + etrans; done. + + eapply (IH (k -kd, (A, val_case))); last done; last done. dsimpl. + - (* pair case *) + destruct Hv as (v1 & v2 & -> & Hv1 & Hv2). + exists v1, v2. split_and!; first done. + all: eapply (IH (k, (_, _))); [ dsimpl | done..]. + - (* sum case *) + destruct Hv as [(v' & -> & Hv) | (v' & -> & Hv)]; [ left | right]. + all: exists v'; split; first done. + all: eapply (IH (k, (_, _))); [ dsimpl | done..]. + - (* rec case *) + destruct k; simp type_interp in Hv. + { simp type_interp. } + destruct Hv as (v' & -> & ? & Hv). + simp type_interp. + exists v'. split_and!; [ done.. | ]. + intros kd. + (* here we crucially use that we can decrease the index *) + eapply (IH (k - kd, (A.[(μ: A)%ty/], val_case))); [ | done | done]. + left. lia. + - (* loc case *) + destruct Hv as (l & -> & (i & INV & Hlook & Heq)). + exists l. split; first done. + destruct (wext_lookup _ _ _ _ HW Hlook) as (i' & Hlook'). + exists i', INV. done. +Qed. + +Lemma val_rel_mono_world A δ k W W' v : W' ⊒ W → 𝒱 A δ k W v → 𝒱 A δ k W' v. +Proof. apply (type_interp_mono_world (k, (A, val_case))). Qed. +Lemma expr_rel_mono_world A δ k W W' e : W' ⊒ W → ℰ A δ k W e → ℰ A δ k W' e. +Proof. apply (type_interp_mono_world (k, (A, expr_case))). Qed. + +Lemma val_rel_mono A δ k k' W W' v : k' ≤ k → W' ⊒ W → 𝒱 A δ k W v → 𝒱 A δ k' W' v. +Proof. + intros. eapply val_rel_mono_idx; last eapply val_rel_mono_world; done. +Qed. +Lemma expr_rel_mono A δ k k' W W' e : k' ≤ k → W' ⊒ W → ℰ A δ k W e → ℰ A δ k' W' e. +Proof. + intros. eapply expr_rel_mono_idx; last eapply expr_rel_mono_world; done. +Qed. + +(** This is the Value Inclusion lemma from the lecture notes *) +Lemma sem_val_expr_rel A δ k W v : + 𝒱 A δ k W v → ℰ A δ k W (of_val v). +Proof. + simp type_interp. intros Hv e' h h' W' n Hincl HW Hn (-> & -> & ->)%nsteps_val_inv. + rewrite to_of_val. eexists _, W'; split; first done. + replace (k - 0) with k by lia. + split_and!; [done | done | ]. + by eapply val_rel_mono_world. +Qed. + +Lemma sem_expr_rel_zero_trivial A δ W e : + ℰ A δ 0 W e. +Proof. + simp type_interp. intros ???. lia. +Qed. + +(** Interpret a syntactic type *) +Program Definition interp_type A δ : sem_type := {| + sem_type_car := 𝒱 A δ; +|}. +Next Obligation. by eapply val_rel_is_closed. Qed. +Next Obligation. by eapply val_rel_mono. Qed. +Next Obligation. by eapply val_rel_mono_world. Qed. + +(** Semantic typing of contexts *) +Implicit Types + (θ : gmap string expr). + +(** Context relation *) +Inductive sem_context_rel (δ : tyvar_interp) (k : nat) (W : world) : typing_context → (gmap string expr) → Prop := + | sem_context_rel_empty : sem_context_rel δ k W ∅ ∅ + | sem_context_rel_insert Γ θ v x A : + 𝒱 A δ k W v → + sem_context_rel δ k W Γ θ → + sem_context_rel δ k W (<[x := A]> Γ) (<[x := of_val v]> θ). + +Notation 𝒢 := sem_context_rel. + +Lemma sem_context_rel_vals {δ k W Γ θ x A} : + sem_context_rel δ k W Γ θ → + Γ !! x = Some A → + ∃ e v, θ !! x = Some e ∧ to_val e = Some v ∧ 𝒱 A δ k W v. +Proof. + induction 1 as [|Γ θ v y B Hvals Hctx IH]. + - naive_solver. + - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]]. + + do 2 eexists. split; first by rewrite lookup_insert. + split; first by eapply to_of_val. done. + + eapply IH in Hlook as (e & w & Hlook & He & Hval). + do 2 eexists; split; first by rewrite lookup_insert_ne. + split; first done. done. +Qed. + +Lemma sem_context_rel_subset δ k W Γ θ : + 𝒢 δ k W Γ θ → dom Γ ⊆ dom θ. +Proof. + intros Hctx. apply elem_of_subseteq. intros x (A & Hlook)%elem_of_dom. + eapply sem_context_rel_vals in Hlook as (e & v & Hlook & Heq & Hval); last done. + eapply elem_of_dom; eauto. +Qed. + +Lemma sem_context_rel_dom_eq δ k W Γ θ : + 𝒢 δ k W Γ θ → dom Γ = dom θ. +Proof. + induction 1 as [ | ??????? IH]. + - rewrite !dom_empty //. + - rewrite !dom_insert IH //. +Qed. + +Lemma sem_context_rel_closed δ k W Γ θ: + 𝒢 δ k W Γ θ → subst_is_closed [] θ. +Proof. + induction 1 as [ | Γ θ v x A Hv Hctx IH]; rewrite /subst_is_closed. + - naive_solver. + - intros y e. rewrite lookup_insert_Some. + intros [[-> <-]|[Hne Hlook]]. + + by eapply val_rel_is_closed. + + eapply IH; last done. +Qed. + +Lemma sem_context_rel_mono_idx Γ δ k k' W θ : + k' ≤ k → 𝒢 δ k W Γ θ → 𝒢 δ k' W Γ θ. +Proof. + intros Hk. induction 1 as [|Γ θ v y B Hvals Hctx IH]; constructor. + - eapply val_rel_mono_idx; done. + - apply IH. +Qed. +Lemma sem_context_rel_mono_world Γ δ k W W' θ : + W' ⊒ W → 𝒢 δ k W Γ θ → 𝒢 δ k W' Γ θ. +Proof. + intros HW. induction 1 as [|Γ θ v y B Hvals Hctx IH]; constructor. + - eapply val_rel_mono_world; done. + - apply IH. +Qed. +Lemma sem_context_rel_mono Γ δ k k' W W' θ : + k' ≤ k → W' ⊒ W → 𝒢 δ k W Γ θ → 𝒢 δ k' W' Γ θ. +Proof. + intros. eapply sem_context_rel_mono_idx; last eapply sem_context_rel_mono_world; done. +Qed. + +(** *** Semantic typing judgment *) +Definition sem_typed (Δ : nat) Γ e A := + ∀ θ δ k W, 𝒢 δ k W Γ θ → ℰ A δ k W (subst_map θ e). +Notation "'TY' Δ ; Γ ⊨ e : A" := (sem_typed Δ Γ e A) (at level 74, e, A at next level). + +Section boring_lemmas. + (** The lemmas in this section are all quite boring and expected statements, + but are quite technical to prove due to De Bruijn binders. + We encourage to skip over the proofs of these lemmas. + *) + + Lemma type_interp_ext : + ∀ '(k, (B, c)), ∀ δ δ' W x, + (∀ n k v W', W' ⊒ W → δ n k W' v ↔ δ' n k W' v) → + type_interp c B δ k W x ↔ type_interp c B δ' k W x. + Proof. + eapply (well_founded_ind (R := term_rel) term_rel_wf). + intros (k & A & []) IH δ δ'. + { (* expression rel *) + intros W e Hd. simp type_interp. eapply forall_proper; intros e'. + eapply forall_proper; intros h. eapply forall_proper; intros h'. + eapply forall_proper; intros W'. eapply forall_proper; intros n. + eapply if_iff'; intros. eapply if_iff'; intros _. eapply if_iff'; intros _. + eapply if_iff; first done. f_equiv. intros v. f_equiv. intros W''. + f_equiv. apply and_iff'; intros. f_equiv. + eapply (IH ((k - n), (A, val_case))); first dsimpl. + intros; apply Hd. etrans; last etrans; done. + } + intros W v Hd. destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simp type_interp; eauto. + - apply Hd. done. + - f_equiv; intros e. f_equiv. f_equiv. + eapply forall_proper; intros τ. + eapply (IH (_, (_, _))); first dsimpl. + intros [|m] ?; simpl; eauto. + - f_equiv; intros w. f_equiv. f_equiv. intros τ. + eapply (IH (_, (_, _))); first dsimpl. + intros [|m] ?; simpl; eauto. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv. eapply forall_proper. intros ?. + eapply forall_proper. intros ?. + eapply forall_proper. intros W'. + eapply if_iff'; intros. + eapply if_iff; (eapply (IH (_, (_, _))); first dsimpl). + all: intros; eapply Hd; etrans; done. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl. + - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl. + - destruct k; simp type_interp. + + done. + + f_equiv; intros ?. f_equiv. f_equiv. + eapply forall_proper; intros ?. + by eapply (IH (_, (_, _))); first dsimpl. + Qed. + + Lemma type_interp_move_ren : + ∀ '(k, (B, c)), ∀ δ W σ x, type_interp c B (λ n, δ (σ n)) k W x ↔ type_interp c (rename σ B) δ k W x. + Proof. + eapply (well_founded_ind (R := term_rel) term_rel_wf). + intros (k & A & []) IH δ W σ. + { (* expression rel *) + intros e. simp type_interp. eapply forall_proper; intros e'. + eapply forall_proper; intros h. eapply forall_proper; intros h'. + eapply forall_proper; intros W'. eapply forall_proper; intros n. + + eapply if_iff; first done. eapply if_iff; first done. + eapply if_iff; first done. eapply if_iff; first done. + f_equiv. intros v. f_equiv. intros W''. f_equiv. f_equiv. f_equiv. + eapply (IH (_, (_, _))). + (* show that the induction is decreasing *) + dsimpl. + } + intros v. destruct A as [x | | | | A | A | A B | A B | A B | A | A ]; simpl; simp type_interp; eauto. + - f_equiv; intros e. f_equiv. f_equiv. + eapply forall_proper; intros τ. + etransitivity; last eapply (IH (_, (_, _))); last dsimpl. + eapply (type_interp_ext (_, (_, _))). + intros [|m] ?; simpl; eauto. + - f_equiv; intros w. f_equiv. f_equiv. intros τ. + etransitivity; last eapply (IH (_, (_, _))); last dsimpl. + eapply (type_interp_ext (_, (_, _))). + intros [|m] ?; simpl; eauto. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv. eapply forall_proper. intros ?. + eapply forall_proper. intros ?. eapply forall_proper. intros ?. + eapply if_iff; first done. eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl. + - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl. + - destruct k; simp type_interp. + + done. + + f_equiv; intros ?. f_equiv. f_equiv. + eapply forall_proper; intros ?. + etransitivity; first eapply (IH (_, (_, _))); first dsimpl. + asimpl. done. + Qed. + + Lemma type_interp_move_subst : + ∀ '(k, (B, c)), ∀ δ W σ x, type_interp c B (λ n, interp_type (σ n) δ) k W x ↔ type_interp c (B.[σ]) δ k W x. + Proof. + eapply (well_founded_ind (R := term_rel) term_rel_wf). + intros (k & A & []) IH δ W σ. + { (* expression rel *) + intros e. simp type_interp. eapply forall_proper; intros e'. + eapply forall_proper; intros h. eapply forall_proper; intros h'. + eapply forall_proper; intros W'. eapply forall_proper; intros n. + + eapply if_iff; first done. eapply if_iff; first done. + eapply if_iff; first done. eapply if_iff; first done. + f_equiv. intros v. f_equiv. intros W''. f_equiv. f_equiv. f_equiv. + eapply (IH (_, (_, _))). + (* show that the induction is decreasing *) + dsimpl. + } + intros v. destruct A as [x | | | | A | A | A B | A B | A B | A | A]; simpl; simp type_interp; eauto. + - f_equiv; intros e. f_equiv. f_equiv. + eapply forall_proper; intros τ. + etransitivity; last eapply (IH (_, (_, _))); last dsimpl. + eapply (type_interp_ext (_, (_, _))). + intros [|m] ??? ?; simpl. + + asimpl. simp type_interp. done. + + unfold up; simpl. etransitivity; + last eapply (type_interp_move_ren (_, (_, _))). + done. + - f_equiv; intros w. f_equiv. f_equiv. intros τ. + etransitivity; last eapply (IH (_, (_, _))); last dsimpl. + eapply (type_interp_ext (_, (_, _))). + intros [|m] ? ???; simpl. + + asimpl. simp type_interp. done. + + unfold up; simpl. etransitivity; + last eapply (type_interp_move_ren (_, (_, _))). + done. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv. eapply forall_proper. intros ?. + eapply forall_proper. intros ?. eapply forall_proper. intros W'. + eapply if_iff; first done. + eapply if_iff; by eapply (IH (_, (_, _))); first dsimpl. + - f_equiv. intros ?. f_equiv. intros ?. + f_equiv. f_equiv; by eapply (IH (_, (_, _))); first dsimpl. + - f_equiv; f_equiv; intros ?; f_equiv; by eapply (IH (_, (_, _))); first dsimpl. + - destruct k; simp type_interp. + + done. + + f_equiv; intros ?. f_equiv. f_equiv. + eapply forall_proper; intros ?. + etransitivity; first eapply (IH (_, (_, _))); first dsimpl. + asimpl. done. + Qed. + + + Lemma sem_val_rel_move_single_subst A B δ k v W : + 𝒱 B (interp_type A δ .: δ) k W v ↔ 𝒱 (B.[A/]) δ k W v. + Proof. + etransitivity; last eapply (type_interp_move_subst (_, (_, _))). + eapply (type_interp_ext (_, (_, _))). + intros [| n] ? w W' ?; simpl; simp type_interp; done. + Qed. + + Lemma sem_expr_rel_move_single_subst A B δ k W e : + ℰ B (interp_type A δ .: δ) k W e ↔ ℰ (B.[A/]) δ k W e. + Proof. + etransitivity; last eapply (type_interp_move_subst (_, (_, _))). + eapply (type_interp_ext (_, (_, _))). + intros [| n] ? w W' ?; simpl; simp type_interp; done. + Qed. + + Lemma sem_val_rel_cons A δ k v W τ : + 𝒱 A δ k W v ↔ 𝒱 A.[ren (+1)] (τ .: δ) k W v. + Proof. + etransitivity; last eapply (type_interp_move_subst (_, (_, _))). + eapply (type_interp_ext (_, (_, _))). + intros [| n] ? w W' ?; simpl; simp type_interp; done. + Qed. + + Lemma sem_expr_rel_cons A δ k e W τ : + ℰ A δ k W e ↔ ℰ A.[ren (+1)] (τ .: δ) k W e. + Proof. + etransitivity; last eapply (type_interp_move_subst (_, (_, _))). + eapply (type_interp_ext (_, (_, _))). + intros [| n] ? w W' ?; simpl; simp type_interp; done. + Qed. + + Lemma sem_context_rel_cons Γ k δ θ τ W : + 𝒢 δ k W Γ θ → + 𝒢 (τ .: δ) k W (⤉ Γ) θ. + Proof. + induction 1 as [ | Γ θ v x A Hv Hctx IH]; simpl. + - rewrite fmap_empty. constructor. + - rewrite fmap_insert. constructor; last done. + rewrite -sem_val_rel_cons. done. + Qed. +End boring_lemmas. + +(** Bind lemma *) +Lemma bind K e k W δ A B : + ℰ A δ k W e → + (∀ j v W', j ≤ k → W' ⊒ W → 𝒱 A δ j W' v → ℰ B δ j W' (fill K (of_val v))) → + ℰ B δ k W (fill K e). +Proof. + intros H1 H2. simp type_interp in H1. simp type_interp. + intros e' h h' W' n HW Hsat Hn (j & e'' & h'' & Hj & Hred1 & Hred2)%red_nsteps_fill. + specialize (H1 e'' h h'' W' j ltac:(done) ltac:(done) ltac:(lia) Hred1) as (v & W'' & Hev & Hincl' & Hsat' & Hv). + specialize (H2 (k-j) v W'' ltac:(lia) ltac:(etrans; done) Hv). + simp type_interp in H2. + rewrite (of_to_val _ _ Hev) in H2. + eapply H2 in Hred2; cycle 1; [ reflexivity | done | lia | ]. + assert (k - n = k - j - (n - j)) as -> by lia. + destruct Hred2 as (v' & W''' & ? & ? & ? & Hred2). + exists v', W'''. split_and!; [done | | done | done]. + etrans; done. +Qed. + +(** This is the closure-under-expansion lemma from the lecture notes *) +Lemma expr_det_step_closure e e' A δ k W : + det_step e e' → + ℰ A δ (k - 1) W e' → + ℰ A δ k W e. +Proof. + simp type_interp. intros Hdet Hexpr e'' h h' W' n Hincl Hsat Hn [? Hred]%(det_step_red _ e'); last done. + destruct (Hexpr e'' h h' W' (n -1) Hincl Hsat ) as (v & W'' & Hev & Hincl' & Hsat' & Hv); [lia | done | ]. + exists v, W''. split; first done. split; first done. + replace (k - n) with (k - 1 - (n - 1)) by lia. done. +Qed. + +Lemma expr_det_steps_closure e e' A δ k W n : + nsteps det_step n e e' → ℰ A δ (k - n) W e' → ℰ A δ k W e. +Proof. + induction 1 as [ | n e1 e2 e3 Hstep Hsteps IH] in k |-* . + - replace (k - 0) with k by lia. done. + - intros He. + eapply expr_det_step_closure; first done. + apply IH. replace (k - 1 - n) with (k - (S n)) by lia. done. +Qed. + +(** ** Compatibility lemmas *) + +Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) : Int. +Proof. + intros θ δ k W _. + eapply (sem_val_expr_rel _ _ _ _ #z). + simp type_interp. eauto. +Qed. + +Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) : Bool. +Proof. + intros θ δ k W _. + eapply (sem_val_expr_rel _ _ _ _ #b). simp type_interp. eauto. +Qed. + +Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) : Unit. +Proof. + intros θ δ k W _. + eapply (sem_val_expr_rel _ _ _ _ #LitUnit). + simp type_interp. eauto. +Qed. + +Lemma compat_var Δ Γ x A : + Γ !! x = Some A → + TY Δ; Γ ⊨ (Var x) : A. +Proof. + intros Hx θ δ k W Hctx; simpl. + specialize (sem_context_rel_vals Hctx Hx) as (e & v & He & Heq & Hv). + rewrite He. simp type_interp. + rewrite -(of_to_val _ _ Heq). + intros e' h h' W' n Hincl Hsat Hn (-> & -> & ->)%nsteps_val_inv. + rewrite to_of_val. eexists _, _. + split_and!; [done.. | ]. + replace (k -0) with k by lia. + eapply val_rel_mono_world; done. +Qed. + +Lemma compat_app Δ Γ e1 e2 A B : + TY Δ; Γ ⊨ e1 : (A → B) → + TY Δ; Γ ⊨ e2 : A → + TY Δ; Γ ⊨ (e1 e2) : B. +Proof. + intros Hfun Harg θ δ k W Hctx; simpl. + specialize (Hfun _ _ _ _ Hctx). + specialize (Harg _ _ _ _ Hctx). + + eapply (bind [AppRCtx _]); first done. + intros j v W' Hj HW Hv. simpl. + + eapply (bind [AppLCtx _ ]). + { eapply expr_rel_mono; cycle -1; [done | lia | done]. } + intros j' f W'' Hj' HW' Hf. + + simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf). + specialize (Hf v 0). + replace (j' - 0) with j' in Hf by lia. + eapply expr_det_step_closure. + { eapply det_step_beta. apply is_val_of_val. } + eapply expr_rel_mono_idx; last apply Hf; [lia | reflexivity | ]. + eapply val_rel_mono; last done; [lia | done]. +Qed. + +Lemma is_closed_subst_map_delete X Γ (x: string) θ A e: + closed X e → + subst_is_closed [] θ → + dom Γ ⊆ dom θ → + (∀ y : string, y ∈ X → y ∈ dom (<[x:=A]> Γ)) → + is_closed (x :b: []) (subst_map (delete x θ) e). +Proof. + intros He Hθ Hdom1 Hdom2. + eapply closed_subst_weaken; [ | | apply He]. + - eapply subst_is_closed_subseteq; last done. + apply map_delete_subseteq. + - intros y Hy%Hdom2 Hn. apply elem_of_list_singleton. + apply not_elem_of_dom in Hn. apply elem_of_dom in Hy. + destruct (decide (x = y)) as [<- | Hneq]; first done. + rewrite lookup_delete_ne in Hn; last done. + rewrite lookup_insert_ne in Hy; last done. + move: Hdom1. rewrite elem_of_subseteq. + move : Hn Hy. rewrite -elem_of_dom -not_elem_of_dom. + naive_solver. +Qed. + +(** Lambdas need to be closed by the context *) +Lemma compat_lam_named Δ Γ x e A B X : + closed X e → + (∀ y, y ∈ X → y ∈ dom (<[x := A]> Γ)) → + TY Δ; (<[ x := A ]> Γ) ⊨ e : B → + TY Δ; Γ ⊨ (Lam (BNamed x) e) : (A → B). +Proof. + intros Hcl Hsub Hbody θ δ k W Hctxt. simpl. + eapply (sem_val_expr_rel _ _ _ _ (LamV x _)). + simp type_interp. + eexists (BNamed x), _. split_and!; [done| | ]. + { eapply is_closed_subst_map_delete; eauto. + + eapply sem_context_rel_closed in Hctxt. naive_solver. + + eapply sem_context_rel_subset in Hctxt; naive_solver. + } + + intros v' kd W' Hv' Hincl. + specialize (Hbody (<[ x := of_val v']> θ) δ (k - kd) W'). + simpl. rewrite subst_subst_map. + 2: { by eapply sem_context_rel_closed. } + apply Hbody. + apply sem_context_rel_insert; first done. + eapply sem_context_rel_mono; [| done| done]. lia. +Qed. + +Lemma is_closed_subst_map_anon X Γ θ e: + closed X e → + subst_is_closed [] θ → + dom Γ ⊆ dom θ → + (∀ y, y ∈ X → y ∈ dom Γ) → + is_closed [] (subst_map θ e). +Proof. + intros He Hθ Hdom1 Hdom2. + eapply closed_subst_weaken; [ | | apply He]. + - eapply subst_is_closed_subseteq; done. + - intros y Hy%Hdom2 Hn. + apply not_elem_of_dom in Hn. apply elem_of_dom in Hy. + move: Hdom1. rewrite elem_of_subseteq. + move : Hn Hy. rewrite -elem_of_dom -not_elem_of_dom. + naive_solver. +Qed. + +Lemma compat_lam_anon Δ Γ e A B X : + closed X e → + (∀ y, y ∈ X → y ∈ dom Γ) → + TY Δ; Γ ⊨ e : B → + TY Δ; Γ ⊨ (Lam BAnon e) : (A → B). +Proof. + intros Hcl Hsub Hbody θ δ k W Hctxt. simpl. + eapply (sem_val_expr_rel _ _ _ _ (LamV BAnon _)). + simp type_interp. + eexists BAnon, _. split_and!; [done| | ]. + { eapply is_closed_subst_map_anon; eauto. + + eapply sem_context_rel_closed in Hctxt. naive_solver. + + eapply sem_context_rel_subset in Hctxt; naive_solver. + } + + intros v' kd W' Hv' Hincl. + apply (Hbody θ δ (k - kd) W'). + eapply sem_context_rel_mono; [ | done..]. lia. +Qed. + +Lemma compat_int_binop Δ Γ op e1 e2 : + bin_op_typed op Int Int Int → + TY Δ; Γ ⊨ e1 : Int → + TY Δ; Γ ⊨ e2 : Int → + TY Δ; Γ ⊨ (BinOp op e1 e2) : Int. +Proof. + intros Hop He1 He2 θ δ k W Hctx. simpl. + specialize (He1 _ _ _ _ Hctx). + specialize (He2 _ _ _ _ Hctx). + + eapply (bind [BinOpRCtx _ _]); first done. + intros j v2 W' Hj HW Hv2. simpl. + + eapply (bind [BinOpLCtx _ _ ]). + { eapply expr_rel_mono; last done; [lia | done]. } + intros j' v1 W'' Hj' HW' Hv1. + + simp type_interp. intros e' h h' W''' n Hincl' Hsat' Hn Hred. + simp type_interp in Hv1. simp type_interp in Hv2. + destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->). + + inversion Hop; subst; simpl. + all: eapply det_step_red in Hred as [ ? Hred]; [ | eapply det_step_binop; done]. + all: apply nsteps_val_inv in Hred as (? & -> & ->). + all: eexists _, W'''; simpl; split_and!; [done.. | ]. + all: simp type_interp; eauto. +Qed. + +Lemma compat_int_bool_binop Δ Γ op e1 e2 : + bin_op_typed op Int Int Bool → + TY Δ; Γ ⊨ e1 : Int → + TY Δ; Γ ⊨ e2 : Int → + TY Δ; Γ ⊨ (BinOp op e1 e2) : Bool. +Proof. + intros Hop He1 He2 θ δ k W Hctx. simpl. + specialize (He1 _ _ _ _ Hctx). + specialize (He2 _ _ _ _ Hctx). + + eapply (bind [BinOpRCtx _ _]); first done. + intros j v2 W' Hj HW Hv2. simpl. + + eapply (bind [BinOpLCtx _ _ ]). + { eapply expr_rel_mono; last done; [lia | done]. } + intros j' v1 W'' Hj' HW' Hv1. + + simp type_interp. intros e' h h' W''' n Hincl' Hsat' Hn Hred. + simp type_interp in Hv1. simp type_interp in Hv2. + destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->). + + inversion Hop; subst; simpl. + all: eapply det_step_red in Hred as [ ? Hred]; [ | eapply det_step_binop; done]. + all: apply nsteps_val_inv in Hred as (? & -> & ->). + all: eexists _, _; simpl; split_and!; [done.. | ]. + all: simp type_interp; eauto. +Qed. + +Lemma compat_unop Δ Γ op A B e : + un_op_typed op A B → + TY Δ; Γ ⊨ e : A → + TY Δ; Γ ⊨ (UnOp op e) : B. +Proof. + intros Hop He θ δ k W Hctx. simpl. + specialize (He _ _ _ _ Hctx). + + eapply (bind [UnOpCtx _]); first done. + intros j v W' Hj HW' Hv. simpl. + + simp type_interp. intros e' h h' W'' n HWincl' Hsat' Hn Hred. + inversion Hop; subst. + all: simp type_interp in Hv; destruct Hv as (? & ->). + all: eapply det_step_red in Hred as [ ? Hred]; [ | eapply det_step_unop; done]. + all: apply nsteps_val_inv in Hred as (? & -> & ->). + all: eexists _, _; simpl; split_and!; [done.. | ]. + all: simp type_interp; eauto. +Qed. + +Lemma compat_tlam Δ Γ e A X : + closed X e → + (∀ y, y ∈ X → y ∈ dom Γ) → + TY S Δ; (⤉ Γ) ⊨ e : A → + TY Δ; Γ ⊨ (Λ, e) : (∀: A). +Proof. + intros Hcl Hsub He θ δ k W Hctx. simpl. + simp type_interp. + intros e' h h' W' n HW Hsat' Hn Hred. eapply nsteps_val_inv' in Hred as ( -> & -> & ->); last done. + eexists _, _; split_and!; [done..| ]. + simp type_interp. + eexists _. split_and!; [ done | | ]. + { eapply is_closed_subst_map_anon; eauto. + + eapply sem_context_rel_closed in Hctx; naive_solver. + + eapply sem_context_rel_subset in Hctx; naive_solver. + } + intros τ. eapply He. + replace (k -0) with k by lia. eapply sem_context_rel_cons. + eapply sem_context_rel_mono_world; done. +Qed. + +Lemma compat_tapp Δ Γ e A B : + type_wf Δ B → + TY Δ; Γ ⊨ e : (∀: A) → + TY Δ; Γ ⊨ (e <>) : (A.[B/]). +Proof. + intros Hwf He θ δ k W Hctx. simpl. + + specialize (He _ _ _ _ Hctx). + eapply (bind [TAppCtx]); first done. + intros j v W' Hj HW Hv. + simp type_interp in Hv. + destruct Hv as (e' & -> & ? & He'). + + set (τ := interp_type B δ). + specialize (He' τ). simpl. + eapply expr_det_step_closure. + { apply det_step_tbeta. } + eapply sem_expr_rel_move_single_subst. + eapply expr_rel_mono_idx; last done. + lia. +Qed. + +Lemma compat_pack Γ e n A B : + type_wf n B → + type_wf (S n) A → + TY n; Γ ⊨ e : A.[B/] → + TY n; Γ ⊨ (pack e) : (∃: A). +Proof. + intros Hwf Hwf' He θ δ k W Hctx. simpl. + + specialize (He _ _ _ _ Hctx). + eapply (bind [PackCtx]); first done. + intros j v W' Hj HW Hv. + simpl. eapply (sem_val_expr_rel _ _ _ _ (PackV v)). + simp type_interp. exists v; split; first done. + exists (interp_type B δ). + apply sem_val_rel_move_single_subst. done. +Qed. + +Lemma compat_unpack n Γ A B e e' x : + type_wf n B → + TY n; Γ ⊨ e : (∃: A) → + TY S n; <[x:=A]> (⤉Γ) ⊨ e' : B.[ren (+1)] → + TY n; Γ ⊨ (unpack e as BNamed x in e') : B. +Proof. + intros Hwf He He' θ δ k W Hctx. simpl. + + specialize (He _ _ _ _ Hctx). + eapply (bind [UnpackCtx _ _]); first done. + intros j v W' Hj HW Hv. + simp type_interp in Hv. destruct Hv as (v' & -> & τ & Hv'). + simpl. + + eapply expr_det_step_closure. + { apply det_step_unpack. apply is_val_of_val. } + simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed. + + specialize (He' (<[x := of_val v']> θ) (τ.:δ) (j - 1) W'). + rewrite <-sem_expr_rel_cons in He'. + apply He'. + constructor. + { eapply val_rel_mono_idx; last done. lia. } + apply sem_context_rel_cons. + eapply sem_context_rel_mono; last done; [lia | done]. +Qed. + +Lemma compat_if n Γ e0 e1 e2 A : + TY n; Γ ⊨ e0 : Bool → + TY n; Γ ⊨ e1 : A → + TY n; Γ ⊨ e2 : A → + TY n; Γ ⊨ (if: e0 then e1 else e2) : A. +Proof. + intros He0 He1 He2 θ δ k W Hctx. simpl. + specialize (He0 _ _ _ _ Hctx). + specialize (He1 _ _ _ _ Hctx). + specialize (He2 _ _ _ _ Hctx). + + eapply (bind [IfCtx _ _]); first done. + intros j v W' Hj HW Hv. + simp type_interp in Hv. destruct Hv as (b & ->). + simpl. + + destruct b. + - eapply expr_det_step_closure. + { apply det_step_if_true. } + eapply expr_rel_mono; last done; [lia | done]. + - eapply expr_det_step_closure. + { apply det_step_if_false. } + eapply expr_rel_mono; last done; [lia | done]. +Qed. + +Lemma compat_pair Δ Γ e1 e2 A B : + TY Δ; Γ ⊨ e1 : A → + TY Δ; Γ ⊨ e2 : B → + TY Δ; Γ ⊨ (e1, e2) : A × B. +Proof. + intros He1 He2 θ δ k W Hctx. simpl. + specialize (He1 _ _ _ _ Hctx). + specialize (He2 _ _ _ _ Hctx). + + eapply (bind [PairRCtx _]); first done. + intros j v2 W' Hj HW Hv2. + eapply (bind [PairLCtx _]). + { eapply expr_rel_mono; last done; [lia | done]. } + intros j' v1 W'' Hj' HW' Hv1. + + simpl. + eapply (sem_val_expr_rel _ _ _ _ (v1, v2)%V). + simp type_interp. exists v1, v2. split_and!; first done. + - done. + - eapply val_rel_mono; last done; [lia | done]. +Qed. + +Lemma compat_fst Δ Γ e A B : + TY Δ; Γ ⊨ e : A × B → + TY Δ; Γ ⊨ Fst e : A. +Proof. + intros He θ δ k W Hctx. + specialize (He _ _ _ _ Hctx). + simpl. eapply (bind [FstCtx]); first done. + intros j v W' Hj HW Hv. + simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2). + + eapply expr_det_step_closure. + { simpl. apply det_step_fst; apply is_val_of_val. } + eapply sem_val_expr_rel. eapply val_rel_mono_idx; last done. lia. +Qed. + +Lemma compat_snd Δ Γ e A B : + TY Δ; Γ ⊨ e : A × B → + TY Δ; Γ ⊨ Snd e : B. +Proof. + intros He θ δ k w Hctx. + specialize (He _ _ _ _ Hctx). + simpl. eapply (bind [SndCtx]); first done. + intros j v W' Hj HW Hv. + simp type_interp in Hv. destruct Hv as (v1 & v2 & -> & Hv1 & Hv2). + + eapply expr_det_step_closure. + { simpl. apply det_step_snd; apply is_val_of_val. } + eapply sem_val_expr_rel. eapply val_rel_mono_idx; last done. lia. +Qed. + +Lemma compat_injl Δ Γ e A B : + TY Δ; Γ ⊨ e : A → + TY Δ; Γ ⊨ InjL e : A + B. +Proof. + intros He θ δ k W Hctx. simpl. + specialize (He _ _ _ _ Hctx). + eapply (bind [InjLCtx]); first done. + intros j v W' Hj HW Hv. + eapply (sem_val_expr_rel _ _ _ _ (InjLV v)). + simp type_interp. left. eauto. +Qed. + +Lemma compat_injr Δ Γ e A B : + TY Δ; Γ ⊨ e : B → + TY Δ; Γ ⊨ InjR e : A + B. +Proof. + intros He θ δ k W Hctx. simpl. + specialize (He _ _ _ _ Hctx). + eapply (bind [InjRCtx]); first done. + intros j v W' Hj HW Hv. + eapply (sem_val_expr_rel _ _ _ _ (InjRV v)). + simp type_interp. eauto. +Qed. + +Lemma compat_case Δ Γ e e1 e2 A B C : + TY Δ; Γ ⊨ e : B + C → + TY Δ; Γ ⊨ e1 : (B → A) → + TY Δ; Γ ⊨ e2 : (C → A) → + TY Δ; Γ ⊨ Case e e1 e2 : A. +Proof. + intros He He1 He2 θ δ k W Hctx. simpl. + specialize (He _ _ _ _ Hctx). + specialize (He1 _ _ _ _ Hctx). + specialize (He2 _ _ _ _ Hctx). + eapply (bind [CaseCtx _ _]); first done. + intros j v W' Hj HW Hv. + simp type_interp in Hv. destruct Hv as [(v' & -> & Hv') | (v' & -> & Hv')]. + - simpl. eapply expr_det_step_closure. + { apply det_step_casel. apply is_val_of_val. } + eapply (bind [AppLCtx _]). + { eapply expr_rel_mono; last done; [lia | done]. } + intros j' v W'' Hj' HW' Hv. simpl. + simp type_interp in Hv. destruct Hv as (x & e' & -> & ? & Hv). + eapply expr_det_step_closure. { apply det_step_beta. apply is_val_of_val. } + apply Hv; first done. eapply val_rel_mono; last done; [lia | done]. + - simpl. eapply expr_det_step_closure. + { apply det_step_caser. apply is_val_of_val. } + eapply (bind [AppLCtx _]). + { eapply expr_rel_mono; last done; [lia | done]. } + intros j' v W'' Hj' HW' Hv. simpl. + simp type_interp in Hv. destruct Hv as (x & e' & -> & ? & Hv). + eapply expr_det_step_closure. { apply det_step_beta. apply is_val_of_val. } + apply Hv; first done. eapply val_rel_mono; last done; [lia | done]. +Qed. + +Lemma compat_roll n Γ e A : + TY n; Γ ⊨ e : (A.[(μ: A)%ty/]) → + TY n; Γ ⊨ (roll e) : (μ: A). +Proof. + intros He θ δ k W Hctx. simpl. + specialize (He _ _ _ _ Hctx). + + eapply (bind [RollCtx]); first done. + intros j v W' Hj HW Hv. + eapply (sem_val_expr_rel _ _ _ _ (RollV v)). + + specialize (val_rel_is_closed _ _ _ _ _ Hv) as ?. + destruct j as [ | j]; simp type_interp; first by eauto. + exists v. split_and!; [done.. | ]. + intros kd. eapply val_rel_mono_idx; last done. lia. +Qed. + +Lemma compat_unroll n Γ e A : + TY n; Γ ⊨ e : (μ: A) → + TY n; Γ ⊨ (unroll e) : (A.[(μ: A)%ty/]). +Proof. + intros He θ δ k W Hctx. simpl. + specialize (He _ _ _ _ Hctx). + + eapply (bind [UnrollCtx]); first done. + intros j v W' Hj HW Hv. + destruct j as [ | j]; first by apply sem_expr_rel_zero_trivial. + simp type_interp in Hv. destruct Hv as (v' & -> & ? & Hv). + eapply expr_det_step_closure. + { simpl. apply det_step_unroll. apply is_val_of_val. } + eapply sem_val_expr_rel. apply Hv. +Qed. + + +(** A bit of theory about first-order types *) +Lemma canonical_values_int n Γ e: + TY n; Γ ⊢ e : Int → + is_val e → + ∃ n: Z, e = (#n)%E. +Proof. inversion 1; simpl; naive_solver. Qed. + +Lemma canonical_values_bool n Γ e: + TY n; Γ ⊢ e : Bool → + is_val e → + ∃ b: bool, e = (#b)%E. +Proof. inversion 1; simpl; naive_solver. Qed. + +Lemma canonical_values_unit n Γ e: + TY n; Γ ⊢ e : Unit → + is_val e → + e = (#LitUnit)%E. +Proof. inversion 1; simpl; naive_solver. Qed. + +Lemma canonical_values_prod n Γ e A B : + TY n; Γ ⊢ e : A × B → + is_val e → + ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2 ∧ + TY n; Γ ⊢ e1 : A ∧ TY n; Γ ⊢ e2 : B . +Proof. inversion 1; simpl; naive_solver. Qed. + +Lemma canonical_values_sum n Γ e A B : + TY n; Γ ⊢ e : A + B → + is_val e → + (∃ e', e = InjL e' ∧ is_val e' ∧ TY n; Γ ⊢ e' : A) ∨ (∃ e', e = InjR e' ∧ is_val e' ∧ TY n; Γ ⊢ e' : B). +Proof. inversion 1; simpl; naive_solver. Qed. + +Lemma type_wf_fotype a : type_wf 0 a. +Proof. induction a; simpl; eauto. Qed. + +(* First-order types are simple. *) +Lemma syn_fo_typed_val a δ k W v : + TY 0; ∅ ⊢ of_val v : a ↔ 𝒱 a δ k W v. +Proof. + induction a as [ | | | a1 IH1 a2 IH2 | a1 IH1 a2 IH2 ] in v |-*. + - split. + + intros [z Heq]%canonical_values_int; simplify_val; last eauto. + simp type_interp. eauto. + + simp type_interp. intros (z & ->). constructor. + - split. + + intros (b & Heq)%canonical_values_bool; simplify_val; last eauto. + simp type_interp. eauto. + + simp type_interp. intros (b & ->). constructor. + - split. + + intros Heq%canonical_values_unit; simplify_val; last eauto. + simp type_interp; eauto. + + simp type_interp. intros ->. econstructor. + - split. + + simpl. intros (e1 & e2 & ? & (v1 & Heq1)%is_val_spec & (v2 & Heq2)%is_val_spec & H1 & H2)%canonical_values_prod; last eauto. + simplify_val. apply of_val_pair_inv in H; subst v. + simp type_interp. exists v1, v2. naive_solver. + + simpl. simp type_interp. intros (v1 & v2 & -> & Hv1%IH1 & Hv2%IH2). econstructor; done. + - split. + + simpl. intros [(e & ? & (v' & Heq)%is_val_spec & H) | (e & ? & (v' & Heq)%is_val_spec & H)]%canonical_values_sum; last eauto. + * simplify_val. apply of_val_injl_inv in H0; subst v. + simp type_interp. left. naive_solver. + * simplify_val. apply of_val_injr_inv in H0; subst v. + simp type_interp. right. naive_solver. + + simpl. simp type_interp. intros [(v' & -> & Hv%IH1) | (v' & -> & Hv%IH2)]. + * simpl. eapply typed_injl; last done. apply type_wf_fotype. + * simpl. eapply typed_injr; last done. apply type_wf_fotype. +Qed. + +Lemma wsat_init_heap σ l v a W : + σ !! l = None → + wsat W σ → + TY 0; ∅ ⊢ v : a → + wsat ((λ σ, ∃ v, σ = <[l := v]> ∅ ∧ TY 0; ∅ ⊢ v : a) :: W) (init_heap l 1 v σ). +Proof. + intros. simpl. eexists. split; [exists v; split; [reflexivity | ] | split ]. + - done. + - unfold init_heap. simpl. rewrite right_id. + rewrite -insert_union_singleton_l. apply insert_mono. + apply map_empty_subseteq. + - unfold init_heap. simpl. rewrite right_id. rewrite -delete_difference map_difference_empty. + rewrite delete_union delete_singleton left_id. + rewrite delete_notin; done. +Qed. + +Lemma compat_new Δ Γ e a : + TY Δ; Γ ⊨ e : a → + TY Δ; Γ ⊨ new e : (Ref a). +Proof. + intros He θ δ k W Hctx. + eapply (bind [NewCtx]). { eapply He; done. } + intros j v W' Hj Hext Hv. + simp type_interp. + + intros e' σ σ' W'' n Hext' Hsat' Hn Hred. + eapply new_nsteps_inv in Hred as [-> Hstep]; last apply to_of_val. + eapply new_step_inv in Hstep as (l & -> & -> & ?); last apply to_of_val. + exists #l, ((λ σ', ∃ v, σ' = <[ l := v ]> ∅ ∧ TY 0; ∅ ⊢ (of_val v) : a) :: W''). + split_and!; [done | eapply suffix_cons_l; reflexivity | .. ]. + { apply wsat_init_heap; [ done.. | ]. + by eapply syn_fo_typed_val. + } + simp type_interp. + exists l. split; first done. eexists 0, _. split; done. +Qed. + +Lemma compat_load Δ Γ e a : + TY Δ; Γ ⊨ e : Ref a → + TY Δ; Γ ⊨ !e : a. +Proof. + intros He θ δ k W Hctx. + eapply (bind [LoadCtx]). { eapply He; done. } + intros j v W' Hj Hext Hv. + simp type_interp in Hv. + destruct Hv as (l & -> & (i & INV & Hlook & ->)). + + simp type_interp. + + intros e' σ σ' W'' n Hext' Hsat' Hn. + eapply wsat_lookup in Hlook; last by eapply wsat_wext. + destruct Hlook as (? & Hincl & (v & -> & ?)). + intros Hred. eapply load_nsteps_inv in Hred as [(-> & -> & -> & Hirred) | [-> Hstep]]; last apply to_of_val. + { exfalso; apply Hirred. + exists (of_val v), σ. apply base_contextual_step. + econstructor. eapply lookup_weaken; last done. apply lookup_insert. + } + eapply load_step_inv in Hstep; last apply to_of_val. + destruct Hstep as (? & v' & [= <-] & Hl & -> & ->). + eapply lookup_weaken_inv in Hincl; [ | apply lookup_insert | done]. subst v'. + rewrite to_of_val. eexists _, _. split_and!; [reflexivity | reflexivity | done | ]. + + (* use that FO types are simple. *) + apply syn_fo_typed_val; done. +Qed. + +Lemma compat_store Δ Γ e1 e2 a : + TY Δ; Γ ⊨ e1 : Ref a → + TY Δ; Γ ⊨ e2 : a → + TY Δ; Γ ⊨ (e1 <- e2) : Unit. +Proof. + (* you may find the lemmas [wsat_lookup, wsat_update] above helpful. *) + (* TODO: exercise *) +Admitted. + + + +Local Hint Resolve compat_var compat_lam_named compat_lam_anon compat_tlam compat_int compat_bool compat_unit compat_if compat_app compat_tapp compat_pack compat_unpack compat_int_binop compat_int_bool_binop compat_unop compat_pair compat_fst compat_snd compat_injl compat_injr compat_case compat_roll compat_unroll compat_new compat_store compat_load: core. + +Lemma sem_soundness Δ Γ e A : + TY Δ; Γ ⊢ e : A → + TY Δ; Γ ⊨ e : A. +Proof. + induction 1 as [ | Δ Γ x e A B Hsyn IH | Δ Γ e A B Hsyn IH| Δ Γ e A Hsyn IH| | | | | | | | | n Γ e1 e2 op A B C Hop ? ? ? ? | | | | | | | | | | | | ]; eauto. + - (* lambda *) + set (X := elements (dom (<[x := A]>Γ))). + specialize (syn_typed_closed _ _ _ _ X Hsyn) as Hcl. + eapply compat_lam_named; last done. + + apply Hcl. apply elem_of_elements. + + intros ??. by apply elem_of_elements. + - (* lambda anon *) + set (X := elements (dom Γ)). + specialize (syn_typed_closed _ _ _ _ X Hsyn) as Hcl. + eapply compat_lam_anon; last done. + + apply Hcl. apply elem_of_elements. + + intros ??. by apply elem_of_elements. + - (* tlam *) + set (X := elements (dom Γ)). + specialize (syn_typed_closed _ _ _ _ X Hsyn) as Hcl. + eapply compat_tlam; last done. + + apply Hcl. rewrite dom_fmap. apply elem_of_elements. + + intros ??. by apply elem_of_elements. + - (* binop *) inversion Hop; subst; eauto. +Qed. + +(* dummy delta which we can use if we don't care *) +Program Definition any_type : sem_type := {| sem_type_car := λ k W v, is_closed [] v |}. +Definition δ_any : var → sem_type := λ _, any_type. + + +Definition safe e h := + ∀ e' h' n, red_nsteps n e h e' h' → is_val e'. + +Lemma type_safety e A : + TY 0; ∅ ⊢ e : A → + safe e ∅. +Proof. + intros He%sem_soundness e' h' n Hred. + specialize (He ∅ δ_any (S n) []). simp type_interp in He. + rewrite subst_map_empty in He. + edestruct (He ) as (v & W' & Hv & _); [ | done | | | eassumption | ]. + - constructor. + - done. + - lia. + - rewrite <- (of_to_val _ _ Hv). apply is_val_of_val. +Qed. + + +(** Additional lemmas *) +Lemma semantic_app A B δ k W e1 e2 : + ℰ (A → B) δ k W e1 → + ℰ A δ k W e2 → + ℰ B δ k W (e1 e2). +Proof. + intros He1 He2. + eapply (bind [AppRCtx e1]); first done. + intros j v W' Hj Hincl Hv. eapply (bind [AppLCtx _]). + { eapply expr_rel_mono; [ | done..]. lia. } + intros j' v' W'' Hj' Hincl' Hf. + simp type_interp in Hf. destruct Hf as (x & e & -> & Hcl & Hf). + eapply expr_det_step_closure. + { apply det_step_beta. apply is_val_of_val. } + apply Hf; first done. + eapply val_rel_mono; [ | done..]. lia. +Qed. diff --git a/theories/type_systems/systemf_mu_state/notation.v b/theories/type_systems/systemf_mu_state/notation.v new file mode 100644 index 0000000..e4d1cd0 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/notation.v @@ -0,0 +1,113 @@ +From semantics.ts.systemf_mu_state 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 LitLoc : loc >-> 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. + +Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. +Notation "'new' e" := (New e%E) (at level 10) : expr_scope. +Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. + + +Definition assert (e : expr) : expr := + if: e then #LitUnit else (#0 #0). +Definition Or (e1 e2 : expr) : expr := + if: e1 then #true else e2. +Definition And (e1 e2 : expr) : expr := + if: e1 then e2 else #false. +Notation "e1 '||' e2" := (Or e1 e2) : expr_scope. +Notation "e1 '&&' e2" := (And e1 e2) : expr_scope. diff --git a/theories/type_systems/systemf_mu_state/parallel_subst.v b/theories/type_systems/systemf_mu_state/parallel_subst.v new file mode 100644 index 0000000..2d177d8 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/parallel_subst.v @@ -0,0 +1,279 @@ +From stdpp Require Import prelude. +From iris Require Import prelude. +From semantics.lib Require Import facts. +From semantics.ts.systemf_mu_state Require Import lang. +From semantics.lib Require Import maps. + +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) + | Load e => Load (subst_map xs e) + | Store e1 e2 => Store (subst_map xs e1) (subst_map xs e2) + | New e => New (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. diff --git a/theories/type_systems/systemf_mu_state/tactics.v b/theories/type_systems/systemf_mu_state/tactics.v new file mode 100644 index 0000000..a38ae75 --- /dev/null +++ b/theories/type_systems/systemf_mu_state/tactics.v @@ -0,0 +1,91 @@ +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_state Require Export lang notation parallel_subst 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_step := idtac. +Ltac solve_typing := + intros; + repeat (asimpl; solve_typing_step). +Ltac solve_typing_fast := + intros; + repeat (solve_typing_step). +Ltac solve_typing_step ::= + 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] *) + | |- _ < _ => simpl; 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. diff --git a/theories/type_systems/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v new file mode 100644 index 0000000..0b020ed --- /dev/null +++ b/theories/type_systems/systemf_mu_state/types.v @@ -0,0 +1,1326 @@ +From stdpp Require Import base relations. +From iris Require Import prelude. +From semantics.lib Require Import maps. +From semantics.ts.systemf_mu_state Require Import lang notation. +From Autosubst Require Export Autosubst. + +(** ** Syntactic typing *) +(** We use De Bruijn indices with the help of the Autosubst library. *) +Inductive type : Type := + (** [var] is the type of variables of Autosubst -- it unfolds to [nat] *) + | TVar : var → type + | Int + | Bool + | Unit + (** The [{bind 1 of type}] tells Autosubst to put a De Bruijn binder here *) + | TForall : {bind 1 of type} → type + | TExists : {bind 1 of type} → type + | Fun (A B : type) + | Prod (A B : type) + | Sum (A B : type) + | TMu : {bind 1 of type} → type + | Ref (A : type) +. + +(** Autosubst instances. + This lets Autosubst do its magic and derive all the substitution functions, etc. + *) +#[export] Instance Ids_type : Ids type. derive. Defined. +#[export] Instance Rename_type : Rename type. derive. Defined. +#[export] Instance Subst_type : Subst type. derive. Defined. +#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed. + +Definition typing_context := gmap string type. +Definition heap_context := gmap loc type. +Implicit Types + (Γ : typing_context) + (Σ : heap_context) + (v : val) + (e : expr) + (A B : type) +. + +Declare Scope FType_scope. +Delimit Scope FType_scope with ty. +Bind Scope FType_scope with type. +Notation "# x" := (TVar x) : FType_scope. +Infix "→" := Fun : FType_scope. +Notation "(→)" := Fun (only parsing) : FType_scope. +Notation "∀: τ" := + (TForall τ%ty) + (at level 100, τ at level 200) : FType_scope. +Notation "∃: τ" := + (TExists τ%ty) + (at level 100, τ at level 200) : FType_scope. +Infix "×" := Prod (at level 70) : FType_scope. +Notation "(×)" := Prod (only parsing) : FType_scope. +Infix "+" := Sum : FType_scope. +Notation "(+)" := Sum (only parsing) : FType_scope. +Notation "μ: A" := + (TMu A%ty) + (at level 100, A at level 200) : FType_scope. + +(** Shift all the indices in the context by one, + used when inserting a new type interpretation in Δ. *) +(* [<$>] is notation for the [fmap] operation that maps the substitution over the whole map. *) +(* [ren] is Autosubst's renaming operation -- it renames all type variables according to the given function, + in this case [(+1)] to shift the variables up by 1. *) +Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ"). + + +(** [type_wf n A] states that a type [A] has only free variables up to < [n]. + (in other words, all variables occurring free are strictly bounded by [n]). *) +Inductive type_wf : nat → type → Prop := + | type_wf_TVar m n: + m < n → + type_wf n (TVar m) + | type_wf_Int n: type_wf n Int + | type_wf_Bool n : type_wf n Bool + | type_wf_Unit n : type_wf n Unit + | type_wf_TForall n A : + type_wf (S n) A → + type_wf n (TForall A) + | type_wf_TExists n A : + type_wf (S n) A → + type_wf n (TExists A) + | type_wf_Fun n A B: + type_wf n A → + type_wf n B → + type_wf n (Fun A B) + | type_wf_Prod n A B : + type_wf n A → + type_wf n B → + type_wf n (Prod A B) + | type_wf_Sum n A B : + type_wf n A → + type_wf n B → + type_wf n (Sum A B) + | type_wf_mu n A : + type_wf (S n) A → + type_wf n (μ: A) + | type_wf_ref n A : + type_wf n A → + type_wf n (Ref A) +. +#[export] Hint Constructors type_wf : core. + +Inductive bin_op_typed : bin_op → type → type → type → Prop := + | plus_op_typed : bin_op_typed PlusOp Int Int Int + | minus_op_typed : bin_op_typed MinusOp Int Int Int + | mul_op_typed : bin_op_typed MultOp Int Int Int + | lt_op_typed : bin_op_typed LtOp Int Int Bool + | le_op_typed : bin_op_typed LeOp Int Int Bool + | eq_op_typed : bin_op_typed EqOp Int Int Bool. +#[export] Hint Constructors bin_op_typed : core. + +Inductive un_op_typed : un_op → type → type → Prop := + | neg_op_typed : un_op_typed NegOp Bool Bool + | minus_un_op_typed : un_op_typed MinusUnOp Int Int. + +Reserved Notation "'TY' Σ ; n ; Γ ⊢ e : A" (at level 74, e, A at next level). +Inductive syn_typed : heap_context → nat → typing_context → expr → type → Prop := + | typed_var Σ n Γ x A : + Γ !! x = Some A → + TY Σ; n; Γ ⊢ (Var x) : A + | typed_lam Σ n Γ x e A B : + TY Σ; n ; (<[ x := A]> Γ) ⊢ e : B → + type_wf n A → + TY Σ; n; Γ ⊢ (Lam (BNamed x) e) : (A → B) + | typed_lam_anon Σ n Γ e A B : + TY Σ; n ; Γ ⊢ e : B → + type_wf n A → + TY Σ; n; Γ ⊢ (Lam BAnon e) : (A → B) + | typed_tlam Σ n Γ e A : + (* we need to shift the context up as we descend under a binder *) + TY (⤉ Σ); S n; (⤉ Γ) ⊢ e : A → + TY Σ; n; Γ ⊢ (Λ, e) : (∀: A) + | typed_tapp Σ n Γ A B e : + TY Σ; n; Γ ⊢ e : (∀: A) → + type_wf n B → + (* A.[B/] is the notation for Autosubst's substitution operation that + replaces variable 0 by [B] *) + TY Σ; n; Γ ⊢ (e <>) : (A.[B/]) + | typed_pack Σ n Γ A B e : + type_wf n B → + type_wf (S n) A → + TY Σ; n; Γ ⊢ e : (A.[B/]) → + TY Σ; n; Γ ⊢ (pack e) : (∃: A) + | typed_unpack Σ n Γ A B e e' x : + type_wf n B → (* we should not leak the existential! *) + TY Σ; n; Γ ⊢ e : (∃: A) → + (* As we descend under a type variable binder for the typing of [e'], + we need to shift the indices in [Γ] and [B] up by one. + On the other hand, [A] is already defined under this binder, so we need not shift it. + *) + TY (⤉ Σ); (S n); (<[x := A]>(⤉Γ)) ⊢ e' : (B.[ren (+1)]) → + TY Σ; n; Γ ⊢ (unpack e as BNamed x in e') : B + | typed_int Σ n Γ z : TY Σ; n; Γ ⊢ (Lit $ LitInt z) : Int + | typed_bool Σ n Γ b : TY Σ; n; Γ ⊢ (Lit $ LitBool b) : Bool + | typed_unit Σ n Γ : TY Σ; n; Γ ⊢ (Lit $ LitUnit) : Unit + | typed_if Σ n Γ e0 e1 e2 A : + TY Σ; n; Γ ⊢ e0 : Bool → + TY Σ; n; Γ ⊢ e1 : A → + TY Σ; n; Γ ⊢ e2 : A → + TY Σ; n; Γ ⊢ If e0 e1 e2 : A + | typed_app Σ n Γ e1 e2 A B : + TY Σ; n; Γ ⊢ e1 : (A → B) → + TY Σ; n; Γ ⊢ e2 : A → + TY Σ; n; Γ ⊢ (e1 e2)%E : B + | typed_binop Σ n Γ e1 e2 op A B C : + bin_op_typed op A B C → + TY Σ; n; Γ ⊢ e1 : A → + TY Σ; n; Γ ⊢ e2 : B → + TY Σ; n; Γ ⊢ BinOp op e1 e2 : C + | typed_unop Σ n Γ e op A B : + un_op_typed op A B → + TY Σ; n; Γ ⊢ e : A → + TY Σ; n; Γ ⊢ UnOp op e : B + | typed_pair Σ n Γ e1 e2 A B : + TY Σ; n; Γ ⊢ e1 : A → + TY Σ; n; Γ ⊢ e2 : B → + TY Σ; n; Γ ⊢ (e1, e2) : A × B + | typed_fst Σ n Γ e A B : + TY Σ; n; Γ ⊢ e : A × B → + TY Σ; n; Γ ⊢ Fst e : A + | typed_snd Σ n Γ e A B : + TY Σ; n; Γ ⊢ e : A × B → + TY Σ; n; Γ ⊢ Snd e : B + | typed_injl Σ n Γ e A B : + type_wf n B → + TY Σ; n; Γ ⊢ e : A → + TY Σ; n; Γ ⊢ InjL e : A + B + | typed_injr Σ n Γ e A B : + type_wf n A → + TY Σ; n; Γ ⊢ e : B → + TY Σ; n; Γ ⊢ InjR e : A + B + | typed_case Σ n Γ e e1 e2 A B C : + TY Σ; n; Γ ⊢ e : B + C → + TY Σ; n; Γ ⊢ e1 : (B → A) → + TY Σ; n; Γ ⊢ e2 : (C → A) → + TY Σ; n; Γ ⊢ Case e e1 e2 : A + | typed_roll Σ n Γ e A : + TY Σ; n; Γ ⊢ e : (A.[(μ: A)/]) → + TY Σ; n; Γ ⊢ (roll e) : (μ: A) + | typed_unroll Σ n Γ e A : + TY Σ; n; Γ ⊢ e : (μ: A) → + TY Σ; n; Γ ⊢ (unroll e) : (A.[(μ: A)/]) + | typed_loc Σ Δ Γ l A : + Σ !! l = Some A → + TY Σ; Δ; Γ ⊢ (Lit $ LitLoc l) : (Ref A) + | typed_load Σ Δ Γ e A : + TY Σ; Δ; Γ ⊢ e : (Ref A) → + TY Σ; Δ; Γ ⊢ !e : A + | typed_store Σ Δ Γ e1 e2 A : + TY Σ; Δ; Γ ⊢ e1 : (Ref A) → + TY Σ; Δ; Γ ⊢ e2 : A → + TY Σ; Δ; Γ ⊢ (e1 <- e2) : Unit + | typed_new Σ Δ Γ e A : + TY Σ; Δ; Γ ⊢ e : A → + TY Σ; Δ; Γ ⊢ (new e) : Ref A +where "'TY' Σ ; n ; Γ ⊢ e : A" := (syn_typed Σ n Γ e%E A%ty). +#[export] Hint Constructors syn_typed : core. + +(** Examples *) +Goal TY ∅; 0; ∅ ⊢ (λ: "x", #1 + "x")%E : (Int → Int). +Proof. eauto. Qed. +(** [∀: #0 → #0] corresponds to [∀ α. α → α] with named binders. *) +Goal TY ∅; 0; ∅ ⊢ (Λ, λ: "x", "x")%E : (∀: #0 → #0). +Proof. repeat econstructor. Qed. +Goal TY ∅; 0; ∅ ⊢ (pack ((λ: "x", "x"), #42)) : ∃: (#0 → #0) × #0. +Proof. + apply (typed_pack _ _ _ _ Int). + - eauto. + - repeat econstructor. + - (* [asimpl] is Autosubst's tactic for simplifying goals involving type substitutions. *) + asimpl. eauto. +Qed. +Goal TY ∅; 0; ∅ ⊢ (unpack (pack ((λ: "x", "x"), #42)) as "y" in (λ: "x", #1337) ((Fst "y") (Snd "y"))) : Int. +Proof. + (* if we want to typecheck stuff with existentials, we need a bit more explicit proofs. + Letting eauto try to instantiate the evars becomes too expensive. *) + apply (typed_unpack _ _ _ ((#0 → #0) × #0)%ty). + - done. + - apply (typed_pack _ _ _ _ Int); asimpl; eauto. + repeat econstructor. + - eapply (typed_app _ _ _ _ _ (#0)%ty); eauto 10. +Qed. + +(** fails: we are not allowed to leak the existential *) +Goal TY ∅; 0; ∅ ⊢ (unpack (pack ((λ: "x", "x"), #42)) as "y" in (Fst "y") (Snd "y")) : #0. +Proof. + apply (typed_unpack _ _ _ ((#0 → #0) × #0)%ty). +Abort. + +(* derived typing rule for match *) +Lemma typed_match Σ n Γ e e1 e2 x1 x2 A B C : + type_wf n B → + type_wf n C → + TY Σ; n; Γ ⊢ e : B + C → + TY Σ; n; <[x1 := B]> Γ ⊢ e1 : A → + TY Σ; n; <[x2 := C]> Γ ⊢ e2 : A → + TY Σ; n; Γ ⊢ match: e with InjL (BNamed x1) => e1 | InjR (BNamed x2) => e2 end : A. +Proof. eauto. Qed. + +Lemma syn_typed_closed Σ n Γ e A X : + TY Σ; n; Γ ⊢ e : A → + (∀ x, x ∈ dom Γ → x ∈ X) → + is_closed X e. +Proof. + induction 1 as [ | ???????? IH | | Σ n Γ e A H IH | | | Σ n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | | | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done. + + { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. } + { (* lam *) apply IH. + intros y. rewrite elem_of_dom lookup_insert_is_Some. + intros [<- | [? Hy]]; first by apply elem_of_cons; eauto. + apply elem_of_cons. right. eapply Hx. by apply elem_of_dom. + } + { (* anon lam *) naive_solver. } + { (* tlam *) + eapply IH. intros x Hel. apply Hx. + by rewrite dom_fmap in Hel. + } + 3: { (* unpack *) + apply andb_True; split. + - apply IH1. apply Hx. + - apply IH2. intros y. rewrite elem_of_dom lookup_insert_is_Some. + intros [<- | [? Hy]]; first by apply elem_of_cons; eauto. + apply elem_of_cons. right. eapply Hx. + apply elem_of_dom. revert Hy. rewrite lookup_fmap fmap_is_Some. done. + } + (* everything else *) + all: repeat match goal with + | |- Is_true (_ && _) => apply andb_True; split + end. + all: try naive_solver. +Qed. + +(** *** Lemmas about [type_wf] *) +Lemma type_wf_mono n m A: + type_wf n A → n ≤ m → type_wf m A. +Proof. + induction 1 in m |-*; eauto with lia. +Qed. + +Lemma type_wf_rename n A δ: + type_wf n A → + (∀ i j, i < j → δ i < δ j) → + type_wf (δ n) (rename δ A). +Proof. + induction 1 in δ |-*; intros Hmon; simpl; eauto. + all: econstructor; eapply type_wf_mono; first eapply IHtype_wf; last done. + all: intros i j Hlt; destruct i, j; simpl; try lia. + all: rewrite -Nat.succ_lt_mono; eapply Hmon; lia. +Qed. + +(** [A.[σ]], i.e. [A] with the substitution [σ] applied to it, is well-formed under [m] if + [A] is well-formed under [n] and all the things we substitute up to [n] are well-formed under [m]. + *) +Lemma type_wf_subst n m A σ: + type_wf n A → + (∀ x, x < n → type_wf m (σ x)) → + type_wf m A.[σ]. +Proof. + induction 1 in m, σ |-*; intros Hsub; simpl; eauto. + + econstructor; eapply IHtype_wf. + intros [|x]; rewrite /up //=. + - econstructor. lia. + - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto. + intros i j Hlt'; simpl; lia. + + econstructor; eapply IHtype_wf. + intros [|x]; rewrite /up //=. + - econstructor. lia. + - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto. + intros i j Hlt'; simpl; lia. + + econstructor. eapply IHtype_wf. + intros [|x]; rewrite /up //=. + - econstructor. lia. + - intros Hlt % Nat.succ_lt_mono. eapply type_wf_rename; eauto. + intros ???. simpl; lia. +Qed. + +Fixpoint free_vars A : nat → Prop := + match A with + | TVar n => λ m, m = n + | Int => λ _, False + | Bool => λ _, False + | Unit => λ _, False + | Fun A B => λ n, free_vars A n ∨ free_vars B n + | Prod A B => λ n, free_vars A n ∨ free_vars B n + | Sum A B => λ n, free_vars A n ∨ free_vars B n + | TForall A => λ n, free_vars A (S n) + | TExists A => λ n, free_vars A (S n) + | TMu A => λ n, free_vars A (S n) + | Ref A => λ n, free_vars A n + end. + +Definition bounded n A := + (∀ x, free_vars A x → x < n). + +Lemma type_wf_bounded n A: + type_wf n A ↔ bounded n A. +Proof. + rewrite /bounded; split. + - induction 1; simpl; try naive_solver. + + intros x Hfree % IHtype_wf. lia. + + intros x Hfree % IHtype_wf. lia. + + intros x Hfree % IHtype_wf. lia. + - induction A in n |-*; simpl; eauto. + + intros Hsub. econstructor. eapply IHA. + intros ??. destruct x as [|x]; first lia. + eapply Hsub in H. lia. + + intros Hsub. econstructor. eapply IHA. + intros ??. destruct x as [|x]; first lia. + eapply Hsub in H. lia. + + intros Hsub. econstructor; eauto. + + intros Hsub. econstructor; eauto. + + intros Hsub. econstructor; eauto. + + intros Hsub. econstructor. eapply IHA. + intros ??. destruct x as [|x]; first lia. + eapply Hsub in H. lia. +Qed. + +Lemma free_vars_rename A x δ: + free_vars A x → free_vars (rename δ A) (δ x). +Proof. + induction A in x, δ |-*; simpl; try naive_solver. + - intros Hf. apply (IHA (S x) (upren δ) Hf). + - intros Hf. apply (IHA (S x) (upren δ) Hf). + - intros Hf. apply (IHA (S x) (upren δ) Hf). +Qed. + +Lemma free_vars_subst x n A σ : + bounded n A.[σ] → free_vars A x → bounded n (σ x). +Proof. + induction A in n, σ, x |-*; simpl; try naive_solver. + - rewrite -type_wf_bounded. inversion 1; subst. revert H2; clear H. + rewrite type_wf_bounded. + intros Hbd Hfree. eapply IHA in Hbd; last done. + revert Hbd. rewrite /up //=. + intros Hbd y Hf. enough (S y < S n) by lia. + eapply Hbd. simpl. by eapply free_vars_rename. + - rewrite -type_wf_bounded. inversion 1; subst. revert H2; clear H. + rewrite type_wf_bounded. + intros Hbd Hfree. eapply IHA in Hbd; last done. + revert Hbd. rewrite /up //=. + intros Hbd y Hf. enough (S y < S n) by lia. + eapply Hbd. simpl. by eapply free_vars_rename. + - rewrite -!type_wf_bounded. inversion 1; subst. + revert H3 H4. rewrite !type_wf_bounded. naive_solver. + - rewrite -!type_wf_bounded. inversion 1; subst. + revert H3 H4. rewrite !type_wf_bounded. naive_solver. + - rewrite -!type_wf_bounded. inversion 1; subst. + revert H3 H4. rewrite !type_wf_bounded. naive_solver. + - rewrite -type_wf_bounded. inversion 1; subst. revert H2; clear H. + rewrite type_wf_bounded. + intros Hbd Hfree. eapply IHA in Hbd; last done. + revert Hbd. rewrite /up //=. + intros Hbd y Hf. enough (S y < S n) by lia. + eapply Hbd. simpl. by eapply free_vars_rename. +Qed. + +Lemma type_wf_rec_type n A: + type_wf n A.[(μ: A)%ty/] → type_wf (S n) A. +Proof. + rewrite !type_wf_bounded. intros Hbound x Hfree. + eapply free_vars_subst in Hbound; last done. + destruct x as [|x]; first lia; simpl in Hbound. + eapply type_wf_bounded in Hbound. inversion Hbound; subst; lia. +Qed. + +Lemma type_wf_single_subst n A B: type_wf n B → type_wf (S n) A → type_wf n A.[B/]. +Proof. + intros HB HA. eapply type_wf_subst; first done. + intros [|x]; simpl; eauto. + intros ?; econstructor. lia. +Qed. + +(** We lift [type_wf] to well-formedness of contexts *) +Definition ctx_wf n Γ := (∀ x A, Γ !! x = Some A → type_wf n A). + +Lemma ctx_wf_empty n : ctx_wf n ∅. +Proof. rewrite /ctx_wf. set_solver. Qed. + +Lemma ctx_wf_insert n x Γ A: ctx_wf n Γ → type_wf n A → ctx_wf n (<[x := A]> Γ). +Proof. intros H1 H2 y B. rewrite lookup_insert_Some. naive_solver. Qed. + +Lemma ctx_wf_up n Γ: + ctx_wf n Γ → ctx_wf (S n) (⤉Γ). +Proof. + intros Hwf x A; rewrite lookup_fmap. + intros (B & Hlook & ->) % fmap_Some. + asimpl. eapply type_wf_subst; first eauto. + intros y Hlt. simpl. econstructor. lia. +Qed. + +Definition heap_ctx_wf Δ (Σ: heap_context) := (∀ x A, Σ !! x = Some A → type_wf Δ A). + +Lemma heap_ctx_wf_empty n : heap_ctx_wf n ∅. +Proof. rewrite /heap_ctx_wf. set_solver. Qed. + +Lemma heap_ctx_wf_insert n l Σ A: heap_ctx_wf n Σ → type_wf n A → heap_ctx_wf n (<[l := A]> Σ). +Proof. intros H1 H2 y B. rewrite lookup_insert_Some. naive_solver. Qed. + +Lemma heap_ctx_wf_up n Σ: + heap_ctx_wf n Σ → heap_ctx_wf (S n) (⤉Σ). +Proof. + intros Hwf x A; rewrite lookup_fmap. + intros (B & Hlook & ->) % fmap_Some. + asimpl. eapply type_wf_subst; first eauto. + intros y Hlt. simpl. econstructor. lia. +Qed. + +#[global] +Hint Resolve ctx_wf_empty ctx_wf_insert ctx_wf_up heap_ctx_wf_up heap_ctx_wf_empty heap_ctx_wf_empty : core. + +(** Well-typed terms at [A] under a well-formed context have well-formed types [A].*) +Lemma syn_typed_wf Σ n Γ e A: + ctx_wf n Γ → + heap_ctx_wf n Σ → + TY Σ; n; Γ ⊢ e : A → + type_wf n A. +Proof. + intros Hwf Hhwf; induction 1 as [ | Σ n Γ x e A B Hty IH Hwfty | | Σ n Γ e A Hty IH | Σ n Γ A B e Hty IH Hwfty | Σ n Γ A B e Hwfty Hty IH| | | | | | Σ n Γ e1 e2 A B HtyA IHA HtyB IHB | Σ n Γ e1 e2 op A B C Hop HtyA IHA HtyB IHB | Σ n Γ e op A B Hop H IH | Σ n Γ e1 e2 A B HtyA IHA HtyB IHB | Σ n Γ e A B Hty IH | Σ n Γ e A B Hty IH | Σ n Γ e A B Hwfty Hty IH | Σ n Γ e A B Hwfty Hty IH| Σ n Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2 | Σ n Γ e A Hty IH | Σ n Γ e A Hty IH | Σ n Γ l A Hlook| Σ n Γ e A Hty IH | Σ n Γ e1 e2 A Hty1 IH1 Hty2 IH2 | Σ n Γ e A Hty IH]; eauto. + - eapply type_wf_single_subst; first done. + specialize (IH Hwf Hhwf) as Hwf'. + by inversion Hwf'. + - specialize (IHA Hwf Hhwf) as Hwf'. + by inversion Hwf'; subst. + - inversion Hop; subst; eauto. + - inversion Hop; subst; eauto. + - specialize (IH Hwf Hhwf) as Hwf'. by inversion Hwf'; subst. + - specialize (IH Hwf Hhwf) as Hwf'. by inversion Hwf'; subst. + - specialize (IHe1 Hwf Hhwf) as Hwf''. by inversion Hwf''; subst. + - specialize (IH Hwf Hhwf) as Hwf'%type_wf_rec_type. + by econstructor. + - eapply type_wf_single_subst; first by apply IH. + specialize (IH Hwf Hhwf) as Hwf'. + by inversion Hwf'. + - specialize (IH Hwf Hhwf) as Hwf'. by inversion Hwf'. +Qed. + +Lemma renaming_ctx_inclusion Γ Δ : Γ ⊆ Δ → ⤉Γ ⊆ ⤉Δ. +Proof. + eapply map_fmap_mono. +Qed. + +Lemma renaming_heap_ctx_inclusion Σ Σ' : Σ ⊆ Σ' → ⤉Σ ⊆ ⤉Σ'. +Proof. + eapply map_fmap_mono. +Qed. + +Lemma typed_weakening n m Γ Δ e A Σ Σ' : + TY Σ; n; Γ ⊢ e : A → + Γ ⊆ Δ → + Σ ⊆ Σ' → + n ≤ m → + TY Σ'; m; Δ ⊢ e : A. +Proof. + induction 1 as [| Σ n Γ x e A B Htyp IH | | Σ n Γ e A Htyp IH | | | Σ n Γ A B e e' x Hwf H1 IH1 H2 IH2 | | | | | | | | | | | | | | | | Σ n Γ l A Hlook | | | ] in Σ', Δ, m |-*; intros Hsub1 Hsub2 Hle; eauto using type_wf_mono. + - (* var *) econstructor. by eapply lookup_weaken. + - (* lam *) econstructor; last by eapply type_wf_mono. eapply IH; eauto. by eapply insert_mono. + - (* tlam *) econstructor. eapply IH; last by lia. + + by eapply renaming_ctx_inclusion. + + by eapply renaming_heap_ctx_inclusion. + - (* pack *) + econstructor; last naive_solver. all: (eapply type_wf_mono; [ done | lia]). + - (* unpack *) econstructor. + + eapply type_wf_mono; done. + + eapply IH1; done. + + eapply IH2; last lia. + * apply insert_mono. by apply renaming_ctx_inclusion. + * by apply renaming_heap_ctx_inclusion. + - (* loc *) + econstructor; by eapply lookup_weaken. +Qed. + +Lemma type_wf_subst_dom σ τ n A: + type_wf n A → + (∀ m, m < n → σ m = τ m) → + A.[σ] = A.[τ]. +Proof. + induction 1 in σ, τ |-*; simpl; eauto. + - (* tforall *) + intros Heq; asimpl. f_equal. + eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done. + intros Hlt. f_equal. eapply Heq. lia. + - (* texists *) + intros Heq; asimpl. f_equal. + eapply IHtype_wf. intros [ | m]; rewrite /up; simpl; first done. + intros Hlt. f_equal. apply Heq. lia. + - (* fun *) intros ?. f_equal; eauto. + - (* prod *) intros ?. f_equal; eauto. + - (* sum *) intros ?. f_equal; eauto. + - (* rec *) + intros Heq; asimpl. f_equal. + eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done. + intros Hlt. f_equal. eapply Heq. lia. + - (* ref *) + intros ?. f_equal. eapply IHtype_wf. done. +Qed. + +Lemma type_wf_closed A σ: + type_wf 0 A → + A.[σ] = A. +Proof. + intros Hwf; erewrite (type_wf_subst_dom _ (ids) 0). + - by asimpl. + - done. + - intros ??; lia. +Qed. + +Lemma heap_ctx_closed Σ σ: + heap_ctx_wf 0 Σ → + fmap (subst σ) Σ = Σ. +Proof. + intros Hwf. eapply stdpp.fin_maps.map_eq; intros l. + rewrite lookup_fmap. destruct lookup as [A|]eqn: H; last done; simpl. + f_equal. eapply type_wf_closed. by eapply Hwf. +Qed. + + + +(** Typing inversion lemmas *) +Lemma var_inversion Σ Γ n (x: string) A: TY Σ; n; Γ ⊢ x : A → Γ !! x = Some A. +Proof. inversion 1; subst; auto. Qed. + +Lemma lam_inversion Σ n Γ (x: string) e C: + TY Σ; n; Γ ⊢ (λ: x, e) : C → + ∃ A B, C = (A → B)%ty ∧ type_wf n A ∧ TY Σ; n; <[x:=A]> Γ ⊢ e : B. +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma lam_anon_inversion Σ n Γ e C: + TY Σ; n; Γ ⊢ (λ: <>, e) : C → + ∃ A B, C = (A → B)%ty ∧ type_wf n A ∧ TY Σ; n; Γ ⊢ e : B. +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma app_inversion Σ n Γ e1 e2 B: + TY Σ; n; Γ ⊢ e1 e2 : B → + ∃ A, TY Σ; n; Γ ⊢ e1 : (A → B) ∧ TY Σ; n; Γ ⊢ e2 : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma if_inversion Σ n Γ e0 e1 e2 B: + TY Σ; n; Γ ⊢ If e0 e1 e2 : B → + TY Σ; n; Γ ⊢ e0 : Bool ∧ TY Σ; n; Γ ⊢ e1 : B ∧ TY Σ; n; Γ ⊢ e2 : B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma binop_inversion Σ n Γ op e1 e2 B: + TY Σ; n; Γ ⊢ BinOp op e1 e2 : B → + ∃ A1 A2, bin_op_typed op A1 A2 B ∧ TY Σ; n; Γ ⊢ e1 : A1 ∧ TY Σ; n; Γ ⊢ e2 : A2. +Proof. inversion 1; subst; eauto. Qed. + +Lemma unop_inversion Σ n Γ op e B: + TY Σ; n; Γ ⊢ UnOp op e : B → + ∃ A, un_op_typed op A B ∧ TY Σ; n; Γ ⊢ e : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma type_app_inversion Σ n Γ e B: + TY Σ; n; Γ ⊢ e <> : B → + ∃ A C, B = A.[C/] ∧ type_wf n C ∧ TY Σ; n; Γ ⊢ e : (∀: A). +Proof. inversion 1; subst; eauto. Qed. + +Lemma type_lam_inversion Σ n Γ e B: + TY Σ; n; Γ ⊢ (Λ,e) : B → + ∃ A, B = (∀: A)%ty ∧ TY ⤉Σ; (S n); ⤉Γ ⊢ e : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma type_pack_inversion Σ n Γ e B : + TY Σ; n; Γ ⊢ (pack e) : B → + ∃ A C, B = (∃: A)%ty ∧ TY Σ; n; Γ ⊢ e : (A.[C/])%ty ∧ type_wf n C ∧ type_wf (S n) A. +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma type_unpack_inversion Σ n Γ e e' x B : + TY Σ; n; Γ ⊢ (unpack e as x in e') : B → + ∃ A x', x = BNamed x' ∧ type_wf n B ∧ TY Σ; n; Γ ⊢ e : (∃: A) ∧ TY ⤉Σ; S n; <[x' := A]> (⤉Γ) ⊢ e' : (B.[ren (+1)]). +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma pair_inversion Σ n Γ e1 e2 C : + TY Σ; n; Γ ⊢ (e1, e2) : C → + ∃ A B, C = (A × B)%ty ∧ TY Σ; n; Γ ⊢ e1 : A ∧ TY Σ; n; Γ ⊢ e2 : B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma fst_inversion Σ n Γ e A : + TY Σ; n; Γ ⊢ Fst e : A → + ∃ B, TY Σ; n; Γ ⊢ e : A × B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma snd_inversion Σ n Γ e B : + TY Σ; n; Γ ⊢ Snd e : B → + ∃ A, TY Σ; n; Γ ⊢ e : A × B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma injl_inversion Σ n Γ e C : + TY Σ; n; Γ ⊢ InjL e : C → + ∃ A B, C = (A + B)%ty ∧ TY Σ; n; Γ ⊢ e : A ∧ type_wf n B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma injr_inversion Σ n Γ e C : + TY Σ; n; Γ ⊢ InjR e : C → + ∃ A B, C = (A + B)%ty ∧ TY Σ; n; Γ ⊢ e : B ∧ type_wf n A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma case_inversion Σ n Γ e e1 e2 A : + TY Σ; n; Γ ⊢ Case e e1 e2 : A → + ∃ B C, TY Σ; n; Γ ⊢ e : B + C ∧ TY Σ; n; Γ ⊢ e1 : (B → A) ∧ TY Σ; n; Γ ⊢ e2 : (C → A). +Proof. inversion 1; subst; eauto. Qed. + +Lemma roll_inversion Σ n Γ e B: + TY Σ; n; Γ ⊢ (roll e) : B → + ∃ A, B = (μ: A)%ty ∧ TY Σ; n; Γ ⊢ e : A.[μ: A/]. +Proof. inversion 1; subst; eauto. Qed. + +Lemma unroll_inversion Σ n Γ e B: + TY Σ; n; Γ ⊢ (unroll e) : B → + ∃ A, B = (A.[μ: A/])%ty ∧ TY Σ; n; Γ ⊢ e : μ: A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma new_inversion Σ n Γ e B : + TY Σ; n; Γ ⊢ (new e) : B → + ∃ A, B = Ref A ∧ TY Σ; n; Γ ⊢ e : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma load_inversion Σ n Γ e B: + TY Σ; n; Γ ⊢ ! e : B → + TY Σ; n; Γ ⊢ e : Ref B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma store_inversion Σ n Γ e1 e2 B: + TY Σ; n; Γ ⊢ (e1 <- e2) : B → + ∃ A, B = Unit ∧ TY Σ; n; Γ ⊢ e1 : Ref A ∧ TY Σ; n; Γ ⊢ e2 : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma typed_substitutivity Σ n e e' Γ (x: string) A B : + heap_ctx_wf 0 Σ → + TY Σ; 0; ∅ ⊢ e' : A → + TY Σ; n; (<[x := A]> Γ) ⊢ e : B → + TY Σ; n; Γ ⊢ lang.subst x e' e : B. +Proof. + intros HwfΣ He'. induction e as [| y | y | | | | | | | | | | | | | | | | | | | ] in n, B, Γ |-*; simpl. + - inversion 1; subst; auto. + - intros Hp % var_inversion. + destruct (decide (x = y)). + + subst. rewrite lookup_insert in Hp. injection Hp as ->. + eapply typed_weakening; [done| | done |lia]. apply map_empty_subseteq. + + rewrite lookup_insert_ne in Hp; last done. auto. + - destruct y as [ | y]. + { intros (A' & C & -> & Hwf & Hty) % lam_anon_inversion. + econstructor; last done. destruct decide as [Heq|]. + + congruence. + + eauto. + } + intros (A' & C & -> & Hwf & Hty) % lam_inversion. + econstructor; last done. destruct decide as [Heq|]. + + injection Heq as [= ->]. by rewrite insert_insert in Hty. + + rewrite insert_commute in Hty; last naive_solver. eauto. + - intros (C & Hty1 & Hty2) % app_inversion. eauto. + - intros (? & Hop & H1) % unop_inversion. + destruct op; inversion Hop; subst; eauto. + - intros (? & ? & Hop & H1 & H2) % binop_inversion. + destruct op; inversion Hop; subst; eauto. + - intros (H1 & H2 & H3)%if_inversion. naive_solver. + - intros (C & D & -> & Hwf & Hty) % type_app_inversion. eauto. + - intros (C & -> & Hty)%type_lam_inversion. econstructor. + rewrite heap_ctx_closed //=. + eapply IHe. revert Hty. rewrite fmap_insert. + eapply syn_typed_wf in He'; eauto. + rewrite heap_ctx_closed //=. + rewrite type_wf_closed; eauto. + - intros (C & D & -> & Hty & Hwf1 & Hwf2)%type_pack_inversion. + econstructor; [done..|]. apply IHe. done. + - intros (C & x' & -> & Hwf & Hty1 & Hty2)%type_unpack_inversion. + econstructor; first done. + + eapply IHe1. done. + + destruct decide as [Heq | ]. + * injection Heq as [= ->]. by rewrite fmap_insert insert_insert in Hty2. + * rewrite fmap_insert in Hty2. rewrite insert_commute in Hty2; last naive_solver. + revert Hty2. rewrite heap_ctx_closed//=. intros Hty2. + eapply IHe2. rewrite type_wf_closed in Hty2; first done. + eapply syn_typed_wf; last apply He'; eauto. + - intros (? & ? & -> & ? & ?) % pair_inversion. eauto. + - intros (? & ?)%fst_inversion. eauto. + - intros (? & ?)%snd_inversion. eauto. + - intros (? & ? & -> & ? & ?)%injl_inversion. eauto. + - intros (? & ? & -> & ? & ?)%injr_inversion. eauto. + - intros (? & ? & ? & ? & ?)%case_inversion. eauto. + - intros (C & -> & Hty) % roll_inversion. eauto. + - intros (C & -> & Hty) % unroll_inversion. eauto. + - intros Hty % load_inversion. eauto. + - intros (C & -> & Hty1 & Hty2)% store_inversion. eauto. + - intros (C & -> & Hty) % new_inversion. eauto. +Qed. + +(** Canonical values *) +Lemma canonical_values_arr Σ n Γ e A B: + TY Σ; n; Γ ⊢ e : (A → B) → + is_val e → + ∃ x e', e = (λ: x, e')%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_forall Σ n Γ e A: + TY Σ; n; Γ ⊢ e : (∀: A)%ty → + is_val e → + ∃ e', e = (Λ, e')%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_exists Σ n Γ e A : + TY Σ; n; Γ ⊢ e : (∃: A) → + is_val e → + ∃ e', e = (pack e')%E. +Proof. inversion 1; simpl; naive_solver. Qed. + +Lemma canonical_values_int Σ n Γ e: + TY Σ; n; Γ ⊢ e : Int → + is_val e → + ∃ n: Z, e = (#n)%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_bool Σ n Γ e: + TY Σ; n; Γ ⊢ e : Bool → + is_val e → + ∃ b: bool, e = (#b)%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_unit Σ n Γ e: + TY Σ; n; Γ ⊢ e : Unit → + is_val e → + e = (#LitUnit)%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_prod Σ n Γ e A B : + TY Σ; n; Γ ⊢ e : A × B → + is_val e → + ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_sum Σ n Γ e A B : + TY Σ; n; Γ ⊢ e : A + B → + is_val e → + (∃ e', e = InjL e' ∧ is_val e') ∨ (∃ e', e = InjR e' ∧ is_val e'). +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_rec Σ n Γ e A: + TY Σ; n; Γ ⊢ e : (μ: A) → + is_val e → + ∃ e', e = (roll e')%E ∧ is_val e'. +Proof. + inversion 1; simpl; subst; naive_solver. +Qed. + +Lemma canonical_values_ref Σ n Γ e A: + TY Σ; n; Γ ⊢ e : Ref A → + is_val e → + ∃ l: loc, e = (#l)%E ∧ Σ !! l = Some A. +Proof. + inversion 1; simpl; subst; naive_solver. +Qed. + +(** Progress *) +Definition heap_type (h: heap) Σ := + ∀ l A, Σ !! l = Some A → ∃ v, h !! l = Some v ∧ TY Σ; 0; ∅ ⊢ of_val v : A. + +Lemma typed_progress Σ e h A: + heap_type h Σ → + TY Σ; 0; ∅ ⊢ e : A → + is_val e ∨ reducible e h. +Proof. + intros Hheap. remember ∅ as Γ. remember 0 as n. + induction 1 as [| | | | Σ n Γ A B e Hty IH | Σ n Γ A B e Hwf Hwf' Hty IH | Σ n Γ A B e e' x Hwf Hty1 IH1 Hty2 IH2 | | | | Σ n Γ e0 e1 e2 A Hty1 IH1 Hty2 IH2 Hty3 IH3 | Σ n Γ e1 e2 A B Hty IH1 _ IH2 | Σ n Γ e1 e2 op A B C Hop Hty1 IH1 Hty2 IH2 | Σ n Γ e op A B Hop Hty IH | Σ n Γ e1 e2 A B Hty1 IH1 Hty2 IH2 | Σ n Γ e A B Hty IH | Σ n Γ e A B Hty IH | Σ n Γ e A B Hwf Hty IH | Σ n Γ e A B Hwf Hty IH| Σ n Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2 | Σ n Γ e A Hty IH | Σ n Γ e A Hty IH | Σ n Γ l A Hlook | Σ n Γ e A Hty IH | Σ n Γ e1 e2 A Hty1 IH1 Hty2 IH2 | Σ n Γ e A Hty IH ]. + - subst. naive_solver. + - left. done. + - left. done. + - left; done. + - right. destruct (IH Hheap HeqΓ Heqn) as [H1|H1]. + + eapply canonical_values_forall in Hty as [e' ->]; last done. + eexists _, _. eapply base_contextual_step. eapply TBetaS. + + destruct H1 as (e' & h' & H1). eexists _, _. + eapply (fill_contextual_step [TAppCtx]). done. + - (* pack *) + destruct (IH Hheap HeqΓ Heqn) as [H | H]. + + by left. + + right. destruct H as (e' & h' & H). eexists _, _. eapply (fill_contextual_step [PackCtx]). done. + - (* unpack *) + destruct (IH1 Hheap HeqΓ Heqn) as [H | H]. + + eapply canonical_values_exists in Hty1 as [e'' ->]; last done. + right. eexists _, _. eapply base_contextual_step. constructor; last done. + done. + + right. destruct H as (e'' & h'' & H). eexists _, _. + eapply (fill_contextual_step [UnpackCtx _ _]). done. + - (* int *)left. done. + - (* bool*) left. done. + - (* unit *) left. done. + - (* if *) + destruct (IH1 Hheap HeqΓ Heqn) as [H1 | H1]. + + eapply canonical_values_bool in Hty1 as (b & ->); last done. + right. destruct b; eexists _, _; eapply base_contextual_step; constructor. + + right. destruct H1 as (e0' & h' & Hstep). + eexists _, _. by eapply (fill_contextual_step [IfCtx _ _]). + - (* app *) + destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|]. + + eapply canonical_values_arr in Hty as (x & e & ->); last done. + right. eexists _, _. + eapply base_contextual_step, BetaS; eauto. + + right. eapply is_val_spec in H2 as [v Heq]. + replace e2 with (of_val v); last by eapply of_to_val. + destruct H1 as (e1' & h' & Hstep). + eexists _, _. eapply (fill_contextual_step [AppLCtx v]). done. + + right. destruct H2 as (e2' & h' & H2). + eexists _, _. eapply (fill_contextual_step [AppRCtx e1]). done. + - (* binop *) + assert (A = Int ∧ B = Int) as [-> ->]. + { inversion Hop; subst A B C; done. } + destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|]. + + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done. + eapply canonical_values_int in Hty2 as [n2 ->]; last done. + inversion Hop; subst; simpl. + all: eexists _, _; eapply base_contextual_step; eapply BinOpS; eauto. + + right. eapply is_val_spec in H2 as [v Heq]. + replace e2 with (of_val v); last by eapply of_to_val. + destruct H1 as (e1' & h' & Hstep). + eexists _, _. eapply (fill_contextual_step [BinOpLCtx op v]). done. + + right. destruct H2 as (e2' & h' & H2). + eexists _, _. eapply (fill_contextual_step [BinOpRCtx op e1]). done. + - (* unop *) + inversion Hop; subst A B op. + + right. destruct (IH Hheap HeqΓ Heqn) as [H2 | H2]. + * eapply canonical_values_bool in Hty as [b ->]; last done. + eexists _, _; eapply base_contextual_step; eapply UnOpS; eauto. + * destruct H2 as (e' & h' & H2). eexists _, _. + eapply (fill_contextual_step [UnOpCtx _]). done. + + right. destruct (IH Hheap HeqΓ Heqn) as [H2 | H2]. + * eapply canonical_values_int in Hty as [z ->]; last done. + eexists _, _; eapply base_contextual_step; eapply UnOpS; eauto. + * destruct H2 as (e' & h' & H2). eexists _, _. + eapply (fill_contextual_step [UnOpCtx _]). done. + - (* pair *) + destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|]. + + left. done. + + right. eapply is_val_spec in H2 as [v Heq]. + replace e2 with (of_val v); last by eapply of_to_val. + destruct H1 as (e1' & h' & Hstep). + eexists _, _. eapply (fill_contextual_step [PairLCtx v]). done. + + right. destruct H2 as (e2' & h' & H2). + eexists _, _. eapply (fill_contextual_step [PairRCtx e1]). done. + - (* fst *) + destruct (IH Hheap HeqΓ Heqn) as [H | H]. + + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done. + right. eexists _, _. eapply base_contextual_step. econstructor; done. + + right. destruct H as (e' & h' & H). + eexists _, _. eapply (fill_contextual_step [FstCtx]). done. + - (* snd *) + destruct (IH Hheap HeqΓ Heqn) as [H | H]. + + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done. + right. eexists _, _. eapply base_contextual_step. econstructor; done. + + right. destruct H as (e' & h' & H). + eexists _, _. eapply (fill_contextual_step [SndCtx]). done. + - (* injl *) + destruct (IH Hheap HeqΓ Heqn) as [H | H]. + + left. done. + + right. destruct H as (e' & h' & H). + eexists _, _. eapply (fill_contextual_step [InjLCtx]). done. + - (* injr *) + destruct (IH Hheap HeqΓ Heqn) as [H | H]. + + left. done. + + right. destruct H as (e' & h' & H). + eexists _, _. eapply (fill_contextual_step [InjRCtx]). done. + - (* case *) + right. destruct (IHe Hheap HeqΓ Heqn) as [H1|H1]. + + eapply canonical_values_sum in Htye as [(e' & -> & ?) | (e' & -> & ?)]; last done. + * eexists _, _. eapply base_contextual_step. econstructor. done. + * eexists _, _. eapply base_contextual_step. econstructor. done. + + destruct H1 as (e' & h' & H1). eexists _, _. + eapply (fill_contextual_step [CaseCtx e1 e2]). done. + - (* roll *) + destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred]. + + by left. + + right. destruct Hred as (e' & h' & Hred). + eexists _, _. eapply (fill_contextual_step [RollCtx]). done. + - (* unroll *) + destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred]. + + eapply canonical_values_rec in Hty as (e' & -> & Hval'); last done. + right. eexists _, _. eapply base_contextual_step. by econstructor. + + right. destruct Hred as (e' & h' & Hred). + eexists _, _. eapply (fill_contextual_step [UnrollCtx]). done. + - (* loc *) + by left. + - (* load *) + destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred]. + + eapply canonical_values_ref in Hty as (l & -> & Hlook); last done. + eapply Hheap in Hlook as (v & Hlook & Hty'). + right. do 2 eexists. eapply base_contextual_step. by econstructor. + + right. destruct Hred as (e' & h' & Hred). + do 2 eexists. eapply (fill_contextual_step [LoadCtx]). done. + - (* store *) + destruct (IH2 Hheap HeqΓ Heqn) as [H2|H2]; [destruct (IH1 Hheap HeqΓ Heqn) as [H1|H1]|]. + + right. eapply canonical_values_ref in Hty1 as (l & -> & Hlook); last done. + eapply Hheap in Hlook as (v & Hlook & Hty'). + eapply is_val_spec in H2 as (w & Heq). + do 2 eexists. eapply base_contextual_step. + econstructor; eauto. + + right. eapply is_val_spec in H2 as [v Heq]. + replace e2 with (of_val v); last by eapply of_to_val. + destruct H1 as (e1' & h' & Hstep). + do 2 eexists. eapply (fill_contextual_step [StoreLCtx v]). done. + + right. destruct H2 as (e2' & h' & H2). + do 2 eexists. eapply (fill_contextual_step [StoreRCtx e1]). done. + - (* new *) + destruct (IH Hheap HeqΓ Heqn) as [Hval|Hred]. + + right. eapply is_val_spec in Hval as [v Heq]. + do 2 eexists. eapply base_contextual_step. + eapply (NewS _ _ _ (fresh (dom h))); last done. + eapply not_elem_of_dom, is_fresh. + + right. destruct Hred as (e' & h' & Hred). + do 2 eexists. eapply (fill_contextual_step [NewCtx]). done. +Qed. + +Definition ectx_item_typing Σ (K: ectx_item) (A B: type) := + ∀ e Σ', Σ ⊆ Σ' → TY Σ'; 0; ∅ ⊢ e : A → TY Σ'; 0; ∅ ⊢ (fill_item K e) : B. + +Notation ectx := (list ectx_item). +Definition ectx_typing Σ (K: ectx) (A B: type) := + ∀ e Σ', Σ ⊆ Σ' → TY Σ'; 0; ∅ ⊢ e : A → TY Σ'; 0; ∅ ⊢ (fill K e) : B. + +Lemma ectx_item_typing_weaking Σ Σ' k B A : + Σ ⊆ Σ' → ectx_item_typing Σ k B A → ectx_item_typing Σ' k B A. +Proof. + intros Hsub Hty e Σ'' Hsub'' Hty'. eapply Hty; last done. + by transitivity Σ'. +Qed. + +Lemma ectx_typing_weaking Σ Σ' K B A : + Σ ⊆ Σ' → ectx_typing Σ K B A → ectx_typing Σ' K B A. +Proof. + intros Hsub Hty e Σ'' Hsub'' Hty'. eapply Hty; last done. + by transitivity Σ'. +Qed. + +Lemma fill_item_typing_decompose Σ k e A: + TY Σ; 0; ∅ ⊢ fill_item k e : A → + ∃ B, TY Σ; 0; ∅ ⊢ e : B ∧ ectx_item_typing Σ k B A. +Proof. + unfold ectx_item_typing; destruct k; simpl; inversion 1; subst; eauto 6 using typed_weakening, map_fmap_mono. +Qed. + +Lemma fill_typing_decompose Σ K e A: + TY Σ; 0; ∅ ⊢ fill K e : A → + ∃ B, TY Σ; 0; ∅ ⊢ e : B ∧ ectx_typing Σ K B A. +Proof. + unfold ectx_typing; revert e; induction K as [|k K]; intros e; simpl; eauto. + intros [B [Hit Hty]] % IHK. + eapply fill_item_typing_decompose in Hit as [B' [? ?]]; eauto. +Qed. + +Lemma fill_typing_compose Σ K e A B: + TY Σ; 0; ∅ ⊢ e : B → + ectx_typing Σ K B A → + TY Σ; 0; ∅ ⊢ fill K e : A. +Proof. + intros H1 H2; by eapply H2. +Qed. + +Lemma fmap_up_subst_ctx σ Γ: ⤉(subst σ <$> Γ) = subst (up σ) <$> ⤉Γ. +Proof. + rewrite -!map_fmap_compose. + eapply map_fmap_ext. intros x A _. by asimpl. +Qed. + +Lemma fmap_up_subst_heap_ctx σ Σ: ⤉(subst σ <$> Σ) = subst (up σ) <$> ⤉Σ. +Proof. + rewrite -!map_fmap_compose. + eapply map_fmap_ext. intros x A _. by asimpl. +Qed. + +Lemma typed_subst_type Σ n m Γ e A σ: + TY Σ; n; Γ ⊢ e : A → (∀ k, k < n → type_wf m (σ k)) → TY (subst σ) <$> Σ; m; (subst σ) <$> Γ ⊢ e : A.[σ]. +Proof. + induction 1 as [ Σ n Γ x A Heq | | | Σ n Γ e A Hty IH | | Σ n Γ A B e Hwf Hwf' Hty IH | Σ n Γ A B e e' x Hwf Hty1 IH1 Hty2 IH2 | | | | | |? ? ? ? ? ? ? ? ? Hop | ? ? ? ? ? ? ? Hop | | | | | | | | | | | | ] in σ, m |-*; simpl; intros Hlt; eauto. + - econstructor. rewrite lookup_fmap Heq //=. + - econstructor; last by eapply type_wf_subst. + rewrite -fmap_insert. eauto. + - econstructor; last by eapply type_wf_subst. eauto. + - econstructor. rewrite fmap_up_subst_ctx fmap_up_subst_heap_ctx. eapply IH. + intros [| x] Hlt'; rewrite /up //=. + + econstructor. lia. + + eapply type_wf_rename; last by (intros ???; simpl; lia). + eapply Hlt. lia. + - replace (A.[B/].[σ]) with (A.[up σ].[B.[σ]/]) by by asimpl. + eauto using type_wf_subst. + - (* pack *) + eapply (typed_pack _ _ _ _ (subst σ B)). + + eapply type_wf_subst; done. + + eapply type_wf_subst; first done. + intros [ | k] Hk; first ( asimpl;constructor; lia). + rewrite /up //=. eapply type_wf_rename; last by (intros ???; simpl; lia). + eapply Hlt. lia. + + replace (A.[up σ].[B.[σ]/]) with (A.[B/].[σ]) by by asimpl. + eauto using type_wf_subst. + - (* unpack *) + eapply (typed_unpack _ _ _ A.[up σ]). + + eapply type_wf_subst; done. + + replace (∃: A.[up σ])%ty with ((∃: A).[σ])%ty by by asimpl. + eapply IH1. done. + + rewrite fmap_up_subst_ctx fmap_up_subst_heap_ctx. rewrite -fmap_insert. + replace (B.[σ].[ren (+1)]) with (B.[ren(+1)].[up σ]) by by asimpl. + eapply IH2. + intros [ | k] Hk; asimpl; first (constructor; lia). + eapply type_wf_subst; first (eapply Hlt; lia). + intros k' Hk'. asimpl. constructor. lia. + - (* binop *) + inversion Hop; subst. + all: econstructor; naive_solver. + - (* unop *) + inversion Hop; subst. + all: econstructor; naive_solver. + - econstructor; last naive_solver. by eapply type_wf_subst. + - econstructor; last naive_solver. by eapply type_wf_subst. + - (* roll *) + econstructor. + replace (A.[up σ].[μ: A.[up σ]/])%ty with (A.[μ: A/].[σ])%ty by by asimpl. eauto. + - (* unroll *) + replace (A.[μ: A/].[σ])%ty with (A.[up σ].[μ: A.[up σ]/])%ty by by asimpl. + econstructor. eapply IHsyn_typed. done. + - (* loc *) + econstructor. rewrite lookup_fmap H //=. +Qed. + +Lemma typed_subst_type_closed Σ C e A: + type_wf 0 C → + heap_ctx_wf 0 Σ → + TY ⤉Σ; 1; ⤉∅ ⊢ e : A → TY Σ; 0; ∅ ⊢ e : A.[C/]. +Proof. + intros Hwf Hwf' Hty. eapply typed_subst_type with (σ := C .: ids) (m := 0) in Hty; last first. + { intros [|k] Hlt; last lia. done. } + revert Hty. rewrite !fmap_empty. + rewrite !(heap_ctx_closed Σ); eauto. +Qed. + +Lemma typed_subst_type_closed' Σ x C B e A: + type_wf 0 A → + type_wf 1 C → + type_wf 0 B → + heap_ctx_wf 0 Σ → + TY ⤉Σ; 1; <[x := C]> ∅ ⊢ e : A → + TY Σ; 0; <[x := C.[B/]]> ∅ ⊢ e : A. +Proof. + intros ???? Hty. + set (s := (subst (B.:ids))). + rewrite -(fmap_empty s) -(fmap_insert s). + replace A with (A.[B/]). + 2: { replace A with (A.[ids]) at 2 by by asimpl. + eapply type_wf_subst_dom; first done. lia. + } + rewrite -(heap_ctx_closed Σ (B.:ids)); last done. + eapply typed_subst_type. + { rewrite -(heap_ctx_closed Σ (ren (+1))); done. } + intros [ | k] Hk; last lia. done. +Qed. + +Lemma heap_ctx_insert h l A Σ: + heap_type h Σ → h !! l = None → Σ ⊆ <[l:=A]> Σ. +Proof. + intros Hheap Hlook. eapply insert_subseteq. + specialize (Hheap l). destruct (lookup) as [B|]; last done. + specialize (Hheap B eq_refl) as (w & Hsome & _). congruence. +Qed. + +Lemma heap_type_insert h Σ e v l B : + heap_type h Σ → + h !! l = None → + TY Σ; 0; ∅ ⊢ e : B → + to_val e = Some v → + heap_type ({[l := v]} ∪ h) (<[l:=B]> Σ). +Proof. + intros Hheap Hlook Hty Hval l' A. rewrite lookup_insert_Some. + intros [(-> & ->)|(Hne & Hlook')]. + - exists v. split; first eapply lookup_union_Some_l, lookup_insert. + eapply of_to_val in Hval as ->. + eapply typed_weakening; first eapply Hty; eauto. + by eapply heap_ctx_insert. + - eapply Hheap in Hlook' as (w & Hlook' & Hty'). + eexists; split. + + rewrite lookup_union_r; eauto. + rewrite lookup_insert_ne //=. + + eapply typed_weakening; first eapply Hty'; eauto. + by eapply heap_ctx_insert. +Qed. + +Lemma heap_type_update h Σ e v l B : + heap_type h Σ → + Σ !! l = Some B → + TY Σ; 0; ∅ ⊢ e : B → + to_val e = Some v → + heap_type (<[l:=v]> h) Σ. +Proof. + intros Hheap Hlook Hty Hval l' A Hlook'. + eapply Hheap in Hlook' as Hlook''. + destruct Hlook'' as (w & Hold & Hval'). + destruct (decide (l = l')); subst. + - exists v. split; first eapply lookup_insert. + eapply of_to_val in Hval as ->. + rewrite Hlook in Hlook'. by injection Hlook' as ->. + - rewrite lookup_insert_ne //=. eauto. +Qed. + + + +Lemma typed_preservation_base_step Σ e e' h h' A: + heap_ctx_wf 0 Σ → + TY Σ; 0; ∅ ⊢ e : A → + heap_type h Σ → + base_step (e, h) (e', h') → + ∃ Σ', Σ ⊆ Σ' ∧ heap_type h' Σ' ∧ heap_ctx_wf 0 Σ' ∧ TY Σ'; 0; ∅ ⊢ e' : A. +Proof. + intros Hwf' Hty Hhty Hstep. inversion Hstep as [ | | | op e1 v v' h1 Heq Heval | op e1 v1 e2 v2 v3 h1 Heq1 Heq2 Heval | | | | | | | | | | ]; subst. + - eapply app_inversion in Hty as (B & H1 & H2). + destruct x as [|x]. + { eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hwf & Hty). + exists Σ. do 3 (split; first done). done. } + eapply lam_inversion in H1 as (C & D & Heq & Hwf & Hty). + injection Heq as -> ->. + exists Σ. do 3 (split; first done). + eapply typed_substitutivity; eauto. + - eapply type_app_inversion in Hty as (B & C & -> & Hwf & Hty). + eapply type_lam_inversion in Hty as (A & Heq & Hty). + injection Heq as ->. exists Σ. split_and!; [done.. | ]. by eapply typed_subst_type_closed. + - eapply type_unpack_inversion in Hty as (B & x' & -> & Hwf & Hty1 & Hty2). + eapply type_pack_inversion in Hty1 as (B' & C & [= <-] & Hty1 & ? & ?). + exists Σ. split_and!; [done.. | ]. + eapply typed_substitutivity. + { done. } + { apply Hty1. } + rewrite fmap_empty in Hty2. + eapply typed_subst_type_closed'; eauto. + replace A with A.[ids] by by asimpl. + enough (A.[ids] = A.[ren (+1)]) as -> by done. + eapply type_wf_subst_dom; first done. intros; lia. + - (* unop *) + eapply unop_inversion in Hty as (A1 & Hop & Hty). + assert ((A1 = Int ∧ A = Int) ∨ (A1 = Bool ∧ A = Bool)) as [(-> & ->) | (-> & ->)]. + { inversion Hop; subst; eauto. } + + eapply canonical_values_int in Hty as [n ->]; last by eapply is_val_spec; eauto. + simpl in Heq. injection Heq as <-. + exists Σ; split_and!; [done..|]. + inversion Hop; subst; simpl in *; injection Heval as <-; constructor. + + eapply canonical_values_bool in Hty as [b ->]; last by eapply is_val_spec; eauto. + simpl in Heq. injection Heq as <-. + exists Σ; split_and!; [done..|]. + inversion Hop; subst; simpl in *; injection Heval as <-; constructor. + - (* binop *) + eapply binop_inversion in Hty as (A1 & A2 & Hop & Hty1 & Hty2). + assert (A1 = Int ∧ A2 = Int ∧ (A = Int ∨ A = Bool)) as (-> & -> & HC). + { inversion Hop; subst; eauto. } + eapply canonical_values_int in Hty1 as [n ->]; last by eapply is_val_spec; eauto. + eapply canonical_values_int in Hty2 as [m ->]; last by eapply is_val_spec; eauto. + simpl in Heq1, Heq2. injection Heq1 as <-. injection Heq2 as <-. + simpl in Heval. + exists Σ; split_and!; [done..|]. + inversion Hop; subst; simpl in *; injection Heval as <-; constructor. + - exists Σ; split_and!; [done..|]. + by eapply if_inversion in Hty as (H1 & H2 & H3). + - exists Σ; split_and!; [done..|]. + by eapply if_inversion in Hty as (H1 & H2 & H3). + - exists Σ; split_and!; [done..|]. + by eapply fst_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion). + - exists Σ; split_and!; [done..|]. + by eapply snd_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion). + - exists Σ; split_and!; [done..|]. + eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injl_inversion & ? & ?). + eauto. + - exists Σ; split_and!; [done..|]. + eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injr_inversion & ? & ?). + eauto. + - (* unroll *) + exists Σ; split_and!; [done..|]. + eapply unroll_inversion in Hty as (B & -> & Hty). + eapply roll_inversion in Hty as (C & Heq & Hty). injection Heq as ->. done. + - (* new *) + (* TODO: exercise *) + admit. + - (* load *) + (* TODO: exercise *) + admit. + - (* store *) + (* TODO: exercise *) + admit. +Admitted. + +Lemma typed_preservation Σ e e' h h' A: + heap_ctx_wf 0 Σ → + TY Σ; 0; ∅ ⊢ e : A → + heap_type h Σ → + contextual_step (e, h) (e', h') → + ∃ Σ', Σ ⊆ Σ' ∧ heap_type h' Σ' ∧ heap_ctx_wf 0 Σ' ∧ TY Σ'; 0; ∅ ⊢ e' : A. +Proof. + intros Hwf Hty Hheap Hstep. inversion Hstep as [K e1' e2' σ1 σ2 e1 e2 -> -> Hstep']; subst. + eapply fill_typing_decompose in Hty as [B [H1 H2]]. + eapply typed_preservation_base_step in H1 as (Σ' & Hsub & Hheap' & Hwf' & Hty'); eauto. + eexists; repeat split; try done. + eapply fill_typing_compose, ectx_typing_weaking; eauto. +Qed. + +Lemma typed_preservation_steps Σ e e' h h' A: + heap_ctx_wf 0 Σ → + TY Σ; 0; ∅ ⊢ e : A → + heap_type h Σ → + rtc contextual_step (e, h) (e', h') → + ∃ Σ', Σ ⊆ Σ' ∧ heap_type h' Σ' ∧ heap_ctx_wf 0 Σ' ∧ TY Σ'; 0; ∅ ⊢ e' : A. +Proof. + intros Hwf Hty Hheap Hsteps. remember (e, h) as c1. remember (e', h') as c2. + induction Hsteps as [|? [] ? Hstep Hsteps IH] in Σ, h, h',e, e', Heqc1, Heqc2, Hwf, Hty, Hheap |-*. + - rewrite Heqc1 in Heqc2. injection Heqc2 as -> ->. eauto. + - subst; eapply typed_preservation in Hty as (Σ' & Hsub' & Hheap' & Hwf' & Hty'); [|eauto..]. + eapply IH in Hty' as (Σ'' & Hsub'' & Hheap'' & Hwf'' & Hty''); [|eauto..]. + exists Σ''; repeat split; eauto. by trans Σ'. +Qed. + +Lemma type_safety Σ e1 e2 h1 h2 A: + heap_ctx_wf 0 Σ → + TY Σ; 0; ∅ ⊢ e1 : A → + heap_type h1 Σ → + rtc contextual_step (e1, h1) (e2, h2) → + is_val e2 ∨ reducible e2 h2. +Proof. + intros Hwf Hy Hheap Hsteps. + eapply typed_preservation_steps in Hsteps as (Σ' & Hsub & Hheap' & Hwf' & Hty'); eauto. + eapply typed_progress; eauto. +Qed. + +(* applies to terms containing no free locations (like the erasure of source terms) *) +Corollary closed_type_safety e e' h A: + TY ∅; 0; ∅ ⊢ e : A → + rtc contextual_step (e, ∅) (e', h) → + is_val e' ∨ reducible e' h. +Proof. + intros Hty Hsteps. eapply type_safety; eauto. + intros ??. set_solver. +Qed. + +(** Derived typing rules *) +Lemma typed_unroll' Σ n Γ e A B: + TY Σ; n; Γ ⊢ e : (μ: A) → + B = A.[(μ: A)%ty/] → + TY Σ; n; Γ ⊢ (unroll e) : B. +Proof. + intros ? ->. by eapply typed_unroll. +Qed. + +Lemma typed_tapp' Σ n Γ A B C e : + TY Σ; n; Γ ⊢ e : (∀: A) → + type_wf n B → + C = A.[B/] → + TY Σ; n; Γ ⊢ e <> : C. +Proof. + intros; subst C; by eapply typed_tapp. +Qed.