Commit b6db9444 authored by Amin Timany's avatar Amin Timany

Generalize lemmas for binary logrel of Fμ,ref,par

parent 13c550dc
......@@ -17,38 +17,6 @@ Section typed_interp.
Implicit Types P Q R : iPropG lang Σ.
Notation "# v" := (of_val v) (at level 20).
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_ : ?A, _) => let W := fresh "W" in evar (W : A); iExists W; unfold W; clear W
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => iNext
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => eapply (@always_intro _ _ _ _)
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
......@@ -92,32 +60,31 @@ Section typed_interp.
Notation "✓✓" := context_interp_Persistent.
Lemma typed_binary_interp_Pair Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ (HΔ : ✓✓ Δ), Δ Γ e1 log e1' τ1)
(IHHtyped2 : Δ (HΔ : ✓✓ Δ), Δ Γ e2 log e2' τ2)
(IHHtyped1 : Δ Γ e1 log e1' τ1)
(IHHtyped2 : Δ Γ e2 log e2' τ2)
:
Δ Γ Pair e1 e2 log Pair e1' e2' TProd τ1 τ2.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (PairLCtx e2.[env_subst (map fst vs)]) v v' "[Hv #Hiv]"
(IHHtyped1 _ _ _ _ _ j
(IHHtyped1 _ _ _ j
(K ++ [PairLCtx e2'.[env_subst (map snd vs)] ])).
smart_wp_bind (PairRCtx v) w w' "[Hw #Hiw]"
(IHHtyped2 _ _ _ _ _ j
(K ++ [(PairRCtx v')])).
(IHHtyped2 _ _ _ j (K ++ [(PairRCtx v')])).
value_case. iExists (PairV v' w'); iFrame "Hw".
iExists (v, w), (v', w'); simpl; eauto 10 with itauto.
iExists (v, w), (v', w'); simpl; repeat iSplit; trivial.
(* unshelving *)
Unshelve. all: trivial.
Qed.
Lemma typed_binary_interp_Fst Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' (TProd τ1 τ2))
(IHHtyped : Δ Γ e log e' (TProd τ1 τ2))
:
Δ Γ Fst e log Fst e' τ1.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [FstCtx])); cbn.
(IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
inversion H; subst.
iPvs (step_fst _ _ _ j K (# (w2.1)) (w2.1) (# (w2.2)) (w2.2)
......@@ -130,13 +97,13 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Snd Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' (TProd τ1 τ2))
(IHHtyped : Δ Γ e log e' (TProd τ1 τ2))
:
Δ Γ Snd e log Snd e' τ2.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [SndCtx])); cbn.
(IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
inversion H; subst.
iPvs (step_snd _ _ _ j K (# (w2.1)) (w2.1) (# (w2.2)) (w2.2)
......@@ -149,13 +116,13 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_InjL Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' τ1)
(IHHtyped : Δ Γ e log e' τ1)
:
Δ Γ InjL e log InjL e' (TSum τ1 τ2).
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [InjLCtx])); cbn.
(IHHtyped _ _ _ j (K ++ [InjLCtx])); cbn.
value_case. iExists (InjLV v'); iFrame "Hv".
iLeft; iExists _; iSplit; [|eauto]; simpl; trivial.
(* unshelving *)
......@@ -163,13 +130,13 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_InjR Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' τ2)
(IHHtyped : Δ Γ e log e' τ2)
:
Δ Γ InjR e log InjR e' (TSum τ1 τ2).
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [InjRCtx])); cbn.
(IHHtyped _ _ _ j (K ++ [InjRCtx])); cbn.
value_case. iExists (InjRV v'); iFrame "Hv".
iRight; iExists _; iSplit; [|eauto]; simpl; trivial.
(* unshelving *)
......@@ -181,15 +148,15 @@ Section typed_interp.
(Htyped3 : typed (τ2 :: Γ) e2 τ3)
(Htyped2' : typed (τ1 :: Γ) e1' τ3)
(Htyped3' : typed (τ2 :: Γ) e2' τ3)
(IHHtyped1 : Δ (HΔ : ✓✓ Δ), Δ Γ e0 log e0' TSum τ1 τ2)
(IHHtyped2 : Δ (HΔ : ✓✓ Δ), Δ τ1 :: Γ e1 log e1' τ3)
(IHHtyped3 : Δ (HΔ : ✓✓ Δ), Δ τ2 :: Γ e2 log e2' τ3)
(IHHtyped1 : Δ Γ e0 log e0' TSum τ1 τ2)
(IHHtyped2 : Δ τ1 :: Γ e1 log e1' τ3)
(IHHtyped3 : Δ τ2 :: Γ e2 log e2' τ3)
:
Δ Γ Case e0 e1 e2 log Case e0' e1' e2' τ3.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]"
(IHHtyped1 _ _ _ _ _ j (K ++ [CaseCtx _ _])); cbn.
(IHHtyped1 _ _ _ j (K ++ [CaseCtx _ _])); cbn.
iDestruct "Hiv" as "[Hiv|Hiv]".
+ iDestruct "Hiv" as {w} "[% Hw]".
inversion H; subst.
......@@ -198,7 +165,7 @@ Section typed_interp.
iFrame "Hspec Hv"; trivial.
iApply wp_case_inl; auto 1 using to_of_val.
asimpl.
specialize (IHHtyped2 Δ HΔ (w::vs)); simpl in IHHtyped2.
specialize (IHHtyped2 (w::vs)); simpl in IHHtyped2.
erewrite <- ?typed_subst_head_simpl in IHHtyped2; eauto;
simpl; try rewrite map_length; eauto with f_equal. iNext.
iApply IHHtyped2; auto 2.
......@@ -210,7 +177,7 @@ Section typed_interp.
iFrame "Hspec Hv"; trivial.
iApply wp_case_inr; auto 1 using to_of_val.
asimpl.
specialize (IHHtyped3 Δ HΔ (w::vs)); simpl in IHHtyped3.
specialize (IHHtyped3 (w::vs)); simpl in IHHtyped3.
erewrite <- ?typed_subst_head_simpl in IHHtyped3; eauto;
simpl; try rewrite map_length; eauto with f_equal. iNext.
iApply IHHtyped3; auto 2.
......@@ -223,7 +190,7 @@ Section typed_interp.
Lemma typed_binary_interp_Lam Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(Htyped : typed (τ1 :: Γ) e τ2)
(Htyped' : typed (τ1 :: Γ) e' τ2)
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ τ1 :: Γ e log e' τ2)
(IHHtyped : Δ τ1 :: Γ e log e' τ2)
:
Δ Γ Lam e log Lam e' TArrow τ1 τ2.
Proof.
......@@ -235,7 +202,7 @@ Section typed_interp.
iFrame "Hspec Hv"; trivial.
asimpl. erewrite ?typed_subst_head_simpl; eauto;
simpl; try rewrite map_length; eauto with f_equal.
specialize (IHHtyped Δ HΔ (v::vs)); simpl in IHHtyped.
specialize (IHHtyped (v::vs)); simpl in IHHtyped.
iApply IHHtyped; auto.
iFrame "Hheap Hspec Hiv HΓ"; trivial.
(* unshelving *)
......@@ -243,20 +210,17 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_App Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ (HΔ : ✓✓ Δ), Δ Γ e1 log e1' TArrow τ1 τ2)
(IHHtyped2 : Δ (HΔ : ✓✓ Δ), Δ Γ e2 log e2' τ1)
(IHHtyped1 : Δ Γ e1 log e1' TArrow τ1 τ2)
(IHHtyped2 : Δ Γ e2 log e2' τ1)
:
Δ Γ App e1 e2 log App e1' e2' τ2.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (AppLCtx (e2.[env_subst (map fst vs)])) v v' "[Hv #Hiv]"
(IHHtyped1
_ _ _ _ _ j
(IHHtyped1 _ _ _ j
(K ++ [(AppLCtx (e2'.[env_subst (map snd vs)]))])); cbn.
smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]"
(IHHtyped2
_ _ _ _ _ j
(K ++ [AppRCtx v'])); cbn.
(IHHtyped2 _ _ _ j (K ++ [AppRCtx v'])); cbn.
iApply ("Hiv" $! j K (w, w')); simpl.
iNext; iFrame "Hw"; trivial.
(* unshelving *)
......@@ -264,8 +228,9 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_TLam Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ),
Δ map (λ t : type, t.[ren (+1)]) Γ e log e' τ)
(IHHtyped : τi (Hpr: BiVal_to_IProp_Persistent τi),
(extend_context_interp_fun1 τi Δ) map (λ t : type, t.[ren (+1)]) Γ
e log e' τ)
:
Δ Γ TLam e log TLam e' TForall τ.
Proof.
......@@ -281,13 +246,13 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_TApp Δ Γ e e' τ τ' {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' TForall τ)
(IHHtyped : Δ Γ e log e' TForall τ)
:
Δ Γ TApp e log TApp e' τ.[τ'/].
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (TAppCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [TAppCtx])); cbn.
(IHHtyped _ _ _ j (K ++ [TAppCtx])); cbn.
iDestruct "Hiv" as {e''} "[% He'']".
inversion H; subst.
iSpecialize ("He''" $! ((interp τ' Δ) _)); cbn.
......@@ -305,36 +270,37 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Fold Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ),
Δ map (λ t : type, t.[ren (+1)]) Γ e log e' τ)
(IHHtyped :
(extend_context_interp ((@interp Σ iS iI (N .@ 1) (TRec τ)) Δ) Δ)
map (λ t : type, t.[ren (+1)]) Γ
e log e' τ)
:
Δ Γ Fold e log Fold e' TRec τ.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
iApply (@wp_bind _ _ _ [FoldCtx]);
iApply wp_wand_l; iSplitR;
[|iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ)
_ _ _ _ j (K ++ [FoldCtx]));
[|iApply (IHHtyped _ _ _ j (K ++ [FoldCtx]));
rewrite fill_app; simpl; repeat iSplitR; trivial].
+ iIntros {v} "Hv"; iDestruct "Hv" as {w} "[Hv #Hiv]";
rewrite fill_app.
value_case. iExists (FoldV w); iFrame "Hv".
rewrite fixpoint_unfold; cbn.
iAlways. iExists (_, _); iSplit; auto with itauto.
iAlways. iExists (_, _); iSplit; try iNext; trivial.
+ rewrite zip_with_context_interp_subst; trivial.
(* unshelving *)
Unshelve. all: rewrite map_length; trivial.
Qed.
Lemma typed_binary_interp_Unfold Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' TRec τ)
(IHHtyped : Δ Γ e log e' TRec τ)
:
Δ Γ Unfold e log Unfold e' τ.[(TRec τ)/].
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_wand_l; iSplitR;
[|iApply (IHHtyped _ _ _ _ _ j (K ++ [UnfoldCtx]));
[|iApply (IHHtyped _ _ _ j (K ++ [UnfoldCtx]));
rewrite fill_app; simpl; repeat iSplitR; trivial].
iIntros {v} "Hv". iDestruct "Hv" as {w} "[Hw #Hiw]"; rewrite fill_app.
simpl. rewrite fixpoint_unfold; simpl.
......@@ -350,9 +316,8 @@ Section typed_interp.
Unshelve. all: eauto using to_of_val.
Qed.
Lemma typed_binary_interp_Fork Δ Γ e e' {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' TUnit)
(IHHtyped : Δ Γ e log e' TUnit)
:
Δ Γ Fork e log Fork e' TUnit.
Proof.
......@@ -364,7 +329,7 @@ Section typed_interp.
iSplitL "Hz1".
+ iNext. iExists UnitV; iFrame "Hz1"; iSplit; trivial.
+ iNext. iApply wp_wand_l; iSplitR;
[|iApply (IHHtyped _ _ _ _ _ _ [])]; trivial.
[|iApply (IHHtyped _ _ _ _ [])]; trivial.
* iIntros {w} "Hw"; trivial.
* iFrame "Hheap Hspec HΓ"; trivial.
(* unshelving *)
......@@ -372,14 +337,13 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Alloc Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' τ)
(IHHtyped : Δ Γ e log e' τ)
:
Δ Γ Alloc e log Alloc e' (Tref τ).
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]"
(IHHtyped
_ _ _ _ _ j (K ++ [AllocCtx])).
(IHHtyped _ _ _ j (K ++ [AllocCtx])).
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
iPvsIntro.
iPvs (step_alloc _ _ _ j K (# v') v' _ _ with "* -") as "Hz".
......@@ -415,14 +379,13 @@ Section typed_interp.
intros S1 S2 Hsdj; set_solver_ndisj.
Lemma typed_binary_interp_Load Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ (HΔ : ✓✓ Δ), Δ Γ e log e' (Tref τ))
(IHHtyped : Δ Γ e log e' (Tref τ))
:
Δ Γ Load e log Load e' τ.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]"
(IHHtyped
_ _ _ _ _ j (K ++ [LoadCtx])).
(IHHtyped _ _ _ j (K ++ [LoadCtx])).
iDestruct "Hiv" as {l} "[% Hinv]".
inversion H; subst.
iApply wp_atomic; cbn; trivial.
......@@ -444,18 +407,16 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Store Δ Γ e1 e2 e1' e2' τ {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ (HΔ : ✓✓ Δ), Δ Γ e1 log e1' (Tref τ))
(IHHtyped2 : Δ (HΔ : ✓✓ Δ), Δ Γ e2 log e2' τ)
(IHHtyped1 : Δ Γ e1 log e1' (Tref τ))
(IHHtyped2 : Δ Γ e2 log e2' τ)
:
Δ Γ Store e1 e2 log Store e1' e2' TUnit.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]"
(IHHtyped1
_ _ _ _ _ j (K ++ [StoreLCtx _])).
(IHHtyped1 _ _ _ j (K ++ [StoreLCtx _])).
smart_wp_bind (StoreRCtx _) w w' "[Hw #Hiw]"
(IHHtyped2
_ _ _ _ _ j (K ++ [StoreRCtx _])).
(IHHtyped2 _ _ _ j (K ++ [StoreRCtx _])).
iDestruct "Hiv" as {l} "[% Hinv]".
inversion H; subst.
iApply wp_atomic; trivial;
......@@ -480,22 +441,19 @@ Section typed_interp.
Lemma typed_binary_interp_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ {HΔ : ✓✓ Δ}
(HEqτ : EqType τ)
(IHHtyped1 : Δ (HΔ : ✓✓ Δ), Δ Γ e1 log e1' Tref τ)
(IHHtyped2 : Δ (HΔ : ✓✓ Δ), Δ Γ e2 log e2' τ)
(IHHtyped3 : Δ (HΔ : ✓✓ Δ), Δ Γ e3 log e3' τ)
(IHHtyped1 : Δ Γ e1 log e1' Tref τ)
(IHHtyped2 : Δ Γ e2 log e2' τ)
(IHHtyped3 : Δ Γ e3 log e3' τ)
:
Δ Γ CAS e1 e2 e3 log CAS e1' e2' e3' TBOOL.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]"
(IHHtyped1
_ _ _ _ _ j (K ++ [CasLCtx _ _])).
(IHHtyped1 _ _ _ j (K ++ [CasLCtx _ _])).
smart_wp_bind (CasMCtx _ _) w w' "[Hw #Hiw]"
(IHHtyped2
_ _ _ _ _ j (K ++ [CasMCtx _ _])).
(IHHtyped2 _ _ _ j (K ++ [CasMCtx _ _])).
smart_wp_bind (CasRCtx _ _) u u' "[Hu #Hiu]"
(IHHtyped3
_ _ _ _ _ j (K ++ [CasRCtx _ _])).
(IHHtyped3 _ _ _ j (K ++ [CasRCtx _ _])).
iDestruct "Hiv" as {l} "[% Hinv]".
inversion H; subst.
iApply wp_atomic; trivial;
......@@ -519,7 +477,7 @@ Section typed_interp.
iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iPvsIntro. iExists TRUEV; iFrame "Hw".
iLeft; iExists (UnitV, UnitV); auto with itauto.
iLeft; iExists (UnitV, UnitV); repeat iSplit; trivial.
+ iPvs (step_cas_fail _ _ _ j K (l.2) 1 (z2) (# w') w' (# u') u' _ _ _
with "[Hu Hw2]") as "[Hw Hw2]"; simpl.
{ iFrame "Hspec Hu Hw2". iNext.
......@@ -533,12 +491,11 @@ Section typed_interp.
iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iPvsIntro. iExists FALSEV; iFrame "Hw".
iRight; iExists (UnitV, UnitV); auto with itauto.
iRight; iExists (UnitV, UnitV); repeat iSplit; trivial.
(* unshelving *)
Unshelve. all: eauto using to_of_val. all: SolveDisj 3 l.
Qed.
Lemma typed_binary_interp Δ Γ e τ {HΔ : context_interp_Persistent Δ}
(Htyped : typed Γ e τ)
: Δ Γ e log e τ.
......
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