Merge remote-tracking branch 'origin/amethyst' into amethyst

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 :=
@@ -15,6 +28,7 @@ Proof.
 Qed.
 
 
+
 Definition swap_args : val :=
   Λ, Λ, Λ, (λ: "f", (λ: "x" "y", "f" "y" "x")).
 Definition swap_args_type : type :=
@@ -26,6 +40,7 @@ Proof.
 Qed.
 
 
+
 Definition lift_prod : val :=
   Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "pair",
     (Pair ("f" (Fst "pair")) ("g" (Snd "pair")))
@@ -50,6 +65,7 @@ Definition lift_sum_type : type :=
   (∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 + #2) → (#1 + #3))).
 Lemma lift_sum_typed :
   TY 0; ∅ ⊢ lift_sum : lift_sum_type.
+
 Proof.
   solve_typing.
 Qed.