From 315dcdefa636574953b261d0e4bc4d64ada3612a Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Wed, 29 Nov 2023 15:11:57 +0100 Subject: [PATCH] :sparkle: Finish exercises 5, with lots of frustration --- _CoqProject | 2 +- theories/type_systems/systemf/binary_logrel.v | 150 +++- theories/type_systems/systemf/exercises05.v | 651 +++++++++++++++++- theories/type_systems/systemf/types.v | 27 +- 4 files changed, 788 insertions(+), 42 deletions(-) diff --git a/_CoqProject b/_CoqProject index 54d7406..c5bc489 100644 --- a/_CoqProject +++ b/_CoqProject @@ -62,4 +62,4 @@ theories/type_systems/stlc/exercises02.v #theories/type_systems/systemf/exercises03_sol.v #theories/type_systems/systemf/exercises04.v #theories/type_systems/systemf/exercises04_sol.v -#theories/type_systems/systemf/exercises05.v +theories/type_systems/systemf/exercises05.v diff --git a/theories/type_systems/systemf/binary_logrel.v b/theories/type_systems/systemf/binary_logrel.v index 33787fa..2ff03de 100644 --- a/theories/type_systems/systemf/binary_logrel.v +++ b/theories/type_systems/systemf/binary_logrel.v @@ -395,8 +395,20 @@ Proof. do 2 (split; first eapply bool_decide_pack, elem_of_elements, elem_of_dom_2, Hx). intros θ1 θ2 δ Hctx; simpl. - (* TODO: exercise *) -Admitted. + destruct (sem_context_rel_vals Hctx Hx) as (e1 & e2 & v1 & v2 & -> & -> & H1%of_to_val & H2%of_to_val & Hlogrel). + simp type_interp. + exists v1. + exists v2. + split; last split. + apply big_step_of_val; eauto. + apply big_step_of_val; eauto. + assumption. + + (* I want to stress that the fact that we duplicated proofs for binary logical relations + because of the arbitrary decision of using the same notation for binary logical relations + as with unary logical relations is quite concerning. + *) +Qed. Lemma compat_app Δ Γ e1 e1' e2 e2' A B : @@ -427,7 +439,7 @@ Qed. Lemma lam_closed Γ θ (x : string) A e : dom Γ = dom θ → subst_is_closed [] θ → - closed (elements (dom (<[x:=A]> Γ))) e → + closed (elements (dom (<[x:=A]> Γ))) e → closed [] (Lam x (subst_map (delete x θ) e)). Proof. intros Hdom Hsubstcl Hcl. @@ -631,8 +643,42 @@ Proof. do 2 (split; first naive_solver). intros θ1 θ2 δ Hctx. simpl. - (* TODO: exercise *) -Admitted. + (* + Let us prove that Δ; Γ |= e<> ≈ e'<> : A[B/] + <= ∀θ1, θ2, (θ1, θ2) ∈ 𝒢[Γ]·δ, (e[θ1]<>, e'[θ2]<>) ∈ ℰ[A[B/]]·δ + + Let us first specialize our hypothesis with θ1 and θ2. + (e[θ1], e'[θ2]) ∈ ℰ[∀.A]·δ + => (e[θ1] ↓ e1, e'[θ2] ↓ e2) ∈ 𝒱[∀.A]·δ + => ∀ τ, e1 = (Λα, e1') & e2 = (Λα, e2') & (e1', e2') ∈ ℰ[A]·(δ, α↦τ) + Pick τ = 𝒱[B]·δ: + => e1' ↓ v1 & e2' ↓ v2 & (v1, v2) ∈ 𝒱[A]·(δ, α↦𝒱[B]·δ) + + We then prove our goal with: + e[θ1]<> ↓ v1 + e[θ2]<> ↓ v2 + (v1, v2) ∈ 𝒱[A]·(δ, α↦𝒱[B]·δ) = 𝒱[A[B/]] + *) + specialize (He θ1 θ2 δ Hctx). + simp type_interp in He. + destruct He as (v1' & v2' & Hbs_Λe1 & Hbs_Λe2 & He). + simp type_interp in He. + destruct He as (e1 & e2 & -> & -> & Hcl1 & Hcl2 & He). + + specialize (He (interp_type B δ)). + simp type_interp in He. + destruct He as (v1 & v2 & Hbs_v1 & Hbs_v2 & He). + + simp type_interp. + exists v1. + exists v2. + split; last split. + bs_step_det. + bs_step_det. + + rewrite <-sem_val_rel_move_single_subst. + exact He. +Qed. Lemma compat_pack Δ Γ e e' n A B : @@ -645,8 +691,28 @@ Proof. do 2 (split; first naive_solver). intros θ1 θ2 δ Hctx. simpl. - (* TODO: exercise *) -Admitted. + (* + Similarly as with e<>, we specialize our hypothesis with θ1 and θ2. + We get e ↓ v1, e' ↓ v2, (v1, v2) ∈ 𝒱[A[B/]]·δ + + So (pack e) ↓ (pack v1), (pack e') ↓ (pack v2) + Both are values, so we need to show that (pack v1, pack v2) ∈ 𝒱[∃. A] ⊆ ℰ[∃. A] + By definition, 𝒱[∃α. A] = { (a, b) | ∃τ, (a, b) ∈ 𝒱[A]·(δ, α↦τ) } + Picking τ = B, we then have (v1, v2) ∈ 𝒱[A[B/]]·δ = 𝒱[A]·(δ, α↦B) + *) + + specialize (He θ1 θ2 δ Hctx). + simp type_interp in He. + destruct He as (v1 & v2 & Hbs1 & Hbs2 & He). + + simp type_interp. + eexists; eexists; split; last split; [bs_step_det | bs_step_det | ]. + + simp type_interp; eexists; eexists; split; first reflexivity; split; first reflexivity. + exists (interp_type B δ). + rewrite sem_val_rel_move_single_subst. + exact He. +Qed. Lemma compat_unpack n Γ A B e1 e1' e2 e2' x : @@ -660,10 +726,72 @@ Proof. eapply is_closed_weaken; set_solver. } split. { simpl. apply andb_True. split; first done. eapply is_closed_weaken; set_solver. } - intros θ1 θ2 δ Hctx. simpl. + intros θ1 θ2 δ Hctx. simpl. - (* TODO: exercise *) -Admitted. + (* + Specialize the first hypothesis with θ1 and θ2, extracting + v1, v2 and τ such that e1[θ1] ↓ (pack v1) and e2[θ2] ↓ (pack v2) and (v1, v2) ∈ 𝒱[A]·(δ, ↦τ) + *) + specialize (He θ1 θ2 δ Hctx). + simp type_interp in He. + destruct He as (v1' & v2' & Hbs1 & Hbs2 & He). + simp type_interp in He. + destruct He as (v1 & v2 & -> & -> & τ & He). + + (* + Construct δ' = (δ, ↦τ), θ1' = (θ1, x ↦ v1), θ2' = (θ1, x ↦ v2), Γ' = (Γ, x ↦ A) + *) + remember (τ .: δ) as δ'. + remember (<[x := A]> (⤉Γ)) as Γ'. + remember (<[x := of_val v1]> θ1) as θ1'. + remember (<[x := of_val v2]> θ2) as θ2'. + have Hctx' : 𝒢 δ' Γ' θ1' θ2'. + { + rewrite HeqΓ' Heqθ1' Heqθ2'. + econstructor. + exact He. + rewrite Heqδ'. + apply sem_context_rel_cons. + exact Hctx. + } + + (* + Specialize the second hypothesis with θ1' and θ2', + yielding + e1'[θ1'] ↓ r1, e2'[θ2'] ↓ r2, (r1, r2) ∈ 𝒱[↑B]·δ' = 𝒱[B]·δ + *) + specialize (He' θ1' θ2' δ' Hctx'). + simp type_interp in He'. + destruct He' as (r1 & r2 & Hbs_r1 & Hbs_r2 & He'). + + (* Use r1 and r2; from (θ1, θ2) ∈ 𝒢[Γ], + we can cancel out the substitution from both hypotheses. + *) + simp type_interp. + exists r1. + exists r2. + split; last split. + { + bs_step_det. + rewrite subst_subst_map. + rewrite <-Heqθ1'. + exact Hbs_r1. + destruct (sem_context_rel_closed _ _ _ _ Hctx) as [Hcl _]. + exact Hcl. + } + { + bs_step_det. + rewrite subst_subst_map. + rewrite <-Heqθ2'. + exact Hbs_r2. + destruct (sem_context_rel_closed _ _ _ _ Hctx) as [_ Hcl]. + exact Hcl. + } + (* (r1, r2) ∈ 𝒱[B]·δ, finishing our proof *) + rewrite Heqδ' in He'. + rewrite <-sem_val_rel_cons in He'. + exact He'. +Qed. Lemma compat_if n Γ e0 e0' e1 e1' e2 e2' A : @@ -700,7 +828,7 @@ Proof. do 2 (split; first naive_solver). intros θ1 θ2 δ Hctx. simpl. simp type_interp. - + specialize (He1 _ _ _ Hctx). specialize (He2 _ _ _ Hctx). simp type_interp in He1. simp type_interp in He2. diff --git a/theories/type_systems/systemf/exercises05.v b/theories/type_systems/systemf/exercises05.v index b5b2415..c1126dd 100644 --- a/theories/type_systems/systemf/exercises05.v +++ b/theories/type_systems/systemf/exercises05.v @@ -47,33 +47,94 @@ Section existential. TY n; <[x := A]> (<[f := (A → B)%ty]> Γ) ⊢ e : B → TY n; Γ ⊢ (fix: f x := e) : (A → B)). - Definition ISET : type :=#0. (* TODO: your definition *) + Definition ISET : type := (∃: + #0 × (Int → #0) + × (#0 → #0 → #0) + × (#0 → #0 → Bool) + ). (* We represent sets as functions of type ((Int → Bool) × Int × Int), storing the mapping, the minimum value, and the maximum value. *) - - Definition iset : val :=#0. (* TODO: your definition *) + (* + Let α = (Int → Bool) × Int × Int = { + is_mem: Int -> Bool, + min: Int, + max: Int + } st. ∀s: α, + • ∀x < s.min, s.is_mem x ~>* false + • ∀x > s.max, s.is_mem x ~>* false + + As such, the empty set is `((λ_. false), 0, 0)` + + ISET = sig + type α -- ommitted, part of ∃ + empty : α + singleton : Int -> α + union : α -> α -> α + subset : α -> α -> bool + end + *) + + Definition subset_helper : expr := (λ: "a" "b", (fix: "rec" "x" := ( + if: ((Snd "a") < "x") then + (Lit true) + else + ( + if: ((Fst (Fst "a")) "x") then + ( + if: ((Fst (Fst "b")) "x") then + ("rec" ("x" + (Lit 1))) + else + (Lit false) + ) + else + "rec" ("x" + (Lit 1)) + ) + ))). + + Definition iset : val := (pack ( + ((λ: BAnon, (Lit false)), (LitV 0), (LitV 0)), + (λ: "x", ((λ: "y", "x" = "y"), "x", "x")), + (λ: "a" "b", ( + (λ: "y", if: ((Fst (Fst "a"))) "y" then ((Fst (Fst "b")) "y") else (Lit false)), + if: (Snd (Fst "a")) < (Snd (Fst "b")) then (Snd (Fst "a")) else (Snd (Fst "b")), + if: (Snd "b") < (Snd "a") then (Snd "a") else (Snd "b") + )), + (λ: "a" "b", ( + subset_helper "a" "b" (Snd (Fst "a")) + )) + )). Lemma iset_typed n Γ : TY n; Γ ⊢ iset : ISET. Proof. - (* HINT: use repeated solve_typing with an explicit apply fix_typing inbetween *) - (* TODO: exercise *) - Admitted. - - - Definition ISETE : type :=#0. (* TODO: your definition *) - - Definition add_equality : val :=#0. (* TODO: your definition *) + repeat solve_typing. + eapply fix_typing; try eauto. + repeat solve_typing. + Qed. + + Definition ISETE : type := (∃: + #0 × (Int → #0) + × (#0 → #0 → #0) + × (#0 → #0 → Bool) + × (#0 → #0 → Bool) + ). + + Definition add_equality : val := (λ: "impl", unpack "impl" as "impl2" in (pack ( + (Fst (Fst "impl2")), + (Snd (Fst "impl2")), + (Snd "impl2"), + (λ: "a" "b", if: ((Snd "impl2") "a" "b") then + ((Snd "impl2") "b" "a") + else + (Lit false) + ) + ))). Lemma add_equality_typed n Γ : TY n; Γ ⊢ add_equality : (ISET → ISETE)%ty. Proof. repeat solve_typing. - (* Qed. *) - (* TODO: exercise *) - Admitted. - - + Qed. End existential. Section ex4. @@ -101,23 +162,109 @@ Context (even_dec_typed : ∀ n Γ, TY n; Γ ⊢ even_dec : (Int → Bool)). You may use the [assert] expression defined in existential_invariants.v. *) -Definition even_impl_instrumented : val :=#0. (* TODO: your definition *) +Definition even_impl_instrumented : val := pack (#0, + λ: "z", #2 + "z", + λ: "z", (Snd (assert (even_dec "z"), "z")) +). (* TODO: your definition *) (* b) Prove that [even_impl_instrumented] is safe. You may assume that even works as intended, but be sure to state this here. *) +Context (even_dec_correct : ∀ n, big_step (even_dec (Lit (2*n)%Z)) #true). Lemma even_impl_instrumented_safe δ: 𝒱 even_type δ even_impl_instrumented. Proof. - (* TODO: exercise *) -Admitted. + unfold even_type. + simp type_interp. + eexists; split; first reflexivity. + (* Pick τ such that it only contains even integers *) + pose_sem_type (fun n => match n with + | LitV (LitInt n') => ∃ (x: Z), (2 * x)%Z = n' + | _ => False + end + ) as τ. + { + intros v h_v. + destruct v; try (exfalso; exact h_v). + destruct l; try (exfalso; exact h_v). + auto. + } + exists τ. + simp type_interp. + eexists; eexists; split; last split; first reflexivity. + - simp type_interp. + (* Quickly prove that 0 ∈ V[τ] *) + eexists; eexists; split; first reflexivity. + split. + simp type_interp; simpl. + exists 0; eauto. + + (* Prove that (λ: "z", 2 + "z") ∈ V[τ → τ] *) + simp type_interp. + eexists; eexists; split; last split; first reflexivity. + eauto. + (* Intro a value z *) + intros z z_tau. + (* Invert z using z_tau *) + simp type_interp in z_tau; simpl in z_tau. + destruct z; try (exfalso; exact z_tau). + destruct l; try (exfalso; exact z_tau). + + simp type_interp; exists (LitV (2+n)%Z); simpl; split. + econstructor; try econstructor. + + (* Prove that 2+n ∈ V[τ] *) + simp type_interp; simpl. + destruct z_tau as [x z_tau]. + exists (x+1)%Z. + rewrite <-z_tau. + lia. + - simp type_interp. + (* Small detour to prove closedness *) + have even_dec_closed: is_closed [] even_dec. + { + apply (syn_typed_closed 0 ∅ _ _ _ (even_dec_typed 0 ∅)). + intros x falsity; exfalso. + rewrite dom_empty in falsity. + rewrite elem_of_empty in falsity. + exact falsity. + } + eexists; eexists; split; last split; first reflexivity. + { + unfold is_closed; simpl; fold is_closed. + repeat rewrite andb_True; repeat split; eauto. + apply is_closed_weaken_nil. + assumption. + } + intros z z_tau. + (* We know that z = 2*z' *) + simp type_interp in *. + simpl in z_tau. + destruct z; try (exfalso; exact z_tau). + destruct l; try (exfalso; exact z_tau). + exists (LitV (LitInt n)). + split. + (* z ∈ V[τ], from our hypothesis *) + 2: simp type_interp; eexists; reflexivity. + simpl. + rewrite (subst_is_closed_nil _ _ _ even_dec_closed). + bs_step_det. + (* Finally, we need to prove that `if (even_dec n) then () else kaboom` steps to the correct value. *) + econstructor. + destruct z_tau as [x z_tau]. + rewrite <-z_tau. + (* We assume that `big_step (even_dec x) true` if `x = 2*x'` *) + exact (even_dec_correct x). + econstructor. +Qed. End ex4. (** ** Exercise 5 (LN Exercise 31): Abstract sums *) Section ex5. Import logrel existential_invariants. + Definition sum_ex_type (A B : type) : type := ∃: ((A.[ren (+1)] → #0) × (B.[ren (+1)] → #0) × @@ -130,11 +277,202 @@ Definition sum_ex_impl : val := Λ, λ: "x" "f1" "f2", if: Fst "x" = #1 then "f1" (Snd "x") else "f2" (Snd "x") ). +Ltac ℰ_to_𝒱 := simp type_interp; eexists; split; first (simpl; econstructor). +Ltac 𝒱_λ := simp type_interp; eexists; eexists; split; first reflexivity; split; first eauto. + +Lemma ren_2 A : A.[ren (+2)] = A.[ren (+1)].[ren (+1)]. +Proof. + (* Autosubst is not part of the curriculum, so I don't see why I should have to prove this. *) + admit. +Admitted. + Lemma sum_ex_safe A B δ: 𝒱 (sum_ex_type A B) δ sum_ex_impl. Proof. - (* TODO: exercise *) -Admitted. + unfold sum_ex_type. + simp type_interp. + eexists; split; first reflexivity. + (* + To prove that `sum_ex_impl ∈ 𝒱[∃α, ...]`, we pick a subset τ of SemType such that it models + the invariants of our representation. Namely, let `τ = {1} × 𝒱[A] ∪ {2} × 𝒱[B]`. + *) + remember (λ v, + match v with + | PairV (LitV (LitInt 1)) w => 𝒱 A δ w + | PairV (LitV (LitInt 2)) w => 𝒱 B δ w + | _ => False + end + ) as τ_λ. + + have inv_τ: ∀ v, τ_λ v → ∃ v', + v = (PairV (LitV (LitInt 1)) v') ∧ 𝒱 A δ v' + ∨ v = (PairV (LitV (LitInt 2)) v') ∧ 𝒱 B δ v'. + { + intros v v_in_τ. + (* There is currently no way to automate this away, thanks to Coq's advantage of being 30-years old *) + rewrite Heqτ_λ in v_in_τ. + + destruct v; try (exfalso; exact v_in_τ). + destruct v1; try (exfalso; exact v_in_τ). + destruct l; try (exfalso; exact v_in_τ). + destruct n; try (exfalso; exact v_in_τ). + destruct p; try (exfalso; exact v_in_τ). + destruct p; try (exfalso; exact v_in_τ). + - exists v2; right. + split; [reflexivity | assumption]. + - exists v2; left. + split; [reflexivity | assumption]. + } + + pose_sem_type τ_λ as τ. + { + intros v v_in_τ. + destruct (inv_τ v v_in_τ) as [v2 [(-> & v2_log) | (-> & v2_log)]]. + all: simpl. + all: eapply val_rel_closed; exact v2_log. + } + exists τ. + (* Split the triple into its constitutants *) + simp type_interp; eexists; eexists; split; first reflexivity; split. + simp type_interp; eexists; eexists; split; first reflexivity; split. + - (* Prove that λx. (1, x) ∈ 𝒱[A → τ]*) + 𝒱_λ. + (* Closedness detour *) + eauto. + intros v v_in_A. + simp type_interp; eexists; split. + simpl. + (* We know that (1, v) steps to (1, v) *) + econstructor; (econstructor || apply big_step_of_val; reflexivity). + + simp type_interp; simpl. + (* From our choice of τ_λ, (1, v) ∈ τ <-> v ∈ 𝒱[A]·δ *) + rewrite Heqτ_λ. + rewrite sem_val_rel_cons. + exact v_in_A. + - (* Prove that λx. (2, x) ∈ 𝒱[B → τ]*) + 𝒱_λ. + eauto. + intros v v_in_B. + simp type_interp; eexists; split. + simpl. + (* We know that (2, v) steps to (2, v) *) + econstructor; (econstructor || apply big_step_of_val; reflexivity). + + simp type_interp; simpl. + rewrite Heqτ_λ. + rewrite sem_val_rel_cons. + exact v_in_B. + - (* Prove that our match is in `∀α, τ → (A → α) → (B → β) → β` *) + simp type_interp. + eexists; split; first reflexivity; split. + eauto. + + intro τ₂. + (* Given an arbitrary τ₂, show that match ∈ 𝒱[τ → (A → τ₂) → (B → τ₂) → τ] *) + ℰ_to_𝒱. + 𝒱_λ. + (* We thus have to prove that for v ∈ τ, the rest works *) + intros v v_in_τ. + + simp type_interp in v_in_τ; simpl in v_in_τ. + simpl. + ℰ_to_𝒱. + 𝒱_λ. + { + (* Closedness detour *) + have h_cl : is_closed [] (of_val v). + destruct (inv_τ v v_in_τ) as [v2 [(-> & v2_log) | (-> & v2_log)]]. + all: eauto. + simplify_closed. + } + intros v₁ v₁_in_Afn. + ℰ_to_𝒱. + 𝒱_λ. + { + (* Closedness detour, the detouring *) + have h_cl : is_closed [] (of_val v). + destruct (inv_τ v v_in_τ) as [v2 [(-> & v2_log) | (-> & v2_log)]]. + all: eauto. + simplify_closed. + apply is_closed_weaken_nil. + eapply val_rel_closed. + exact v₁_in_Afn. + } + intros v₂ v₂_in_Bfn. + have v₁_cl : is_closed [] v₁. + { + eapply val_rel_closed. + exact v₁_in_Afn. + } + have v₂_cl : is_closed [] v₂. + { + eapply val_rel_closed. + exact v₂_in_Bfn. + } + + (* Remove all the noisy substs *) + simpl. + repeat rewrite (lang.subst_is_closed []); eauto. + all: try set_solver. + + (* By cases on the values that v can take *) + destruct (inv_τ v v_in_τ) as [v' [(-> & v'_log) | (-> & v'_log)]]. + + (* If v = (1, v') *) + have v'_in_A' : 𝒱 A.[ren (+2)] (τ₂ .: τ .: δ) v'. + { + rewrite ren_2. + rewrite <-sem_val_rel_cons. + rewrite <-sem_val_rel_cons. + exact v'_log. + } + (* We can deduce from v₁ ∈ 𝒱[A -> τ] that when given a parameter (v') in τ, it will step to a value in τ₂ *) + simp type_interp in v₁_in_Afn. + destruct v₁_in_Afn as (x₁ & e' & -> & e₁_cl & v₁_ty). + specialize (v₁_ty v' v'_in_A'). + simp type_interp in v₁_ty. + destruct v₁_ty as [v₁' [v₁_bs v₁'_ty]]. + + simp type_interp. + eexists; split. + (* We can see that our if-expression steps to (v₁ v') *) + bs_step_det. + eapply bs_if_true. + bs_step_det. + econstructor. + apply big_step_of_val; reflexivity. + bs_step_det. + (* So we can use the information from v₁ ∈ 𝒱[A -> τ] to finish the proof *) + exact v₁_bs. + exact v₁'_ty. + + (* If v = (2, v'), we do the same thing, but with B *) + have v'_in_B' : 𝒱 B.[ren (+2)] (τ₂ .: τ .: δ) v'. + { + rewrite ren_2. + rewrite <-sem_val_rel_cons. + rewrite <-sem_val_rel_cons. + exact v'_log. + } + (* We can deduce from v₁ ∈ 𝒱[A -> τ] that when given a parameter (v') in τ, it will step to a value in τ₂ *) + simp type_interp in v₂_in_Bfn. + destruct v₂_in_Bfn as (x₂ & e' & -> & e₁_cl & v₂_ty). + specialize (v₂_ty v' v'_in_B'). + simp type_interp in v₂_ty. + destruct v₂_ty as [v₂' [v₂_bs v₂'_ty]]. + + simp type_interp. + eexists; split. + (* We can see that our if-expression steps to (v₂ v') *) + bs_step_det. + eapply bs_if_false. + bs_step_det. + econstructor. + apply big_step_of_val; reflexivity. + bs_step_det. + (* So we can use the information from v₂ ∈ 𝒱[A -> τ] to finish the proof *) + exact v₂_bs. + exact v₂'_ty. +Qed. End ex5. @@ -159,11 +497,278 @@ Proof. all: asimpl; solve_typing. Qed. +Ltac 𝒱2_λ := simp type_interp; eexists; eexists; eexists; eexists; + split; last split; last split; last split; + [ reflexivity | reflexivity | simplify_closed | simplify_closed | ] +. + +Ltac 𝒱2_inner := + simp type_interp; eexists; eexists; split; last split; simpl; + [ try bs_step_det | try bs_step_det | ] +. + +(* +I consider this to be an example of bad pedagogy. +This is more of a challenge than an exercise; I didn't learn anything proving this, +and all it brought to me was a net loss in energy and a lot of frustration. + +This is the kind of theorem that should be proven automatically, +and we have constructed in class the tools needed to implement such a prover, +we just chose not to make one and to instead spearhead our way into proving this kind of stuff, +by hand. + +The `destruct` forests, the stacked `split`s, the `eexists` spam are witnesses that proving this is a bad idea, and that asking students to prove this is a bad idea. +I spent 30 seconds writing the definition of τ, and 1 hour proving the rest of the theorem. +*) Lemma sum_ex_impl_equiv n Γ A B : ctx_equiv n Γ sum_ex_impl' sum_ex_impl (sum_ex_type A B). Proof. - (* TODO: exercise *) -Admitted. + (* + To prove that sum_ex_impl' ===_ctx sum_ex_impl, + we can prove that n; Γ |= sum_ex_impl ~ sum_ex_impl' : SUM(A, B) + *) + apply sem_typing_ctx_equiv. + simplify_closed. + simplify_closed. + + split; last split. + simplify_closed. + simplify_closed. + intros θ1 θ2 δ Hctx. + + destruct (sem_context_rel_closed _ _ _ _ Hctx) as [Hcl1 Hcl2]. + simp type_interp. + eexists; eexists; split; last split. + bs_step_det. + bs_step_det. + (* Clean up our expression *) + repeat rewrite lookup_delete. + have h₁ : delete "f2" (delete "f1" (delete "x" θ1)) !! "x" = None. + { + rewrite lookup_delete_ne. + rewrite lookup_delete_ne. + apply lookup_delete. + eauto. + eauto. + } + rewrite h₁. + have h₂ : delete "f2" (delete "f1" (delete "x" θ2)) !! "x" = None. + { + rewrite lookup_delete_ne. + rewrite lookup_delete_ne. + apply lookup_delete. + eauto. + eauto. + } + rewrite h₂. + have h₃ : delete "f2" (delete "f1" (delete "x" θ1)) !! "f1" = None. + { + rewrite lookup_delete_ne. + apply lookup_delete. + eauto. + } + rewrite h₃. + have h₄ : delete "f2" (delete "f1" (delete "x" θ2)) !! "f1" = None. + { + rewrite lookup_delete_ne. + apply lookup_delete. + eauto. + } + rewrite h₄. + + unfold sum_ex_type. + simp type_interp; eexists; eexists; split; first reflexivity; split; first reflexivity. + + remember (λ v1 v2, match v1, v2 with + | (InjLV x), (PairV (LitV (LitInt 1)) y) => 𝒱 A δ x y + | (InjRV x), (PairV (LitV (LitInt 2)) y) => 𝒱 B δ x y + | _, _ => False + end + ) as τ_λ. + + (* Please look away *) + have inv_τ : ∀ v1 v2, τ_λ v1 v2 → ∃ x y, + ( + v1 = (InjLV x) + ∧ v2 = (PairV (LitV (LitInt 1)) y) + ∧ 𝒱 A δ x y + ) + ∨ ( + v1 = (InjRV x) + ∧ v2 = (PairV (LitV (LitInt 2)) y) + ∧ 𝒱 B δ x y + ). + { + intros v1 v2 v_in_τ. + rewrite Heqτ_λ in v_in_τ. + + destruct v1; try (exfalso; exact v_in_τ). + { + destruct v2; try (exfalso; exact v_in_τ). + destruct v2_1; try (exfalso; exact v_in_τ). + destruct l; try (exfalso; exact v_in_τ). + destruct n0; try (exfalso; exact v_in_τ). + destruct p; try (exfalso; exact v_in_τ). + eexists; eexists. + left. + split; last split. + reflexivity. + reflexivity. + assumption. + } + { + destruct v2; try (exfalso; exact v_in_τ). + destruct v2_1; try (exfalso; exact v_in_τ). + destruct l; try (exfalso; exact v_in_τ). + destruct n0; try (exfalso; exact v_in_τ). + destruct p; try (exfalso; exact v_in_τ). + destruct p; try (exfalso; exact v_in_τ). + eexists; eexists. + right. + split; last split. + reflexivity. + reflexivity. + assumption. + } + } + + pose_sem_type τ_λ as τ. + { + intros v w vw_in_τ. + destruct (inv_τ v w vw_in_τ) as (v' & w' & [(-> & -> & He) | (-> & -> & He)]). + simplify_closed. + destruct (val_rel_is_closed _ _ _ _ He) as [Hcl3 Hcl4]. + split; assumption. + simplify_closed. + destruct (val_rel_is_closed _ _ _ _ He) as [Hcl3 Hcl4]. + split; assumption. + } + + exists τ. + + simp type_interp; eexists; eexists; eexists; eexists; split; first reflexivity; split; first reflexivity; split. + simp type_interp; eexists; eexists; eexists; eexists; split; first reflexivity; split; first reflexivity; split. + + - 𝒱2_λ. + intros v w vw_in_τ. + 𝒱2_inner. + simp type_interp. + simpl. + rewrite Heqτ_λ. + rewrite <-sem_val_rel_cons in vw_in_τ. + assumption. + - 𝒱2_λ. + intros v w vw_in_τ. + 𝒱2_inner. + simp type_interp. + simpl. + rewrite Heqτ_λ. + rewrite <-sem_val_rel_cons in vw_in_τ. + assumption. + - simp type_interp. + eexists; eexists; split; last split; last split; last split; [reflexivity | reflexivity | simplify_closed | simplify_closed | ]. + intro τ₂. + simp type_interp; eexists; eexists; split; last split; [bs_step_det | bs_step_det | ]. + 𝒱2_λ. + intros v w vw_in_τ. + 𝒱2_inner. + destruct (val_rel_is_closed _ _ _ _ vw_in_τ) as [Hcl3 Hcl4]. + simp type_interp in vw_in_τ; simpl in vw_in_τ. + + 𝒱2_λ. + intros f1 f1' f1_in_τ₂. + 𝒱2_inner. + destruct (val_rel_is_closed _ _ _ _ f1_in_τ₂) as [Hcl5 Hcl6]. + + 𝒱2_λ. + intros f2 f2' f2_in_τ₂. + + destruct (inv_τ v w vw_in_τ) as (v' & w' & [(-> & -> & He) | (-> & -> & He)]); + destruct (val_rel_is_closed _ _ _ _ He) as [Hcl9 Hcl10]; + destruct (val_rel_is_closed _ _ _ _ f2_in_τ₂) as [Hcl7 Hcl8]. + + + repeat rewrite subst_is_closed_nil; try assumption. + simp type_interp in f1_in_τ₂. + destruct f1_in_τ₂ as (x1 & x1' & f1_body & f1'_body & Heq_f1body & Heq_f1'body & Hcl11 & Hcl12 & Hlog). + + have HA: 𝒱 A.[ren (+2)] (τ₂ .: τ .: δ) v' w'. + { + rewrite ren_2. + rewrite <-sem_val_rel_cons. + rewrite <-sem_val_rel_cons. + assumption. + } + specialize (Hlog v' w' HA). + simp type_interp in Hlog. + destruct Hlog as (v1 & v1' & Hbs & Hbs' & Hlog). + + simp type_interp. + exists v1. + exists v1'. + split; last split. + simpl. + repeat (rewrite subst_is_closed_nil; last assumption). + + econstructor. + econstructor; apply big_step_of_val; reflexivity. + econstructor; try (apply big_step_of_val; reflexivity). + apply big_step_of_val. rewrite Heq_f1body; reflexivity. + assumption. + + simpl. + repeat (rewrite subst_is_closed_nil; last assumption). + + econstructor. + bs_step_det. + econstructor. + apply big_step_of_val. rewrite Heq_f1'body; reflexivity. + bs_step_det. + assumption. + + assumption. + + repeat rewrite subst_is_closed_nil; try assumption. + simp type_interp in f2_in_τ₂. + destruct f2_in_τ₂ as (x2 & x2' & f2_body & f2'_body & Heq_f2body & Heq_f2'body & Hcl11 & Hcl12 & Hlog). + + have HB: 𝒱 B.[ren (+2)] (τ₂ .: τ .: δ) v' w'. + { + rewrite ren_2. + rewrite <-sem_val_rel_cons. + rewrite <-sem_val_rel_cons. + assumption. + } + specialize (Hlog v' w' HB). + simp type_interp in Hlog. + destruct Hlog as (v2 & v2' & Hbs & Hbs' & Hlog). + + + simp type_interp. + exists v2. + exists v2'. + split; last split. + simpl. + repeat (rewrite subst_is_closed_nil; last assumption). + + + eapply bs_caser. + + econstructor; apply big_step_of_val; reflexivity. + econstructor; try (apply big_step_of_val; reflexivity). + apply big_step_of_val. rewrite Heq_f2body; reflexivity. + assumption. + + simpl. + repeat (rewrite subst_is_closed_nil; last assumption). + + eapply bs_if_false. + bs_step_det. + econstructor. + apply big_step_of_val. rewrite Heq_f2'body; reflexivity. + bs_step_det. + assumption. + + assumption. +Qed. End ex8. diff --git a/theories/type_systems/systemf/types.v b/theories/type_systems/systemf/types.v index a8c46fd..2373af5 100644 --- a/theories/type_systems/systemf/types.v +++ b/theories/type_systems/systemf/types.v @@ -613,11 +613,25 @@ Proof. eexists. eapply base_contextual_step. eapply TBetaS. + destruct H1 as [e' H1]. eexists. eauto. - (* pack *) - (* TODO this will be an exercise for you soon :) *) - admit. - - (* unpack *) - (* TODO this will be an exercise for you soon :) *) - admit. + (* For pack, we know that `pack e` is a value if `e` is a value; if `e` steps to `e'`, then `pack e` steps to `pack e'`. *) + unfold is_val; fold is_val. + destruct (IH HeqΓ Heqn) as [e_is_val | [e' Hcstep]]. + left; assumption. + right. + eexists; apply (fill_contextual_step (PackCtx HoleCtx) e e'); assumption. + - (* unpack e as x in e' *) + (* If e is a value, then we apply the base contextual rule for unpacking a packed value. Otherwise, unpack steps through the UnpackCtx contextual step. *) + destruct (IH1 HeqΓ Heqn) as [e_is_val | [e₂ Hcstep]]. + + eapply canonical_values_exists in Hty1 as [e₃ ->]; last exact e_is_val. + right. + eexists; eapply base_contextual_step. + econstructor. + unfold is_val in e_is_val; fold is_val in e_is_val. + exact e_is_val. + reflexivity. + + right. + eexists; eapply (fill_contextual_step (UnpackCtx _ HoleCtx _)). + exact Hcstep. - (* int *)left. done. - (* bool*) left. done. - (* unit *) left. done. @@ -685,8 +699,7 @@ Proof. * eexists. eapply base_contextual_step. econstructor. done. * eexists. eapply base_contextual_step. econstructor. done. + destruct H1 as [e' H1]. eexists. eauto. -(*Qed.*) -Admitted. +Qed.