Commit 04f63a10 authored by Dan Frumin's avatar Dan Frumin
Browse files

General cleanup

parent eba7639e
......@@ -111,11 +111,11 @@ Ltac of_expr e :=
| to_expr ?e => e
| of_val ?v => constr:(Val v)
| _ =>
match goal with
| [H : Closed e |- _] => constr:(@ClosedExpr e H)
| [H : Is_true (is_closed e) |- _] => constr:(@ClosedExpr e H)
lazymatch goal with
| [H : to_val e = Some ?ev |- _] =>
constr:(@ClosedExpr e (to_val_closed e ev H))
| [H : Closed e |- _] => constr:(@ClosedExpr e H)
| [H : Is_true (is_closed e) |- _] => constr:(@ClosedExpr e H)
end
end.
......
......@@ -26,7 +26,6 @@ Section properties.
iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
Qed.
(* TODO: should there be a corresponding =ElimModal= instance? *)
Lemma fupd_logrel' Γ E1 E2 e e' τ :
((|={E1}=> ({E1,E2;Γ} e log e' : τ))
- {E1,E2;Γ} e log e' : τ)%I.
......@@ -40,11 +39,19 @@ Section properties.
Global Instance elim_modal_logrel E1 E2 Γ e e' P τ :
ElimModal (|={E1,E2}=> P) P
({E1,E2;Γ} e log e' : τ) ({E2,E2;Γ} e log e' : τ) | 0.
({E1,E2;Γ} e log e' : τ) ({E2,E2;Γ} e log e' : τ) | 10.
Proof.
iIntros "[HP HI]". iApply fupd_logrel.
iMod "HP". iApply ("HI" with "HP").
Qed.
Global Instance elim_modal_logrel' E1 E2 Γ e e' P τ :
ElimModal (|={E1}=> P) P
({E1,E2;Γ} e log e' : τ) ({E1,E2;Γ} e log e' : τ) | 0.
Proof.
iIntros "[HP HI]". iApply fupd_logrel'.
iMod "HP". iApply ("HI" with "HP").
Qed.
Lemma bin_log_related_val Γ E τ e e' v v' :
to_val e = Some v
......@@ -127,13 +134,13 @@ Section properties.
Qed.
Lemma bin_log_related_fst_l Γ E K v1 v2 e τ :
({E,E;Γ} (fill K (of_val v1)) log e : τ)
{E,E;Γ} (fill K (Fst (Pair (of_val v1) (of_val v2)))) log e : τ.
({E,E;Γ} fill K (of_val v1) log e : τ)
{E,E;Γ} fill K (Fst (Pair (of_val v1) (of_val v2))) log e : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- by inversion H1.
- by inversion H0.
Qed.
Lemma bin_log_related_snd_l Γ E K v1 v2 e τ :
......@@ -143,7 +150,7 @@ Section properties.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- by inversion H1.
- by inversion H0.
Qed.
Lemma bin_log_related_rec_l Γ E K (f x : binder) e e' v t τ
......@@ -197,9 +204,9 @@ Section properties.
Lemma bin_log_related_pack_l Γ E K e e' v t τ
(Hclosed' : Closed e') :
(to_val e = Some v)
to_val e = Some v
({E,E;Γ} fill K (App e' e) log t : τ)
{E,E;Γ} (fill K (Unpack (Pack e) e')) log t : τ.
{E,E;Γ} fill K (Unpack (Pack e) e') log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -212,9 +219,9 @@ Section properties.
Lemma bin_log_related_case_inl_l Γ E K e v e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
(to_val e = Some v)
to_val e = Some v
({E,E;Γ} fill K (App e1 e) log t : τ)
{E,E;Γ} (fill K (Case (InjL e) e1 e2)) log t : τ.
{E,E;Γ} fill K (Case (InjL e) e1 e2) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -227,9 +234,9 @@ Section properties.
Lemma bin_log_related_case_inr_l Γ E K e v e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
(to_val e = Some v)
to_val e = Some v
({E,E;Γ} fill K (App e2 e) log t : τ)
{E,E;Γ} (fill K (Case (InjR e) e1 e2)) log t : τ.
{E,E;Γ} fill K (Case (InjR e) e1 e2) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -243,7 +250,7 @@ Section properties.
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
({E,E;Γ} fill K e1 log t : τ)
{E,E;Γ} (fill K (If (# true) e1 e2)) log t : τ.
{E,E;Γ} fill K (If (# true) e1 e2) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros.
......@@ -257,7 +264,7 @@ Section properties.
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
({E1,E2;Γ} fill K e1 log t : τ)
{E1,E2;Γ} (fill K (If (# true) e1 e2)) log t : τ.
{E1,E2;Γ} fill K (If (# true) e1 e2) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_masked_l with "Hlog"); auto.
......@@ -324,17 +331,6 @@ Section properties.
rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
done.
Qed.
Lemma bin_log_related_step_l Φ Γ E K e1 e2 τ
(Hclosed1 : Closed e1) :
(|={E}=> WP e1 @ E {{ Φ }}) -
( v, Φ v - {E,E;Γ} fill K (of_val v) log e2 : τ) -
{E,E;Γ} fill K e1 log e2 : τ.
Proof.
iIntros "He Hlog".
iApply bin_log_related_wp_l.
iMod "He". by iApply (wp_wand with "He").
Qed.
Lemma bin_log_related_wp_atomic_l Γ (E1 E2 : coPset) K e1 e2 τ
(Hatomic : atomic e1)
......@@ -788,6 +784,7 @@ Section properties.
iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
{ cbv[Φ].
iIntros (ρ j K') "#Hs Hj /=". iExists UnitV.
Ltac solve_to_val ::= idtac.
tp_store j.
iFrame. eauto. }
iIntros (w) "[% Hl]"; subst.
......
......@@ -213,10 +213,6 @@ Proof.
rewrite assoc (comm _ {[f]} {[s]}) -assoc.
by eapply IHe.
+ rewrite !(delete_commute _ _ s).
(* TODO: weird behaviour: *)
(* rewrite !assoc. *)
(* rewrite (comm union {[f]} {[s]}). *)
(* END TODO *)
rewrite (assoc _ {[f]} {[s]}).
rewrite (comm _ {[f]} {[s]}).
rewrite !assoc.
......@@ -252,8 +248,9 @@ Proof.
+ simpl in Hcl.
eapply IHe; eauto.
rewrite dom_delete.
(* TODO: set_solver does not solve this *)
set_unfold.
(* Set solver cannot solve this because we have an additional assumption of decidable equality on [X] *)
revert Hdom. clear.
set_unfold. intros Hdom.
intros y [Hy|Hy]; subst; eauto.
destruct (Hdom _ Hy); eauto.
destruct (decide (y = x)); subst; eauto.
......
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