Commit 973b87c5 by Lennard Gäher

exercises 06

parent 915fbeaf
 ... ... @@ -122,55 +122,50 @@ Admitted. (** ** Exercise 1: Encode arithmetic expressions *) Definition aexpr : type := μ: (Int + (#0 × #0)) + (#0 × #0). Definition aexpr : type := #0 (* FIXME *). Definition num_val (v : val) : val := RollV (InjLV \$ InjLV v). Definition num_expr (e : expr) : expr := Roll (InjL \$ InjL e). Definition num_val (v : val) : val := #0 (* FIXME *). Definition num_expr (e : expr) : expr := #0 (* FIXME *). 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 plus_val (v1 v2 : val) : val := #0 (* FIXME *). Definition plus_expr (e1 e2 : expr) : expr := #0 (* FIXME *). Definition mul_val (v1 v2 : val) : val := RollV (InjRV (v1, v2)). Definition mul_expr (e1 e2 : expr) : expr := Roll (InjR (e1, e2)). Definition mul_val (v1 v2 : val) : val := #0 (* FIXME *). Definition mul_expr (e1 e2 : expr) : expr := #0 (* FIXME *). Lemma num_expr_typed n Γ e : TY n; Γ ⊢ e : Int → TY n; Γ ⊢ num_expr e : aexpr. Proof. intros. solve_typing. Qed. (* FIXME *) (*Qed.*) Admitted. 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. (*intros; solve_typing.*) (*Qed.*) Admitted. 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. (*intros; solve_typing.*) (*Qed.*) Admitted. 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. #0 (* FIXME *). Lemma eval_aexpr_typed Γ n : TY n; Γ ⊢ eval_aexpr : (aexpr → Int). Proof. unfold eval_aexpr. apply fix_typing; solve_typing. done. Qed. (*Qed.*) (* FIXME *) Admitted. (** Exercise 3: Lists *) ... ... @@ -182,118 +177,12 @@ Definition list_t (A : type) : type := . 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 *) #0 (* FIXME *) . 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. (* FIXME *) Admitted.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!