✨ De Bruijn substitution of expressions, church encoding of sums and lists

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 :