Compare commits

..

5 Commits

@ -50,6 +50,7 @@ theories/type_systems/systemf/free_theorems.v
theories/type_systems/systemf/binary_logrel.v
theories/type_systems/systemf/binary_logrel_sol.v
theories/type_systems/systemf/existential_invariants.v
theories/type_systems/systemf/church_encodings_faithful.v
# SystemF-Mu
theories/type_systems/systemf_mu/lang.v
@ -57,9 +58,21 @@ theories/type_systems/systemf_mu/notation.v
theories/type_systems/systemf_mu/types.v
theories/type_systems/systemf_mu/tactics.v
theories/type_systems/systemf_mu/pure.v
theories/type_systems/systemf_mu/pure_sol.v
theories/type_systems/systemf_mu/untyped_encoding.v
theories/type_systems/systemf_mu/parallel_subst.v
theories/type_systems/systemf_mu/logrel.v
theories/type_systems/systemf_mu/logrel_sol.v
# SystemF + Mu + State
theories/type_systems/systemf_mu_state/locations.v
theories/type_systems/systemf_mu_state/lang.v
theories/type_systems/systemf_mu_state/notation.v
theories/type_systems/systemf_mu_state/types.v
theories/type_systems/systemf_mu_state/tactics.v
theories/type_systems/systemf_mu_state/execution.v
theories/type_systems/systemf_mu_state/parallel_subst.v
theories/type_systems/systemf_mu_state/logrel.v
# By removing the # below, you can add the exercise sheets to make
theories/type_systems/warmup/warmup.v
@ -77,3 +90,5 @@ theories/type_systems/systemf/exercises04.v
theories/type_systems/systemf/exercises05.v
#theories/type_systems/systemf/exercises05_sol.v
#theories/type_systems/systemf_mu/exercises06.v
#theories/type_systems/systemf_mu/exercises06_sol.v
#theories/type_systems/systemf_mu_state/exercises07.v

@ -338,6 +338,14 @@ Proof.
by apply of_to_val.
Qed.
(*
By induction on the transitive closure,
we need to show that if `e = v`, then `v | v` (trivial), and if `e >- e'` and `e' | v`,
then `e | v`.
To prove this, we do an induction on the rule used for the single small step.
Each of the cases are individually quite easy: one just needs to provide which big step rule should be used,
and the induction hypothesis can be plugged into the conditions of the big step.
*)
Lemma steps_big_step e (v: val):
rtc step e v big_step e v.
Proof.
@ -345,8 +353,7 @@ Proof.
remember (of_val v) eqn:H_val in H.
induction H; subst.
apply big_step_vals.
remember ((IHrtc (eq_refl (of_val v)))) as IH.
clear HeqIH.
have IH := ((IHrtc (eq_refl (of_val v)))).
clear IHrtc.
(* This is ridiculous. *)
revert H0.

@ -107,7 +107,10 @@ Qed.
(** Now the other direction. *)
(* You may find it helpful to introduce intermediate lemmas. *)
(*
To prove this, we first need to invert the contextual step.
By induction on the context, we can reconstruct the small-step rule used.
*)
Lemma contextual_step_step e1 e2:
contextual_step e1 e2 step e1 e2.
Proof.
@ -320,6 +323,12 @@ Inductive src_typed : typing_context → src_expr → type → Prop :=
where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
#[export] Hint Constructors src_typed : core.
(*
This is trivial enough for `eauto` to be able to solve all the cases for us.
Doing an induction on the source typing rule used, we can infer the structure of `E`,
the hypothesis needed, and then unfold `erase` to reveal in each case an equivalent
syntactical typing rule.
*)
Lemma type_erasure_correctness Γ E A:
(Γ S E : A)%ty (Γ erase E : A)%ty.
Proof.
@ -329,6 +338,14 @@ Qed.
(** ** Exercise 4: Unique Typing *)
(*
This is a bit of a boring lemma.
We do induction on the first typing and inversion on the second typing.
- for integers, this is trivial
- for variables, since the Γ is shared, by injection we can see that A = B since Γ[x] = Some A = Some B
- for functions of type `C -> A2` =? `C -> B2`, we need to use the induction hypothesis, which asks us to prove that `Γ |- body : B2` to get that `A2 = B2`
- for function applications, the induction hypothesis tells us that if `Γ |- e_fn : B1 -> B2`, then `A1 -> A2` = `B1 -> B2`, allowing us to show that `A2 = B2`.
*)
Lemma src_typing_unique Γ E A B:
(Γ S E : A)%ty (Γ S E : B)%ty A = B.
Proof.

@ -287,6 +287,18 @@ Proof.
Qed.
(*
First, unfold the definition of `Γ |=` everywhere.
The closedness of our term can easily be solved by `naive_solver`.
We can then use the same θ and H_ctx in all hypotheses,
and unroll all definitions of `E[A]`, yielding `v_lhs` and `v_rhs` to which resp. `e_lhs` and `e_rhs` step.
Then, pick `(v_lhs, v_rhs)` as the value this should step to.
We then just need to show that `(e_lhs, e_rhs)` step towards `(v_lhs, v_rhs)`,
and that `(v_lhs, v_rhs) V[A × B]`.
*)
Lemma compat_pair Γ e_lhs e_rhs A B:
Γ e_lhs: A
Γ e_rhs: B
@ -323,6 +335,10 @@ Proof.
eauto. (* Trivial from then on *)
Qed.
(*
Proving this is very similar to the above, except that we need to work on two goals at once,
and we apply the definition of `V[A × B]` to get the necessary stuff to prove both statements.
*)
Lemma compat_fst_snd {Γ e_pair A B}:
Γ e_pair: A × B
Γ (Fst e_pair): A Γ (Snd e_pair): B.

@ -342,6 +342,14 @@ Proof.
intros H1 H2; by eapply H2.
Qed.
(*
By induction on the base step,
we can invert the the typing rules used for `|- e : A` and its hypotheses.
- in the `base_step_case_l` case, we can also invert the `InjL` typing rule
that appears after the first inversion. We then get that `e1 : A' -> A` and `e2 : B' -> A`,
and `v : A'`.
We now just reconstruct the typing of `e'` by using the application constructor.
*)
Lemma typed_preservation_base_step e e' A:
e : A
base_step e e'
@ -366,7 +374,7 @@ Proof.
assumption.
- eapply case_inversion in Hty as (A' & B' & Hty_inj & Hty_lhs & Hty_rhs).
eapply injl_inversion in Hty_inj as (A'' & B'' & Heq & Hty_inj).
injection Heq as -> ->.
injection Heq as <- <-.
eapply typed_app.
exact Hty_lhs.
exact Hty_inj.

