Commit e803a554 authored by Dan Frumin's avatar Dan Frumin

Generalize some lemmas about the relational interpretation

And improve the proof of the fundamental property
parent 8c470b74
......@@ -265,13 +265,13 @@ Section bin_log_related_under_typed_ctx.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_pair with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_fst.
+ iApply bin_log_related_fst; first by auto.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_snd.
+ iApply bin_log_related_snd; first by auto.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_injl.
+ iApply bin_log_related_injl; first done.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_injr.
+ iApply bin_log_related_injr; first done.
iApply (IHK with "[Hrel]"); auto.
+ inversion Hx2; subst.
* iApply (bin_log_related_case with "[] []"); try fundamental.
......@@ -311,7 +311,7 @@ Section bin_log_related_under_typed_ctx.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fold with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_unfold with "[]"); try fundamental.
+ iApply (bin_log_related_unfold with "[]"); auto; try fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tlam with "[]"); try fundamental.
iAlways. iApply (IHK with "[Hrel]"); auto.
......
......@@ -10,8 +10,8 @@ Section bin_log_def.
Definition bin_log_related (E1 E2 : coPset) (Γ : list type) (e e' : expr) (τ : type) : iProp Σ := ( Δ vvs ρ,
spec_ctx ρ -
Γ * Δ vvs
- interp_expr E1 E2 ( τ ) Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)]))%I.
interp_env Γ Δ vvs
- interp_expr E1 E2 (interp τ) Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)]))%I.
End bin_log_def.
Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
......@@ -33,7 +33,8 @@ Section fundamental.
wp_bind e;
tp_bind j e';
iSpecialize (IH with "* Hs [HΓ] * Hj"); eauto;
iApply fupd_wp; iMod IH as IH; iModIntro;
iApply fupd_wp; iApply (fupd_mask_mono _); auto;
iMod IH as IH; iModIntro;
iApply (wp_wand with IH);
iIntros (v);
let vh := iFresh in
......@@ -47,7 +48,8 @@ Section fundamental.
Proof.
iIntros (? Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[% ?]"; first done.
rewrite /env_subst !list_lookup_fmap; simplify_option_eq. value_case; eauto.
rewrite /env_subst !list_lookup_fmap; simplify_option_eq.
value_case; eauto.
Qed.
Lemma bin_log_related_unit Γ E : {E,E;Γ} Unit log Unit : TUnit.
......@@ -82,39 +84,42 @@ Section fundamental.
iSplit; simpl; eauto. auto.
Qed.
Lemma bin_log_related_fst Γ e e' τ1 τ2 :
Γ e log e' : TProd τ1 τ2 -
Γ Fst e log Fst e' : τ1.
Lemma bin_log_related_fst Γ E e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : TProd τ1 τ2 -
{E,E;Γ} Fst e log Fst e' : τ1.
Proof.
iIntros "IH".
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j e.[_] e'.[_] "IH" v w "IH".
iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]".
inversion H1; subst.
simplify_eq.
iApply wp_fst; eauto. iNext.
iExists v2.
tp_fst j; eauto. tp_normalise j. eauto.
Qed.
Lemma bin_log_related_snd Γ e e' τ1 τ2 :
Γ e log e' : TProd τ1 τ2 -
Γ Snd e log Snd e' : τ2.
Lemma bin_log_related_snd Γ E e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : TProd τ1 τ2 -
{E,E;Γ} Snd e log Snd e' : τ2.
Proof.
iIntros "IH".
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j e.[_] e'.[_] "IH" v w "IH".
iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]".
inversion H1; subst.
simplify_eq.
iApply wp_snd; eauto. iNext.
iExists w2.
tp_snd j; eauto. tp_normalise j. eauto.
Qed.
Lemma bin_log_related_injl Γ e e' τ1 τ2 :
Γ e log e' : τ1 -
Γ InjL e log InjL e' : (TSum τ1 τ2).
Lemma bin_log_related_injl Γ E e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : τ1 -
{E,E;Γ} InjL e log InjL e' : (TSum τ1 τ2).
Proof.
iIntros "IH".
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j e.[_] e'.[_] "IH" v w "IH".
value_case. tp_normalise j.
......@@ -122,11 +127,12 @@ Section fundamental.
iLeft. iExists (_,_); eauto 10.
Qed.
Lemma bin_log_related_injr Γ e e' τ1 τ2 :
Γ e log e' : τ2 -
Γ InjR e log InjR e' : TSum τ1 τ2.
Lemma bin_log_related_injr Γ E e e' τ1 τ2 :
specN E
{E,E;Γ} e log e' : τ2 -
{E,E;Γ} InjR e log InjR e' : TSum τ1 τ2.
Proof.
iIntros "IH".
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j e.[_] e'.[_] "IH" v w "IH".
value_case. tp_normalise j.
......@@ -220,13 +226,14 @@ Section fundamental.
try destruct lt_dec; eauto.
Qed.
Lemma bin_log_related_rec Γ (e e' : expr) τ1 τ2
Lemma bin_log_related_rec Γ E (e e' : expr) τ1 τ2
(Hclosed : f, e.[upn (S (S (length Γ))) f] = e)
(Hclosed' : f, e'.[upn (S (S (length Γ))) f] = e') :
(TArrow τ1 τ2 :: τ1 :: Γ e log e' : τ2) -
Γ Rec e log Rec e' : TArrow τ1 τ2.
( specN E)
({E,E;TArrow τ1 τ2 :: τ1 :: Γ} e log e' : τ2) -
{E,E;Γ} Rec e log Rec e' : TArrow τ1 τ2.
Proof.
iIntros "#Ht".
iIntros (?) "#Ht".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
value_case. iExists (RecV _). iIntros "{$Hj} !#".
iLöb as "IH". iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj".
......@@ -236,17 +243,19 @@ Section fundamental.
tp_rec j'; eauto; tp_normalise j'.
asimpl. change (Rec ?e) with (of_val (RecV e)).
erewrite !n_closed_subst_head_simpl_2 by (rewrite ?fmap_length; eauto).
iAssert ( TArrow τ1 τ2 :: τ1 :: Γ * Δ ((RecV e.[_], RecV e'.[_])::(v,v')::vvs)) as "#HΓ'".
iAssert (interp_env (TArrow τ1 τ2 :: τ1 :: Γ) Δ ((RecV e.[_], RecV e'.[_])::(v,v')::vvs)) as "#HΓ'".
{ iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto. }
iSpecialize ("Ht" with "* Hs [HΓ']"); eauto.
iSpecialize ("Ht" with "* Hs [HΓ']"); eauto. simpl.
iSpecialize ("Ht" with "* Hj").
iApply "Ht".
simpl.
iApply (fupd_mask_mono E); auto.
Qed.
Lemma bin_log_related_app Γ e1 e2 e1' e2' τ1 τ2 :
Γ e1 log e1' : TArrow τ1 τ2 -
Γ e2 log e2' : τ1 -
Γ App e1 e2 log App e1' e2' : τ2.
(* Cannot write a sensible instance with an arbitrary mask *)
Lemma bin_log_related_app Γ E e1 e2 e1' e2' τ1 τ2 :
{E,E;Γ} e1 log e1' : TArrow τ1 τ2 -
{E,E;Γ} e2 log e2' : τ1 -
{E,E;Γ} App e1 e2 log App e1' e2' : τ2.
Proof.
iIntros "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
......@@ -307,11 +316,12 @@ Section fundamental.
iAlways; iExists (_, _); eauto.
Qed.
Lemma bin_log_related_unfold Γ e e' τ :
Γ e log e' : TRec τ -
Γ Unfold e log Unfold e' : τ.[(TRec τ)/].
Lemma bin_log_related_unfold Γ E e e' τ :
(specN E)
{E,E;Γ} e log e' : TRec τ -
{E,E;Γ} Unfold e log Unfold e' : τ.[(TRec τ)/].
Proof.
iIntros "IH".
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j e.[_] e'.[_] "IH" v v' "#IH".
rewrite /= fixpoint_unfold /=.
......@@ -490,54 +500,45 @@ Section fundamental.
iExists (#v false); repeat iModIntro; eauto.
Qed.
Ltac induct_case := repeat
lazymatch goal with
| [H : uPred_valid (?Γ ?e1 log ?e2 : ?t) |-
_ ?Γ ?e1 log _ : _] =>
let G := iFresh in by iPoseProof H as G
end.
Opaque bin_log_related.
(* Without this iApply doesn't work and iInduction is very slow *)
Theorem binary_fundamental Γ e τ :
Γ ⊢ₜ e : τ Γ e log e : τ.
Γ ⊢ₜ e : τ (Γ e log e : τ)%I.
Proof.
induction 1.
- by apply bin_log_related_var.
- by apply bin_log_related_unit.
- by apply bin_log_related_nat.
- by apply bin_log_related_bool.
- iApply (bin_log_related_nat_binop with "[]");
induct_case.
- iApply (bin_log_related_pair with "[]");
induct_case.
- iApply bin_log_related_fst; induct_case.
- iApply bin_log_related_snd; induct_case.
- iApply bin_log_related_injl; induct_case.
- iApply bin_log_related_injr; induct_case.
- iApply (bin_log_related_case with "[] []"); induct_case.
intros Ht. iInduction Ht as [] "IH".
- by iApply bin_log_related_var.
- iApply bin_log_related_unit.
- by iApply bin_log_related_nat.
- by iApply bin_log_related_bool.
- by iApply (bin_log_related_nat_binop with "[]").
- by iApply (bin_log_related_pair with "[]").
- by iApply bin_log_related_fst.
- by iApply bin_log_related_snd.
- by iApply bin_log_related_injl.
- by iApply bin_log_related_injr.
- iApply (bin_log_related_case with "[] []"); eauto.
all: repeat lazymatch goal with
[ H : (?Γ ⊢ₜ ?e : ?t) |- f, ?e.[_] = ?e ] =>
try eapply (typed_n_closed _ _ _ H)
end.
- iApply (bin_log_related_if with "[] []"); induct_case.
- iApply (bin_log_related_rec with "[]");
- by iApply (bin_log_related_if with "[] []").
- iApply (bin_log_related_rec with "[]"); eauto;
repeat lazymatch goal with
[ H : (?Γ ⊢ₜ ?e : ?t) |- f, ?e.[_] = ?e ] =>
try eapply (typed_n_closed _ _ _ H)
end.
iAlways. induct_case.
- iApply (bin_log_related_app with "[] []"); induct_case.
- iApply bin_log_related_tlam. iAlways. induct_case.
- iApply bin_log_related_tapp; induct_case.
- iApply bin_log_related_fold; induct_case.
- iApply bin_log_related_unfold; induct_case.
- iApply bin_log_related_pack; induct_case.
- iApply (bin_log_related_unpack with "[]"); induct_case; eauto.
- iApply bin_log_related_fork; induct_case.
- iApply bin_log_related_alloc; induct_case.
- iApply bin_log_related_load; induct_case.
- iApply (bin_log_related_store with "[]"); induct_case.
- iApply (bin_log_related_CAS with "[] []"); induct_case.
auto.
- by iApply (bin_log_related_app with "[] []").
- by iApply bin_log_related_tlam.
- by iApply bin_log_related_tapp.
- by iApply bin_log_related_fold.
- by iApply bin_log_related_unfold.
- by iApply bin_log_related_pack.
- by iApply (bin_log_related_unpack with "[]").
- by iApply bin_log_related_fork.
- by iApply bin_log_related_alloc.
- by iApply bin_log_related_load.
- by iApply (bin_log_related_store with "[]").
- by iApply (bin_log_related_CAS with "[] []").
Qed.
End fundamental.
......@@ -35,7 +35,7 @@ Section logrel.
Definition interp_expr (E1 E2 : coPset) (τi : listC D -n> D) (Δ : listC D)
(ee : expr * expr) : iProp Σ := ( j K,
j fill K (ee.2) -
|={E1,E2}=> WP ee.1 @ E2 {{ v, v', j fill K (of_val v') τi Δ (v, v') }})%I.
|={E1,E2}=> WP ee.1 {{ v, v', j fill K (of_val v') τi Δ (v, v') }})%I.
Global Instance interp_expr_ne n E1 E2:
Proper (dist n ==> dist n ==> (=) ==> dist n) (interp_expr E1 E2).
Proof. solve_proper. Qed.
......
......@@ -51,14 +51,14 @@ Section properties.
(** ** Reductions on the left *)
(** Lifting of the pure reductions *)
Lemma bin_log_pure_l Γ τ e e' t K'
Lemma bin_log_pure_l Γ E τ e e' t K'
(Hclosed : f, e.[f] = e)
(Hclosed' : f, e'.[f] = e')
(Hsafe : σ, head_reducible e σ) :
to_val e = None ->
( σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs)
(Γ fill K' e' log t : τ)
Γ fill K' e log t : τ.
({E,E;Γ} fill K' e' log t : τ)
{E,E;Γ} fill K' e log t : τ.
Proof.
iIntros (Hval Hstep) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
......@@ -69,8 +69,8 @@ Section properties.
iSpecialize ("IH" with "* Hs [HΓ] * Hj"); auto. simpl.
rewrite fill_subst.
rewrite -{2}(Hclosed' (env_subst (vvs.*1))).
iApply wp_bind_inv. iMod "IH".
done.
iApply wp_bind_inv. iApply fupd_wp.
iApply (fupd_mask_mono E); auto.
Qed.
Lemma bin_log_related_fst_l Γ K e v1 v2 τ
......@@ -99,12 +99,12 @@ Section properties.
- by inversion H1.
Qed.
Lemma bin_log_related_rec_l Γ K e e' v t τ
Lemma bin_log_related_rec_l Γ E K e e' v t τ
(Hclosed1 : f, e.[upn 2 f] = e)
(Hclosed2 : f, e'.[f] = e') :
(to_val e' = Some v)
(Γ (fill K (e.[(Rec e), e' /])) log t : τ)
Γ (fill K (App (Rec e) e')) log t : τ.
({E,E;Γ} (fill K (e.[(Rec e), e' /])) log t : τ)
{E,E;Γ} (fill K (App (Rec e) e')) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -210,11 +210,11 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_if_true_l Γ K e1 e2 t τ
Lemma bin_log_related_if_true_l Γ E K e1 e2 t τ
(Hclosed1 : f, e1.[f] = e1)
(Hclosed2 : f, e2.[f] = e2) :
(Γ fill K e1 log t : τ)
Γ (fill K (If (# true) e1 e2)) log t : τ.
({E,E;Γ} fill K e1 log t : τ)
{E,E;Γ} (fill K (If (# true) e1 e2)) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -240,9 +240,9 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_binop_l Γ K op a b t τ :
(Γ fill K (of_val (binop_eval op a b)) log t : τ)
Γ (fill K (BinOp op (#n a) (#n b))) log t : τ.
Lemma bin_log_related_binop_l Γ E K op a b t τ :
({E,E;Γ} fill K (of_val (binop_eval op a b)) log t : τ)
{E,E;Γ} (fill K (BinOp op (#n a) (#n b))) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -265,74 +265,65 @@ Section properties.
rewrite fill_subst /=.
rewrite Hclosed1.
iApply (wp_bind (subst_ctx (env_subst (vvs.*1)) K)).
iMod "He".
iApply fupd_wp. iApply (fupd_mask_mono E1); auto.
iMod "He". iModIntro.
iApply (wp_mask_mono E1); auto.
iApply (wp_wand with "He").
iIntros (v) "[Hv Hcl]". iDestruct "Hcl" as %Hclosed_v.
iSpecialize ("Hlog" $! v with "Hv * Hs [HΓ]"); first by iFrame.
iSpecialize ("Hlog" with "* Hj"). simpl.
rewrite fill_subst /=. rewrite Hclosed_v.
iMod "Hlog".
iDestruct (wp_bind_inv with "Hlog") as "Hlog".
iDestruct (wp_value_inv with "Hlog") as "Hlog".
iMod "Hlog".
done.
iApply fupd_wp. iApply (fupd_mask_mono E1); auto.
Qed.
Lemma bin_log_related_atomic_l K Γ E1 E2 e1 e2 τ
Lemma bin_log_related_wp_atomic_l K Γ (E1 E2 : coPset) e1 e2 τ
(Hatomic : atomic e1)
(Hclosed1 : f, e1.[f] = e1) :
(|={E1,E2}=> WP e1 @ E2 {{ v,
⌜∀ f, (of_val v).[f] = of_val v
|={E2,E1}=>{E1,E1;Γ} fill K (of_val v) log e2 : τ }})%I -
{E2,E1;Γ} fill K (of_val v) log e2 : τ }})%I -
{E1,E1;Γ} fill K e1 log e2 : τ.
Proof.
iIntros "He".
iIntros "Hlog".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
rewrite fill_subst /=.
rewrite Hclosed1.
iApply (wp_bind (subst_ctx (env_subst (vvs.*1)) K)).
iApply wp_atomic; auto.
iMod "He".
iApply (wp_mask_mono E1); auto.
iMod "Hlog" as "He".
iApply (wp_wand with "He").
iIntros (v) "[% Hv]".
iMod "Hv".
iSpecialize ("Hv" with "* Hs [HΓ] * Hj"); auto.
iMod "Hv". simpl.
rewrite fill_subst /=. rewrite H1.
iIntros (v) "[Hcl Hlog]". iDestruct "Hcl" as %Hclosed_v.
iSpecialize ("Hlog" with "* Hs [HΓ]"); first by iFrame.
iSpecialize ("Hlog" with "* Hj"). simpl.
rewrite fill_subst /=. rewrite Hclosed_v.
iMod "Hlog".
iDestruct (wp_bind_inv with "Hlog") as "Hlog".
iDestruct (wp_value_inv with "Hlog") as "Hlog".
iModIntro. iMod "Hlog".
done.
Qed.
Lemma bin_log_related_alloc_l_alt Γ E1 E2 K e v t τ
(Heval : to_val e = Some v)
(Hclosed : f, e.[f] = e) :
(|={E1,E2}=> (l : loc), l ↦ᵢ v -
|={E2,E1}=>{E1,E1;Γ} fill K (Loc l) log t : τ)%I
- {E1,E1;Γ} fill K (Alloc e) log t : τ.
Lemma bin_log_related_bind_l K Γ E e1 e2 τ
(Hclosed1 : f, e1.[f] = e1) :
(WP e1 @ E {{ v,
⌜∀ f, (of_val v).[f] = of_val v
{E,E;Γ} fill K (of_val v) log e2 : τ }})%I -
{E,E;Γ} fill K e1 log e2 : τ.
Proof.
iIntros "Hsafe".
iApply bin_log_related_atomic_l; auto.
{ intro f. asimpl. by rewrite Hclosed. }
iMod "Hsafe". iModIntro.
iApply wp_alloc. apply Heval.
iNext. iIntros (l) "Hl".
iSpecialize ("Hsafe" with "* Hl").
iSplitR; eauto.
iIntros "He".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
rewrite fill_subst /=.
rewrite Hclosed1. iModIntro.
iApply (wp_bind (subst_ctx (env_subst (vvs.*1)) K)).
iApply (wp_mask_mono E); auto.
iApply (wp_wand with "He").
iIntros (v) "[% Hv]".
iApply fupd_wp. iApply (fupd_mask_mono E); auto.
iMod ("Hv" with "* Hs [HΓ] * Hj"); auto.
rewrite fill_subst /=. rewrite H1.
done.
Qed.
Lemma bin_log_related_load_l_alt E1 E2 Γ K l t τ :
(|={E1,E2}=> v', ⌜∀ f, (of_val v').[f] = of_val v'⌝
(l ↦ᵢ v')
(l ↦ᵢ v' - (|={ E2,E1}=> {E1,E1;Γ} fill K (of_val v') log t : τ)))%I
- {E1,E1;Γ} fill K (Load (Loc l)) log t : τ.
Proof.
iIntros "Hsafe".
iApply bin_log_related_atomic_l; auto.
iMod "Hsafe" as (v') "[% [Hl Hsafe]]". iModIntro.
iApply (wp_load with "Hl").
iNext. iIntros "Hl".
iSpecialize ("Hsafe" with "* Hl").
iSplitR; eauto.
Qed.
Lemma bin_log_related_step_atomic_l {A} (Φ : A val iProp Σ) K Γ E1 E2 e1 e2 τ
(Hatomic : atomic e1)
......@@ -342,21 +333,11 @@ Section properties.
{E1,E1;Γ} fill K e1 log e2 : τ.
Proof.
iIntros "Hlog".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
rewrite fill_subst /=.
rewrite Hclosed1.
iApply (wp_bind (subst_ctx (env_subst (vvs.*1)) K)).
iMod "Hlog" as (a) "[He Hlog]".
iApply bin_log_related_wp_atomic_l; auto.
iMod "Hlog" as (a) "[He Hlog]". iModIntro.
iApply (wp_wand with "He").
iIntros (v) "[Hv Hcl]". iDestruct "Hcl" as %Hclosed_v.
iSpecialize ("Hlog" $! v with "Hv * Hs [HΓ]"); first by iFrame.
iSpecialize ("Hlog" with "* Hj"). simpl.
rewrite fill_subst /=. rewrite Hclosed_v.
iMod "Hlog".
iDestruct (wp_bind_inv with "Hlog") as "Hlog".
iDestruct (wp_value_inv with "Hlog") as "Hlog".
iMod "Hlog".
done.
iIntros (v) "[HΦ $]".
iApply ("Hlog" with "* HΦ").
Qed.
(* TODO: how to make eauto do this? *)
......
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