From 930b4510bd12abfe8b9c1ce15e46a56dde034b2e Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Wed, 22 Nov 2023 21:02:25 +0100 Subject: [PATCH] :sparkles: Ugly but working proof of the third free theorem --- theories/type_systems/systemf/exercises04.v | 170 +++++++++++++++++++- 1 file changed, 163 insertions(+), 7 deletions(-) diff --git a/theories/type_systems/systemf/exercises04.v b/theories/type_systems/systemf/exercises04.v index 02ec664..b9ee84b 100644 --- a/theories/type_systems/systemf/exercises04.v +++ b/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.