From fb0a3219b5de10ac0de942d806902af46bb7388c Mon Sep 17 00:00:00 2001 From: mueck Date: Thu, 2 Nov 2023 16:03:25 +0100 Subject: [PATCH 1/3] Release exercises02 -- Coq code for the last exercise will be released soon --- _CoqProject | 3 + theories/type_systems/stlc/exercises02.v | 273 +++++++++++++++++++++++ theories/type_systems/stlc/lang.v | 19 ++ theories/type_systems/stlc/types.v | 235 +++++++++++++++++++ theories/type_systems/stlc/untyped.v | 221 ++++++++++++++++++ 5 files changed, 751 insertions(+) create mode 100644 theories/type_systems/stlc/exercises02.v create mode 100644 theories/type_systems/stlc/types.v create mode 100644 theories/type_systems/stlc/untyped.v diff --git a/_CoqProject b/_CoqProject index 5a2249c..9328d94 100644 --- a/_CoqProject +++ b/_CoqProject @@ -15,9 +15,12 @@ theories/lib/sets.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 # By removing the # below, you can add the exercise sheets to make #theories/type_systems/warmup/warmup.v #theories/type_systems/warmup/warmup_sol.v #theories/type_systems/stlc/exercises01.v #theories/type_systems/stlc/exercises01_sol.v +#theories/type_systems/stlc/exercises02.v diff --git a/theories/type_systems/stlc/exercises02.v b/theories/type_systems/stlc/exercises02.v new file mode 100644 index 0000000..a759308 --- /dev/null +++ b/theories/type_systems/stlc/exercises02.v @@ -0,0 +1,273 @@ +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. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_app_r (e1 e2 e2': expr) : + contextual_step e2 e2' → + contextual_step (e1 e2) (e1 e2'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_app_l (e1 e1' e2: expr) : + is_val e2 → + contextual_step e1 e1' → + contextual_step (e1 e2) (e1' e2). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_plus_red (n1 n2 n3: Z) : + (n1 + n2)%Z = n3 → + contextual_step (n1 + n2)%E n3. +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_plus_r e1 e2 e2' : + contextual_step e2 e2' → + contextual_step (Plus e1 e2) (Plus e1 e2'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_plus_l e1 e1' e2 : + is_val e2 → + contextual_step e1 e1' → + contextual_step (Plus e1 e2) (Plus e1' e2). +Proof. + (* TODO: exercise *) +Admitted. + + +(** 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. + (* TODO: exercise *) +Admitted. + + +(** Now the other direction. *) +(* You may find it helpful to introduce intermediate lemmas. *) + + +Lemma contextual_step_step e1 e2: + contextual_step e1 e2 → step e1 e2. +Proof. + (* TODO: exercise *) +Admitted. + + + +(** ** 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 := 0(* TODO *). + Definition false_scott : val := 0(* TODO *). + + Lemma true_red (v1 v2 : val) : + closed [] v1 → + closed [] v2 → + rtc step (true_scott v1 v2) v1. + Proof. + (* TODO: exercise *) + Admitted. + + + Lemma false_red (v1 v2 : val) : + closed [] v1 → + closed [] v2 → + rtc step (false_scott v1 v2) v2. + Proof. + (* TODO: exercise *) + Admitted. + + + (** Scott encoding of Pairs *) + Definition pair_scott : val := 0(* TODO *). + + Definition fst_scott : val := 0(* TODO *). + Definition snd_scott : val := 0(* TODO *). + + Lemma fst_red (v1 v2 : val) : + is_closed [] v1 → + is_closed [] v2 → + rtc step (fst_scott (pair_scott v1 v2)) v1. + Proof. + (* TODO: exercise *) + Admitted. + + + Lemma snd_red (v1 v2 : val) : + is_closed [] v1 → + is_closed [] v2 → + rtc step (snd_scott (pair_scott v1 v2)) v2. + Proof. + (* TODO: exercise *) + Admitted. + + +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 := +0 (* TODO *). + +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. + (* TODO: exercise *) +Admitted. + + +(** ** Exercise 4: Unique Typing *) +Lemma src_typing_unique Γ E A B: + (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B. +Proof. + (* TODO: exercise *) +Admitted. + + +(** TODO: Is runtime typing (Curry-style) also unique? Prove it or give a counterexample. *) + + +(** ** 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 + (* TODO: complete the definition for the remaining cases *) + | ELitInt l => None (* TODO *) + | EApp E1 E2 => None (* TODO *) + | EPlus E1 E2 => None (* TODO *) + | 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. + (* TODO: exercise *) +Admitted. + + +Lemma typing_infer_type Γ E A: + (Γ ⊢S E : A)%ty → infer_type Γ E = Some A. +Proof. + (* TODO: exercise *) +Admitted. + + + +(** ** 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 := 0 (* TODO *). + + Lemma ust_safe e': + rtc step ust e' → is_val e' ∨ reducible e'. + Proof. + (* TODO: exercise *) + Admitted. + + + Lemma ust_no_type Γ A: + ¬ (Γ ⊢ ust : A)%ty. + Proof. + (* TODO: exercise *) + Admitted. + +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. + (* TODO: exercise *) + Admitted. + +End prove_non_existence. \ No newline at end of file diff --git a/theories/type_systems/stlc/lang.v b/theories/type_systems/stlc/lang.v index b668d78..ee27fad 100644 --- a/theories/type_systems/stlc/lang.v +++ b/theories/type_systems/stlc/lang.v @@ -319,3 +319,22 @@ Qed. Lemma subst_closed_nil e x es : closed [] e → subst x es e = e. Proof. intros. apply subst_closed with []; set_solver. Qed. + +Lemma val_no_step e e': + step e e' → is_val e → False. +Proof. + by destruct 1. +Qed. + +Lemma val_no_step' (v : val) (e : expr) : + step (of_val v) e -> False. +Proof. + intros H. eapply (val_no_step _ _ H). + apply is_val_val. +Qed. + +Ltac val_no_step := + match goal with + | [H: step ?e1 ?e2 |- _] => + solve [exfalso; eapply (val_no_step _ _ H); done] + end. \ No newline at end of file diff --git a/theories/type_systems/stlc/types.v b/theories/type_systems/stlc/types.v new file mode 100644 index 0000000..67ec84d --- /dev/null +++ b/theories/type_systems/stlc/types.v @@ -0,0 +1,235 @@ +From stdpp Require Import base relations tactics. +From iris Require Import prelude. +From semantics.ts.stlc Require Import lang notation. +From semantics.lib Require Import sets maps. + +(** ** Syntactic typing *) +(** In the Coq formalization, we exclusively define runtime typing (Curry-style). *) +(** It will be an exercise to consider Church-style typing. *) + +Inductive type : Set := + | Int + | Fun (A B : type). + +Definition typing_context := gmap string type. +Implicit Types + (Γ : typing_context) + (v : val) + (e : expr) + (A : type) + (x: string). + +(** We define notation for types in a new scope with delimiter [ty]. + See below for an example. *) +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. + +(** Typing rules *) +(** We need to reserve the notation beforehand to already use it when defining the + typing rules. *) +Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level). +Inductive syn_typed : typing_context → expr → type → Prop := + | typed_var Γ x A : + (* lookup the variable in the context *) + Γ !! x = Some A → + Γ ⊢ (Var x) : A + | typed_lam Γ x e A B : + (* add a new type assignment to the context *) + (<[ x := A]> Γ) ⊢ e : B → + Γ ⊢ (Lam (BNamed x) e) : (A → B) + | typed_int Γ z : + Γ ⊢ (LitInt z) : Int + | typed_app Γ e1 e2 A B : + Γ ⊢ e1 : (A → B) → + Γ ⊢ e2 : A → + Γ ⊢ e1 e2 : B + | typed_add Γ e1 e2 : + Γ ⊢ e1 : Int → + Γ ⊢ e2 : Int → + Γ ⊢ e1 + e2 : Int +where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty) : FType_scope. +(** Add constructors to [eauto]'s hint database. *) +#[export] Hint Constructors syn_typed : core. +Local Open Scope FType_scope. + +(** a small example *) +Goal ∅ ⊢ (λ: "x", 1 + "x")%E : (Int → Int). +Proof. eauto. Qed. + +(** We derive some inversion lemmas -- this is cleaner than directly + using the [inversion] tactic everywhere.*) +Lemma var_inversion Γ (x: string) A: Γ ⊢ x : A → Γ !! x = Some A. +Proof. inversion 1; subst; auto. Qed. + +Lemma lam_inversion Γ (x: binder) e C: + Γ ⊢ (λ: x, e) : C → + ∃ A B y, C = (A → B)%ty ∧ x = BNamed y ∧ <[y:=A]> Γ ⊢ e : B. +Proof. inversion 1; subst; eauto 10. Qed. + +Lemma lit_int_inversion Γ (n: Z) A: Γ ⊢ n : A → A = Int. +Proof. inversion 1; subst; auto. 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. + + +Lemma syn_typed_closed Γ e A X : + Γ ⊢ e : A → + (∀ x, x ∈ dom Γ → x ∈ X) → + is_closed X e. +Proof. + 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. + } + (* everything else *) + all: repeat match goal with + | |- Is_true (_ && _) => apply andb_True; split + end. + all: naive_solver. +Qed. + +Lemma typed_weakening Γ Δ e A: + Γ ⊢ e : A → + Γ ⊆ Δ → + Δ ⊢ e : A. +Proof. + induction 1 as [| Γ x e A B Htyp IH | | | ] in Δ; intros Hsub; eauto. + - econstructor. by eapply lookup_weaken. + - econstructor. eapply IH. by eapply insert_mono. +Qed. + +(** Preservation of typing under substitution *) +Lemma typed_substitutivity e e' Γ x A B : + ∅ ⊢ e' : A → + <[x := A]> Γ ⊢ e : B → + Γ ⊢ subst x e' e : B. +Proof. + intros He'. revert B Γ; induction e as [y | y | | |]; intros B Γ; simpl. + - intros Hp%var_inversion; destruct decide; subst; eauto. + + rewrite lookup_insert in Hp. injection Hp as ->. + eapply typed_weakening; first done. apply map_empty_subseteq. + + rewrite lookup_insert_ne in Hp; last done. auto. + - intros (C & D & z & -> & -> & Hty)%lam_inversion. + econstructor. destruct decide as [|Heq]; simplify_eq. + + by rewrite insert_insert in Hty. + + rewrite insert_commute in Hty; last naive_solver. eauto. + - intros (C & Hty1 & Hty2)%app_inversion; eauto. + - intros ->%lit_int_inversion. eauto. + - intros (-> & Hty1 & Hty2)%plus_inversion; eauto. +Qed. + +(** Canonical value lemmas *) +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. +Proof. + inversion 1; simpl; naive_solver. +Qed. + + +(** Progress lemma *) +Lemma typed_progress e A: + ∅ ⊢ e : A → is_val e ∨ contextual_reducible e. +Proof. + remember ∅ as Γ. induction 1 as [| | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2]. + - subst. naive_solver. + - left. done. + - left. done. + - 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. eapply is_val_spec in H2 as [v Heq]. + replace e2 with (of_val v); last by eapply of_to_val. + destruct H1 as [e1' Hstep]. + eexists. eapply (fill_contextual_step (AppLCtx HoleCtx v)). done. + + right. destruct H2 as [e2' H2]. + eexists. eapply (fill_contextual_step (AppRCtx e1 HoleCtx)). done. + - 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. + eexists. eapply base_contextual_step. eapply PlusS; eauto. + + right. eapply is_val_spec in H2 as [v Heq]. + replace e2 with (of_val v); last by eapply of_to_val. + destruct H1 as [e1' Hstep]. + eexists. eapply (fill_contextual_step (PlusLCtx HoleCtx v)). done. + + right. destruct H2 as [e2' H2]. + eexists. eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)). done. +Qed. + +(** Contextual typing *) +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 [B [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. + +(** Base preservation *) +Lemma typed_preservation_base_step e e' A: + ∅ ⊢ e : A → + base_step e e' → + ∅ ⊢ e' : A. +Proof. + intros Hty Hstep. destruct Hstep as [| e1 e2 n1 n2 n3 Heq1 Heq2 Heval]; subst. + - eapply app_inversion in Hty as (B & Hty1 & Hty2). + eapply lam_inversion in Hty1 as (B' & A' & y & Heq1 & Heq2 & Hty). + simplify_eq. eapply typed_substitutivity; eauto. + - eapply plus_inversion in Hty as (-> & Hty1 & Hty2). + econstructor. +Qed. + +(** Preservation *) +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 typed_safety e1 e2 A: + ∅ ⊢ e1 : A → + rtc contextual_step e1 e2 → + is_val e2 ∨ contextual_reducible e2. +Proof. + induction 2; eauto using typed_progress, typed_preservation. +Qed. diff --git a/theories/type_systems/stlc/untyped.v b/theories/type_systems/stlc/untyped.v new file mode 100644 index 0000000..c38d85e --- /dev/null +++ b/theories/type_systems/stlc/untyped.v @@ -0,0 +1,221 @@ +From stdpp Require Import base relations tactics. +From iris Require Import prelude. +From semantics.lib Require Import sets maps. +From semantics.ts.stlc Require Import lang notation. + +(** The following two lemmas will be helpful in the sequel. + They just lift multiple reduction steps (via [rtc]) to application. + *) +Lemma steps_app_r (e1 e2 e2' : expr) : + rtc step e2 e2' → + rtc step (e1 e2) (e1 e2'). +Proof. + induction 1 as [ e | e e' e'' Hstep Hsteps IH]. + - reflexivity. + - eapply (rtc_l _ _ (e1 e')). + { by eapply StepAppR. } + done. +Qed. + +Lemma steps_app_l (e1 e1' e2 : expr) : + is_val e2 → + rtc step e1 e1' → + rtc step (e1 e2) (e1' e2). +Proof. + intros Hv. + induction 1 as [ e | e e' e'' Hstep Hsteps IH]. + - reflexivity. + - eapply (rtc_l _ _ (e' e2)). + { by eapply StepAppL. } + done. +Qed. + + +(** * Untyped λ calculus *) + +(** We do not re-define the language to remove primitive addition -- instead, we just + restrict our usage in this file to variables, application, and lambdas. + *) + + +Definition I_val : val := λ: "x", "x". +Definition F_val : val := λ: "x" "y", "x". +Definition S_val : val := λ: "x" "y", "y". +Definition ω : val := λ: "x", "x" "x". +Definition Ω : expr := ω ω. + + +(** Ω reduces to itself! *) +Lemma Omega_step : step Ω Ω. +Proof. + apply StepBeta. done. +Qed. + +(** ** Scott encodings *) + +Definition zero : val := λ: "x" "y", "x". + +Definition succ (n : val) : val := λ: "x" "y", "y" n. +(** [Succ] can be seen as a constructor: it takes [n] at the level of the language. *) +Definition Succ : val := λ: "n" "x" "y", "y" "n". + +Fixpoint enc_nat (n : nat) : val := + match n with + | 0 => zero + | S n => succ (enc_nat n) + end. + +Lemma enc_nat_closed n : + closed [] (enc_nat n). +Proof. + induction n as [ | n IH]. + - done. + - simpl. by apply closed_weaken_nil. +Qed. + +Lemma enc_0_red (z s : val) : + is_closed [] z → + rtc step (enc_nat 0 z s) z. +Proof. + intros Hcl. + eapply rtc_l. + { econstructor; first auto. econstructor. auto. } + simpl. eapply rtc_l. + { econstructor. auto. } + simpl. rewrite subst_closed_nil; done. +Qed. + +Lemma enc_S_red n (z s : val) : + rtc step (enc_nat (S n) z s) (s (enc_nat n)). +Proof. + simpl. eapply rtc_l. + { econstructor; first auto. econstructor. auto. } + simpl. eapply rtc_l. + { econstructor. auto. } + simpl. rewrite (subst_closed_nil (enc_nat n)); last apply enc_nat_closed. + rewrite subst_closed_nil; last apply enc_nat_closed. + reflexivity. +Qed. + +Lemma Succ_red n : step (Succ (enc_nat n)) (enc_nat (S n)). +Proof. econstructor. apply is_val_val. Qed. + +Lemma Succ_red_n n : rtc step (Nat.iter n Succ zero) (enc_nat n). +Proof. + induction n as [ | n IH]. + - reflexivity. + - simpl. + etrans. + { simpl. eapply steps_app_r. apply IH. } + eapply rtc_l. + { apply Succ_red. } + reflexivity. +Qed. + +(** ** Recursion *) +Definition Fix' : val := λ: "z" "y", "y" (λ: "x", "z" "z" "y" "x"). +Definition Fix (s : val) : val := λ: "x", Fix' Fix' s "x". +Arguments Fix : simpl never. + +Local Hint Immediate is_val_val : core. + +(** We prove that it satisfies the recursive unfolding *) +Lemma Fix_step (s r : val) : + is_closed [] s → + rtc step (Fix s r) (s ((Fix s))%E r). +Proof. + intros Hclosed. + eapply rtc_l. + { econstructor. auto. } + eapply rtc_l. + { simpl. econstructor; first by auto. + econstructor. { rewrite subst_closed_nil; auto. } + econstructor. done. + } + simpl. rewrite subst_closed_nil; last done. + eapply rtc_l. + { econstructor; first by auto. + econstructor. auto. + } + simpl. reflexivity. +Qed. + +(** Example usage: addition on Scott-encoded numbers *) +Definition add_step : val := λ: "r", λ: "n" "m", "n" "m" (λ: "p", Succ ("r" "p" "m")). +Definition add := Fix add_step. + +(** We are now going to prove it correct: + [add (enc_nat n) (enc_nat m)) ≻* (enc_nat (n + m))] + + First, we prove that it satisfies the expected defining equations for Peano addition. + *) + +Lemma add_step_0 m : rtc step (add (enc_nat 0) (enc_nat m)) (enc_nat m). +Proof. + (* use the unfolding equation of the fixpoint combinator *) + etrans. + { eapply steps_app_l; first by auto. + eapply Fix_step. done. + } + (* subst it into the [add_step] function *) + eapply rtc_l. + { econstructor; auto. econstructor; auto. econstructor. auto. } + simpl. + (* subst in the zero *) + eapply rtc_l. + { econstructor; auto. econstructor. done. } + simpl. + (* subst in the m *) + eapply rtc_l. + { econstructor; auto. } + simpl. + + (* do a step *) + etrans. + { apply (enc_0_red (enc_nat m) (λ: "p", Succ (Fix add_step "p" (enc_nat m)))). + apply enc_nat_closed. + } + reflexivity. +Qed. + +Lemma add_step_S n m : rtc step (add (enc_nat (S n)) (enc_nat m)) (Succ (add (enc_nat n) (enc_nat m))). +Proof. + (* use the unfolding equation of the fixpoint combinator *) + etrans. + { eapply steps_app_l; first by auto. + eapply Fix_step. done. + } + (* subst it into the [add_step] function *) + eapply rtc_l. + { econstructor; auto. econstructor; auto. econstructor. auto. } + simpl. + (* subst in the zero *) + eapply rtc_l. + { econstructor; auto. econstructor. done. } + simpl. + (* subst in the m *) + eapply rtc_l. + { econstructor; auto. } + simpl. + (* do a step *) + etrans. + { rewrite subst_closed_nil; last apply enc_nat_closed. + apply (enc_S_red n (enc_nat m) (λ: "p", Succ (Fix add_step "p" (enc_nat m)))). + } + + eapply rtc_l. + { econstructor. auto. } + simpl. + rewrite subst_closed_nil; last apply enc_nat_closed. + reflexivity. +Qed. + +Lemma add_correct n m : rtc step (add (enc_nat n) (enc_nat m)) (enc_nat (n + m)). +Proof. + induction n as [ | n IH]. + - apply add_step_0. + - etrans. { apply add_step_S. } + etrans. { apply steps_app_r. apply IH. } + eapply rtc_l. { apply Succ_red. } + reflexivity. +Qed. From 1f956e528e2a55fa9f7ce41502e40fe2408cca28 Mon Sep 17 00:00:00 2001 From: mueck Date: Thu, 2 Nov 2023 20:47:06 +0100 Subject: [PATCH 2/3] Release exercise 2.7 --- _CoqProject | 7 + theories/type_systems/stlc_extended/bigstep.v | 49 ++++ theories/type_systems/stlc_extended/ctxstep.v | 180 +++++++++++++ theories/type_systems/stlc_extended/lang.v | 175 ++++++++++++ .../type_systems/stlc_extended/notation.v | 56 ++++ theories/type_systems/stlc_extended/types.v | 255 ++++++++++++++++++ 6 files changed, 722 insertions(+) create mode 100644 theories/type_systems/stlc_extended/bigstep.v create mode 100644 theories/type_systems/stlc_extended/ctxstep.v create mode 100644 theories/type_systems/stlc_extended/lang.v create mode 100644 theories/type_systems/stlc_extended/notation.v create mode 100644 theories/type_systems/stlc_extended/types.v diff --git a/_CoqProject b/_CoqProject index 9328d94..2ef3baf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,6 +18,13 @@ theories/type_systems/stlc/notation.v theories/type_systems/stlc/untyped.v theories/type_systems/stlc/types.v +# Extended STLC +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/bigstep.v +theories/type_systems/stlc_extended/ctxstep.v + # By removing the # below, you can add the exercise sheets to make #theories/type_systems/warmup/warmup.v #theories/type_systems/warmup/warmup_sol.v diff --git a/theories/type_systems/stlc_extended/bigstep.v b/theories/type_systems/stlc_extended/bigstep.v new file mode 100644 index 0000000..eb5a78c --- /dev/null +++ b/theories/type_systems/stlc_extended/bigstep.v @@ -0,0 +1,49 @@ +From stdpp Require Import gmap base relations. +From iris Require Import prelude. +From semantics.ts.stlc_extended Require Import lang notation types. + +(** * Big-step semantics *) + +Implicit Types + (Γ : typing_context) + (v : val) + (e : expr) + (A : type). + +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 + +(* TODO : extend the big-step semantics *) + . +#[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. + +(* TODO : this should be fixed once you have added the right semantics *) +Admitted. + + +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.v b/theories/type_systems/stlc_extended/ctxstep.v new file mode 100644 index 0000000..f2bef44 --- /dev/null +++ b/theories/type_systems/stlc_extended/ctxstep.v @@ -0,0 +1,180 @@ +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) + (* TODO: extend the definition *) +. + +#[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) + (* TODO: extend the definition *) +. + +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) + (* TODO: extend the definition *) + 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') + (* TODO: extend the definition *) + 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. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_pair_r e1 e2 e2': + contextual_step e2 e2' → + contextual_step (Pair e1 e2) (Pair e1 e2'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_fst e e': + contextual_step e e' → + contextual_step (Fst e) (Fst e'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_snd e e': + contextual_step e e' → + contextual_step (Snd e) (Snd e'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_injl e e': + contextual_step e e' → + contextual_step (InjL e) (InjL e'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_injr e e': + contextual_step e e' → + contextual_step (InjR e) (InjR e'). +Proof. + (* TODO: exercise *) +Admitted. + + +Lemma contextual_step_case e e' e1 e2: + contextual_step e e' → + contextual_step (Case e e1 e2) (Case e' e1 e2). +Proof. + (* TODO: exercise *) +Admitted. + + +#[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/lang.v b/theories/type_systems/stlc_extended/lang.v new file mode 100644 index 0000000..1f82aef --- /dev/null +++ b/theories/type_systems/stlc_extended/lang.v @@ -0,0 +1,175 @@ +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. + +Inductive expr := + (* Base lambda calculus *) + | Var (x : string) + | Lam (x : binder) (e : expr) + | App (e1 e2 : expr) + (* Base types and their operations *) + | LitInt (n: Z) + | Plus (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 := + | LitIntV (n: Z) + | LamV (x : binder) (e : expr) + | 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 + | LitIntV n => LitInt n + | LamV x e => Lam x e + | 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 + | LitInt n => Some $ LitIntV n + | Lam x e => Some (LamV x e) + | 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 + | LitInt l => True + | Lam x e => True + | 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 | | 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 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. + +(** Substitution *) +Fixpoint subst (x : string) (es : expr) (e : expr) : expr := + match e with + | LitInt _ => 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) + | Plus e1 e2 => Plus (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. + +(** Closed terms **) + +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 + | LitInt _ => true + | Fst e | Snd e | InjL e | InjR e => is_closed X e + | App e1 e2 | Plus e1 e2 | Pair e1 e2 => is_closed X e1 && is_closed X 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. diff --git a/theories/type_systems/stlc_extended/notation.v b/theories/type_systems/stlc_extended/notation.v new file mode 100644 index 0000000..4499df2 --- /dev/null +++ b/theories/type_systems/stlc_extended/notation.v @@ -0,0 +1,56 @@ +From semantics.ts.stlc_extended Require Export lang. +Set Default Proof Using "Type". + + +(** Coercions to make programs easier to type. *) +Coercion of_val : val >-> expr. +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" := (LitIntV l%Z%V%stdpp) (at level 8, format "# l"). +Notation "# l" := (LitInt 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 "e1 + e2" := (Plus e1%E e2%E) : expr_scope. + +(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : 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. diff --git a/theories/type_systems/stlc_extended/types.v b/theories/type_systems/stlc_extended/types.v new file mode 100644 index 0000000..51317d5 --- /dev/null +++ b/theories/type_systems/stlc_extended/types.v @@ -0,0 +1,255 @@ +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. + +(** ** 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 + (* TODO: provide the new typing rules *) +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. + +(* TODO: add inversion lemmas for the new typing rules. + They will be very useful for the proofs below! +*) + + +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. + - (* TODO *) admit. + - (* TODO *) admit. + - (* TODO *) admit. + - (* TODO *) admit. + - (* TODO *) admit. + - (* TODO *) admit. +Admitted. + +(** 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. + +(* TODO: add canonical forms lemmas for the new types *) + +(** 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]. + - 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. + +(* FIXME: prove the new cases *) +Admitted. + +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. + +(* TODO: extend this for the new cases *) +Admitted. + +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. From 9f77d69dcfcf4a36a400044ebd268a7d8d48e923 Mon Sep 17 00:00:00 2001 From: mueck Date: Thu, 2 Nov 2023 20:54:02 +0100 Subject: [PATCH 3/3] Minor improvement --- theories/type_systems/stlc_extended/bigstep.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/theories/type_systems/stlc_extended/bigstep.v b/theories/type_systems/stlc_extended/bigstep.v index eb5a78c..372f3d4 100644 --- a/theories/type_systems/stlc_extended/bigstep.v +++ b/theories/type_systems/stlc_extended/bigstep.v @@ -1,14 +1,12 @@ From stdpp Require Import gmap base relations. From iris Require Import prelude. -From semantics.ts.stlc_extended Require Import lang notation types. +From semantics.ts.stlc_extended Require Import lang notation. (** * Big-step semantics *) Implicit Types - (Γ : typing_context) (v : val) - (e : expr) - (A : type). + (e : expr). Inductive big_step : expr → val → Prop := | bs_lit (n : Z) :