diff --git a/_CoqProject b/_CoqProject index 1786b8b..45fcbf7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -11,12 +11,16 @@ # library stuff theories/lib/maps.v theories/lib/sets.v +theories/lib/debruijn.v +theories/lib/facts.v # STLC theories/type_systems/stlc/lang.v theories/type_systems/stlc/notation.v theories/type_systems/stlc/untyped.v theories/type_systems/stlc/types.v +theories/type_systems/stlc/logrel.v +theories/type_systems/stlc/parallel_subst.v # Extended STLC theories/type_systems/stlc_extended/lang.v @@ -27,6 +31,16 @@ theories/type_systems/stlc_extended/bigstep.v theories/type_systems/stlc_extended/bigstep_sol.v theories/type_systems/stlc_extended/ctxstep.v theories/type_systems/stlc_extended/ctxstep_sol.v +theories/type_systems/stlc_extended/parallel_subst.v +theories/type_systems/stlc_extended/logrel.v + +# System F +theories/type_systems/systemf/lang.v +theories/type_systems/systemf/notation.v +theories/type_systems/systemf/types.v +theories/type_systems/systemf/tactics.v +theories/type_systems/systemf/bigstep.v +theories/type_systems/systemf/parallel_subst.v # By removing the # below, you can add the exercise sheets to make #theories/type_systems/warmup/warmup.v @@ -35,3 +49,5 @@ theories/type_systems/stlc_extended/ctxstep_sol.v #theories/type_systems/stlc/exercises01_sol.v #theories/type_systems/stlc/exercises02.v #theories/type_systems/stlc/exercises02_sol.v +#theories/type_systems/stlc/cbn_logrel.v +#theories/type_systems/systemf/exercises03.v diff --git a/theories/lib/debruijn.v b/theories/lib/debruijn.v new file mode 100644 index 0000000..704a9bc --- /dev/null +++ b/theories/lib/debruijn.v @@ -0,0 +1,47 @@ +From iris.prelude Require Import prelude options. +From Autosubst Require Export Autosubst. + + +(* [idss n sigma] alters the substitution [sigma] by + "prepending" binders [0..n), so that [#i] is substituted for binder [i]. + After that, the binders from [sigma] follow. + *) +Definition idss `{Ids X} (n : nat) (sigma : var → X) (x : var) := + if decide (x < n) then ids x else sigma (x - n). +Lemma idss_0 `{Ids X} (sigma : var → X) : + idss 0 sigma = sigma. +Proof. + f_ext. intros x; unfold idss. simpl. + replace (x - 0) with x by lia. done. +Qed. +Lemma up_idss `{Ids X} `{Rename X} (sigma : var → X) n : + (* this precondition holds for the instances we are interested in, + but is not a general law assumed by autosubst *) + (∀ x : var, rename (+1) (ids x) = ids (S x)) → + up (idss n sigma) = idss (S n) (sigma >>> rename (+1) ). +Proof. + intros Hren_law. + f_ext. intros x. destruct x as [ | x]; unfold idss; simpl; first done. + unfold up. simpl. + destruct (decide (x < n)). + - rewrite decide_True; last lia. apply Hren_law. + - rewrite decide_False; last lia. done. +Qed. + +(* We will also need something like [idss] to shift variable renamings [var → var]. + Instead of doing a separate definition like + [ Definition idsc (n : nat) (sigma : var → var) (x : var) := if decide (x < n) then x else sigma (x - n). ] + we declare suitable instances to use [idss] for variable renamings. +*) +#[global] Instance Ids_var : Ids var. exact id. Defined. +#[global] Instance Rename_var : Rename var. exact id. Defined. + +(* a lemma for the nat instance *) +Lemma upren_idss sigma n : + upren (idss n sigma) = idss (S n) (sigma >>> S). +Proof. + f_ext. intros x. destruct x as [ | x]; unfold idss; simpl; first done. + destruct (decide (x < n)). + - rewrite decide_True; [done | lia ]. + - rewrite decide_False; lia. +Qed. diff --git a/theories/lib/facts.v b/theories/lib/facts.v new file mode 100644 index 0000000..364c17d --- /dev/null +++ b/theories/lib/facts.v @@ -0,0 +1,53 @@ +From stdpp Require Export relations. +From stdpp Require Import binders gmap. + +Lemma if_iff P Q R S: + (P ↔ Q) → + (R ↔ S) → + ((P → R) ↔ (Q → S)). +Proof. + naive_solver. +Qed. + +Lemma if_iff' P R S : + (P → R ↔ S) → (P → R) ↔ (P → S). +Proof. tauto. Qed. +Lemma and_iff' (P R S : Prop) : + (P → R ↔ S) → (P ∧ R) ↔ (P ∧ S). +Proof. tauto. Qed. +Lemma and_iff (P Q R S : Prop) : + (P ↔ Q) → ((P ∨ Q) → R ↔ S) → (P ∧ R) ↔ (Q ∧ S). +Proof. tauto. Qed. + +Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B. +Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed. +Lemma list_subseteq_cons_binder A B x : A ⊆ B → x :b: A ⊆ x :b: B. +Proof. destruct x; [done|]. apply list_subseteq_cons. Qed. +Lemma list_subseteq_cons_l {X} (A B : list X) x : A ⊆ x :: B → x :: A ⊆ x :: B. +Proof. + intros Hincl. intros y. rewrite elem_of_cons. intros [-> | ?]. + - left. + - apply Hincl. naive_solver. +Qed. + +Lemma list_subseteq_cons_elem {X} (A B : list X) x : + x ∈ B → A ⊆ B → (x :: A) ⊆ B. +Proof. + intros Hel Hincl. + intros a [-> | ?]%elem_of_cons; [done|]. + by apply Hincl. +Qed. + +Lemma elements_subseteq `{EqDecision A} `{Countable A} (X Y : gset A): + X ⊆ Y → elements X ⊆ elements Y. +Proof. + rewrite elem_of_subseteq. + intros Ha a. rewrite !elem_of_elements. + apply Ha. +Qed. +Lemma list_subseteq_cons_r {X} (A B : list X) x : + A ⊆ B → A ⊆ (x :: B). +Proof. + intros Hincl. trans B; [done|]. + intros b Hel. apply elem_of_cons; by right. +Qed. diff --git a/theories/type_systems/stlc/cbn_logrel.v b/theories/type_systems/stlc/cbn_logrel.v new file mode 100644 index 0000000..a087a6f --- /dev/null +++ b/theories/type_systems/stlc/cbn_logrel.v @@ -0,0 +1,184 @@ +From stdpp Require Import base relations. +From iris Require Import prelude. +From semantics.lib Require Import sets maps. +From semantics.ts.stlc Require Import lang notation types parallel_subst. +From Equations Require Import Equations. + +Implicit Types + (Γ : typing_context) + (v : val) + (e : expr) + (A : type). + +(** *** Big-Step Semantics for cbn *) +Inductive big_step : expr → val → Prop := + | bs_lit (n : Z) : + big_step (LitInt n) (LitIntV n) + | bs_lam (x : binder) (e : expr) : + big_step (Lam x e) (LamV x e) + | bs_add e1 e2 (z1 z2 : Z) : + big_step e1 (LitIntV z1) → + big_step e2 (LitIntV z2) → + big_step (Plus e1 e2) (LitIntV (z1 + z2))%Z + | bs_app e1 e2 x e v2 v : + big_step e1 (@LamV x e) → + big_step (subst' x e2 e) v → + big_step (App e1 e2) v + . +#[export] Hint Constructors big_step : core. + + +Lemma big_step_vals (v: val): big_step (of_val v) v. +Proof. + induction v; econstructor. +Qed. + +Lemma big_step_inv_vals (v w: val): big_step (of_val v) w → v = w. +Proof. + destruct v; inversion 1; eauto. +Qed. + + + +(* *** Definition of the logical relation. *) +(* We reuse most of these definitions. *) +Inductive val_or_expr : Type := +| inj_val : val → val_or_expr +| inj_expr : expr → val_or_expr. + +(* Note that we're using a slightly modified termination argument here. *) +Equations type_size (t : type) : nat := + type_size Int := 1; + type_size (Fun A B) := type_size A + type_size B + 2. +Equations mut_measure (ve : val_or_expr) (t : type) : nat := + mut_measure (inj_val _) t := type_size t; + mut_measure (inj_expr _) t := 1 + type_size t. + +Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve t) := { + type_interp (inj_val v) Int => + ∃ z : Z, v = z ; + type_interp (inj_val v) (A → B) => + ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧ + ∀ e', + type_interp (inj_expr e') A → + type_interp (inj_expr (subst' x e' e)) B; + + type_interp (inj_expr e) t => + (* we now need to explicitly require that expressions here are closed so + that we can apply them to lambdas directly. *) + ∃ v, big_step e v ∧ closed [] e ∧ type_interp (inj_val v) t +}. +Next Obligation. + repeat simp mut_measure; simp type_size; lia. +Qed. +Next Obligation. + simp mut_measure. simp type_size. + destruct A; repeat simp mut_measure; repeat simp type_size; lia. +Qed. + +(* We derive the expression/value relation. *) +Notation sem_val_rel t v := (type_interp (inj_val v) t). +Notation sem_expr_rel t e := (type_interp (inj_expr e) t). + +Notation 𝒱 t v := (sem_val_rel t v). +Notation ℰ t v := (sem_expr_rel t v). + + +(* *** Semantic typing of contexts *) +Implicit Types + (θ : gmap string expr). + +Inductive sem_context_rel : typing_context → (gmap string expr) → Prop := + | sem_context_rel_empty : sem_context_rel ∅ ∅ + (* contexts may now contain arbitrary (semantically well-typed) expressions + as opposed to just values. *) + | sem_context_rel_insert Γ θ e x A : + ℰ A e → + sem_context_rel Γ θ → + sem_context_rel (<[x := A]> Γ) (<[x := e]> θ). + +Notation 𝒢 := sem_context_rel. + +(* The semantic typing judgement. Note that we require e to be closed under Γ. *) +Definition sem_typed Γ e A := + closed (elements (dom Γ)) e ∧ + ∀ θ, 𝒢 Γ θ → ℰ A (subst_map θ e). +Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). + + +(* We start by proving a couple of helper lemmas that will be useful later. *) + +Lemma sem_expr_rel_of_val A v: + ℰ A v → 𝒱 A v. +Proof. + simp type_interp. + intros (v' & ->%big_step_inv_vals & Hv'). + apply Hv'. +Qed. + + + +Lemma val_rel_closed v A: + 𝒱 A v → closed [] v. +Proof. + induction A; simp type_interp. + - intros [z ->]. done. + - intros (x & e & -> & Hcl & _). done. +Qed. +Lemma val_inclusion A v: + 𝒱 A v → ℰ A v. +Proof. + intros H. simp type_interp. eauto using big_step_vals, val_rel_closed. +Qed. +Lemma expr_rel_closed e A : + ℰ A e → closed [] e. +Proof. + simp type_interp. intros (v & ? & ? & ?). done. +Qed. +Lemma sem_context_rel_closed Γ θ: + 𝒢 Γ θ → subst_closed [] θ. +Proof. + induction 1; rewrite /subst_closed. + - naive_solver. + - intros y e'. rewrite lookup_insert_Some. + intros [[-> <-]|[Hne Hlook]]. + + by eapply expr_rel_closed. + + eapply IHsem_context_rel; last done. +Qed. + + +(* This is essentially an inversion lemma for 𝒢 *) +Lemma sem_context_rel_exprs Γ θ x A : + sem_context_rel Γ θ → + Γ !! x = Some A → + ∃ e, θ !! x = Some e ∧ ℰ A e. +Proof. + induction 1 as [|Γ θ e y B Hvals Hctx IH]. + - naive_solver. + - rewrite lookup_insert_Some. intros [[-> ->]|[Hne Hlook]]. + + eexists; first by rewrite lookup_insert. + + eapply IH in Hlook as (e' & Hlook & He). + eexists; split; first by rewrite lookup_insert_ne. + done. +Qed. + +Lemma sem_context_rel_dom Γ θ : + 𝒢 Γ θ → dom Γ = dom θ. +Proof. + induction 1. + - by rewrite !dom_empty. + - rewrite !dom_insert. congruence. +Qed. + + + + +Lemma termination e A : + (∅ ⊢ e : A)%ty → + ∃ v, big_step e v. +Proof. + (* You may want to add suitable intermediate lemmas, like we did for the cbv + logical relation as seen in the lecture. *) + (* TODO: exercise *) +Admitted. + diff --git a/theories/type_systems/stlc/logrel.v b/theories/type_systems/stlc/logrel.v new file mode 100644 index 0000000..212c19c --- /dev/null +++ b/theories/type_systems/stlc/logrel.v @@ -0,0 +1,296 @@ +From stdpp Require Import base relations. +From iris Require Import prelude. +From semantics.lib Require Import sets maps. +From semantics.ts.stlc Require Import lang notation types parallel_subst. +From Equations Require Import Equations. + +Implicit Types + (Γ : typing_context) + (v : val) + (e : expr) + (A : type). + + +(* *** Definition of the logical relation. *) +(* In Coq, we need to make argument why the logical relation is well-defined + precise: + In particular, we need to show that the mutual recursion between the value + relation and the expression relation, which are defined in terms of each + other, terminates. We therefore define a termination measure [mut_measure] + that makes sure that for each recursive call, we either decrease the size of + the type or switch from the expression case to the value case. + + We use the Equations package to define the logical relation, as it's tedious + to make the termination argument work with Coq's built-in support for + recursive functions---but under the hood, Equations also just encodes it as + a Coq Fixpoint. + *) +Inductive val_or_expr : Type := +| inj_val : val → val_or_expr +| inj_expr : expr → val_or_expr. + +(* The [type_size] function essentially computes the size of the "type tree". *) +Equations type_size (t : type) : nat := + type_size Int := 1; + type_size (Fun A B) := type_size A + type_size B + 1. +(* The definition of the expression relation uses the value relation -- therefore, it needs to be larger, and we add [1]. *) +Equations mut_measure (ve : val_or_expr) (t : type) : nat := + mut_measure (inj_val _) t := type_size t; + mut_measure (inj_expr _) t := 1 + type_size t. + + +(* The main definition of the logical relation. + To handle the mutual recursion, both the expression and value relation are + handled by one definition, with [val_or_expr] determining the case. + + The [by wf ..] part tells Equations to use [mut_measure] for the + well-formedness argument. + *) +Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve t) := { + type_interp (inj_val v) Int => + ∃ z : Z, v = z ; + type_interp (inj_val v) (A → B) => + ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧ + ∀ v', + type_interp (inj_val v') A → + type_interp (inj_expr (subst' x v' e)) B; + + type_interp (inj_expr e) t => + ∃ v, big_step e v ∧ type_interp (inj_val v) t +}. +Next Obligation. + (* [simp] is a tactic provided by [Equations]. It rewrites with the defining equations of the definition. + [simpl]/[cbn] will NOT unfold definitions made with Equations. + *) + repeat simp mut_measure; simp type_size; lia. +Qed. +Next Obligation. + simp mut_measure. simp type_size. + destruct A; repeat simp mut_measure; repeat simp type_size; lia. +Qed. + +(* We derive the expression/value relation. + Note that these are [Notation], not [Definition]: we are not introducing new + terms here that have to be unfolded, we are merely introducing a notational + short-hand. This means tactics like [simp] can still "see" the underlying + [type_interp], which makes proofs a lot more pleasant. *) +Notation sem_val_rel t v := (type_interp (inj_val v) t). +Notation sem_expr_rel t e := (type_interp (inj_expr e) t). + +Notation 𝒱 t v := (sem_val_rel t v). +Notation ℰ t v := (sem_expr_rel t v). + + +(* *** Semantic typing of contexts *) +(* Substitutions map to expressions (as opposed to values)) -- this is so that + we can more easily reuse notions like closedness *) +Implicit Types + (θ : gmap string expr). + +Inductive sem_context_rel : typing_context → (gmap string expr) → Prop := + | sem_context_rel_empty : sem_context_rel ∅ ∅ + | sem_context_rel_insert Γ θ v x A : + 𝒱 A v → + sem_context_rel Γ θ → + sem_context_rel (<[x := A]> Γ) (<[x := of_val v]> θ). + +Notation 𝒢 := sem_context_rel. + +(* The semantic typing judgement. Note that we require e to be closed under Γ. + This is not strictly required for the semantic soundness proof, but does + make it more elegant. *) +Definition sem_typed Γ e A := + closed (elements (dom Γ)) e ∧ + ∀ θ, 𝒢 Γ θ → ℰ A (subst_map θ e). +Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). + + +(* We start by proving a couple of helper lemmas that will be useful later. *) + +Lemma sem_expr_rel_of_val A v: + ℰ A v → 𝒱 A v. +Proof. + simp type_interp. + intros (v' & ->%big_step_inv_vals & Hv'). + apply Hv'. +Qed. +Lemma val_inclusion A v: + 𝒱 A v → ℰ A v. +Proof. + intros H. simp type_interp. eauto using big_step_vals. +Qed. + + + +Lemma val_rel_closed v A: + 𝒱 A v → closed [] v. +Proof. + induction A; simp type_interp. + - intros [z ->]. done. + - intros (x & e & -> & Hcl & _). done. +Qed. +Lemma sem_context_rel_closed Γ θ: + 𝒢 Γ θ → subst_closed [] θ. +Proof. + induction 1; rewrite /subst_closed. + - naive_solver. + - intros y e. rewrite lookup_insert_Some. + intros [[-> <-]|[Hne Hlook]]. + + by eapply val_rel_closed. + + eapply IHsem_context_rel; last done. +Qed. + + +(* This is essentially an inversion lemma for 𝒢 *) +Lemma sem_context_rel_vals Γ θ x A : + 𝒢 Γ θ → + Γ !! x = Some A → + ∃ e v, θ !! x = Some e ∧ to_val e = Some v ∧ 𝒱 A 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_dom Γ θ : + 𝒢 Γ θ → dom Γ = dom θ. +Proof. + induction 1. + - by rewrite !dom_empty. + - rewrite !dom_insert. congruence. +Qed. + + +(* *** Compatibility lemmas *) +Lemma compat_int Γ z : Γ ⊨ (LitInt z) : Int. +Proof. + split; first done. + intros θ _. simp type_interp. + exists z. split; simpl. + - constructor. + - simp type_interp. eauto. +Qed. + +Lemma compat_var Γ x A : + Γ !! x = Some A → + Γ ⊨ (Var x) : A. +Proof. + intros Hx. split. + { eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx. } + intros θ Hctx; simpl. + eapply sem_context_rel_vals in Hx as (e & v & He & Heq & Hv); last done. + rewrite He. simp type_interp. exists v. split; last done. + rewrite -(of_to_val _ _ Heq). + by apply big_step_vals. +Qed. + +Lemma compat_app Γ e1 e2 A B : + Γ ⊨ e1 : (A → B) → + Γ ⊨ e2 : A → + Γ ⊨ (e1 e2) : B. +Proof. + intros [Hfuncl Hfun] [Hargcl Harg]. split. + { simpl. eauto. } + intros θ Hctx; simpl. + specialize (Hfun _ Hctx). simp type_interp in Hfun. destruct Hfun as (v1 & Hbs1 & Hv1). + simp type_interp in Hv1. destruct Hv1 as (x & e & -> & Hcl & Hv1). + specialize (Harg _ Hctx). simp type_interp in Harg. + destruct Harg as (v2 & Hbs2 & Hv2). + + apply Hv1 in Hv2. + simp type_interp in Hv2. destruct Hv2 as (v & Hbsv & Hv). + + simp type_interp. + exists v. split; last done. + eauto. +Qed. + + +(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *) +Lemma lam_closed Γ θ (x : string) A e : + closed (elements (dom (<[x:=A]> Γ))) e → + 𝒢 Γ θ → + closed [] (Lam x (subst_map (delete x θ) e)). +Proof. + intros Hcl Hctxt. + eapply subst_map_closed'_2. + - eapply closed_weaken; first done. + rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //. + (* The [set_solver] tactic is great for solving goals involving set + inclusion and union. However, when set difference is involved, it can't + always solve the goal -- we need to help it by doing a case distinction on + whether the element we are considering is [x] or not. *) + intros y. destruct (decide (x = y)); set_solver. + - eapply subst_closed_weaken, sem_context_rel_closed; last done. + + set_solver. + + apply map_delete_subseteq. +Qed. +Lemma compat_lam Γ x e A B : + (<[ x := A ]> Γ) ⊨ e : B → + Γ ⊨ (Lam (BNamed x) e) : (A → B). +Proof. + intros [Hbodycl Hbody]. split. + { simpl. eapply closed_weaken; first eassumption. set_solver. } + intros θ Hctxt. simpl. simp type_interp. + eexists. + split; first by eauto. + simp type_interp. + eexists x, _. split; first reflexivity. + split; first by eapply lam_closed. + intros v' Hv'. + specialize (Hbody (<[ x := of_val v']> θ)). + simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed. + apply Hbody. + apply sem_context_rel_insert; done. +Qed. + +Lemma compat_add Γ e1 e2 : + Γ ⊨ e1 : Int → + Γ ⊨ e2 : Int → + Γ ⊨ (e1 + e2) : Int. +Proof. + intros [Hcl1 He1] [Hcl2 He2]. split. + { simpl. eauto. } + intros θ Hctx. + simp type_interp. + specialize (He1 _ Hctx). specialize (He2 _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & Hb1 & Hv1). + destruct He2 as (v2 & Hb2 & Hv2). + simp type_interp in Hv1, Hv2. + destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->). + + exists (z1 + z2)%Z. split. + - constructor; done. + - exists (z1 + z2)%Z. done. +Qed. + +Lemma sem_soundness Γ e A : + (Γ ⊢ e : A)%ty → + Γ ⊨ e : A. +Proof. + induction 1 as [ | Γ x e A B Hsyn IH | | | ]. + - by apply compat_var. + - by apply compat_lam. + - apply compat_int. + - by eapply compat_app. + - by apply compat_add. +Qed. + +Lemma termination e A : + (∅ ⊢ e : A)%ty → + ∃ v, big_step e v. +Proof. + intros [Hsemcl Hsem]%sem_soundness. + specialize (Hsem ∅). + simp type_interp in Hsem. + rewrite subst_map_empty in Hsem. + destruct Hsem as (v & Hbs & _); last eauto. + constructor. +Qed. diff --git a/theories/type_systems/stlc/parallel_subst.v b/theories/type_systems/stlc/parallel_subst.v new file mode 100644 index 0000000..013b75a --- /dev/null +++ b/theories/type_systems/stlc/parallel_subst.v @@ -0,0 +1,189 @@ +From semantics.ts.stlc Require Import lang. +From stdpp Require Import prelude. +From iris Require Import prelude. +From semantics.lib Require Export maps . + +(** * Parallel substitution *) + +(** This is the parallel substitution operation. We represent a substitution map as a finite map [xs]. *) +Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr := + match e with + | LitInt n => LitInt n + | 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) + | Plus e1 e2 => Plus (subst_map xs e1) (subst_map xs e2) + end. + +Lemma subst_map_empty e : + subst_map ∅ e = e. +Proof. + induction e; simpl; f_equal; eauto. + destruct x; simpl; [done | by rewrite !delete_empty..]. +Qed. + + + +Lemma subst_map_closed X e xs : + 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. + { (* 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. + } + (* all other cases *) + all: repeat match goal with + | H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ] + end. + all: repeat match goal with + | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H + end; done. +Qed. + +Lemma subst_map_subst map x (e e': expr) : + closed [] e' → + subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e. +Proof. + intros He'; induction e as [y|y e IH | | |]in map|-*; simpl; try (f_equal; eauto). + - case_decide. + + simplify_eq/=. rewrite lookup_insert. + rewrite (subst_map_closed []); [done | apply He' | ]. + intros ? ?. apply not_elem_of_nil. + + rewrite lookup_insert_ne; done. + - destruct y; simpl; first done. + + case_decide. + * simplify_eq/=. by rewrite delete_insert_delete. + * rewrite delete_insert_ne; last by congruence. done. +Qed. + +(** We lift the notion of closedness [closed] to substitution maps. *) +Definition subst_closed (X : list string) (map : gmap string expr) := + ∀ x e, map !! x = Some e → closed X e. +Lemma subst_closed_subseteq X map1 map2 : + map1 ⊆ map2 → subst_closed X map2 → subst_closed X map1. +Proof. + intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done. +Qed. + +Lemma subst_closed_weaken X Y map1 map2 : + Y ⊆ X → map1 ⊆ map2 → subst_closed Y map2 → subst_closed X map1. +Proof. + intros Hsub1 Hsub2 Hclosed2 x e Hl. + eapply closed_weaken. 1:eapply Hclosed2, map_subseteq_spec; done. done. +Qed. + +(** Lemma about the interaction with "normal" substitution. *) +Lemma subst_subst_map x es map e : + subst_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_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_closed_subseteq; last done. + apply map_delete_subseteq. +Qed. + +Lemma subst'_subst_map b (es : expr) map e : + subst_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_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 |-*; simpl; intros Hmclosed Hsub Hcl. + { (* vars *) + destruct (map !! x) as [es | ] eqn:Heq. + + apply 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_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 + | H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ] + end. + all: repeat match goal with + | |- Is_true (_ && _) => apply andb_True; split + end. + all: naive_solver. +Qed. + + +Lemma subst_map_closed' X Y Θ e: + closed Y e → + (∀ x, x ∈ Y → if Θ !! x is (Some e') then closed X e' else x ∈ X) → + closed X (subst_map Θ e). +Proof. + induction e in X, Θ, Y |-*; simpl. + - intros Hel%bool_decide_unpack Hcl. + eapply Hcl in Hel. + destruct (Θ !! x); first done. + simpl. by eapply bool_decide_pack. + - intros Hcl Hcl'. destruct x as [|x]; simpl; first naive_solver. + eapply IHe; first done. + intros y [|]%elem_of_cons. + + subst. rewrite lookup_delete. set_solver. + + destruct (decide (x = y)); first by subst; rewrite lookup_delete; set_solver. + rewrite lookup_delete_ne //=. eapply Hcl' in H. + destruct lookup; last set_solver. + eapply closed_weaken; eauto with set_solver. + - rewrite !andb_True. intros [H1 H2] Hcl. split; eauto. + - auto. + - rewrite !andb_True. intros [H1 H2] Hcl. split; eauto. +Qed. + +Lemma subst_map_closed'_2 X Θ e: + closed (X ++ (elements (dom Θ))) e -> + subst_closed X Θ -> + closed X (subst_map Θ e). +Proof. + intros Hcl Hsubst. + eapply subst_map_closed'; first eassumption. + intros x Hx. + destruct (Θ !! x) as [e'|] eqn:Heq. + - eauto. + - by eapply elem_of_app in Hx as [H|H%elem_of_elements%not_elem_of_dom]. +Qed. diff --git a/theories/type_systems/stlc_extended/logrel.v b/theories/type_systems/stlc_extended/logrel.v new file mode 100644 index 0000000..7a3b32e --- /dev/null +++ b/theories/type_systems/stlc_extended/logrel.v @@ -0,0 +1,307 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.stlc_extended Require Import lang notation parallel_subst types bigstep. +From semantics.ts.stlc_extended Require Import lang notation parallel_subst types bigstep. +From Equations Require Export Equations. + + + +(** * Logical relation for the extended STLC *) + +Implicit Types + (Γ : typing_context) + (v : val) + (e : expr) + (A : type). + + +(* *** Definition of the logical relation. *) + +Inductive val_or_expr : Type := +| inj_val : val → val_or_expr +| inj_expr : expr → val_or_expr. + +Equations type_size (A : type) : nat := + type_size Int := 1; + type_size (A → B) := type_size A + type_size B + 1; + type_size (A × B) := type_size A + type_size B + 1; + type_size (A + B) := max (type_size A) (type_size B) + 1. +Equations mut_measure (ve : val_or_expr) (t : type) : nat := + mut_measure (inj_val _) t := type_size t; + mut_measure (inj_expr _) t := 1 + type_size t. + + +Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve t) := { + type_interp (inj_val v) Int => + ∃ z : Z, v = #z ; + type_interp (inj_val v) (A × B) => + (* TODO: add type interpretation *) + False; + type_interp (inj_val v) (A + B) => + (* TODO: add type interpretation *) + False; + type_interp (inj_val v) (A → B) => + ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧ + ∀ v', + type_interp (inj_val v') A → + type_interp (inj_expr (subst' x v' e)) B; + + type_interp (inj_expr e) t => + ∃ v, big_step e v ∧ type_interp (inj_val v) t +}. +Next Obligation. + repeat simp mut_measure; simp type_size; lia. +Qed. +Next Obligation. + simp mut_measure. simp type_size. + destruct A; repeat simp mut_measure; repeat simp type_size; lia. +Qed. +(* Uncomment the following once you have amended the type interpretation to + solve the new obligations: *) +(* +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed. +*) + + +Notation sem_val_rel t v := (type_interp (inj_val v) t). +Notation sem_expr_rel t e := (type_interp (inj_expr e) t). + +Notation 𝒱 t v := (sem_val_rel t v). +Notation ℰ t v := (sem_expr_rel t v). + + +(* *** Semantic typing of contexts *) +Implicit Types + (θ : gmap string expr). + +Inductive sem_context_rel : typing_context → (gmap string expr) → Prop := + | sem_context_rel_empty : sem_context_rel ∅ ∅ + | sem_context_rel_insert Γ θ v x A : + 𝒱 A v → + sem_context_rel Γ θ → + sem_context_rel (<[x := A]> Γ) (<[x := of_val v]> θ). + +Notation 𝒢 := sem_context_rel. + +Definition sem_typed Γ e A := + closed (elements (dom Γ)) e ∧ + ∀ θ, 𝒢 Γ θ → ℰ A (subst_map θ e). +Notation "Γ ⊨ e : A" := (sem_typed Γ e A) (at level 74, e, A at next level). + + +(* We start by proving a couple of helper lemmas that will be useful later. *) + +Lemma sem_expr_rel_of_val A v: + ℰ A v → 𝒱 A v. +Proof. + simp type_interp. + intros (v' & ->%big_step_val & Hv'). + apply Hv'. +Qed. +Lemma val_inclusion A v: + 𝒱 A v → ℰ A v. +Proof. + intros H. simp type_interp. eauto using big_step_of_val. +Qed. + + + +Lemma val_rel_closed v A: + 𝒱 A v → closed [] v. +Proof. + induction A in v |-*; simp type_interp. + - intros [z ->]. done. + - intros (x & e & -> & Hcl & _). done. + (* TODO: exercise *) +Admitted. + +Lemma sem_context_rel_closed Γ θ: + 𝒢 Γ θ → subst_closed [] θ. +Proof. + induction 1; rewrite /subst_closed. + - naive_solver. + - intros y e. rewrite lookup_insert_Some. + intros [[-> <-]|[Hne Hlook]]. + + by eapply val_rel_closed. + + eapply IHsem_context_rel; last done. +Qed. + + +(* This is essentially an inversion lemma for 𝒢 *) +Lemma sem_context_rel_vals Γ θ x A : + 𝒢 Γ θ → + Γ !! x = Some A → + ∃ e v, θ !! x = Some e ∧ to_val e = Some v ∧ 𝒱 A 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_dom Γ θ : + 𝒢 Γ θ → dom Γ = dom θ. +Proof. + induction 1. + - by rewrite !dom_empty. + - rewrite !dom_insert. congruence. +Qed. + + +(* *** Compatibility lemmas *) +Lemma compat_int Γ z : Γ ⊨ (LitInt z) : Int. +Proof. + split; first done. + intros θ _. simp type_interp. + exists #z. split; simpl. + - constructor. + - simp type_interp. eauto. +Qed. + +Lemma compat_var Γ x A : + Γ !! x = Some A → + Γ ⊨ (Var x) : A. +Proof. + intros Hx. split. + { eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx. } + intros θ Hctx; simpl. + eapply sem_context_rel_vals in Hx as (e & v & He & Heq & Hv); last done. + rewrite He. simp type_interp. exists v. split; last done. + rewrite -(of_to_val _ _ Heq). + by apply big_step_of_val. +Qed. + +Lemma compat_app Γ e1 e2 A B : + Γ ⊨ e1 : (A → B) → + Γ ⊨ e2 : A → + Γ ⊨ (e1 e2) : B. +Proof. + intros [Hfuncl Hfun] [Hargcl Harg]. split. + { unfold closed. simpl. eauto. } + intros θ Hctx; simpl. + specialize (Hfun _ Hctx). simp type_interp in Hfun. destruct Hfun as (v1 & Hbs1 & Hv1). + simp type_interp in Hv1. destruct Hv1 as (x & e & -> & Hcl & Hv1). + specialize (Harg _ Hctx). simp type_interp in Harg. + destruct Harg as (v2 & Hbs2 & Hv2). + + apply Hv1 in Hv2. + simp type_interp in Hv2. destruct Hv2 as (v & Hbsv & Hv). + + simp type_interp. + exists v. split; last done. + eauto. +Qed. + + +(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *) +Lemma lam_closed Γ θ (x : string) A e : + closed (elements (dom (<[x:=A]> Γ))) e → + 𝒢 Γ θ → + closed [] (Lam x (subst_map (delete x θ) e)). +Proof. + intros Hcl Hctxt. + eapply subst_map_closed'_2. + - eapply is_closed_weaken; first done. + rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //. + intros y. destruct (decide (x = y)); set_solver. + - eapply subst_closed_weaken, sem_context_rel_closed; last done. + + set_solver. + + apply map_delete_subseteq. +Qed. +Lemma compat_lam Γ x e A B : + (<[ x := A ]> Γ) ⊨ e : B → + Γ ⊨ (Lam (BNamed x) e) : (A → B). +Proof. + intros [Hbodycl Hbody]. split. + { unfold closed in *. cbn in *. eapply is_closed_weaken; first eassumption. + set_solver. } + intros θ Hctxt. simpl. simp type_interp. + eexists. + split; first by eauto. + simp type_interp. + eexists x, _. split; first reflexivity. + split; first by eapply lam_closed. + intros v' Hv'. + specialize (Hbody (<[ x := of_val v']> θ)). + simpl. rewrite subst_subst_map; last by eapply sem_context_rel_closed. + apply Hbody. + apply sem_context_rel_insert; done. +Qed. +Lemma compat_lam_anon Γ e A B : + Γ ⊨ e : B → + Γ ⊨ (Lam BAnon e) : (A → B). +Proof. + intros [Hbodycl Hbody]. split; first done. + intros θ Hctxt. simpl. simp type_interp. + eexists. + split; first by eauto. + simp type_interp. + eexists _, _. split; first reflexivity. + split. + { simpl. eapply subst_map_closed'_2; simpl. + - by erewrite <-sem_context_rel_dom. + - by eapply sem_context_rel_closed. } + naive_solver. +Qed. + +Lemma compat_add Γ e1 e2 : + Γ ⊨ e1 : Int → + Γ ⊨ e2 : Int → + Γ ⊨ (e1 + e2) : Int. +Proof. + intros [Hcl1 He1] [Hcl2 He2]. split. + { unfold closed in *. naive_solver. } + intros θ Hctx. + simp type_interp. + specialize (He1 _ Hctx). specialize (He2 _ Hctx). + simp type_interp in He1. simp type_interp in He2. + + destruct He1 as (v1 & Hb1 & Hv1). + destruct He2 as (v2 & Hb2 & Hv2). + simp type_interp in Hv1, Hv2. + destruct Hv1 as (z1 & ->). destruct Hv2 as (z2 & ->). + + exists #(z1 + z2). split. + - constructor; done. + - exists (z1 + z2)%Z. done. + +Qed. + + + + +Lemma sem_soundness Γ e A : + (Γ ⊢ e : A)%ty → + Γ ⊨ e : A. +Proof. + induction 1. + - by apply compat_var. + - by apply compat_lam. + - by apply compat_lam_anon. + - apply compat_int. + - by eapply compat_app. + - by apply compat_add. + (* add compatibility lemmas for the new rules here. *) + (* TODO: exercise *) +Admitted. + + +Lemma termination e A : + (∅ ⊢ e : A)%ty → + ∃ v, big_step e v. +Proof. + intros [Hsemcl Hsem]%sem_soundness. + specialize (Hsem ∅). + simp type_interp in Hsem. + rewrite subst_map_empty in Hsem. + destruct Hsem as (v & Hbs & _); last eauto. + constructor. +Qed. + diff --git a/theories/type_systems/stlc_extended/parallel_subst.v b/theories/type_systems/stlc_extended/parallel_subst.v new file mode 100644 index 0000000..d980b4c --- /dev/null +++ b/theories/type_systems/stlc_extended/parallel_subst.v @@ -0,0 +1,193 @@ +From stdpp Require Import prelude. +From iris Require Import prelude. +From semantics.ts.stlc_extended Require Import lang. +From semantics.lib Require Import maps. + +Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr := + match e with + | LitInt n => LitInt n + | 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) + | Plus e1 e2 => Plus (subst_map xs e1) (subst_map 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) + end. + + +Lemma subst_map_empty e : + subst_map ∅ e = e. +Proof. + induction e; simpl; f_equal; eauto. + destruct x; simpl; [done | by rewrite !delete_empty..]. +Qed. + + + +Lemma subst_map_closed X e xs : + 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. + { (* 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. + } + (* all other cases *) + all: unfold closed in *; simpl in *. + all: repeat match goal with + | H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ] + end. + all: repeat match goal with + | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H + end; try done. +Qed. + +Lemma subst_map_subst map x (e e': expr) : + closed [] e' → + subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e. +Proof. + intros He'; induction e as [y|y e IH | | | | | | | | | ]in map|-*; simpl; try (f_equal; eauto). + - case_decide. + + simplify_eq/=. rewrite lookup_insert. + rewrite (subst_map_closed []); [done | apply He' | ]. + intros ? ?. apply not_elem_of_nil. + + rewrite lookup_insert_ne; done. + - destruct y; simpl; first done. + + case_decide. + * simplify_eq/=. by rewrite delete_insert_delete. + * rewrite delete_insert_ne; last by congruence. done. +Qed. + +(** We lift the notion of closedness [closed] to substitution maps. *) +Definition subst_closed (X : list string) (map : gmap string expr) := + ∀ x e, map !! x = Some e → closed X e. +Lemma subst_closed_subseteq X map1 map2 : + map1 ⊆ map2 → subst_closed X map2 → subst_closed X map1. +Proof. + intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done. +Qed. + +Lemma subst_closed_weaken X Y map1 map2 : + Y ⊆ X → map1 ⊆ map2 → subst_closed Y map2 → subst_closed X map1. +Proof. + intros Hsub1 Hsub2 Hclosed2 x e Hl. + eapply is_closed_weaken. 1:eapply Hclosed2, map_subseteq_spec; done. done. +Qed. + +(** Lemma about the interaction with "normal" substitution. *) +Lemma subst_subst_map x es map e : + subst_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_closed_subseteq; last done. + apply map_delete_subseteq. +Qed. + +Lemma subst'_subst_map b (es : expr) map e : + subst_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_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 |-*; simpl; intros Hmclosed Hsub Hcl. + { (* 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_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: unfold closed in *; simpl in *. + all: repeat match goal with + | H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ] + end. + all: repeat match goal with + | |- Is_true (_ && _) => apply andb_True; split + end. + all: try naive_solver. +Qed. + + +Lemma subst_map_closed' X Y Θ e: + closed Y e → + (∀ x, x ∈ Y → if Θ !! x is (Some e') then closed X e' else x ∈ X) → + closed X (subst_map Θ e). +Proof. + induction e in X, Θ, Y |-*; simpl. + { intros Hel%bool_decide_unpack Hcl. + eapply Hcl in Hel. + destruct (Θ !! x); first done. + simpl. by eapply bool_decide_pack. } + { intros Hcl Hcl'. destruct x as [|x]; simpl; first naive_solver. + eapply IHe; first done. + intros y [|]%elem_of_cons. + + subst. rewrite lookup_delete. set_solver. + + destruct (decide (x = y)); first by subst; rewrite lookup_delete; set_solver. + rewrite lookup_delete_ne //=. eapply Hcl' in H. + destruct lookup; last set_solver. + eapply is_closed_weaken; eauto with set_solver. } + all: unfold closed; simpl; naive_solver. +Qed. + +Lemma subst_map_closed'_2 X Θ e: + closed (X ++ (elements (dom Θ))) e -> + subst_closed X Θ -> + closed X (subst_map Θ e). +Proof. + intros Hcl Hsubst. + eapply subst_map_closed'; first eassumption. + intros x Hx. + destruct (Θ !! x) as [e'|] eqn:Heq. + - eauto. + - by eapply elem_of_app in Hx as [H|H%elem_of_elements%not_elem_of_dom]. +Qed. diff --git a/theories/type_systems/systemf/bigstep.v b/theories/type_systems/systemf/bigstep.v new file mode 100644 index 0000000..0170fe4 --- /dev/null +++ b/theories/type_systems/systemf/bigstep.v @@ -0,0 +1,223 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.lib Require Export debruijn. +From semantics.ts.systemf Require Import lang notation types. +From Equations Require Import Equations. + +(** * Big-step semantics *) + +Implicit Types + (Δ : nat) + (Γ : typing_context) + (v : val) + (α : var) + (e : expr) + (A : type). + +Inductive big_step : expr → val → Prop := + | bs_lit (l : base_lit) : + big_step (Lit l) (LitV l) + | bs_lam (x : binder) (e : expr) : + big_step (λ: x, e)%E (λ: x, e)%V + | bs_binop e1 e2 v1 v2 v' op : + big_step e1 v1 → + big_step e2 v2 → + bin_op_eval op v1 v2 = Some v' → + big_step (BinOp op e1 e2) v' + | bs_unop e v v' op : + big_step e v → + un_op_eval op v = Some v' → + big_step (UnOp op e) v' + | bs_app e1 e2 x e v2 v : + big_step e1 (LamV x e) → + big_step e2 v2 → + big_step (subst' x (of_val v2) e) v → + big_step (App e1 e2) v + | bs_tapp e1 e2 v : + big_step e1 (TLamV e2) → + big_step e2 v → + big_step (e1 <>) v + | bs_tlam e : + big_step (Λ, e)%E (Λ, e)%V + | bs_pack e v : + big_step e v → + big_step (pack e)%E (pack v)%V + | bs_unpack e1 e2 v1 v2 x : + big_step e1 (pack v1)%V → + big_step (subst' x (of_val v1) e2) v2 → + big_step (unpack e1 as x in e2) v2 + | bs_if_true e0 e1 e2 v : + big_step e0 #true → + big_step e1 v → + big_step (if: e0 then e1 else e2) v + | bs_if_false e0 e1 e2 v : + big_step e0 #false → + big_step e2 v → + big_step (if: e0 then e1 else e2) v + | bs_pair e1 e2 v1 v2 : + big_step e1 v1 → + big_step e2 v2 → + big_step (e1, e2) (v1, v2) + | bs_fst e v1 v2 : + big_step e (v1, v2) → + big_step (Fst e) v1 + | bs_snd e v1 v2 : + big_step e (v1, v2) → + big_step (Snd e) v2 + | bs_injl e v : + big_step e v → + big_step (InjL e) (InjLV v) + | bs_injr e v : + big_step e v → + big_step (InjR e) (InjRV v) + | bs_casel e e1 e2 v v' : + big_step e (InjLV v) → + big_step (e1 (of_val v)) v' → + big_step (Case e e1 e2) v' + | bs_caser e e1 e2 v v' : + big_step e (InjRV v) → + big_step (e2 (of_val v)) v' → + big_step (Case e e1 e2) v' + . +#[export] Hint Constructors big_step : core. +#[export] Hint Constructors base_step : core. +#[export] Hint Constructors contextual_step : core. + +Lemma fill_rtc_contextual_step {e1 e2} K : + rtc contextual_step e1 e2 → + rtc contextual_step (fill K e1) (fill K e2). +Proof. + induction 1 as [ | x y z H1 H2 IH]; first done. + etrans; last apply IH. + econstructor 2; last constructor 1. + by apply fill_contextual_step. +Qed. + +Lemma big_step_contextual e v : + big_step e v → rtc contextual_step e (of_val v). +Proof. + induction 1 as [ | | e1 e2 v1 v2 v' op H1 IH1 H2 IH2 Hop | e v v' op H1 IH1 Hop | e1 e2 x e v2 v H1 IH1 H2 IH2 H3 IH3 | e1 e2 v1 H1 IH1 H2 IH2 | | | e1 e2 v1 v2 x H1 IH1 H2 IH2 | e0 e1 e2 v H1 IH1 H2 IH2 | e0 e1 e2 v H1 IH1 H2 IH2| e1 e2 v1 v2 H1 IH1 H2 IH2 | e v1 v2 H IH | e v1 v2 H IH | e v H IH | e v H IH | e e1 e2 v v' H1 IH1 H2 IH2 | e e1 e2 v v' H1 IH1 H2 IH2 ]. + - constructor. + - constructor. + - (* binop *) + etrans. + { eapply (fill_rtc_contextual_step (BinOpRCtx _ _ HoleCtx)). apply IH2. } + etrans. + { eapply (fill_rtc_contextual_step (BinOpLCtx _ HoleCtx _)). apply IH1. } + simpl. + etrans. + { econstructor 2; last econstructor 1. + apply base_contextual_step. econstructor; last done. + all: apply to_of_val. + } + constructor. + - (* unop *) + etrans. + { eapply (fill_rtc_contextual_step (UnOpCtx _ HoleCtx)). apply IH1. } + simpl. etrans. + { econstructor 2; last econstructor 1. + apply base_contextual_step. econstructor; last done. + all: apply to_of_val. + } + constructor. + - etrans. + { eapply (fill_rtc_contextual_step (AppRCtx _ HoleCtx)). apply IH2. } + etrans. + { eapply (fill_rtc_contextual_step (AppLCtx HoleCtx _)). apply IH1. } + simpl. etrans. + { econstructor 2; last econstructor 1. + apply base_contextual_step. constructor; [| reflexivity]. apply is_val_of_val. + } + apply IH3. + - etrans. + { eapply (fill_rtc_contextual_step (TAppCtx HoleCtx)). apply IH1. } + etrans. { econstructor 2; last constructor. apply base_contextual_step. by constructor. } + done. + - constructor. + - etrans. + { eapply (fill_rtc_contextual_step (PackCtx HoleCtx)). done. } + done. + - etrans. + { eapply (fill_rtc_contextual_step (UnpackCtx x HoleCtx e2)). done. } + etrans. + { econstructor 2; last constructor. apply base_contextual_step. simpl. constructor; last reflexivity. + apply is_val_spec. rewrite to_of_val. eauto. + } + done. + - etrans. + { eapply (fill_rtc_contextual_step (IfCtx HoleCtx _ _)). done. } + etrans. + { econstructor; last constructor. eapply base_contextual_step. econstructor. } + done. + - etrans. + { eapply (fill_rtc_contextual_step (IfCtx HoleCtx _ _)). done. } + etrans. + { econstructor; last constructor. eapply base_contextual_step. econstructor. } + done. + - etrans. + { eapply (fill_rtc_contextual_step (PairRCtx e1 HoleCtx)). done. } + etrans. + { eapply (fill_rtc_contextual_step (PairLCtx HoleCtx v2)). done. } + econstructor. + - etrans. + { eapply (fill_rtc_contextual_step (FstCtx HoleCtx)). done. } + econstructor. + { eapply base_contextual_step. simpl. constructor; apply is_val_of_val. } + econstructor. + - etrans. + { eapply (fill_rtc_contextual_step (SndCtx HoleCtx)). done. } + econstructor. + { eapply base_contextual_step. simpl. constructor; apply is_val_of_val. } + econstructor. + - etrans. + { eapply (fill_rtc_contextual_step (InjLCtx HoleCtx)). done. } + econstructor. + - etrans. + { eapply (fill_rtc_contextual_step (InjRCtx HoleCtx)). done. } + econstructor. + - etrans. + { eapply (fill_rtc_contextual_step (CaseCtx HoleCtx e1 e2)). done. } + simpl. econstructor. + { eapply base_contextual_step. constructor. apply is_val_of_val. } + done. + - etrans. + { eapply (fill_rtc_contextual_step (CaseCtx HoleCtx e1 e2)). done. } + simpl. econstructor. + { eapply base_contextual_step. constructor. apply is_val_of_val. } + done. +Qed. + +Lemma big_step_of_val e v : + e = of_val v → + big_step e v. +Proof. + intros ->. + induction v; simpl; eauto. +Qed. + +Lemma big_step_val v v' : + big_step (of_val v) v' → v' = v. +Proof. + enough (∀ e, big_step e v' → e = of_val v → v' = v) by naive_solver. + intros e Hb. + induction Hb in v |-*; intros Heq; subst; destruct v; inversion Heq; subst; naive_solver. +Qed. + +Lemma big_step_preserve_closed e v : + is_closed [] e → big_step e v → is_closed [] v. +Proof. + intros Hcl. induction 1; try done. + all: simpl in Hcl; + repeat match goal with + | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H + end; try naive_solver. + - (* binOP *) + destruct v1 as [[] | | | | | |], v2 as [[] | | | | | |]; simpl in H1; try congruence. + destruct op; simpl in H1; inversion H1; done. + - (* unop *) + destruct v as [[] | | | | | |]; destruct op; simpl in H0; inversion H0; done. + - (* app *) + apply IHbig_step3. apply is_closed_do_subst'; naive_solver. + - (* unpack *) + apply IHbig_step2. apply is_closed_do_subst'; naive_solver. +Qed. diff --git a/theories/type_systems/systemf/exercises03.v b/theories/type_systems/systemf/exercises03.v new file mode 100644 index 0000000..13725fb --- /dev/null +++ b/theories/type_systems/systemf/exercises03.v @@ -0,0 +1,100 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.systemf Require Import lang notation types tactics. + +(** Exercise 3 (LN Exercise 22): Universal Fun *) + +Definition fun_comp : val := + #0 (* TODO *). +Definition fun_comp_type : type := + #0 (* TODO *). +Lemma fun_comp_typed : + TY 0; ∅ ⊢ fun_comp : fun_comp_type. +Proof. + (* should be solved by solve_typing. *) + (* TODO: exercise *) +Admitted. + + +Definition swap_args : val := + #0 (* TODO *). +Definition swap_args_type : type := + #0 (* TODO *). +Lemma swap_args_typed : + TY 0; ∅ ⊢ swap_args : swap_args_type. +Proof. + (* should be solved by solve_typing. *) + (* TODO: exercise *) +Admitted. + + +Definition lift_prod : val := + #0 (* TODO *). +Definition lift_prod_type : type := + #0 (* TODO *). +Lemma lift_prod_typed : + TY 0; ∅ ⊢ lift_prod : lift_prod_type. +Proof. + (* should be solved by solve_typing. *) + (* TODO: exercise *) +Admitted. + + +Definition lift_sum : val := + #0 (* TODO *). +Definition lift_sum_type : type := + #0 (* TODO *). +Lemma lift_sum_typed : + TY 0; ∅ ⊢ lift_sum : lift_sum_type. +Proof. + (* should be solved by solve_typing. *) + (* TODO: exercise *) +Admitted. + + +(** Exercise 5 (LN Exercise 18): Named to De Bruijn *) +Inductive ptype : Type := + | PTVar : string → ptype + | PInt + | PBool + | PTForall : string → ptype → ptype + | PTExists : string → ptype → ptype + | PFun (A B : ptype). + +Declare Scope PType_scope. +Delimit Scope PType_scope with pty. +Bind Scope PType_scope with ptype. +Coercion PTVar: string >-> ptype. +Infix "→" := PFun : PType_scope. +Notation "∀: x , τ" := + (PTForall x τ%pty) + (at level 100, τ at level 200) : PType_scope. +Notation "∃: x , τ" := + (PTExists x τ%pty) + (at level 100, τ at level 200) : PType_scope. + +Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type := + None (* FIXME *). + +(* Example *) +Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty. +Proof. + (* Should be solved by reflexivity. *) + (* TODO: exercise *) +Admitted. + + +Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty. +Proof. + (* Should be solved by reflexivity. *) + (* TODO: exercise *) +Admitted. + + +Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty. +Proof. + (* Should be solved by reflexivity. *) + (* TODO: exercise *) +Admitted. + + diff --git a/theories/type_systems/systemf/lang.v b/theories/type_systems/systemf/lang.v new file mode 100644 index 0000000..e7992cf --- /dev/null +++ b/theories/type_systems/systemf/lang.v @@ -0,0 +1,516 @@ +From stdpp Require Export binders strings. +From iris.prelude Require Import options. +From semantics.lib Require Export maps. + +Declare Scope expr_scope. +Declare Scope val_scope. +Delimit Scope expr_scope with E. +Delimit Scope val_scope with V. + +(** Expressions and vals. *) +Inductive base_lit : Set := + | LitInt (n : Z) | LitBool (b : bool) | LitUnit. +Inductive un_op : Set := + | NegOp | MinusUnOp. +Inductive bin_op : Set := + | PlusOp | MinusOp | MultOp (* Arithmetic *) + | LtOp | LeOp | EqOp. (* Comparison *) + + +Inductive expr := + | Lit (l : base_lit) + (* Base lambda calculus *) + | Var (x : string) + | Lam (x : binder) (e : expr) + | App (e1 e2 : expr) + (* Base types and their operations *) + | UnOp (op : un_op) (e : expr) + | BinOp (op : bin_op) (e1 e2 : expr) + | If (e0 e1 e2 : expr) + (* Polymorphism *) + | TApp (e : expr) + | TLam (e : expr) + | Pack (e : expr) + | Unpack (x : binder) (e1 e2 : expr) + (* Products *) + | Pair (e1 e2 : expr) + | Fst (e : expr) + | Snd (e : expr) + (* Sums *) + | InjL (e : expr) + | InjR (e : expr) + | Case (e0 : expr) (e1 : expr) (e2 : expr). + +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) +. + +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) + 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) + | _ => 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 + | _ => 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 ]; + simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto. + - rewrite IH. intros (v & ->). eauto. + - apply IH. eauto. + - rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto. + - rewrite IH1, IH2. eauto. + - rewrite IH. intros (v & ->). eauto. + - apply IH. eauto. + - rewrite IH. intros (v & ->); eauto. + - apply IH. eauto. +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 + end. + +(* Misc *) +Lemma is_val_of_val v : is_val (of_val v). +Proof. apply is_val_spec. rewrite to_of_val. eauto. Qed. + +(* literals and our operators have decidable equality. *) +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) + end. + +Definition subst' (mx : binder) (es : expr) : expr → expr := + match mx with BNamed x => subst x es | BAnon => id end. + +(** The stepping relation *) +Definition un_op_eval (op : un_op) (v : val) : option val := + match op, v with + | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b) + | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n) + | _, _ => None + end. + +Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit := + match op with + | PlusOp => Some $ LitInt (n1 + n2) + | MinusOp => Some $ LitInt (n1 - n2) + | MultOp => Some $ LitInt (n1 * n2) + | LtOp => Some $ LitBool (bool_decide (n1 < n2)) + | LeOp => Some $ LitBool (bool_decide (n1 ≤ n2)) + | EqOp => Some $ LitBool (bool_decide (n1 = n2)) + end%Z. + +Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := + match v1, v2 with + | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2 + | _, _ => None + end. + +Inductive base_step : expr → expr → Prop := + | BetaS x e1 e2 e' : + is_val e2 → + e' = subst' x e2 e1 → + base_step (App (Lam x e1) e2) e' + | TBetaS e1 : + base_step (TApp (TLam e1)) e1 + | UnpackS e1 e2 e' x : + is_val e1 → + e' = subst' x e1 e2 → + base_step (Unpack x (Pack e1) e2) e' + | UnOpS op e v v' : + to_val e = Some v → + un_op_eval op v = Some v' → + base_step (UnOp op e) (of_val v') + | BinOpS op e1 v1 e2 v2 v' : + to_val e1 = Some v1 → + to_val e2 = Some v2 → + bin_op_eval op v1 v2 = Some v' → + base_step (BinOp op e1 e2) (of_val v') + | IfTrueS e1 e2 : + base_step (If (Lit $ LitBool true) e1 e2) e1 + | IfFalseS e1 e2 : + base_step (If (Lit $ LitBool false) e1 e2) e2 + | FstS e1 e2 : + is_val e1 → + is_val e2 → + base_step (Fst (Pair e1 e2)) e1 + | SndS e1 e2 : + is_val e1 → + is_val e2 → + base_step (Snd (Pair e1 e2)) e2 + | CaseLS e e1 e2 : + is_val e → + base_step (Case (InjL e) e1 e2) (App e1 e) + | CaseRS e e1 e2 : + is_val e → + base_step (Case (InjR e) e1 e2) (App e2 e) +. + +(** We define evaluation contexts *) +Inductive ectx := + | HoleCtx + | AppLCtx (K: ectx) (v2 : val) + | AppRCtx (e1 : expr) (K: ectx) + | TAppCtx (K: ectx) + | PackCtx (K: ectx) + | UnpackCtx (x : binder)(K: ectx) (e2 : expr) + | UnOpCtx (op : un_op) (K: ectx) + | BinOpLCtx (op : bin_op) (K: ectx) (v2 : val) + | BinOpRCtx (op : bin_op) (e1 : expr) (K: ectx) + | IfCtx (K: ectx) (e1 e2 : expr) + | PairLCtx (K: ectx) (v2 : val) + | PairRCtx (e1 : expr) (K: ectx) + | FstCtx (K: ectx) + | SndCtx (K: ectx) + | InjLCtx (K: ectx) + | InjRCtx (K: ectx) + | CaseCtx (K: ectx) (e1 : expr) (e2 : expr) . + +Fixpoint fill (K : ectx) (e : expr) : expr := + match K with + | HoleCtx => e + | AppLCtx K v2 => App (fill K e) (of_val v2) + | AppRCtx e1 K => App e1 (fill K e) + | TAppCtx K => TApp (fill K e) + | PackCtx K => Pack (fill K e) + | UnpackCtx x K e2 => Unpack x (fill K e) e2 + | UnOpCtx op K => UnOp op (fill K e) + | BinOpLCtx op K v2 => BinOp op (fill K e) (of_val v2) + | BinOpRCtx op e1 K => BinOp op e1 (fill K e) + | IfCtx K e1 e2 => If (fill K e) e1 e2 + | PairLCtx K v2 => Pair (fill K e) (of_val v2) + | PairRCtx e1 K => Pair e1 (fill K e) + | FstCtx K => Fst (fill K e) + | SndCtx K => Snd (fill K e) + | InjLCtx K => InjL (fill K e) + | InjRCtx K => InjR (fill K e) + | CaseCtx K e1 e2 => Case (fill K e) e1 e2 + end. + +Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx := + match K with + | HoleCtx => K' + | AppLCtx K v2 => AppLCtx (comp_ectx K K') v2 + | AppRCtx e1 K => AppRCtx e1 (comp_ectx K K') + | TAppCtx K => TAppCtx (comp_ectx K K') + | PackCtx K => PackCtx (comp_ectx K K') + | UnpackCtx x K e2 => UnpackCtx x (comp_ectx K K') e2 + | UnOpCtx op K => UnOpCtx op (comp_ectx K K') + | BinOpLCtx op K v2 => BinOpLCtx op (comp_ectx K K') v2 + | BinOpRCtx op e1 K => BinOpRCtx op e1 (comp_ectx K K') + | IfCtx K e1 e2 => IfCtx (comp_ectx K K') e1 e2 + | PairLCtx K v2 => PairLCtx (comp_ectx K K') v2 + | PairRCtx e1 K => PairRCtx e1 (comp_ectx K K') + | FstCtx K => FstCtx (comp_ectx K K') + | SndCtx K => SndCtx (comp_ectx K K') + | InjLCtx K => InjLCtx (comp_ectx K K') + | InjRCtx K => InjRCtx (comp_ectx K K') + | CaseCtx K e1 e2 => CaseCtx (comp_ectx K K') e1 e2 + end. + +(** Contextual steps *) +Inductive contextual_step (e1 : expr) (e2 : expr) : Prop := + Ectx_step K e1' e2' : + e1 = fill K e1' → e2 = fill K e2' → + base_step e1' e2' → contextual_step e1 e2. + +Definition reducible (e : expr) := + ∃ e', contextual_step e e'. + + +Definition empty_ectx := HoleCtx. + +(** Basic properties about the language *) +Lemma fill_empty e : fill empty_ectx e = e. +Proof. done. Qed. + +Lemma fill_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e. +Proof. induction K1; simpl; congruence. Qed. + + + +Lemma base_contextual_step e1 e2 : + base_step e1 e2 → contextual_step e1 e2. +Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed. + +Lemma fill_contextual_step K e1 e2 : + contextual_step e1 e2 → contextual_step (fill K e1) (fill K e2). +Proof. + destruct 1 as [K' e1' e2' -> ->]. + rewrite !fill_comp. by econstructor. +Qed. + +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 => is_closed X e + | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 => is_closed X e1 && is_closed X e2 + | If e0 e1 e2 | Case e0 e1 e2 => + is_closed X e0 && is_closed X e1 && is_closed X e2 + end. + +(** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *) +Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e). +#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e). +Proof. unfold closed. apply _. Qed. +#[export] Instance closed_dec X e : Decision (closed X e). +Proof. unfold closed. apply _. Defined. + +(** closed expressions *) +Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e. +Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed. + +Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e. +Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed. + +Lemma is_closed_subst X e x es : + is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e). +Proof. + intros ?. + induction e in X |-*; simpl; intros ?; destruct_and?; split_and?; simplify_option_eq; + try match goal with + | H : ¬(_ ∧ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable] + end; eauto using is_closed_weaken with set_solver. +Qed. +Lemma is_closed_do_subst' X e x es : + is_closed [] es → is_closed (x :b: X) e → is_closed X (subst' x es e). +Proof. destruct x; eauto using is_closed_subst. Qed. + +(** 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. + + +(* we derive a few lemmas about contextual steps *) +Lemma contextual_step_app_l e1 e1' e2: + is_val e2 → + contextual_step e1 e1' → + contextual_step (App e1 e2) (App e1' e2). +Proof. + intros [v <-%of_to_val]%is_val_spec Hcontextual. + by eapply (fill_contextual_step (AppLCtx HoleCtx v)). +Qed. + +Lemma contextual_step_app_r e1 e2 e2': + contextual_step e2 e2' → + contextual_step (App e1 e2) (App e1 e2'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (AppRCtx e1 HoleCtx)). +Qed. + +Lemma contextual_step_tapp e e': + contextual_step e e' → + contextual_step (TApp e) (TApp e'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (TAppCtx HoleCtx)). +Qed. + +Lemma contextual_step_pack e e': + contextual_step e e' → + contextual_step (Pack e) (Pack e'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (PackCtx HoleCtx)). +Qed. + +Lemma contextual_step_unpack x e e' e2: + contextual_step e e' → + contextual_step (Unpack x e e2) (Unpack x e' e2). + Proof. + intros Hcontextual. + by eapply (fill_contextual_step (UnpackCtx x HoleCtx e2)). + Qed. + +Lemma contextual_step_unop op e e': + contextual_step e e' → + contextual_step (UnOp op e) (UnOp op e'). + Proof. + intros Hcontextual. + by eapply (fill_contextual_step (UnOpCtx op HoleCtx)). + Qed. + +Lemma contextual_step_binop_l op e1 e1' e2: + is_val e2 → + contextual_step e1 e1' → + contextual_step (BinOp op e1 e2) (BinOp op e1' e2). +Proof. + intros [v <-%of_to_val]%is_val_spec Hcontextual. + by eapply (fill_contextual_step (BinOpLCtx op HoleCtx v)). +Qed. + +Lemma contextual_step_binop_r op e1 e2 e2': + contextual_step e2 e2' → + contextual_step (BinOp op e1 e2) (BinOp op e1 e2'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (BinOpRCtx op e1 HoleCtx)). +Qed. + +Lemma contextual_step_if e e' e1 e2: + contextual_step e e' → + contextual_step (If e e1 e2) (If e' e1 e2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (IfCtx HoleCtx e1 e2)). +Qed. + +Lemma contextual_step_pair_l e1 e1' e2: + is_val e2 → + contextual_step e1 e1' → + contextual_step (Pair e1 e2) (Pair e1' e2). +Proof. + intros [v <-%of_to_val]%is_val_spec Hcontextual. + by eapply (fill_contextual_step (PairLCtx HoleCtx v)). +Qed. + +Lemma contextual_step_pair_r e1 e2 e2': + contextual_step e2 e2' → + contextual_step (Pair e1 e2) (Pair e1 e2'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (PairRCtx e1 HoleCtx)). +Qed. + + +Lemma contextual_step_fst e e': + contextual_step e e' → + contextual_step (Fst e) (Fst e'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (FstCtx HoleCtx)). +Qed. + +Lemma contextual_step_snd e e': + contextual_step e e' → + contextual_step (Snd e) (Snd e'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (SndCtx HoleCtx)). +Qed. + +Lemma contextual_step_injl e e': + contextual_step e e' → + contextual_step (InjL e) (InjL e'). + Proof. + intros Hcontextual. + by eapply (fill_contextual_step (InjLCtx HoleCtx)). + Qed. + +Lemma contextual_step_injr e e': + contextual_step e e' → + contextual_step (InjR e) (InjR e'). + Proof. + intros Hcontextual. + by eapply (fill_contextual_step (InjRCtx HoleCtx)). + Qed. + +Lemma contextual_step_case e e' e1 e2: + contextual_step e e' → + contextual_step (Case e e1 e2) (Case e' e1 e2). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)). +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 : core. diff --git a/theories/type_systems/systemf/notation.v b/theories/type_systems/systemf/notation.v new file mode 100644 index 0000000..563b111 --- /dev/null +++ b/theories/type_systems/systemf/notation.v @@ -0,0 +1,90 @@ +From semantics.ts.systemf Require Export lang. +Set Default Proof Using "Type". + + +(** Coercions to make programs easier to type. *) +Coercion of_val : val >-> expr. +Coercion LitInt : Z >-> base_lit. +Coercion LitBool : bool >-> base_lit. +Coercion App : expr >-> Funclass. +Coercion Var : string >-> expr. + +(** Define some derived forms. *) +Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing). +Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing). +Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing). + +(* No scope for the values, does not conflict and scope is often not inferred +properly. *) +Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l"). +Notation "# l" := (Lit l%Z%E%stdpp) (at level 8, format "# l") : expr_scope. + +(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come + first. *) +Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. +Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. + +Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := + (Match e0 x1%binder e1 x2%binder e2) + (e0, x1, e1, x2, e2 at level 200, + format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope. +Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := + (Match e0 x2%binder e2 x1%binder e1) + (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. + +Notation "()" := LitUnit : val_scope. + +Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope. +Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope. +Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope. +Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope. +Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope. +Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope. + +(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*) + +Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) + (at level 200, e1, e2, e3 at level 200) : expr_scope. + +Notation "λ: x , e" := (Lam x%binder e%E) + (at level 200, x at level 1, e at level 200, + format "'[' 'λ:' x , '/ ' e ']'") : expr_scope. +Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..)) + (at level 200, x, y, z at level 1, e at level 200, + format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope. + +Notation "λ: x , e" := (LamV x%binder e%E) + (at level 200, x at level 1, e at level 200, + format "'[' 'λ:' x , '/ ' e ']'") : val_scope. +Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. )) + (at level 200, x, y, z at level 1, e at level 200, + format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope. + +Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E) + (at level 200, x at level 1, e1, e2 at level 200, + format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. +Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E) + (at level 100, e2 at level 200, + format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope. + + +Notation "'Λ' , e" := (TLam e%E) + (at level 200, e at level 200, + format "'[' 'Λ' , '/ ' e ']'") : expr_scope. +Notation "'Λ' , e" := (TLamV e%E) + (at level 200, e at level 200, + format "'[' 'Λ' , '/ ' e ']'") : val_scope. + +(* the [e] always needs to be paranthesized, due to the level + (chosen to make this cooperate with the [App] coercion) *) +Notation "e '<>'" := (TApp e%E) + (at level 10) : expr_scope. +(*Check ((Λ, #4) <>)%E.*) +(*Check (((λ: "x", "x") #5) <>)%E.*) + +Notation "'pack' e" := (Pack e%E) + (at level 200, e at level 200) : expr_scope. +Notation "'pack' v" := (PackV v%V) + (at level 200, v at level 200) : val_scope. +Notation "'unpack' e1 'as' x 'in' e2" := (Unpack x%binder e1%E e2%E) + (at level 200, e1, e2 at level 200, x at level 1) : expr_scope. diff --git a/theories/type_systems/systemf/parallel_subst.v b/theories/type_systems/systemf/parallel_subst.v new file mode 100644 index 0000000..8f8987b --- /dev/null +++ b/theories/type_systems/systemf/parallel_subst.v @@ -0,0 +1,180 @@ +From stdpp Require Import prelude. +From iris Require Import prelude. +From semantics.ts.systemf 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) + 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. diff --git a/theories/type_systems/systemf/tactics.v b/theories/type_systems/systemf/tactics.v new file mode 100644 index 0000000..85eb10e --- /dev/null +++ b/theories/type_systems/systemf/tactics.v @@ -0,0 +1,113 @@ +From stdpp Require Import base relations. +From iris Require Import prelude. +From semantics.lib Require Import facts. +From semantics.ts.systemf Require Export lang notation parallel_subst types bigstep. + +Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B. +Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed. +Lemma list_subseteq_cons_binder A B x : A ⊆ B → x :b: A ⊆ x :b: B. +Proof. destruct x; first done. apply list_subseteq_cons. Qed. + +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 + 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 + | |- _ ∉ ?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. + + +Ltac bs_step_det := + repeat match goal with + | |- big_step ?e _ => + simpl; + match e with + (* case analysis, don't backtrack but pose the goal to the user *) + | Case _ _ _ => idtac + | If _ _ _ => idtac + (* use the value lemma *) + | of_val _ => apply big_step_of_val; done + (* try to solve substitutions by using disjointness assumptions *) + | context[decide (?p = ?p)] => rewrite decide_True; [ | done] + | context[decide (_ = _)] => rewrite decide_True; [ | congruence] + | context[decide (_ = _)] => rewrite decide_False; [ | congruence] + | context[decide (_ ≠ _)] => rewrite decide_True; [ | congruence] + | context[decide (_ ≠ _)] => rewrite decide_False; [ | congruence] + (* if we have a substitution that didn't simplify, try to show that it's closed *) + (* we don't make any attempt to solve it if it isn't closed under [] *) + | context[lang.subst _ _ ?e] => is_var e; rewrite subst_is_closed_nil; last solve[simplify_closed] + | context[lang.subst _ _ (of_val ?v)] => is_var v; rewrite subst_is_closed_nil; last solve[simplify_closed] + (* try to use a [big_step] assumption, or else apply a constructor *) + | _ => first [eassumption | econstructor] + end + | |- bin_op_eval _ _ _ = _ => + simpl; reflexivity + end; simplify_closed. +Ltac bs_steps_det := repeat bs_step_det. + +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 := + repeat match goal with + | |- TY _ ; _ ⊢ ?e : ?A => first [eassumption | econstructor] + (* heuristic to solve tapp goals where we need to pick the right type for the substitution *) + | |- TY _ ; _ ⊢ ?e <> : ?A => eapply typed_tapp'; [solve_typing | | asimpl; reflexivity] + | |- bin_op_typed _ _ _ _ => econstructor + | |- type_wf _ ?e => assert_fails (is_evar e); eassumption + | |- type_wf _ ?e => assert_fails (is_evar e); econstructor + | |- type_wf _ (subst _ ?A) => eapply type_wf_subst; [ | intros; simpl] + | |- type_wf _ ?e => assert_fails (is_evar e); eapply type_wf_mono; [eassumption | lia] + (* conditions spawned by the tyvar case of [type_wf] *) + | |- _ < _ => lia + (* conditions spawned by the variable case *) + | |- _ !! _ = Some _ => map_solver + end. + +Tactic Notation "unify_type" uconstr(A) := + match goal with + | |- TY ?n; ?Γ ⊢ ?e : ?B => unify A B + end. +Tactic Notation "replace_type" uconstr(A) := + match goal with + | |- TY ?n; ?Γ ⊢ ?e : ?B => replace B%ty with A%ty; cycle -1; first try by asimpl + end. diff --git a/theories/type_systems/systemf/types.v b/theories/type_systems/systemf/types.v new file mode 100644 index 0000000..d6ffb7e --- /dev/null +++ b/theories/type_systems/systemf/types.v @@ -0,0 +1,866 @@ +From stdpp Require Import base relations. +From iris Require Import prelude. +From semantics.lib Require Import maps. +From semantics.ts.systemf 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). + +(** 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). + +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. + + +(** 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 "⤉ Γ"). + +Reserved Notation "'TY' n ; Γ ⊢ e : A" (at level 74, e, A at next level). + +(** [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) +. +#[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. + +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 +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. +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. + +#[global] +Hint Resolve ctx_wf_empty ctx_wf_insert ctx_wf_up : 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 Γ → + TY n; Γ ⊢ e : A → + type_wf n A. +Proof. + intros Hwf; 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 ]; eauto. + - eapply type_wf_single_subst; first done. + specialize (IH Hwf) as Hwf'. + by inversion Hwf'. + - specialize (IHA Hwf) as Hwf'. + by inversion Hwf'; subst. + - inversion Hop; subst; eauto. + - inversion Hop; subst; eauto. + - specialize (IH Hwf) as Hwf'. by inversion Hwf'; subst. + - specialize (IH Hwf) as Hwf'. by inversion Hwf'; subst. + - specialize (IHe1 Hwf) as Hwf''. by inversion Hwf''; subst. +Qed. + +Lemma renaming_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 | | | | | | | | | | | | | ] in Δ, m |-*; intros Hsub 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_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_inclusion. +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. +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. + +(** 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 typed_substitutivity n e e' Γ (x: string) A B : + TY 0; ∅ ⊢ e' : A → + TY n; (<[x := A]> Γ) ⊢ e : B → + TY n; Γ ⊢ lang.subst x e' e : B. +Proof. + intros He'. revert n B Γ; induction e as [| y | y | | | | | | | | | | | | | | ]; intros 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| |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. + eapply IHe. revert Hty. rewrite fmap_insert. + eapply syn_typed_wf in He'; last by naive_solver. + 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. + eapply IHe2. rewrite type_wf_closed in Hty2; first done. + eapply syn_typed_wf; last apply He'. done. + - intros (? & ? & -> & ? & ?) % pair_inversion. eauto. + - intros (? & ?)%fst_inversion. eauto. + - intros (? & ?)%snd_inversion. eauto. + - intros (? & ? & -> & ? & ?)%injl_inversion. eauto. + - intros (? & ? & -> & ? & ?)%injr_inversion. eauto. + - intros (? & ? & ? & ? & ?)%case_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. + +(** Progress *) +Lemma typed_progress e A: + TY 0; ∅ ⊢ e : A → is_val e ∨ reducible e. +Proof. + 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]. + - subst. naive_solver. + - left. done. + - left. done. + - (* big lambda *) left; done. + - (* type app *) + right. destruct (IH 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' H1]. eexists. eauto. + - (* pack *) + (* FIXME this will be an exercise for you soon :) *) + admit. + - (* unpack *) + (* FIXME this will be an exercise for you soon :) *) + admit. + - (* int *)left. done. + - (* bool*) left. done. + - (* unit *) left. done. + - (* if *) + destruct (IH1 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' Hstep]. + eexists. eauto. + - (* app *) + destruct (IH2 HeqΓ Heqn) as [H2|H2]; [destruct (IH1 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. destruct H1 as [e1' Hstep]. + eexists. eauto. + + right. destruct H2 as [e2' H2]. + eexists. eauto. + - (* binop *) + assert (A = Int ∧ B = Int) as [-> ->]. + { inversion Hop; subst A B C; done. } + destruct (IH2 HeqΓ Heqn) as [H2|H2]; [destruct (IH1 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. destruct H1 as [e1' Hstep]. eexists. eauto. + + right. destruct H2 as [e2' H2]. eexists. eauto. + - (* unop *) + inversion Hop; subst A B op. + + right. destruct (IH 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' H2]. eexists. eauto. + + right. destruct (IH 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' H2]. eexists. eauto. + - (* pair *) + destruct (IH2 HeqΓ Heqn) as [H2|H2]; [destruct (IH1 HeqΓ Heqn) as [H1|H1]|]. + + left. done. + + right. destruct H1 as [e1' Hstep]. eexists. eauto. + + right. destruct H2 as [e2' H2]. eexists. eauto. + - (* fst *) + destruct (IH 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]. eexists. eauto. + - (* snd *) + destruct (IH 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]. eexists. eauto. + - (* injl *) + destruct (IH HeqΓ Heqn) as [H | H]. + + left. done. + + right. destruct H as [e' H]. eexists. eauto. + - (* injr *) + destruct (IH HeqΓ Heqn) as [H | H]. + + left. done. + + right. destruct H as [e' H]. eexists. eauto. + - (* case *) + right. destruct (IHe 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' H1]. eexists. eauto. +(*Qed.*) +Admitted. + + + + +Definition ectx_typing (K: ectx) (A B: type) := + ∀ e, TY 0; ∅ ⊢ e : A → TY 0; ∅ ⊢ (fill K e) : B. + + +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; induction K in A |-*; simpl; inversion 1; subst; eauto. + all: edestruct IHK as (? & ? & ?); 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 σ Γ: ⤉(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 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. 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. 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. +Qed. + +Lemma typed_subst_type_closed C e A: + type_wf 0 C → TY 1; ⤉∅ ⊢ e : A → TY 0; ∅ ⊢ e : A.[C/]. +Proof. + intros Hwf Hty. eapply typed_subst_type with (σ := C .: ids) (m := 0) in Hty; last first. + { intros [|k] Hlt; last lia. done. } + revert Hty. by rewrite !fmap_empty. +Qed. + +Lemma typed_subst_type_closed' x C B e A: + type_wf 0 A → + type_wf 1 C → + type_wf 0 B → + 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. + } + eapply typed_subst_type; first done. + intros [ | k] Hk; last lia. done. +Qed. + +Lemma typed_preservation_base_step e e' A: + TY 0; ∅ ⊢ e : A → + base_step e e' → + TY 0; ∅ ⊢ e' : A. +Proof. + intros Hty Hstep. destruct Hstep as [ | | | op e v v' Heq Heval | op e1 v1 e2 v2 v3 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). done. } + eapply lam_inversion in H1 as (C & D & Heq & Hwf & Hty). + injection Heq as -> ->. + 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 ->. by eapply typed_subst_type_closed. + - (* unpack *) + (* FIXME: this will be an exercise for you soon :) *) + admit. + - (* 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 <-. + 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 <-. + 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. + inversion Hop; subst; simpl in *; injection Heval as <-; constructor. + - by eapply if_inversion in Hty as (H1 & H2 & H3). + - by eapply if_inversion in Hty as (H1 & H2 & H3). + - by eapply fst_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion). + - by eapply snd_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion). + - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injl_inversion & ? & ?). + eauto. + - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty & ?)%injr_inversion & ? & ?). + eauto. +(*Qed.*) +Admitted. + +Lemma typed_preservation e e' A: + TY 0; ∅ ⊢ e : A → + contextual_step e e' → + TY 0; ∅ ⊢ e' : A. +Proof. + intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep]. + eapply fill_typing_decompose in Hty as [B [H1 H2]]. + eapply fill_typing_compose; last done. + by eapply typed_preservation_base_step. +Qed. + +Lemma typed_safety e1 e2 A: + TY 0; ∅ ⊢ e1 : A → + rtc contextual_step e1 e2 → + is_val e2 ∨ reducible e2. +Proof. + induction 2; eauto using typed_progress, typed_preservation. +Qed. + +(** derived typing rules *) +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.