Answer question 3.1

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 :=
@@ -96,5 +109,3 @@ Proof.
   (* Should be solved by reflexivity. *)
   (* TODO: exercise *)
 Admitted.
-
-