@ -0,0 +1,273 @@
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.lib Require Export facts.
From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics binary_logrel.
From semantics.ts.systemf Require church_encodings.
Import church_encodings.
(* we first prove some helpful lemmas *)
Lemma big_step_bind e v w K:
big_step e v big_step (fill K v) w big_step (fill K e) w.
Proof.
intros Hbs; induction K in w |-*; simpl.
{ intros ->%big_step_val. done. }
all: inversion 1; subst; by econstructor; eauto.
Qed.
Lemma big_step_bind_inv e w K:
big_step (fill K e) w v, big_step e v big_step (fill K v) w.
Proof.
induction K in w |-*; simpl.
{ intros ?; eexists _; split; first done. by eapply big_step_of_val. }
all: inversion 1; subst; edestruct IHK as [? [? ?]]; eauto.
Qed.
Lemma big_step_det e v w:
big_step e v big_step e w v = w.
Proof.
induction 1 in w |-*; inversion 1; subst; eauto 2.
all: naive_solver.
Qed.
Lemma closure_under_reduction e1 e2 v1 v2 δ A:
big_step e1 v1
big_step e2 v2
𝒱 A δ v1 v2
A δ e1 e2.
Proof. simp type_interp. eauto. Qed.
Lemma closure_under_partial_reduction e1 e2 v1 v2 K1 K2 δ A:
big_step e1 v1
big_step e2 v2
A δ (fill K1 v1) (fill K2 v2)
A δ (fill K1 e1) (fill K2 e2).
Proof.
simp type_interp. intros Hbs1 Hbs2 (v3 & v4 & Hbs3 & Hbs4 & Hty).
eexists _, _. eauto using big_step_bind.
Qed.
Lemma closure_under_expansion e1 e2 v1 v2 K1 K2 δ A:
big_step e1 v1
big_step e2 v2
A δ (fill K1 e1) (fill K2 e2)
A δ (fill K1 v1) (fill K2 v2).
Proof.
simp type_interp. intros Hbs1 Hbs2 (v3 & v4 & Hbs3 & Hbs4 & Hty).
eapply big_step_bind_inv in Hbs3 as [? [Hr1 Hbs3]].
eapply big_step_bind_inv in Hbs4 as [? [Hr2 Hbs4]].
eapply big_step_det in Hr1; last apply Hbs1.
eapply big_step_det in Hr2; last apply Hbs2.
subst. eauto.
Qed.
Lemma tforall_expand (v1 v2 v3 v4 : val) δ A:
( τ, A (τ.:δ) (v1 <>) (v2 <>))
𝒱 (: A) δ v1 v3
𝒱 (: A) δ v2 v4
𝒱 (: A) δ v1 v2.
Proof.
simp type_interp.
intros Hty (e1 & e2 & -> & -> & Hc1 & Hc2 & Hty2) (e3 & e4 & -> & -> & Hc3 & Hc4 & Hty3).
eexists _, _. split_and!; eauto. intros τ. specialize (Hty τ).
revert Hty. simp type_interp.
intros (v1 & v2 & Hbs1 & Hbs2 & Hty).
inversion Hbs1; subst. inversion Hbs2; subst. inversion H0; subst. inversion H2; subst.
eexists _, _. split_and!; done.
Qed.
Lemma tforall_reduce v1 v2 δ A τ:
𝒱 (: A) δ v1 v2
A (τ.:δ) (v1 <>) (v2 <>).
Proof.
simp type_interp. intros (? & ? & -> & -> & ? & ? & Hty).
specialize (Hty τ). revert Hty.
simp type_interp. intros (? & ? & ? & ? & Hval).
eexists _, _. split_and!; eauto using big_step.
Qed.
Lemma fun_expand (e1 e2 e3 e4 : expr) δ A B:
( v w, 𝒱 A δ v w B δ (e1 v) (e2 w))
(A B) δ e1 e3
(A B) δ e4 e2
(A B) δ e1 e2.
Proof.
simp type_interp.
intros Hty (v1 & v3 & Hbs1 & Hbs3 & Hty13) (v2 & v4 & Hbs2 & Hbs4 & Hty24).
simp type_interp in Hty13. simp type_interp in Hty24.
destruct Hty13 as (x1 & x3 & e1' & e3' & -> & -> & Hc1 & Hc3 & _),
Hty24 as (x2 & x4 & e2' & e4' & -> & -> & Hc2 & Hc4 & _).
eexists _, _. split_and!; eauto. simp type_interp.
eexists _, _, _, _. split_and!; eauto.
intros v' w' Hty'. specialize (Hty _ _ Hty').
simp type_interp. simp type_interp in Hty.
destruct Hty as (v1 & v2 & Hbs1' & Hbs2' & Hval).
eexists _, _. split_and!; last done.
- eapply big_step_bind_inv with (K := AppLCtx HoleCtx v') in Hbs1' as [u1 [Hu1 Hu2]].
eapply big_step_det in Hu1; last by apply Hbs1.
subst u1. simpl in Hu2. inversion Hu2; subst. eapply big_step_val in H2. inversion H1; subst.
done.
- eapply big_step_bind_inv with (K := AppLCtx HoleCtx w') in Hbs2' as [u1 [Hu1 Hu2]].
eapply big_step_det in Hu1; last by apply Hbs4.
subst u1. simpl in Hu2. inversion Hu2; subst. eapply big_step_val in H2. inversion H1; subst.
done.
Qed.
Lemma fun_reduce e1 e2 δ A B:
(A B) δ e1 e2
( v w, 𝒱 A δ v w B δ (e1 v) (e2 w)).
Proof.
simp type_interp. intros (? & ? & Hbs1 & Hbs2 & Hty) v w Hval.
simp type_interp in Hty. destruct Hty as (? & ? & e1' & e3' & -> & -> & ? & ? & Hrest).
specialize (Hrest _ _ Hval).
simp type_interp in Hrest.
destruct Hrest as (v' & w' & ? & ? & Hval').
simp type_interp. eexists _, _; split_and!; eauto using big_step, big_step_of_val.
Qed.
Lemma bind e1 e2 K1 K2 δ δ' A B:
A δ e1 e2
( v w, 𝒱 A δ v w B δ' (fill K1 v) (fill K2 w))
B δ' (fill K1 e1) (fill K2 e2).
Proof.
simp type_interp. intros (v & w & Hbs1 & Hbs2 & Hty) Hcont.
specialize (Hcont v w Hty). simp type_interp in Hcont.
destruct Hcont as (v' & w' & Hbs1' & Hbs2' & Hcont).
eexists _, _. split_and!; eauto using big_step_bind.
Qed.
(* faithfulness of bool *)
Definition eta_bool (e: expr) : expr :=
e <> bool_true bool_false.
Lemma bool_type_full (v w f g : val) δ :
closed [] v
closed [] w
type_interp (inj_val f g) bool_type δ
b, (b = v b = w) (big_step (f <> v w) b big_step (g <> v w) b).
Proof.
intros Hc1 Hc2.
rewrite /bool_type. simp type_interp.
intros (e1 & e2 & -> & -> & Hcl1 & Hcl2 & Hty).
specialize_sem_type Hty with (λ u1 u2, (u1 = u2 u2 = v) (u1 = u2 u2 = w)) as B.
{ intros u1 u2 [[-> ->]|[-> ->]]; split; done. }
simp type_interp in Hty. destruct Hty as (u3 & u4 & Hbs1 & Hbs2 & Hu34).
simp type_interp in Hu34. destruct Hu34 as (x1 & x1' & e3 & e3' & -> & -> & ? & ? & Hty).
opose proof* (Hty v v) as Hty; first simp type_interp; simpl; eauto.
simp type_interp in Hty. destruct Hty as (u5 & u6 & Hbs3 & Hbs4 & Hu56).
simp type_interp in Hu56. destruct Hu56 as (x2 & x2' & e4 & e4' & -> & -> & ? & ? & Hty).
opose proof* (Hty w w) as Hty; first simp type_interp; simpl; eauto.
simp type_interp in Hty. destruct Hty as (u7 & u8 & Hbs5 & Hbs6 & Hu78).
simp type_interp in Hu78. simpl in Hu78. destruct Hu78 as [[-> ->] | [-> ->]].
- exists v. split; first naive_solver.
split; repeat econstructor; eauto using big_step_of_val.
- exists w. split; first naive_solver.
split; repeat econstructor; eauto using big_step_of_val.
Qed.
Lemma bool_true_sem_bool δ: 𝒱 bool_type δ bool_true bool_true.
Proof.
assert (TY 0; bool_true: bool_type) as Hty by solve_typing.
eapply sem_soundness in Hty as (Htycl1 & Htycl2 & Hty).
opose proof* (Hty δ) as Hty; first constructor.
by eapply sem_expr_rel_of_val.
Qed.
Lemma bool_false_sem_bool δ: 𝒱 bool_type δ bool_false bool_false.
Proof.
assert (TY 0; bool_false: bool_type) as Hty by solve_typing.
eapply sem_soundness in Hty as (Htycl1 & Htycl2 & Hty).
opose proof* (Hty δ) as Hty; first constructor.
by eapply sem_expr_rel_of_val.
Qed.
Lemma bool_faithful Δ Γ e:
TY Δ; Γ e: bool_type ctx_equiv Δ Γ e (eta_bool e) bool_type.
Proof.
intros Hty. eapply soundness_wrt_ctx_equiv; [solve_typing..].
split_and!. 1-2: apply syn_typed_closed in Hty; naive_solver.
intros θ1 θ2 δ Hctx. eapply sem_soundness in Hty as (Htycl1 & Htycl2 & Hty).
specialize (Hty θ1 θ2 δ Hctx). simp type_interp in Hty.
replace (subst_map θ2 (eta_bool e)) with (eta_bool (subst_map θ2 e)); last first.
{ simpl; rewrite lookup_delete_ne //= !lookup_delete //. }
destruct Hty as (v1 & v2 & Hbs1 & Hbs2 & Hty).
eapply closure_under_partial_reduction with (K1 := HoleCtx) (K2:= (AppLCtx (AppLCtx (TAppCtx HoleCtx) bool_true) bool_false)); eauto.
simpl; change (v2 <> _ _)%E with (eta_bool v2). clear Hctx Hbs1 Hbs2.
generalize Hty=> Hfull.
eapply (bool_type_full bool_true bool_false) in Hfull; [|done..].
destruct Hfull as (b & Hopt & Hv1b & Hv2b).
eapply closure_under_reduction; eauto using big_step_of_val.
assert (𝒱 bool_type δ b b) as Hb.
{ destruct Hopt; subst; eauto using bool_true_sem_bool, bool_false_sem_bool. }
eapply tforall_expand; eauto.
intros R. generalize Hty=>Hty'.
(* we have to evaluate these assumptions along the way *)
rewrite /bool_type in Hb, Hty'.
eapply tforall_reduce with (τ := R) in Hb.
eapply tforall_reduce with (τ := R) in Hty'.
eapply fun_expand; eauto.
intros a1 a2 Ha12.
eapply fun_reduce in Hb; last done.
eapply fun_reduce in Hty'; last done.
eapply fun_expand; eauto.
intros b1 b2 Hb12.
simp type_interp in Ha12; simpl in Ha12.
simp type_interp in Hb12; simpl in Hb12.
clear Hb Hty'.
eapply closure_under_expansion with
(K1:= (AppLCtx (AppLCtx (TAppCtx HoleCtx) a1) b1))
(K2:= (AppLCtx (AppLCtx (TAppCtx HoleCtx) a2) b2));
[by eapply big_step_of_val | eapply Hv2b|]; cbn [fill].
pose_sem_type (λ v w, (v = a1 w = bool_true) (v = b1 w = bool_false)) as τ.
{ apply sem_type_closed_val in Ha12, Hb12. naive_solver. }
eapply bind with
(K1 := HoleCtx)
(K2 := AppLCtx (AppLCtx (TAppCtx HoleCtx) a2) b2)
(A := (#0)%ty)
(δ := τ.:δ).
{ eapply fun_reduce.
eapply fun_reduce.
eapply tforall_reduce.
exact Hty.
- simp type_interp. simpl. auto.
- simp type_interp. simpl. auto. }
simpl. intros v w Hty'. simp type_interp in Hty'. simpl in Hty'.
destruct Hty' as [[-> ->]|[-> ->]].
- simp type_interp. exists a1, a2. split_and!.
+ by apply big_step_of_val.
+ simpl. bs_step_det.
rewrite subst_is_closed_nil; first by apply big_step_of_val.
apply sem_type_closed_val in Ha12. naive_solver.
+ simp type_interp.
- simp type_interp. exists b1, b2. split_and!.
+ by apply big_step_of_val.
+ simpl. bs_step_det. by apply big_step_of_val.
+ simp type_interp.
Qed.

@ -171,5 +171,6 @@ Qed.
In the lecture, we also saw `A[id] = (. #0 -> #1)[id] = . (#0 -> #1)[id] = . (#0 -> (id(0))) = . #0 -> #0`
To fix this, we would have to carefully tweak each value in our substitution map to increment all the free type variables
To fix this, we would have to carefully tweak each value in our substitution map to increment all the free type variables.
This is what `ren` does.
*)

@ -0,0 +1,375 @@
From stdpp Require Import gmap base relations tactics.
From iris Require Import prelude.
From semantics.ts.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 :=
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) : 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.
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 (fun v => 𝒱 A δ_any k' v) 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 k' Hk' 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 k'2 Hk'2 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 v' Hv'. eapply val_rel_mono; last apply Hv'. 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 k' Hk' 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 k'2 Hk'2 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 k'3 Hk'3 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 v' Hv'. eapply val_rel_mono; last apply Hv'. lia.
Qed.

@ -531,6 +531,18 @@ Section boring_lemmas.
End boring_lemmas.
(** Bind lemma *)
(*
From the definition of `E[A]` and `E[B]`,
we get that ` e', n < k, K[e] \^n e' -> (k - n, e') V[B]`
- We know that ` j, e \^j e''` and `K[e''] \^(n-j) e'` using a lemma.
- From the expansion of `E[A]`, we can plug `e''` and `j` into `e E[A]`,
yielding `(k-j, e'') V[A]`
- We can use the second hypothesis with `k-j` and the value associated to `e''` as input, yielding `(k-j, K[e'']) E[B]`
- Plugging in the expansion of `E[B]` into `K[e''] \^(n-j) e'`,
we get that `(k-j-(n-j), e') V[B]`
- `k-j-(n-j) = k-n`, allowing us to prove our goal
*)
Lemma bind K e k δ A B :
A δ k e
( j v, j k 𝒱 A δ j v B δ j (fill K (of_val v)))

File diff suppressed because it is too large Load Diff

@ -0,0 +1,310 @@
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.lib Require Import maps.
From semantics.ts.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.
Proof. intros Ht. rewrite -(of_to_val _ _ Ht). apply nsteps_val_inv. Qed.
Lemma red_nsteps_fill K k e e' :
red_nsteps k (fill K e) e'
j e'', j k
red_nsteps j e e''
red_nsteps (k - j) (fill K e'') e'.
Proof.
intros [Hsteps Hirred].
induction k as [ | k IH] in e, e', Hsteps, Hirred |-*.
- inversion Hsteps; subst.
exists 0, e. split_and!; [done | split | ].
+ constructor.
+ by eapply irreducible_fill.
+ done.
- inversion Hsteps as [ | n e1 e2 e3 Hstep Hsteps' Heq1 Heq2 Heq3]. subst.
destruct (contextual_ectx_step_case _ _ _ Hstep) as [(e'' & -> & Hstep') | Hv].
+ apply IH in Hsteps' as (j & e3 & ? & Hsteps' & Hsteps''); last done.
eexists (S j), _. split_and!; [lia | | done].
eapply contextual_step_red_nsteps; done.
+ exists 0, e. split_and!; [ lia | | ].
* split; [constructor | ].
apply val_irreducible. by apply is_val_spec.
* simpl. by eapply contextual_step_red_nsteps.
Qed.
(** Additionally useful stepping lemmas *)
Lemma app_step_r (e1 e2 e2': expr) :
contextual_step e2 e2' contextual_step (e1 e2) (e1 e2').
Proof. by apply (fill_contextual_step [AppRCtx _]). Qed.
Lemma app_step_l (e1 e1' e2: expr) :
contextual_step e1 e1' is_val e2 contextual_step (e1 e2) (e1' e2).
Proof.
intros ? (v & Hv)%is_val_spec.
rewrite <-(of_to_val _ _ Hv).
by apply (fill_contextual_step [AppLCtx _]).
Qed.
Lemma app_step_beta (x: string) (e e': expr) :
is_val e' is_closed [x] e contextual_step ((λ: x, e) e') (lang.subst x e' e).
Proof.
intros Hval Hclosed. eapply base_contextual_step, BetaS; eauto.
Qed.
Lemma unroll_roll_step (e: expr) :
is_val e contextual_step (unroll (roll e)) e.
Proof.
intros ?; by eapply base_contextual_step, UnrollS.
Qed.
Lemma fill_reducible K e :
reducible e reducible (fill K e).
Proof.
intros (e' & Hstep).
exists (fill K e'). eapply fill_contextual_step. done.
Qed.
Lemma reducible_contextual_step_case K e e' :
contextual_step (fill K e) (e')
reducible e
e'', e' = fill K e'' contextual_step e e''.
Proof.
intros [ | Hval]%contextual_ectx_step_case Hred; first done.
exfalso. apply is_val_spec in Hval as (v & Hval).
apply reducible_not_val in Hred. congruence.
Qed.
(** Contextual lifting lemmas for deterministic reduction *)
Tactic Notation "lift_det" uconstr(ctx) :=
intros;
let Hs := fresh in
match goal with
| H : det_step _ _ |- _ => destruct H as [? Hs]
end;
simplify_val; econstructor;
[intros; by eapply (fill_reducible ctx) |
intros ? (? & -> & ->%Hs)%(reducible_contextual_step_case ctx); done ].
Lemma det_step_pair_r e1 e2 e2' :
det_step e2 e2'
det_step (e1, e2)%E (e1, e2')%E.
Proof. lift_det [PairRCtx _]. Qed.
Lemma det_step_pair_l e1 e1' e2 :
is_val e2
det_step e1 e1'
det_step (e1, e2)%E (e1', e2)%E.
Proof. lift_det [PairLCtx _]. Qed.
Lemma det_step_binop_r e1 e2 e2' op :
det_step e2 e2'
det_step (BinOp op e1 e2)%E (BinOp op e1 e2')%E.
Proof. lift_det [BinOpRCtx _ _]. Qed.
Lemma det_step_binop_l e1 e1' e2 op :
is_val e2
det_step e1 e1'
det_step (BinOp op e1 e2)%E (BinOp op e1' e2)%E.
Proof. lift_det [BinOpLCtx _ _]. Qed.
Lemma det_step_if e e' e1 e2 :
det_step e e'
det_step (If e e1 e2)%E (If e' e1 e2)%E.
Proof. lift_det [IfCtx _ _]. Qed.
Lemma det_step_app_r e1 e2 e2' :
det_step e2 e2'
det_step (App e1 e2)%E (App e1 e2')%E.
Proof. lift_det [AppRCtx _]. Qed.
Lemma det_step_app_l e1 e1' e2 :
is_val e2
det_step e1 e1'
det_step (App e1 e2)%E (App e1' e2)%E.
Proof. lift_det [AppLCtx _]. Qed.
Lemma det_step_snd_lift e e' :
det_step e e'
det_step (Snd e)%E (Snd e')%E.
Proof. lift_det [SndCtx]. Qed.
Lemma det_step_fst_lift e e' :
det_step e e'
det_step (Fst e)%E (Fst e')%E.
Proof. lift_det [FstCtx]. Qed.
#[global]
Hint Resolve app_step_r app_step_l app_step_beta unroll_roll_step : core.
#[global]
Hint Extern 1 (is_val _) => (simpl; fast_done) : core.
#[global]
Hint Immediate is_val_of_val : core.
#[global]
Hint Resolve det_step_beta det_step_tbeta det_step_unpack det_step_unop det_step_binop det_step_if_true det_step_if_false det_step_fst det_step_snd det_step_casel det_step_caser det_step_unroll : core.
#[global]
Hint Resolve det_step_pair_r det_step_pair_l det_step_binop_r det_step_binop_l det_step_if det_step_app_r det_step_app_l det_step_snd_lift det_step_fst_lift : core.
#[global]
Hint Constructors nsteps : core.
#[global]
Hint Extern 1 (is_val _) => simpl : core.
(** Prove a single deterministic step using the lemmas we just proved *)
Ltac do_det_step :=
match goal with
| |- nsteps det_step _ _ _ => econstructor 2; first do_det_step
| |- det_step _ _ => simpl; solve[eauto 10]
end.

@ -0,0 +1,450 @@
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.ts.systemf_mu_state Require Import lang notation.
(* TODO: everywhere replace the metavar σ for heaps with h *)
(** ** Deterministic reduction *)
Record det_step (e1 : expr) (e2 : expr) := {
det_step_safe h : reducible e1 h;
det_step_det e2' h h' :
contextual_step (e1, h) (e2', h') e2' = e2 h' = h
}.
Record det_base_step (e1 e2 : expr) := {
det_base_step_safe h : base_reducible e1 h;
det_base_step_det e2' h h' :
base_step (e1, h) (e2', h') e2' = e2 h' = h
}.
Lemma det_base_step_det_step e1 e2 : det_base_step e1 e2 det_step e1 e2.
Proof.
intros [Hp1 Hp2]. split.
- intros h. destruct (Hp1 h) as (e2' & h' & ?).
eexists e2', h'. by apply base_contextual_step.
- intros e2' h h' ?%base_reducible_contextual_step; [ | done]. by eapply 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, ?σ2) |- _ =>
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 h e' h' := nsteps contextual_step n (e, h) (e', h') irreducible e' h'.
Lemma det_step_red e e' e'' h h'' n :
det_step e e'
red_nsteps n e h e'' h''
1 n red_nsteps (n - 1) e' h e'' h''.
Proof.
intros [Hprog Hstep] Hred.
specialize (Hprog h).
destruct Hred as [Hred Hirred].
destruct n as [ | n].
{ inversion Hred; subst.
exfalso; eapply not_reducible; done.
}
inversion Hred as [ | ??[e1 h1]? Hstep0]; subst. simpl.
apply Hstep in Hstep0 as [<- <-].
split; first lia.
replace (n - 0) with n by lia. done.
Qed.
Lemma contextual_step_red_nsteps n e e' e'' h h' h'':
contextual_step (e, h) (e', h')
red_nsteps n e' h' e'' h''
red_nsteps (S n) e h e'' h''.
Proof.
intros Hstep [Hsteps Hirred].
split; last done.
by econstructor.
Qed.
Lemma nsteps_val_inv n v e' h h' :
red_nsteps n (of_val v) h e' h' n = 0 e' = of_val v h' = h.
Proof.
intros [Hred Hirred]; cbn in *.
destruct n as [ | n].
- inversion Hred; subst. done.
- inversion Hred as [ | ??[e1 h1]]; subst. exfalso. eapply val_irreducible; last done.
rewrite to_of_val. eauto.
Qed.
Lemma nsteps_val_inv' n v e e' h h' :
to_val e = Some v
red_nsteps n e h e' h' n = 0 e' = of_val v h' = h.
Proof. intros Ht. rewrite -(of_to_val _ _ Ht). apply nsteps_val_inv. Qed.
Lemma red_nsteps_fill K k e e' h h' :
red_nsteps k (fill K e) h e' h'
j e'' h'', j k
red_nsteps j e h e'' h''
red_nsteps (k - j) (fill K e'') h'' e' h'.
Proof.
intros [Hsteps Hirred].
induction k as [ | k IH] in e, e', h, h', Hsteps, Hirred |-*.
- inversion Hsteps; subst.
exists 0, e, h'. split_and!; [done | split | ].
+ constructor.
+ by eapply irreducible_fill.
+ done.
- inversion Hsteps as [ | n [e1 h1] [e2 h2] [e3 h3] Hstep Hsteps' Heq1 Heq2 Heq3]. subst.
destruct (contextual_ectx_step_case _ _ _ _ _ Hstep) as [(e'' & -> & Hstep') | Hv].
+ apply IH in Hsteps' as (j & e3 & h3 & ? & Hsteps' & Hsteps''); last done.
eexists (S j), _, _. split_and!; [lia | | done ].
eapply contextual_step_red_nsteps; done.
+ exists 0, e, h. split_and!; [ lia | | ].
* split; [constructor | ].
apply val_irreducible. by apply is_val_spec.
* simpl. by eapply contextual_step_red_nsteps.
Qed.
(** * Heap execution lemmas *)
Lemma new_step_inv v e e' σ σ' :
to_val e = Some v
base_step (New e, σ) (e', σ')
l, e' = (Lit $ LitLoc l) σ' = init_heap l 1 v σ σ !! l = None.
Proof.
intros <-%of_to_val.
inversion 1; subst.
rewrite to_of_val in H5. injection H5 as [= ->].
eauto.
Qed.
Lemma new_nsteps_inv n v e e' σ σ' :
to_val e = Some v
red_nsteps n (New e) σ e' σ'
(n = 1 base_step (New e, σ) (e', σ')).
Proof.
intros <-%of_to_val [Hsteps Hirred%not_reducible].
inversion Hsteps; subst.
- exfalso; apply Hirred. eapply base_reducible_reducible. eexists _, _. eapply new_fresh.
- destruct y.
eapply base_reducible_contextual_step in H.
2: { eexists _, _. apply new_fresh. }
inversion H0; subst.
{ eauto. }
eapply new_step_inv in H; last apply to_of_val.
destruct H as (l & -> & -> & ?).
destruct y. apply val_stuck in H1. done.
Qed.
Lemma load_step_inv e v σ e' σ' :
to_val e = Some v
base_step (Load e, σ) (e', σ')
(l : loc) v', v = #l σ !! l = Some v' e' = of_val v' σ' = σ.
Proof.
intros <-%of_to_val.
inversion 1; subst.
symmetry in H0. apply of_val_lit in H0 as ->.
eauto 8.
Qed.
Definition sub_redexes_are_values (e : expr) :=
K e', e = fill K e' to_val e' = None K = empty_ectx.
Lemma contextual_base_reducible e σ :
reducible e σ sub_redexes_are_values e base_reducible e σ.
Proof.
intros (e' & σ' & Hstep) ?. inversion Hstep; subst.
assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck.
rewrite fill_empty /base_reducible; eauto.
Qed.
Ltac solve_sub_redexes_are_values :=
let K := fresh "K" in
let e' := fresh "e'" in
let Heq := fresh "Heq" in
let Hv := fresh "Hv" in
let IH := fresh "IH" in
let Ki := fresh "Ki" in
let Ki' := fresh "Ki'" in
intros K e' Heq Hv;
destruct K as [ | Ki K]; first (done);
exfalso; induction K as [ | Ki' K IH] in e', Ki, Hv, Heq |-*;
[destruct Ki; inversion Heq; subst; simplify_val; cbn in *; congruence
| eapply IH; first (by rewrite Heq);
apply fill_item_no_val; done].
Lemma load_nsteps_inv n v e e' σ σ' :
to_val e = Some v
red_nsteps n (Load e) σ e' σ'
(n = 0 σ' = σ e' = Load e ¬ reducible (Load e) σ)
(n = 1 base_step (Load e, σ) (e', σ')).
Proof.
intros <-%of_to_val [Hsteps Hirred%not_reducible].
inversion Hsteps; subst.
- by left.
- right. destruct y.
eapply base_reducible_contextual_step in H.
2: { eapply contextual_base_reducible; [eexists _, _; done | solve_sub_redexes_are_values]. }
inversion H0; subst.
{ eauto. }
eapply load_step_inv in H as (l & ? & -> & ? & -> & ->); last apply to_of_val.
destruct y. apply val_stuck in H1. simplify_val. done.
Qed.
(** useful derived lemma when we know upfront that l satisfies some invariant [P] *)
Lemma load_nsteps_inv' n l e e' σ σ' (P : val Prop) :
to_val e = Some (LitV $ LitLoc l)
( v', σ !! l = Some v' P v')
red_nsteps n (Load e) σ e' σ'
v' : val, n = 1 e' = v' σ' = σ σ !! l = Some v' P v'.
Proof.
intros <-%of_to_val (v' & Hlook & HP) Hred.
eapply load_nsteps_inv in Hred; last done.
destruct Hred as [(-> & -> & -> & Hnred) | (-> & Hstep)].
- exfalso; eapply Hnred. eexists v', _.
eapply base_contextual_step. econstructor. done.
- exists v'. split; first done.
eapply load_step_inv in Hstep; last done.
destruct Hstep as (l' & v'' & [= <-] & ? & -> & ->).
split; first by simplify_option_eq.
split; last done. econstructor; done.
Qed.
Lemma store_step_inv v1 v2 σ e' σ' :
base_step (Store (of_val v1) (of_val v2), σ) (e', σ')
(l : loc) v', v1 = #l σ !! l = Some v' e' = Lit LitUnit σ' = <[l := v2]> σ.
Proof.
inversion 1; subst.
symmetry in H0. apply of_val_lit in H0 as ->.
simplify_val. simplify_option_eq.
eauto 8.
Qed.
Lemma store_nsteps_inv n v1 v2 e' σ σ' :
red_nsteps n (Store (of_val v1) (of_val v2)) σ e' σ'
(n = 0 σ' = σ e' = Store (of_val v1) (of_val v2) ¬ reducible (Store (of_val v1) (of_val v2)) σ)
(n = 1 base_step (Store (of_val v1) (of_val v2), σ) (e', σ')).
Proof.
intros [Hsteps Hirred%not_reducible].
inversion Hsteps; subst.
- by left.
- right. destruct y.
eapply base_reducible_contextual_step in H.
2: { eapply contextual_base_reducible; [eexists _, _; done | solve_sub_redexes_are_values]. }
inversion H0; subst.
{ eauto. }
apply store_step_inv in H as (l & ? & -> & ? & -> & ->).
destruct y. apply val_stuck in H1. simplify_val. done.
Qed.
Lemma store_nsteps_inv' n e1 e2 v0 v l e' σ σ' :
to_val e1 = Some (LitV $ LitLoc l)
to_val e2 = Some v
σ !! l = Some v0
red_nsteps n (Store e1 e2) σ e' σ'
n = 1 e' = Lit $ LitUnit σ' = <[l := v ]> σ.
Proof.
intros <-%of_to_val <-%of_to_val Hlook Hred%store_nsteps_inv.
destruct Hred as [(-> & -> & -> & Hnred) | (-> & Hb)].
- exfalso; eapply Hnred.
eexists #(), _.
eapply base_contextual_step. econstructor; [done | apply to_of_val ].
- eapply store_step_inv in Hb. destruct Hb as (l' & v' & [= <-] & Hlook' & -> & ->).
simplify_option_eq. done.
Qed.
(** Additionally useful stepping lemmas *)
Lemma app_step_r (e1 e2 e2': expr) h h' :
contextual_step (e2, h) (e2', h') contextual_step (e1 e2, h) (e1 e2', h').
Proof. by apply (fill_contextual_step [AppRCtx _]). Qed.
Lemma app_step_l (e1 e1' e2: expr) h h' :
contextual_step (e1, h) (e1', h') is_val e2 contextual_step (e1 e2, h) (e1' e2, h').
Proof.
intros ? (v & Hv)%is_val_spec.
rewrite <-(of_to_val _ _ Hv).
by apply (fill_contextual_step [AppLCtx _]).
Qed.
Lemma app_step_beta (x: string) (e e': expr) h :
is_val e' is_closed [x] e contextual_step ((λ: x, e)%E e', h) (lang.subst x e' e, h).
Proof.
intros Hval Hclosed. eapply base_contextual_step, BetaS; eauto.
Qed.
Lemma unroll_roll_step (e: expr) h :
is_val e contextual_step ((unroll (roll e))%E, h) (e, h).
Proof.
intros ?; by eapply base_contextual_step, UnrollS.
Qed.
Lemma fill_reducible K e h :
reducible e h reducible (fill K e) h.
Proof.
intros (e' & h' & Hstep).
exists (fill K e'), h'. eapply fill_contextual_step. done.
Qed.
Lemma reducible_contextual_step_case K e e' h1 h2 :
contextual_step (fill K e, h1) (e', h2)
reducible e h1
e'', e' = fill K e'' contextual_step (e, h1) (e'', h2).
Proof.
intros [ | Hval]%contextual_ectx_step_case Hred; first done.
exfalso. apply is_val_spec in Hval as (v & Hval).
apply reducible_not_val in Hred. congruence.
Qed.
(** Contextual lifting lemmas for deterministic reduction *)
Tactic Notation "lift_det" uconstr(ctx) :=
intros;
let Hs := fresh in
match goal with
| H : det_step _ _ |- _ => destruct H as [? Hs]
end;
simplify_val; econstructor;
[intros; by eapply (fill_reducible ctx) |
intros ? ? ? (? & -> & [-> ->]%Hs)%(reducible_contextual_step_case ctx); done ].
Lemma det_step_pair_r e1 e2 e2' :
det_step e2 e2'
det_step (e1, e2)%E (e1, e2')%E.
Proof. lift_det [PairRCtx _]. Qed.
Lemma det_step_pair_l e1 e1' e2 :
is_val e2
det_step e1 e1'
det_step (e1, e2)%E (e1', e2)%E.
Proof. lift_det [PairLCtx _]. Qed.
Lemma det_step_binop_r e1 e2 e2' op :
det_step e2 e2'
det_step (BinOp op e1 e2)%E (BinOp op e1 e2')%E.
Proof. lift_det [BinOpRCtx _ _]. Qed.
Lemma det_step_binop_l e1 e1' e2 op :
is_val e2
det_step e1 e1'
det_step (BinOp op e1 e2)%E (BinOp op e1' e2)%E.
Proof. lift_det [BinOpLCtx _ _]. Qed.
Lemma det_step_if e e' e1 e2 :
det_step e e'
det_step (If e e1 e2)%E (If e' e1 e2)%E.
Proof. lift_det [IfCtx _ _]. Qed.
Lemma det_step_app_r e1 e2 e2' :
det_step e2 e2'
det_step (App e1 e2)%E (App e1 e2')%E.
Proof. lift_det [AppRCtx _]. Qed.
Lemma det_step_app_l e1 e1' e2 :
is_val e2
det_step e1 e1'
det_step (App e1 e2)%E (App e1' e2)%E.
Proof. lift_det [AppLCtx _]. Qed.
Lemma det_step_snd_lift e e' :
det_step e e'
det_step (Snd e)%E (Snd e')%E.
Proof. lift_det [SndCtx]. Qed.
Lemma det_step_fst_lift e e' :
det_step e e'
det_step (Fst e)%E (Fst e')%E.
Proof. lift_det [FstCtx]. Qed.
Lemma det_step_store_r e1 e2 e2' :
det_step e2 e2'
det_step (Store e1 e2)%E (Store e1 e2')%E.
Proof. lift_det [StoreRCtx _]. Qed.
Lemma det_step_store_l e1 e1' e2 :
is_val e2
det_step e1 e1'
det_step (Store e1 e2)%E (Store e1' e2)%E.
Proof. lift_det [StoreLCtx _]. Qed.
#[global]
Hint Resolve app_step_r app_step_l app_step_beta unroll_roll_step : core.
#[global]
Hint Extern 1 (is_val _) => (simpl; fast_done) : core.
#[global]
Hint Immediate is_val_of_val : core.
#[global]
Hint Resolve det_step_beta det_step_tbeta det_step_unpack det_step_unop det_step_binop det_step_if_true det_step_if_false det_step_fst det_step_snd det_step_casel det_step_caser det_step_unroll : core.
#[global]
Hint Resolve det_step_pair_r det_step_pair_l det_step_binop_r det_step_binop_l det_step_if det_step_app_r det_step_app_l det_step_snd_lift det_step_fst_lift det_step_store_l det_step_store_r : core.
#[global]
Hint Constructors nsteps : core.
#[global]
Hint Extern 1 (is_val _) => simpl : core.
Ltac do_det_step :=
match goal with
| |- nsteps det_step _ _ _ => econstructor 2; first do_det_step
| |- det_step _ _ => simpl; solve[eauto 10]
end.

@ -0,0 +1,127 @@
From iris Require Import prelude.
From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst tactics execution.
(** * Exercise Sheet 7 *)
(** Exercise 1: Stack (LN Exercise 45) *)
(* We use lists to model our stack *)
Section lists.
Context (A : type).
Definition list_type : type :=
μ: Unit + (A.[ren (+1)] × #0).
Definition nil_val : val :=
RollV (InjLV (LitV LitUnit)).
Definition cons_val (v : val) (xs : val) : val :=
RollV (InjRV (v, xs)).
Definition cons_expr (v : expr) (xs : expr) : expr :=
roll (InjR (v, xs)).
Definition list_case : val :=
Λ, λ: "l" "n" "hf", match: unroll "l" with InjL <> => "n" | InjR "h" => "hf" (Fst "h") (Snd "h") end.
Lemma nil_val_typed Σ n Γ :
type_wf n A
TY Σ; n; Γ nil_val : list_type.
Proof.
intros. solve_typing.
Qed.
Lemma cons_val_typed Σ n Γ (v xs : val) :
type_wf n A
TY Σ; n; Γ v : A
TY Σ; n; Γ xs : list_type
TY Σ; n; Γ cons_val v xs : list_type.
Proof.
intros. simpl. solve_typing.
Qed.
Lemma cons_expr_typed Σ n Γ (x xs : expr) :
type_wf n A
TY Σ; n; Γ x : A
TY Σ; n; Γ xs : list_type
TY Σ; n; Γ cons_expr x xs : list_type.
Proof.
intros. simpl. solve_typing.
Qed.
Lemma list_case_typed Σ n Γ :
type_wf n A
TY Σ; n; Γ list_case : (: list_type.[ren (+1)] #0 (A.[ren(+1)] list_type.[ren (+1)] #0) #0).
Proof.
intros. simpl. solve_typing.
Qed.
End lists.
(* The stack interface *)
Definition stack_t A : type :=
: ((Unit #0) (* new *)
× (#0 A.[ren (+1)] Unit) (* push *)
× (#0 Unit + A.[ren (+1)])) (* pop *)
.
(** We assume an abstract implementation of lists (an example implementation is provided above) *)
Definition list_t (A : type) : type :=
: (#0 (* mynil *)
× (A.[ren (+1)] #0 #0) (* mycons *)
× (: #1 #0 (A.[ren (+2)] #1 #0) #0)) (* mylistcase *)
.
Definition mystack : val :=
(* define your stack implementation, assuming "lc" is a list implementation *)
λ: "lc", #0. (* FIXME *)
Definition make_mystack : val :=
Λ, λ: "lc",
unpack "lc" as "lc" in
#0. (* FIXME *)
Lemma make_mystack_typed Σ n Γ :
TY Σ; n; Γ make_mystack : (: list_t #0 stack_t #0).
Proof.
repeat solve_typing_fast.
Admitted.
(** Exercise 2 (LN Exercise 46): Obfuscated code *)
Definition obf_expr : expr :=
let: "x" := new (λ: "x", "x" + "x") in
let: "f" := (λ: "g", let: "f" := !"x" in "x" <- "g";; "f" #11) in
"f" (λ: "x", "f" (λ: <>, "x")) + "f" (λ: "x", "x" + #9).
(* The following contextual lifting lemma will be helpful *)
Lemma rtc_contextual_step_fill K e e' h h' :
rtc contextual_step (e, h) (e', h')
rtc contextual_step (fill K e, h) (fill K e', h').
Proof.
remember (e, h) as a eqn:Heqa. remember (e', h') as b eqn:Heqb.
induction 1 as [ | ? c ? Hstep ? IH] in e', h', e, h, Heqa, Heqb |-*; subst.
- simplify_eq. done.
- destruct c as (e1, h1).
econstructor 2.
+ apply fill_contextual_step. apply Hstep.
+ apply IH; done.
Qed.
(* You may use the [new_fresh] and [init_heap_singleton] lemmas to allocate locations *)
Lemma obf_expr_eval :
h', rtc contextual_step (obf_expr, ) (of_val #0 (* FIXME: what is the result? *), h').
Proof.
eexists. unfold obf_expr.
(* TODO: exercise *)
Admitted.
(** Exercise 4 (LN Exercise 48): Fibonacci *)
Definition fibonacci : val := #0. (* FIXME *)
Lemma fibonacci_typed Σ n Γ :
TY Σ; n; Γ fibonacci : (Int Int).
Proof.
repeat solve_typing_fast.
Admitted.

@ -0,0 +1,858 @@
From iris.prelude Require Import prelude.
From stdpp Require Export binders strings.
From semantics.ts.systemf_mu_state Require Export locations.
From semantics.lib Require Export maps.
Declare Scope expr_scope.
Declare Scope val_scope.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
(** Expressions and vals. *)
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | MultOp (* Arithmetic *)
| LtOp | LeOp | EqOp. (* Comparison *)
Inductive expr :=
| Lit (l : base_lit)
(* Base lambda calculus *)
| Var (x : string)
| Lam (x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
(* Polymorphism *)
| TApp (e : expr)
| TLam (e : expr)
| Pack (e : expr)
| Unpack (x : binder) (e1 e2 : expr)
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
(* Isorecursive types *)
| Roll (e : expr)
| Unroll (e : expr)
(* State *)
| Load (e : expr)
| Store (e1 e2 : expr)
| New (e : expr)
.
Bind Scope expr_scope with expr.
Inductive val :=
| LitV (l : base_lit)
| LamV (x : binder) (e : expr)
| TLamV (e : expr)
| PackV (v : val)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| RollV (v : val)
.
Bind Scope val_scope with val.
Fixpoint of_val (v : val) : expr :=
match v with
| LitV l => Lit l
| LamV x e => Lam x e
| TLamV e => TLam e
| PackV v => Pack (of_val v)
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| RollV v => Roll (of_val v)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
| Lit l => Some $ LitV l
| Lam x e => Some (LamV x e)
| TLam e => Some (TLamV e)
| Pack e =>
to_val e = (λ v, Some $ PackV v)
| Pair e1 e2 =>
to_val e1 = (λ v1, to_val e2 = (λ v2, Some $ PairV v1 v2))
| InjL e => to_val e = (λ v, Some $ InjLV v)
| InjR e => to_val e = (λ v, Some $ InjRV v)
| Roll e => to_val e = (λ v, Some $ RollV v)
| _ => None
end.
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
Lemma of_to_val e v : to_val e = Some v of_val v = e.
Proof.
revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.
#[export] Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
(** structural computational version *)
Fixpoint is_val (e : expr) : Prop :=
match e with
| Lit l => True
| Lam x e => True
| TLam e => True
| Pack e => is_val e
| Pair e1 e2 => is_val e1 is_val e2
| InjL e => is_val e
| InjR e => is_val e
| Roll e => is_val e
| _ => False
end.
Lemma is_val_spec e : is_val e v, to_val e = Some v.
Proof.
induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | | | ];
simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try naive_solver.
- rewrite IH. intros (v & ->). eauto.
- rewrite IH1 IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
- rewrite IH. intros (v & ->). eauto.
- rewrite IH. intros (v & ->); eauto.
- rewrite IH. intros (v & ->). eauto.
Qed.
Global Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Global Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
Global Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
(** Substitution *)
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Lit _ => e
| Var y => if decide (x = y) then es else Var y
| Lam y e =>
Lam y $ if decide (BNamed x = y) then e else subst x es e
| App e1 e2 => App (subst x es e1) (subst x es e2)
| TApp e => TApp (subst x es e)
| TLam e => TLam (subst x es e)
| Pack e => Pack (subst x es e)
| Unpack y e1 e2 => Unpack y (subst x es e1) (if decide (BNamed x = y) then e2 else subst x es e2)
| UnOp op e => UnOp op (subst x es e)
| BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
| If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
| Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
| Fst e => Fst (subst x es e)
| Snd e => Snd (subst x es e)
| InjL e => InjL (subst x es e)
| InjR e => InjR (subst x es e)
| Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
| Roll e => Roll (subst x es e)
| Unroll e => Unroll (subst x es e)
| Load e => Load (subst x es e)
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| New e => New (subst x es e)
end.
Definition subst' (mx : binder) (es : expr) : expr expr :=
match mx with BNamed x => subst x es | BAnon => id end.
(** The stepping relation *)
Definition un_op_eval (op : un_op) (v : val) : option val :=
match op, v with
| NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
| MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
| _, _ => None
end.
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
match op with
| PlusOp => Some $ LitInt (n1 + n2)
| MinusOp => Some $ LitInt (n1 - n2)
| MultOp => Some $ LitInt (n1 * n2)
| LtOp => Some $ LitBool (bool_decide (n1 < n2))
| LeOp => Some $ LitBool (bool_decide (n1 n2))
| EqOp => Some $ LitBool (bool_decide (n1 = n2))
end%Z.
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
| _, _ => None
end.
Definition heap := gmap loc val.
Fixpoint heap_array (l : loc) (vs : list val) : heap :=
match vs with
| [] =>
| v :: vs' => {[l := v]} heap_array (l + 1) vs'
end.
Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
Proof. by rewrite /heap_array right_id. Qed.
Lemma heap_array_lookup l vs w k :
heap_array l vs !! k = Some w
j, (0 j)%Z k = l + j vs !! (Z.to_nat j) = Some w.
Proof.
revert k l; induction vs as [|v' vs IH]=> l' l /=.
{ rewrite lookup_empty. naive_solver lia. }
rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
- intros [[-> ?] | (Hl & j & ? & -> & ?)].
{ eexists 0. rewrite loc_add_0. naive_solver lia. }
eexists (1 + j)%Z. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; eauto with lia.
- intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
{ rewrite loc_add_0. eauto. }
right. split.
{ rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
{ rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
rewrite Hj /= in Hil.
eexists (j - 1)%Z. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
auto with lia.
Qed.
Lemma heap_array_map_disjoint (h : heap) (l : loc) (vs : list val) :
( i, (0 i)%Z (i < length vs)%Z h !! (l + i) = None)
(heap_array l vs) ## h.
Proof.
intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
Qed.
Definition init_heap (l : loc) (n : Z) (v : val) (σ : heap) : heap :=
heap_array l (replicate (Z.to_nat n) v) σ.
Lemma init_heap_singleton l v σ :
init_heap l 1 v σ = <[l:=v]> σ.
Proof.
rewrite /init_heap /=.
rewrite right_id insert_union_singleton_l. done.
Qed.
Inductive base_step : expr * heap expr * heap Prop :=
| BetaS x e1 e2 e' σ :
is_val e2
e' = subst' x e2 e1
base_step (App (Lam x e1) e2, σ) (e', σ)
| TBetaS e1 σ :
base_step (TApp (TLam e1), σ) (e1, σ)
| UnpackS e1 e2 e' x σ :
is_val e1
e' = subst' x e1 e2
base_step (Unpack x (Pack e1) e2, σ) (e', σ)
| UnOpS op e v v' σ :
to_val e = Some v
un_op_eval op v = Some v'
base_step (UnOp op e, σ) (of_val v', σ)
| BinOpS op e1 v1 e2 v2 v' σ :
to_val e1 = Some v1
to_val e2 = Some v2
bin_op_eval op v1 v2 = Some v'
base_step (BinOp op e1 e2, σ) (of_val v', σ)
| IfTrueS e1 e2 σ :
base_step (If (Lit $ LitBool true) e1 e2, σ) (e1, σ)
| IfFalseS e1 e2 σ :
base_step (If (Lit $ LitBool false) e1 e2, σ) (e2, σ)
| FstS e1 e2 σ :
is_val e1
is_val e2
base_step (Fst (Pair e1 e2), σ) (e1, σ)
| SndS e1 e2 σ :
is_val e1
is_val e2
base_step (Snd (Pair e1 e2), σ) (e2, σ)
| CaseLS e e1 e2 σ :
is_val e
base_step (Case (InjL e) e1 e2, σ) (App e1 e, σ)
| CaseRS e e1 e2 σ :
is_val e
base_step (Case (InjR e) e1 e2, σ) (App e2 e, σ)
| UnrollS e σ :
is_val e
base_step (Unroll (Roll e), σ) (e, σ)
| NewS e v σ l :
σ !! l = None
to_val e = Some v
base_step (New e, σ) (Lit $ LitLoc l, init_heap l 1 v σ)
| LoadS l v σ :
σ !! l = Some v
base_step (Load (Lit $ LitLoc l), σ) (of_val v, σ)
| StoreS l v w e2 σ :
σ !! l = Some v
to_val e2 = Some w
base_step (Store (Lit $ LitLoc l) e2, σ)
(Lit LitUnit, <[l:=w]> σ)
.
(* Misc *)
Lemma is_val_of_val v : is_val (of_val v).
Proof. apply is_val_spec. rewrite to_of_val. eauto. Qed.
(** If [e1] makes a base step to a value under some state [σ1] then any base
step from [e1] under any other state [σ1'] must necessarily be to a value. *)
Lemma base_step_to_val e1 e2 e2' σ1 σ2 σ2' :
base_step (e1, σ1) (e2, σ2)
base_step (e1, σ1) (e2', σ2') is_Some (to_val e2) is_Some (to_val e2').
Proof. inversion 1; inversion 1; naive_solver. Qed.
Lemma new_fresh v σ :
let l := fresh_locs (dom σ) in
base_step (New (of_val v), σ) (Lit $ LitLoc l, init_heap l 1 v σ).
Proof.
intros.
apply NewS.
- apply (not_elem_of_dom).
rewrite -(loc_add_0 l).
by apply fresh_locs_fresh.
- rewrite to_of_val. eauto.
Qed.
(** We define evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (v2 : val)
| AppRCtx (e1 : expr)
| TAppCtx
| PackCtx
| UnpackCtx (x : binder) (e2 : expr)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (v2 : val)
| BinOpRCtx (op : bin_op) (e1 : expr)
| IfCtx (e1 e2 : expr)
| PairLCtx (v2 : val)
| PairRCtx (e1 : expr)
| FstCtx
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (e1 : expr) (e2 : expr)
| UnrollCtx
| RollCtx
| LoadCtx
| StoreRCtx (e1 : expr)
| StoreLCtx (v2 : val)
| NewCtx
.
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx v2 => App e (of_val v2)
| AppRCtx e1 => App e1 e
| TAppCtx => TApp e
| PackCtx => Pack e
| UnpackCtx x e2 => Unpack x e e2
| UnOpCtx op => UnOp op e
| BinOpLCtx op v2 => BinOp op e (of_val v2)
| BinOpRCtx op e1 => BinOp op e1 e
| IfCtx e1 e2 => If e e1 e2
| PairLCtx v2 => Pair e (of_val v2)
| PairRCtx e1 => Pair e1 e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| UnrollCtx => Unroll e
| RollCtx => Roll e
| LoadCtx => Load e
| StoreRCtx e1 => Store e1 e
| StoreLCtx v2 => Store e (of_val v2)
| NewCtx => New e
end.
(** Basic properties about the language *)
Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) is_Some (to_val e).
Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
Lemma fill_item_no_val Ki e :
to_val e = None to_val (fill_item Ki e) = None.
Proof.
intros Hn. destruct (to_val (fill_item _ _ )) eqn:Heq; last done.
edestruct (fill_item_val Ki e) as (? & ?); last simplify_eq.
eauto.
Qed.
Lemma val_base_stuck e1 e2 σ1 σ2 : base_step (e1, σ1) (e2, σ2) to_val e1 = None.
Proof. inversion 1; naive_solver. Qed.
Lemma of_val_lit v l :
of_val v = (Lit l) v = LitV l.
Proof. destruct v; simpl; inversion 1; done. Qed.
Lemma of_val_pair_inv (v v1 v2 : val) :
of_val v = Pair (of_val v1) (of_val v2) v = PairV v1 v2.
Proof.
destruct v; simpl; inversion 1.
apply of_val_inj in H1. apply of_val_inj in H2. subst; done.
Qed.
Lemma of_val_injl_inv (v v' : val) :
of_val v = InjL (of_val v') v = InjLV v'.
Proof.
destruct v; simpl; inversion 1.
apply of_val_inj in H1. subst; done.
Qed.
Lemma of_val_injr_inv (v v' : val) :
of_val v = InjR (of_val v') v = InjRV v'.
Proof.
destruct v; simpl; inversion 1.
apply of_val_inj in H1. subst; done.
Qed.
Ltac simplify_val :=
repeat match goal with
| H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
| H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
| H: to_val ?e = ?v |- _ => is_var e; specialize (of_to_val _ _ H); intros <-; clear H
| H: of_val ?v = Lit ?l |- _ => is_var v; specialize (of_val_lit _ _ H); intros ->; clear H
| |- context[to_val (of_val ?e)] => rewrite to_of_val
end.
Lemma base_ectxi_step_val Ki e e2 σ1 σ2 :
base_step (fill_item Ki e, σ1) (e2, σ2) is_Some (to_val e).
Proof.
revert e2. induction Ki; inversion_clear 1; simplify_option_eq; simplify_val; eauto.
Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None to_val e2 = None
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof.
revert Ki1. induction Ki2; intros Ki1; induction Ki1; try naive_solver eauto with f_equal.
all: intros ?? Heq; injection Heq; intros ??; simplify_eq; simplify_val; naive_solver.
Qed.
Section contexts.
Notation ectx := (list ectx_item).
Definition empty_ectx : ectx := [].
Definition comp_ectx : ectx ectx ectx := flip (++).
Definition fill (K : ectx) (e : expr) : expr := foldl (flip fill_item) e K.
Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
Proof. apply foldl_app. Qed.
Lemma fill_empty e : fill empty_ectx e = e.
Proof. done. Qed.
Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
Proof. unfold fill, comp_ectx; simpl. by rewrite foldl_app. Qed.
Global Instance fill_inj K : Inj (=) (=) (fill K).
Proof. induction K as [|Ki K IH]; unfold Inj; naive_solver. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e).
Proof.
induction K as [|Ki K IH] in e |-*; [ done |]. by intros ?%IH%fill_item_val.
Qed.
Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
End contexts.
(** Contextual steps *)
Inductive contextual_step : expr * heap expr * heap Prop :=
Ectx_step K e1 e2 σ1 σ2 e1' e2' :
e1 = fill K e1' e2 = fill K e2'
base_step (e1', σ1) (e2', σ2) contextual_step (e1, σ1) (e2, σ2).
Lemma base_contextual_step e1 e2 σ1 σ2 :
base_step (e1, σ1) (e2, σ2) contextual_step (e1, σ1) (e2, σ2).
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
Lemma fill_contextual_step K e1 e2 σ1 σ2 :
contextual_step (e1, σ1) (e2, σ2) contextual_step (fill K e1, σ1) (fill K e2, σ2).
Proof.
inversion 1; subst.
rewrite !fill_comp. by econstructor.
Qed.
(** *** closedness *)
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x X)
| Lam x e => is_closed (x :b: X) e
| Unpack x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
| Lit _ => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | TApp e | TLam e | Pack e | Roll e | Unroll e | Load e | New e=> is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 => is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
end.
(** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
Proof. unfold closed. apply _. Qed.
#[export] Instance closed_dec X e : Decision (closed X e).
Proof. unfold closed. apply _. Defined.
(** closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e X Y is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed [] e is_closed X e.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x es :
is_closed [] es is_closed (x :: X) e is_closed X (subst x es e).
Proof.
intros ?.
induction e in X |-*; simpl; intros ?; destruct_and?; split_and?; simplify_option_eq;
try match goal with
| H : ¬(_ _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_do_subst' X e x es :
is_closed [] es is_closed (x :b: X) e is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.
Lemma closed_is_closed X e :
is_closed X e = true closed X e.
Proof.
unfold closed. split.
- apply Is_true_eq_left.
- apply Is_true_eq_true.
Qed.
(** Substitution lemmas *)
Lemma subst_is_closed X e x es : is_closed X e x X subst x es e = e.
Proof.
induction e in X |-*; simpl; rewrite ?bool_decide_spec ?andb_True; intros ??;
repeat case_decide; simplify_eq; simpl; f_equal; intuition eauto with set_solver.
Qed.
Lemma subst_is_closed_nil e x es : is_closed [] e subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
Lemma subst'_is_closed_nil e x es : is_closed [] e subst' x es e = e.
Proof. intros. destruct x as [ | x]. { done. } by apply subst_is_closed_nil. Qed.
(** ** More on the contextual semantics *)
Definition base_reducible (e : expr) σ :=
e' σ', base_step (e, σ) (e', σ').
Definition base_irreducible (e : expr) σ :=
e' σ', ¬base_step (e, σ) (e', σ').
Definition base_stuck (e : expr) σ :=
to_val e = None base_irreducible e σ.
(** Given a base redex [e1_redex] somewhere in a term, and another
decomposition of the same term into [fill K' e1'] such that [e1'] is not
a value, then the base redex context is [e1']'s context [K'] filled with
another context [K'']. In particular, this implies [e1 = fill K''
e1_redex] by [fill_inj], i.e., [e1]' contains the base redex.)
*)
Lemma step_by_val K' K_redex e1' e1_redex e2 σ1 σ2 :
fill K' e1' = fill K_redex e1_redex
to_val e1' = None
base_step (e1_redex, σ1) (e2, σ2)
K'', K_redex = comp_ectx K' K''.
Proof.
rename K' into K. rename K_redex into K'.
rename e1' into e1. rename e1_redex into e1'.
intros Hfill Hred Hstep; revert K' Hfill.
induction K as [|Ki K IH] using rev_ind; simpl; intros K' Hfill; eauto using app_nil_r.
destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
{ rewrite fill_app in Hstep. apply base_ectxi_step_val in Hstep.
apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
rewrite !fill_app in Hfill; simpl in Hfill.
assert (Ki = Ki') as ->.
{ eapply fill_item_no_val_inj, Hfill.
- by apply fill_not_val.
- apply fill_not_val. eauto using val_base_stuck.
}
simplify_eq. destruct (IH K') as [K'' ->]; auto.
exists K''. unfold comp_ectx; simpl. rewrite assoc; done.
Qed.
(** If [fill K e] takes a base step, then either [e] is a value or [K] is
the empty evaluation context. In other words, if [e] is not a value
wrapping it in a context does not add new base redex positions. *)
Lemma base_ectx_step_val K e e2 σ1 σ2 :
base_step (fill K e, σ1) (e2, σ2) is_Some (to_val e) K = empty_ectx.
Proof.
destruct K as [|Ki K _] using rev_ind; simpl; [by auto|].
rewrite fill_app; simpl.
intros ?%base_ectxi_step_val; eauto using fill_val.
Qed.
(** If a [contextual_step] preserving a surrounding context [K] happens,
the reduction happens entirely below the context. *)
Lemma contextual_step_ectx_inv K e e' σ1 σ2 :
to_val e = None
contextual_step (fill K e, σ1) (fill K e', σ2)
contextual_step (e, σ1) (e', σ2).
Proof.
intros ? Hcontextual.
inversion Hcontextual as [??????? Heq1 Heq2 ?]; subst.
eapply step_by_val in H as (K'' & Heq); [ | done | done].
subst K0.
rewrite <-fill_comp in Heq1. rewrite <-fill_comp in Heq2.
apply fill_inj in Heq1. apply fill_inj in Heq2. subst.
econstructor; done.
Qed.
Lemma contextual_ectx_step_case K e e' σ1 σ2 :
contextual_step (fill K e, σ1) (e', σ2)
( e'', e' = fill K e'' contextual_step (e, σ1) (e'', σ2)) 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.
Lemma base_reducible_contextual_step_ectx K e1 e2 σ1 σ2 :
base_reducible e1 σ1
contextual_step (fill K e1, σ1) (e2, σ2)
e2', e2 = fill K e2' base_step (e1, σ1) (e2', σ2).
Proof.
intros (e2''&σ2'' & HhstepK) Hctx.
inversion Hctx as [K' ???? e1' e2' HKe1 -> Hstep].
edestruct (step_by_val K) as [K'' ?];
eauto using val_base_stuck; simplify_eq/=.
rewrite <-fill_comp in HKe1; simplify_eq.
exists (fill K'' e2'). rewrite fill_comp; split; [done | ].
apply base_ectx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
{ apply val_base_stuck in Hstep; simplify_eq. }
by rewrite !fill_empty.
Qed.
Lemma base_reducible_contextual_step e1 e2 σ1 σ2 :
base_reducible e1 σ1
contextual_step (e1, σ1) (e2, σ2)
base_step (e1, σ1) (e2, σ2).
Proof.
intros.
edestruct (base_reducible_contextual_step_ectx empty_ectx) as (?&?&?);
rewrite ?fill_empty; eauto.
by simplify_eq; rewrite fill_empty.
Qed.
(** *** Reducibility *)
Definition reducible (e : expr) σ :=
e' σ', contextual_step (e, σ) (e', σ').
Definition irreducible (e : expr) σ :=
e' σ', ¬contextual_step (e, σ) (e', σ').
Definition stuck (e : expr) σ :=
to_val e = None irreducible e σ.
Definition not_stuck (e : expr) σ :=
is_Some (to_val e) reducible e σ.
Lemma base_step_not_stuck e e' σ σ' : base_step (e, σ) (e', σ') not_stuck e σ.
Proof. unfold not_stuck, reducible; simpl. eauto 10 using base_contextual_step. Qed.
Lemma val_stuck e e' σ σ' : contextual_step (e, σ) (e', σ') to_val e = None.
Proof.
inversion 1 as [??????? -> -> ?%val_base_stuck].
apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
Qed.
Lemma not_reducible e σ : ¬reducible e σ irreducible e σ.
Proof. unfold reducible, irreducible. naive_solver. Qed.
Lemma reducible_not_val e σ : reducible e σ to_val e = None.
Proof. intros (?&?&?). eauto using val_stuck. Qed.
Lemma val_irreducible e σ : is_Some (to_val e) irreducible e σ.
Proof. intros [??] ?? ?%val_stuck. by destruct (to_val e). Qed.
Lemma irreducible_fill K e σ :
irreducible (fill K e) σ irreducible e σ.
Proof.
intros Hirred e' σ' Hstep.
eapply Hirred. by apply fill_contextual_step.
Qed.
Lemma base_reducible_reducible e σ :
base_reducible e σ reducible e σ.
Proof. intros (e' & σ' & Hhead). exists e', σ'. by apply base_contextual_step. Qed.
(* we derive a few lemmas about contextual steps *)
Lemma contextual_step_app_l e1 e1' e2 σ1 σ2 :
is_val e2
contextual_step (e1, σ1) (e1', σ2)
contextual_step (App e1 e2, σ1) (App e1' e2, σ2).
Proof.
intros [v <-%of_to_val]%is_val_spec Hcontextual.
by eapply (fill_contextual_step [AppLCtx _]).
Qed.
Lemma contextual_step_app_r e1 e2 e2' σ1 σ2 :
contextual_step (e2, σ1) (e2', σ2)
contextual_step (App e1 e2, σ1) (App e1 e2', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [AppRCtx e1]).
Qed.
Lemma contextual_step_tapp e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (TApp e, σ1) (TApp e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [TAppCtx]).
Qed.
Lemma contextual_step_pack e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Pack e, σ1) (Pack e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [PackCtx]).
Qed.
Lemma contextual_step_unpack x e e' e2 σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Unpack x e e2, σ1) (Unpack x e' e2, σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [UnpackCtx x e2]).
Qed.
Lemma contextual_step_unop op e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (UnOp op e, σ1) (UnOp op e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [UnOpCtx op]).
Qed.
Lemma contextual_step_binop_l op e1 e1' e2 σ1 σ2 :
is_val e2
contextual_step (e1, σ1) (e1', σ2)
contextual_step (BinOp op e1 e2, σ1) (BinOp op e1' e2, σ2).
Proof.
intros [v <-%of_to_val]%is_val_spec Hcontextual.
by eapply (fill_contextual_step [BinOpLCtx op v]).
Qed.
Lemma contextual_step_binop_r op e1 e2 e2' σ1 σ2 :
contextual_step (e2, σ1) (e2', σ2)
contextual_step (BinOp op e1 e2, σ1) (BinOp op e1 e2', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [BinOpRCtx op e1]).
Qed.
Lemma contextual_step_if e e' e1 e2 σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (If e e1 e2, σ1) (If e' e1 e2, σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [IfCtx e1 e2]).
Qed.
Lemma contextual_step_pair_l e1 e1' e2 σ1 σ2 :
is_val e2
contextual_step (e1, σ1) (e1', σ2)
contextual_step (Pair e1 e2, σ1) (Pair e1' e2, σ2).
Proof.
intros [v <-%of_to_val]%is_val_spec Hcontextual.
by eapply (fill_contextual_step [PairLCtx v]).
Qed.
Lemma contextual_step_pair_r e1 e2 e2' σ1 σ2 :
contextual_step (e2, σ1) (e2', σ2)
contextual_step (Pair e1 e2, σ1) (Pair e1 e2', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [PairRCtx e1]).
Qed.
Lemma contextual_step_fst e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Fst e, σ1) (Fst e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [FstCtx]).
Qed.
Lemma contextual_step_snd e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Snd e, σ1) (Snd e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [SndCtx]).
Qed.
Lemma contextual_step_injl e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (InjL e, σ1) (InjL e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [InjLCtx]).
Qed.
Lemma contextual_step_injr e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (InjR e, σ1) (InjR e', σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [InjRCtx]).
Qed.
Lemma contextual_step_case e e' e1 e2 σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Case e e1 e2, σ1) (Case e' e1 e2, σ2).
Proof.
intros Hcontextual.
by eapply (fill_contextual_step [CaseCtx e1 e2]).
Qed.
Lemma contextual_step_roll e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Roll e, σ1) (Roll e', σ2).
Proof. by apply (fill_contextual_step [RollCtx]). Qed.
Lemma contextual_step_unroll e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Unroll e, σ1) (Unroll e', σ2).
Proof. by apply (fill_contextual_step [UnrollCtx]). Qed.
Lemma contextual_step_new e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (New e, σ1) (New e', σ2).
Proof. by apply (fill_contextual_step [NewCtx]). Qed.
Lemma contextual_step_load e e' σ1 σ2 :
contextual_step (e, σ1) (e', σ2)
contextual_step (Load e, σ1) (Load e', σ2).
Proof. by apply (fill_contextual_step [LoadCtx]). Qed.
Lemma contextual_step_store_r e1 e2 e2' σ1 σ2 :
contextual_step (e2, σ1) (e2', σ2)
contextual_step (Store e1 e2, σ1) (Store e1 e2', σ2).
Proof. by apply (fill_contextual_step [StoreRCtx _]). Qed.
Lemma contextual_step_store_l e1 e1' e2 σ1 σ2 :
is_val e2
contextual_step (e1, σ1) (e1', σ2)
contextual_step (Store e1 e2, σ1) (Store e1' e2, σ2).
Proof.
intros [v <-%of_to_val]%is_val_spec Hcontextual.
by eapply (fill_contextual_step [StoreLCtx _]).
Qed.
#[export]
Hint Resolve
contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
contextual_step_pack contextual_step_pair_l contextual_step_pair_r contextual_step_snd contextual_step_tapp
contextual_step_tapp contextual_step_unop contextual_step_unpack contextual_step_roll contextual_step_unroll
contextual_step_new contextual_step_load contextual_step_store_r contextual_step_store_l : core.

@ -0,0 +1,46 @@
From stdpp Require Import countable numbers gmap.
Record loc := Loc { loc_car : Z }.
Add Printing Constructor loc.
Global Instance loc_eq_decision : EqDecision loc.
Proof. solve_decision. Defined.
Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
Global Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation. done. Qed.
Definition loc_add (l : loc) (off : Z) : loc :=
{| loc_car := loc_car l + off|}.
Notation "l +ₗ off" :=
(loc_add l off) (at level 50, left associativity) : stdpp_scope.
Lemma loc_add_assoc l i j : l + i + j = l + (i + j).
Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed.
Lemma loc_add_0 l : l + 0 = l.
Proof. destruct l; unfold loc_add; simpl; f_equal; lia. Qed.
Global Instance loc_add_inj l : Inj eq eq (loc_add l).
Proof. destruct l; unfold Inj, loc_add; simpl; intros; simplify_eq; lia. Qed.
Definition fresh_locs (ls : gset loc) : loc :=
{| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}.
Lemma fresh_locs_fresh ls i :
(0 i)%Z fresh_locs ls + i ls.
Proof.
intros Hi. cut ( l, l ls loc_car l < loc_car (fresh_locs ls) + i)%Z.
{ intros help Hf%help. simpl in *. lia. }
apply (set_fold_ind_L (λ r ls, l, l ls (loc_car l < r + i)%Z));
set_solver by eauto with lia.
Qed.
Global Opaque fresh_locs.

File diff suppressed because it is too large Load Diff

@ -0,0 +1,113 @@
From semantics.ts.systemf_mu_state Require Export lang.
Set Default Proof Using "Type".
(** Coercions to make programs easier to type. *)
Coercion of_val : val >-> expr.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion Var : string >-> expr.
(** Define some derived forms. *)
Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
Notation "# l" := (Lit l%Z%E%stdpp) (at level 8, format "# l") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%binder e1 x2%binder e2)
(e0, x1, e1, x2, e2 at level 200,
format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%binder e2 x1%binder e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Notation "()" := LitUnit : val_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope.
(*Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.*)
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (LamV x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200,
format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope.
Notation "'Λ' , e" := (TLam e%E)
(at level 200, e at level 200,
format "'[' 'Λ' , '/ ' e ']'") : expr_scope.
Notation "'Λ' , e" := (TLamV e%E)
(at level 200, e at level 200,
format "'[' 'Λ' , '/ ' e ']'") : val_scope.
(* the [e] always needs to be paranthesized, due to the level
(chosen to make this cooperate with the [App] coercion) *)
Notation "e '<>'" := (TApp e%E)
(at level 10) : expr_scope.
(*Check ((Λ, #4) <>)%E.*)
(*Check (((λ: "x", "x") #5) <>)%E.*)
Notation "'pack' e" := (Pack e%E)
(at level 200, e at level 200) : expr_scope.
Notation "'pack' v" := (PackV v%V)
(at level 200, v at level 200) : val_scope.
Notation "'unpack' e1 'as' x 'in' e2" := (Unpack x%binder e1%E e2%E)
(at level 200, e1, e2 at level 200, x at level 1) : expr_scope.
Notation "'roll' e" := (Roll e%E)
(at level 200, e at level 200) : expr_scope.
Notation "'roll' v" := (RollV v%E)
(at level 200, v at level 200) : val_scope.
Notation "'unroll' e" := (Unroll e%E)
(at level 200, e at level 200) : expr_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'new' e" := (New e%E) (at level 10) : expr_scope.
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Definition assert (e : expr) : expr :=
if: e then #LitUnit else (#0 #0).
Definition Or (e1 e2 : expr) : expr :=
if: e1 then #true else e2.
Definition And (e1 e2 : expr) : expr :=
if: e1 then e2 else #false.
Notation "e1 '||' e2" := (Or e1 e2) : expr_scope.
Notation "e1 '&&' e2" := (And e1 e2) : expr_scope.

@ -0,0 +1,279 @@
From stdpp Require Import prelude.
From iris Require Import prelude.
From semantics.lib Require Import facts.
From semantics.ts.systemf_mu_state 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)
| Load e => Load (subst_map xs e)
| Store e1 e2 => Store (subst_map xs e1) (subst_map xs e2)
| New e => New (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 :
subst_is_closed X θ
closed (X ++ elements (dom θ)) e
closed X (subst_map θ e).
Proof.
induction e in X, θ |-*; eauto.
all: try solve [intros; simplify_closed; naive_solver].
- unfold subst_map.
destruct (θ !! x) eqn:Heq.
+ intros Hcl _. eapply Hcl; done.
+ intros _ Hcl.
apply closed_is_closed in Hcl.
apply bool_decide_eq_true in Hcl.
apply elem_of_app in Hcl.
destruct Hcl as [ | H].
* apply closed_is_closed. by apply bool_decide_eq_true.
* apply elem_of_elements in H.
by apply not_elem_of_dom in Heq.
- intros. simplify_closed.
eapply IHe.
+ destruct x as [ | x]; simpl; first done.
intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
eapply is_closed_weaken; first done.
by apply list_subseteq_cons_r.
+ eapply is_closed_weaken; first done.
simpl. destruct x as [ | x]; first done; simpl.
apply list_subseteq_cons_l.
apply stdpp.sets.elem_of_subseteq.
intros y; simpl. rewrite elem_of_cons !elem_of_app.
intros [ | Helem]; first naive_solver.
destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
apply elem_of_elements in Helem; done.
- intros. simplify_closed. { naive_solver. }
(* same proof as for lambda *)
eapply IHe2.
+ destruct x as [ | x]; simpl; first done.
intros y e'. rewrite lookup_delete_Some. intros (? & Hlook%H).
eapply is_closed_weaken; first done.
by apply list_subseteq_cons_r.
+ eapply is_closed_weaken; first done.
simpl. destruct x as [ | x]; first done; simpl.
apply list_subseteq_cons_l.
apply stdpp.sets.elem_of_subseteq.
intros y; simpl. rewrite elem_of_cons !elem_of_app.
intros [ | Helem]; first naive_solver.
destruct (decide (x = y)) as [<- | Hneq]; first naive_solver.
right. right. apply elem_of_elements. rewrite dom_delete elem_of_difference elem_of_singleton.
apply elem_of_elements in Helem; done.
Qed.

@ -0,0 +1,91 @@
From stdpp Require Import gmap base relations.
From iris Require Import prelude.
From semantics.lib Require Export facts maps sets.
From semantics.ts.systemf_mu_state Require Export lang notation parallel_subst types.
Ltac map_solver :=
repeat match goal with
| |- ( _) !! _ = Some _ =>
rewrite fmap_insert
| |- <[ ?p := _ ]> _ !! ?p = Some _ =>
apply lookup_insert
| |- <[ _ := _ ]> _ !! _ = Some _ =>
rewrite lookup_insert_ne; [ | congruence]
end.
Ltac solve_typing_step := idtac.
Ltac solve_typing :=
intros;
repeat (asimpl; solve_typing_step).
Ltac solve_typing_fast :=
intros;
repeat (solve_typing_step).
Ltac solve_typing_step ::=
match goal with
| |- TY _; _ ; _ ?e : ?A => first [eassumption | econstructor]
(* heuristic to solve tapp goals where we need to pick the right type for the substitution *)
| |- TY _ ; _ ; _ ?e <> : ?A => eapply typed_tapp'; [solve_typing | | asimpl; reflexivity]
| |- TY _ ; _ ; _ Unroll ?e : ?A => eapply typed_unroll'; [solve_typing | asimpl; reflexivity]
| |- bin_op_typed _ _ _ _ => econstructor
| |- un_op_typed _ _ _ _ => econstructor
| |- type_wf _ ?e => assert_fails (is_evar e); eassumption
| |- type_wf _ ?e => assert_fails (is_evar e); econstructor
| |- type_wf _ (subst _ ?A) => eapply type_wf_subst; [ | intros; simpl]
| |- type_wf _ ?e => assert_fails (is_evar e); eapply type_wf_mono; [eassumption | lia]
(* conditions spawned by the tyvar case of [type_wf] *)
| |- _ < _ => simpl; lia
(* conditions spawned by the variable case *)
| |- _ !! _ = Some _ => map_solver
end.
Tactic Notation "unify_type" uconstr(A) :=
match goal with
| |- TY ?Σ; ?n; ?Γ ?e : ?B => unify A B
end.
Tactic Notation "replace_type" uconstr(A) :=
match goal with
| |- TY ?Σ; ?n; ?Γ ?e : ?B => replace B%ty with A%ty; cycle -1; first try by asimpl
end.
Ltac simplify_list_elem :=
simpl;
repeat match goal with
| |- ?x ?y :: ?l => apply elem_of_cons; first [left; reflexivity | right]
| |- _ [] => apply not_elem_of_nil
| |- _ _ :: _ => apply not_elem_of_cons; split
end; try fast_done.
Ltac simplify_list_subseteq :=
simpl;
repeat match goal with
| |- ?x :: _ ?x :: _ => apply list_subseteq_cons_l
| |- ?x :: _ _ => apply list_subseteq_cons_elem; first solve [simplify_list_elem]
| |- elements _ elements _ => apply elements_subseteq; set_solver
| |- [] _ => apply list_subseteq_nil
| |- ?x :b: _ ?x :b: _ => apply list_subseteq_cons_binder
(* NOTE: this might make the goal unprovable *)
(*| |- elements _ ⊆ _ :: _ => apply list_subseteq_cons_r*)
end;
try fast_done.
(* Try to solve [is_closed] goals using a number of heuristics (that shouldn't make the goal unprovable) *)
Ltac simplify_closed :=
simpl; intros;
repeat match goal with
| |- closed _ _ => unfold closed; simpl
| |- Is_true (is_closed [] _) => first [assumption | done]
| |- Is_true (is_closed _ (lang.subst _ _ _)) => rewrite subst_is_closed_nil; last solve[simplify_closed]
| |- Is_true (is_closed ?X ?v) => assert_fails (is_evar X); eapply is_closed_weaken
| |- Is_true (is_closed _ _) => eassumption
| |- Is_true (_ && true) => rewrite andb_true_r
| |- Is_true (true && _) => rewrite andb_true_l
| |- Is_true (?a && ?a) => rewrite andb_diag
| |- Is_true (_ && _) => simpl; rewrite !andb_True; split_and!
| |- _ ?A => match type of A with | list _ => simplify_list_subseteq end
| |- _ ?A => match type of A with | list _ => simplify_list_elem end
| |- _ _ => congruence
| H : closed _ _ |- _ => unfold closed in H; simpl in H
| H: Is_true (_ && _) |- _ => simpl in H; apply andb_True in H
| H : _ _ |- _ => destruct H
| |- Is_true (bool_decide (_ _)) => apply bool_decide_pack; set_solver
end; try fast_done.

File diff suppressed because it is too large Load Diff
Loading…
Cancel
Save