Commit 958678fb authored by Amin Timany's avatar Amin Timany

Simplify iterp for arrow forall in bin_logrel

parent 15005661
......@@ -192,6 +192,37 @@ Definition ctx_refines (Γ : list type)
Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
(ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
Ltac fold_interp :=
match goal with
| |- context [ interp_expr (interp_arrow (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_arrow (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TArrow A A')) B (C, D))
| |- context [ interp_expr (interp_prod (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_prod (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TProd A A')) B (C, D))
| |- context [ interp_expr (interp_prod (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_prod (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TProd A A')) B (C, D))
| |- context [ interp_expr (interp_sum (interp ?A) (interp ?A'))
?B (?C, ?D) ] =>
change (interp_expr (interp_sum (interp A) (interp A')) B (C, D)) with
(interp_expr (interp (TSum A A')) B (C, D))
| |- context [ interp_expr (interp_rec (interp ?A)) ?B (?C, ?D) ] =>
change (interp_expr (interp_rec (interp A)) B (C, D)) with
(interp_expr (interp (TRec A)) B (C, D))
| |- context [ interp_expr (interp_forall (interp ?A))
?B (?C, ?D) ] =>
change (interp_expr (interp_forall (interp A)) B (C, D)) with
(interp_expr (interp (TForall A)) B (C, D))
| |- context [ interp_expr (interp_ref (interp ?A))
?B (?C, ?D) ] =>
change (interp_expr (interp_ref (interp A)) B (C, D)) with
(interp_expr (interp (Tref A)) B (C, D))
end.
Section bin_log_related_under_typed_ctx.
Context `{heapIG Σ, cfgSG Σ}.
......@@ -206,7 +237,7 @@ Section bin_log_related_under_typed_ctx.
- inversion_clear 1; trivial.
- inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3 Δ HΔ.
specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3).
inversion Hx1; subst; simpl.
inversion Hx1; subst; simpl; try fold_interp.
+ eapply bin_log_related_rec; eauto;
match goal with
H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H)
......
......@@ -297,7 +297,7 @@ Section CG_Counter.
iFrame "Hj".
iExists (_, _), (_, _); simpl; repeat iSplit; trivial.
- (* refinement of increment *)
iAlways. clear j K. iIntros {j K v} "[#Heq Hj]".
iAlways. clear j K. iIntros {v} "#Heq". iIntros {j K} "Hj".
rewrite CG_locked_increment_of_val /=.
destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=.
iLöb as "Hlat".
......@@ -340,7 +340,7 @@ Section CG_Counter.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of read *)
iAlways. clear j K. iIntros {j K v} "[#Heq Hj]".
iAlways. clear j K. iIntros {v} "#Heq". iIntros {j K} "Hj".
rewrite ?counter_read_of_val.
iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=.
Transparent counter_read.
......
......@@ -25,7 +25,7 @@ Section Stack_refinement.
rewrite ?empty_env_subst /CG_stack /FG_stack.
iApply wp_value; eauto.
iExists (TLamV _); iFrame "Hj".
clear j K. iAlways. iIntros {τi j K} "% Hj /=".
clear j K. iAlways. iIntros {τi} "%". iIntros {j K} "Hj /=".
iPvs (step_tlam _ _ j K with "[Hj]") as "Hj"; eauto.
iApply wp_tlam; iNext.
iPvs (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) _ with "[Hj]")
......@@ -92,7 +92,7 @@ Section Stack_refinement.
(* refinement of push and pop *)
- iExists (_, _), (_, _); iSplit; eauto. iSplit.
+ (* refinement of push *)
iAlways. clear j K. iIntros {j K [v1 v2] } "[#Hrel Hj] /=".
iAlways. clear j K. iIntros { [v1 v2] } "#Hrel". iIntros {j K} "Hj /=".
rewrite -(FG_push_folding (Loc stk)).
iLöb as "Hlat".
rewrite {2}(FG_push_folding (Loc stk)).
......@@ -145,7 +145,8 @@ Section Stack_refinement.
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
+ (* refinement of pop *)
iAlways. clear j K. iIntros {j K [v1 v2] } "[[% %] Hj] /="; simplify_eq/=.
iAlways. clear j K. iIntros { [v1 v2] } "[% %]".
iIntros {j K} "Hj /="; simplify_eq/=.
rewrite -(FG_pop_folding (Loc stk)).
iLöb as "Hlat".
rewrite {2}(FG_pop_folding (Loc stk)).
......@@ -266,7 +267,7 @@ Section Stack_refinement.
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of iter *)
iAlways. clear j K. iIntros {j K [f1 f2] } "/= [#Hfs Hj]".
iAlways. clear j K. iIntros { [f1 f2] } "/= #Hfs". iIntros {j K} "Hj".
iApply wp_rec; auto using to_of_val. iNext.
iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
{ by iFrame "Hspec Hj". }
......@@ -335,9 +336,10 @@ Section Stack_refinement.
iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
rewrite StackLink_unfold.
iDestruct "HLK''" as {istk6 w'} "[% HLK]"; simplify_eq/=.
iSpecialize ("Hfs" $! _ (K ++ [AppRCtx (RecV _)]) (yn1, zn1)).
iSpecialize ("Hfs" $! (yn1, zn1) with "Hrel").
iSpecialize ("Hfs" $! _ (K ++ [AppRCtx (RecV _)])).
rewrite fill_app; simpl.
iApply wp_wand_l; iSplitR "Hj"; [|iApply "Hfs"; by iFrame "Hrel Hj"].
iApply wp_wand_l; iSplitR "Hj"; [|iApply "Hfs"; by iFrame "Hj"].
iIntros {u} "/="; iDestruct 1 as {z} "[Hj [% %]]".
rewrite fill_app; simpl. subst. asimpl.
iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
......
......@@ -202,7 +202,7 @@ Section fundamental.
Proof.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
value_case. iExists (RecV _). iIntros "{$Hj} !".
iLöb as "IH". iIntros {j' K' [v v'] } "[#Hiv Hv]".
iLöb as "IH". iIntros { [v v'] } "#Hiv". iIntros {j' K'} "Hj".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_rec; auto 1 using to_of_val. iNext.
iPvs (step_rec _ _ j' K' _ (# v') v' with "* [-]") as "Hz"; eauto.
......@@ -221,8 +221,8 @@ Section fundamental.
smart_wp_bind (AppLCtx (e2.[env_subst (vvs.*1)])) v v' "[Hv #Hiv]"
('IHHtyped1 _ _ _ j (K ++ [(AppLCtx (e2'.[env_subst (vvs.*2)]))])); cbn.
smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]"
('IHHtyped2 _ _ _ j (K ++ [AppRCtx v'])); cbn.
iApply ("Hiv" $! j K (w, w')); simpl; eauto.
('IHHtyped2 _ _ _ j (K ++ [AppRCtx v'])); cbn.
iApply ("Hiv" $! (w, w') with "Hiw *"); simpl; eauto.
Qed.
Lemma bin_log_related_tlam Γ e e' τ
......@@ -231,7 +231,7 @@ Section fundamental.
Proof.
iIntros {Δ vvs ρ ?} "#(Hh & Hs & HΓ)"; iIntros {j K} "Hj /=".
value_case. iExists (TLamV _).
iIntros "{$Hj} /= !"; iIntros {τi j' K'} "% Hv /=".
iIntros "{$Hj} /= !"; iIntros {τi} "%". iIntros {j' K'} "Hv /=".
iApply wp_tlam; iNext.
iPvs (step_tlam _ _ j' K' (e'.[env_subst (vvs.*2)]) with "* [-]") as "Hz"; eauto.
iApply 'IHHtyped; repeat iSplit; eauto. by iApply interp_env_ren.
......@@ -245,7 +245,8 @@ Section fundamental.
smart_wp_bind (TAppCtx) v v' "[Hj #Hv]"
('IHHtyped _ _ _ j (K ++ [TAppCtx])); cbn.
iApply wp_wand_r; iSplitL.
{ iApply ("Hv" $! (interp τ' Δ) with "[#] Hj"); iPureIntro; apply _. }
{ iSpecialize ("Hv" $! (interp τ' Δ) with "[#]"); [iPureIntro; apply _|].
iApply "Hv"; eauto. }
iIntros {w} "Hw". iDestruct "Hw" as {w'} "[Hw #Hiw]".
iExists _; rewrite -interp_subst; eauto.
Qed.
......
......@@ -27,6 +27,11 @@ Section logrel.
Implicit Types Δ : listC D.
Implicit Types interp : listC D D.
Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
(ee : expr * expr) : iPropG lang Σ := ( j K,
j fill K (ee.2)
WP ee.1 {{ v, v', j fill K (# v') τi Δ (v, v') }})%I.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper_alt.
......@@ -54,19 +59,30 @@ Section logrel.
Solve Obligations with solve_proper.
Program Definition interp_arrow
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
( j K vv,
interp1 Δ vv j fill K (App (# ww.2) (# vv.2))
WP App (# ww.1) (# vv.1) {{ v, v', j fill K (# v') interp2 Δ (v, v') }})%I.
(interp1 interp2 : listC D -n> D) : listC D -n> D :=
λne Δ ww,
( vv, interp1 Δ vv
interp_expr
interp2 Δ (App (# ww.1) (# vv.1), App (# ww.2) (# vv.2)))%I.
Solve Obligations with solve_proper.
Next Obligation.
Proof.
intros d d' n x x' Hx z. eapply always_ne.
apply forall_ne => z'. apply impl_ne. by rewrite Hx. solve_proper.
Qed.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ ww,
( τi j K,
( ww, PersistentP (τi ww))
j fill K (TApp (# ww.2))
WP TApp (# ww.1) {{ v, v', j fill K (# v') interp (τi :: Δ) (v, v')}})%I.
( τi,
( ww, PersistentP (τi ww))
interp_expr
interp (τi :: Δ) (TApp (# ww.1), TApp (# ww.2)))%I.
Solve Obligations with solve_proper.
Next Obligation.
Proof.
intros d n x x' Hx z. eapply always_ne.
apply forall_ne => z'. apply impl_ne; trivial. solve_proper.
Qed.
Program Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
......@@ -117,11 +133,6 @@ Section logrel.
(length Γ = length vvs [] zip_with (λ τ, τ Δ) Γ vvs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D)
(ee : expr * expr) : iPropG lang Σ := ( j K,
j fill K (ee.2)
WP ee.1 {{ v, v', j fill K (# v') τ Δ (v, v') }})%I.
Class env_PersistentP Δ :=
ctx_persistentP : Forall (λ τi, vv, PersistentP (τi vv)) Δ.
Global Instance ctx_persistent_nil : env_PersistentP [].
......@@ -152,14 +163,16 @@ Section logrel.
- intros ww; simpl; properness; auto.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- unfold interp_expr.
intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi ww /=.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
change (uPredC (iResUR lang _)) with (iPropG lang Σ).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
- intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
- unfold interp_expr.
intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply IHτ.
Qed.
......@@ -173,7 +186,8 @@ Section logrel.
- intros ww; simpl; properness; auto.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- unfold interp_expr.
intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi ww /=.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
......@@ -184,7 +198,8 @@ Section logrel.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
change (uPredC (iResUR lang _)) with (iPropG lang Σ).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
- intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
- unfold interp_expr.
intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros ww; simpl; properness; auto. by apply IHτ.
Qed.
......@@ -242,5 +257,5 @@ End logrel.
Typeclasses Opaque interp_env.
Notation "⟦ τ ⟧" := (interp τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr (interp τ)).
Notation "⟦ Γ ⟧*" := (interp_env Γ).
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