Commit 915fbeaf by Lennard Gäher

### new stuff

parent 2bb70c42
 ... ... @@ -60,6 +60,9 @@ theories/systemf_mu/types.v theories/systemf_mu/tactics.v theories/systemf_mu/pure.v theories/systemf_mu/untyped_encoding.v theories/systemf_mu/parallel_subst.v theories/systemf_mu/logrel.v theories/systemf_mu/z_combinator.v ... ... @@ -81,4 +84,4 @@ theories/systemf_mu/untyped_encoding.v #theories/systemf/exercises04_sol.v #theories/systemf/exercises05.v #theories/systemf/exercises05_sol.v #theories/systemf/exercises06.v #theories/systemf_mu/exercises06.v
 From stdpp Require Import gmap base relations tactics. From iris Require Import prelude. From semantics.systemf_mu Require Import lang notation types pure tactics logrel. From Autosubst Require Import Autosubst. (** * Exercise Sheet 6 *) Notation sub := lang.subst. Implicit Types (e : expr) (v : val) (A B : type) . (** ** Exercise 5: Keep Rollin' *) (** This exercise is slightly tricky. We strongly recommend you to first work on the other exercises. You may use the results from this exercise, in particular the fixpoint combinator and its typing, in other exercises, however (which is why it comes first in this Coq file). *) Section recursion_combinator. Variable (f x: string). (* the template of the recursive function *) Hypothesis (Hfx: f ≠ x). (** Recursion Combinator *) (* First, setup a definition [Rec] satisfying the reduction lemmas below. *) (** You may find an auxiliary definition [rec_body] helpful *) Definition rec_body (t: expr) : expr := (* FIXME *) roll (λ: f x, #0). Definition Rec (t: expr): val := λ: x, rec_body t. (* FIXME *) Lemma closed_rec_body t : is_closed [] t → is_closed [] (rec_body t). Proof. simplify_closed. Qed. Lemma closed_Rec t : is_closed [] t → is_closed [] (Rec t). Proof. simplify_closed. Qed. Lemma is_val_Rec t: is_val (Rec t). Proof. done. Qed. Lemma Rec_red (t e: expr): is_val e → is_val t → is_closed [] e → is_closed [] t → rtc contextual_step ((Rec t) e) (t (Rec t) e). Proof. (* FIXME *) Admitted. Lemma rec_body_typing n Γ (A B: type) t : Γ !! x = None → Γ !! f = None → type_wf n A → type_wf n B → TY n; Γ ⊢ t : ((A → B) → (A → B)) → TY n; Γ ⊢ rec_body t : (μ: #0 → rename (+1) A → rename (+1) B). Proof. (* FIXME *) Admitted. Lemma Rec_typing n Γ A B t: type_wf n A → type_wf n B → Γ !! x = None → Γ !! f = None → TY n; Γ ⊢ t : ((A → B) → (A → B)) → TY n; Γ ⊢ (Rec t) : (A → B). Proof. (* FIXME *) Admitted. End recursion_combinator. Definition Fix (f x: string) (e: expr) : val := (Rec f x (Lam f%string (Lam x%string e))). (** We "seal" the definition to make it opaque to the [solve_typing] tactic. We do not want [solve_typing] to unfold the definition, instead, we should manually apply the typing rule below. You do not need to understand this in detail -- the only thing of relevance is that you can use the equality [Fix_eq] to unfold the definition of [Fix]. *) Definition Fix_aux : seal (Fix). Proof. by eexists. Qed. Definition Fix' := Fix_aux.(unseal). Lemma Fix_eq : Fix' = Fix. Proof. rewrite -Fix_aux.(seal_eq) //. Qed. Arguments Fix' _ _ _ : simpl never. (* the actual fixpoint combinator *) 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. Lemma fix_red (f x: string) (e e': expr): is_closed [x; f] e → is_closed [] e' → is_val e' → f ≠ x → rtc contextual_step ((fix: f x := e) e')%V (sub x e' (sub f (fix: f x := e)%V e)). Proof. (* FIXME *) Admitted. Lemma 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). Proof. (* FIXME *) Admitted. (** ** Exercise 1: Encode arithmetic expressions *) Definition aexpr : type := μ: (Int + (#0 × #0)) + (#0 × #0). Definition num_val (v : val) : val := RollV (InjLV \$ InjLV v). Definition num_expr (e : expr) : expr := Roll (InjL \$ InjL e). Definition plus_val (v1 v2 : val) : val := RollV (InjLV \$ InjRV (v1, v2)). Definition plus_expr (e1 e2 : expr) : expr := Roll (InjL \$ InjR (e1, e2)). Definition mul_val (v1 v2 : val) : val := RollV (InjRV (v1, v2)). Definition mul_expr (e1 e2 : expr) : expr := Roll (InjR (e1, e2)). Lemma num_expr_typed n Γ e : TY n; Γ ⊢ e : Int → TY n; Γ ⊢ num_expr e : aexpr. Proof. intros. solve_typing. Qed. Lemma plus_expr_typed n Γ e1 e2 : TY n; Γ ⊢ e1 : aexpr → TY n; Γ ⊢ e2 : aexpr → TY n; Γ ⊢ plus_expr e1 e2 : aexpr. Proof. intros; solve_typing. Qed. Lemma mul_expr_typed n Γ e1 e2 : TY n; Γ ⊢ e1 : aexpr → TY n; Γ ⊢ e2 : aexpr → TY n; Γ ⊢ mul_expr e1 e2 : aexpr. Proof. intros; solve_typing. Qed. Definition eval_aexpr : val := fix: "rec" "e" := match: unroll "e" with InjL "e'" => match: "e'" with InjL "n" => "n" | InjR "es" => "rec" (Fst "es") + "rec" (Snd "es") end | InjR "es" => "rec" (Fst "es") * "rec" (Snd "es") end. Lemma eval_aexpr_typed Γ n : TY n; Γ ⊢ eval_aexpr : (aexpr → Int). Proof. unfold eval_aexpr. apply fix_typing; solve_typing. done. Qed. (** Exercise 3: Lists *) Definition list_t (A : type) : type := ∃: (#0 (* mynil *) × (A.[ren (+1)] → #0 → #0) (* mycons *) × (∀: #1 → #0 → (A.[ren (+2)] → #1 → #0) → #0)) (* mylistcase *) . Definition mylist_impl : val := pack ((#0, #()), (* mynil *) (λ: "a" "l", (#1 + Fst "l", ("a", Snd "l"))), (* mycons *) (Λ, λ: "l" "n" "c", if: Fst "l" = #0 then "n" else "c" (Fst (Snd "l")) (Fst "l" - #1, Snd (Snd "l")))) (* mycase *) . Fixpoint represents_list_rec (l : list val) (v : val) := match l with | [] => v = #() | h :: l' => ∃ v' : val, v = (h, v')%V ∧ represents_list_rec l' v' end. Definition represents_list (l : list val) (v : val) := ∃ (n : Z) (v' : val), n = length l ∧ v = (#n, v')%V ∧ represents_list_rec l v'. Lemma mylist_impl_sem_typed A : type_wf 0 A → ∀ k, 𝒱 (list_t A) δ_any k mylist_impl. Proof. intros Hwf k. unfold list_t. simp type_interp. eexists _. split; first done. pose_sem_type (λ k' (v : val), ∃ l : list val, represents_list l v ∧ Forall (𝒱 A δ_any k') l) as τ. { intros k' v (l & Hrep & Hl). destruct Hrep as (n & v' & -> & -> & Hrep). simplify_closed. induction l as [ | h l IH] in v', Hrep, Hl |-*; simpl in Hrep. - rewrite Hrep. done. - destruct Hrep as (v'' & -> & Hrep). simplify_closed. + eapply Forall_inv in Hl. eapply val_rel_is_closed in Hl. done. + eapply IH; first done. eapply Forall_inv_tail in Hl. done. } { intros k' k'' v (l & Hrep & Hl) Hle. exists l. split; first done. eapply Forall_impl; first done. intros v'. by eapply val_rel_mono. } exists τ. simp type_interp. eexists _, _. split; first done. split; [ simp type_interp; eexists _, _; split; first done; split | ]. - simp type_interp. simpl. exists []. split; last done. eexists _, _; simpl; split; first done. done. - simp type_interp. eexists _, _. split; first done. split; first done. intros v2 kd Hv2. simpl. eapply (sem_val_expr_rel _ _ _ (LamV _ _)). simp type_interp. eexists _, _. split; first done. specialize (val_rel_is_closed _ _ _ _ Hv2) as ?. split; first by simplify_closed. intros v3 kd2 Hv3. simpl. rewrite subst_is_closed_nil; last done. simp type_interp in Hv3. destruct Hv3 as (l & (len & hv & -> & -> & Hv3) & Hl). simpl. eapply expr_det_steps_closure. { repeat do_det_step. constructor. } eapply (sem_val_expr_rel _ _ _ (PairV _ (PairV _ _))). simp type_interp. simpl. exists (v2 :: l). split. { simpl. eexists _, (v2, hv)%V. split; first done. simpl. split. { f_equal. f_equal. f_equal. lia. } eexists _; done. } econstructor. { eapply sem_val_rel_cons; eapply val_rel_mono; last done. lia. } eapply Forall_impl; first done. intros. eapply val_rel_mono; last done. lia. - simp type_interp. eexists; split; first done. split; first done. intros τ'. eapply (sem_val_expr_rel _ _ _ (LamV _ _)). simp type_interp. eexists _, _. split; first done. split; first done. intros v2 kd Hv2. simpl. eapply (sem_val_expr_rel _ _ _ (LamV _ _)). simp type_interp. eexists _, _. split; first done. specialize (val_rel_is_closed _ _ _ _ Hv2) as ?. split; first by simplify_closed. intros v3 kd2 Hv3. simpl. rewrite subst_is_closed_nil; last done. eapply (sem_val_expr_rel _ _ _ (LamV _ _)). simp type_interp. eexists _, _. split; first done. specialize (val_rel_is_closed _ _ _ _ Hv3) as ?. split; first by simplify_closed. intros v4 kd3 Hv4. simpl. rewrite !subst_is_closed_nil; [ | done..]. simp type_interp in Hv2. simpl in Hv2. destruct Hv2 as (l & (len & vl & -> & -> & Hl) & Hlf). simpl. destruct l as [ | h l]. + eapply expr_det_steps_closure. { repeat do_det_step. econstructor. } eapply sem_val_expr_rel. eapply val_rel_mono; last done. lia. + simpl in Hl. destruct Hl as (vl' & -> & Hl). eapply expr_det_steps_closure. { repeat do_det_step. econstructor. } replace (S (length l) - 1)%Z with (Z.of_nat \$ length l) by lia. eapply semantic_app. { eapply semantic_app. { eapply sem_val_expr_rel. eapply val_rel_mono; last done. lia. } apply Forall_inv in Hlf. eapply sem_val_expr_rel, val_rel_mono. 2: { eapply sem_val_rel_cons in Hlf. erewrite sem_val_rel_cons in Hlf. asimpl in Hlf. apply Hlf. } lia. } eapply (sem_val_expr_rel _ _ _ (PairV (LitV _) _)). simp type_interp. simpl. exists l. split. { eexists _, _. done. } eapply Forall_inv_tail. eapply Forall_impl; first done. intros. eapply val_rel_mono; last done. lia. Qed.
This diff is collapsed.
 From stdpp Require Import prelude. From iris Require Import prelude. From semantics.lib Require Import facts. From semantics.systemf_mu Require Import lang. From semantics.lib Require Import maps. Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr := match e with | Lit l => Lit l | Var y => match xs !! y with Some es => es | _ => Var y end | App e1 e2 => App (subst_map xs e1) (subst_map xs e2) | Lam x e => Lam x (subst_map (binder_delete x xs) e) | UnOp op e => UnOp op (subst_map xs e) | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2) | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2) | TApp e => TApp (subst_map xs e) | TLam e => TLam (subst_map xs e) | Pack e => Pack (subst_map xs e) | Unpack x e1 e2 => Unpack x (subst_map xs e1) (subst_map (binder_delete x xs) e2) | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2) | Fst e => Fst (subst_map xs e) | Snd e => Snd (subst_map xs e) | InjL e => InjL (subst_map xs e) | InjR e => InjR (subst_map xs e) | Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2) | Roll e => Roll (subst_map xs e) | Unroll e => Unroll (subst_map xs e) end. Lemma subst_map_empty e : subst_map ∅ e = e. Proof. induction e; simpl; f_equal; eauto. all: destruct x; simpl; [done | by rewrite !delete_empty..]. Qed. Lemma subst_map_is_closed X e xs : is_closed X e → (∀ x : string, x ∈ dom xs → x ∉ X) → subst_map xs e = e. Proof. intros Hclosed Hd. induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done. all: repeat match goal with | H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ] end. { (* Var *) apply bool_decide_spec in Hclosed. assert (xs !! x = None) as ->; last done. destruct (xs !! x) as [s | ] eqn:Helem; last done. exfalso; eapply Hd; last apply Hclosed. apply elem_of_dom; eauto. } { (* lambdas *) erewrite IHe; [done | done |]. intros y. destruct x as [ | x]; first apply Hd. simpl. rewrite dom_delete elem_of_difference not_elem_of_singleton. intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done. } 8: { (* Unpack *) erewrite IHe1; [ | done | done]. erewrite IHe2; [ done | done | ]. intros y. destruct x as [ | x]; first apply Hd. simpl. rewrite dom_delete elem_of_difference not_elem_of_singleton. intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done. } (* all other cases *) all: repeat match goal with | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H end; done. Qed. Lemma subst_map_subst map x (e e' : expr) : is_closed [] e' → subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e. Proof. intros He'. revert x map; induction e; intros xx map; simpl; try (f_equal; eauto). - case_decide. + simplify_eq/=. rewrite lookup_insert. rewrite (subst_map_is_closed []); [done | apply He' | ]. intros ? ?. apply not_elem_of_nil. + rewrite lookup_insert_ne; done. - destruct x; simpl; first done. + case_decide. * simplify_eq/=. by rewrite delete_insert_delete. * rewrite delete_insert_ne; last by congruence. done. - destruct x; simpl; first done. + case_decide. * simplify_eq/=. by rewrite delete_insert_delete. * rewrite delete_insert_ne; last by congruence. done. Qed. Definition subst_is_closed (X : list string) (map : gmap string expr) := ∀ x e, map !! x = Some e → closed X e. Lemma subst_is_closed_subseteq X map1 map2 : map1 ⊆ map2 → subst_is_closed X map2 → subst_is_closed X map1. Proof. intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done. Qed. Lemma subst_subst_map x es map e : subst_is_closed [] map → subst x es (subst_map (delete x map) e) = subst_map (<[x:=es]>map) e. Proof. revert map es x; induction e; intros map v0 xx Hclosed; simpl; try (f_equal; eauto). - destruct (decide (xx=x)) as [->|Hne]. + rewrite lookup_delete // lookup_insert //. simpl. rewrite decide_True //. + rewrite lookup_delete_ne // lookup_insert_ne //. destruct (_ !! x) as [rr|] eqn:Helem. * apply Hclosed in Helem. by apply subst_is_closed_nil. * simpl. rewrite decide_False //. - destruct x; simpl; first by auto. case_decide. + simplify_eq. rewrite delete_idemp delete_insert_delete. done. + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe. eapply subst_is_closed_subseteq; last done. apply map_delete_subseteq. - destruct x; simpl; first by auto. case_decide. + simplify_eq. rewrite delete_idemp delete_insert_delete. done. + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe2. eapply subst_is_closed_subseteq; last done. apply map_delete_subseteq. Qed. Lemma subst'_subst_map b (es : expr) map e : subst_is_closed [] map → subst' b es (subst_map (binder_delete b map) e) = subst_map (binder_insert b es map) e. Proof. destruct b; first done. apply subst_subst_map. Qed. Lemma closed_subst_weaken e map X Y : subst_is_closed [] map → (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) → closed X e → closed Y (subst_map map e). Proof. induction e in X, Y, map |-*; rewrite /closed; simpl; intros Hmclosed Hsub Hcl; first done. all: repeat match goal with | H : Is_true (_ && _) |- _ => apply andb_True in H as [ ? ? ] end. { (* vars *) destruct (map !! x) as [es | ] eqn:Heq. + apply is_closed_weaken_nil. by eapply Hmclosed. + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack. by apply not_elem_of_dom. } { (* lambdas *) eapply IHe; last done. + eapply subst_is_closed_subseteq; last done. destruct x; first done. apply map_delete_subseteq. + intros y. destruct x as [ | x]; first by apply Hsub. rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left. destruct (decide (y = x)) as [ -> | Hneq]; first by left. right. eapply Hsub; first done. set_solver. } 8: { (* unpack *) apply andb_True; split; first naive_solver. eapply IHe2; last done. + eapply subst_is_closed_subseteq; last done. destruct x; first done. apply map_delete_subseteq. + intros y. destruct x as [ | x]; first by apply Hsub. rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left. destruct (decide (y = x)) as [ -> | Hneq]; first by left. right. eapply Hsub; first done. set_solver. } (* all other cases *) all: repeat match goal with | |- Is_true (_ && _) => apply andb_True; split end. all: naive_solver. Qed. Lemma subst_is_closed_weaken X1 X2 θ : subst_is_closed X1 θ → X1 ⊆ X2 → subst_is_closed X2 θ. Proof. intros Hcl Hincl x e Hlook. eapply is_closed_weaken; last done. by eapply Hcl. Qed. Lemma subst_is_closed_weaken_nil X θ : subst_is_closed [] θ → subst_is_closed X θ. Proof. intros; eapply subst_is_closed_weaken; first done. apply list_subseteq_nil. Qed. Lemma subst_is_closed_insert X e f θ : is_closed X e → subst_is_closed X (delete f θ) → subst_is_closed X (<[f := e]> θ). Proof. intros Hcl Hcl' x e'. destruct (decide (x = f)) as [<- | ?]. - rewrite lookup_insert. intros [= <-]. done. - rewrite lookup_insert_ne; last done. intros Hlook. eapply Hcl'. rewrite lookup_delete_ne; done. Qed. (* NOTE: this is a simplified version of the tactic in tactics.v which suffice for this proof *) Ltac simplify_closed := repeat match goal with | |- closed _ _ => unfold closed; simpl | |- Is_true (_ && _) => simpl; rewrite !andb_True; split_and! | H : closed _ _ |- _ => unfold closed in H; simpl in H | H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H | H : _ ∧ _ |- _ => destruct H end. Lemma is_closed_subst_map X θ e :