Commit 7947eab3 authored by Amin Timany's avatar Amin Timany

Remove some superfluous later operators (▷)

parent 73b0c36c
......@@ -74,12 +74,12 @@ Section typed_interp.
smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_fst; eauto using to_of_val; cbn.
iApply wp_fst; try iNext; eauto using to_of_val; cbn.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_snd; eauto using to_of_val.
iApply wp_snd; try iNext; eauto using to_of_val.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
......@@ -109,8 +109,9 @@ Section typed_interp.
- (* TLam *)
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto; try iExact "HP".
iIntros "#HΓ"; iNext.
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try iExact "HP".
iIntros "#HΓ".
iApply IHHtyped; [rewrite map_length|]; trivial.
iRevert "HΓ".
rewrite zip_with_context_interp_subst.
......
......@@ -95,7 +95,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( w1 w2, w = PairV w1 w2 τ1i w1 τ2i w2)%I
λ w, ( w1 w2, w = PairV w1 w2 τ1i w1 τ2i w2)%I
|}
|}
|}.
......@@ -115,8 +115,8 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, (( w1, w = InjLV w1 τ1i w1)
( w2, w = InjRV w2 τ2i w2))%I
λ w, (( w1, w = InjLV w1 τ1i w1)
( w2, w = InjRV w2 τ2i w2))%I
|}
|}
|}.
......@@ -136,7 +136,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
|}
|}
|}.
......@@ -159,7 +159,7 @@ Section logrel.
( e, w = TLamV e
(τ'i : {f : (leibniz_val -n> iProp lang Σ) |
Val_to_IProp_Persistent f}),
( WP e @ {{λ v, (τi (`τ'i) v)}}))%I
(WP e @ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
......@@ -170,7 +170,7 @@ Section logrel.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
apply forall_ne=> P.
apply always_ne, (contractive_ne _), wp_ne => w.
apply always_ne, wp_ne => w.
rewrite Hfg; trivial.
Qed.
......
......@@ -86,12 +86,12 @@ Section typed_interp.
smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_fst; eauto using to_of_val; cbn.
iApply wp_fst; try iNext; eauto using to_of_val; cbn.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_snd; eauto using to_of_val; cbn.
iApply wp_snd; try iNext; eauto using to_of_val; cbn.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
......@@ -124,7 +124,7 @@ Section typed_interp.
iRevert "Hheap".
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try (iApply always_impl; iExact "HP").
iIntros "#HΓ #Hheap"; iNext.
iIntros "#HΓ #Hheap".
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
iRevert "Hheap HΓ". rewrite zip_with_context_interp_subst.
......
......@@ -100,7 +100,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( w1 w2, w = PairV w1 w2 τ1i w1 τ2i w2)%I
λ w, ( w1 w2, w = PairV w1 w2 τ1i w1 τ2i w2)%I
|}
|}
|}.
......@@ -120,8 +120,8 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, (( w1, w = InjLV w1 τ1i w1)
( w2, w = InjRV w2 τ2i w2))%I
λ w, (( w1, w = InjLV w1 τ1i w1)
( w2, w = InjRV w2 τ2i w2))%I
|}
|}
|}.
......@@ -141,7 +141,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
|}
|}
|}.
......@@ -164,7 +164,7 @@ Section logrel.
( e, w = TLamV e
(τ'i : {f : (leibniz_val -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
( WP e @ {{λ v, (τi (`τ'i) v)}}))%I
(WP e @ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
......@@ -175,7 +175,7 @@ Section logrel.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
apply forall_ne=> P.
apply always_ne, (contractive_ne _), wp_ne => w.
apply always_ne, wp_ne => w.
rewrite Hfg; trivial.
Qed.
......
......@@ -326,7 +326,7 @@ Section CG_Counter.
- (* refinement of increment *)
iAlways. clear j K. iIntros {j K v} "[#Heq Hj]".
rewrite CG_locked_increment_of_val. simpl.
iTimeless "Heq". destruct v; iDestruct "Heq" as "[% %]"; simpl in *;subst.
destruct v; iDestruct "Heq" as "[% %]"; simpl in *;subst.
iLöb as "Hlat".
iApply wp_lam; trivial. asimpl.
iNext.
......@@ -367,11 +367,11 @@ Section CG_Counter.
{ abstract prove_disj N 2 4. }
iNext; iFrame "Hcnt"; iIntros "Hcnt".
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_false. iNext. iApply "Hlat". iNext; trivial.
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of read *)
iAlways. clear j K. iIntros {j K v} "[#Heq Hj]".
rewrite ?counter_read_of_val.
iTimeless "Heq". destruct v; iDestruct "Heq" as "[% %]".
destruct v; iDestruct "Heq" as "[% %]".
simpl in *; subst; simpl.
Transparent counter_read.
unfold counter_read at 2.
......
......@@ -38,7 +38,7 @@ Section Stack_refinement.
iExists (TLamV _); iFrame "Hj".
iExists (_, _); iSplit; eauto.
iIntros {τi}. destruct τi as [τi Hτ]; simpl.
iAlways. iNext. clear j K. iIntros {j K} "Hj".
iAlways. clear j K. iIntros {j K} "Hj".
iPvs (steps_newlock _ _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
as {l} "[Hj Hl]"; eauto.
rewrite fill_app; simpl.
......@@ -163,11 +163,11 @@ Section Stack_refinement.
iFrame "Hheap Hstk". iNext. iIntros "Hstk".
iSplitR "Hj".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply wp_if_false. iNext. iApply "Hlat". by iNext.
iApply wp_if_false. iNext. by iApply "Hlat".
+ (* refinement of pop *)
iAlways. clear j K. iIntros {j K v}. destruct v as [v1 v2].
iIntros "[#Hrel Hj]". simpl.
iTimeless "Hrel". iDestruct "Hrel" as "[% %]". subst.
iDestruct "Hrel" as "[% %]". subst.
rewrite -(FG_pop_folding (Loc stk)).
iLöb as "Hlat".
rewrite -> (FG_pop_folding (Loc stk)) at 2.
......@@ -302,10 +302,10 @@ Section Stack_refinement.
iFrame "Hheap Hstk". iNext. iIntros "Hstk".
iSplitR "Hj".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". }
iApply wp_if_false. iNext. iApply "Hlat". by iNext.
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of iter *)
iAlways. clear j K. iIntros {j K f}. destruct f as [f1 f2]. simpl.
rewrite -always_later. iIntros "[#Hfs Hj]".
iIntros "[#Hfs Hj]".
iApply wp_lam; auto using to_of_val. iNext.
iPvs (step_lam _ _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
{ by iFrame "Hspec Hj". }
......
......@@ -268,7 +268,7 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]"
(IHHtyped2 _ _ _ j (K ++ [AppRCtx v'])); cbn.
iApply ("Hiv" $! j K (w, w')); simpl.
iNext; iFrame "Hw"; trivial.
iFrame "Hw"; trivial.
(* unshelving *)
Unshelve. all: trivial.
Qed.
......@@ -285,7 +285,7 @@ Section typed_interp.
iExists (e.[env_subst (map fst vs)], e'.[env_subst (map snd vs)]).
iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iAlways. iNext. iIntros {j' K'} "Hv". simpl.
iAlways. iIntros {j' K'} "Hv". simpl.
iApply IHHtyped; [rewrite map_length; trivial|].
iFrame "Hheap Hspec Hv".
rewrite zip_with_context_interp_subst; trivial.
......
......@@ -91,12 +91,12 @@ Section typed_interp.
smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_fst; eauto using to_of_val; cbn.
iApply wp_fst; try iNext; eauto using to_of_val; cbn.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_snd; eauto using to_of_val; cbn.
iApply wp_snd; try iNext; eauto using to_of_val; cbn.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
......@@ -137,7 +137,7 @@ Section typed_interp.
iRevert "Hheap".
iPoseProof (always_intro with "HΓ") as "HP"; try typeclasses eauto;
try (iApply always_impl; iExact "HP").
iIntros "#HΓ #Hheap"; iNext.
iIntros "#HΓ #Hheap".
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
iRevert "Hheap HΓ". rewrite zip_with_context_interp_subst.
......
......@@ -188,7 +188,7 @@ Section logrel.
{|
cofe_mor_car :=
λ w, ( j K v,
τ1i v j (fill K (App (# w.2) (# v.2)))
τ1i v j (fill K (App (# w.2) (# v.2)))
WP (App (# w.1) (# v.1)) @
{{z, z', j (fill K (# z')) τ2i (z, z')}})%I
|}
......@@ -227,7 +227,7 @@ Section logrel.
( e, w = (TLamV (e.1), TLamV (e.2))
(τ'i : {f : (bivalC -n> iPropG lang Σ) |
BiVal_to_IProp_Persistent f}),
( j K,
( j K,
j (fill K (e.2))
WP e.1 @
{{v, v', j (fill K (# v'))
......@@ -243,7 +243,7 @@ Section logrel.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
apply forall_ne=> P.
apply always_ne, (contractive_ne _).
apply always_ne.
apply forall_ne => j; apply forall_ne => K.
apply impl_ne; trivial. apply wp_ne => w; apply exist_ne => v'.
rewrite Hfg; trivial.
......
......@@ -109,7 +109,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( w1 w2, w = PairV w1 w2 τ1i w1 τ2i w2)%I
λ w, ( w1 w2, w = PairV w1 w2 τ1i w1 τ2i w2)%I
|}
|}
|}.
......@@ -129,8 +129,8 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, (( w1, w = InjLV w1 τ1i w1)
( w2, w = InjRV w2 τ2i w2))%I
λ w, (( w1, w = InjLV w1 τ1i w1)
( w2, w = InjRV w2 τ2i w2))%I
|}
|}
|}.
......@@ -150,7 +150,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
|}
|}
|}.
......@@ -173,7 +173,7 @@ Section logrel.
( e, w = TLamV e
(τ'i : {f : (valC -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
( WP e @ {{λ v, (τi (`τ'i) v)}}))%I
(WP e @ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
......@@ -184,7 +184,7 @@ Section logrel.
Next Obligation.
intros n f g Hfg x; cbn. apply exist_ne => e; apply and_ne; auto.
apply forall_ne=> P.
apply always_ne, (contractive_ne _), wp_ne => w.
apply always_ne, wp_ne => w.
rewrite Hfg; trivial.
Qed.
......
......@@ -64,12 +64,12 @@ Section typed_interp.
smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_fst; eauto using to_of_val.
iApply wp_fst; try iNext; eauto using to_of_val.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_snd; eauto using to_of_val.
iApply wp_snd; try iNext; eauto using to_of_val.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; value_case.
iLeft; iExists v; auto with itauto.
......
......@@ -13,11 +13,11 @@ Notation "# v" := (of_val v) (at level 20).
Fixpoint interp (τ : type) (w : val) : iProp lang Σ :=
match τ with
| TUnit => w = UnitV
| TProd τ1 τ2 => w1 w2, w = PairV w1 w2 interp τ1 w1 interp τ2 w2
| TProd τ1 τ2 => w1 w2, w = PairV w1 w2 interp τ1 w1 interp τ2 w2
| TSum τ1 τ2 =>
( w1, w = InjLV w1 interp τ1 w1) ( w2, w = InjRV w2 interp τ2 w2)
( w1, w = InjLV w1 interp τ1 w1) ( w2, w = InjRV w2 interp τ2 w2)
| TArrow τ1 τ2 =>
v, interp τ1 v wp (App (of_val w) (of_val v)) (interp τ2)
v, interp τ1 v wp (App (of_val w) (of_val v)) (interp τ2)
end%I.
Global Instance interp_always_stable τ v : PersistentP (interp τ 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