From 0538dc6c8aa9e39808ffe1bac5a0cb6342ddfa2b Mon Sep 17 00:00:00 2001 From: mueck Date: Wed, 8 Nov 2023 15:15:07 +0100 Subject: [PATCH] Solution for exercises02 --- _CoqProject | 4 + theories/type_systems/stlc/exercises02_sol.v | 378 ++++++++++++++++++ .../type_systems/stlc_extended/bigstep_sol.v | 69 ++++ .../type_systems/stlc_extended/ctxstep_sol.v | 211 ++++++++++ .../type_systems/stlc_extended/types_sol.v | 350 ++++++++++++++++ 5 files changed, 1012 insertions(+) create mode 100644 theories/type_systems/stlc/exercises02_sol.v create mode 100644 theories/type_systems/stlc_extended/bigstep_sol.v create mode 100644 theories/type_systems/stlc_extended/ctxstep_sol.v create mode 100644 theories/type_systems/stlc_extended/types_sol.v diff --git a/_CoqProject b/_CoqProject index 2ef3baf..1786b8b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -22,8 +22,11 @@ theories/type_systems/stlc/types.v theories/type_systems/stlc_extended/lang.v theories/type_systems/stlc_extended/notation.v theories/type_systems/stlc_extended/types.v +theories/type_systems/stlc_extended/types_sol.v 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 # By removing the # below, you can add the exercise sheets to make #theories/type_systems/warmup/warmup.v @@ -31,3 +34,4 @@ theories/type_systems/stlc_extended/ctxstep.v #theories/type_systems/stlc/exercises01.v #theories/type_systems/stlc/exercises01_sol.v #theories/type_systems/stlc/exercises02.v +#theories/type_systems/stlc/exercises02_sol.v diff --git a/theories/type_systems/stlc/exercises02_sol.v b/theories/type_systems/stlc/exercises02_sol.v new file mode 100644 index 0000000..59d035c --- /dev/null +++ b/theories/type_systems/stlc/exercises02_sol.v @@ -0,0 +1,378 @@ +From stdpp Require Import gmap base relations tactics. +From iris Require Import prelude. +From semantics.ts.stlc Require Import lang notation. +From semantics.ts.stlc Require untyped types. + + +(** README: Please also download the assigment sheet as a *.pdf from here: + https://cms.sic.saarland/semantics_ws2324/materials/ + It contains additional explanation and excercises. **) + +(** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *) +(** You will find it very helpful to separately derive the structural rules of the + structural semantics for the contextual semantics. *) + +Lemma contextual_step_beta x e e': + is_val e' → contextual_step ((λ: x, e) e') (subst' x e' e). +Proof. + intros Hval. eapply base_contextual_step, BetaS; done. +Qed. + +Lemma contextual_step_app_r (e1 e2 e2': expr) : + contextual_step e2 e2' → + contextual_step (e1 e2) (e1 e2'). +Proof. + intros Hval. by eapply fill_contextual_step with (K := AppRCtx e1 HoleCtx). +Qed. + +Lemma contextual_step_app_l (e1 e1' e2: expr) : + is_val e2 → + contextual_step e1 e1' → + contextual_step (e1 e2) (e1' e2). +Proof. + intros Hval. eapply is_val_spec in Hval as [v Hval]. + eapply of_to_val in Hval as <-. + eapply fill_contextual_step with (K := (AppLCtx HoleCtx v)). +Qed. + +Lemma contextual_step_plus_red (n1 n2 n3: Z) : + (n1 + n2)%Z = n3 → + contextual_step (n1 + n2)%E n3. +Proof. + intros Hval. eapply base_contextual_step, PlusS; done. +Qed. + +Lemma contextual_step_plus_r e1 e2 e2' : + contextual_step e2 e2' → + contextual_step (Plus e1 e2) (Plus e1 e2'). +Proof. + intros Hval. by eapply fill_contextual_step with (K := (PlusRCtx e1 HoleCtx)). +Qed. + +Lemma contextual_step_plus_l e1 e1' e2 : + is_val e2 → + contextual_step e1 e1' → + contextual_step (Plus e1 e2) (Plus e1' e2). +Proof. + intros Hval. eapply is_val_spec in Hval as [v Hval]. + eapply of_to_val in Hval as <-. + eapply fill_contextual_step with (K := (PlusLCtx HoleCtx v)). +Qed. + +(** We register these lemmas as hints for [eauto]. *) +#[global] +Hint Resolve contextual_step_beta contextual_step_app_l contextual_step_app_r contextual_step_plus_red contextual_step_plus_l contextual_step_plus_r : core. + +Lemma step_contextual_step e1 e2: step e1 e2 → contextual_step e1 e2. +Proof. + (* The hints above make sure eauto uses the right lemmas. *) + induction 1; eauto. +Qed. + +(** Now the other direction. *) +(* You may find it helpful to introduce intermediate lemmas. *) + +Lemma base_step_step e1 e2: + base_step e1 e2 → step e1 e2. +Proof. + destruct 1; subst. + - eauto. + - by econstructor. +Qed. + +Lemma fill_step K e1 e2: + step e1 e2 → step (fill K e1) (fill K e2). +Proof. + induction K; simpl; eauto. +Qed. +Lemma contextual_step_step e1 e2: + contextual_step e1 e2 → step e1 e2. +Proof. + destruct 1 as [K h1 h2 -> -> Hstep]. + eapply fill_step, base_step_step, Hstep. +Qed. + + +(** ** Exercise 2: Scott encodings *) +Section scott. + (* take a look at untyped.v for usefull lemmas and definitions *) + Import semantics.ts.stlc.untyped. + + (** Scott encoding of Booleans *) + Definition true_scott : val := λ: "t" "f", "t". + Definition false_scott : val := λ: "t" "f", "f". + + Lemma true_red (v1 v2 : val) : + closed [] v1 → + closed [] v2 → + rtc step (true_scott v1 v2) v1. + Proof. + intros Hcl1 Hcl2. + eapply rtc_l. + { econstructor; first auto. + econstructor. auto. + } + simpl. + eapply rtc_l. + { econstructor; auto. } + simpl. + rewrite subst_closed_nil; done. + Qed. + + Lemma false_red (v1 v2 : val) : + closed [] v1 → + closed [] v2 → + rtc step (false_scott v1 v2) v2. + Proof. + intros Hcl1 Hcl2. + eapply rtc_l. + { econstructor; first auto. + econstructor. auto. + } + simpl. + eapply rtc_l. + { econstructor; auto. } + simpl. done. + Qed. + + (** Scott encoding of Pairs *) + Definition pair_scott : val := λ: "v1" "v2", λ: "d", "d" "v1" "v2". + + Definition fst_scott : val := λ: "p", "p" (λ: "a" "b", "a"). + Definition snd_scott : val := λ: "p", "p" (λ: "a" "b", "b"). + + Lemma fst_red (v1 v2 : val) : + is_closed [] v1 → + is_closed [] v2 → + rtc step (fst_scott (pair_scott v1 v2)) v1. + Proof. + intros Hcl1 Hcl2. + eapply rtc_l. + { econstructor 3. econstructor; first auto. + econstructor. auto. + } + simpl. eapply rtc_l. + { econstructor 3. econstructor; first auto. } + simpl. eapply rtc_l. + { econstructor. done. } + simpl. eapply rtc_l. + { econstructor. done. } + simpl. + rewrite !(subst_closed_nil v1); [ | done..]. + rewrite subst_closed_nil; last done. + eapply rtc_l. + { econstructor; first auto. + econstructor. auto. + } + simpl. eapply rtc_l. + { econstructor; first auto. } + simpl. rewrite subst_closed_nil; done. + Qed. + + Lemma snd_red (v1 v2 : val) : + is_closed [] v1 → + is_closed [] v2 → + rtc step (snd_scott (pair_scott v1 v2)) v2. + Proof. + intros Hcl1 Hcl2. + eapply rtc_l. + { econstructor 3. econstructor; first auto. + econstructor. auto. + } + simpl. eapply rtc_l. + { econstructor 3. econstructor; first auto. } + simpl. eapply rtc_l. + { econstructor. done. } + simpl. eapply rtc_l. + { econstructor. done. } + simpl. + rewrite !(subst_closed_nil v2); [ | done..]. + rewrite !(subst_closed_nil v1); [ | done..]. + eapply rtc_l. + { econstructor; first auto. + econstructor. auto. + } + simpl. eapply rtc_l. + { econstructor; first auto. } + simpl. done. + Qed. + +End scott. + +Import semantics.ts.stlc.types. + +(** ** Exercise 3: type erasure *) +(** Source terms *) +Inductive src_expr := +| ELitInt (n: Z) +(* Base lambda calculus *) +| EVar (x : string) +| ELam (x : binder) (A: type) (e : src_expr) +| EApp (e1 e2 : src_expr) +(* Base types and their operations *) +| EPlus (e1 e2 : src_expr). + +(** The erasure function *) +Fixpoint erase (E: src_expr) : expr := +match E with +| ELitInt n => LitInt n +| EVar x => Var x +| ELam x A E => Lam x (erase E) +| EApp E1 E2 => App (erase E1) (erase E2) +| EPlus E1 E2 => Plus (erase E1) (erase E2) +end. + +Reserved Notation "Γ '⊢S' e : A" (at level 74, e, A at next level). +Inductive src_typed : typing_context → src_expr → type → Prop := +| src_typed_var Γ x A : + Γ !! x = Some A → + Γ ⊢S (EVar x) : A +| src_typed_lam Γ x E A B : + (<[ x := A]> Γ) ⊢S E : B → + Γ ⊢S (ELam (BNamed x) A E) : (A → B) +| src_typed_int Γ z : + Γ ⊢S (ELitInt z) : Int +| src_typed_app Γ E1 E2 A B : + Γ ⊢S E1 : (A → B) → + Γ ⊢S E2 : A → + Γ ⊢S EApp E1 E2 : B +| src_typed_add Γ E1 E2 : + Γ ⊢S E1 : Int → + Γ ⊢S E2 : Int → + Γ ⊢S EPlus E1 E2 : Int +where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope. +#[export] Hint Constructors src_typed : core. + +Lemma type_erasure_correctness Γ E A: + (Γ ⊢S E : A)%ty → (Γ ⊢ erase E : A)%ty. +Proof. + induction 1; simpl; eauto. +Qed. + +(** ** Exercise 4: Unique Typing *) +Lemma src_typing_unique Γ E A B: + (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B. +Proof. + induction 1 as [ | ????? H1 IH1 | | ????? H1 IH1 H2 IH2 | ??? H1 IH1 H2 IH2] in B |-*; inversion 1; subst; try congruence. + - f_equal. eauto. + - rename select (_ ⊢S _ : (_ → _))%ty into Ha. + eapply IH1 in Ha. by injection Ha. +Qed. + +(** TODO: Is runtime typing (Curry-style) also unique? Prove it or give a counterexample. *) +(** Runtime typing is not unique! *) +Lemma id_int: (∅ ⊢ (λ: "x", "x") : (Int → Int))%ty. +Proof. eauto. Qed. + +Lemma id_int_to_int: (∅ ⊢ (λ: "x", "x") : ((Int → Int) → (Int → Int)))%ty. +Proof. eauto. Qed. + +(** ** Exercise 5: Type Inference *) + +Fixpoint type_eq A B := + match A, B with + | Int, Int => true + | Fun A B, Fun A' B' => type_eq A A' && type_eq B B' + | _, _ => false + end. + +Lemma type_eq_iff A B: type_eq A B ↔ A = B. +Proof. + induction A in B |-*; destruct B; simpl; naive_solver. +Qed. + +Notation ctx := (gmap string type). +Fixpoint infer_type (Γ: ctx) E := + match E with + | EVar x => Γ !! x + | ELam (BNamed x) A E => + match infer_type (<[x := A]> Γ) E with + | Some B => Some (Fun A B) + | None => None + end + | ELitInt l => Some Int + | EApp E1 E2 => + match infer_type Γ E1, infer_type Γ E2 with + | Some (Fun A B), Some C => if type_eq A C then Some B else None + | _, _ => None + end + | EPlus E1 E2 => + match infer_type Γ E1, infer_type Γ E2 with + | Some Int, Some Int => Some Int + | _, _ => None + end + | ELam BAnon A E => None + end. + +(** Prove both directions of the correctness theorem. *) +Lemma infer_type_typing Γ E A: + infer_type Γ E = Some A → (Γ ⊢S E : A)%ty. +Proof. + induction E as [l|x|x B E IH|E1 IH1 E2 IH2|E1 IH1 E2 IH2] in Γ, A |-*; simpl. + - destruct l; naive_solver. + - eauto. + - destruct x as [|x]; first naive_solver. + destruct infer_type eqn: Heq; last naive_solver. + eapply IH in Heq. injection 1 as <-. eauto. + - destruct infer_type as [B|] eqn: Heq1; last naive_solver. + destruct B as [|B1 B2]; try naive_solver. + destruct (infer_type Γ E2) as [C|] eqn: Heq2; last naive_solver. + destruct type_eq eqn: Heq3; last naive_solver. + injection 1 as <-. eapply Is_true_eq_left in Heq3. + eapply type_eq_iff in Heq3 as ->. + eauto. + - destruct infer_type as [B|] eqn: Heq1; last naive_solver. + destruct B; try naive_solver. + destruct (infer_type Γ E2) as [C|] eqn: Heq2; last naive_solver. + destruct C; naive_solver. +Qed. + +Lemma typing_infer_type Γ E A: + (Γ ⊢S E : A)%ty → infer_type Γ E = Some A. +Proof. + induction 1; simpl; eauto. + - by rewrite IHsrc_typed. + - rewrite IHsrc_typed1 IHsrc_typed2. + rewrite (Is_true_eq_true (type_eq A A)) //=. + by eapply type_eq_iff. + - by rewrite IHsrc_typed1 IHsrc_typed2. +Qed. + + +(** ** Exercise 6: untypable, safe term *) + +(* The exercise asks you to: + "Give one example if there is such an expression, otherwise prove their non-existence." + So either finish one section or the other. +*) + +Section give_example. + Definition ust : expr := (λ: "f", 5) (λ: "x", 0 0)%E. + + Lemma ust_safe e': + rtc step ust e' → is_val e' ∨ reducible e'. + Proof. + inversion 1 as [ | x y z H1 H2]; subst. + - right. eexists. eapply StepBeta. done. + - inversion H1 as [??? Ha | ??? Ha Hb | ??? Ha | | ??? Ha Hb | ??? Ha ]; subst. + + simpl in H2. inversion H2 as [ | ??? [] _]; subst; eauto. + + inversion Hb. + + inversion Ha. + Qed. + + Lemma ust_no_type Γ A: + ¬ (Γ ⊢ ust : A)%ty. + Proof. + intros H. inversion H; subst. + inversion H5; subst. inversion H6; subst. + inversion H4. + Qed. +End give_example. + +Section prove_non_existence. + Lemma no_ust : + ∀ e, (∀ e', rtc step e e' → is_val e' ∨ reducible e') → ∃ A, (∅ ⊢ e : A)%ty. + Proof. + (* This is not possible as shown above *) + Abort. +End prove_non_existence. \ No newline at end of file diff --git a/theories/type_systems/stlc_extended/bigstep_sol.v b/theories/type_systems/stlc_extended/bigstep_sol.v new file mode 100644 index 0000000..4d97292 --- /dev/null +++ b/theories/type_systems/stlc_extended/bigstep_sol.v @@ -0,0 +1,69 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.stlc_extended Require Import lang notation. + +(** * Big-step semantics *) + +Implicit Types + (v : val) + (e : expr). + +Inductive big_step : expr → val → Prop := + | bs_lit (n : Z) : + big_step (LitInt n) (LitIntV n) + | bs_lam (x : binder) (e : expr) : + big_step (λ: x, e)%E (λ: x, e)%V + | 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 e2 v2 → + big_step (subst' x (of_val v2) e) v → + big_step (App e1 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. + +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. diff --git a/theories/type_systems/stlc_extended/ctxstep_sol.v b/theories/type_systems/stlc_extended/ctxstep_sol.v new file mode 100644 index 0000000..f54a90e --- /dev/null +++ b/theories/type_systems/stlc_extended/ctxstep_sol.v @@ -0,0 +1,211 @@ +From semantics.ts.stlc_extended Require Export lang. + +(** The stepping relation *) + +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' + | PlusS e1 e2 (n1 n2 n3 : Z): + e1 = (LitInt n1) → + e2 = (LitInt n2) → + (n1 + n2)%Z = n3 → + base_step (Plus e1 e2) (LitInt n3) + | 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) +. + +#[export] Hint Constructors base_step : core. + +(** We define evaluation contexts *) +Inductive ectx := + | HoleCtx + | AppLCtx (K: ectx) (v2 : val) + | AppRCtx (e1 : expr) (K: ectx) + | PlusLCtx (K: ectx) (v2 : val) + | PlusRCtx (e1 : expr) (K: ectx) + | 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) + | PlusLCtx K v2 => Plus (fill K e) (of_val v2) + | PlusRCtx e1 K => Plus e1 (fill K e) + | 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') + | PlusLCtx K v2 => PlusLCtx (comp_ectx K K') v2 + | PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K K') + | 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. + +#[export] Hint Constructors contextual_step : core. + +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. + +(** We derive a few lemmas about contextual steps: + these essentially provide rules for structural lifting + akin to the structural semantics. + *) +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_plus_l e1 e1' e2: + is_val e2 → + contextual_step e1 e1' → + contextual_step (Plus e1 e2) (Plus e1' e2). +Proof. + intros [v <-%of_to_val]%is_val_spec Hcontextual. + by eapply (fill_contextual_step (PlusLCtx HoleCtx v)). +Qed. + +Lemma contextual_step_plus_r e1 e2 e2': + contextual_step e2 e2' → + contextual_step (Plus e1 e2) (Plus e1 e2'). +Proof. + intros Hcontextual. + by eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)). +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. + +#[global] +Hint Resolve + contextual_step_app_l contextual_step_app_r contextual_step_plus_l contextual_step_plus_r + contextual_step_case contextual_step_fst contextual_step_injl contextual_step_injr + contextual_step_pair_l contextual_step_pair_r contextual_step_snd : core. diff --git a/theories/type_systems/stlc_extended/types_sol.v b/theories/type_systems/stlc_extended/types_sol.v new file mode 100644 index 0000000..680effa --- /dev/null +++ b/theories/type_systems/stlc_extended/types_sol.v @@ -0,0 +1,350 @@ +From stdpp Require Import base relations. +From iris Require Import prelude. +From semantics.lib Require Import maps. +From semantics.ts.stlc_extended Require Import lang notation ctxstep_sol. + +(** ** Syntactic typing *) +Inductive type : Type := + | Int + | Fun (A B : type) + | Prod (A B : type) + | Sum (A B : type). + +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. +Infix "→" := Fun : FType_scope. +Notation "(→)" := Fun (only parsing) : 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. + +Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level). + +Inductive syn_typed : typing_context → expr → type → Prop := + | typed_var Γ x A : + Γ !! x = Some A → + Γ ⊢ (Var x) : A + | typed_lam Γ x e A B : + (<[ x := A]> Γ) ⊢ e : B → + Γ ⊢ (Lam (BNamed x) e) : (A → B) + | typed_lam_anon Γ e A B : + Γ ⊢ e : B → + Γ ⊢ (Lam BAnon e) : (A → B) + | typed_int Γ z : Γ ⊢ (LitInt z) : Int + | typed_app Γ e1 e2 A B : + Γ ⊢ e1 : (A → B) → + Γ ⊢ e2 : A → + Γ ⊢ (e1 e2)%E : B + | typed_add Γ e1 e2 : + Γ ⊢ e1 : Int → + Γ ⊢ e2 : Int → + Γ ⊢ e1 + e2 : Int + | typed_pair Γ e1 e2 A B : + Γ ⊢ e1 : A → + Γ ⊢ e2 : B → + Γ ⊢ (e1, e2) : A × B + | typed_fst Γ e A B : + Γ ⊢ e : A × B → + Γ ⊢ Fst e : A + | typed_snd Γ e A B : + Γ ⊢ e : A × B → + Γ ⊢ Snd e : B + | typed_injl Γ e A B : + Γ ⊢ e : A → + Γ ⊢ InjL e : A + B + | typed_injr Γ e A B : + Γ ⊢ e : B → + Γ ⊢ InjR e : A + B + | typed_case Γ e e1 e2 A B C : + Γ ⊢ e : B + C → + Γ ⊢ e1 : (B → A) → + Γ ⊢ e2 : (C → A) → + Γ ⊢ Case e e1 e2 : A +where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty). +#[export] Hint Constructors syn_typed : core. + +(** Examples *) +Goal ∅ ⊢ (λ: "x", "x")%E : (Int → Int). +Proof. eauto. Qed. + +Lemma syn_typed_closed Γ e A X : + Γ ⊢ e : A → + (∀ x, x ∈ dom Γ → x ∈ X) → + is_closed X e. +Proof. + (* TODO: you will need to add the new cases, i.e. "|"'s to the intro pattern. The proof then should go through *) + induction 1 as [ | ?????? IH | | | | | | | | | | ] 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. } + (* everything else *) + all: repeat match goal with + | |- Is_true (_ && _) => apply andb_True; split + end. + all: try naive_solver. +Qed. + +Lemma typed_weakening Γ Δ e A: + Γ ⊢ e : A → + Γ ⊆ Δ → + Δ ⊢ e : A. +Proof. + (* TODO: here you will need to add the new cases to the intro pattern as well. The proof then should go through *) + induction 1 as [| Γ x e A B Htyp IH | | | | | | | | | |] in Δ |-*; intros Hsub; eauto. + - (* var *) econstructor. by eapply lookup_weaken. + - (* lam *) econstructor. eapply IH; eauto. by eapply insert_mono. +Qed. + +(** Typing inversion lemmas *) +Lemma var_inversion Γ (x: string) A: Γ ⊢ x : A → Γ !! x = Some A. +Proof. inversion 1; subst; auto. Qed. + +Lemma lam_inversion Γ (x: string) e C: + Γ ⊢ (λ: x, e) : C → + ∃ A B, C = (A → B)%ty ∧ <[x:=A]> Γ ⊢ e : B. +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma lam_anon_inversion Γ e C: + Γ ⊢ (λ: <>, e) : C → + ∃ A B, C = (A → B)%ty ∧ Γ ⊢ e : B. +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma app_inversion Γ e1 e2 B: + Γ ⊢ e1 e2 : B → + ∃ A, Γ ⊢ e1 : (A → B) ∧ Γ ⊢ e2 : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma plus_inversion Γ e1 e2 B: + Γ ⊢ e1 + e2 : B → + B = Int ∧ Γ ⊢ e1 : Int ∧ Γ ⊢ e2 : Int. +Proof. inversion 1; subst; eauto. Qed. + + +(* There are the inversion lemmas for the new typing rules *) +Lemma pair_inversion Γ e1 e2 C : + Γ ⊢ (e1, e2) : C → + ∃ A B, C = (A × B)%ty ∧ Γ ⊢ e1 : A ∧ Γ ⊢ e2 : B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma fst_inversion Γ e A : + Γ ⊢ Fst e : A → + ∃ B, Γ ⊢ e : A × B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma snd_inversion Γ e B : + Γ ⊢ Snd e : B → + ∃ A, Γ ⊢ e : A × B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma injl_inversion Γ e C : + Γ ⊢ InjL e : C → + ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e : A. +Proof. inversion 1; subst; eauto. Qed. + +Lemma injr_inversion Γ e C : + Γ ⊢ InjR e : C → + ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e : B. +Proof. inversion 1; subst; eauto. Qed. + +Lemma case_inversion Γ e e1 e2 A : + Γ ⊢ Case e e1 e2 : A → + ∃ B C, Γ ⊢ e : B + C ∧ Γ ⊢ e1 : (B → A) ∧ Γ ⊢ e2 : (C → A). +Proof. inversion 1; subst; eauto. Qed. + +Lemma typed_substitutivity e e' Γ (x: string) A B : + ∅ ⊢ e' : A → + (<[x := A]> Γ) ⊢ e : B → + Γ ⊢ lang.subst x e' e : B. +Proof. + intros He'. revert B Γ; induction e as [y | y | | | | | | | | | ]; intros B Γ; simpl. + - intros Hp % var_inversion. + destruct (decide (x = y)). + + subst. rewrite lookup_insert in Hp. injection Hp as ->. + eapply typed_weakening; [done| ]. apply map_empty_subseteq. + + rewrite lookup_insert_ne in Hp; last done. auto. + - destruct y as [ | y]. + { intros (A' & C & -> & Hty) % lam_anon_inversion. + econstructor. destruct decide as [Heq|]. + + congruence. + + eauto. + } + intros (A' & C & -> & Hty) % lam_inversion. + econstructor. 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. + - inversion 1; subst; auto. + - intros (-> & Hty1 & Hty2)%plus_inversion; eauto. + - intros (? & ? & -> & ? & ?) % pair_inversion. eauto. + - intros (? & ?)%fst_inversion. eauto. + - intros (? & ?)%snd_inversion. eauto. + - intros (? & ? & -> & ?)%injl_inversion. eauto. + - intros (? & ? & -> & ?)%injr_inversion. eauto. + - intros (? & ? & ? & ? & ?)%case_inversion. eauto. +Qed. + +(** Canonical values *) +Lemma canonical_values_arr Γ e A B: + Γ ⊢ e : (A → B) → + is_val e → + ∃ x e', e = (λ: x, e')%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +Lemma canonical_values_int Γ e: + Γ ⊢ e : Int → + is_val e → + ∃ n: Z, e = (#n)%E. +Proof. + inversion 1; simpl; naive_solver. +Qed. + +(* canonical forms lemmas for the new types *) +Lemma canonical_values_prod Γ e A B : + Γ ⊢ 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 Γ e A B : + Γ ⊢ 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: + ∅ ⊢ e : A → is_val e ∨ reducible e. +Proof. + remember ∅ as Γ. + (* TODO: you will need to extend the intro pattern *) + induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2 | Γ e1 e2 A B Hty1 IH1 Hty2 IH2 | Γ e A B Hty IH | Γ e A B Hty IH | Γ e A B Hty IH | Γ e A B Hty IH| Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2]. + - subst. naive_solver. + - left. done. + - left. done. + - (* int *)left. done. + - (* app *) + destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) 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. + - (* plus *) + destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|]. + + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done. + eapply canonical_values_int in Hty2 as [n2 ->]; last done. + subst. eexists; eapply base_contextual_step. eauto. + + right. destruct H1 as [e1' Hstep]. eexists. eauto. + + right. destruct H2 as [e2' H2]. eexists. eauto. +- (* pair *) + destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) 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Γ) 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Γ) 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Γ) as [H | H]. + + left. done. + + right. destruct H as [e' H]. eexists. eauto. + - (* injr *) + destruct (IH HeqΓ) as [H | H]. + + left. done. + + right. destruct H as [e' H]. eexists. eauto. + - (* case *) + right. destruct (IHe HeqΓ) 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. + + +Definition ectx_typing (K: ectx) (A B: type) := + ∀ e, ∅ ⊢ e : A → ∅ ⊢ (fill K e) : B. + +Lemma fill_typing_decompose K e A: + ∅ ⊢ fill K e : A → + ∃ B, ∅ ⊢ e : B ∧ ectx_typing K B A. +Proof. + unfold ectx_typing; induction K in e,A |-*; simpl; eauto. + all: inversion 1; subst; edestruct IHK as [? [Hit Hty]]; eauto. +Qed. + +Lemma fill_typing_compose K e A B: + ∅ ⊢ e : B → + ectx_typing K B A → + ∅ ⊢ fill K e : A. +Proof. + intros H1 H2; by eapply H2. +Qed. + +Lemma typed_preservation_base_step e e' A: + ∅ ⊢ e : A → + base_step e e' → + ∅ ⊢ e' : A. +Proof. + intros Hty Hstep. + destruct Hstep as [ ]; subst. + - eapply app_inversion in Hty as (B & H1 & H2). + destruct x as [|x]. + { eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hty). done. } + eapply lam_inversion in H1 as (C & D & Heq & Hty). + injection Heq as -> ->. + eapply typed_substitutivity; eauto. + - eapply plus_inversion in Hty as (-> & Hty1 & Hty2). constructor. +- 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. + + +Lemma typed_preservation e e' A: + ∅ ⊢ e : A → + contextual_step e e' → + ∅ ⊢ 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 type_safety e1 e2 A: + ∅ ⊢ e1 : A → + rtc contextual_step e1 e2 → + is_val e2 ∨ reducible e2. +Proof. + induction 2; eauto using typed_progress, typed_preservation. +Qed.