Commit 7ebb1345 authored by Dan Frumin's avatar Dan Frumin

Do some cleaning up

parent 794299db
From iris.program_logic Require Export ectx_language ectxi_language.
(* From iris_logrel.prelude Require Export base. *)
From iris.algebra Require Export ofe.
From stdpp Require Import strings gmap mapset stringmap.
From iris_logrel.prelude Require Export base.
From iris_logrel.F_mu_ref_conc Require Export binder.
From iris.algebra Require Export ofe.
Module lang.
(** * Syntax and syntactic categories *)
Definition loc := positive.
Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
(** ** Expressions *)
Inductive binop := Add | Sub | Eq | Le | Lt.
Instance binop_dec_eq (op op' : binop) : Decision (op = op').
......@@ -62,6 +63,7 @@ Module lang.
Instance expr_dec_eq (e e' : expr) : Decision (e = e').
Proof. solve_decision. Defined.
(** ** Closed expressions *)
Fixpoint is_closed (X : gset string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x X)
......@@ -90,11 +92,10 @@ Module lang.
fold_leibniz. by subst.
Defined.
(* Definition allClosed (X : gset string) (es : stringmap expr) := (i : string) e', es !! i = Some e' is_closed X e'. *)
(** ** Values *)
Inductive val :=
| RecV (f x : binder) (e : expr) `{!Closed (x :b: f :b: ) e}
| TLamV (e : expr) `{!Closed e}
| TLamV (e : expr) `{!Closed e} (* only closed lambdas are values *)
| UnitV
| NatV (n : nat)
| BoolV (b : bool)
......@@ -176,7 +177,7 @@ Module lang.
refine (cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
Defined.
(** Evaluation contexts *)
(** ** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
......@@ -232,6 +233,7 @@ Module lang.
end.
(** * Substitutions *)
(** Parallel substitutions and some properties are defined in [subst.v] *)
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Var y => if decide (x = y) then es else Var y
......@@ -383,7 +385,7 @@ Module lang.
Canonical Structure exprC := leibnizC expr.
End lang.
(** Language *)
(** Language instance for Iris *)
Program Instance heap_ectxi_lang :
EctxiLanguage
(lang.expr) lang.val lang.ectx_item lang.state := {|
......
......@@ -126,10 +126,8 @@ Section properties.
Qed.
Lemma bin_log_related_rec_l Γ E K f x e e' v t τ
(* (Hclosed : Closed (Rec f x e)) : *)
(Hclosed : Closed (x :b: f :b: ) e) :
(to_val e' = Some v)
(* ({E,E;Γ} (fill K (subst_p (<[x:=v]>{[f:=(RecV f x e)]}) e)) log t : τ) *)
({E,E;Γ} (fill K (subst' f (Rec f x e) (subst' x e' e))) log t : τ)
{E,E;Γ} (fill K (App (Rec f x e) e')) log t : τ.
Proof.
......@@ -413,7 +411,6 @@ Section properties.
iIntros "Hlog".
pose (Φ:=(fun (_ : unit) w => l, w = LocV l l ↦ᵢ v)%I).
iApply (bin_log_related_step_atomic_l Φ); auto.
(* { rewrite_closed. } *)
iMod "Hlog". iModIntro.
iExists ().
iSplitR "Hlog".
......@@ -473,7 +470,6 @@ Section properties.
iIntros (?) "Hlog".
pose (Φ:=(fun (_ : unit) w => w = UnitV l ↦ᵢ v')%I).
iApply (bin_log_related_step_atomic_l Φ); auto.
(* { rewrite_closed. } *)
iMod "Hlog" as (v) "[Hl Hlog]". iModIntro.
iExists ().
iSplitR "Hlog".
......@@ -508,7 +504,6 @@ Section properties.
pose (Φ:=(fun v' w => (v' v1 - w = BoolV false l ↦ᵢ v')
(v' = v1 - w = BoolV true l ↦ᵢ v2))%I).
iApply (bin_log_related_step_atomic_l Φ); auto.
(* { rewrite_closed. } *)
iMod "Hlog" as (v') "[Hl [Hlog_fail Hlog_suc]]". iModIntro.
destruct (decide (v' = v1)).
- (* CAS successful *) subst.
......@@ -545,7 +540,6 @@ Section properties.
iIntros (??) "Hlog".
pose (Φ:=(fun v' w => w = BoolV false l ↦ᵢ v')%I).
iApply (bin_log_related_step_atomic_l Φ); auto.
(* { rewrite_closed. } *)
iMod "Hlog" as (v') "[Hl [% Hlog]]". iModIntro.
iExists v'.
iSplitR "Hlog".
......@@ -580,7 +574,6 @@ Section properties.
iIntros (??) "Hlog".
pose (Φ:=(fun (_ : unit) w => w = BoolV true l ↦ᵢ v2)%I).
iApply (bin_log_related_step_atomic_l Φ); auto.
(* { rewrite_closed. } *)
iMod "Hlog" as "[Hl Hlog]". iModIntro.
iExists ().
iSplitR "Hlog".
......@@ -627,10 +620,8 @@ Section properties.
Lemma bin_log_related_rec_r Γ K E1 E2 f x e e' t v' τ
(Hspec : nclose specN E1)
(* (Hclosed : Closed (Rec f x e)) : *)
(Hclosed : Closed (x :b: f :b: ) e) :
(to_val e' = Some v')
(* {E1,E2;Γ} t log fill K (subst_p (<[x:=v']>{[f:=(RecV f x e)]}) e) : τ *)
{E1,E2;Γ} t log fill K (subst' f (Rec f x e) (subst' x e' e)) : τ
{E1,E2;Γ} t log fill K (App (Rec f x e) e') : τ.
Proof.
......@@ -658,7 +649,6 @@ Section properties.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
rewrite_closed.
{ econstructor; eauto. }
Qed.
......@@ -669,7 +659,6 @@ Section properties.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
rewrite_closed.
{ econstructor; eauto. }
Qed.
......@@ -686,7 +675,6 @@ Section properties.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
rewrite_closed.
{ econstructor; eauto. }
Qed.
......@@ -699,7 +687,6 @@ Section properties.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
rewrite_closed.
{ econstructor; eauto. }
Qed.
......@@ -710,7 +697,7 @@ Section properties.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
econstructor; eauto.
{ econstructor; eauto. }
Qed.
(** Stateful reductions *)
......@@ -742,11 +729,9 @@ Section properties.
iIntros "Hlog".
pose (Φ := (fun w => l, w = (LocV l) l ↦ₛ v)%I).
iApply (bin_log_related_step_r Φ with "[]").
(* { rewrite_closed. } *)
{ cbv[Φ].
iIntros (ρ j K') "#Hs Hj /=".
tp_alloc j as l "Hl". iExists (LocV l).
simpl. tp_normalise j.
iFrame. iExists l. eauto. }
iIntros (v') "He'". iDestruct "He'" as (l) "[% Hl]". subst.
iApply "Hlog".
......@@ -764,7 +749,7 @@ Section properties.
iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
{ cbv[Φ].
iIntros (ρ j K') "#Hs Hj /=". iExists v'.
tp_load j. tp_normalise j.
tp_load j.
iFrame. eauto. }
iIntros (v) "[% Hl]"; subst.
iApply "Hlog".
......@@ -781,10 +766,9 @@ Section properties.
iIntros (?) "Hl Hlog".
pose (Φ := (fun w => w = UnitV l ↦ₛ v')%I).
iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
rewrite_closed.
{ cbv[Φ].
iIntros (ρ j K') "#Hs Hj /=". iExists UnitV.
tp_store j. tp_normalise j.
tp_store j.
iFrame. eauto. }
iIntros (w) "[% Hl]"; subst.
iApply "Hlog".
......@@ -803,10 +787,9 @@ Section properties.
iIntros (????) "Hl Hlog".
pose (Φ := (fun w => w = BoolV false l ↦ₛ v)%I).
iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
rewrite_closed.
{ cbv[Φ].
iIntros (ρ j K') "#Hs Hj /=".
tp_cas_fail j; auto. tp_normalise j.
tp_cas_fail j; auto.
iExists (BoolV false). simpl.
iFrame. eauto. }
iIntros (w) "[% Hl]"; subst.
......@@ -826,10 +809,9 @@ Section properties.
iIntros (????) "Hl Hlog".
pose (Φ := (fun w => w = BoolV true l ↦ₛ v2)%I).
iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
(* rewrite_closed. *)
{ cbv[Φ].
iIntros (ρ j K') "#Hs Hj /=".
tp_cas_suc j; auto. tp_normalise j.
tp_cas_suc j; auto.
iExists (BoolV true). simpl.
iFrame. eauto. }
iIntros (w) "[% Hl]"; subst.
......
......@@ -5,6 +5,7 @@ From iris_logrel.F_mu_ref_conc Require Export binder lang.
(** Definitions and properties about substitution and closedness *)
(** * Definitions *)
(** Parallel substitution *)
Fixpoint subst_p (es : stringmap val) (e : expr) : expr :=
match e with
......@@ -42,6 +43,7 @@ Fixpoint subst_p (es : stringmap val) (e : expr) : expr :=
| CAS e0 e1 e2 => CAS (subst_p es e0) (subst_p es e1) (subst_p es e2)
end.
(** Substitution in the contexts *)
Fixpoint subst_ctx_item (es : stringmap val) (K : ectx_item)
{struct K} :=
match K with
......@@ -76,7 +78,8 @@ Definition subst_ctx (es : stringmap val) (K : list ectx_item) :=
map (subst_ctx_item es) K.
(** * Basic substitution properties *)
(** * Properties *)
(** ** Parallel substitution properties *)
Lemma subst_p_empty e :
subst_p e = e.
Proof.
......@@ -108,10 +111,7 @@ Proof.
by rewrite subst_p_empty.
Qed.
Definition subst_f (es : stringmap val) (e : expr) : expr :=
map_fold (fun k v f e => subst k (of_val v) (f e)) id es e.
(** * Properties of [Closed] and [is_closed] *)
(** ** Properties of [Closed] and [is_closed] *)
Lemma is_closed_weaken (e : expr) : (X Y : gset string),
is_closed X e X Y is_closed Y e.
Proof.
......@@ -126,16 +126,6 @@ Proof.
apply is_closed_weaken.
Qed.
(* Lemma allClosed_mono_1 X Y es : X Y allClosed X es allClosed Y es. *)
(* Proof. *)
(* intros HXY Hc i e' ?. eapply Closed_mono; eauto. by eapply Hc. *)
(* Qed. *)
(* Lemma allClosed_mono_2 es es' X : es' es allClosed X es allClosed X es'. *)
(* Proof. *)
(* intros HXY Hc i e' ?. eapply Hc. *)
(* by eapply lookup_weaken. *)
(* Qed. *)
Lemma of_val_closed' (v : val) X :
Closed X (of_val v).
Proof.
......@@ -143,6 +133,7 @@ Proof.
apply (Closed_mono _ (x :b: f :b: )); auto. set_solver.
apply (Closed_mono _ ); auto. set_solver.
Qed.
Lemma of_val_closed (v : val) :
Closed (of_val v).
Proof.
......@@ -159,10 +150,11 @@ Qed.
Hint Resolve to_val_closed.
Hint Resolve of_val_closed.
(* I find this mildly useful *)
(* I find this mildly useful for this file *)
Local Hint Extern 0 (Closed _ _) => eauto : typeclass_instances.
(** ** Relations between [Closed] and substitutions *)
(** *** Relations between [Closed] and substitutions *)
(** Closure properties of [Closed] *)
Lemma subst_closed x (es : expr) e `{Closed X e} `{Closed X es} :
Closed X (subst x es e).
Proof.
......@@ -192,43 +184,6 @@ Proof.
end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_subst_id X e x es :
is_closed X e x X subst x es e = e.
Proof.
revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma Closed_subst_id e x es :
Closed e
subst x es e = e.
Proof. intros Hc. eapply is_closed_subst_id. apply Hc. set_solver. Qed.
Lemma Closed_subst_p_id' X es e :
Closed X e
( x, x X es !! x = None)
subst_p es e = e.
Proof.
revert X es; unfold Closed. induction e => X es; simplify_option_eq;
rewrite ?bool_decide_spec; move => Hc HX; intuition eauto 20 with set_solver;
repeat lazymatch goal with
| [IH : context[subst_p _ ?e = ?e] |- _ ] =>
erewrite IH; eauto; clear IH
end. all: try set_solver.
- specialize (HX x). by rewrite HX.
- intro y. destruct f as [|f], x as [|x]; simpl; cbn-[union]; eauto;
rewrite ?elem_of_union ?elem_of_singleton;
intros [H | H]; rewrite ?lookup_delete_None; eauto.
destruct H; eauto.
Qed.
Lemma Closed_subst_p_id es e :
Closed e
subst_p es e = e.
Proof.
intros. eapply Closed_subst_p_id'; eauto.
intro x; rewrite elem_of_empty; intuition.
Qed.
Lemma subst_p_delete_Closed : forall e X (x:string) vs,
Closed X (subst_p vs e)
Closed ({[x]} X) (subst_p (delete x vs) e).
......@@ -321,6 +276,58 @@ Proof.
}
Qed.
(** When substitutions are identities *)
Lemma is_closed_subst_id X e x es :
is_closed X e x X subst x es e = e.
Proof.
revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma Closed_subst_id e x es :
Closed e
subst x es e = e.
Proof. intros Hc. eapply is_closed_subst_id. apply Hc. set_solver. Qed.
Lemma Closed_subst_p_id' X es e :
Closed X e
( x, x X es !! x = None)
subst_p es e = e.
Proof.
revert X es; unfold Closed. induction e => X es; simplify_option_eq;
rewrite ?bool_decide_spec; move => Hc HX; intuition eauto 20 with set_solver;
repeat lazymatch goal with
| [IH : context[subst_p _ ?e = ?e] |- _ ] =>
erewrite IH; eauto; clear IH
end. all: try set_solver.
- specialize (HX x). by rewrite HX.
- intro y. destruct f as [|f], x as [|x]; simpl; cbn-[union]; eauto;
rewrite ?elem_of_union ?elem_of_singleton;
intros [H | H]; rewrite ?lookup_delete_None; eauto.
destruct H; eauto.
Qed.
Lemma Closed_subst_p_id es e :
Closed e
subst_p es e = e.
Proof.
intros. eapply Closed_subst_p_id'; eauto.
intro x; rewrite elem_of_empty; intuition.
Qed.
Lemma of_val_subst (v : val) x (es : expr) :
subst x es (of_val v) = of_val v.
Proof.
by apply Closed_subst_id.
Qed.
Lemma of_val_subst_p (v : val) (es : stringmap val) :
subst_p es (of_val v) = of_val v.
Proof.
by apply Closed_subst_p_id.
Qed.
(** Relation between [subst_p] and [subst] *)
Lemma subst_p_insert (x : binder) v (m : stringmap val) e :
subst_p (<[x:=v]>m) e =
(subst_p m (subst' x (of_val v) e)).
......@@ -388,19 +395,7 @@ Proof.
by rewrite subst_p_empty.
Qed.
(* Other derived properties *)
Lemma of_val_subst (v : val) x (es : expr) :
subst x es (of_val v) = of_val v.
Proof.
by apply Closed_subst_id.
Qed.
Lemma of_val_subst_p (v : val) (es : stringmap val) :
subst_p es (of_val v) = of_val v.
Proof.
by apply Closed_subst_p_id.
Qed.
(** Properties of the context substitution *)
Lemma fill_item_subst_p (es : stringmap val) (Ki : ectx_item) (e : expr) :
subst_p es (fill_item Ki e) = fill_item (subst_ctx_item es Ki) (subst_p es e).
Proof.
......
From iris_logrel.F_mu_ref_conc Require Export lang notation subst.
From iris_logrel.F_mu_ref_conc Require Export lang notation binder subst.
From iris_logrel.prelude Require Export base.
From Autosubst Require Import Autosubst_Classes. (* for [subst] *)
(** Types *)
Inductive type :=
| TUnit : type
| TNat : type
......@@ -33,14 +34,9 @@ Inductive EqType : type → Prop :=
| EqTProd τ τ' : EqType τ EqType τ' EqType (TProd τ τ')
| EqSum τ τ' : EqType τ EqType τ' EqType (TSum τ τ').
(** Typing judgements *)
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Instance: Insert binder type (stringmap type) := fun k τ Γ =>
match k with
| BAnon => Γ
| BNamed x => <[x:=τ]>Γ
end.
Inductive typed (Γ : stringmap type) : expr type Prop :=
| Var_typed x τ : Γ !! x = Some τ Γ ⊢ₜ Var x : τ
| Unit_typed : Γ ⊢ₜ Unit : TUnit
......@@ -83,6 +79,7 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
Γ ⊢ₜ CAS e1 e2 e3 : TBool
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
(** Environment substitution and closedness *)
Definition env_subst := subst_p.
Lemma env_subst_empty (e : expr) : env_subst e = e.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment