✨ Ugly but working proof of the third free theorem

theories/type_systems/systemf/exercises04.v

@@ -308,6 +308,54 @@ Section free_theorems.
 
   Definition 𝒢_any: 𝒢 δ_any ∅ ∅ := sem_context_rel_any.
 
+  Ltac destruct_type_interp H := match type of H with
+  | ℰ (?T) ?delta ?f =>
+    let Hval := fresh "v" in
+    let Hstep := fresh "Hbs" in
+    simp type_interp in H;
+    destruct H as (Hval & Hstep & H);
+    try destruct_type_interp H
+  | 𝒱 (∀: ?T) ?delta ?f =>
+    let Hclosed := fresh "Hcl" in
+    simp type_interp in H;
+    destruct H as (? & -> & Hclosed & H);
+    try destruct_type_interp H
+  | 𝒱 (?T → ?U) ?delta ?f =>
+    let Hclosed := fresh "Hcl" in
+    let param := fresh "arg" in
+    let body := fresh "e_body" in
+    simp type_interp in H;
+    destruct H as (param & body & -> & Hclosed & H)
+  | 𝒱 (?T × ?U) ?delta ?f =>
+    let lhs := fresh "e_lhs" in
+    let rhs := fresh "e_rhs" in
+    simp type_interp in H;
+    destruct H as (lhs & rhs & -> & ?H1 & ?H2);
+    try destruct_type_interp H1;
+    try destruct_type_interp H2
+  | 𝒱 (TVar ?n) ?delta ?f =>
+    simp type_interp in H;
+    simpl in H
+  end.
+
+  Ltac choose_type_interp H pred :=
+    let tau := fresh "τ" in
+    let v := fresh "v" in
+    let Hv := fresh "Hv" in
+    specialize_sem_type H with (pred) as tau;
+    first (intros v Hv; try naive_solver);
+    last try destruct_type_interp H.
+
+  Ltac choose_param H param :=
+    specialize (H param);
+    match type of H with
+    | 𝒱 ?T ?delta ?expr → ?rest =>
+      let hyp := fresh "Harg" in
+      assert (𝒱 T delta expr) as hyp;
+      first try (simp type_interp; simpl; naive_solver);
+      last (specialize (H hyp); try destruct_type_interp H; try destruct_type_interp hyp)
+    end.
+
   (** Exercise 4 (LN Exercise 27): Free Theorems I *)
   (* a) State a free theorem for the type ∀ α, β. α → β → α × β *)
   (*
@@ -330,6 +378,25 @@ Section free_theorems.
     is_closed [] vb →
     big_step (f<><> (of_val va) (of_val vb)) (va, vb).
   Proof.
+    intros f [Hcl₁ H]%sem_soundness va vb Hcla Hclb.
+    specialize (H ∅ δ_any 𝒢_any).
+    rewrite subst_map_empty in H.
+
+    destruct_type_interp H.
+
+    choose_type_interp H (λ v, v = va).
+    choose_type_interp H (λ v, v = vb).
+    choose_param H va.
+    choose_param H vb.
+
+    subst.
+
+    clear Harg Harg0 Hcl Hcl0 Hcl1 Hcl2.
+
+    econstructor; [ | (apply big_step_of_val; reflexivity) | exact Hbs3 ].
+    econstructor; [ | (apply big_step_of_val; reflexivity) | exact Hbs2 ].
+    eauto.
+  Restart.
     intros f Hty_f va vb Hcla Hclb.
     destruct (sem_soundness Hty_f) as [Hcl₁ Hlog₁].
 
@@ -488,8 +555,6 @@ Section free_theorems.
     exact Hsem.
   Qed.
 
-
-
   (** Exercise 5 (LN Exercise 28): Free Theorems II *)
   Lemma free_theorem_either :
     ∀ f : val,
@@ -497,19 +562,39 @@ Section free_theorems.
     ∀ (v1 v2 : val), is_closed [] v1 → is_closed [] v2 →
       big_step (f <> v1 v2) v1 ∨ big_step (f <> v1 v2) v2.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
+    intros f [Hcl H]%sem_soundness va vb Hcla Hclb.
+    specialize (H ∅ δ_any 𝒢_any).
+    rewrite subst_map_empty in H.
+
+    destruct_type_interp H.
+
+    choose_type_interp H (λ v, ((v = va) ∨ (v = vb))).
+    choose_param H va.
+    choose_param H vb.
+
+    induction H as [-> | ->].
+    1: left.
+    2: right.
+    all: (
+      econstructor; [ | apply big_step_of_val; reflexivity | exact Hbs2 ];
+      econstructor; [ | apply big_step_of_val; reflexivity | exact Hbs1 ];
+      eauto
+    ).
+  Qed.
 
 
   (** Exercise 6 (LN Exercise 29): Free Theorems III *)
   (* Hint: you might want to use the fact that our reduction is deterministic. *)
-  Lemma big_step_det e v1 v2 :
+  Lemma big_step_det {e v1 v2} :
     big_step e v1 → big_step e v2 → v1 = v2.
   Proof.
     induction 1 in v2 |-*; inversion 1; subst; eauto 2.
     all: naive_solver.
   Qed.
 
+  (*
+    Idea: pick τ_α = { v ∈ CVal | ∃ v1, v2, bigstep (g v1 v2) v }
+  *)
   Lemma free_theorems_magic :
     ∀ (A A1 A2 : type) (f g : val),
     type_wf 0 A → type_wf 0 A1 → type_wf 0 A2 →
@@ -525,8 +610,79 @@ Section free_theorems.
         - [val_rel_is_closed]
         - [big_step_preserve_closed]
     *)
-    (* TODO: exercise *)
-  Admitted.
+    intros A B C f g HwfA HwfB HwfC Hcl Hcl0 [Hcl_f Hsem_f]%sem_soundness [Hcl_g Hsem_g]%sem_soundness v Hbs.
+
+    specialize (Hsem_f ∅ δ_any 𝒢_any).
+    specialize (Hsem_g ∅ δ_any 𝒢_any).
+
+    destruct_type_interp Hsem_f.
+    choose_type_interp Hsem_f (λ (v' : val),
+      is_closed [] v'
+      ∧ ∃ (v1 v2 : val), big_step (g v1 v2) v'
+      ∧ 𝒱 B δ_any v1
+      ∧ 𝒱 C δ_any v2
+    ).
+    destruct_type_interp Hsem_g.
+    rewrite subst_map_empty in Hbs2.
+    rename arg0 into g_arg.
+    rename e_body0 into g_body.
+
+    choose_param Hsem_f (LamV g_arg g_body).
+    {
+      (* TODO: do the paper proof to see if there isn't a cleaner way to go about this part *)
+      simp type_interp.
+      eexists.
+      eexists.
+      split; last split; [ reflexivity | eauto | ].
+      intros v' Hsem_v'.
+
+      simp type_interp.
+      choose_param Hsem_g v'.
+      {
+        erewrite <-(type_wf_closed B) in Hsem_v'; last assumption.
+        rewrite <-sem_val_rel_cons in Hsem_v'.
+        exact Hsem_v'.
+      }
+
+      eexists; split.
+      exact Hbs3.
+      simp type_interp.
+      eexists; eexists; split; last split; first reflexivity.
+      eauto.
+      intros w Hsem_w.
+      simp type_interp.
+      choose_param Hsem_g w.
+      {
+        erewrite <-(type_wf_closed C) in Hsem_w; last assumption.
+        rewrite <-sem_val_rel_cons in Hsem_w.
+        exact Hsem_w.
+      }
+
+      eexists; split.
+      exact Hbs4.
+
+      simp type_interp; simpl; split.
+      eapply val_rel_closed; exact Hsem_g.
+      exists v'.
+      exists w.
+      split; last split; try assumption.
+      econstructor; eauto.
+      econstructor; eauto.
+      all: eapply big_step_of_val; reflexivity.
+    }
+    destruct Hsem_f as (Hcl4 & v1 & v2 & Hbs4).
+    exists v1.
+    exists v2.
+
+    choose_param Hsem_g v1.
+    choose_param Hsem_g v2.
+
+    rewrite subst_map_empty in Hbs0.
+    assert (big_step ((f<>) g) v0) as Hbs'; first by eauto.
+    rewrite (big_step_det Hbs Hbs').
+    destruct Hbs4 as [Hbs4 _].
+    exact Hbs4.
+  Qed.
 
 
 End free_theorems.