From ae6e26733ceb0ecb0b314fcbe1ba7e46a90140e5 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Fri, 17 Nov 2023 15:48:08 +0100
Subject: [PATCH] :sparkles: Finish exercise sheet 3

---
 theories/type_systems/stlc/cbn_logrel.v     | 249 +++++++++++++++++++-
 theories/type_systems/systemf/exercises03.v | 127 +++++++---
 2 files changed, 335 insertions(+), 41 deletions(-)

diff --git a/theories/type_systems/stlc/cbn_logrel.v b/theories/type_systems/stlc/cbn_logrel.v
index a087a6f..656e7d0 100644
--- a/theories/type_systems/stlc/cbn_logrel.v
+++ b/theories/type_systems/stlc/cbn_logrel.v
@@ -143,12 +143,13 @@ Proof.
   - intros y e'. rewrite lookup_insert_Some.
     intros [[-> <-]|[Hne Hlook]].
     + by eapply expr_rel_closed.
-    + eapply IHsem_context_rel; last done.
+    + eapply IHsem_context_rel.
+      exact Hlook.
 Qed.
 
 
 (* This is essentially an inversion lemma for 𝒢 *)
-Lemma sem_context_rel_exprs Γ θ x A :
+Lemma sem_context_rel_exprs {Γ θ x A} :
   sem_context_rel Γ θ →
   Γ !! x = Some A →
   ∃ e, θ !! x = Some e ∧ ℰ A e.
@@ -170,15 +171,249 @@ Proof.
   - rewrite !dom_insert. congruence.
 Qed.
 
