From 3be5b55caedfcaa9ea329fe5457495201a09a37f Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Tue, 21 Nov 2023 12:03:17 +0100
Subject: [PATCH] Start working on exercise sheet 4

---
 theories/type_systems/systemf/exercises04.v | 37 +++++++++++++--------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/theories/type_systems/systemf/exercises04.v b/theories/type_systems/systemf/exercises04.v
index df39922..b0a5a06 100644
--- a/theories/type_systems/systemf/exercises04.v
+++ b/theories/type_systems/systemf/exercises04.v
@@ -14,19 +14,28 @@ Module dbterm.
   .
 
   (** Formalize substitutions and renamings as functions. *)
-  Definition subt := nat → expr.
-  Definition rent := nat → nat.
+  Definition sub_t := nat → expr.
+  Definition ren_t := nat → nat.
 
   Implicit Types
-    (σ : subt)
-    (δ : rent)
+    (σ : sub_t)
+    (δ : ren_t)
     (n x : nat)
     (e : expr).
 
   Fixpoint subst σ e :=
-    (* FIXME *) 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 =>
+    end.
+
 
-  
 
   Goal (subst
     (λ n, match n with
@@ -34,10 +43,10 @@ Module dbterm.
           | 1 => Var 0
           | _ => Var n
           end)
-    (Lam (Plus (Plus (Var 2) (Var 1)) (Var 0)))) = 
+    (Lam (Plus (Plus (Var 2) (Var 1)) (Var 0)))) =
     Lam (Plus (Plus (Var 1) (Lit 42%Z)) (Var 0)).
   Proof.
-    cbn. 
+    cbn.
     (* Should be by reflexivity. *)
     (* TODO: exercise *)
   Admitted.
@@ -49,7 +58,7 @@ 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 *).
-    
+
 
   (* b) Implement inj1, inj2, case *)
   Definition injl_val (v : val) : val := #0 (* FIXME *).
@@ -59,7 +68,7 @@ Section church_encodings.
 
   (* 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 *)
-    
+
 
   (* c) Reduction behavior *)
   (* Some lemmas about substitutions might be useful. Look near the end of the lang.v file! *)
@@ -146,7 +155,7 @@ Section church_encodings.
 
   (* a) translate the type of lists into De Bruijn. *)
   Definition list_type (A : type) : type := #0 (* FIXME *).
-    
+
 
   (* b) Implement nil and cons. *)
   Definition nil_val : val := #0 (* FIXME *).
@@ -176,7 +185,7 @@ Section church_encodings.
 
   (* d) Define a function head of type list A → A + 1 *)
   Definition head : val := #0 (* FIXME *).
-    
+
 
   Lemma head_typed n Γ A :
     type_wf n A →
@@ -188,9 +197,9 @@ Section church_encodings.
 
 
   (* e) Define a function [tail] of type list A → list A *)
-  
+
   Definition tail : val := #0 (* FIXME *).
-    
+
 
   Lemma tail_typed n Γ A :
     type_wf n A →