Commit 16b71648 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

ex 6 sol

parent 967e3847
......@@ -63,6 +63,8 @@ theories/systemf_mu/untyped_encoding.v
theories/systemf_mu/parallel_subst.v
theories/systemf_mu/logrel.v
theories/systemf_mu/z_combinator.v
theories/systemf_mu/logrel_sol.v
theories/systemf_mu/pure_sol.v
# SystemF + Mu + State
theories/systemf_mu_state/locations.v
......@@ -98,4 +100,5 @@ theories/systemf_mu_state/mutbit.v
#theories/systemf/exercises05.v
#theories/systemf/exercises05_sol.v
#theories/systemf_mu/exercises06.v
#theories/systemf_mu/exercises06_sol.v
#theories/systemf_mu_state/exercises07.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 *)
Definition rec_body (t: expr) : expr :=
roll (λ: f x, t (λ: x, (unroll f) f x) x).
Definition Rec (t: expr): val :=
λ: x, (unroll (rec_body t)) (rec_body t) x.
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_body_subst_x e t:
(sub x e (rec_body t))%E = rec_body t.
Proof.
simpl. destruct decide; try naive_solver.
destruct decide; naive_solver.
Qed.
Lemma rec_body_subst_f e t:
(sub f e (rec_body t))%E = rec_body t.
Proof.
simpl. destruct decide; naive_solver.
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.
intros Hval1 Hval2 Hcl1 Hcl2. do 4 try econstructor 2.
- rewrite /Rec. eapply app_step_beta; first eauto.
simplify_closed.
- cbn -[rec_body]. rewrite rec_body_subst_x.
destruct decide; try naive_solver.
simpl. eapply app_step_l; last eauto.
eapply app_step_l; last done.
eapply unroll_roll_step; done.
- eapply app_step_l; last eauto.
eapply app_step_beta; first done.
simplify_closed.
- simpl.
rewrite decide_False; last congruence.
rewrite decide_False; last congruence.
rewrite decide_True; last done.
rewrite !decide_False; last done.
eapply app_step_beta; [eauto|].
simplify_closed.
- cbn -[rec_body].
rewrite (subst_is_closed_nil _ f); last done.
rewrite (subst_is_closed_nil _ x); last done.
destruct decide; try naive_solver.
destruct decide; naive_solver.
Qed.
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.
intros Hx Hf Hwf1 Hwf2 Hty.
rewrite /rec_body. econstructor; asimpl.
solve_typing.
eapply typed_weakening; eauto.
etrans; first eapply insert_subseteq; first done.
eapply insert_subseteq; rewrite lookup_insert_ne //=.
Qed.
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.
intros Hwf1 Hwf2 Hx Hf Ht. econstructor; last done.
econstructor; last first.
{ econstructor. rewrite lookup_insert //=. }
econstructor; first eapply typed_unroll'.
- eapply typed_weakening with (Γ := Γ); eauto; last by eapply insert_subseteq.
eapply rec_body_typing with (A := A) (B := B); eauto.
- simpl. f_equal. f_equal; by asimpl.
- eapply typed_weakening with (Γ := Γ); eauto; last by eapply insert_subseteq.
eapply rec_body_typing; eauto.
Qed.
End recursion_combinator.
Definition Fix (f x: string) (e: expr) := (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.
Arguments Rec _ _ _ : 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.
intros He Hval. etransitivity; [|econstructor 2]; [| |econstructor 2].
- rewrite Fix_eq /Fix. eapply Rec_red; simpl; eauto.
- eapply app_step_l; last done.
eapply app_step_beta; last done.
done.
- simpl. rewrite decide_False; last congruence.
eapply app_step_beta; first done.
eapply is_closed_subst.
{ apply closed_Rec; done. }
eapply is_closed_weaken; eauto. set_solver.
- rewrite Fix_eq; done.
Qed.
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.
intros Hwf1 Hwf2 Hfx He.
rewrite Fix_eq /Fix.
eapply typed_weakening with (Γ := delete x (delete f Γ)); eauto; last first.
{ etrans; eapply delete_subseteq. }
eapply Rec_typing; eauto.
- eapply lookup_delete.
- rewrite lookup_delete_ne //=. eapply lookup_delete.
- econstructor; last eauto.
econstructor; last eauto.
rewrite -delete_insert_ne //=.
rewrite !insert_delete_insert. done.
Qed.
(** ** 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 *)
.
(** We define a recursive representation predicate for lists.
This is a common pattern: we specify the shape of lists in our language in terms of lists at the meta-level (i.e., in Coq).
*)
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.
(* A full list also needs to store the length, otherwise we'd have no way of knowing
when a list ends (we can't analyze whether a term is () or a pair from inside the language) *)
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 gmap base relations.
From iris Require Import prelude.
From semantics.lib Require Import maps.
From semantics.systemf_mu Require Import lang notation.
Lemma contextual_ectx_step_case K e e' :
contextual_step (fill K e) e'
( e'', e' = fill K e'' contextual_step e e'') is_val e.
Proof.
destruct (to_val e) as [ v | ] eqn:Hv.
{ intros _. right. apply is_val_spec. eauto. }
intros Hcontextual. left.
inversion Hcontextual as [K' e1' e2' Heq1 Heq2 Hstep]; subst.
eapply step_by_val in Heq1 as (K'' & ->); [ | done | done].
rewrite <-fill_comp.
eexists _. split; [done | ].
rewrite <-fill_comp in Hcontextual.
apply contextual_step_ectx_inv in Hcontextual; done.
Qed.
(** ** Deterministic reduction *)
Record det_step (e1 e2 : expr) := {
det_step_safe : reducible e1;
det_step_det e2' :
contextual_step e1 e2' e2' = e2
}.
Record det_base_step (e1 e2 : expr) := {
det_base_step_safe : base_reducible e1;
det_base_step_det e2' :
base_step e1 e2' e2' = e2
}.
Lemma det_base_step_det_step e1 e2 : det_base_step e1 e2 det_step e1 e2.
Proof.
intros [Hp1 Hp2]. split.
- destruct Hp1 as (e2' & ?).
eexists e2'. by apply base_contextual_step.
- intros e2' ?%base_reducible_contextual_step; [ | done]. by apply Hp2.
Qed.
(** *** Pure execution lemmas *)
Local Ltac inv_step :=
repeat match goal with
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : base_step ?e ?e2 |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and should thus better be avoided. *)
inversion H; subst; clear H
end.
Local Ltac solve_exec_safe := intros; subst; eexists; econstructor; eauto.
Local Ltac solve_exec_detdet := simpl; intros; inv_step; try done.
Local Ltac solve_det_exec :=
subst; intros; apply det_base_step_det_step;
constructor; [solve_exec_safe | solve_exec_detdet].
Lemma det_step_beta x e e2 :
is_val e2
det_step (App (@Lam x e) e2) (subst' x e2 e).
Proof. solve_det_exec. Qed.
Lemma det_step_tbeta e :
det_step ((Λ, e) <>) e.
Proof. solve_det_exec. Qed.
Lemma det_step_unpack e1 e2 x :
is_val e1
det_step (unpack (pack e1) as x in e2) (subst' x e1 e2).
Proof. solve_det_exec. Qed.
Lemma det_step_unop op e v v' :
to_val e = Some v
un_op_eval op v = Some v'
det_step (UnOp op e) v'.
Proof. solve_det_exec. by simplify_eq. Qed.
Lemma det_step_binop op e1 v1 e2 v2 v' :
to_val e1 = Some v1
to_val e2 = Some v2
bin_op_eval op v1 v2 = Some v'
det_step (BinOp op e1 e2) v'.
Proof. solve_det_exec. by simplify_eq. Qed.
Lemma det_step_if_true e1 e2 :
det_step (if: #true then e1 else e2) e1.
Proof. solve_det_exec. Qed.
Lemma det_step_if_false e1 e2 :
det_step (if: #false then e1 else e2) e2.
Proof. solve_det_exec. Qed.
Lemma det_step_fst e1 e2 :
is_val e1
is_val e2
det_step (Fst (e1, e2)) e1.
Proof. solve_det_exec. Qed.
Lemma det_step_snd e1 e2 :
is_val e1
is_val e2
det_step (Snd (e1, e2)) e2.
Proof. solve_det_exec. Qed.
Lemma det_step_casel e e1 e2 :
is_val e
det_step (Case (InjL e) e1 e2) (e1 e).
Proof. solve_det_exec. Qed.
Lemma det_step_caser e e1 e2 :
is_val e
det_step (Case (InjR e) e1 e2) (e2 e).
Proof. solve_det_exec. Qed.
Lemma det_step_unroll e :
is_val e
det_step (unroll (roll e)) e.
Proof. solve_det_exec. Qed.
(** ** n-step reduction *)
(** Reduce in n steps to an irreducible expression.
(this is ⇝^n from the lecture notes)
*)
Definition red_nsteps (n : nat) (e e' : expr) := nsteps contextual_step n e e' irreducible e'.
Lemma det_step_red e e' e'' n :
det_step e e'
red_nsteps n e e''
1 n red_nsteps (n - 1) e' e''.
Proof.
intros [Hprog Hstep] Hred.
inversion Hprog; subst.
destruct Hred as [Hred Hirred].
destruct n as [ | n].
{ inversion Hred; subst.
exfalso; eapply not_reducible; done.
}
inversion Hred; subst. simpl.
apply Hstep in H as ->. apply Hstep in H1 as ->.
split; first lia.
replace (n - 0) with n by lia. done.
Qed.
Lemma contextual_step_red_nsteps n e e' e'' :
contextual_step e e'
red_nsteps n e' e''
red_nsteps (S n) e e''.
Proof.
intros Hstep [Hsteps Hirred].
split; last done.
by econstructor.
Qed.
Lemma nsteps_val_inv n v e' :
red_nsteps n (of_val v) e' n = 0 e' = of_val v.
Proof.
intros [Hred Hirred]; cbn in *.
destruct n as [ | n].
- inversion Hred; subst. done.
- inversion Hred; subst. exfalso. eapply val_irreducible; last done.
rewrite to_of_val. eauto.
Qed.
Lemma nsteps_val_inv' n v e e' :
to_val e = Some v
red_nsteps n e e' n = 0 e' = of_val v.