Commit 45db2579 authored by Dan Frumin's avatar Dan Frumin
Browse files

Cleaning up rel_tactics

parent 6b0f9777
......@@ -8,16 +8,16 @@ Set Default Proof Using "Type".
Import lang.
(** General tactics *)
Lemma tac_rel_bind_l `{logrelG Σ} e' K Δ E1 E2 Γ e t Δ' τ :
Lemma tac_rel_bind_l `{logrelG Σ} e' K E1 E2 Δ Γ e t τ :
e = fill K e'
(Δ bin_log_related E1 E2 Δ' Γ (fill K e') t τ)
(Δ bin_log_related E1 E2 Δ' Γ e t τ).
( bin_log_related E1 E2 Δ Γ (fill K e') t τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof. intros. subst. eauto. Qed.
Lemma tac_rel_bind_r `{logrelG Σ} t' K Δ E1 E2 Γ e t Δ' τ :
Lemma tac_rel_bind_r `{logrelG Σ} t' K E1 E2 Δ Γ e t τ :
t = fill K t'
(Δ bin_log_related E1 E2 Δ' Γ e (fill K t') τ)
(Δ bin_log_related E1 E2 Δ' Γ e t τ).
( bin_log_related E1 E2 Δ Γ e (fill K t') τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof. intros. subst. eauto. Qed.
Ltac tac_bind_helper :=
......@@ -94,16 +94,17 @@ Tactic Notation "rel_apply_r" open_constr(lem) :=
(** Pure reductions *)
Lemma tac_rel_pure_l `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ (b : bool) :
Lemma tac_rel_pure_l `{logrelG Σ} K e1 E1 E2 Δ Γ e e2 eres ϕ t τ (b : bool) :
e = fill K e1
PureExec ϕ e1 e2
ϕ
Closed e1
((b = true E1 = E2) b = false)
(Δ' ?b bin_log_related E1 E2 Δ Γ (fill K e2) t τ)
(Δ' bin_log_related E1 E2 Δ Γ e t τ).
eres = fill K e2
( ?b bin_log_related E1 E2 Δ Γ eres t τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros Hfill Hpure Hϕ ? Hb Hp. subst.
intros Hfill Hpure Hϕ ? Hb ? Hp. subst.
assert (Closed e2).
{ eapply PureExec_Closed; eauto. }
destruct b.
......@@ -128,6 +129,7 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
|try (exact I || reflexivity || tac_rel_done)
|try (simpl; solve_closed) (* Closed e1 *)
|first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
|simpl; reflexivity (* eres = fill K e2 *)
|try iNext; simpl_subst/= (* new goal *)])
|| fail "rel_pure_l: cannot find the reduct".
......@@ -147,24 +149,25 @@ Tactic Notation "rel_case_inr_l" := rel_pure_l (Case (InjL _) _ _).
Tactic Notation "rel_case_l" := rel_pure_l (Case _ _ _).
Tactic Notation "rel_op_l" := rel_pure_l (BinOp _ _ _).
Lemma tac_rel_pure_r `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ :
Lemma tac_rel_pure_r `{logrelG Σ} K e1 E1 E2 Δ Γ e e2 eres ϕ t τ :
e = fill K e1
PureExec ϕ e1 e2
ϕ
Closed e1
nclose specN E1
(Δ' bin_log_related E1 E2 Δ Γ t (fill K e2) τ)
(Δ' bin_log_related E1 E2 Δ Γ t e τ).
eres = fill K e2
( bin_log_related E1 E2 Δ Γ t (fill K e2) τ)
( bin_log_related E1 E2 Δ Γ t e τ).
Proof.
intros Hfill Hpure Hϕ ?? Hp. subst.
intros Hfill Hpure Hϕ ??? Hp. subst.
assert (Closed e2).
{ eapply PureExec_Closed; eauto. }
rewrite -(bin_log_pure_r Δ Γ E1 E2 K e1 e2 t τ).
{ exact Hp. }
{ assumption. }
{ assumption. }
{ intros σ.
destruct Hpure as [Hsafe Hstep].
destruct (Hsafe Hϕ σ) as [e2' [σ2' [? Hstep']]].
destruct (Hsafe Hϕ σ) as [e2' [σ2' [? Hstep']]].
destruct (Hstep Hϕ _ _ _ _ Hstep') as (? & ? & ?); subst.
done. }
Qed.
......@@ -174,11 +177,12 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
rel_reshape_cont_r ltac:(fun K e' =>
unify e' ef;
simple eapply (tac_rel_pure_r K e');
[tac_bind_helper (* e = fill K e1' *)
[tac_bind_helper (* e = fill K e1 *)
|apply _ (* PureExec ϕ e1 e2 *)
|try (exact I || reflexivity || tac_rel_done)
|try (simpl; solve_closed) (* Closed e1 *)
|try (exact I || reflexivity || tac_rel_done) (* φ *)
|try (simpl; solve_closed) (* Closed e1 *)
|solve_ndisj (* specN E1 *)
|simpl; reflexivity (* eres = fill K e2 *)
|try iNext; simpl_subst/= (* new goal *)])
|| fail "rel_pure_r: cannot find the reduct".
......@@ -200,38 +204,64 @@ Tactic Notation "rel_op_r" := rel_pure_r (BinOp _ _ _).
(** Stateful reductions *)
Lemma tac_rel_fork_l `{logrelG Σ} Δ1 E1 E2 e' K' Γ e t Δ' τ :
e = fill K' (Fork e')
(* Fork *)
Lemma tac_rel_fork_l `{logrelG Σ} Δ E1 E2 e' K eres Γ e t τ :
e = fill K (Fork e')
Closed e'
(Δ1 |={E1,E2}=> WP e' {{ _ , True }} bin_log_related E2 E1 Δ' Γ (fill K' (Lit Unit)) t τ)
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
eres = fill K (Lit Unit)
( |={E1,E2}=> WP e' {{ _ , True }} bin_log_related E2 E1 Δ Γ eres t τ)
( bin_log_related E1 E1 Δ Γ e t τ).
Proof.
intros ???.
subst e.
rewrite -(bin_log_related_fork_l Δ' Γ E1 E2); eassumption.
intros ????.
subst e eres.
rewrite -(bin_log_related_fork_l Δ Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_fork_l" :=
iStartProof;
eapply (tac_rel_fork_l);
[tac_bind_helper || fail "rel_fork_l: cannot find 'fork'"
|solve_closed
|solve_closed (* Closed e' *)
|simpl; reflexivity (* eres = fill K () *)
|simpl (* new goal *) ].
Lemma tac_rel_fork_r `{logrelG Σ} Δ E1 E2 e' K Γ e t eres τ :
nclose specN E1
e = fill K (Fork e')
Closed e'
eres = fill K (Lit Unit)
( i, i e' - bin_log_related E1 E2 Δ Γ t eres τ)
( bin_log_related E1 E2 Δ Γ t e τ).
Proof.
intros ?????.
subst e eres.
rewrite -(bin_log_related_fork_r Δ Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_fork_r" "as" ident(i) constr(H) :=
iStartProof;
eapply (tac_rel_fork_r);
[solve_ndisj || fail "rel_fork_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_fork_r: cannot find 'fork'"
|solve_closed (* Closed e' *)
|simpl; reflexivity (* eres = fill K () *)
|simpl; iIntros (i) H (* new goal *)].
(* Alloc *)
Tactic Notation "rel_alloc_l_atomic" := rel_apply_l bin_log_related_alloc_l.
Lemma tac_rel_alloc_l_simp `{logrelG Σ} Δ1 Δ2 E1 e' v' K' Γ e t Δ' τ :
e = fill K' (Alloc e')
IntoLaterNEnvs 1 Δ1 Δ2
Lemma tac_rel_alloc_l_simp `{logrelG Σ} 1 2 E1 Δ Γ e t e' v' K τ :
e = fill K (Alloc e')
IntoLaterNEnvs 1 1 2
to_val e' = Some v'
(Δ2 l,
(l ↦ᵢ v' - bin_log_related E1 E1 Δ' Γ (fill K' (Loc l)) t τ))
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
(2 l,
(l ↦ᵢ v' - bin_log_related E1 E1 Δ Γ (fill K (Loc l)) t τ))
(1 bin_log_related E1 E1 Δ Γ e t τ).
Proof.
intros ???.
subst e.
rewrite into_laterN_env_sound /=.
rewrite -(bin_log_related_alloc_l' Δ' Γ E1); eauto.
rewrite -(bin_log_related_alloc_l' Δ Γ E1); eauto.
apply uPred.later_mono.
Qed.
......@@ -243,49 +273,109 @@ Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
|solve_to_val (* to_val e' = Some v *)
|iIntros (l) H (* new goal *)].
Lemma tac_rel_alloc_r `{logrelG Σ} E1 E2 Δ Γ t' v' K' e t τ :
nclose specN E1
t = fill K' (Alloc t')
to_val t' = Some v'
( l, l ↦ₛ v' - bin_log_related E1 E2 Δ Γ e (fill K' (Loc l)) τ)
( bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros ????.
subst t.
rewrite -(bin_log_related_alloc_r Δ Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
iStartProof;
eapply (tac_rel_alloc_r);
[solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
|solve_to_val (* to_val t' = Some v' *)
|simpl; iIntros (l) H (* new goal *)].
Tactic Notation "rel_alloc_r" :=
let l := fresh in
let H := iFresh "H" in
rel_alloc_r as l H.
(* Load *)
Tactic Notation "rel_load_l_atomic" := rel_apply_l bin_log_related_load_l.
Lemma tac_rel_load_l_simp `{logrelG Σ} Δ1 Δ2 E1 i1 l v K' Γ e t Δ' τ :
e = fill K' (Load (Loc l))
IntoLaterNEnvs 1 Δ1 Δ2
envs_lookup i1 Δ2 = Some (false, l ↦ᵢ v)%I
(Δ2 bin_log_related E1 E1 Δ' Γ (fill K' (of_val v)) t τ)
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
Lemma tac_rel_load_l_simp `{logrelG Σ} 1 2 i1 E1 Δ Γ l v K e t eres τ :
e = fill K (Load (Loc l))
IntoLaterNEnvs 1 1 2
envs_lookup i1 2 = Some (false, l ↦ᵢ v)%I
eres = fill K (of_val v)
(2 bin_log_related E1 E1 Δ Γ eres t τ)
(1 bin_log_related E1 E1 Δ Γ e t τ).
Proof.
intros ??? HΔ2.
subst e.
intros ???? HΔ2.
subst e eres.
rewrite into_laterN_env_sound envs_lookup_split //; simpl.
rewrite uPred.later_sep.
rewrite HΔ2.
apply uPred.wand_elim_l'.
by rewrite -(bin_log_related_load_l' Δ' Γ E1).
by rewrite -(bin_log_related_load_l' Δ Γ E1).
Qed.
Tactic Notation "rel_load_l" :=
iStartProof;
eapply (tac_rel_alloc_l_simp);
eapply (tac_rel_load_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|apply _ (* IntoLaterNenvs _ Δ1 Δ2 *)
|iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
|simpl; reflexivity (* eres = fill K (of_val v) *)
| (* new goal *)].
Lemma tac_rel_load_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l e t tres τ v :
nclose specN E1
t = fill K (Load (Loc l))
envs_lookup i1 1 = Some (false, l ↦ₛ v)%I
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v)%I) 1 = Some 2
tres = fill K (of_val v)
(2 bin_log_related E1 E2 Δ Γ e tres τ)
(1 bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros ????? Hg.
rewrite (envs_simple_replace_sound 1 2 i1) //; simpl.
rewrite right_id.
subst t tres.
rewrite {1}(bin_log_related_load_r Δ Γ E1 E2); [ | eassumption ].
rewrite Hg.
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_load_r" :=
iStartProof;
eapply (tac_rel_load_r);
[solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K (Store (Loc l) e') *)
|iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl; reflexivity (* tres = fill K (of_val v) *)
|simpl (* new goal *)].
(* Store *)
Tactic Notation "rel_store_l_atomic" := rel_apply_l bin_log_related_store_l.
Lemma tac_rel_store_l_simp `{logrelG Σ} Δ1 Δ2 i1 E1 l v e' v' K' Γ e t Δ' τ :
e = fill K' (Store (Loc l) e')
Lemma tac_rel_store_l_simp `{logrelG Σ} 1 2 3 i1 E1 Δ Γ K l v e' v' e t eres τ :
e = fill K (Store (Loc l) e')
to_val e' = Some v'
envs_lookup i1 Δ1 = Some (false, l ↦ᵢ v)%I
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E1 Δ' Γ (fill K' (Lit Unit)) t τ)
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
IntoLaterNEnvs 1 1 2
envs_lookup i1 2 = Some (false, l ↦ᵢ v)%I
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) 2 = Some 3
eres = fill K (Lit Unit)
(3 bin_log_related E1 E1 Δ Γ eres t τ)
(1 bin_log_related E1 E1 Δ Γ e t τ).
Proof.
intros ?????.
subst e.
rewrite envs_simple_replace_sound //; simpl.
intros ?????? Hg.
subst e eres.
rewrite into_laterN_env_sound envs_simple_replace_sound //; simpl.
rewrite uPred.later_sep.
rewrite right_id.
rewrite (uPred.later_intro (l ↦ᵢ v)%I).
rewrite (bin_log_related_store_l' Δ' Γ E1). 2: eassumption.
rewrite H4.
rewrite (bin_log_related_store_l' Δ Γ E1). 2: eassumption.
rewrite Hg.
apply uPred.wand_elim_l.
Qed.
......@@ -294,49 +384,28 @@ Tactic Notation "rel_store_l" :=
eapply (tac_rel_store_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|solve_to_val (* to_val e' = Some v' *)
|apply _ (* IntoLaterNEnvs *)
|iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
| (* new goal *)].
Tactic Notation "rel_cas_l_atomic" := rel_apply_l bin_log_related_cas_l.
(********************************)
Lemma tac_rel_fork_r `{logrelG Σ} Δ1 E1 E2 t' K' Γ e t Δ' τ :
nclose specN E1
t = fill K' (Fork t')
Closed t'
(Δ1 i, i t' - bin_log_related E1 E2 Δ' Γ e (fill K' (Lit Unit)) τ)
(Δ1 bin_log_related E1 E2 Δ' Γ e t τ).
Proof.
intros ????.
subst t.
rewrite -(bin_log_related_fork_r Δ' Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_fork_r" "as" ident(i) constr(H) :=
iStartProof;
eapply (tac_rel_fork_r);
[solve_ndisj || fail "rel_fork_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_fork_r: cannot find 'alloc'"
|solve_closed
|simpl; iIntros (i) H (* new goal *)].
|simpl; reflexivity (* eres = fill K () *)
|(* new goal *)].
Lemma tac_rel_store_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l t' v' K' Γ e t Δ' τ v :
Lemma tac_rel_store_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l t' v' e t tres τ v :
nclose specN E1
t = fill K' (Store (Loc l) t')
t = fill K (Store (Loc l) t')
to_val t' = Some v'
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Δ' Γ e (fill K' (Lit Unit)) τ)
(Δ1 bin_log_related E1 E2 Δ' Γ e t τ).
envs_lookup i1 1 = Some (false, l ↦ₛ v)%I
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) 1 = Some 2
tres = fill K (Lit Unit)
(2 bin_log_related E1 E2 Δ Γ e tres τ)
(1 bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros ??????.
intros ?????? Hg.
rewrite envs_simple_replace_sound //; simpl.
rewrite right_id.
subst t.
rewrite (bin_log_related_store_r Δ' Γ E1 E2); [ | eassumption | eassumption ].
rewrite H5.
subst t tres.
rewrite (bin_log_related_store_r Δ Γ E1 E2); [ | eassumption..].
rewrite Hg.
apply uPred.wand_elim_l.
Qed.
......@@ -346,80 +415,33 @@ Tactic Notation "rel_store_r" :=
[solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|solve_to_val (* to_val e' = Some v *)
|iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?"
|iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_store_r: this should not happen"
|simpl; reflexivity (* tres = fill K () *)
|(* new goal *)].
Lemma tac_rel_alloc_r `{logrelG Σ} Δ1 E1 E2 t' v' K' Γ e t Δ' τ :
nclose specN E1
t = fill K' (Alloc t')
to_val t' = Some v'
(Δ1 l, l ↦ₛ v' - bin_log_related E1 E2 Δ' Γ e (fill K' (Loc l)) τ)
(Δ1 bin_log_related E1 E2 Δ' Γ e t τ).
Proof.
intros ????.
subst t.
rewrite -(bin_log_related_alloc_r Δ' Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
iStartProof;
eapply (tac_rel_alloc_r);
[solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
|solve_to_val (* to_val t' = Some v' *)
|simpl; iIntros (l) H (* new goal *)].
Tactic Notation "rel_alloc_r" :=
let l := fresh in
let H := iFresh "H" in
rel_alloc_r as l H.
Lemma tac_rel_load_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t Δ' τ v :
nclose specN E1
t = fill K' (Load (Loc l))
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v)%I) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Δ' Γ e (fill K' (of_val v)) τ)
(Δ1 bin_log_related E1 E2 Δ' Γ e t τ).
Proof.
intros ?????.
rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl.
rewrite right_id.
subst t.
rewrite {1}(bin_log_related_load_r Δ' Γ E1 E2); [ | eassumption ].
rewrite H4.
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_load_r" :=
iStartProof;
eapply (tac_rel_load_r);
[solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl (* new goal *)].
(* CAS *)
Tactic Notation "rel_cas_l_atomic" := rel_apply_l bin_log_related_cas_l.
Lemma tac_rel_cas_fail_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 Δ' τ v :
Lemma tac_rel_cas_fail_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l e t e1 e2 v1 v2 tres τ v :
nclose specN E1
t = fill K' (CAS (Loc l) e1 e2)
t = fill K (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
envs_lookup i1 1 = Some (false, l ↦ₛ v)%I
v v1
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v)%I) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Δ' Γ e (fill K' (# false)) τ)
(Δ1 bin_log_related E1 E2 Δ' Γ e t τ).
(Esnoc Enil i1 (l ↦ₛ v)%I) 1 = Some 2
tres = fill K (# false)
(2 bin_log_related E1 E2 Δ Γ e tres τ)
(1 bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros ????????.
rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl.
intros ???????? Hg.
rewrite (envs_simple_replace_sound 1 2 i1) //; simpl.
rewrite right_id.
subst t.
rewrite {1}(bin_log_related_cas_fail_r Δ' Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
rewrite H7.
subst t tres.
rewrite {1}(bin_log_related_cas_fail_r Δ Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
rewrite Hg.
apply uPred.wand_elim_l.
Qed.
......@@ -433,27 +455,29 @@ Tactic Notation "rel_cas_fail_r" :=
|iAssumptionCore || fail "rel_cas_fail_l: cannot find ? ↦ₛ ?"
|try fast_done (* v v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl; reflexivity (* tres = fill K false *)
|(* new goal *)].
Lemma tac_rel_cas_suc_r `{logrelG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 Δ' τ v :
Lemma tac_rel_cas_suc_r `{logrelG Σ} 1 2 E1 E2 Δ Γ K i1 l e t e1 e2 v1 v2 tres τ v :
nclose specN E1
t = fill K' (CAS (Loc l) e1 e2)
t = fill K (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
envs_lookup i1 1 = Some (false, l ↦ₛ v)%I
v = v1
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v2)%I) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Δ' Γ e (fill K' (# true)) τ)
(Δ1 bin_log_related E1 E2 Δ' Γ e t τ).
(Esnoc Enil i1 (l ↦ₛ v2)%I) 1 = Some 2
tres = fill K (# true)
(2 bin_log_related E1 E2 Δ Γ e tres τ)
(1 bin_log_related E1 E2 Δ Γ e t τ).
Proof.
intros ????????.
rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl.
intros ???????? Hg.
rewrite (envs_simple_replace_sound 1 2 i1) //; simpl.
rewrite right_id.
subst t.
rewrite {1}(bin_log_related_cas_suc_r Δ' Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
rewrite H7.
subst t tres.
rewrite {1}(bin_log_related_cas_suc_r Δ Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
rewrite Hg.
apply uPred.wand_elim_l.
Qed.
......@@ -467,6 +491,7 @@ Tactic Notation "rel_cas_suc_r" :=
|iAssumptionCore || fail "rel_cas_suc_l: cannot find ? ↦ₛ ?"
|try fast_done (* v = v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl; reflexivity (* tres = fill K true *)
|(* new goal *)].
Section test.
......
......@@ -62,7 +62,7 @@ Section properties.
iIntros (Hv Hv') "IH".
iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
replace e with (of_val v); auto using of_to_val.
replace e' with (of_val v'); auto using of_to_val.
replace e' with (of_val v'); auto using of_to_val.
rewrite /env_subst !Closed_subst_p_id.
iMod "IH" as "IH".
iModIntro. iApply wp_value; 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