Commit 2bb70c42 by Lennard Gäher

### solutions

parent ceb39ea6
 ... ... @@ -49,6 +49,10 @@ theories/systemf/free_theorems.v theories/systemf/binary_logrel.v theories/systemf/existential_invariants.v theories/systemf/logrel_sol.v theories/systemf/binary_logrel_sol.v theories/systemf/types_sol.v # SystemF-Mu theories/systemf_mu/lang.v theories/systemf_mu/notation.v ... ... @@ -76,3 +80,5 @@ theories/systemf_mu/untyped_encoding.v #theories/systemf/exercices04.v #theories/systemf/exercises04_sol.v #theories/systemf/exercises05.v #theories/systemf/exercises05_sol.v #theories/systemf/exercises06.v
This diff is collapsed.
 From stdpp Require Import gmap base relations. From iris Require Import prelude. From semantics.systemf_sol Require Import lang notation parallel_subst types tactics. From semantics.systemf_sol Require existential_invariants logrel binary_logrel. (** * Exercise Sheet 5 *) Implicit Types (e : expr) (v : val) (A B : type) . (** ** Exercise 3: Existential Fun *) Section existential. (** Since extending our language with records would be tedious, we encode records using nested pairs. For instance, we would represent the record type { add : Int → Int → Int; sub : Int → Int → Int; neg : Int → Int } as (Int → Int → Int) × (Int → Int → Int) × (Int → Int). Similarly, we would represent the record value { add := λ: "x" "y", "x" + "y"; sub := λ: "x" "y", "x" - "y"; neg := λ: "x", #0 - "x" } as the nested pair ((λ: "x" "y", "x" + "y", (* add *) λ: "x" "y", "x" - "y"), (* sub *) λ: "x", #0 - "x"). (* neg *) *) (** We will also assume a recursion combinator. We have not formally added it to our language, but we could do so. *) Context (Fix : string → string → expr → val). Notation "'fix:' f x := e" := (Fix f x e)%E (at level 200, f, x at level 1, e at level 200, format "'[' 'fix:' f x := '/ ' e ']'") : val_scope. Notation "'fix:' f x := e" := (Fix f x e)%E (at level 200, f, x at level 1, e at level 200, format "'[' 'fix:' f x := '/ ' e ']'") : expr_scope. Context (fix_typing : ∀ n Γ (f x: string) (A B: type) (e: expr), type_wf n A → type_wf n B → f ≠ x → TY n; <[x := A]> (<[f := (A → B)%ty]> Γ) ⊢ e : B → TY n; Γ ⊢ (fix: f x := e) : (A → B)). Definition ISET : type := ∃: (#0 (* empty *) × (Int → #0) (* singleton *) × (#0 → #0 → #0) (* union *) × (#0 → #0 → Bool) (* subset *) ). (* We represent sets as functions of type ((Int → Bool) × Int × Int), storing the mapping, the minimum value, and the maximum value. *) Definition mini : val := λ: "x" "y", if: "x" < "y" then "x" else "y". Definition maxi : val := λ: "x" "y", if: "x" < "y" then "x" else "y". Definition iterupiv : val := λ: "f" "max", fix: "rec" "acc" := let: "i" := Fst "acc" in let: "b" := Snd "acc" in if: "max" < "i" then "b" else "rec" ("i" + #1, "f" "i" "b"). Definition iterupv : val := λ: "f" "init" "min" "max", iterupiv "f" "max" ("min", "init"). Lemma iterupv_typed n Γ : TY n; Γ ⊢ iterupv : ((Int → Bool → Bool) → Bool → Int → Int → Bool). Proof. repeat solve_typing. apply fix_typing; solve_typing. done. Qed. Definition iset : val := pack (((λ: "x", #false), #0, #0), (* empty *) (λ: "n", ((λ: "x", "n" = "x"), "n", "n")), (* singleton *) (* union *) (λ: "s1" "s2", ((λ: "x", if: (Fst \$ Fst "s1") "x" then #true else (Fst \$ Fst "s2") "x"), mini (Snd \$ Fst "s1") (Snd \$ Fst "s1"), maxi (Snd "s1") (Snd "s1"))), (* subset *) (λ: "s1" "s2", let: "min" := Snd \$ Fst "s1" in let: "max" := Snd \$ "s1" in (* iteration variable is set to #false if we detect a subset violation *) iterupv (λ: "i" "acc", if: (Fst \$ Fst "s2") "i" then "acc" else #false) #true "min" "max" )). Lemma iset_typed n Γ : TY n; Γ ⊢ iset : ISET. Proof. unfold iset. repeat solve_typing. apply fix_typing; solve_typing. done. Qed. Definition ISETE : type := ∃: (#0 (* empty *) × (Int → #0) (* singleton *) × (#0 → #0 → #0) (* union *) × (#0 → #0 → Bool) (* subset *) × (#0 → #0 → Bool) (* equality *) ). Definition add_equality : val := λ: "is", unpack "is" as "isi" in let: "subset" := Snd "isi" in pack ("isi", λ: "s1" "s2", if: "subset" "s1" "s2" then "subset" "s2" "s1" else #false). Lemma add_equality_typed n Γ : TY n; Γ ⊢ add_equality : (ISET → ISETE)%ty. Proof. repeat solve_typing. Qed. End existential. Section ex4. Import logrel existential_invariants. (** ** Exercise 4: Evenness *) (* Consider the following existential type: *) Definition even_type : type := ∃: (#0 × (* zero *) (#0 → #0) × (* add2 *) (#0 → Int) (* toint *) )%ty. (* and consider the following implementation of [even_type]: *) Definition even_impl : val := pack (#0, λ: "z", #2 + "z", λ: "z", "z" ). (* We want to prove that [toint] will only every yield even numbers. *) (* For that purpose, assume that we have a function [even] that decides even parity available: *) Context (even_dec : val). Context (even_dec_typed : ∀ n Γ, TY n; Γ ⊢ even_dec : (Int → Bool)). (* a) Change [even_impl] to [even_impl_instrumented] such that [toint] asserts evenness of the argument before returned. You may use the [assert] expression. *) Definition even_impl_instrumented : val := pack (#0, λ: "z", #2 + "z", λ: "z", assert (even_dec "z");; "z" ). (* b) Prove that [even_impl_instrumented] is safe. You may assume that even works as intended. *) Context (even_spec : ∀ z: Z, big_step (even_dec #z) #(Z.even z)). Context (even_closed : is_closed [] even_dec). Lemma even_impl_instrumented_safe δ: 𝒱 even_type δ even_impl_instrumented. Proof. unfold even_type. simp type_interp. eexists _. split; first done. pose_sem_type (λ v, ∃ z : Z, Z.Even z ∧ v = #z) as τ. { intros v (z & ? & ->). done. } exists τ. simp type_interp. eexists _, _. split_and!; first done. - simp type_interp. eexists _, _. split_and!; first done. + simp type_interp. simpl. exists 0. split; last done. apply Z.even_spec. done. + simp type_interp. eexists _, _. split_and!; [done | done | ]. intros v. simp type_interp. simpl. intros (z & Heven & ->). exists #(2 + z)%Z. split; first bs_step_det. simp type_interp. simpl. exists (2 + z)%Z. split; last done. destruct Heven as (z' & ->). exists (z' + 1)%Z. lia. - simp type_interp. eexists _, _. split_and!; [done | | ]. { simpl. rewrite !andb_True. split_and!;[ | done..]. eapply is_closed_weaken; first done. apply list_subseteq_nil. } intros v'. simp type_interp. simpl. intros (z & Heven & ->). exists #z. split. + bs_step_det. eapply bs_if_true; last bs_step_det. replace true with (Z.even z); first by eapply even_spec. by apply Z.even_spec. + simp type_interp. exists z. done. Qed. End ex4. (** ** Exercise 5: Abstract sums *) Section ex5. Import logrel. Definition sum_ex_type (A B : type) : type := ∃: ((A.[ren (+1)] → #0) × (B.[ren (+1)] → #0) × (∀: #1 → (A.[ren (+2)] → #0) → (B.[ren (+2)] → #0) → #0) )%ty. Definition sum_ex_impl : val := pack (λ: "x", (#1, "x"), λ: "x", (#2, "x"), Λ, λ: "x" "f1" "f2", if: Fst "x" = #1 then "f1" (Snd "x") else "f2" (Snd "x") ). Lemma sum_ex_safe A B δ: 𝒱 (sum_ex_type A B) δ sum_ex_impl. Proof. intros. unfold sum_ex_type. simp type_interp. eexists _. split; first done. pose_sem_type (λ v, (∃ v', 𝒱 A δ v' ∧ v = (#1, v')%V) ∨ (∃ v', 𝒱 B δ v' ∧ v = (#2, v')%V)) as τ. { intros v [(v' & Hv & ->) | (v' & Hv & ->)]; simpl; by eapply val_rel_is_closed. } exists τ. simp type_interp. eexists _, _. split; first done. split. 1: simp type_interp; eexists _, _; split; first done; split. - simp type_interp. eexists _, _. split_and!; [done..|]. intros v' Hv'. simp type_interp. simpl. eexists. split; first bs_step_det. simp type_interp. simpl. left. eexists; split; last done. eapply sem_val_rel_cons; done. - simp type_interp. eexists _, _. split_and!; [done..|]. intros v' Hv'. simp type_interp. simpl. eexists. split; first bs_step_det. simp type_interp. simpl. right. eexists; split; last done. eapply sem_val_rel_cons; done. - simp type_interp. eexists _. split_and!; [done..|]. intros τ'. simp type_interp. eexists. split; first bs_step_det. simp type_interp. eexists _, _; split_and!; [done..|]. intros v'. simp type_interp. simpl. intros [(v & Hv & ->) | (v & Hv & ->)]. + eexists. split; first bs_step_det. specialize (val_rel_is_closed _ _ _ Hv) as ?. simp type_interp. eexists _, _; split_and!; [done| simplify_closed | ]. intros v'. simp type_interp. intros (? & ? & -> & ? & Hv'). specialize (Hv' v). simp type_interp in Hv'. destruct Hv' as (? & ? & Hv'). { revert Hv. rewrite sem_val_rel_cons. rewrite sem_val_rel_cons. asimpl. done. } eexists _. split; first bs_step_det. simp type_interp. eexists _, _. split_and!; [done| simplify_closed | ]. intros v'. simp type_interp. intros (? & ? & -> & ? & _). eexists _. split. { bs_step_det. eapply bs_if_true; bs_step_det. case_decide; bs_step_det. erewrite lang.subst_is_closed; bs_step_det. destruct x; simpl; simplify_closed. } simp type_interp. simpl. simp type_interp in Hv'. + eexists. split; first bs_step_det. specialize (val_rel_is_closed _ _ _ Hv) as ?. simp type_interp. eexists _, _; split_and!; [done| simplify_closed | ]. intros v'. simp type_interp. intros (? & ? & -> & ? & _). eexists _. split; first bs_step_det. simp type_interp. eexists _, _. split_and!; [done| simplify_closed | ]. intros v'. simp type_interp. intros (? & ? & -> & ? & Hv'). specialize (Hv' v). simp type_interp in Hv'. destruct Hv' as (? & ? & Hv'). { revert Hv. rewrite sem_val_rel_cons. rewrite sem_val_rel_cons. asimpl. done. } eexists _. split. { bs_step_det. eapply bs_if_false; bs_step_det. } simp type_interp. simpl. simp type_interp in Hv'. Qed. End ex5. (** ** Exercise 8: Contextual equivalence *) Section ex8. Import binary_logrel. Definition sum_ex_impl' : val := pack ((λ: "x", InjL "x"), (λ: "x", InjR "x"), (Λ, λ: "x" "f1" "f2", Case "x" "f1" "f2") ). Lemma sum_ex_impl'_typed n Γ A B : type_wf n A → type_wf n B → TY n; Γ ⊢ sum_ex_impl' : sum_ex_type A B. Proof. intros. eapply (typed_pack _ _ _ (A + B)%ty). all: asimpl; solve_typing. Qed. Lemma sum_ex_impl_equiv n Γ A B : ctx_equiv n Γ sum_ex_impl' sum_ex_impl (sum_ex_type A B). Proof. intros. eapply sem_typing_ctx_equiv; [done | done | ]. intros θ1 θ2 δ Hctx. rewrite (subst_map_is_closed []); [ | done | intros; simplify_list_elem ]. rewrite (subst_map_is_closed []); [ | done | intros; simplify_list_elem ]. simp type_interp. eexists _, _. split_and!; [bs_step_det.. | ]. unfold sum_ex_type. simp type_interp. eexists _, _; split_and!; [ done | done | ]. pose_sem_type (λ v1 v2, (∃ v w : val, 𝒱 A δ v w ∧ v1 = InjLV v ∧ v2 = (#1, w)%V) ∨ (∃ v w: val, 𝒱 B δ v w ∧ v1 = InjRV v ∧ v2 = (#2, w)%V)) as R. { intros ?? [(? & ? & []%val_rel_is_closed & -> & ->) | (? & ? & []%val_rel_is_closed & -> & ->)]; done. } exists R. simp type_interp. eexists _, _, _, _. split; first done. split; first done. split. - simp type_interp. eexists _, _, _, _. split_and!; [done | done | | ]. + simp type_interp. eexists _, _, _, _. split_and!; [done | done | done | done | ]. intros v' w' ?%sem_val_rel_cons. simp type_interp. simpl. eexists _, _. split_and!; [bs_steps_det | bs_steps_det | ]. simp type_interp. simpl. left; eauto. + simp type_interp. eexists _, _, _, _. split_and!; [done | done | done | done | ]. intros v' w' ?%sem_val_rel_cons. simp type_interp. simpl. eexists _, _. split_and!; [bs_steps_det | bs_steps_det | ]. simp type_interp. simpl. right; eauto. - simp type_interp. eexists _, _. split_and!; [done | done | done | done | ]. intros R'. simp type_interp. eexists _, _. split_and!; [bs_steps_det | bs_steps_det | ]. simp type_interp. eexists _, _, _, _. split_and!; [ done | done | done | done | ]. intros v' w'. simp type_interp. simpl. intros Hsum. assert (is_closed [] v' ∧ is_closed [] w') as [Hclv' Hclw']. { destruct Hsum as [(? & ? & []%val_rel_is_closed & -> & ->) | (? & ? & []%val_rel_is_closed & -> & ->)]; done. } eexists _, _. split_and!; [bs_steps_det | bs_steps_det | ]. simp type_interp. eexists _, _, _, _. split_and!; [ done | done | simplify_closed | simplify_closed | ]. intros f f' Hf. simpl. repeat (rewrite subst_is_closed_nil; [ | done]). simp type_interp. eexists _, _. split_and!; [ bs_steps_det | bs_steps_det | ]. simp type_interp. eexists _, _, _, _. specialize (val_rel_is_closed _ _ _ _ Hf) as []. split_and!; [done | done | simplify_closed | simplify_closed | ]. intros g g' Hg. simpl. repeat (rewrite subst_is_closed_nil; [ | done]). (* CA *) destruct Hsum as [(v & w & Hvw & -> & ->) | (v & w & Hvw & -> & ->)]. + simpl; simp type_interp. simp type_interp in Hf. destruct Hf as (? & ? & ? & ? & -> & -> & ? & ? & Hf). feed pose proof (Hf v w) as Hf. { revert Hvw. rewrite sem_val_rel_cons. rewrite sem_val_rel_cons. asimpl. done. } simp type_interp in Hf. destruct Hf as (v1 & v2 & ? & ? & Hf). simp type_interp in Hf. simpl in Hf. eexists _, _. split_and!. { eapply bs_casel; bs_step_det. } { eapply bs_if_true; bs_step_det. } done. + simpl; simp type_interp. simp type_interp in Hg. destruct Hg as (? & ? & ? & ? & -> & -> & ? & ? & Hg). feed pose proof (Hg v w) as Hg. { revert Hvw. rewrite sem_val_rel_cons. rewrite sem_val_rel_cons. asimpl. done. } simp type_interp in Hg. destruct Hg as (v1 & v2 & ? & ? & Hg). simp type_interp in Hg. simpl in Hg. eexists _, _. split_and!. { eapply bs_caser; bs_step_det. } { eapply bs_if_false; bs_step_det. } done. Qed. End ex8.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!