From ef2a8c2b755d9c5a7a0d711ad94539c46c819f25 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Tue, 14 Nov 2023 12:29:56 +0100
Subject: [PATCH] Answer question 3.1

---
 theories/type_systems/systemf/exercises03.v | 25 +++++++++++++++------
 1 file changed, 18 insertions(+), 7 deletions(-)

diff --git a/theories/type_systems/systemf/exercises03.v b/theories/type_systems/systemf/exercises03.v
index 13725fb..1afcd45 100644
--- a/theories/type_systems/systemf/exercises03.v
+++ b/theories/type_systems/systemf/exercises03.v
@@ -2,6 +2,19 @@ From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.ts.systemf Require Import lang notation types tactics.
 
+(*
+  Exercise 3.1:
+  With V[A->B] = {v | ∀v', v' ∈ V[A] -> v v' ∈ E[B]}
+  The set V[A->B] is equal to:
+  V[A->B] = {v | ∀v', v' ∈ V[A], ∃w, v v' | w, w ∈ V[B]}
+  According to big step semantics, `v v' | w` inverts to `v | λx.e` and `e[v'/x] | w`.
+  Assuming that `v` and `v'` are closed, we have `e[v'/x]` closed, and thus `e[v'/x] ∈ E[B]`.
+  Since `v` is a value and `v | λx.e`, we have `v = λx.e`.
+
+  We thus have `{v | ∀v', v' ∈ V[A] -> v v' ∈ E[B]} = {λx.e | ∀v', v' ∈ V[A] -> e[v'/x] ∈ E[B]}`,
+  after which we can carry out our proof as before.
+*)
+
 (** Exercise 3 (LN Exercise 22): Universal Fun *)
 
 Definition fun_comp : val :=
@@ -10,7 +23,7 @@ Definition fun_comp_type : type :=
   #0 (* TODO *).
 Lemma fun_comp_typed :
   TY 0; ∅ ⊢ fun_comp : fun_comp_type.
-Proof. 
+Proof.
   (* should be solved by solve_typing. *)
   (* TODO: exercise *)
 Admitted.
@@ -22,7 +35,7 @@ Definition swap_args_type : type :=
   #0 (* TODO *).
 Lemma swap_args_typed :
   TY 0; ∅ ⊢ swap_args : swap_args_type.
-Proof. 
+Proof.
   (* should be solved by solve_typing. *)
   (* TODO: exercise *)
 Admitted.
@@ -34,7 +47,7 @@ Definition lift_prod_type : type :=
   #0 (* TODO *).
 Lemma lift_prod_typed :
   TY 0; ∅ ⊢ lift_prod : lift_prod_type.
-Proof. 
+Proof.
   (* should be solved by solve_typing. *)
   (* TODO: exercise *)
 Admitted.
@@ -46,7 +59,7 @@ Definition lift_sum_type : type :=
   #0 (* TODO *).
 Lemma lift_sum_typed :
   TY 0; ∅ ⊢ lift_sum : lift_sum_type.
-Proof. 
+Proof.
   (* should be solved by solve_typing. *)
   (* TODO: exercise *)
 Admitted.
@@ -74,7 +87,7 @@ Notation "∃:  x , τ" :=
     (at level 100, τ at level 200) : PType_scope.
 
 Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type :=
-  None (* FIXME *). 
+  None (* FIXME *).
 
 (* Example *)
 Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
@@ -96,5 +109,3 @@ Proof.
   (* Should be solved by reflexivity. *)
   (* TODO: exercise *)
 Admitted.
-
-