Skip to content

GitLab

Commit 08817aea authored by Dan Frumin's avatar Dan Frumin
Browse files

Use `bin_log_FG_increment_logatomic` in the refinement proof 

Using the lambdasubst hack-- instead of formulating
lemmas for (App e1 v), formulate them for (e1[x:=v]).
parent b18b2448
Hide whitespace changes
Inline Side-by-side
F_mu_ref_conc/examples/counter.v
View file @ 08817aea
......@@ -5,11 +5,16 @@ From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import tactics soundness_binary relational_properties.
From iris.program_logic Require Import adequacy.
From iris_logrel.F_mu_ref_conc Require Import hax.
Definition CG_increment : val := λ: "x" <>,
"x" <- BinOp Add (#n 1) (! "x").
Definition CG_locked_increment : val := λ: "x" "l",
with_lock (λ: "l", CG_increment "x" "l") "l".
Definition CG_locked_increment : val := λ: "x" "l" <>,
acquire "l";;
CG_increment "x" #();;
release "l".
(* with_lock (λ: "l", CG_increment "x" "l") "l". *)
Definition counter_read : val := λ: "x" "y", !"x".
......@@ -58,8 +63,8 @@ Section CG_Counter.
tp_op j. tp_normalise j.
tp_store j.
by iFrame.
Qed.
Qed.
Lemma bin_log_related_CG_increment_r Γ K E1 E2 x n t τ :
nclose specN ⊆ E1 →
x ↦ₛ (#nv n) -∗
......@@ -100,14 +105,23 @@ Section CG_Counter.
unfold CG_locked_increment. unlock. (* TODO: unlock needed :( *)
tp_rec j; simpl. rewrite !Closed_subst_id.
tp_rec j; simpl. rewrite !Closed_subst_id.
tp_apply j (steps_with_lock _ _ _ K _ _ l _ _ UnitV UnitV) with "Hx Hl";
last by iFrame.
{ simpl. by rewrite decide_left. }
{ iIntros (K') "#Hspec Hx Hj /=".
iApply fupd_trans.
iApply (steps_CG_increment E with "Hspec Hx"); auto.
tp_rec j; simpl. by rewrite !Closed_subst_id.
}
tp_rec j; tp_normalise j.
tp_bind j (acquire #l).
tp_apply j (steps_acquire _ _ _ _ l) with "Hl" as "Hl". tp_normalise j.
tp_rec j; tp_normalise j.
tp_bind j ((CG_increment #x) #())%E.
tp_apply j steps_CG_increment with "Hx" as "$". tp_normalise j.
tp_rec j; tp_normalise j.
tp_apply j lock.steps_release with "Hl" as "$". (*TODO: remove steps_release from tactics.v *)
done.
(* tp_apply j (steps_with_lock _ _ _ K _ _ l _ _ UnitV UnitV) with "Hx Hl"; *)
(* last by iFrame. *)
(* { simpl. by rewrite decide_left. } *)
(* { iIntros (K') "#Hspec Hx Hj /=". *)
(* iApply fupd_trans. *)
(* iApply (steps_CG_increment E with "Hspec Hx"); auto. *)
(* tp_rec j; simpl. by rewrite !Closed_subst_id. *)
(* } *)
Qed.
Lemma bin_log_related_CG_locked_increment_r Γ K E1 E2 t τ x n l :
......@@ -115,19 +129,29 @@ Section CG_Counter.
(x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) -∗
(x ↦ₛ (#nv S n) -∗ l ↦ₛ (#♭v false) -∗
({E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)) -∗
{E1,E2;Γ} ⊨ t ≤log≤ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) : τ)%I.
{E1,E2;Γ} ⊨ t ≤log≤ fill K ((lamsubst (lamsubst CG_locked_increment (LocV x)) (LocV l)) Unit) : τ)%I.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_locked_increment. unlock.
rel_bind_r (App _ (#x))%E.
iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.
rel_bind_r (App _ (#l))%E.
iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_with_lock_r Γ K E1 E2 (x ↦ₛ (#nv S n)) _ Unit Unit with "[Hx] Hl"); eauto.
- simpl. by rewrite decide_left.
- iIntros (K') "Hlog".
iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_CG_increment_r with "Hx"); auto.
unfold CG_locked_increment. unlock. simpl.
rewrite !Closed_subst_id.
(* rel_bind_r (App _ (#x))%E. *)
(* iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id. *)
(* rel_bind_r (App _ (#l))%E. *)
(* iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id. *)
iApply bin_log_related_rec_r; eauto. simpl.
rel_bind_r (acquire #l).
iApply (bin_log_related_acquire_r with "Hl"); eauto. iIntros "Hl". simpl.
iApply bin_log_related_rec_r; eauto. simpl.
rel_bind_r (CG_increment #x #())%E.
iApply (bin_log_related_CG_increment_r with "Hx"); auto. simpl. iIntros "Hx".
iApply bin_log_related_rec_r; eauto. simpl.
iApply (bin_log_related_release_r with "Hl"); eauto.
by iApply "Hlog".
(* iApply (bin_log_related_with_lock_r Γ K E1 E2 (x ↦ₛ (#nv S n)) _ Unit Unit with "[Hx] Hl"); eauto. *)
(* - simpl. by rewrite decide_left. *)
(* - iIntros (K') "Hlog". *)
(* iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id. *)
(* iApply (bin_log_related_CG_increment_r with "Hx"); auto. *)
Qed.
Global Opaque CG_locked_increment.
......@@ -215,47 +239,8 @@ Section CG_Counter.
iApply wp_if_true. iNext.
iApply wp_value; auto.
by iApply "Hlog".
(* TODO !!!!
Is this actually better than using bin_log_related lemmas?
*)
Qed.
(* TODO: this is not really needed.
This is just an experiment to seeif it is easier to use bin_log_related lemmas *)
(* Lemma bin_log_FG_increment_l' Γ K E x n t τ : *)
(* x ↦ᵢ (#nv n) -∗ *)
(* (x ↦ᵢ (#nv (S n)) -∗ {E,E;Γ} ⊨ fill K Unit ≤log≤ t : τ) -∗ *)
(* {E,E;Γ} ⊨ fill K (App (FG_increment (Loc x)) Unit) ≤log≤ t : τ. *)
(* Proof. *)
(* iIntros "Hx Hlog". *)
(* iApply (bin_log_related_rec_l Γ E with "[-]"); auto. *)
(* iNext. *)
(* change (Rec *)
(* (App *)
(* (Rec *)
(* (If *)
(* (CAS (Loc x).[ren (+4)] *)
(* (Var 1) (BinOp Add (#n 1) (Var 1))) Unit *)
(* (App (Var 2) (Var 3)))) *)
(* (Load (Loc x).[ren (+2)]))) with (FG_increment (Loc x)). simpl. *)
(* rel_bind_l (Load (Loc x)). rewrite -fill_app. *)
(* iApply (bin_log_related_load_l E E Γ with "[-]"); auto. *)
(* iModIntro. iExists (#nv n). iSplit; eauto. iFrame "Hx". *)
(* iIntros "Hx". rewrite fill_app /=. *)
(* iApply (bin_log_related_rec_l); auto. *)
(* iNext. simpl. *)
(* rel_bind_l (BinOp Add _ _). rewrite -fill_app. *)
(* iApply (bin_log_related_binop_l). rewrite fill_app /=. *)
(* iNext. rel_bind_l (CAS _ _ _). rewrite -fill_app. *)
(* iApply (bin_log_related_cas_l); auto. *)
(* iModIntro. iExists (#nv n). iFrame. *)
(* iSplitR. *)
(* - iDestruct 1 as %Hfoo. by exfalso. *)
(* - iIntros "% Hx". rewrite fill_app /=. *)
(* iApply bin_log_related_if_true_l; auto. *)
(* iNext. by iApply "Hlog". *)
(* Qed. *)
Global Opaque FG_increment.
Lemma FG_counter_body_type Γ :
......@@ -280,28 +265,6 @@ Section CG_Counter.
Definition counterN : namespace := nroot .@ "counter".
Lemma bin_log_related_arrow Γ (f x f' x' : binder) (e e' : expr) (τ τ' : type)
(Hclosed : Closed ∅ (rec: f x := e)%E )
(Hclosed' : Closed ∅ (rec: f' x' := e')%E) :
□(∀ Δ vv, ⟦ τ ⟧ Δ vv -∗
∅ ⊨ App (Rec f x e) (of_val (vv.1)) ≤log≤ App (Rec f' x' e') (of_val (vv.2)) : τ') -∗
Γ ⊨ (Rec f x e) ≤log≤ (Rec f' x' e') : TArrow τ τ'.
Proof.
iIntros "#H".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
cbn-[subst_p]. rewrite /env_subst !Closed_subst_p_id.
iModIntro. iApply wp_value; auto.
{ simpl. erewrite decide_left. done. }
iExists (RecV f' x' e'). simpl.
iFrame "Hj". iAlways. iIntros (vv) "Hvv".
iSpecialize ("H" $! Δ vv with "Hvv").
iSpecialize ("H" $! Δ with "Hs []").
{ iAlways. iApply interp_env_nil. }
rewrite !fmap_empty /env_subst !subst_p_empty. done.
Unshelve. all: rewrite /Closed /= in Hclosed Hclosed'; eauto.
Qed.
Definition counter_inv l cnt cnt' : iProp Σ :=
(∃ n, l ↦ₛ (#♭v false) ∗ cnt ↦ᵢ (#nv n) ∗ cnt' ↦ₛ (#nv n))%I.
......@@ -313,15 +276,13 @@ Section CG_Counter.
((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
(∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗
{E2,E1;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ))
-∗ ({E1,E1;Γ} ⊨ fill K (FG_increment (Loc x) Unit) ≤log≤ t : τ).
-∗ ({E1,E1;Γ} ⊨ fill K ((lamsubst FG_increment (LocV x)) Unit) ≤log≤ t : τ).
Proof.
iIntros "#H".
rel_bind_l (FG_increment _).
Transparent FG_increment. unfold FG_increment. unlock.
iApply (bin_log_related_rec_l _ E1 (_ ++ K)); auto. iNext. simpl.
Opaque FG_increment.
iIntros "#H".
Transparent FG_increment. unfold FG_increment. unlock. simpl.
iLöb as "IH".
iApply (bin_log_related_rec_l _ E1 K); auto. iNext. simpl.
Opaque FG_increment.
rel_bind_l (Load (Loc x)).
iPoseProof "H" as "H2". (* lolwhat *)
Opaque bin_log_related.
......@@ -357,31 +318,6 @@ Section CG_Counter.
iApply "IH".
Qed.
(* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
(* Closed ∅ (Lam x e) → *)
(* to_val (lang.subst x (of_val v) e) = Some ev → *)
(* Γ ⊨ (App (Lam x e) v) ≤log≤ t : τ *)
(* ⊢ Γ ⊨ (lang.subst x (of_val v) e) ≤log≤ t : τ. *)
(* Proof. *)
(* iIntros (??) "Hr". *)
(* Transparent bin_log_related. *)
(* iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". *)
(* cbn-[subst_p]. *)
(* (* assert (Closed ∅ (lang.subst x v e)). *) *)
(* (* { eapply is_closed_subst_preserve; eauto. solve_closed. } *) *)
(* rewrite /env_subst !Closed_subst_p_id. *)
(* iSpecialize ("Hr" with "Hs []"). *)
(* { iAlways. by iFrame. } *)
(* rewrite /env_subst. erewrite (Closed_subst_p_id (fst <$> vvs)); last first. *)
(* { rewrite /Closed. simpl. *)
(* rewrite /Closed /= in H1. split_and; eauto; try solve_closed. } *)
(* iMod ("Hr" with "Hj") as "Hr". *)
(* iModIntro. simpl. *)
(* rewrite {1}wp_unfold /wp_pre /=. *)
(* iApply wp_value; eauto. *)
(* iApply (wp_bind_inv in "Hr". *)
(* Opaque bin_log_related. *)
(* TODO: try to use with_lock rules *)
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
......@@ -389,94 +325,59 @@ Section CG_Counter.
Γ ⊨ FG_increment (Loc cnt) ≤log≤ CG_locked_increment (Loc cnt') (Loc l) : (TArrow TUnit TUnit).
Proof.
iIntros "#Hinv".
Transparent CG_locked_increment with_lock.
Transparent FG_increment.
unfold CG_locked_increment. unlock.
unfold FG_increment. unlock.
iApply (bin_log_related_rec_l _ ⊤ []); auto.
iNext. simpl.
rel_bind_r (App _ (#cnt')%E).
Transparent CG_locked_increment.
unfold CG_locked_increment. unlock.
iApply (bin_log_related_rec_r _ _); auto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _ _ []); auto. simpl. rewrite !Closed_subst_id.
unfold with_lock. unlock.
rel_bind_r (App _ (λ: "l", _))%E.
(* rel_bind_r (App _ (λ: "l", _))%E. *)
iApply (bin_log_related_rec_r Γ); eauto.
{ simpl. by rewrite decide_left. }
simpl. rewrite !Closed_subst_id.
(* Transparent with_lock. unfold with_lock. unlock. *)
(* iApply (bin_log_related_rec_r Γ); eauto. *)
(* { simpl. by rewrite decide_left. } *)
(* simpl. rewrite !Closed_subst_id. *)
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
(* iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id. *)
iApply bin_log_related_arrow.
iApply bin_log_related_arrow.
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
(* TODO: cannot use FG_increment_logatomic atm *)
(* iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]"). *)
(* iAlways. *)
(* iInv counterN as ">Hcnt" "Hcl". iModIntro. *)
(* iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". *)
(* iExists n. iFrame. clear n. *)
(* iSplit. *)
(* - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]". *)
(* iMod ("Hcl" with "[-]"). *)
(* { iNext. iExists _. iFrame. } *)
(* done. *)
(* - iIntros (m) "[Hcnt [Hl Hcnt']]". *)
(* iApply (bin_log_related_CG_locked_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj. } *)
(* iIntros "Hcnt' Hl". *)
(* iMod ("Hcl" with "[-]"). *)
(* { iNext. iExists _. iFrame. } *)
(* simpl. *)
(* iApply bin_log_related_unit. *)
(* Opaque CG_locked_increment with_lock. *)
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
iLöb as "IH".
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
rel_bind_l (! #cnt)%E.
iApply (bin_log_related_load_l).
iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
iExists (#nv n). iFrame. iIntros "Hcnt".
iMod ("Hcl" with "[-]"); simpl.
{ iNext. iExists _. iFrame. }
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
rel_bind_l (BinOp Add _ _).
iApply bin_log_related_binop_l. iNext. simpl.
rel_bind_l (CAS _ _ _).
iApply (bin_log_related_cas_l); eauto.
(* :( *)
replace (rec: "inc" <>
:= (λ: "c",
if: CAS #cnt "c" (BinOp Add (Nat 1) "c") then #() else "inc" #())
! #cnt)%E with (lamsubst FG_increment (LocV cnt)); last first.
{ unfold FG_increment. unlock. reflexivity. }
Opaque FG_increment.
replace (λ: <>,
acquire #l ;; (CG_increment #cnt') #() ;; release #l)%E
with (lamsubst (lamsubst CG_locked_increment (LocV cnt')) (LocV l)); last first.
{ unfold CG_locked_increment. unlock. simpl.
rewrite !Closed_subst_id. reflexivity. }
Opaque CG_locked_increment.
iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
iAlways.
iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (m) "[Hl [Hcnt Hcnt']]".
iExists _; iFrame.
destruct (decide (m = n)) as [|Hmn]; subst.
- (* CASE [m = n], CAS successful *)
iSplitR. iIntros "%". by exfalso.
iIntros "% Hcnt".
rel_bind_r (acquire #l).
iApply (bin_log_related_acquire_r with "Hl"); simpl; eauto. solve_ndisj.
iIntros "Hl".
iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj.
rel_bind_r (App _ #())%E.
iApply (bin_log_related_rec_r _ _); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
rel_bind_r (CG_increment _ _).
iApply (bin_log_related_CG_increment_r with "Hcnt'"). solve_ndisj. simpl.
iIntros "Hcnt'".
iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
rel_bind_r (release #l)%E.
iApply (bin_log_related_release_r with "Hl"). solve_ndisj.
iIntros "Hl". simpl.
iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
iExists n. iFrame. clear n.
iSplit.
- iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. by iFrame. }
iApply (bin_log_related_if_true_l _ _ []). iNext. simpl.
iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto.
iApply bin_log_related_unit.
- (* CASE [m ≠ n], CAS fails *)
iSplitL; last first. iIntros "%". exfalso. apply Hmn. by inversion H1.
iIntros "% Hcnt". simpl.
{ iNext. iExists _. iFrame. }
done.
- iIntros (m) "[Hcnt [Hl Hcnt']]".
iApply (bin_log_related_CG_locked_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj. }
iIntros "Hcnt' Hl".
iMod ("Hcl" with "[-]").
{ iNext. iExists _. by iFrame. }
iApply (bin_log_related_if_false_l _ _ []). iNext. simpl.
iApply "IH".
{ iNext. iExists _. iFrame. }
simpl.
iApply bin_log_related_unit.
Qed.
Lemma FG_CG_counter_refinement :
......
F_mu_ref_conc/hax.v 0 → 100644
View file @ 08817aea
(* the contents of this file sould belong elsewhere *)
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import lang subst tactics rules rules_binary logrel_binary.
Definition lamsubst (e : expr) (v : val) : expr :=
match e with
| Rec (BNamed f) x e' => lang.subst f e (subst' x (of_val v) e')
| Rec BAnon x e' => subst' x (of_val v) e'
| _ => e
end.
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : _ = of_val ?v |- _ =>
is_var v; destruct v; first[discriminate H|injection H as H]
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Section hax.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
Lemma bin_log_related_arrow Γ (f x f' x' : binder) (e e' : expr) (τ τ' : type)
(Hclosed : Closed ∅ (rec: f x := e)%E )
(Hclosed' : Closed ∅ (rec: f' x' := e')%E) :
□(∀ Δ vv, ⟦ τ ⟧ Δ vv -∗
∅ ⊨ App (Rec f x e) (of_val (vv.1)) ≤log≤ App (Rec f' x' e') (of_val (vv.2)) : τ') -∗
Γ ⊨ (Rec f x e) ≤log≤ (Rec f' x' e') : TArrow τ τ'.
Proof.
iIntros "#H".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
cbn-[subst_p]. rewrite /env_subst !Closed_subst_p_id.
iModIntro. iApply wp_value; auto.
{ simpl. erewrite decide_left. done. }
iExists (RecV f' x' e'). simpl.
iFrame "Hj". iAlways. iIntros (vv) "Hvv".
iSpecialize ("H" $! Δ vv with "Hvv").
iSpecialize ("H" $! Δ with "Hs []").
{ iAlways. iApply interp_env_nil. }
rewrite !fmap_empty /env_subst !subst_p_empty. done.
Unshelve. all: rewrite /Closed /= in Hclosed Hclosed'; eauto.
Qed.
Lemma weird_bind e Q :
WP App e #() {{ Q }} ⊢ WP e {{ v, WP (App v #()) {{ Q }} }}.
Proof.
(* ugh, turns out this is just the inverse bind:
Check (wp_bind_inv (fun v => App v #())). *)
iLöb as "IH" forall (e).
iIntros "wp".
rewrite (wp_unfold _ e) /wp_pre /=.
remember (to_val e) as eval. destruct eval.
- symmetry in Heqeval. rewrite -(of_to_val _ _ Heqeval). eauto.
- iIntros (σ1) "Hσ1".
rewrite wp_unfold /wp_pre /=.
iMod ("wp" $! σ1 with "Hσ1") as "[r wp]". iModIntro.
iDestruct "r" as %er.
assert (reducible e σ1).
{ symmetry in Heqeval.
unfold reducible in er.
destruct er as (e2 & σ2 & efs & Hpst).
inversion Hpst; simpl in *; subst; clear Hpst.
admit. }
iSplitR; eauto.
iNext.
iIntros (e2 σ2 efs) "Hpst". iDestruct "Hpst" as %Hpst.
iSpecialize ("wp" $! (App e2 #()) σ2 efs).
iAssert (⌜prim_step (e #()%E) σ1 (e2 #()%E) σ2 efs⌝)%I as "Hprim'".
{ iPureIntro.
inversion Hpst; simpl in *; subst; clear Hpst.
eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (#())%E])); simpl; eauto.
by rewrite fill_app.
by rewrite fill_app. }
iMod ("wp" with "Hprim'") as "[$ [wp $]]". iModIntro.
by iApply "IH".
Admitted.
(* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
(* Closed ∅ (Lam x e) → *)
(* to_val (lang.subst x (of_val v) e) = Some ev → *)
(* Γ ⊨ (App (Lam x e) v) ≤log≤ t : τ *)
(* ⊢ Γ ⊨ (lang.subst x (of_val v) e) ≤log≤ t : τ. *)
(* Proof. *)
(* iIntros (??) "Hr". *)
(* Transparent bin_log_related. *)
(* iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". *)
(* cbn-[subst_p]. *)
(* (* assert (Closed ∅ (lang.subst x v e)). *) *)
(* (* { eapply is_closed_subst_preserve; eauto. solve_closed. } *) *)
(* rewrite /env_subst !Closed_subst_p_id. *)
(* iSpecialize ("Hr" with "Hs []"). *)
(* { iAlways. by iFrame. } *)
(* rewrite /env_subst. erewrite (Closed_subst_p_id (fst <$> vvs)); last first. *)
(* { rewrite /Closed. simpl. *)
(* rewrite /Closed /= in H1. split_and; eauto; try solve_closed. } *)
(* iMod ("Hr" with "Hj") as "Hr". *)
(* iModIntro. simpl. *)
(* rewrite {1}wp_unfold /wp_pre /=. *)
(* iApply wp_value; eauto. *)
(* iApply (wp_bind_inv in "Hr". *)
End hax.
_CoqProject
View file @ 08817aea
......@@ -5,6 +5,7 @@ prelude/base.v
F_mu_ref_conc/binder.v
F_mu_ref_conc/lang.v
F_mu_ref_conc/subst.v
F_mu_ref_conc/hax.v
F_mu_ref_conc/reflection.v
F_mu_ref_conc/rules.v
F_mu_ref_conc/typing.v
......
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