Skip to content

GitLab

R
ReLoC-v1
Commit 39148535 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Simplify Persistent stuff.

parent 01db92e2
Hide whitespace changes
Inline Side-by-side
Showing with 115 additions and 262 deletions
F_mu/fundamental.v
View file @ 39148535
......@@ -16,12 +16,11 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp Δ Γ vs e τ
Lemma typed_interp (Δ : varC -n> valC -n> iProp lang Σ) Γ vs e τ
(Htyped : typed Γ e τ)
(HΔ : context_interp_Persistent Δ)
(HΔ : ∀ x v, PersistentP (Δ x v))
: List.length Γ = List.length vs →
[∧] zip_with (λ τ v, interp τ Δ v) Γ vs ⊢
WP e.[env_subst vs] {{ λ v, (@interp Σ) τ Δ v }}.
[∧] zip_with (λ τ, interp τ Δ) Γ vs ⊢ WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#HΓ"; cbn.
......@@ -74,8 +73,8 @@ Section typed_interp.
- (* TLam *)
value_case.
iIntros { [τi τiPr] } "!". iApply wp_TLam; iNext; simpl in *.
iApply IHHtyped; [rewrite map_length|]; trivial.
rewrite zip_with_context_interp_subst; trivial.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
by iDestruct (zip_with_context_interp_subst with "HΓ") as "?".
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
unshelve iSpecialize ("Hv" $! ((interp τ' Δ) ↾ _)); try apply _; cbn.
......@@ -92,7 +91,7 @@ Section typed_interp.
change (fixpoint _) with (interp (TRec τ) Δ) at 1; trivial.
rewrite fixpoint_unfold; cbn.
iAlways; eauto.
+ iRevert "HΓ"; rewrite zip_with_context_interp_subst; iIntros "#HΓ"; trivial.
+ by iDestruct (zip_with_context_interp_subst with "HΓ") as "?".
- (* Unfold *)
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply IHHtyped; trivial].
......
F_mu/logrel.v
View file @ 39148535
......@@ -10,11 +10,6 @@ Section logrel.
Context {Σ : iFunctor}.
Notation "# v" := (of_val v) (at level 20).
Class Val_to_IProp_Persistent (f : valC -n> iProp lang Σ) :=
val_to_iprop_persistent : ∀ v : val, PersistentP (f v).
Arguments Val_to_IProp_Persistent /.
(** Just to get nicer closed forms, we define extend_context_interp in three steps. *)
Program Definition extend_context_interp_fun1
(τi : valC -n> iProp lang Σ)
......@@ -153,8 +148,7 @@ Section logrel.
{|
cofe_mor_car :=
λ w,
(∀ (τ'i : {f : (valC -n> iProp lang Σ) |
Val_to_IProp_Persistent f}),
(∀ (τ'i : {f : (valC -n> iProp lang Σ) | ∀ v, PersistentP (f v)}%type),
□ WP TApp (# w) {{λ v, (τi (`τ'i) v)}})%I
|}
|}.
......@@ -240,41 +234,23 @@ Section logrel.
Solve Obligations with
repeat intros ?; match goal with [H : _ ≡{_}≡ _|- _] => rewrite H end; trivial.
Class context_interp_Persistent (Δ : varC -n> valC -n> iProp lang Σ) :=
contextinterppersistent : ∀ v : var, Val_to_IProp_Persistent (Δ v).
Global Instance Val_to_IProp_Persistent_Persistent
(f : valC -n> iProp lang Σ)
{Hf : Val_to_IProp_Persistent f}
(v : val)
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_Persistent
τ (Δ : varC -n> valC -n> iProp lang Σ)
{HΔ : context_interp_Persistent Δ}
: Val_to_IProp_Persistent (interp τ Δ).
{HΔ : ∀ x v, PersistentP (Δ x v)}
: ∀ v, PersistentP (interp τ Δ v).
Proof.
revert Δ HΔ.
induction τ; cbn; intros Δ HΔ v; try apply _.
- rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
apply always_intro'; trivial.
- apply Val_to_IProp_Persistent_Persistent; apply HΔ.
rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
apply always_intro'; trivial.
Qed.
Global Instance Persistent_context_interp_rel Δ Γ vs
{HΔ : context_interp_Persistent Δ}
: PersistentP ([∧] zip_with(λ τ v, interp τ Δ v) Γ vs)%I.
Proof. typeclasses eauto. Qed.
Global Program Instance extend_context_interp_Persistent f Δ
(Hf : Val_to_IProp_Persistent f)
{HΔ : context_interp_Persistent Δ}
: context_interp_Persistent (@extend_context_interp f Δ).
Next Obligation.
intros f Δ Hf HΔ v w; destruct v; cbn; trivial.
apply HΔ.
Qed.
Global Instance extend_context_interp_Persistent
(f : valC -n> iProp lang Σ) (Δ : varC -n> valC -n> iProp lang Σ)
(Hf : ∀ v, PersistentP (f v))
{HΔ : ∀ x v, PersistentP (Δ x v)}
: ∀ x v, PersistentP (@extend_context_interp f Δ x v).
Proof. intros x v. destruct x; cbn; trivial. Qed.
Local Ltac properness :=
repeat
......@@ -542,8 +518,8 @@ Section logrel.
Lemma zip_with_context_interp_subst
(Δ : varC -n> valC -n> iProp lang Σ) (Γ : list type)
(vs : list valC) (τi : valC -n> iProp lang Σ) :
(([∧] zip_with (λ τ v, interp τ Δ v) Γ vs)%I)
≡ ([∧] zip_with (λ τ v, interp τ (extend_context_interp τi Δ) v)
(([∧] zip_with (λ τ, interp τ Δ) Γ vs)%I)
≡ ([∧] zip_with (λ τ, interp τ (extend_context_interp τi Δ))
(map (λ t : type, t.[ren (+1)]) Γ) vs)%I.
Proof.
revert Δ vs τi.
......
F_mu/soundness.v
View file @ 39148535
......@@ -23,21 +23,15 @@ Section Soundness.
λ x,
{|
cofe_mor_car :=
λ y, (True)%I
λ y, True%I
|}
|}.
Global Instance free_context_interp_Persistent :
context_interp_Persistent free_type_context.
Proof. intros x v; apply const_persistent. Qed.
Lemma wp_soundness e τ
: typed [] e τ → True ⊢ WP e {{@interp (globalF Σ) τ free_type_context}}.
: typed [] e τ → True ⊢ WP e {{ @interp (globalF Σ) τ free_type_context}}.
Proof.
iIntros {H} "".
rewrite -(empty_env_subst e).
iPoseProof (@typed_interp _ _ _ []) as "Hi"; eauto; try typeclasses eauto.
iApply "Hi"; eauto.
iIntros {H} "". rewrite -(empty_env_subst e).
by iApply (@typed_interp _ _ _ []).
Qed.
Theorem Soundness e τ :
......@@ -47,12 +41,11 @@ Section Soundness.
Proof.
intros H1 e' thp Hstp Hnr.
eapply wp_soundness in H1; eauto.
edestruct(@wp_adequacy_reducible lang (globalF Σ) ⊤
edestruct (@wp_adequacy_reducible lang (globalF Σ) ⊤
(interp τ free_type_context)
e e' (e' :: thp) tt ∅) as [Ha|Ha];
eauto using ucmra_unit_valid; try tauto.
- iIntros "H". iApply H1.
- constructor.
Qed.
End Soundness.
\ No newline at end of file
F_mu_ref/fundamental.v
View file @ 39148535
......@@ -22,13 +22,13 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N Δ Γ vs e τ
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : ∀ l : loc, N ⊥ L .@ l)
(Htyped : typed Γ e τ)
(HΔ : context_interp_Persistent Δ)
(HΔ : ∀ x v, PersistentP (Δ x v))
: List.length Γ = List.length vs →
heap_ctx N ∧ [∧] zip_with (λ τ v, (@interp Σ i L) τ Δ v) Γ vs ⊢
WP e.[env_subst vs] {{ λ v, (@interp Σ i L) τ Δ v }}.
heap_ctx N ∧ [∧] zip_with (λ τ, interp L τ Δ) Γ vs ⊢
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
......@@ -80,10 +80,9 @@ Section typed_interp.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case. iIntros { [τi τiPr] } "!".
iApply wp_TLam; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
rewrite zip_with_context_interp_subst; trivial.
iApply wp_TLam; iNext. simpl.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
rewrite -zip_with_context_interp_subst. auto.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
unshelve iSpecialize ("Hv" $! ((interp L τ' Δ) ↾ _)); try apply _; cbn.
......
F_mu_ref/logrel.v
View file @ 39148535
......@@ -14,11 +14,6 @@ Section logrel.
Context {Σ : gFunctors}.
Notation "# v" := (of_val v) (at level 20).
Class Val_to_IProp_Persistent (f : valC -n> iPropG lang Σ) :=
val_to_iprop_persistent : ∀ v : val, PersistentP (f v).
Arguments Val_to_IProp_Persistent /.
(** Just to get nicer closed forms, we define extend_context_interp in three steps. *)
Program Definition extend_context_interp_fun1
(τi : valC -n> iPropG lang Σ)
......@@ -156,13 +151,11 @@ Section logrel.
{|
cofe_mor_car :=
λ w,
(∀ (τ'i : {f : (valC -n> iPropG lang Σ) |
Val_to_IProp_Persistent f}),
(∀ (τ'i : {f : (valC -n> iPropG lang Σ) | ∀ v, PersistentP (f v)}%type),
□ (WP TApp (# w) @ ⊤ {{λ v, (τi (`τ'i) v)}}))%I
|}
|}.
Next Obligation.
Proof.
intros τ τ' x y Hxy; cbn; rewrite Hxy; trivial.
Qed.
Next Obligation.
......@@ -187,16 +180,13 @@ Section logrel.
|}
|}.
Next Obligation.
Proof.
intros τi rec_appr n x y Hxy; rewrite Hxy; trivial.
Qed.
Next Obligation.
Proof.
intros τi n f g Hfg x. cbn.
apply always_ne, exist_ne =>w; rewrite Hfg; trivial.
Qed.
Next Obligation.
Proof.
intros n τi τi' Hτi f x. cbn.
apply always_ne, exist_ne =>w; rewrite Hτi; trivial.
Qed.
......@@ -220,7 +210,7 @@ Section logrel.
cofe_mor_car := λ τi, fixpoint (interp_rec_pre τi)
|}.
Next Obligation.
Proof. intros n f g H; apply fixpoint_ne => z; rewrite H; trivial. Qed.
intros n f g H; apply fixpoint_ne => z; rewrite H; trivial. Qed.
Context `{i : heapG Σ} (L : namespace).
......@@ -229,8 +219,7 @@ Section logrel.
{|
cofe_mor_car := λ τi, (∃ v, l ↦ v ★ (τi v))%I
|}.
Next Obligation.
Proof. intros ???? H; apply exist_ne =>w; rewrite H; trivial. Qed.
Next Obligation. intros ???? H; apply exist_ne =>w; rewrite H; trivial. Qed.
Program Definition interp_ref :
(valC -n> iPropG lang Σ) -n> valC -n> iPropG lang Σ :=
......@@ -241,10 +230,8 @@ Section logrel.
λ w, (∃ l, w = LocV l ∧ inv (L .@ l) (interp_ref_pred l τi))%I
|}
|}.
Next Obligation. intros ???? H; rewrite H; trivial. Qed.
Next Obligation.
Proof. intros ???? H; rewrite H; trivial. Qed.
Next Obligation.
Proof.
intros ??? H ?; apply exist_ne=>w; apply and_ne; trivial; cbn.
apply (contractive_ne _); apply exist_ne=>w'; rewrite H; trivial.
Qed.
......@@ -273,41 +260,23 @@ Section logrel.
Solve Obligations
with repeat intros ?; match goal with [H : _ ≡{_}≡ _|- _] => rewrite H end; trivial.
Class context_interp_Persistent (Δ : varC -n> valC -n> iPropG lang Σ) :=
contextinterppersistent : ∀ v : var, Val_to_IProp_Persistent (Δ v).
Global Instance Val_to_IProp_Persistent_Persistent
(f : valC -n> iPropG lang Σ)
{Hf : Val_to_IProp_Persistent f}
(v : val)
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_Persistent
τ (Δ : varC -n> valC -n> iPropG lang Σ)
{HΔ : context_interp_Persistent Δ}
: Val_to_IProp_Persistent (interp τ Δ).
{HΔ : ∀ x v, PersistentP (Δ x v)}
: ∀ v, PersistentP (interp τ Δ v).
Proof.
revert Δ HΔ.
induction τ; cbn; intros Δ HΔ v; try apply _.
- rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
apply always_intro'; trivial.
- apply Val_to_IProp_Persistent_Persistent; apply HΔ.
rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
apply always_intro'; trivial.
Qed.
Global Instance Persistent_context_interp_rel Δ Γ vs
{HΔ : context_interp_Persistent Δ}
: PersistentP ([∧] zip_with(λ τ v, interp τ Δ v) Γ vs)%I.
Proof. typeclasses eauto. Qed.
Global Program Instance extend_context_interp_Persistent f Δ
(Hf : Val_to_IProp_Persistent f)
{HΔ : context_interp_Persistent Δ}
: context_interp_Persistent (@extend_context_interp f Δ).
Next Obligation.
intros f Δ Hf HΔ v w; destruct v; cbn; trivial.
apply HΔ.
Qed.
Global Instance extend_context_interp_Persistent
(f : valC -n> iPropG lang Σ) (Δ : varC -n> valC -n> iPropG lang Σ)
(Hf : ∀ v, PersistentP (f v))
{HΔ : ∀ x v, PersistentP (Δ x v)}
: ∀ x v, PersistentP (@extend_context_interp f Δ x v).
Proof. intros x v. destruct x; cbn; trivial. Qed.
Local Ltac properness :=
repeat
......@@ -380,10 +349,8 @@ Section logrel.
λ Δ,
{| cofe_mor_car := λ v, if lt_dec v m then Δ v else Δ (v - n) |}
|}.
Next Obligation. intros ?????? Hxy; destruct Hxy; trivial. Qed.
Next Obligation.
Proof. intros ?????? Hxy; destruct Hxy; trivial. Qed.
Next Obligation.
Proof.
intros ????? Hfg ?; cbn. destruct lt_dec; rewrite Hfg; trivial.
Qed.
......@@ -474,12 +441,10 @@ Section logrel.
Next Obligation.
Proof. intros m τi Δ n x y Hxy; destruct Hxy; trivial. Qed.
Next Obligation.
Proof.
intros m τi n Δ Δ' HΔ x; cbn;
destruct lt_dec; try destruct eq_nat_dec; auto.
Qed.
Next Obligation.
Proof.
intros m n f g Hfg F Δ x; cbn;
destruct lt_dec; try destruct eq_nat_dec; auto.
Qed.
......@@ -579,8 +544,8 @@ Section logrel.
Lemma zip_with_context_interp_subst
(Δ : varC -n> valC -n> iPropG lang Σ) (Γ : list type)
(vs : list valC) (τi : valC -n> iPropG lang Σ) :
(([∧] zip_with (λ τ v, interp τ Δ v) Γ vs)%I)
≡ ([∧] zip_with (λ τ v, interp τ (extend_context_interp τi Δ) v)
(([∧] zip_with (λ τ, interp τ Δ) Γ vs)%I)
≡ ([∧] zip_with (λ τ, interp τ (extend_context_interp τi Δ))
(map (λ t : type, t.[ren (+1)]) Γ) vs)%I.
Proof.
revert Δ vs τi.
......
F_mu_ref/soundness.v
View file @ 39148535
......@@ -23,14 +23,10 @@ Section Soundness.
λ x,
{|
cofe_mor_car :=
λ y, (True)%I
λ y, True%I
|}
|}.
Global Instance free_context_interp_Persistent :
context_interp_Persistent free_type_context.
Proof. intros x v; apply const_persistent. Qed.
Lemma wp_soundness e τ
: typed [] e τ →
ownership.ownP ∅ ⊢ WP e {{v, ∃ H, @interp Σ H (nroot .@ "Fμ,ref" .@ 1)
......@@ -42,11 +38,9 @@ Section Soundness.
iApply wp_wand_l. iSplitR.
{ iIntros {v} "HΦ". iExists H. iExact "HΦ". }
rewrite -(empty_env_subst e).
iPoseProof (@typed_interp _ _ (nroot .@ "Fμ,ref" .@ 1)
(nroot .@ "Fμ,ref" .@ 2) _ _ []) as "Hi"; eauto;
try typeclasses eauto.
- intros l. apply ndot_preserve_disjoint_r, ndot_ne_disjoint; auto.
- iApply "Hi"; iSplit; eauto.
iApply (@typed_interp _ _ (nroot .@ "Fμ,ref" .@ 1)
(nroot .@ "Fμ,ref" .@ 2) _ _ []); eauto.
intros l. apply ndot_preserve_disjoint_r, ndot_ne_disjoint; auto.
Unshelve. all: trivial.
Qed.
......
F_mu_ref_par/context_refinement.v
View file @ 39148535
......@@ -205,14 +205,15 @@ Section bin_log_related_under_typed_context.
Context {Σ : gFunctors}
{iI : heapIG Σ} {iS : cfgSG Σ}
{N : namespace}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Lemma bin_log_related_under_typed_context Γ e e' τ Γ' τ' K :
(∀ f, e.[iter (List.length Γ) up f] = e) →
(∀ f, e'.[iter (List.length Γ) up f] = e') →
typed_context K Γ τ Γ' τ' →
(∀ Δ {HΔ : context_interp_Persistent Δ},
(∀ Δ {HΔ : ∀ x vw, PersistentP (Δ x vw)},
@bin_log_related _ _ _ N Δ Γ e e' τ HΔ) →
∀ Δ {HΔ : context_interp_Persistent Δ},
∀ Δ {HΔ : ∀ x vw, PersistentP (Δ x vw)},
@bin_log_related _ _ _ N Δ Γ' (fill_ctx K e) (fill_ctx K e') τ' HΔ.
Proof.
revert Γ τ Γ' τ' e e'.
......
F_mu_ref_par/examples/counter.v
View file @ 39148535
......@@ -6,6 +6,7 @@ Import uPred.
Section CG_Counter.
Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
(* Coarse-grained increment *)
Definition CG_increment (x : expr) : expr :=
......@@ -269,7 +270,7 @@ Section CG_Counter.
set (Hdsj := ndot_ne_disjoint N n n' Hneq); set_solver_ndisj.
Lemma FG_CG_counter_refinement N Δ
{HΔ : context_interp_Persistent Δ}
{HΔ : ∀ x v, PersistentP (Δ x v)}
:
(@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)) HΔ).
......
F_mu_ref_par/examples/stack/refinement.v
View file @ 39148535
......@@ -9,6 +9,8 @@ Import uPred.
Section Stack_refinement.
Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ}
{iSTK : authG lang Σ stackUR}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Ltac prove_disj N n n' :=
let Hneq := fresh "Hneq" in
let Hdsj := fresh "Hdsj" in
......@@ -16,7 +18,7 @@ Section Stack_refinement.
set (Hdsj := ndot_ne_disjoint N n n' Hneq); set_solver_ndisj.
Lemma FG_CG_counter_refinement N Δ
{HΔ : context_interp_Persistent Δ}
{HΔ : ∀ x vw, PersistentP (Δ x vw)}
:
(@bin_log_related _ _ _ N Δ [] FG_stack CG_stack
(TForall
......
F_mu_ref_par/examples/stack/stack_rules.v
View file @ 39148535
......@@ -52,7 +52,7 @@ Section Rules.
Qed.
Program Definition StackLink_pre (Q : bivalC -n> iPropG lang Σ)
{HQ : BiVal_to_IProp_Persistent Q} :
{HQ : ∀ vw, PersistentP (Q vw)} :
(bivalC -n> iPropG lang Σ) -n> bivalC -n> iPropG lang Σ :=
{|
cofe_mor_car :=
......@@ -72,12 +72,10 @@ Section Rules.
|}
|}.
Next Obligation.
Proof.
intros Q HQ P n [v1 v2] [w1 w2] [Hv1 Hv2]; simpl in *;
by rewrite Hv1 Hv2.
Qed.
Next Obligation.
Proof.
intros Q HQ n P1 P2 HP v; simpl in *.
repeat (apply exist_ne => ?). repeat apply sep_ne; trivial.
rewrite or_ne; trivial. repeat (apply exist_ne => ?).
......
F_mu_ref_par/fundamental_binary.v
View file @ 39148535
......@@ -13,7 +13,7 @@ Import uPred.
Section typed_interp.
Context {Σ : gFunctors} {iI : heapIG Σ} {iS : cfgSG Σ} {N : namespace}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Implicit Types P Q R : iPropG lang Σ.
Notation "# v" := (of_val v) (at level 20).
......@@ -35,25 +35,23 @@ Section typed_interp.
destruct k; simpl; trivial.
Qed.
Definition bin_log_related Δ Γ e e' τ
{HΔ : context_interp_Persistent Δ} :=
Definition bin_log_related Δ Γ e e' τ {HΔ : ∀ x vw, PersistentP (Δ x vw)} :=
∀ vs,
List.length Γ = List.length vs →
∀ ρ j K,
heapI_ctx (N .@ 2) ★ Spec_ctx (N .@ 3) ρ ★
[∧] zip_with (λ τ v, @interp Σ iS iI (N .@ 1) τ Δ v) Γ vs
★ j ⤇ (fill K (e'.[env_subst (map snd vs)]))
[∧] zip_with (λ τ, interp (N .@ 1) τ Δ) Γ vs
★ j ⤇ fill K (e'.[env_subst (map snd vs)])
⊢ WP e.[env_subst (map fst vs)]
{{ λ v, ∃ v', j ⤇ (fill K (# v')) ★
(@interp Σ iS iI (N .@ 1)
τ Δ (v, v')) }}.
{{ λ v, ∃ v', j ⤇ fill K (# v') ★
interp (N .@ 1) τ Δ (v, v') }}.
Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ)
(at level 20) : bin_logrel_scope.
Local Open Scope bin_logrel_scope.
Notation "✓✓" := context_interp_Persistent.
Notation "✓✓ Δ" := (∀ x v, PersistentP (Δ x v)) (at level 20).
Lemma typed_binary_interp_Pair Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ ∥ Γ ⊩ e1 ≤log≤ e1' ∷ τ1)
......@@ -261,7 +259,7 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_TLam Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : ∀ τi (Hpr: BiVal_to_IProp_Persistent τi),
(IHHtyped : ∀ (τi : bivalC -n> _) (Hpr: ∀ vw, PersistentP (τi vw)),
(extend_context_interp_fun1 τi Δ) ∥ map (λ t : type, t.[ren (+1)]) Γ
⊩ e ≤log≤ e' ∷ τ)
:
......@@ -500,7 +498,7 @@ Qed.
Unshelve. all: eauto using to_of_val. all: SolveDisj 3 l.
Qed.
Lemma typed_binary_interp Δ Γ e τ {HΔ : context_interp_Persistent Δ}
Lemma typed_binary_interp Δ Γ e τ {HΔ : ∀ x vw, PersistentP (Δ x vw)}
(Htyped : typed Γ e τ) : Δ ∥ Γ ⊩ e ≤log≤ e ∷ τ.
Proof.
revert Δ HΔ; induction Htyped; intros Δ HΔ.
......
F_mu_ref_par/fundamental_unary.v
View file @ 39148535
......@@ -22,13 +22,13 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N Δ Γ vs e τ
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : ∀ l : loc, N ⊥ L .@ l)
(Htyped : typed Γ e τ)
(HΔ : context_interp_Persistent Δ)
(HΔ : ∀ x v, PersistentP (Δ x v))
: List.length Γ = List.length vs →
heapI_ctx N ∧ [∧] zip_with (λ τ v, (@interp Σ i L) τ Δ v) Γ vs ⊢
WP e.[env_subst vs] {{ λ v, (@interp Σ i L) τ Δ v }}.
heapI_ctx N ∧ [∧] zip_with (λ τ, interp L τ Δ) Γ vs ⊢
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
......@@ -94,8 +94,8 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case. iIntros { [τi τiPr] } "!". iApply wp_TLam; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
value_case. iIntros { [τi τiPr] } "! /=". iApply wp_TLam; iNext.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
iSplit; trivial.
rewrite zip_with_context_interp_subst; trivial.
- (* TApp *)
......@@ -104,12 +104,12 @@ Section typed_interp.
iApply wp_mono; [|done] => w. by rewrite -interp_subst; simpl.
- (* Fold *)
specialize (IHHtyped Δ HΔ vs Hlen).
setoid_rewrite <- interp_subst in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
iApply wp_wand_l.
iSplitL; [|iApply IHHtyped; auto].
iIntros {v} "#Hv".
value_case.
rewrite -interp_subst.
rewrite fixpoint_unfold; cbn.
iAlways; eauto.
- (* Unfold *)
......
F_mu_ref_par/logrel_binary.v
View file @ 39148535
......@@ -17,12 +17,6 @@ Section logrel.
Canonical Structure bivalC := prodC valC valC.
Class BiVal_to_IProp_Persistent (f : bivalC -n> iPropG lang Σ) :=
val_to_iprop_persistent :
∀ v : (val * val), PersistentP ((cofe_mor_car _ _ f) v).
Arguments BiVal_to_IProp_Persistent /.
(** Just to get nicer closed forms, we define extend_context_interp in
three steps. *)
Program Definition extend_context_interp_fun1
......@@ -193,12 +187,10 @@ Section logrel.
|}
|}.
Next Obligation.
Proof.
intros τ1i τ2i n [x1 x2] [y1 y2] [H1 H2]; simpl in *.
rewrite H1 H2; trivial.
Qed.
Next Obligation.
Proof.
intros τ1i n τi τi' Hτi z; simpl in *.
apply always_ne;
apply forall_ne =>j; apply forall_ne =>K; apply forall_ne =>v.
......@@ -206,7 +198,6 @@ Section logrel.
apply wp_ne => t; apply exist_ne => h. rewrite Hτi; trivial.
Qed.
Next Obligation.
Proof.
intros n τi τi' Hτi τ2i z; simpl in *.
apply always_ne;
apply forall_ne =>j; apply forall_ne =>K; apply forall_ne =>v.
......@@ -223,7 +214,7 @@ Section logrel.
cofe_mor_car :=
λ w,
(∀ (τ'i : {f : (bivalC -n> iPropG lang Σ) |
BiVal_to_IProp_Persistent f}),
∀ vw, PersistentP (f vw)}%type),
□ (∀ j K,
j ⤇ (fill K (TApp (# w.2))) →
WP TApp (# w.1) {{v, ∃ v', j ⤇ (fill K (# v')) ★
......@@ -231,7 +222,6 @@ Section logrel.
|}
|}.
Next Obligation.
Proof.
intros τi n [x1 x2] [y1 y2 ] [H1 H2]. simpl in *; auto.
inversion H1; subst; inversion H2; subst; trivial.
Qed.
......@@ -261,17 +251,14 @@ Section logrel.
|}
|}.
Next Obligation.
Proof.
intros τi rec_appr n [x1 x2] [y1 y2] [H1 H2]; simpl in *.
inversion H1; inversion H2; subst; trivial.
Qed.
Next Obligation.
Proof.
intros τi n f g Hfg x. cbn.
apply always_ne, exist_ne =>w; rewrite Hfg; trivial.
Qed.
Next Obligation.
Proof.
intros n τi τi' Hτi f x. cbn.
apply always_ne, exist_ne =>w; rewrite Hτi; trivial.
Qed.
......@@ -318,12 +305,10 @@ Section logrel.
|}
|}.
Next Obligation.
Proof.
intros τi n [x1 x2] [y1 y2] [H1 H2]; simpl in *.
inversion H1; inversion H2; subst; trivial.
Qed.
Next Obligation.
Proof.
intros n τi τi' Hτi z; simpl in *.