Commit 324ba2b6 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies, add missing frame instances

parent 744a9606
Pipeline #65081 passed with stage
in 20 minutes and 11 seconds
......@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
depends: [
"coq-iris-heap-lang" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2022-01-17.2.ec624937") | (= "dev") }
"coq-autosubst" { = "dev" }
]
......
......@@ -261,9 +261,9 @@ Section rules.
end.
Lemma seq_or_2' (f g h f' g' h' : expr) A :
is_closed_expr [] f
is_closed_expr [] g
is_closed_expr [] h
is_closed_expr f
is_closed_expr g
is_closed_expr h
(REL f << f' : A) -
(REL g << g' : A) -
(REL h << h' : A) -
......@@ -275,7 +275,7 @@ Section rules.
Proof.
iIntros (???) "Hf Hg Hh". rel_pures_r.
rel_newproph_l vs p as "Hp". repeat rel_pure_l.
(rewrite !(subst_is_closed []) //; try by set_solver); [].
(rewrite !(subst_is_closed ) //; try by set_solver); [].
rel_apply_r or_refines_r.
destruct (to_choice vs) as [|] eqn:Hchoice.
- iLeft. iApply (refines_seq with "Hf").
......@@ -298,9 +298,9 @@ Section rules.
(** We then prove that the non-instrumented program refines the original one *)
Lemma seq_or_2_instrument (f g h f' g' h' : expr) A :
is_closed_expr [] f'
is_closed_expr [] g'
is_closed_expr [] h'
is_closed_expr f'
is_closed_expr g'
is_closed_expr h'
(REL f << f' : A) -
(REL g << g' : A) -
(REL h << h' : A) -
......@@ -312,7 +312,7 @@ Section rules.
Proof.
iIntros (???) "Hf Hg Hh".
rel_newproph_r p. repeat rel_pure_r.
(rewrite !(subst_is_closed []) //; try by set_solver); [].
(rewrite !(subst_is_closed ) //; try by set_solver); [].
iApply (refines_seq with "Hf").
rel_pures_l. rel_pures_r.
iApply (or_compatible with "[Hg] [Hh]").
......
......@@ -202,8 +202,8 @@ Section rules.
(* This proof is now simpler but it still requires unfolding the REL judgement *)
Lemma par_comm e1 e2 :
is_closed_expr [] e1
is_closed_expr [] e2
is_closed_expr e1
is_closed_expr e2
(REL e1 << e1 : ()) -
(REL e2 << e2 : ()) -
REL (e2 e1) << (e1 e2) : ().
......@@ -246,8 +246,8 @@ Section rules.
Qed.
Lemma seq_par e1 e2 (A B : lrel Σ) :
is_closed_expr [] e1
is_closed_expr [] e2
is_closed_expr e1
is_closed_expr e2
(REL e1 << e1 : A) -
(REL e2 << e2 : B) -
REL e1 ;; e2 << (e1 ||| e2)%V : lrel_true.
......@@ -289,10 +289,10 @@ Section rules.
Qed.
Lemma interchange a b c d (A B C D : lrel Σ) :
is_closed_expr [] a
is_closed_expr [] b
is_closed_expr [] c
is_closed_expr [] d
is_closed_expr a
is_closed_expr b
is_closed_expr c
is_closed_expr d
(REL a << a : A) -
(REL b << b : B) -
(REL c << c : C) -
......
......@@ -21,10 +21,10 @@ Tactic Notation "use_logrel/=" :=
Lemma typed_is_closed_empty e τ :
e : τ is_closed_expr [] e.
e : τ is_closed_expr e.
Proof.
intros H%typed_is_closed. revert H.
by rewrite dom_empty_L elements_empty.
by rewrite dom_empty_L.
Qed.
Ltac fundamental := by iApply (refines_typed TUnit []).
......
......@@ -664,7 +664,7 @@ Tactic Notation "rel_resolveproph_r" :=
(** Fork *)
Lemma tac_rel_fork_l `{!relocG Σ} K E e' eres e t A :
e = fill K (Fork e')
is_closed_expr [] e'
is_closed_expr e'
eres = fill K #()
envs_entails (|={,E}=> (WP e' {{ _ , True%I }} refines E eres t A))%I
envs_entails (refines e t A).
......@@ -687,7 +687,7 @@ Tactic Notation "rel_fork_l" :=
Lemma tac_rel_fork_r `{!relocG Σ} K E e' e t eres A :
e = fill K (Fork e')
nclose specN E
is_closed_expr [] e'
is_closed_expr e'
eres = fill K #()
envs_entails ( k, refines_right k e' - refines E t eres A)
envs_entails (refines E t e A).
......
......@@ -160,6 +160,10 @@ Section mapsto.
Global Instance mapstoS_as_fractional l q v :
AsFractional (l ↦ₛ{q} v) (λ q, l ↦ₛ{q} v)%I q.
Proof. split. done. apply _. Qed.
Global Instance frame_mapstoS p l v q1 q2 RES :
FrameFractionalHyps p (l ↦ₛ{q1} v) (λ q, l ↦ₛ{q} v)%I RES q1 q2
Frame p (l ↦ₛ{q1} v) (l ↦ₛ{q2} v) RES | 5.
Proof. apply: frame_fractional. Qed.
Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 - l ↦ₛ{q2} v2 - v1 = v2.
Proof.
......
......@@ -266,6 +266,7 @@ Definition maybe_insert_binder (x : binder) (X : stringset) : stringset :=
| BNamed f => {[f]} X
end.
(* FIXME: this can be removed now, since [is_closed_expr] already uses [stringset]. *)
Local Fixpoint is_closed_expr_set (X : stringset) (e : expr) : bool :=
match e with
| Val v => is_closed_val_set v
......@@ -287,54 +288,13 @@ with is_closed_val_set (v : val) : bool :=
| InjLV v | InjRV v => is_closed_val_set v
end.
Lemma is_closed_expr_permute (e : expr) (xs ys : list string) :
xs ys
is_closed_expr xs e = is_closed_expr ys e.
Proof.
revert xs ys. induction e=>xs ys Hxsys /=;
repeat match goal with
| [ |- _ && _ = _ && _ ] => f_equal
| [ H : xs ys, xs ys is_closed_expr xs _ = is_closed_expr ys _
|- is_closed_expr _ _ = is_closed_expr _ _ ] => eapply H; eauto
end; try done.
- apply bool_decide_ext. by rewrite Hxsys.
- by rewrite Hxsys.
Qed.
Global Instance is_closed_expr_proper : Proper (Permutation ==> eq ==> eq) is_closed_expr.
Proof.
intros X1 X2 HX x y ->. by eapply is_closed_expr_permute.
Qed.
Lemma is_closed_expr_set_sound (X : stringset) (e : expr) :
is_closed_expr_set X e is_closed_expr (elements X) e
is_closed_expr_set X e is_closed_expr X e
with is_closed_val_set_sound (v : val) :
is_closed_val_set v is_closed_val v.
Proof.
- induction e; simplify_eq/=; try by (intros; destruct_and?; split_and?; eauto).
+ intros. case_bool_decide; last done.
by apply bool_decide_pack, elem_of_elements.
+ destruct f as [|f], x as [|x]; simplify_eq/=.
* eapply IHe.
* intros H%is_closed_expr_set_sound.
eapply is_closed_weaken; eauto. by set_solver.
* intros H%is_closed_expr_set_sound.
eapply is_closed_weaken; eauto. by set_solver.
* intros H%is_closed_expr_set_sound.
eapply is_closed_weaken; eauto. by set_solver.
- induction v; simplify_eq/=; try naive_solver.
destruct f as [|f], x as [|x]; simplify_eq/=;
intros H%is_closed_expr_set_sound; revert H.
+ set_solver.
+ by rewrite ?right_id_L elements_singleton.
+ by rewrite ?right_id_L elements_singleton.
+ rewrite ?right_id_L.
intros. eapply is_closed_weaken; eauto.
destruct (decide (f = x)) as [->|?].
* rewrite union_idemp_L elements_singleton.
set_solver.
* rewrite elements_disj_union; last set_solver.
rewrite !elements_singleton. set_solver.
- induction v; simplify_eq/=; try by (intros; destruct_and?; split_and?; eauto).
Qed.
Local Lemma typed_is_closed_set Γ e τ :
......@@ -386,6 +346,6 @@ Proof.
Qed.
Theorem typed_is_closed Γ e τ :
Γ e : τ is_closed_expr (elements (dom stringset Γ)) e.
Γ e : τ is_closed_expr (dom stringset Γ) e.
Proof. intros. eapply is_closed_expr_set_sound, typed_is_closed_set; eauto. Qed.
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