From c2ce491075d6532099244c8ab4c336fd35350af9 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Tue, 21 Nov 2023 14:53:18 +0100 Subject: [PATCH] :sparkles: De Bruijn substitution of expressions, church encoding of sums and lists --- theories/type_systems/systemf/exercises04.v | 197 ++++++++++++++------ 1 file changed, 142 insertions(+), 55 deletions(-) diff --git a/theories/type_systems/systemf/exercises04.v b/theories/type_systems/systemf/exercises04.v index b0a5a06..96db977 100644 --- a/theories/type_systems/systemf/exercises04.v +++ b/theories/type_systems/systemf/exercises04.v @@ -23,16 +23,36 @@ Module dbterm. (n x : nat) (e : expr). + (* + Renames the free variable indices according to δ. + For instance, if δ = Nat.succ, all the variable indices will be incremented, + leaving room to prepend a new variable on the "context stack". + *) + Fixpoint ren (δ: ren_t) (e: expr): expr := + match e with + | Lit l => Lit l + | Var i => Var (δ i) + | Lam e => Lam (ren δ e) + | Plus e1 e2 => Plus (ren δ e1) (ren δ e2) + | App e1 e2 => App (ren δ e1) (ren δ e2) + end. + + (* Applies `ren δ e` to all elements in `σ` *) + Definition subst_ren (δ: ren_t) (σ: sub_t): sub_t := (ren δ) ∘ σ. + + Definition subst_inc (σ: sub_t): sub_t := λ n, match n with + | 0 => Var 0 + (* Note: calling σ is not enough, as all the free variables in it need to be incremented. *) + | S n => (subst_ren Nat.succ σ) n + end. + Fixpoint subst σ e := match e with | Lit l => Lit l | Var i => σ i - | Lam e => Lam (subst (λ n, match n with - | 0 => Var 0 - | S n => σ n - )) - | Plus e1 e2 => Plus (subst σ a) (subst σ b) - | App e_fn e_arg => + | Lam e => Lam (subst (subst_inc σ) e) + | Plus e1 e2 => Plus (subst σ e1) (subst σ e2) + | App e_fn e_arg => App (subst σ e_fn) (subst σ e_arg) end. @@ -47,28 +67,35 @@ Module dbterm. Lam (Plus (Plus (Var 1) (Lit 42%Z)) (Var 0)). Proof. cbn. - (* Should be by reflexivity. *) - (* TODO: exercise *) - Admitted. - - + reflexivity. + Qed. End dbterm. Section church_encodings. (** Exercise 2 (LN Exercise 24): Church encoding, sum types *) (* a) Define your encoding *) - Definition sum_type (A B : type) : type := #0 (* FIXME *). + + (* ∀α, ∀β, ∀γ, (α → γ) → (β → γ) → γ *) + (* Note: we have to increment the types A and B, as we are wrapping them *) + Definition sum_type (A B : type) : type := (∀: (A.[ren (+1)] → #0) → (B.[ren (+1)] → #0) → #0). (* b) Implement inj1, inj2, case *) - Definition injl_val (v : val) : val := #0 (* FIXME *). - Definition injl_expr (e : expr) : expr := #0 (* FIXME *). - Definition injr_val (v : val) : val := #0 (* FIXME *). - Definition injr_expr (e : expr) : expr := #0 (* FIXME *). + Definition injl_val (v : val) : val := (Λ, λ: "f_l" "f_r", "f_l" v). + Definition injl_expr (e : expr) : expr := ((λ: "v", Λ, (λ: "f_l" "f_r", "f_l" "v")) e). + Definition injr_val (v : val) : val := (Λ, λ: "f_l" "f_r", "f_r" v). + Definition injr_expr (e : expr) : expr := ((λ: "v", Λ, (λ: "f_l" "f_r", "f_r" "v")) e). (* You may want to use the variables x1, x2 for the match arms to fit the typing statements below. *) - Definition match_expr (e : expr) (e1 e2 : expr) : expr := #0. (* FIXME *) + Definition match_expr (e : expr) (e1 e2 : expr) : expr := + e<> (λ: "x1", e1)%E (λ: "x2", e2)%E + . + Lemma is_closed_lam {X: list string} {e: expr} {name: string} (Hcl: is_closed (List.cons name X) e) : is_closed X (λ: name, e). + Proof. + simpl. + assumption. + Qed. (* c) Reduction behavior *) (* Some lemmas about substitutions might be useful. Look near the end of the lang.v file! *) @@ -79,9 +106,25 @@ Section church_encodings. big_step (subst' "x1" vl e1) v' → big_step (match_expr e e1 e2) v'. Proof. - (* TODO: exercise *) - Admitted. - + intros Hcl1 Hcl2 Hbs_v Hbs_e1. + econstructor; [ | by apply bs_lam | ]. + (* First application *) + { + eapply bs_app; [eapply bs_tapp; first exact Hbs_v; last by apply bs_lam | by apply bs_lam | ]. + simpl; rewrite (subst_is_closed_nil _ _ _ Hcl1). + by apply bs_lam. + } + (* Second application *) + { + simpl. + eapply bs_app; [by apply bs_lam | | ]. + rewrite (subst_is_closed_nil _ _ _ Hcl1). + apply big_step_of_val; reflexivity. + + erewrite (lang.subst_is_closed ["x1"] _ "f_r"); [ | exact Hcl2 | set_solver]. + exact Hbs_e1. + } + Qed. Lemma match_expr_red_injr e e1 e2 (vl v' : val) : is_closed [] vl → @@ -90,8 +133,7 @@ Section church_encodings. big_step (match_expr e e1 e2) v'. Proof. intros. bs_step_det. - (* TODO: exercise *) - Admitted. + Qed. Lemma injr_expr_red e v : @@ -99,8 +141,7 @@ Section church_encodings. big_step (injr_expr e) (injr_val v). Proof. intros. bs_step_det. - (* TODO: exercise *) - Admitted. + Qed. Lemma injl_expr_red e v : @@ -108,10 +149,7 @@ Section church_encodings. big_step (injl_expr e) (injl_val v). Proof. intros. bs_step_det. - (* TODO: exercise *) - Admitted. - - + Qed. (* d) Typing rules *) Lemma sum_injl_typed n Γ (e : expr) A B : @@ -120,11 +158,12 @@ Section church_encodings. TY n; Γ ⊢ e : A → TY n; Γ ⊢ injl_expr e : sum_type A B. Proof. - intros. solve_typing. - (* TODO: exercise *) - Admitted. + intros. + solve_typing. + Qed. + (* TODO: write paper proof *) Lemma sum_injr_typed n Γ e A B : type_wf n B → type_wf n A → @@ -132,8 +171,7 @@ Section church_encodings. TY n; Γ ⊢ injr_expr e : sum_type A B. Proof. intros. solve_typing. - (* TODO: exercise *) - Admitted. + Qed. Lemma sum_match_typed n Γ A B C e e1 e2 : @@ -146,21 +184,40 @@ Section church_encodings. TY n; Γ ⊢ match_expr e e1 e2 : C. Proof. intros. solve_typing. - (* TODO: exercise *) - Admitted. - + Qed. (** Exercise 3 (LN Exercise 25): church encoding, list types *) (* a) translate the type of lists into De Bruijn. *) - Definition list_type (A : type) : type := #0 (* FIXME *). + (* A match on a list looks like: + ``` + match list with + | [] => e_empty + | cons head rest => e_head + ``` + + At first glance, our list type should look something like under scott encoding: + ∀α, (α → (A → self → α) → α) + + We can't have self-referential types, + and since we only care to return α, we can type it as + ∀α, (α → (A → α → α) → α) + + This process is well-described in: + https://jnkr.tech/blog/church-scott-encodings-of-adts + *) + + Definition list_type (A : type) : type := (∀: #0 → (A.[ren (+1)] → #0 → #0) → #0). (* b) Implement nil and cons. *) - Definition nil_val : val := #0 (* FIXME *). - Definition cons_val (v1 v2 : val) : val := #0 (* FIXME *). - Definition cons_expr (e1 e2 : expr) : expr := #0 (* FIXME *). + Definition nil_val : val := (Λ, λ: "nil" "cons", "nil"). + (* For cons_val, we want to call cons (of type A → α → α) with as first argument v1 (the head), then with as second argument v2, called recursively *) + Definition cons_val (v1 v2 : val) : val := (Λ, λ: "nil" "cons", "cons" v1 (v2<> "nil" "cons")). + Definition cons_expr (e1 e2 : expr) : expr := ((λ: "x1" "x2", ( + Λ, λ: "nil" "cons", "cons" "x1" ("x2"<> "nil" "cons") + )) e1 e2). (* c) Define typing rules and prove them *) Lemma nil_typed n Γ A : @@ -168,8 +225,7 @@ Section church_encodings. TY n; Γ ⊢ nil_val : list_type A. Proof. intros. solve_typing. - (* TODO: exercise *) - Admitted. + Qed. Lemma cons_typed n Γ (e1 e2 : expr) A : @@ -178,13 +234,17 @@ Section church_encodings. TY n; Γ ⊢ e1 : A → TY n; Γ ⊢ cons_expr e1 e2 : list_type A. Proof. - intros. repeat solve_typing. - (* TODO: exercise *) - Admitted. + intros. + repeat solve_typing. + Qed. + (* d) Define a function head of type list A → A + 1 *) - Definition head : val := #0 (* FIXME *). + Definition head : val := (λ: "list", "list"<> + (InjRV (LitV LitUnit)) + (λ: "head" "rec", (InjL "head")) + ). Lemma head_typed n Γ A : @@ -192,13 +252,44 @@ Section church_encodings. TY n; Γ ⊢ head: (list_type A → (A + Unit)). Proof. intros. solve_typing. - (* TODO: exercise *) - Admitted. + Qed. (* e) Define a function [tail] of type list A → list A *) - - Definition tail : val := #0 (* FIXME *). + (* + This one's a tricky: + ``` + cons x rest = \nil \rec, rec x (rest nil rec) + ``` + Somehow, our `rec` function must be able to tell when it's being called first, + and return the second argument, and when it's called the other times, where it should return `cons head rest`. + + An alternative is to return a function inside of `rec`. + The `nil` case is easy, as it becomes `thunk nil`. + + Let `rec` return a function that matches its parameter to know if it is called recursively (by `rec`), or not. + + ``` + tail_helper head rec_value = \is_first. match is_first with + | true => rec_value false + | false => cons head (rec_value false) + end + -- aka: + tail_helper head rec_value = \is_first. is_first (rec_value false_val) (cons head (rec_value false_val)) + + tail = \list, list (\_, nil) (\head \rec_value, tail_helper head rec_value) + ``` + *) + Definition true_val : val := (λ: "t" "f", "t"). + Definition false_val : val := (λ: "t" "f", "f"). + + Definition tail_helper (head rec_value : expr) : val := (λ: "is_first", + "is_first" (rec_value false_val) (cons_expr head (rec_value false_val))). + Definition tail : val := ((λ: "list", "list"<> + (λ: BAnon, nil_val) + (λ: "head" "rec_value", tail_helper "head" "rec_value") + true_val + )). Lemma tail_typed n Γ A : @@ -206,14 +297,10 @@ Section church_encodings. TY n; Γ ⊢ tail: (list_type A → list_type A). Proof. intros. repeat solve_typing. - (* TODO: exercise *) - Admitted. - - + Qed. End church_encodings. Section free_theorems. - (** Exercise 4 (LN Exercise 27): Free Theorems I *) (* a) State a free theorem for the type ∀ α, β. α → β → α × β *) Lemma free_thm_1 :