✨ Solve compat lemmas in system f and most free theorems

theories/type_systems/systemf/exercises04.v

@@ -301,35 +301,192 @@ Section church_encodings.
 End church_encodings.
 
 Section free_theorems.
+  Lemma sem_context_rel_any: 𝒢 δ_any ∅ ∅.
+  Proof.
+    exact (sem_context_rel_empty δ_any).
+  Qed.
+
+  Definition 𝒢_any: 𝒢 δ_any ∅ ∅ := sem_context_rel_any.
+
   (** Exercise 4 (LN Exercise 27): Free Theorems I *)
   (* a) State a free theorem for the type ∀ α, β. α → β → α × β *)
+  (*
+    The way we prove this is by first destroying everything,
+    specializing all the theorems using δ_any and 𝒢_any_any.
+
+    We then unwrap `f ∈ E[∀α, ∀β, α → β → α × β]`:
+    - first pick τa = {va}
+    - then pick τb = {vb}
+    - pick as argument in V[α → β → α × β] va; va ∈ V[α]·(α↦τa) is trivially true
+    - pick as argument in V[β → α × β] vb; vb ∈ V[β]·(β↦τb) is trivially true
+    - f must finally return a pair of type (α × β); from our choice of τa and τb, the only possible choice is (va × vb)
+    - go back and re-construct the `big_step`
+  *)
   Lemma free_thm_1 :
     ∀ f : val,
     TY 0; ∅ ⊢ f : (∀: ∀: #1 → #0 → #1 × #0) →
-    True (* FIXME state your theorem *).
+    ∀ (va vb : val),
+    is_closed [] va →
+    is_closed [] vb →
+    big_step (f<><> (of_val va) (of_val vb)) (va, vb).
   Proof.
-    (* TODO: exercise *)
+    intros f Hty_f va vb Hcla Hclb.
-  Admitted.
+    destruct (sem_soundness Hty_f) as [Hcl₁ Hlog₁].
+
+    specialize (Hlog₁ ∅ δ_any 𝒢_any).
+
+    rewrite subst_map_empty in Hlog₁.
+    simp type_interp in *.
+    destruct Hlog₁ as (vf₁ & Hbs₁ & Hlog₁).
+
+    simp type_interp in Hlog₁; destruct Hlog₁ as (f₂ & -> & Hcl₂ & Hlog₂).
+    (* POI 1: choose τa = {va} *)
+    specialize_sem_type Hlog₂ with (λ v, v = va) as τa.
+    {
+      intros v ->; done.
+    }
+
+    simp type_interp in Hlog₂; destruct Hlog₂ as (vf₂ & Hbs₂ & Hlog₂).
+    simp type_interp in Hlog₂; destruct Hlog₂ as (f₃ & -> & Hcl₃ & Hlog₃).
+    (* POI 2: choose τb = {vb} *)
+    specialize_sem_type Hlog₃ with (λ v, v = vb) as τb.
+    {
+      intros v ->; done.
+    }
+
+    simp type_interp in Hlog₃; destruct Hlog₃ as (vf₃ & Hbs₃ & Hlog₃).
+
+    simp type_interp in Hlog₃; destruct Hlog₃ as (
+      xa & f₄ & -> & Hcl₄ & Hlog₄
+    ).
+    (* Pick va as argument *)
+    specialize (Hlog₄ va ltac:(done)).
+
+    simp type_interp in Hlog₄; destruct Hlog₄ as (vf₄ & Hbs₄ & Hlog₄).
+
+    simp type_interp in Hlog₄; destruct Hlog₄ as (
+      xb & f₅ & -> & Hcl₅ & Hlog₅
+    ).
+    (* Pick vb as argument *)
+    specialize (Hlog₅ vb ltac:(done)).
+    simp type_interp in Hlog₅; destruct Hlog₅ as (vf₅ & Hbs₅ & Hlog₅).
+
+    simp type_interp in Hlog₅; destruct Hlog₅ as (
+      va' & vb' & -> & -> & ->
+    ).
+
+    econstructor; [ | (apply big_step_of_val; reflexivity) | exact Hbs₅ ].
+    econstructor; [ | (apply big_step_of_val; reflexivity) | exact Hbs₄ ].
+    eauto.
+  Qed.
 
 
   (* b) State a free theorem for the type ∀ α, β. α × β → α *)
   Lemma free_thm_2 :
     ∀ f : val,
     TY 0; ∅ ⊢ f : (∀: ∀: #1 × #0 → #1) →
-    True (* FIXME state your theorem *).
+    ∀ (va vb : val),
+    is_closed [] va →
+    is_closed [] vb →
+    big_step (f<><> (PairV va vb)) va.
   Proof.
-    (* TODO: exercise *)
+    intros f Hty_f va vb Hcla Hclb.
-  Admitted.
+
+    destruct (sem_soundness Hty_f) as [Hcl₁ Hlog₁].
+
+    specialize (Hlog₁ ∅ δ_any 𝒢_any).
+
+    rewrite subst_map_empty in Hlog₁.
+    simp type_interp in *.
+    destruct Hlog₁ as (vf₁ & Hbs₁ & Hlog₁).
+
+    simp type_interp in Hlog₁; destruct Hlog₁ as (f₂ & -> & Hcl₂ & Hlog₂).
+    (* POI 1: choose τa = {va} *)
+    specialize_sem_type Hlog₂ with (λ v, v = va) as τa.
+    {
+      intros v ->; done.
+    }
+
+    simp type_interp in Hlog₂; destruct Hlog₂ as (vf₂ & Hbs₂ & Hlog₂).
+    simp type_interp in Hlog₂; destruct Hlog₂ as (f₃ & -> & Hcl₃ & Hlog₃).
+    (* POI 2: choose τb = {vb} *)
+    specialize_sem_type Hlog₃ with (λ v, v = vb) as τb.
+    {
+      intros v ->; done.
+    }
+
+    simp type_interp in Hlog₃; destruct Hlog₃ as (vf₃ & Hbs₃ & Hlog₃).
+    simp type_interp in Hlog₃; destruct Hlog₃ as (
+      xpair & f₄ & -> & Hcl₄ & Hlog₄
+    ).
+    assert (𝒱 (#1 × #0) (τb .: τa .: δ_any) (PairV va vb)) as Hlog_pair.
+    {
+      simp type_interp.
+      exists va.
+      exists vb.
+      split; last split.
+      reflexivity.
+      done.
+      done.
+    }
+    specialize (Hlog₄ (PairV va vb) ltac:(done)).
+    simp type_interp in Hlog₄.
+    destruct Hlog₄ as (vf₄ & Hbs₄ & Hlog₄).
+
+    simp type_interp in Hlog₄.
+    simpl in Hlog₄.
+    rewrite Hlog₄ in Hbs₄.
+
+    econstructor.
+    2: eapply big_step_of_val; reflexivity.
+    2: exact Hbs₄.
+    eauto.
+  Qed.
 
 
   (* c) State a free theorem for the type ∀ α, β. α → β *)
+  (*
+    f cannot exist.
+    We have, by semantical soundness, that `f ∈ E[∀ α, β. α → β]`.
+    Repeatedly apply the definition of `E[T]` and `V[T]`, with:
+    - τα = Int for α
+    - τβ = ∅ for β
+    - provide any integer to `f' ∈ V[#0 → #1]·(↦Int, ↦∅)`, here 1
+    - `f'` steps to `λx.f''` and `f''[1/x] ∈ V[#1]·(↦Int, ↦∅)`
+    - unrolling the definition of `V[#1]`, this means that `f''[1/x] ∈ ∅`
+    - kaboom :)
+  *)
   Lemma free_thm_3 :
     ∀ f : val,
     TY 0; ∅ ⊢ f : (∀: ∀: #1 → #0) →
-    True (* FIXME state your theorem *).
+    False.
   Proof.
-    (* TODO: exercise *)
+    intros f [Hcl Hsem]%sem_soundness.
-  Admitted.
+    specialize (Hsem ∅ δ_any 𝒢_any).
+    simp type_interp in Hsem; destruct Hsem as (v & Hbs & Hsem).
+    simp type_interp in Hsem; destruct Hsem as (e₁ & -> & Hcl₂ & Hsem).
+    specialize (Hsem (interp_type Int δ_any)).
+
+    simp type_interp in Hsem; destruct Hsem as (v & Hbs₂ & Hsem).
+    simp type_interp in Hsem; destruct Hsem as (e₂ & -> & Hcl₃ & Hsem).
+    specialize_sem_type Hsem with (λ _, False) as τ; first done.
+
+    simp type_interp in Hsem; destruct Hsem as (v & Hbs₃ & Hsem).
+    simp type_interp in Hsem; destruct Hsem as (x & body & -> & Hcl₄ & Hsem).
+
+    assert (𝒱 #1 (τ .: interp_type Int δ_any .: δ_any) #1%nat).
+    {
+      simp type_interp.
+      simpl.
+      simp type_interp.
+      eauto.
+    }
+    specialize (Hsem (LitV 1) ltac:(done)).
+    simp type_interp in Hsem; destruct Hsem as (v & Hbs₄ & Hsem).
+    simp type_interp in Hsem.
+    simpl in Hsem.
+    exact Hsem.
+  Qed.
 
 
 

theories/type_systems/systemf/logrel.v

@@ -17,7 +17,7 @@ Implicit Types
 
 (* *** Definition of the logical relation. *)
 (* In Coq, we need to make argument why the logical relation is well-defined
-   precise: 
+   precise:
    In particular, we need to show that the mutual recursion between the value
    relation and the expression relation, which are defined in terms of each
    other, terminates. We therefore define a termination measure [mut_measure]
@@ -339,7 +339,7 @@ End boring_lemmas.
 
 Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) : Int.
 Proof.
-  split; first done. 
+  split; first done.
   intros θ δ _. simp type_interp.
   exists #z. split. { simpl. constructor. }
   simp type_interp. eauto.
@@ -347,7 +347,7 @@ Qed.
 
 Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) : Bool.
 Proof.
-  split; first done. 
+  split; first done.
   intros θ δ _. simp type_interp.
   exists #b. split. { simpl. constructor. }
   simp type_interp. eauto.
@@ -355,7 +355,7 @@ Qed.
 
 Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) : Unit.
 Proof.
-  split; first done. 
+  split; first done.
   intros θ δ _. simp type_interp.
   exists #LitUnit. split. { simpl. constructor. }
   simp type_interp. eauto.
@@ -398,8 +398,8 @@ Qed.
 
 (* Compatibility for [lam] unfortunately needs a very technical helper lemma. *)
 Lemma lam_closed δ Γ θ (x : string) A e :
-  closed (elements (dom (<[x:=A]> Γ))) e → 
+  closed (elements (dom (<[x:=A]> Γ))) e →
-  𝒢 δ Γ θ → 
+  𝒢 δ Γ θ →
   closed [] (Lam x (subst_map (delete x θ) e)).
 Proof.
   intros Hcl Hctxt.
@@ -548,42 +548,207 @@ Proof.
   simp type_interp.
   eexists _. split_and!; first done.
   { simpl. eapply subst_map_closed; simpl.
-    - erewrite <-sem_context_rel_dom; last eassumption. 
+    - erewrite <-sem_context_rel_dom; last eassumption.
       by erewrite <-dom_fmap.
     - by eapply sem_context_rel_closed. }
   intros τ. eapply He.
   by eapply sem_context_rel_cons.
 Qed.
 
+(*
+  Recall that our semantical judgement for `TY Δ; Γ ⊨ e: A` means that:
+  - e is closed under Γ
+  - for any θ ∈ G[Γ] · δ, (these should really be bundled as part of some kind of structure)
+  - e[θ] ∈ E[A]·δ → ∃v, big_step e v ∧ v ∈ V[A]·δ
+  - V[∀: A] = {Λα.e | e is closed ∧ ∀τ, e ∈ E[A]·(δ[α↦τ])}
+
+  Thus, to prove that `TY Δ; Γ ⊨ e<> : A[B/]`,
+  - intro θ, δ, and use them on `TY Δ; Γ ⊨ e : ∀α.A`
+  - we can get by the definition of `E[∀α.A]` that `big_step e v`, `v = (Λα.e')` and `∀τ, e' ∈ E[A]·(δ[α↦τ])`
+  - pick τ = V[B]·δ and use the definition of `E[A]` on `e'` to get that `big_step e' v'` and `v' ∈ V[A]·(δ[α↦τ])`
+  - to prove that `e<> ∈ E[A[B/]]`, we need to prove that `big_step e<>[θ,δ] v'[θ,δ[α↦B]]` and `v' ∈ V[A[B/]]`
+  - from the definition of `big_step e<>`, we need to prove that:
+    - `big_step e (Λα.e')` (which we have)
+    - `big_step e' v'` (which we just proved).
+  - we now just need to prove that given `τ = V[B]` and `v' ∈ V[A]·(δ[α↦τ])`,
+    `v' ∈ V[A[B/]]`
+  - for this we can use the theorem `sem_val_rel_move_single_subst`,
+    which states that `∀A B v, v ∈ V[A]·(δ[↦V[B]]) ↔ v ∈ V[A[B/]]`
+*)
 Lemma compat_tapp Δ Γ e A B :
   type_wf Δ B →
   TY Δ; Γ ⊨ e : (∀: A) →
   TY Δ; Γ ⊨ (e <>) : (A.[B/]).
 Proof.
-  (* TODO: exercise *)
+  intros Hwf Hst.
-Admitted.
+  destruct Hst as [Hcl Hlog].
+  constructor.
+  (* Closedness is easily dispatched *)
+  simpl; exact Hcl.
+  (* Intro θ and δ and use them on Hlog *)
+  intros θ δ Hg; specialize (Hlog θ δ Hg).
+  (* Use the definition of `E[∀α.A]` *)
+  simp type_interp in *; destruct Hlog as (v & Hbs & Hv).
+  simp type_interp in Hv; destruct Hv as (e_body & -> & Hcl' & Hlog').
+  (* Pick τ = V[B] *)
+  remember (interp_type B δ) as Bτ.
+  specialize (Hlog' Bτ).
+  (* Use the definition of E[A]·(δ[α↦τ]) to get the value to which e_body steps and our v_body ∈ V[A]·(δ[α↦τ]) *)
+  simp type_interp in Hlog'; destruct Hlog' as (v_body & Hbs_body & Hlog_body).
+
+  (* We can now prove that e<> steps to v_body *)
+  exists v_body.
+  split; simpl.
+  econstructor; [exact Hbs | exact Hbs_body].
+
+  (* And we can prove that v_body ∈ V[A[B/]], using one of the boring lemmas *)
+  rewrite <-sem_val_rel_move_single_subst.
+  rewrite <-HeqBτ; exact Hlog_body.
+Qed.
+
+(*
+  Recall that:
+  - V[∃: A]·δ = { pack v | ∃τ, v ∈ V[A]·(δ[↦τ]) }
+
+  As usual, we start the proof by intro-ing θ, δ and θ ∈ G[Γ]·δ,
+  and applying these terms to `TY n; Γ ⊨ e : A.[B/]`, yielding `e ∈ E[A[B/]]·δ`.
 
+  Then, apply the definition of `E[T]` everywhere:
+  - we have `big_step e[θ] v` and `v ∈ V[A[B/]]·δ`
+  - we need to provide a `v'` such that `big_step (pack e)[θ] v'` and `v' ∈ V[∃.A]`
 
+  Let `v' = PackV v`, we have `big_step (pack e)[θ] v' = big_step (pack e[θ]) v'`,
+  which we can construct from the definition and from `big_step e[θ] v`.
+
+  Using the definition of `v' ∈ V[∃.A]`, we just need to prove that:
+  - `v' = pack w` (trivial)
+  - `∃τ, w ∈ E[A]·(δ[↦τ])`: pick τ = V[B], apply the same equivalence as the proof of type application:
+
+  We have `v' ∈ V[A]·(δ↦V[B])` ↔ `v' ∈ V[A[B/]]·δ`; we have the latter from the definition of `e ∈ E[A[B/]]`.
+*)
 Lemma compat_pack Δ Γ e n A B :
   type_wf n B →
   type_wf (S n) A →
   TY n; Γ ⊨ e : A.[B/] →
   TY n; Γ ⊨ (pack e) : (∃: A).
 Proof.
-  (* This will be an exercise for you next week :) *)
+  intros HwfB HwfA Hsem.
-  (* TODO: exercise *)
+  destruct Hsem as [Hcl Hlog].
-Admitted.
+  constructor.
+  (* Prove closedness real quick *)
+  {
+    simpl; exact Hcl.
+  }
+  (* Flatten everything under θ and δ *)
+  intros θ δ Hg; specialize (Hlog θ δ Hg).
+
+  (* Apply the definition of E[T] *)
+  simp type_interp in *.
+  destruct Hlog as (v_inner & Hbs & Hlog).
+  simpl.
+
+  (* Pick v' = PackV v *)
+  exists (PackV v_inner).
+  split.
+
+  (* Prove that big_step (Pack e[θ]) v' *)
+  econstructor; exact Hbs.
 
+  simp type_interp.
+  eexists; split; first reflexivity.
+  exists (interp_type B δ).
+  rewrite sem_val_rel_move_single_subst.
+  exact Hlog.
+Qed.
+
+(*
+  This proof is a bit trickier, as it combines the difficulties of both previous proofs.
+
+  We can intro θ and δ and specialize `TY n; Γ ⊨ e : (∃: A)`, yielding `big_step e v_pack`
+  and `v_pack ∈ V[∃.A]`.
+
+  We can then unwrap the definition of `V[∃.A]`, asserting that `v_pack = pack v_inner`,
+  and yielding a semantic type τ such that `v_inner ∈ V[A]·(δ[↦τ])`.
 
+  We can construct θ' = θ[x ↦ v_inner], δ' = δ[↦τ] and Γ' = (⤉Γ)[x↦A].
+  Proving that θ' ∈ G[Γ']·δ' can be done using the fact that `v_inner ∈ V[A]·(δ[↦τ])`
+  and one of the boring lemmas.
+
+  We can then plug θ', δ' and Γ' into `TY S n; <[x:=A]> (⤉Γ) ⊨ e' : B.[ren (+1)]`
+  and unwrap the definition of `E[B[ren +1]]`, yielding a value `v_unpacked`, towards which `e'[θ']` steps,
+  and the proposition that `v_unpacked ∈ V[B[ren +1]]·(δ[↦τ])`
+
+  We can now plug in `v_unpacked` as our target of `big_step (unpack e as BNamed x in e')[θ]`.
+  We need to prove that `e[θ]` steps to `v_inner` and that `e'[θ-x][v_inner/x]` steps to `v_unpacked`.
+  The latter requires a few boring lemmas to get to `big_step e'[θ'] v_unpacked`.
+
+  We now just need to prove that `v_unpacked ∈ V[B]·δ`. Boring lemma time :)
+*)
 Lemma compat_unpack n Γ A B e e' x :
   type_wf n B →
   TY n; Γ ⊨ e : (∃: A) →
   TY S n; <[x:=A]> (⤉Γ) ⊨ e' : B.[ren (+1)] →
   TY n; Γ ⊨ (unpack e as BNamed x in e') : B.
 Proof.
-  (* This will be an exercise for you next week :) *)
+  intros HwfB Hsem Hsem'.
-  (* TODO: exercise *)
+  destruct Hsem as [Hcl Hlog].
-Admitted.
+  destruct Hsem' as [Hcl' Hlog'].
+  constructor.
+  (* Closedness is a bit trickier but can be done: *)
+  {
+    simpl.
+    apply andb_True; split.
+    - exact Hcl.
+    - rewrite dom_insert in Hcl'.
+      rewrite dom_fmap in Hcl'.
+      induction (decide (x ∈ dom Γ)) as [ | H_notin ].
+      + assert ({[x]} ∪ dom Γ = dom Γ) as Heq by set_solver.
+        rewrite Heq in Hcl'.
+        eapply is_closed_weaken.
+        exact Hcl'.
+        set_solver.
+      + eapply is_closed_weaken.
+        exact Hcl'.
+        set_solver.
+  }
+  intros θ δ Hg; specialize (Hlog θ δ Hg).
+  simpl.
+
+  simp type_interp in *.
+  destruct Hlog as (v_pack & Hbs_pack & Hlog_pack).
+  simp type_interp in Hlog_pack.
+  destruct Hlog_pack as (v_inner & -> & τ & Hlog_inner).
+
+  remember (τ .: δ) as δ'.
+  remember (<[x := of_val v_inner]> θ) as θ'.
+  remember (<[x:=A]> (⤉Γ)) as Γ'.
+
+  assert (𝒢 δ' Γ' θ') as Hg'.
+  {
+    subst.
+    econstructor.
+    exact Hlog_inner.
+    apply sem_context_rel_cons.
+    exact Hg.
+  }
+  specialize (Hlog' θ' δ' Hg').
+
+  simp type_interp in Hlog'.
+  destruct Hlog' as (v_unpacked & Hbs_unpacked & Hlog_unpacked).
+
+  exists v_unpacked; split.
+  - econstructor.
+    exact Hbs_pack.
+
+    simpl.
+    rewrite subst_subst_map.
+    rewrite <-Heqθ'.
+    exact Hbs_unpacked.
+    exact (sem_context_rel_closed _ _ _ Hg).
+  - rewrite Heqδ' in Hlog_unpacked.
+    rewrite <-sem_val_rel_cons in Hlog_unpacked.
+    exact Hlog_unpacked.
+Qed.
 
 
 Lemma compat_if n Γ e0 e1 e2 A :
@@ -707,7 +872,7 @@ Proof.
     econstructor; [done | apply big_step_of_val; done | done].
 Qed.
 
-Lemma sem_soundness Δ Γ e A :
+Lemma sem_soundness {Δ Γ e A} :
   TY Δ; Γ ⊢ e : A →
   TY Δ; Γ ⊨ e : A.
 Proof.