Commit 392b7b43 authored by Amin Timany's avatar Amin Timany

Finish using new iris with "proof mode"

In Fμ and Fμ_ref we do support reduction under Fold.
In fact `Unfold (Fold v)` is reduced to `v` if and only if v is a variable.
parent 9825e341
......@@ -68,7 +68,7 @@ Section typed_interp.
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial]; cbn;
......@@ -148,84 +148,64 @@ Section typed_interp.
iApply wp_mono; [|iApply "Hv"; auto with itauto].
intros; apply interp_closed_irrel_turnstile.
- (* TLam *)
value_case; rewrite -exist_intro; apply and_intro; auto.
apply forall_intro =>τi;
apply (always_intro _ _).
rewrite map_length in IHHtyped.
destruct τi as [τi τiAS].
specialize (IHHtyped
(Vlist_cons τi Δ)
(closed_ctx_map
_ _ _ _
Hctx (λ τ, closed_type_S_ren2 τ 1 0 _))
(closed_type_forall HC)
(alwyas_stable_Vlist_cons _ _ _ τiAS)
_
Hlen
).
rewrite -wp_impl_l -later_intro. apply and_intro;
[ apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l|].
2: etransitivity; [|apply IHHtyped].
+ rewrite and_elim_l; trivial.
+ rewrite zip_with_closed_ctx_list_subst; trivial.
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iPoseProof always_intro "HΓ" as "HP"; try typeclasses eauto; try iExact "HP".
iIntros "#HΓ"; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iRevert "HΓ".
rewrite zip_with_closed_ctx_list_subst.
iIntros "#HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx _ v; cbn.
rewrite and_elim_l.
rewrite exist_elim; eauto => e'.
apply const_elim_l; intros H'; rewrite H'.
rewrite (forall_elim ((interp k τ' H Δ) _)).
rewrite always_elim.
rewrite -wp_TLam; apply later_mono.
apply wp_mono=> w.
rewrite interp_subst; trivial.
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply exist_elim; [|iExact "Hv"]; cbn.
iIntros {e'} "[% #He']"; rewrite H0.
iApply wp_TLam.
iSpecialize "He'" {((interp k τ' H Δ) _)}; cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
intros w; rewrite interp_subst; trivial.
- (* Fold *)
value_case. unfold interp_rec.
rewrite fixpoint_unfold.
cbn.
rewrite -exist_intro.
apply (always_intro _ _).
apply and_intro; auto.
rewrite map_length in IHHtyped.
specialize (IHHtyped
(Vlist_cons (interp k (TRec τ) HC Δ) Δ)
(closed_ctx_map
_ _ _ _
Hctx (λ τ, closed_type_S_ren2 τ 1 0 _))
(closed_type_rec HC)
(alwyas_stable_Vlist_cons _ _ _ _)
_
Hlen
).
rewrite -wp_impl_l -later_intro. apply and_intro;
[ apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l|].
2: etransitivity; [|apply IHHtyped].
+ rewrite and_elim_l; trivial.
+ rewrite zip_with_closed_ctx_list_subst; trivial.
iApply (@wp_bind _ _ _ [FoldCtx]);
iApply wp_impl_l;
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped _ _ (closed_type_rec HC)); trivial]; cbn.
+ iIntros {v} "#Hv".
value_case. rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
eapply (@always_intro _ _ _ _).
iApply exist_intro; iSplit; trivial.
iNext.
change (fixpoint (interp_rec_pre
(Vlist_cons_apply Δ (interp (S k) τ (closed_type_rec HC)))))
with ((interp k (TRec τ) HC) Δ); trivial.
+ iRevert "HΓ"; rewrite zip_with_closed_ctx_list_subst; iIntros "#HΓ"; trivial.
- (* Unfold *)
smart_wp_bind UnfoldCtx _ v; cbn.
rewrite and_elim_l.
unfold interp_rec. rewrite fixpoint_unfold /interp_rec_pre; cbn.
replace (fixpoint
(λ rec_apr : leibniz_val -n> iProp lang Σ,
CofeMor
(λ w : leibniz_val,
( e1 : expr,
w = FoldV e1
WP e1 @ {{ λ v1 : val,
((interp (S k) τ (closed_type_rec ?HC4))
(Vlist_cons rec_apr Δ)) v1 }}))%I))
with
(interp k (TRec τ) (typed_closed_type _ _ _ _ Htyped) Δ) by (cbn; unfold interp_rec; trivial).
rewrite always_elim.
rewrite exist_elim; eauto => e'.
apply const_elim_l; intros H'; rewrite H'.
rewrite -wp_Fold.
apply later_mono, wp_mono => w.
rewrite -interp_subst; eauto.
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_impl_l;
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped _ _ (typed_closed_type _ _ _ _ Htyped)); trivial]; cbn.
iIntros {v}.
rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
iIntros "#Hv".
iApply exist_elim; [|iAssumption].
iIntros {w}; cbn.
change (fixpoint (interp_rec_pre
(Vlist_cons_apply
Δ
(interp
(S k) τ
(closed_type_rec
(typed_closed_type k Γ e (TRec τ) Htyped))))))
with ((interp k (TRec τ) (typed_closed_type k Γ e (TRec τ) Htyped)) Δ); trivial.
iIntros "[% #Hw]"; rewrite H.
iApply wp_Fold; cbn; auto using to_of_val.
iRevert "Hw". rewrite -interp_subst. iIntros "#Hw". trivial.
(* unshelving *)
Unshelve.
all: solve [eauto 2 using typed_closed_type | try typeclasses eauto].
all: cbn; solve [eauto 2 using closed_ctx_map_S_back,
typed_closed_type | try typeclasses eauto].
Qed.
End typed_interp.
End typed_interp.
\ No newline at end of file
......@@ -21,7 +21,6 @@ Section logrel.
Arguments val_to_iprop_always_stable /.
Definition interp_unit : leibniz_val -n> iProp lang Σ :=
{|
cofe_mor_car := λ w, (w = UnitV)%I
......@@ -124,22 +123,22 @@ Section logrel.
(rec_apr : (leibniz_val -n> iProp lang Σ))
: (leibniz_val -n> iProp lang Σ) :=
{|
cofe_mor_car := λ w, ( ( e, w = FoldV e WP e @ {{ λ v, τi rec_apr v}}))%I
cofe_mor_car := λ w, ( ( v, w = FoldV v (τi rec_apr v)))%I
|}.
Global Instance interp_rec_pre_proper : Proper (() ==> () ==> ()) interp_rec_pre.
Proof.
intros τ1 τ1' H1 τ2 τ2' H2 w.
apply always_proper; apply exist_proper=>e; apply and_proper; trivial.
apply later_proper, wp_proper=>v.
apply always_proper, exist_proper=>e; apply and_proper; trivial.
apply later_proper.
rewrite H1 H2; trivial.
Qed.
Global Instance interp_rec_pre_ne n : Proper (dist n ==> dist n ==> dist n) interp_rec_pre.
Proof.
intros τ1 τ1' H1 τ2 τ2' H2 w.
apply always_ne; apply exist_ne=>e; apply and_ne; trivial.
apply (contractive_ne _), wp_ne=>v.
apply always_ne, exist_ne=>e; apply and_ne; trivial.
apply (contractive_ne _).
rewrite H1 H2; trivial.
Qed.
......@@ -149,9 +148,9 @@ Section logrel.
Contractive (interp_rec_pre τi).
Proof.
intros n f g H w; cbn.
apply always_ne;apply exist_ne; intros e; apply and_ne; trivial.
apply always_ne, exist_ne; intros e; apply and_ne; trivial.
apply later_contractive =>i Hi.
apply wp_ne; intros v; rewrite H; trivial.
rewrite H; trivial.
Qed.
Definition interp_rec (τi : (leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ))
......@@ -281,14 +280,15 @@ Section logrel.
{HΔ : VlistAlwaysStable Δ}
: Val_to_IProp_AlwaysStable (interp k τ H Δ).
Proof.
induction τ; cbn; intros v; try apply _.
- rewrite /interp_rec /PersistentP fixpoint_unfold /interp_rec_pre.
apply always_intro'; trivial.
- apply (@force_lookup_Forall
_ _
(λ f : leibniz_val -n> iProp lang Σ, PersistentP (f v))).
apply Forall_forall => f H1.
eapply Forall_forall in HΔ; [apply HΔ|trivial].
revert k H Δ HΔ.
induction τ; cbn; intros k H Δ HΔ v; try apply _.
- rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
apply always_intro'; trivial.
- apply (@force_lookup_Forall
_ _
(λ f : leibniz_val -n> iProp lang Σ, PersistentP (f v))).
apply Forall_forall => f H1.
eapply Forall_forall in HΔ; [apply HΔ|trivial].
Qed.
Global Instance alwyas_stable_Δ k Δ Γ vs
......
......@@ -94,11 +94,13 @@ Section lang_rules.
- by rewrite right_id.
Qed.
Lemma wp_Fold E e Q :
wp E e Q wp E (Unfold (Fold e)) Q.
Lemma wp_Fold E e v Q :
to_val e = Some v
Q v wp E (Unfold (Fold e)) Q.
Proof.
rewrite -(wp_lift_pure_det_step (Unfold _) e None) //=; auto.
- by rewrite right_id.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Unfold _) (of_val v) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Q :
......
......@@ -334,4 +334,14 @@ Proof.
(s1 s2 : nat A) x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega typed_subst_invariant.
Qed.
Lemma closed_ctx_map_S_back (k : nat) (Γ : list type) (e : expr) (τ : type) :
closed_ctx k Γ
closed_ctx (S k) (map (λ t : type, t.[ren (+1)]) Γ).
Proof.
intros H.
eapply closed_ctx_map; [eassumption|].
clear; intros τ' H'.
set (HW := closed_type_S_ren2 τ' 1 0); cbn in HW; apply HW; trivial.
Qed.
\ No newline at end of file
......@@ -18,6 +18,7 @@ Section typed_interp.
Implicit Types P Q R : iPropG lang Σ.
Notation "# v" := (of_val v) (at level 20).
(*
Local Ltac ipropsimpl :=
repeat
match goal with
......@@ -45,6 +46,44 @@ Section typed_interp.
Local Hint Extern 2 (_ _)%I => etransitivity; [|rewrite -later_intro] : itauto.
Local Ltac value_case := rewrite -wp_value/= ?to_of_val //; auto 2.
*)
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
|-
(_
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial];
[apply (always_intro _ _); iIntros {v} Hv|iSplit; trivial]; cbn.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma later_exist_turnstile (M : cmraT) (A : Type) :
Inhabited A Φ : A uPred M, ( ( a : A, Φ a))%I ( a : A, Φ a)%I.
Proof. intros H Φ. rewrite later_exist; trivial. Qed.
Lemma typed_interp N k Δ Γ vs e τ
(HNLdisj : l : loc, N L .@ l)
......@@ -52,255 +91,192 @@ Section typed_interp.
(Hctx : closed_ctx k Γ)
(HC : closed_type k τ)
(HΔ : VlistAlwaysStable Δ)
: length Γ = length vs
: List.length Γ = List.length vs
(heap_ctx N Π∧ zip_with (λ τ v, (@interp Σ i L) k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I
WP (e.[env_subst vs]) @ {{ λ v, (@interp Σ i L) k τ HC Δ v }}.
Proof.
revert Hctx HC HΔ vs.
induction Htyped; intros Hctx HC HΔ vs Hlen; cbn.
induction Htyped; intros Hctx HC HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv /= -wp_value; eauto using to_of_val.
rewrite /env_subst Hv; value_case.
edestruct (zipwith_Forall_lookup _ Hctx) as [Hτ' Hτ'eq]; eauto.
rewrite and_elim_r.
etransitivity.
apply big_and_elem_of, elem_of_list_lookup_2 with x.
iApply interp_closed_irrel_turnstile.
iApply big_and_elem_of "HΓ"; eauto.
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
rewrite interp_closed_irrel; trivial.
- (* unit *) value_case.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) _ v; eauto.
(* weird!: and_alwaysstable is an instance but is not resolved! *)
smart_wp_bind (PairRCtx v) (and_persistent _ _ _ _) v'.
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
value_case; eauto 10 with itauto.
- (* fst *)
smart_wp_bind (FstCtx) v. ipropsimpl; eauto.
apply const_elim_l; intros H; rewrite H.
rewrite -wp_fst; eauto using to_of_val, and_elim_l.
rewrite and_elim_l; rewrite interp_closed_irrel; eauto.
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.
iNext; iApply interp_closed_irrel_turnstile; trivial.
- (* snd *)
smart_wp_bind SndCtx v. ipropsimpl; eauto.
apply const_elim_l; intros H; rewrite H.
rewrite -wp_snd; eauto using to_of_val, and_elim_l.
rewrite and_elim_r; rewrite interp_closed_irrel; eauto.
- (* injl *) smart_wp_bind InjLCtx v; value_case; eauto 7 with itauto.
- (* injr *) smart_wp_bind InjRCtx v; value_case; eauto 7 with itauto.
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.
iNext; iApply interp_closed_irrel_turnstile; trivial.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn.
value_case; iRight; auto with itauto.
- (* case *)
smart_wp_bind (CaseCtx _ _) _ v. cbn.
rewrite (later_intro (heap_ctx N Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v0 : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v0) (closed_ctx_list k Γ Hctx) vs));
rewrite or_elim; [apply impl_elim_l| |].
+ rewrite exist_elim; eauto; intros v'.
apply const_elim_l; intros H; rewrite H.
rewrite -impl_intro_r //; rewrite -later_and later_mono; eauto.
rewrite -wp_case_inl; eauto using to_of_val.
asimpl.
specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (v'::vs)).
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
rewrite -IHHtyped2; cbn; auto.
rewrite interp_closed_irrel type_context_closed_irrel /closed_ctx_list.
apply later_mono; repeat apply and_intro; eauto 3 with itauto.
+ rewrite exist_elim; eauto; intros v'.
apply const_elim_l; intros H; rewrite H.
rewrite -impl_intro_r //; rewrite -later_and later_mono; eauto.
rewrite -wp_case_inr; eauto using to_of_val.
asimpl.
specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (v'::vs)).
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
rewrite -IHHtyped3; cbn; auto.
rewrite interp_closed_irrel type_context_closed_irrel /closed_ctx_list.
apply later_mono; repeat apply and_intro; eauto 3 with itauto.
smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "HΓ"; iRevert "Hheap";
iApply exist_elim; eauto; cbn;
iIntros {w} "#[% Hw2] #HΓ #Hheap"; rewrite H; cbn;
[iApply wp_case_inl|iApply wp_case_inr];
auto 1 using to_of_val;
asimpl;
[specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (w::vs)) |
specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (w::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto;
(iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
iApply type_context_closed_irrel_turnstile]; trivial).
- (* lam *)
value_case; apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l.
rewrite -wp_lam ?to_of_val //=.
asimpl. erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
rewrite (later_intro (heap_ctx N Π∧ _)) -later_and; apply later_mono.
rewrite interp_closed_irrel type_context_closed_irrel /closed_ctx_list.
rewrite -(IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC) HΔ (v :: vs)); cbn; auto 2 with f_equal.
repeat apply and_intro; eauto 3 with itauto.
value_case; apply (always_intro _ _); iIntros {w} "#Hw".
iApply wp_lam; auto 1 using to_of_val.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
iNext; iApply (IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC)
HΔ (w :: vs)); cbn; auto.
(iSplit; [trivial|iSplit]; [iApply interp_closed_irrel_turnstile|
iApply type_context_closed_irrel_turnstile]; trivial).
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) _ v.
rewrite -(@wp_bind _ _ _ [AppRCtx v]) /=.
rewrite -wp_impl_l /=; apply and_intro.
2: etransitivity; [|apply IHHtyped2]; eauto using and_elim_r.
rewrite and_elim_l. apply always_mono.
apply forall_intro =>v'.
rewrite forall_elim.
apply impl_intro_l.
rewrite -(later_intro).
etransitivity; [apply impl_elim_r|].
apply wp_mono => w.
rewrite interp_closed_irrel; trivial.
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"; auto with itauto].
intros; apply interp_closed_irrel_turnstile.
- (* TLam *)
value_case; rewrite -exist_intro; apply and_intro; auto.
apply forall_intro =>τi;
apply (always_intro _ _).
rewrite map_length in IHHtyped.
destruct τi as [τi τiAS].
specialize (IHHtyped
(Vlist_cons τi Δ)
(closed_ctx_map
_ _ _ _
Hctx (λ τ, closed_type_S_ren2 τ 1 0 _))
(closed_type_forall HC)
(alwyas_stable_Vlist_cons _ _ _ τiAS)
_
Hlen
).
rewrite -wp_impl_l -later_intro. apply and_intro;
[ apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l|].
2: etransitivity; [|apply IHHtyped].
+ rewrite and_elim_l; trivial.
+ rewrite zip_with_closed_ctx_list_subst; trivial.
value_case; iApply exist_intro; iSplit; trivial.
iIntros {τi}; destruct τi as [τi τiPr].
iRevert "Hheap".
iPoseProof always_intro "HΓ" as "HP"; try typeclasses eauto;
try (iApply always_impl; iExact "HP").
iIntros "#HΓ #Hheap"; iNext.
iApply IHHtyped; [rewrite map_length|]; trivial.
iSplit; trivial.
iRevert "HΓ". rewrite zip_with_closed_ctx_list_subst. iIntros "#HΓ"; trivial.
- (* TApp *)
smart_wp_bind TAppCtx _ v; cbn.
rewrite and_elim_l.
rewrite exist_elim; eauto => e'.
apply const_elim_l; intros H'; rewrite H'.
rewrite (forall_elim ((interp k τ' H Δ) _)).
rewrite always_elim.
rewrite -wp_TLam; apply later_mono.
apply wp_mono=> w.
eapply entails_proper.
+ apply interp_subst.
+ eauto.
+ eauto.
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iApply exist_elim; [|iExact "Hv"]; cbn.
iIntros {e'} "[% #He']"; rewrite H0.
iApply wp_TLam.
iSpecialize "He'" {((interp k τ' H Δ) _)}; cbn.
iApply always_elim. iApply always_mono; [|trivial].
iIntros "He'"; iNext.
iApply wp_mono; [|trivial].
intros w; cbn; rewrite -interp_subst; trivial.
- (* Fold *)
value_case. unfold interp_rec.
rewrite fixpoint_unfold.
cbn.
rewrite -exist_intro.
apply (always_intro _ _).
apply and_intro; auto.
rewrite map_length in IHHtyped.
specialize (IHHtyped
(Vlist_cons (@interp Σ i L k (TRec τ) HC Δ) Δ)
(closed_ctx_map
_ _ _ _
Hctx (λ τ, closed_type_S_ren2 τ 1 0 _))
(closed_type_rec HC)
(alwyas_stable_Vlist_cons _ _ _ _)
_
Hlen
).
rewrite -wp_impl_l -later_intro. apply and_intro;
[ apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l|].
2: etransitivity; [|apply IHHtyped].
+ rewrite and_elim_l; trivial.
+ rewrite zip_with_closed_ctx_list_subst; trivial.
iApply (@wp_bind _ _ _ [FoldCtx]);
iApply wp_impl_l;
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped _ _ (closed_type_rec HC)); trivial]; cbn.
+ iIntros {v} "#Hv".
value_case. rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
eapply (@always_intro _ _ _ _).
iApply exist_intro; iSplit; trivial.
iNext.
change (fixpoint (interp_rec_pre
(Vlist_cons_apply Δ (interp (S k) τ (closed_type_rec HC)))))
with ((@interp _ _ L k (TRec τ) HC) Δ); trivial.
+ iRevert "HΓ"; rewrite zip_with_closed_ctx_list_subst; iIntros "#HΓ";
iSplit; trivial.
- (* Unfold *)
smart_wp_bind UnfoldCtx _ v; cbn.
rewrite and_elim_l.
unfold interp_rec. rewrite fixpoint_unfold /interp_rec_pre; cbn.
replace (fixpoint
(λ rec_apr : leibniz_val -n> iPropG lang Σ,
CofeMor
(λ w : leibniz_val,
( e1 : expr,
w = FoldV e1
WP e1 @ {{ λ v1 : val,
((interp (S k) τ (closed_type_rec ?HC4))
(Vlist_cons rec_apr Δ)) v1 }}))%I))
with
(@interp Σ i L k (TRec τ) (typed_closed_type _ _ _ _ Htyped) Δ) by (cbn; unfold interp_rec; trivial).
rewrite always_elim.
rewrite exist_elim; eauto => e'.
apply const_elim_l; intros H'; rewrite H'.
rewrite -wp_Fold.
apply later_mono, wp_mono => w.
rewrite -interp_subst; eauto.
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_impl_l;
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped _ _ (typed_closed_type _ _ _ _ Htyped)); trivial];
[|iSplit; trivial]; cbn.
iIntros {v}.
rewrite /interp_rec fixpoint_unfold. unfold interp_rec_pre at 1; cbn.
iIntros "#Hv".
iApply exist_elim; [|iAssumption].
iIntros {w}; cbn.
change (fixpoint (interp_rec_pre
(Vlist_cons_apply
Δ
(interp
(S k) τ
(closed_type_rec
(typed_closed_type k Γ e (TRec τ) Htyped))))))
with ((@interp _ _ L k (TRec τ) (typed_closed_type k Γ e (TRec τ) Htyped)) Δ);
trivial.
iIntros "[% #Hw]"; rewrite H.
iApply wp_Fold; cbn; auto using to_of_val.
iRevert "Hw". rewrite -interp_subst. iIntros "#Hw". trivial.
- (* Alloc *)
smart_wp_bind AllocCtx _ v; cbn.
rewrite -wp_atomic; cbn; eauto using to_of_val.
rewrite -wp_alloc.
apply pvs_intro.
all : eauto 3 using to_of_val with itauto.
rewrite -later_intro.
apply forall_intro => l.
apply wand_intro_l.
rewrite -exist_intro.
rewrite -pvs_always_l.
apply and_intro; auto.
rewrite -inv_alloc; auto.
rewrite -later_intro /interp_ref_pred.
rewrite -exist_intro.
apply sep_mono; eauto.
auto with itauto.
smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
iApply pvs_intro.
iApply wp_alloc; [| | | |iSplit;[iExact "Hheap"|iExact "Hv"]];
[|iIntros "#[Hheap Hv]"| |]; auto using to_of_val.
iIntros "#[Hheap Hv]". iNext.
iIntros {l} "Hl".
iApply exist_intro.
iApply and_intro; [| trivial |]; auto.
iApply inv_alloc; trivial. iNext.
iApply exist_intro.
iSplit; trivial.
- (* Load *)
smart_wp_bind LoadCtx _ v; cbn.
rewrite and_exist_r. apply exist_elim => l.
rewrite -and_assoc.
apply const_elim_l; intros Heq; rewrite Heq.
rewrite -wp_atomic; cbn; eauto using to_of_val.
rewrite -wp_inv; try match goal with |- _ _ => trivial end.
rewrite -pvs_intro; eauto.
cbn; eauto using to_of_val.
apply and_elim_l.
rewrite and_elim_r and_elim_l.
apply wand_intro_l.
unfold interp_ref_pred at 1.
apply wand_elim_l'.
etrans; [rewrite later_exist|]; eauto.
rewrite exist_elim; eauto => w.
apply wand_intro_r.
rewrite -(wp_load _ _ _ 1); try match goal with |- _ _ => trivial end; eauto.
rewrite sep_elim_r; auto with itauto.
smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
iRevert "Hheap". iApply exist_elim; [|iExact "Hv"].
iIntros {l} "[% #Hv] #Hheap"; rewrite H.
iApply wp_atomic; cbn; eauto using to_of_val.
iApply wp_inv; [auto using to_of_val| trivial
| apply and_elim_r | apply and_elim_l | ].
iApply pvs_intro. iSplit; trivial.
iIntros "Hl".
iPoseProof later_exist_turnstile "Hl" as "Hl'"; [typeclasses eauto|].
iRevert "Hheap".
iApply exist_elim; [|iExact "Hl'"].
iIntros {w} "[Hl1 #Hl2] #Hheap".
iApply (wp_load _ _ _ 1);
[apply and_elim_r| trivial | apply and_elim_l | iSplit; trivial].
specialize (HNLdisj l); set_solver_ndisj.
rewrite sep_elim_l.
unfold interp_ref_pred.
rewrite -later_sep.
apply later_mono.
apply sep_mono; eauto.
apply wand_intro_l.
rewrite -later_intro.
rewrite -exist_intro.
rewrite (always_sep_dup (((interp k τ (closed_type_ref _)) Δ) w)).
rewrite sep_assoc.
apply sep_mono; eauto.
rewrite -pvs_intro.
rewrite interp_closed_irrel; trivial.
iNext.
iSplitL; trivial.
iIntros "Hl".
iSplitL.
+ iNext. iApply exist_intro; iSplitL; trivial.
+ iApply pvs_intro; iApply interp_closed_irrel_turnstile; trivial.
- (* Store *)
smart_wp_bind (StoreLCtx _) _ v; cbn.
smart_wp_bind (StoreRCtx _) _ v'; cbn.
rewrite and_comm ?and_assoc.
rewrite !and_exist_r. apply exist_elim => l.