+Ltac specialize_all' θ H_ctx := repeat (
+  match goal with
+  | [ H: ∀ θ, ∀ (_: sem_context_rel ?G θ), ?e |- ?goal ] =>
+    specialize (H θ H_ctx)
+  | [ H: ?G ⊨ ?e : ?T |- ?goal ] =>
+    destruct H as [? H];
+    specialize (H θ H_ctx)
+  end
+).
+
+Ltac specialize_all_closed := repeat (
+  match goal with
+  | [ H: ?G ⊨ ?e : ?T |- ?goal ] =>
+    destruct H as [H _]
+  end
+).
+
+Ltac specialize_all θ H_ctx :=
+  match goal with
+  | [ |- ∀ θ, ∀ (_: sem_context_rel ?G θ), ?e ] => intros θ H_ctx; specialize_all' θ H_ctx
+  | [ |- ?G ⊨ ?e : ?T ] => econstructor; first (specialize_all_closed); last (intros θ H_ctx; specialize_all' θ H_ctx)
+  end.
+
+Ltac break_expr_rel H val Hcl Hval :=
+  simp type_interp in H;
+  destruct H as (val & H & Hcl & Hval).
+
+Ltac split3 := split; last split.
+
+(* Search (?A !! ?B = Some ?C) (?B ∈ ?D). *)
+(* Search (?x ∈ elements ?y). *)
+
+Lemma compat_var Γ x A:
+  Γ !! x = Some A →
+  Γ ⊨ (Var x): A.
+Proof.
+  intro H_some.
+  split.
+  - simpl.
+    apply bool_decide_pack.
+    rewrite elem_of_elements.
+    exact (elem_of_dom_2 Γ x A H_some).
+  - specialize_all θ H_ctx.
+    destruct (sem_context_rel_exprs H_ctx H_some) as (e & Hθ_some & He).
+    simpl.
+    rewrite Hθ_some.
+    exact He.
+Qed.
 
+Search (elem_of ?x (cons ?x ?y)).
+
+(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *)
+Lemma lam_closed Γ θ (x : string) A e :
+  closed (elements (dom (<[x:=A]> Γ))) e →
+  𝒢 Γ θ →
+  closed [] (Lam x (subst_map (delete x θ) e)).
+Proof.
+  intros Hcl Hctxt.
+  eapply subst_map_closed'_2.
+  - eapply closed_weaken; first done.
+    rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //.
+    (* The [set_solver] tactic is great for solving goals involving set
+    inclusion and union. However, when set difference is involved, it can't
+    always solve the goal -- we need to help it by doing a case distinction on
+    whether the element we are considering is [x] or not. *)
+    intros y. destruct (decide (x = y)); set_solver.
+  - eapply subst_closed_weaken, sem_context_rel_closed; last done.
+    + set_solver.
+    + apply map_delete_subseteq.
+Qed.
+
+Lemma lam_closed' {Γ θ x A e}:
+  closed (elements (dom (<[x:=A]> Γ))) e →
+  𝒢 Γ θ →
+  closed [x] (subst_map (delete x θ) e).
+Proof.
+  intros Hcl H_ctx.
+  eapply closed_subst_weaken.
+  eapply subst_closed_weaken; first reflexivity.
+  by apply map_delete_subseteq.
+  exact (sem_context_rel_closed _ _ H_ctx).
+  2: exact Hcl.
+
+  rewrite dom_insert.
+  intros y Hy_in Hy_notin.
+
+  rewrite (sem_context_rel_dom _ _ H_ctx) in Hy_in.
+  rewrite dom_delete in Hy_notin.
+  rewrite not_elem_of_difference in Hy_notin.
+  rewrite elem_of_elements in Hy_in.
+  set_solver.
+Qed.
+the internship
+Lemma compat_lam Γ x e A B:
+  (<[x:=A]> Γ ⊢ e : B)%ty →
+  <[x:=A]> Γ ⊨ e : B →
+  Γ ⊨ (λ: (BNamed x), e) : (A → B).
+Proof.
+  intros He_ty IHe.
+
+  specialize_all θ H_ctx.
+  - simpl.
+    rename IHe into IHcl.
+    eapply closed_weaken.
+    exact IHcl.
+
+    rewrite dom_insert.
+
+    induction (decide (x ∈ (dom Γ))) as [Hin | Hnotin]; set_solver.
+  - destruct IHe as [Hcl IHe].
+
+    simp type_interp.
+    eexists.
+    simpl; split3.
+    {
+      constructor.
+    }
+    {
+      by eapply lam_closed.
+    }
+
+    simp type_interp.
+    exists x.
+    eexists.
+    simpl; split3.
+    {
+      reflexivity.
+    }
+    {
+      by eapply lam_closed'.
+    }
+    intros e_arg He_arg.
+
+    rewrite subst_subst_map.
+    {
+      eapply IHe.
+      econstructor.
+      assumption.
+      assumption.
+    }
+    {
+      exact (sem_context_rel_closed _ _ H_ctx).
+    }
+Qed.
+
+Lemma compat_int Γ z:
+  Γ ⊨ LitInt z : Int.
+Proof.
+  econstructor.
+  1: eauto.
+  simpl; intros; simp type_interp.
+  exists z.
+  split; last split; eauto.
+  simp type_interp.
+  exists z; reflexivity.
+Qed.
+
+Lemma compat_plus Γ e1 e2:
+  Γ ⊨ e1 : Int →
+  Γ ⊨ e2 : Int →
+  Γ ⊨ (e1 + e2) : Int.
+Proof.
+  intros H1 H2.
+  destruct H1 as [Hcl1 He1].
+  destruct H2 as [Hcl2 He2].
+  econstructor.
+  1: naive_solver.
+  specialize_all θ H_ctx.
+  break_expr_rel He1 v1 Hcl1' Hv1.
+  break_expr_rel He2 v2 Hcl2' Hv2.
+  simp type_interp in Hv1; destruct Hv1 as [z1 ->].
+  simp type_interp in Hv2; destruct Hv2 as [z2 ->].
+
+  simpl.
+  simp type_interp.
+  exists (z1 + z2)%Z.
+  split3.
+  - econstructor; assumption.
+  - naive_solver.
+  - simp type_interp.
+    eauto.
+Qed.
+
+Lemma compat_app Γ e1 e2 A B:
+  Γ ⊨ e1 : (A → B) →
+  Γ ⊨ e2 : A →
+  Γ ⊨ App e1 e2 : B.
+Proof.
+  intros Hsem_fn Hsem_e2.
+
+  specialize_all θ H_ctx.
+  - simpl; rewrite andb_True; split; assumption.
+  - simpl.
+    simp type_interp; simpl; eauto.
+    break_expr_rel Hsem_fn v_fn Hcl_fn Hv_fn.
+    break_expr_rel Hsem_e2 v_e2 Hcl_e2 Hv_e2.
+    simp type_interp in Hv_fn.
+    simpl in Hv_fn; destruct Hv_fn as (x & e_body & -> & Hcl_e & IHe_subst).
+
+    assert (ℰ A (subst_map θ e2)) as Hsem_subst.
+    {
+      simp type_interp.
+      eauto.
+    }
+    specialize (IHe_subst (subst_map θ e2) Hsem_subst).
+    break_expr_rel IHe_subst v_target Hcl_target Hv_target.
+
+    exists v_target; split3.
+    {
+      econstructor.
+      exact v_target.
+      exact Hsem_fn.
+      exact IHe_subst.
+    }
+    apply andb_True; split; eauto.
+    assumption.
+Qed.
+
+Lemma sem_soundness {Γ e A}:
+  (Γ ⊢ e: A)%ty →
+  Γ ⊨ e: A.
+Proof.
+  induction 1.
+  - by apply compat_var.
+  - by apply compat_lam.
+  - by apply compat_int.
+  - by eapply compat_app.
+  - by apply compat_plus.
+Qed.
 
 
 Lemma termination e A :
   (∅ ⊢ e : A)%ty →
   ∃ v, big_step e v.
 Proof.
-  (* You may want to add suitable intermediate lemmas, like we did for the cbv
-     logical relation as seen in the lecture. *)
-  (* TODO: exercise *)
-Admitted.
-
+  intro H_step.
+  remember (sem_soundness H_step) as H_sem.
+  destruct H_sem as [H_closed H_e].
+  clear HeqH_sem.
+  specialize (H_e ∅ sem_context_rel_empty).
+  simp type_interp in H_e.
+  destruct H_e as (target & Hbs_subst & _ & _).
+  exists target.
+  rewrite subst_map_empty in Hbs_subst.
+  assumption.
+Qed.
diff --git a/theories/type_systems/systemf/exercises03.v b/theories/type_systems/systemf/exercises03.v
index 13725fb..b040ee7 100644
--- a/theories/type_systems/systemf/exercises03.v
+++ b/theories/type_systems/systemf/exercises03.v
@@ -5,51 +5,54 @@ From semantics.ts.systemf Require Import lang notation types tactics.
 (** Exercise 3 (LN Exercise 22): Universal Fun *)
 
 Definition fun_comp : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, (λ: "f" "g" "x", "g" ("f" "x")).
 Definition fun_comp_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: (#0 → #1) → (#1 → #2) → (#0 → #2)).
 Lemma fun_comp_typed :
   TY 0; ∅ ⊢ fun_comp : fun_comp_type.
-Proof. 
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+Proof.
+  solve_typing.
+Qed.
 
 
 Definition swap_args : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, (λ: "f", (λ: "x" "y", "f" "y" "x")).
 Definition swap_args_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: (#0 → #1 → #2) → (#1 → #0 → #2)).
 Lemma swap_args_typed :
   TY 0; ∅ ⊢ swap_args : swap_args_type.
-Proof. 
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+Proof.
+  solve_typing.
+Qed.
 
 
 Definition lift_prod : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "pair",
+    (Pair ("f" (Fst "pair")) ("g" (Snd "pair")))
+  )).
 Definition lift_prod_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 × #2) → (#1 × #3))).
 Lemma lift_prod_typed :
   TY 0; ∅ ⊢ lift_prod : lift_prod_type.
-Proof. 
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+Proof.
+  solve_typing.
+Qed.
 
 
 Definition lift_sum : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "inj",
+    (match: "inj" with
+      InjL "x" => (InjL ("f" "x"))
+      | InjR "x" => (InjR ("g" "x"))
+    end)
+  )).
 Definition lift_sum_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 + #2) → (#1 + #3))).
 Lemma lift_sum_typed :
   TY 0; ∅ ⊢ lift_sum : lift_sum_type.
-Proof. 
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+Proof.
+  solve_typing.
+Qed.
 
 
 (** Exercise 5 (LN Exercise 18): Named to De Bruijn *)
@@ -73,28 +76,84 @@ Notation "∃:  x , τ" :=
     (PTExists x τ%pty)
     (at level 100, τ at level 200) : PType_scope.
 
+(*
+De Bruijn representation of the following types:
+∀α. α:
+  ∀.#0
+∀α. α → α:
+  ∀.#0->#0
+∀α, β. α → (β → α) → α:
+  ∀.∀. #1 -> (#0 -> #1) -> #1
+∀α. (∀β. β → α) → (∀β, δ. β → δ → α):
+  ∀. (∀. #0 -> #1) -> (∀. ∀. #1 -> #0 -> #2)
+∀α, β. (β → (∀α. α → β)) → α:
+  ∀. ∀. (#0 -> (∀. #0 -> #1)) -> #1
+
+Named representation of the following types:
+∀. ∀. #0:
+  ∀α,β. β
+∀. (∀. #1 → #0):
+  ∀α. ∀β. α→β
+∀. ∀. (∀. #1 → #0):
+  ∀α,β,γ. β→γ
+∀. (∀. #0 → #1) → ∀. #0 → #1 → #0:
+  ∀α. (∀δ. δ→α) → ∀γ. γ → α → γ
+*)
+
+(* Imagine being a coq standard library author *)
+Definition merge {A B C: Type} (f: A → B → C):
+  option A → option B → option C
+  := fun oa ob => match oa, ob with
+    | Some a, Some b => Some (f a b)
+    | _, _ => None
+  end.
+
+Definition gmap_inc_insert (m: gmap string nat) (key: string): gmap string nat :=
+  <[ key := 0 ]> (Nat.succ <$> m).
+
 Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type :=
-  None (* FIXME *). 
+  match A with
+  | PTVar ty_name => TVar <$> (m !! ty_name)
+  | PInt => Some Int
+  | PBool => Some Bool
+  | PTForall ty_name body => TForall <$> (debruijn (gmap_inc_insert m ty_name) body)
+  | PTExists ty_name body => TExists <$> (debruijn (gmap_inc_insert m ty_name) body)
+  | PFun lhs rhs =>
+    merge Fun (debruijn m lhs) (debruijn m rhs)
+  end.
 
 (* Example *)
 Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
 Proof.
-  (* Should be solved by reflexivity. *)
-  (* TODO: exercise *)
-Admitted.
+  reflexivity.
+Qed.
 
 
 Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty.
 Proof.
-  (* Should be solved by reflexivity. *)
-  (* TODO: exercise *)
-Admitted.
+  reflexivity.
+Qed.
 
 
 Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty.
 Proof.
-  (* Should be solved by reflexivity. *)
-  (* TODO: exercise *)
-Admitted.
+  reflexivity.
+Qed.
+
+Theorem debruijn_inv_multiple: ∃ (T1 T2: ptype), T1 ≠ T2 ∧ debruijn ∅ T1 = debruijn ∅ T2.
+Proof.
+  exists (∀: "x", "x")%pty.
+  exists (∀: "y", "y")%pty.
+  split.
+  discriminate.
+  reflexivity.
+Qed.
+
+(*
+  The issue with our naive implementation of ⤉σ is that any non-primitive type can cause unwanted behavior if that type refers to something from the higher context:
+  ∀. (∀.∀. #0 → #1)<∀.#0→#1> => ∀. (∀. (∀.#0→#1) → #1) and not what we expect, ie ∀. (∀. (∀.#0→#2) → #1)
 
+  In the lecture, we also saw `A[id] = (∀. #0 -> #1)[id] = ∀. (#0 -> #1)[⤉id] = ∀. (#0 -> (id(0))) = ∀. #0 -> #0`
 
+  To fix this, we would have to carefully tweak each value in our substitution map to increment all the free type variables
+*)