Library iris.chan2heap.simple_reln
From iris.program_logic Require Import ownership hoare auth.
From iris.chan_lang Require Export lang.
From iris.chan2heap Require Export refine_protocol.
From iris.chan_lang Require Export simple_types substitution.
From iris.heap_lang Require Import lang heap proofmode substitution.
Section lr.
Definition Kd := 200%nat.
Definition dinit : nat := 100%nat.
Definition dK K ec :=
match chan_lang.to_val (ectx_language.fill K ec) with
| None ⇒ dinit
| Some _ ⇒ O
end.
Context `{!protG Σ}.
Context `{!refineG heap_lang Σ (delayed_lang (chan_lang) Kd dinit) (S Kd × (Kd + 3))}.
Context `{!scheapG heap_lang Σ}.
Context `{!heap.heapG Σ}.
Definition protN : namespace := nroot.@ "prot".
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Local Notation hexprC := (leibnizC (heap_lang.expr)).
Local Notation cexprC := (leibnizC (chan_lang.expr)).
Local Notation hvalC := (leibnizC (heap_lang.val)).
Local Notation cvalC := (leibnizC (chan_lang.val)).
From iris.proofmode Require Import coq_tactics.
Import uPred.
Definition expr_rel_lift (vrel: hvalC -n> cvalC -n> iProp) eh ec : iProp :=
(∀ i K, ⧆ (ownT i ec K (dK K ec)
-★ WP eh {{ vh, ∃ vc, ⧆ vrel vh vc
★ ownT i (chan_lang.of_val vc) K (dK K vc)}}))%I.
Import uPred.
Lemma expr_rel_lift_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) expr_rel_lift.
Proof.
intros vr1 vr2 Hr ?? → ?? →.
rewrite /expr_rel_lift. setoid_rewrite Hr. eauto.
Qed.
Lemma expr_rel_aff_pres (vrel: hvalC -n> cvalC -n> iProp): (∀ v V, AffineP (vrel v V)) →
∀ e E, AffineP (expr_rel_lift vrel e E).
Proof.
rewrite /AffineP. intros.
rewrite /expr_rel_lift.
apply affine_intro. apply _. auto.
Qed.
Definition lift2 (f: hvalC → cvalC → iProp) : hvalC -n> cvalC -n> iProp :=
CofeMor(λ x, CofeMor (λ y, f x y)).
Definition lift3 (f: typC → hvalC → cvalC → iProp) : typC -n> hvalC -n> cvalC -n> iProp :=
CofeMor(λ x, CofeMor(λ y, CofeMor (λ z, f x y z))).
From iris.heap_lang Require Import notation.
Fixpoint val_equiv_pre
(ve: typC -n> hvalC -n> cvalC -n> iProp)
(ty: typ) (vh: heap_lang.val) (vc: chan_lang.val)
: iProp :=
match ty with
| Int ⇒ (∃ (n: Z), ⧆(vh = #n) ★ ⧆(vc = chan_lang.LitV (chan_lang.LitInt n)))%I
| Bool ⇒ (∃ (b: bool), ⧆(vh = #b) ★ ⧆(vc = chan_lang.LitV (chan_lang.LitBool b)))%I
| Unit ⇒ (⧆(vh = #()) ★ ⧆(vc = chan_lang.LitV chan_lang.LitUnit))%I
| Tensor ty1 ty2 ⇒
(∃ (vh1 vh2: heap_lang.val) (vc1 vc2: chan_lang.val),
⧆(vh = (vh1, vh2)%V) ★
⧆(vc = chan_lang.PairV vc1 vc2) ★
(val_equiv_pre ve ty1 vh1 vc1) ★
(val_equiv_pre ve ty2 vh2 vc2))%I
| Lolli ty1 ty2 ⇒
(∃ x (eh1: heap_lang.expr) pfh y (ec1: chan_lang.expr) pfc,
⧆(vh = @heap_lang.RecV BAnon x%bind eh1 pfh) ★
⧆(vc = @chan_lang.RecV BAnon y%bind ec1 pfc) ★
(∀ vh1 vc1, ⧆(val_equiv_pre ve ty1 vh1 vc1
-★ expr_rel_lift (lift2 (val_equiv_pre ve ty2))
(App vh vh1) (chan_lang.App vc vc1))))%I
| Styp p ⇒ (∃ (lh: heap_lang.loc) (lc: chan_lang.loc) (s: side),
⧆(vh = #lh) ★
⧆(vc = chan_lang.LitV $ chan_lang.LitLoc lc s) ★
prot_mapsto protN typ
(CofeMor (λ ty, (CofeMor (λ vh, CofeMor (λ vc, ▷ (ve ty vh vc))))))
(lc, s) lh
p)%I
| _ ⇒ False%I
end.
Definition val_equiv_preC (ve: typC -n> hvalC -n> cvalC -n> iProp):
typC -n> hvalC -n> cvalC -n> iProp := lift3 (val_equiv_pre ve).
Instance val_equiv_pre_contractive : Contractive (val_equiv_preC).
Proof.
intros n ve1 ve2 Hvd ty vh vc. simpl.
revert ve1 ve2 Hvd ty vh vc.
induction ty; intros; rewrite /val_equiv_pre; fold val_equiv_pre.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto;
eapply later_contractive; intros; eapply Hvd; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
repeat apply forall_ne=>?.
apply affine_ne. apply wand_ne; first eauto.
eapply expr_rel_lift_ne; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
- eauto.
- apply exist_ne=>?; apply sep_ne; eauto.
- eauto.
- repeat apply exist_ne=>?.
apply sep_ne; first eauto.
apply sep_ne; first eauto.
apply prot_mapsto_ne; auto.
intros ???. apply later_contractive=>??.
rewrite Hvd; eauto.
Qed.
Definition val_equiv: typC -n> hvalC -n> cvalC -n> iProp := fixpoint val_equiv_preC.
Lemma val_equiv_fix_unfold ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_preC val_equiv ty vh vc.
Proof. by rewrite /val_equiv -fixpoint_unfold. Qed.
Lemma val_equiv_fix_unfold' ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_pre val_equiv ty vh vc.
Proof. rewrite val_equiv_fix_unfold. auto. Qed.
Instance val_equiv_affine ty eh ec: AffineP (val_equiv ty eh ec).
Proof.
rewrite /AffineP val_equiv_fix_unfold'; revert eh ec; induction ty⇒eh ec; simpl.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply sep_affine; rewrite /AffineP; eauto.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply affine_intro; first apply _.
repeat (rewrite ?affine_forall; apply forall_mono=>?).
apply affine_mono; eauto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- rewrite affine_exist; apply exist_mono=>?.
rewrite affine_exist; apply exist_mono=>?.
rewrite affine_exist; apply exist_mono⇒s.
repeat (apply sep_affine; first apply _).
rewrite /prot_mapsto.
rewrite /prot_ctx. destruct s; simpl; apply _.
Qed.
Instance val_equiv_pre_affine ty eh ec: AffineP (val_equiv_pre val_equiv ty eh ec).
Proof. rewrite /AffineP. rewrite -val_equiv_fix_unfold'. apply val_equiv_affine. Qed.
Notation csubst_map := chan_lang.substitution.subst_map.
Notation hsubst_map := heap_lang.substitution.subst_map.
Notation cmsubst := chan_lang.substitution.msubst.
Notation hmsubst := heap_lang.substitution.msubst.
Definition expr_equiv ty := expr_rel_lift (val_equiv ty).
Instance expr_equiv_affine ty eh ec: AffineP (expr_equiv ty eh ec).
Proof. eapply expr_rel_aff_pres=>??; apply _. Qed.
Record subst_tuple :=
stuple { styp : typ ; hval : heap_lang.expr; cval : chan_lang.expr }.
Definition subst_ctx := gmap string subst_tuple.
Definition subst2typ (S: subst_ctx) : typ_ctx := styp <$> S.
Definition subst2cl (S: subst_ctx) : csubst_map := cval <$> S.
Definition subst2hl (S: subst_ctx) : hsubst_map := hval <$> S.
Implicit Types S : subst_ctx.
Coercion subst2hl' := subst2hl.
Coercion subst2cl' := subst2cl.
Coercion subst2typ' := subst2typ.
Definition ctx_expr_equiv (Γ: typ_ctx) (ty: typ) (eh: heap_lang.expr) (ec: chan_lang.expr) : Prop :=
∀ (S: subst_ctx) (Herase: subst2typ S = Γ),
ClosedSubst [] S →
chan_lang.substitution.ClosedSubst [] S →
heap_ctx ★ scheap_ctx ★ ([★ map] x ↦ P ∈ S, (expr_equiv (styp P) (hval P) (cval P)))
⊢ expr_equiv ty (hmsubst S eh)
(cmsubst S ec).
Instance ctx_prop_affine S:
AffineP ([★ map] x↦P ∈S, (expr_equiv (styp P) (hval P) (cval P)))%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using expr_equiv_affine.
Qed.
Lemma val_equiv_expr ty vh vc:
(val_equiv_pre val_equiv ty vh vc ⊢ expr_equiv ty vh vc)%I.
Proof.
rewrite /expr_equiv /expr_rel_lift.
iIntros "Hve". iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists vc. iFrame "Hown".
iIntros "@". by rewrite val_equiv_fix_unfold'.
Qed.
Lemma expr_equiv_empty ty eh ec (pf: ctx_expr_equiv ∅ ty eh ec):
heap_ctx ★ scheap_ctx ⊢ (expr_rel_lift (val_equiv ty) eh ec).
Proof.
rewrite /expr_equiv in pf.
specialize (pf ∅). rewrite /subst2typ fmap_empty in pf.
efeed pose proof pf as pf'; eauto; try done.
rewrite big_sepM_empty right_id in pf' ×.
intros ->; auto.
Qed.
Definition bool_refine (v: heap_lang.val) (v': chan_lang.val) :=
match v, v' with
| LitV (LitBool b), chan_lang.LitV (chan_lang.LitBool b') ⇒
b = b'
| _, _ ⇒ False
end.
Lemma chan_prim_dec: ∀ (e: chan_lang.expr) σ,
{ t | prim_step (e: chan_lang.expr) σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}.
Proof.
intros. edestruct (ClassicalEpsilon.excluded_middle_informative
((∃ (e' : language.expr (ectx_lang (chan_lang.expr)))
(σ' : language.state (ectx_lang (chan_lang.expr)))
(ef' : option (language.expr (ectx_lang (chan_lang.expr)))),
language.prim_step e σ e' σ' ef'))).
× apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (e'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (σ'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (ef'&e0).
left. ∃ (e', σ', ef'). eauto.
× right. auto.
Qed.
From iris.heap_lang Require Import proofmode notation.
Lemma subst2typ_inv Γ S x ty:
Γ !! x = Some ty →
subst2typ S = Γ →
∃ eh ec, S !! x = Some {| styp := ty; hval := eh; cval := ec |}.
Proof.
rewrite /subst2typ. intros Hlook <-.
move:Hlook. rewrite lookup_fmap. case_eq (S !! x).
- intros st Heq. rewrite ?Heq.
inversion 1. destruct st; eauto.
- intros Hnone. rewrite ?Hnone.
inversion 1.
Qed.
Lemma NoDup_filter_fmap {A B: Type} (f: A → B) P pf (l: list A):
NoDup (f <$> l) → NoDup (f <$> (@filter _ _ _ P pf l)).
Proof.
induction l. eauto.
simpl. inversion 1. subst.
rewrite /filter /list_filter. case_decide.
- rewrite //=. econstructor; eauto.
intros (?&Heq&Helem)%elem_of_list_fmap_2.
match goal with [ H: ¬ _ |- _] ⇒ apply H end.
rewrite Heq. apply elem_of_list_fmap_1.
rewrite elem_of_list_filter in Helem ×. intros (?&?); auto.
- auto.
Qed.
Lemma subst_ctx_subseteq S Γ Γ1 Γ2:
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
subst2typ S = Γ →
∃ S1 S2,
S1 ⊆ S ∧
S2 ⊆ S ∧
dom (gset string) S1 ∩ dom (gset string) S2 ≡ ∅ ∧
subst2typ S1 = Γ1 ∧
subst2typ S2 = Γ2.
Proof.
intros Hsub1 Hsub2 Hdom Herase.
set (l := map_to_list S).
set (l1 := filter (λ p, p.1 ∈ dom (gset string) Γ1) l).
set (l2 := filter (λ p, p.1 ∈ dom (gset string) Γ2) l).
∃ (map_of_list l1).
∃ (map_of_list l2).
split_and!.
- rewrite /l1 /l. apply map_subseteq_spec⇒x P.
intros Helem%elem_of_map_of_list_2.
by apply elem_of_list_filter in Helem as (?&?%elem_of_map_to_list).
- rewrite /l2 /l. apply map_subseteq_spec⇒x P.
intros Helem%elem_of_map_of_list_2.
by apply elem_of_list_filter in Helem as (?&?%elem_of_map_to_list).
- clear -Hdom. set_unfold. rewrite /l1 /l2 /l⇒x.
rewrite ?elem_of_dom.
rewrite /is_Some.
intros ((P1&Helem1)&(P2&Helem2)).
apply elem_of_map_of_list_2, elem_of_list_filter in Helem1 as (Hd1&_).
apply elem_of_map_of_list_2, elem_of_list_filter in Helem2 as (Hd2&_).
eapply Hdom. split; eauto.
- apply map_eq_iff⇒x. rewrite /subst2typ lookup_fmap.
case_eq (Γ1 !! x).
× intros ty Hlook1.
assert (Γ !! x = Some ty) as Hlook.
{ eapply (map_subseteq_spec Γ1); eauto. }
eapply subst2typ_inv in Hlook as (eh&ec&?); eauto.
efeed pose proof (elem_of_map_of_list_1 l1 x {| styp := ty; hval := eh; cval := ec|})
as Hlook'.
{ rewrite /l1 /l. eapply NoDup_filter_fmap. apply NoDup_fst_map_to_list. }
{ rewrite /l1 /l. apply elem_of_list_filter. split.
- rewrite elem_of_dom; eauto.
- by rewrite elem_of_map_to_list. }
rewrite Hlook'. auto.
× intros Hnone.
rewrite Hnone.
rewrite not_elem_of_map_of_list_1; auto.
rewrite /l1.
intros ((?&P)&Heq&Helem)%elem_of_list_fmap_2.
apply elem_of_list_filter in Helem as (HelemΓ1&?).
rewrite -Heq elem_of_dom in HelemΓ1 ×.
rewrite Hnone. inversion 1. congruence.
- apply map_eq_iff⇒x. rewrite /subst2typ lookup_fmap.
case_eq (Γ2 !! x).
× intros ty Hlook1.
assert (Γ !! x = Some ty) as Hlook.
{ eapply (map_subseteq_spec Γ2); eauto. }
eapply subst2typ_inv in Hlook as (eh&ec&?); eauto.
efeed pose proof (elem_of_map_of_list_1 l2 x {| styp := ty; hval := eh; cval := ec|})
as Hlook'.
{ rewrite /l2 /l. eapply NoDup_filter_fmap. apply NoDup_fst_map_to_list. }
{ rewrite /l2 /l. apply elem_of_list_filter. split.
- rewrite elem_of_dom; eauto.
- by rewrite elem_of_map_to_list. }
rewrite Hlook'. auto.
× intros Hnone.
rewrite Hnone.
rewrite not_elem_of_map_of_list_1; auto.
rewrite /l2.
intros ((?&P)&Heq&Helem)%elem_of_list_fmap_2.
apply elem_of_list_filter in Helem as (HelemΓ1&?).
rewrite -Heq elem_of_dom in HelemΓ1 ×.
rewrite Hnone. inversion 1. congruence.
Qed.
Lemma fmap_subseteq {A B} (f: A → B) (S1 S2: gmap string A):
S1 ⊆ S2 → f <$> S1 ⊆ f <$> S2.
Proof.
rewrite ?map_subseteq_spec⇒ Hs1 i x.
rewrite ?lookup_fmap.
specialize (Hs1 i). destruct (S1 !! i).
- erewrite Hs1; eauto.
- inversion 1.
Qed.
From iris.chan_lang Require Export lang derived refine refine_heap refine_heap_proofmode protocol.
Lemma tac_refine_bind Δ Δ' k t e K K' P:
envs_lookup k Δ = Some (false, ownT t (fill K' e) K (dK K (fill K' e))) →
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') (dK (comp_ectx K K') e))) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
rewrite ownT_focus //= ?right_id. by rewrite wand_elim_r.
Qed.
Lemma tac_refine_unbind Δ Δ' k t e K K' P :
envs_lookup k Δ = Some (false, ownT t e (comp_ectx K K') (dK (comp_ectx K K') e)) →
envs_simple_replace k false (Esnoc Enil k (ownT t (fill K' e) K (dK K (fill K' e)))) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
by rewrite -ownT_fill //= ?right_id wand_elim_r.
Qed.
Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_bind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) constr(K') "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ j _ _ K K';
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ _ _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_focus" open_constr(efoc) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
chan_lang.tactics.reshape_expr e ltac:(fun K' e' ⇒
match e' with
| efoc ⇒ idtac K';
unify e' efoc;
refine_bind K' at j
end) || fail "refine_focus: cannot find" efoc "in" e
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_unfocus" :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (comp_ectx ?K0 ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (?K0 ++ ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
refine_unbind empty_ectx K at j; simpl_subst
| _ ⇒ fail "refine_unocus: could not find ownT"
end.
Instance: Params (@val_equiv_pre) 1.
Lemma ClosedSubst_subseteq_hsubst S1 S2 l:
ClosedSubst l S1 →
S2 ⊆ S1 →
ClosedSubst l S2.
Proof.
intros. eapply ClosedSubst_subseteq; eauto.
rewrite /subst2hl' /subst2hl. apply fmap_subseteq; auto.
Qed.
Lemma ClosedSubst_subseteq_csubst S1 S2 l:
chan_lang.substitution.ClosedSubst l S1 →
S2 ⊆ S1 →
chan_lang.substitution.ClosedSubst l S2.
Proof.
intros. eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
rewrite /subst2cl' /subst2cl. apply fmap_subseteq; auto.
Qed.
Lemma subst2typ_insert2_bigM x y s1 s2 (Φ: subst_tuple → iProp) S:
x ≠ y →
subst2typ S !! x = None →
subst2typ S !! y = None →
([★ map] z↦P ∈ <[x:=s1]>(<[y := s2]>S), Φ P)
⊣⊢ Φ s1 ★ Φ s2 ★ ([★ map] z↦P ∈ S, Φ P)%I.
Proof.
intros Hneq Hl1 Hl2.
rewrite big_sepM_insert; last first.
- rewrite lookup_insert_ne; auto.
× move:Hl1. rewrite /subst2typ lookup_fmap.
case_eq (S !! x).
** intros s Heq. rewrite Heq. inversion 1.
** intros s Heq. auto.
- rewrite big_sepM_insert; last first.
× move:Hl2. rewrite /subst2typ lookup_fmap.
case_eq (S !! y).
** intros s Heq. rewrite Heq. inversion 1.
** intros s Heq. auto.
× done.
Qed.
Lemma elem_of_dom_insert_mono {A A'} (x y: string) (s1: A) (s2: A')
(S1: gmap string A) (S2: gmap string A'):
(x ∈ dom (gset string) S1 → x ∈ dom (gset string) S2) →
(x ∈ dom (gset string) (<[y := s1]>S1) → x ∈ dom (gset string) (<[y := s2]>S2)).
Proof.
rewrite ?dom_insert. intros ? [Hy|HS2]%elem_of_union; apply elem_of_union.
- left. auto.
- right. auto.
Qed.
Lemma insert_mono {A} (x: string) (s: A)
(S1 S2: gmap string A):
S1 ⊆ S2 → <[x := s]>S1 ⊆ <[x := s]>S2.
Proof.
rewrite ?map_subseteq_spec. intros Hsub i s'.
case (decide(x = i)).
- intros →. rewrite ?lookup_insert; inversion 1. auto.
- intros Hneq. rewrite ?lookup_insert_ne //. apply Hsub.
Qed.
Lemma fill_val_dK K e1 e2:
is_Some (chan_lang.to_val e1) →
is_Some (chan_lang.to_val e2) →
dK K e1 = dK K e2.
Proof.
intros. rewrite /dK.
rewrite /ectx_language.fill //=.
do 2 case_match; auto.
- exfalso.
specialize (@ectxi_language.fill_val_2 chan_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (chan_lang.fill_item_val_2) K e1 e2);
eauto.
congruence.
- exfalso.
specialize (@ectxi_language.fill_val_2 chan_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (chan_lang.fill_item_val_2) K e2 e1);
eauto.
congruence.
Qed.
Lemma lookup_delete_subst_ctx_1 (S: subst_ctx) (x: string):
delete x S !! x = None.
Proof. apply lookup_delete. Qed.
Lemma lookup_delete_subst_ctx_2 (S: subst_ctx) (x: string):
delete x (subst2cl' S) !! x = None.
Proof. apply lookup_delete. Qed.
Lemma lookup_delete_subst_ctx_3 (S: subst_ctx) (x: string):
delete x (subst2hl' S) !! x = None.
Proof. apply lookup_delete. Qed.
Existing Instance prot_mapsto_affine.
Existing Instance prot_mapsto_proper.
Arguments heap_lang.of_val: simpl never.
Lemma fundamental Γ ty ec:
has_typ Γ ec ty →
ctx_expr_equiv Γ ty (c2h ec) ec.
Proof.
rewrite /ctx_expr_equiv.
intros has_typ.
induction has_typ .
- intros S Herase HcloSh HcloSc.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
eapply subst2typ_inv in Herase as (eh&ec&Hlook); eauto.
rewrite big_sepM_delete; eauto.
rewrite ?lookup_fmap ?Hlook //=.
iIntros "(?&?&?&_)". done.
- intros; iIntros "_". simpl.
rewrite /c2h msubst_msubst' // chan_lang.substitution.msubst_msubst' //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists (chan_lang.LitV (chan_lang.LitBool b)).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists b. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite /c2h msubst_msubst' // chan_lang.substitution.msubst_msubst' //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists (chan_lang.LitV (chan_lang.LitInt n)).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists n. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite /c2h msubst_msubst' // chan_lang.substitution.msubst_msubst' //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists (chan_lang.LitV (chan_lang.LitUnit)).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_focus (msubst S (c2h e1)).
refine_focus (chan_lang.substitution.msubst S e1)%C.
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
erewrite (chan_lang.substitution.msubst_weaken_2 e1 S1 S); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
rewrite -Herase1. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
erewrite (heap_lang.substitution.msubst_weaken_2 (c2h e1) S1 S); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
rewrite -Herase1. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_focus (msubst S (c2h e2)).
refine_focus (chan_lang.substitution.msubst S e2)%C.
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
erewrite (chan_lang.substitution.msubst_weaken_2 e2 S2 S); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
rewrite -Herase2. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
erewrite (heap_lang.substitution.msubst_weaken_2 (c2h e2) S2 S); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
rewrite -Herase2. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
refine_unfocus.
wp_value. iPvsIntro. iExists (chan_lang.PairV vc vc').
iFrame.
rewrite ?val_equiv_fix_unfold; simpl.
iIntros "@". iExists vh, vh', vc, vc'.
iFrame. iSplitL; iPureIntro; done.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_focus (msubst S (c2h e)).
refine_focus (chan_lang.substitution.msubst S e)%C.
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
erewrite (chan_lang.substitution.msubst_weaken_2 e S1 S); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
rewrite -Herase1. intros x' Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
erewrite (heap_lang.substitution.msubst_weaken_2 (c2h e) S1 S); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
rewrite -Herase1. intros x' Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
subst.
rewrite val_equiv_fix_unfold'.
simpl. iDestruct "Hvequiv" as (vh1 vh2 vc1 vc2) "Hv'".
rewrite affine_elim. iDestruct "Hv'" as "(%&%&Hv1&Hv2)".
subst.
replace (heap_lang.of_val (vh1, vh2)%V) with
(heap_lang.of_val vh1, heap_lang.of_val vh2)%E; auto.
assert (heap_lang.Closed [x; y] (hmsubst (delete x (delete y (subst2hl' S))) (c2h eb))).
{ rewrite /heap_lang.Closed.
rewrite /subst2hl' /subst2hl ?fmap_delete.
eapply msubst_closing_inv_3.
{ apply ClosedSubst_delete; auto. }
eapply heap_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply msubst_closing_inv_3; eauto.
eapply heap_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply msubst_closing_1.
{ apply c2h_closed. eapply typ_context_closed_2; eauto. }
eauto.
intros x'.
intros ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
{ intros →. left. set_solver+. }
intros Hne. move: Helem. rewrite lookup_insert_ne; auto.
case (decide (s = y)).
{ intros →. left. set_solver+. }
intros Hne'. rewrite lookup_insert_ne; auto.
rewrite /subst2typ lookup_fmap.
intros; right. apply elem_of_dom.
rewrite lookup_fmap //=.
case_eq (S2 !! s).
× intros P Hlook%map_subseteq_spec; eauto. rewrite Hlook. eauto.
× intros Hnone. rewrite Hnone in Helem. inversion Helem.
}
assert (chan_lang.Closed [x; y] (cmsubst (delete x (delete y (subst2cl' S))) eb)).
{ rewrite /chan_lang.Closed.
rewrite /subst2cl' /subst2cl ?fmap_delete.
eapply chan_lang.substitution.msubst_closing_inv_3.
{ apply chan_lang.substitution.ClosedSubst_delete; auto. }
eapply chan_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply chan_lang.substitution.msubst_closing_inv_3; eauto.
eapply chan_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply chan_lang.substitution.msubst_closing_1.
{ eapply typ_context_closed_2; eauto. }
eauto.
intros x'.
intros ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
{ intros →. left. set_solver+. }
intros Hne. move: Helem. rewrite lookup_insert_ne; auto.
case (decide (s = y)).
{ intros →. left. set_solver+. }
intros Hne'. rewrite lookup_insert_ne; auto.
rewrite /subst2typ lookup_fmap.
intros; right. apply elem_of_dom.
rewrite lookup_fmap //=.
case_eq (S2 !! s).
× intros P Hlook%map_subseteq_spec; eauto. rewrite Hlook. eauto.
× intros Hnone. rewrite Hnone in Helem. inversion Helem.
}
wp_letp.
refine_letp (dK K (cmsubst (<[x:=of_val vc1]> (<[y:=of_val vc2]> (subst2cl' S))) eb)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
rewrite -heap_lang.substitution.msubst_insert_2.
rewrite -delete_insert_ne //.
rewrite -heap_lang.substitution.msubst_insert_2.
rewrite -chan_lang.substitution.msubst_insert_2.
rewrite -delete_insert_ne //.
rewrite -chan_lang.substitution.msubst_insert_2.
rewrite insert_commute //.
rewrite {1}(insert_commute _ y x) //.
specialize (IHhas_typ2 (<[x := {| styp := ty1;
hval := vh1;
cval := vc1 |}]>
(<[y := {| styp := ty2;
hval := vh2;
cval := vc2 |}]>S2))).
iPoseProof (IHhas_typ2 with "[Hv1 Hv2 HS2]") as "HS2'".
{ rewrite /subst2typ. subst. rewrite ?fmap_insert //. }
{ rewrite /subst2hl' /subst2hl ?fmap_insert //=.
apply ClosedSubst_insert; last solve_closed.
apply ClosedSubst_insert; last solve_closed.
eapply ClosedSubst_subseteq; eauto.
apply fmap_subseteq; auto.
}
{ rewrite /subst2cl' /subst2cl ?fmap_insert //=.
apply chan_lang.substitution.ClosedSubst_insert; last chan_lang.tactics.solve_closed.
apply chan_lang.substitution.ClosedSubst_insert; last chan_lang.tactics.solve_closed.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; auto.
}
{
iFrame "Hheap". iFrame "Hscheap".
rewrite subst2typ_insert2_bigM //=; auto.
iFrame "HS2".
iSplitL "Hv1"; by iApply val_equiv_expr.
}
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i K).
assert ((cmsubst
(subst2cl'
(<[x:={|
styp := ty1;
hval := heap_lang.of_val vh1;
cval := of_val vc1 |}]>
(<[y:={|
styp := ty2;
hval := heap_lang.of_val vh2;
cval := of_val vc2 |}]> S2))) eb) =
(cmsubst
((<[x:=of_val vc1]>(<[y:= of_val vc2]>(subst2cl' S2))))) eb) as Hsimpl.
{ clear. f_equal. rewrite /subst2cl' /subst2cl.
rewrite ?fmap_insert. auto. }
rewrite Hsimpl. clear Hsimpl.
assert ((hmsubst
(subst2hl'
(<[x:={|
styp := ty1;
hval := heap_lang.of_val vh1;
cval := of_val vc1 |}]>
(<[y:={|
styp := ty2;
hval := heap_lang.of_val vh2;
cval := of_val vc2 |}]> S2))) (c2h eb) =
(hmsubst
((<[x:=heap_lang.of_val vh1]>
(<[y:= heap_lang.of_val vh2]>(subst2hl' S2)))) (c2h eb)))) as Hsimpl.
{ clear. f_equal. rewrite /subst2hl' /subst2hl.
rewrite ?fmap_insert. auto. }
rewrite Hsimpl. clear Hsimpl.
erewrite (chan_lang.substitution.msubst_weaken_2 eb
(<[x:=of_val vc1]>(<[y:=of_val vc2]> (subst2cl' S2)))
(<[x:=of_val vc1]>(<[y:=of_val vc2]> (subst2cl' S)))); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
do 2 apply insert_mono. apply fmap_subseteq; eauto.
apply chan_lang.substitution.ClosedSubst_insert; eauto.
apply chan_lang.substitution.ClosedSubst_insert; eauto.
chan_lang.tactics.solve_closed.
chan_lang.tactics.solve_closed.
erewrite (substitution.msubst_weaken_2 (c2h eb)
(<[x:=heap_lang.of_val vh1]>(<[y:=heap_lang.of_val vh2]> (subst2hl' S2)))
(<[x:=heap_lang.of_val vh1]>(<[y:=heap_lang.of_val vh2]> (subst2hl' S)))); eauto;
last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite /subst2hl' /subst2hl ?dom_insert ?dom_fmap //.
}
do 2 apply insert_mono. apply fmap_subseteq; eauto.
apply ClosedSubst_insert; eauto.
apply ClosedSubst_insert; eauto.
heap_lang.tactics.solve_closed.
heap_lang.tactics.solve_closed.
iApply "HS2'".
done.
apply chan_lang.substitution.ClosedSubst_insert; eauto.
chan_lang.tactics.solve_closed.
apply chan_lang.substitution.ClosedSubst_delete; eauto.
apply heap_lang.substitution.ClosedSubst_insert; eauto.
heap_lang.tactics.solve_closed.
apply heap_lang.substitution.ClosedSubst_delete; eauto.
rewrite /is_Some. eexists. eauto.
rewrite /is_Some. eexists. eauto.
auto.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
erewrite <-(chan_lang.substitution.msubst_weaken_2 e1
(subst2cl' S1)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(chan_lang.substitution.msubst_weaken_2 e2
(subst2cl' S2)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e1)
(subst2hl' S1)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e2)
(subst2hl' S2)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
assert (chan_lang.Closed [] (cmsubst (subst2cl' S1) e1)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (chan_lang.Closed [] (cmsubst (subst2cl' S2) e2)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S1) (c2h e1))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S2) (c2h e2))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
idtac.
wp_focus (hmsubst S2 (c2h e2)).
refine_focus (cmsubst S2 e2).
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_seq. refine_seq (dK K (cmsubst S1 e1)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
iExists vc'. iFrame "Hown". auto.
- intros; iIntros "(#?&#?&HS)". simpl.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_apply wp_fork.
refine_fork (dK K (chan_lang.Lit chan_lang.LitUnit)) i' as "Hown'".
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
iSplitL "Hown".
{ iExists (chan_lang.LitV chan_lang.LitUnit).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
}
iPoseProof (IHhas_typ S with "[HS]") as "HS'"; try assumption.
iFrame. { iSplitL; auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS'" $! i' [] with "Hown'").
iApply wp_wand_l; iFrame "HS'".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc) "(?&?)".
rewrite /dK //= chan_lang.to_of_val.
refine_stopped.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
assert (Hcloc: chan_lang.Closed [x] (cmsubst (delete x (subst2cl' S)) e)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
{ apply chan_lang.substitution.ClosedSubst_delete. eauto. }
intros x' ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
- intros. subst. left. set_solver+.
- intros Hneq; right.
apply elem_of_dom.
move: Helem.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (Hcloh: heap_lang.Closed [x] (hmsubst (delete x (subst2hl' S)) (c2h e))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
{ apply ClosedSubst_delete. eauto. }
intros x' ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
- intros. subst. left. set_solver+.
- intros Hneq; right.
apply elem_of_dom.
move: Helem.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (Hclo1: heap_lang.Closed [] (heap_lang.derived.Lam x (hmsubst (delete x (subst2hl' S))
(c2h e)))).
{ rewrite //=. }
assert (Hclo2: chan_lang.Closed [] (chan_lang.derived.Lam x (cmsubst (delete x (subst2cl' S))
(e)))).
{ rewrite //=. }
assert (heap_lang.to_val ((heap_lang.derived.Lam x (hmsubst (delete x (subst2hl' S))
(c2h e))))
= Some (heap_lang.derived.LamV x (hmsubst (delete x (subst2hl' S))
(c2h e)))).
{ rewrite //=. case_decide; eauto.
- repeat f_equal. apply proof_irrel.
- exfalso; eauto. }
iApply wp_value; eauto.
iExists (LamV (BNamed x) (cmsubst (delete x (subst2cl' S)) e)).
iFrame "Hown".
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iExists x. iExists (hmsubst (delete x (subst2hl' S)) (c2h e)).
iExists Hcloh.
iExists x. iExists (cmsubst (delete x (subst2cl' S)) (e)).
iExists Hcloc.
iSplitR; first auto.
iSplitR; first auto.
iIntros (vh vc). iIntros "@".
iIntros "Hpre".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i' K'). iIntros "@". iIntros "Hown".
pose (S' := (<[x := {| styp := ty1;
hval := heap_lang.of_val vh;
cval := chan_lang.of_val vc|}]>(delete x S))).
specialize (IHhas_typ S').
rewrite /S' in IHhas_typ ×.
iPoseProof (IHhas_typ with "[HS Hpre]") as "HS'".
{ subst. rewrite /subst2typ ?fmap_insert //=.
rewrite fmap_delete insert_delete //. }
{ rewrite /subst2hl' /subst2hl fmap_insert //=.
apply ClosedSubst_insert; auto.
rewrite fmap_delete.
apply ClosedSubst_delete; auto.
solve_closed. }
{ rewrite /subst2cl' /subst2cl fmap_insert //=.
apply chan_lang.substitution.ClosedSubst_insert; auto.
rewrite fmap_delete.
apply chan_lang.substitution.ClosedSubst_delete; auto.
chan_lang.tactics.solve_closed. }
{
rewrite big_sepM_insert //=.
iFrame. iFrame "Hheap". iFrame "Hscheap".
iSplitL "Hpre".
- by iApply val_equiv_expr.
- case (decide (is_Some (S !! x))).
× intros (P&Heq). rewrite big_sepM_delete.
iDestruct "HS" as "(?&?)".
iFrame; eauto. apply Heq.
× intros Hnone. assert (S = delete x S) as Heq.
{ rewrite delete_notin; eauto. apply eq_None_not_Some; eauto. }
rewrite -Heq. eauto.
- apply lookup_delete_subst_ctx_1.
}
idtac.
rewrite /expr_equiv /expr_rel_lift.
wp_let. refine_let (dK K' (cmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) e)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
rewrite -msubst_insert_1.
rewrite -chan_lang.substitution.msubst_insert_1.
assert ((cmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) e) =
(cmsubst (<[x:=chan_lang.of_val vc]> (delete x (subst2cl' S))) e)) as Heqc.
{ f_equal. rewrite /subst2cl' /subst2cl. rewrite ?fmap_insert //=.
rewrite fmap_delete //. }
assert ((hmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) (c2h e)) =
(hmsubst (<[x:=heap_lang.of_val vh]> (delete x (subst2hl' S))) (c2h e))) as Heqh.
{ f_equal. rewrite /subst2hl' /subst2hl. rewrite ?fmap_insert //=.
rewrite fmap_delete //. }
rewrite Heqc Heqh.
iSpecialize ("HS'" $! i' K' with "Hown").
iApply wp_wand_l. iFrame "HS'".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc') ("Hpre'").
iExists vc'.
rewrite val_equiv_fix_unfold'.
auto.
apply chan_lang.substitution.ClosedSubst_delete. eauto.
eapply lookup_delete_subst_ctx_2.
apply heap_lang.substitution.ClosedSubst_delete. eauto.
eapply lookup_delete_subst_ctx_3.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
idtac.
erewrite <-(chan_lang.substitution.msubst_weaken_2 e1
(subst2cl' S1)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(chan_lang.substitution.msubst_weaken_2 e2
(subst2cl' S2)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e1)
(subst2hl' S1)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e2)
(subst2hl' S2)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
assert (chan_lang.Closed [] (cmsubst (subst2cl' S1) e1)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (chan_lang.Closed [] (cmsubst (subst2cl' S2) e2)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S1) (c2h e1))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S2) (c2h e2))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
wp_focus (hmsubst S1 (c2h e1)).
refine_focus (cmsubst S1 e1).
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_focus (hmsubst S2 (c2h e2)).
refine_focus (cmsubst S2 e2).
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_rel_lift.
iDestruct "Hvequiv" as (??????) "(%&%&Hvequiv)".
iSpecialize ("Hvequiv" $! vh' vc' with "[Hvequiv']"); auto.
iSpecialize ("Hvequiv" $! i K with "Hown").
iApply wp_wand_l. iFrame "Hvequiv".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc'') "Hpre'".
iExists vc''.
rewrite ?val_equiv_fix_unfold' //=.
- intros S Herase HcloSh HcloSc.
iIntros "(#Hheap&#Hscheap&_)".
rewrite //=.
assert (hmsubst S alloc = alloc) as →.
{ apply msubst_closed. rewrite /alloc. solve_closed. }
assert (cmsubst S (newch)%C = (newch)%C) as →.
{ apply chan_lang.substitution.msubst_closed. chan_lang.tactics.solve_closed. }
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
iPoseProof (alloc_spec protN _ _ _ p i K (dK K (newch)%C)
(dK K (chan_lang.Lit (LitLoc 1%positive cleft))) with "[Hown]")
as "Hwp".
{ rewrite /dK /dinit /Kd. rewrite //=.
specialize (fill_not_val K (newch)%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone. omega. auto.
}
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ iFrame "Hown". iFrame "Hheap". iFrame "Hscheap".
repeat iSplit; iPureIntro; eauto with ndisj. }
iApply wp_wand_l. iFrame "Hwp".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (l c) "?".
iExists (chan_lang.PairV (chan_lang.LitV $ chan_lang.LitLoc c cleft)
(chan_lang.LitV $ chan_lang.LitLoc c cright)).
iDestruct "Hpre" as "(%&Hleft&Hright&Hown)".
assert (dK K $ chan_lang.PairV
(chan_lang.LitV $ chan_lang.LitLoc c cleft)
(chan_lang.LitV $ chan_lang.LitLoc c cright)
=
dK K $ (chan_lang.Lit $ chan_lang.LitLoc 1%positive cleft)) as <-.
{ eapply fill_val_dK; eauto. }
iFrame "Hown".
iIntros "@". rewrite val_equiv_fix_unfold' //=.
iExists (#l)%V. iExists (#l)%V.
iExists (chan_lang.LitV $ chan_lang.LitLoc c cleft)%V.
iExists (chan_lang.LitV $ chan_lang.LitLoc c cright)%V.
iSplitR; first auto.
iSplitR; first auto.
iSplitL "Hleft".
× iExists l. iExists c. iExists cleft.
iSplitR; first auto.
iSplitR; first auto.
iAssumption.
× iExists l. iExists c. iExists cright.
iSplitR; first auto.
iSplitR; first auto.
iAssumption.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
erewrite <-(chan_lang.substitution.msubst_weaken_2 e
(subst2cl' S1)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(chan_lang.substitution.msubst_weaken_2 ev
(subst2cl' S2)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
rewrite msubst_unfold // //=.
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e)
(subst2hl' S1)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h ev)
(subst2hl' S2)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
assert (chan_lang.Closed [] (cmsubst (subst2cl' S1) e)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (chan_lang.Closed [] (cmsubst (subst2cl' S2) ev)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S1) (c2h e))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S2) (c2h ev))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
wp_focus (hmsubst S1 (c2h e)).
refine_focus (cmsubst S1 e).
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_focus (hmsubst S2 (c2h ev)).
refine_focus (cmsubst S2 ev).
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_rel_lift.
rewrite affine_elim.
assert(
(letp: "l" "v" := (vh, vh')
in hmsubst (delete "l" (delete "v" (subst2hl' S)))
(let: "lnew" := ref SOME #()
in "l" <- heap_lang.InjL ("lnew", "v")
;; "lnew"))%E
= hmsubst S (send vh vh')) as →.
{
rewrite /send.
symmetry.
rewrite msubst_unfold // //=.
rewrite msubst_unfold // //=.
assert (hmsubst S vh = vh) as →.
{ apply msubst_closed. solve_closed. }
assert (hmsubst S vh' = vh') as →.
{ apply msubst_closed. solve_closed. }
trivial.
}
assert (hmsubst S (send vh vh') = send vh vh') as →.
{ apply msubst_closed. rewrite /send. solve_closed. }
iDestruct "Hvequiv" as (l c s) "(%&%&Hmaps)"; subst.
iPoseProof (send_spec protN _ _
(CofeMor (λ ty, (CofeMor (λ vh,
CofeMor (λ vc, ▷ (val_equiv ty vh vc))
))))%I
ty vc' vc' vh' vh' _ c s l i K
(dK K (Lit $ LitLoc c s <- vc'))%C
(dK K (LitV $ LitLoc c s)%C)) as "Hsend".
{ rewrite /dK /dinit /Kd //=; split.
- specialize (fill_not_val K (#(LitLoc c s) <- vc')%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone. omega. auto.
- case_match; omega.
}
{ rewrite /dK /dinit /Kd //=. case_match; omega. }
rewrite chan_lang.to_of_val //=.
rewrite heap_lang.to_of_val //=.
iSpecialize ("Hsend" with "[Hmaps Hvequiv' Hown]").
{ iFrame "Hown". iFrame "Hmaps".
simpl. iIntros "@". iNext.
rewrite val_equiv_fix_unfold'. auto.
}
iApply wp_wand_l. iFrame "Hsend".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (l') "(%&Hprot&Hown)".
iExists (LitV $ LitLoc c s)%C.
iFrame "Hown".
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iExists l'. iExists c. iExists s.
iSplitR; first auto.
iSplitR; first auto.
done.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
assert (chan_lang.Closed [] (cmsubst (subst2cl' S) e)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S) (c2h e))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
idtac.
assert (hmsubst S recv = recv) as →.
{ apply msubst_closed. rewrite /recv. solve_closed. }
rewrite /recv.
wp_focus (hmsubst S (c2h e)).
refine_focus (cmsubst S e).
iPoseProof (IHhas_typ S with "[HS]") as "HS'"; try assumption.
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
rewrite /recv.
assert
(((rec: "recv" "l"
:= match: ! "l" with InjL "x" ⇒ "x" | InjR "_" ⇒
("recv": heap_lang.expr) "l" end)%V vh)%E
= recv vh) as Heq.
{ rewrite /recv. auto. }
rewrite Heq.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_rel_lift.
rewrite affine_elim.
iDestruct "Hvequiv" as (l c s) "(%&%&Hmaps)"; subst.
iPoseProof (recv_spec protN _ _
(CofeMor (λ ty, (CofeMor (λ vh,
CofeMor (λ vc, ▷ (val_equiv ty vh vc))
))))%I
ty
(val_equiv_pre val_equiv ty)
_ c s l i K
(dK K (! (LitV $ LitLoc c s)))%C
(dK K (LitV $ LitLoc c s)%C)) as "Hrecv".
{ rewrite /dK /dinit /Kd //=; split.
- specialize (fill_not_val K (! (LitV $ LitLoc c s))%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone. omega. auto.
- case_match; omega.
}
{ rewrite /dK /dinit /Kd //=. case_match; omega. }
{ intros. simpl. rewrite val_equiv_fix_unfold'. auto. }
iSpecialize ("Hrecv" with "[Hmaps Hown]").
{ iFrame "Hown". iFrame "Hmaps". auto. }
iApply wp_wand_l. iFrame "Hrecv".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (l' vh' vc') "(%&Hprot&Hvequiv&Hown)".
iExists (PairV (LitV $ LitLoc c s) vc')%C.
assert (dK K $ chan_lang.PairV
(chan_lang.LitV $ chan_lang.LitLoc c s)
vc'
=
dK K $ (chan_lang.LitV $ chan_lang.LitLoc c s)) as <-.
{ eapply fill_val_dK; eauto. eauto.
rewrite //=. rewrite to_of_val. eauto.
}
iFrame "Hown".
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iExists (#l')%V. iExists vh'.
iExists (LitV $ LitLoc c s)%C. iExists vc'.
iSplitR; first auto.
iSplitR; first auto.
iFrame "Hvequiv".
iExists l'. iExists c. iExists s.
iSplitR; first auto.
iSplitR; first auto.
idtac.
auto.
- intros. rewrite IHhas_typ; eauto.
rewrite /expr_equiv /expr_rel_lift.
iIntros "Hpre". iIntros (i K) "@ Hown".
iSpecialize ("Hpre" $! i K with "Hown").
iApply wp_wand_l. iFrame "Hpre".
iIntros "@". iIntros (v) "Hpre".
idtac.
iDestruct "Hpre" as (vc) "(Hve&Hown)".
iExists vc. iFrame "Hown".
iIntros "@".
rewrite val_equiv_fix_unfold'.
rewrite val_equiv_fix_unfold'.
rewrite //=.
iDestruct "Hve" as (lh lc s) "(%&%&?)".
iExists lh. iExists lc. iExists s.
iSplitR; first auto.
iSplitR; first auto.
idtac.
rewrite H0.
auto.
Grab Existential Variables.
rewrite /Kd. compute. auto.
rewrite /Kd. compute. auto.
rewrite /Kd. compute. auto.
Qed.
End lr.
Section closed.
Definition Σ : gFunctors := #[ heapGF ; scheapGF ; protGF ;
refineGF (delayed_lang (chan_lang) Kd dinit)
(S Kd × (Kd + 3))].
Lemma Σ_len: projT1 Σ = 5%nat.
Proof. auto. Qed.
Ltac gid_destruct g1 g2 :=
match type of g1 with
| fin ?T ⇒
refine
(match g1 as g' in fin n return ∀ (pf: n = T),
eq_rect n fin g' T pf = g1 →
_ with
| Fin.F1 _ ⇒ _
| FS _ g2 ⇒ _
end Init.Logic.eq_refl Init.Logic.eq_refl);
let pf := fresh "pf" in
intros pf ?; inversion pf; subst; simpl;
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec; clear pf
| _ ⇒ fail g1 "is not a fin."
end.
Tactic Notation "gid_destruct" constr(g1) "as" simple_intropattern(g2) :=
gid_destruct g1 g2.
Instance inGF_refineG : refineG heap_lang Σ (delayed_lang (chan_lang) Kd dinit) (S Kd × (Kd + 3)).
Proof. eapply inGF_refineG. intros g A.
rewrite /gid in g ×.
assert (fin (projT1 Σ) = fin 5) as Hlen.
{ rewrite Σ_len. auto. }
rewrite /projT2 /Σ.
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ simpl in ×. intros (?&_). exfalso; eauto. }
inversion g.
Grab Existential Variables.
rewrite /Kd. auto.
Qed.
Instance inGF_scheapG: scheapG heap_lang Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 1%positive. Qed.
Instance inGF_heapG: heapG Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 2%positive. Qed.
Instance inGF_protG: protG Σ.
Proof. eauto. split; try apply _; eauto. Qed.
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Local Notation hexprC := (leibnizC (heap_lang.expr)).
Local Notation cexprC := (leibnizC (chan_lang.expr)).
Local Notation hvalC := (leibnizC (heap_lang.val)).
Local Notation cvalC := (leibnizC (chan_lang.val)).
Fixpoint c2h_refine (v: heap_lang.val) (v': chan_lang.val) :=
match v, v' with
| heap_lang.LitV (heap_lang.LitBool b),
chan_lang.LitV (chan_lang.LitBool b') ⇒
b = b'
| heap_lang.LitV (heap_lang.LitInt n),
chan_lang.LitV (chan_lang.LitInt n') ⇒
n = n'
| heap_lang.LitV (heap_lang.LitUnit),
chan_lang.LitV (chan_lang.LitUnit) ⇒
True
| heap_lang.LitV (heap_lang.LitLoc _),
chan_lang.LitV (chan_lang.LitLoc _ _) ⇒
True
| heap_lang.RecV _ _ _ _,
chan_lang.RecV _ _ _ _ ⇒
True
| heap_lang.PairV vh1 vh2,
chan_lang.PairV vc1 vc2⇒
c2h_refine vh1 vc1 ∧ c2h_refine vh2 vc2
| _, _ ⇒ False
end.
Import uPred.
Existing Instance prot_mapsto_affine.
Lemma val_equiv_c2h_refine H1 H2 H3 H4 ty vh vc:
(@val_equiv Σ H1 H2 H3 H4) ty vh vc ⊢ ⧆ ■ c2h_refine vh vc.
Proof.
rewrite val_equiv_fix_unfold'.
revert vh vc.
induction ty; simpl; intros.
- iIntros "HVC".
iDestruct "HVC" as (vh1 vh2 vc1 vc2) "(%&%&Hv1&Hv2)".
subst.
iPoseProof (IHty1 with "Hv1") as "H1". iDestruct "H1" as "%".
iPoseProof (IHty2 with "Hv2") as "H2". iDestruct "H2" as "%".
iPureIntro. split; auto.
- iIntros "HVC".
iDestruct "HVC" as (xh eh1 Hcloh xc ec1 Hcloc) "(%&%&?)".
subst. iPureIntro. rewrite //=.
- iIntros "(%&%)". subst. iPureIntro. rewrite //=.
- iIntros "HVC". iDestruct "HVC" as (n') "(%&%)".
subst. iPureIntro. rewrite //=.
- iIntros "HVC". iDestruct "HVC" as (b') "(%&%)".
subst. iPureIntro. rewrite //=.
- iIntros. iApply False_elim. done.
- iIntros "HVC". iDestruct "HVC" as (lh lc s) "(%&%&_)".
subst. iPureIntro. rewrite //=.
Qed.
Lemma soundness ty eh ec:
(∀ H1 H2 H3 H4 H5, @ctx_expr_equiv H1 H2 H3 H4 H5 ∅ ty eh ec) →
safe_refine (c2h_refine) eh ∅ ec ∅.
Proof.
intros Hpre.
case_eq (chan_lang.to_val ec).
- intros Hv Heqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := 0%nat).
× eapply head_step_det_prim_det, chan_lang.head_step_det.
× apply chan_prim_dec.
×
iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (scheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Heqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown')".
iExists vc.
rewrite {1}/dK //= chan_lang.to_of_val.
iFrame "Hown'".
rewrite affine_elim.
iApply (val_equiv_c2h_refine _ _ _ _ ty vh vc).
iAssumption.
- intros Hneqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := dinit%nat).
× eapply head_step_det_prim_det, chan_lang.head_step_det.
× apply chan_prim_dec.
× iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (scheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Hneqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown1)".
iExists vc.
rewrite {1}/dK //= chan_lang.to_of_val.
iFrame.
rewrite affine_elim.
iApply (val_equiv_c2h_refine _ _ _ _ ty vh vc).
iAssumption.
Qed.
End closed.
From iris.chan_lang Require Export lang.
From iris.chan2heap Require Export refine_protocol.
From iris.chan_lang Require Export simple_types substitution.
From iris.heap_lang Require Import lang heap proofmode substitution.
Section lr.
Definition Kd := 200%nat.
Definition dinit : nat := 100%nat.
Definition dK K ec :=
match chan_lang.to_val (ectx_language.fill K ec) with
| None ⇒ dinit
| Some _ ⇒ O
end.
Context `{!protG Σ}.
Context `{!refineG heap_lang Σ (delayed_lang (chan_lang) Kd dinit) (S Kd × (Kd + 3))}.
Context `{!scheapG heap_lang Σ}.
Context `{!heap.heapG Σ}.
Definition protN : namespace := nroot.@ "prot".
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Local Notation hexprC := (leibnizC (heap_lang.expr)).
Local Notation cexprC := (leibnizC (chan_lang.expr)).
Local Notation hvalC := (leibnizC (heap_lang.val)).
Local Notation cvalC := (leibnizC (chan_lang.val)).
From iris.proofmode Require Import coq_tactics.
Import uPred.
Definition expr_rel_lift (vrel: hvalC -n> cvalC -n> iProp) eh ec : iProp :=
(∀ i K, ⧆ (ownT i ec K (dK K ec)
-★ WP eh {{ vh, ∃ vc, ⧆ vrel vh vc
★ ownT i (chan_lang.of_val vc) K (dK K vc)}}))%I.
Import uPred.
Lemma expr_rel_lift_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) expr_rel_lift.
Proof.
intros vr1 vr2 Hr ?? → ?? →.
rewrite /expr_rel_lift. setoid_rewrite Hr. eauto.
Qed.
Lemma expr_rel_aff_pres (vrel: hvalC -n> cvalC -n> iProp): (∀ v V, AffineP (vrel v V)) →
∀ e E, AffineP (expr_rel_lift vrel e E).
Proof.
rewrite /AffineP. intros.
rewrite /expr_rel_lift.
apply affine_intro. apply _. auto.
Qed.
Definition lift2 (f: hvalC → cvalC → iProp) : hvalC -n> cvalC -n> iProp :=
CofeMor(λ x, CofeMor (λ y, f x y)).
Definition lift3 (f: typC → hvalC → cvalC → iProp) : typC -n> hvalC -n> cvalC -n> iProp :=
CofeMor(λ x, CofeMor(λ y, CofeMor (λ z, f x y z))).
From iris.heap_lang Require Import notation.
Fixpoint val_equiv_pre
(ve: typC -n> hvalC -n> cvalC -n> iProp)
(ty: typ) (vh: heap_lang.val) (vc: chan_lang.val)
: iProp :=
match ty with
| Int ⇒ (∃ (n: Z), ⧆(vh = #n) ★ ⧆(vc = chan_lang.LitV (chan_lang.LitInt n)))%I
| Bool ⇒ (∃ (b: bool), ⧆(vh = #b) ★ ⧆(vc = chan_lang.LitV (chan_lang.LitBool b)))%I
| Unit ⇒ (⧆(vh = #()) ★ ⧆(vc = chan_lang.LitV chan_lang.LitUnit))%I
| Tensor ty1 ty2 ⇒
(∃ (vh1 vh2: heap_lang.val) (vc1 vc2: chan_lang.val),
⧆(vh = (vh1, vh2)%V) ★
⧆(vc = chan_lang.PairV vc1 vc2) ★
(val_equiv_pre ve ty1 vh1 vc1) ★
(val_equiv_pre ve ty2 vh2 vc2))%I
| Lolli ty1 ty2 ⇒
(∃ x (eh1: heap_lang.expr) pfh y (ec1: chan_lang.expr) pfc,
⧆(vh = @heap_lang.RecV BAnon x%bind eh1 pfh) ★
⧆(vc = @chan_lang.RecV BAnon y%bind ec1 pfc) ★
(∀ vh1 vc1, ⧆(val_equiv_pre ve ty1 vh1 vc1
-★ expr_rel_lift (lift2 (val_equiv_pre ve ty2))
(App vh vh1) (chan_lang.App vc vc1))))%I
| Styp p ⇒ (∃ (lh: heap_lang.loc) (lc: chan_lang.loc) (s: side),
⧆(vh = #lh) ★
⧆(vc = chan_lang.LitV $ chan_lang.LitLoc lc s) ★
prot_mapsto protN typ
(CofeMor (λ ty, (CofeMor (λ vh, CofeMor (λ vc, ▷ (ve ty vh vc))))))
(lc, s) lh
p)%I
| _ ⇒ False%I
end.
Definition val_equiv_preC (ve: typC -n> hvalC -n> cvalC -n> iProp):
typC -n> hvalC -n> cvalC -n> iProp := lift3 (val_equiv_pre ve).
Instance val_equiv_pre_contractive : Contractive (val_equiv_preC).
Proof.
intros n ve1 ve2 Hvd ty vh vc. simpl.
revert ve1 ve2 Hvd ty vh vc.
induction ty; intros; rewrite /val_equiv_pre; fold val_equiv_pre.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto;
eapply later_contractive; intros; eapply Hvd; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
repeat apply forall_ne=>?.
apply affine_ne. apply wand_ne; first eauto.
eapply expr_rel_lift_ne; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
- eauto.
- apply exist_ne=>?; apply sep_ne; eauto.
- eauto.
- repeat apply exist_ne=>?.
apply sep_ne; first eauto.
apply sep_ne; first eauto.
apply prot_mapsto_ne; auto.
intros ???. apply later_contractive=>??.
rewrite Hvd; eauto.
Qed.
Definition val_equiv: typC -n> hvalC -n> cvalC -n> iProp := fixpoint val_equiv_preC.
Lemma val_equiv_fix_unfold ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_preC val_equiv ty vh vc.
Proof. by rewrite /val_equiv -fixpoint_unfold. Qed.
Lemma val_equiv_fix_unfold' ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_pre val_equiv ty vh vc.
Proof. rewrite val_equiv_fix_unfold. auto. Qed.
Instance val_equiv_affine ty eh ec: AffineP (val_equiv ty eh ec).
Proof.
rewrite /AffineP val_equiv_fix_unfold'; revert eh ec; induction ty⇒eh ec; simpl.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply sep_affine; rewrite /AffineP; eauto.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply affine_intro; first apply _.
repeat (rewrite ?affine_forall; apply forall_mono=>?).
apply affine_mono; eauto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- rewrite affine_exist; apply exist_mono=>?.
rewrite affine_exist; apply exist_mono=>?.
rewrite affine_exist; apply exist_mono⇒s.
repeat (apply sep_affine; first apply _).
rewrite /prot_mapsto.
rewrite /prot_ctx. destruct s; simpl; apply _.
Qed.
Instance val_equiv_pre_affine ty eh ec: AffineP (val_equiv_pre val_equiv ty eh ec).
Proof. rewrite /AffineP. rewrite -val_equiv_fix_unfold'. apply val_equiv_affine. Qed.
Notation csubst_map := chan_lang.substitution.subst_map.
Notation hsubst_map := heap_lang.substitution.subst_map.
Notation cmsubst := chan_lang.substitution.msubst.
Notation hmsubst := heap_lang.substitution.msubst.
Definition expr_equiv ty := expr_rel_lift (val_equiv ty).
Instance expr_equiv_affine ty eh ec: AffineP (expr_equiv ty eh ec).
Proof. eapply expr_rel_aff_pres=>??; apply _. Qed.
Record subst_tuple :=
stuple { styp : typ ; hval : heap_lang.expr; cval : chan_lang.expr }.
Definition subst_ctx := gmap string subst_tuple.
Definition subst2typ (S: subst_ctx) : typ_ctx := styp <$> S.
Definition subst2cl (S: subst_ctx) : csubst_map := cval <$> S.
Definition subst2hl (S: subst_ctx) : hsubst_map := hval <$> S.
Implicit Types S : subst_ctx.
Coercion subst2hl' := subst2hl.
Coercion subst2cl' := subst2cl.
Coercion subst2typ' := subst2typ.
Definition ctx_expr_equiv (Γ: typ_ctx) (ty: typ) (eh: heap_lang.expr) (ec: chan_lang.expr) : Prop :=
∀ (S: subst_ctx) (Herase: subst2typ S = Γ),
ClosedSubst [] S →
chan_lang.substitution.ClosedSubst [] S →
heap_ctx ★ scheap_ctx ★ ([★ map] x ↦ P ∈ S, (expr_equiv (styp P) (hval P) (cval P)))
⊢ expr_equiv ty (hmsubst S eh)
(cmsubst S ec).
Instance ctx_prop_affine S:
AffineP ([★ map] x↦P ∈S, (expr_equiv (styp P) (hval P) (cval P)))%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using expr_equiv_affine.
Qed.
Lemma val_equiv_expr ty vh vc:
(val_equiv_pre val_equiv ty vh vc ⊢ expr_equiv ty vh vc)%I.
Proof.
rewrite /expr_equiv /expr_rel_lift.
iIntros "Hve". iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists vc. iFrame "Hown".
iIntros "@". by rewrite val_equiv_fix_unfold'.
Qed.
Lemma expr_equiv_empty ty eh ec (pf: ctx_expr_equiv ∅ ty eh ec):
heap_ctx ★ scheap_ctx ⊢ (expr_rel_lift (val_equiv ty) eh ec).
Proof.
rewrite /expr_equiv in pf.
specialize (pf ∅). rewrite /subst2typ fmap_empty in pf.
efeed pose proof pf as pf'; eauto; try done.
rewrite big_sepM_empty right_id in pf' ×.
intros ->; auto.
Qed.
Definition bool_refine (v: heap_lang.val) (v': chan_lang.val) :=
match v, v' with
| LitV (LitBool b), chan_lang.LitV (chan_lang.LitBool b') ⇒
b = b'
| _, _ ⇒ False
end.
Lemma chan_prim_dec: ∀ (e: chan_lang.expr) σ,
{ t | prim_step (e: chan_lang.expr) σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}.
Proof.
intros. edestruct (ClassicalEpsilon.excluded_middle_informative
((∃ (e' : language.expr (ectx_lang (chan_lang.expr)))
(σ' : language.state (ectx_lang (chan_lang.expr)))
(ef' : option (language.expr (ectx_lang (chan_lang.expr)))),
language.prim_step e σ e' σ' ef'))).
× apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (e'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (σ'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (ef'&e0).
left. ∃ (e', σ', ef'). eauto.
× right. auto.
Qed.
From iris.heap_lang Require Import proofmode notation.
Lemma subst2typ_inv Γ S x ty:
Γ !! x = Some ty →
subst2typ S = Γ →
∃ eh ec, S !! x = Some {| styp := ty; hval := eh; cval := ec |}.
Proof.
rewrite /subst2typ. intros Hlook <-.
move:Hlook. rewrite lookup_fmap. case_eq (S !! x).
- intros st Heq. rewrite ?Heq.
inversion 1. destruct st; eauto.
- intros Hnone. rewrite ?Hnone.
inversion 1.
Qed.
Lemma NoDup_filter_fmap {A B: Type} (f: A → B) P pf (l: list A):
NoDup (f <$> l) → NoDup (f <$> (@filter _ _ _ P pf l)).
Proof.
induction l. eauto.
simpl. inversion 1. subst.
rewrite /filter /list_filter. case_decide.
- rewrite //=. econstructor; eauto.
intros (?&Heq&Helem)%elem_of_list_fmap_2.
match goal with [ H: ¬ _ |- _] ⇒ apply H end.
rewrite Heq. apply elem_of_list_fmap_1.
rewrite elem_of_list_filter in Helem ×. intros (?&?); auto.
- auto.
Qed.
Lemma subst_ctx_subseteq S Γ Γ1 Γ2:
Γ1 ⊆ Γ →
Γ2 ⊆ Γ →
dom (gset string) Γ1 ∩ dom (gset string) Γ2 ≡ ∅ →
subst2typ S = Γ →
∃ S1 S2,
S1 ⊆ S ∧
S2 ⊆ S ∧
dom (gset string) S1 ∩ dom (gset string) S2 ≡ ∅ ∧
subst2typ S1 = Γ1 ∧
subst2typ S2 = Γ2.
Proof.
intros Hsub1 Hsub2 Hdom Herase.
set (l := map_to_list S).
set (l1 := filter (λ p, p.1 ∈ dom (gset string) Γ1) l).
set (l2 := filter (λ p, p.1 ∈ dom (gset string) Γ2) l).
∃ (map_of_list l1).
∃ (map_of_list l2).
split_and!.
- rewrite /l1 /l. apply map_subseteq_spec⇒x P.
intros Helem%elem_of_map_of_list_2.
by apply elem_of_list_filter in Helem as (?&?%elem_of_map_to_list).
- rewrite /l2 /l. apply map_subseteq_spec⇒x P.
intros Helem%elem_of_map_of_list_2.
by apply elem_of_list_filter in Helem as (?&?%elem_of_map_to_list).
- clear -Hdom. set_unfold. rewrite /l1 /l2 /l⇒x.
rewrite ?elem_of_dom.
rewrite /is_Some.
intros ((P1&Helem1)&(P2&Helem2)).
apply elem_of_map_of_list_2, elem_of_list_filter in Helem1 as (Hd1&_).
apply elem_of_map_of_list_2, elem_of_list_filter in Helem2 as (Hd2&_).
eapply Hdom. split; eauto.
- apply map_eq_iff⇒x. rewrite /subst2typ lookup_fmap.
case_eq (Γ1 !! x).
× intros ty Hlook1.
assert (Γ !! x = Some ty) as Hlook.
{ eapply (map_subseteq_spec Γ1); eauto. }
eapply subst2typ_inv in Hlook as (eh&ec&?); eauto.
efeed pose proof (elem_of_map_of_list_1 l1 x {| styp := ty; hval := eh; cval := ec|})
as Hlook'.
{ rewrite /l1 /l. eapply NoDup_filter_fmap. apply NoDup_fst_map_to_list. }
{ rewrite /l1 /l. apply elem_of_list_filter. split.
- rewrite elem_of_dom; eauto.
- by rewrite elem_of_map_to_list. }
rewrite Hlook'. auto.
× intros Hnone.
rewrite Hnone.
rewrite not_elem_of_map_of_list_1; auto.
rewrite /l1.
intros ((?&P)&Heq&Helem)%elem_of_list_fmap_2.
apply elem_of_list_filter in Helem as (HelemΓ1&?).
rewrite -Heq elem_of_dom in HelemΓ1 ×.
rewrite Hnone. inversion 1. congruence.
- apply map_eq_iff⇒x. rewrite /subst2typ lookup_fmap.
case_eq (Γ2 !! x).
× intros ty Hlook1.
assert (Γ !! x = Some ty) as Hlook.
{ eapply (map_subseteq_spec Γ2); eauto. }
eapply subst2typ_inv in Hlook as (eh&ec&?); eauto.
efeed pose proof (elem_of_map_of_list_1 l2 x {| styp := ty; hval := eh; cval := ec|})
as Hlook'.
{ rewrite /l2 /l. eapply NoDup_filter_fmap. apply NoDup_fst_map_to_list. }
{ rewrite /l2 /l. apply elem_of_list_filter. split.
- rewrite elem_of_dom; eauto.
- by rewrite elem_of_map_to_list. }
rewrite Hlook'. auto.
× intros Hnone.
rewrite Hnone.
rewrite not_elem_of_map_of_list_1; auto.
rewrite /l2.
intros ((?&P)&Heq&Helem)%elem_of_list_fmap_2.
apply elem_of_list_filter in Helem as (HelemΓ1&?).
rewrite -Heq elem_of_dom in HelemΓ1 ×.
rewrite Hnone. inversion 1. congruence.
Qed.
Lemma fmap_subseteq {A B} (f: A → B) (S1 S2: gmap string A):
S1 ⊆ S2 → f <$> S1 ⊆ f <$> S2.
Proof.
rewrite ?map_subseteq_spec⇒ Hs1 i x.
rewrite ?lookup_fmap.
specialize (Hs1 i). destruct (S1 !! i).
- erewrite Hs1; eauto.
- inversion 1.
Qed.
From iris.chan_lang Require Export lang derived refine refine_heap refine_heap_proofmode protocol.
Lemma tac_refine_bind Δ Δ' k t e K K' P:
envs_lookup k Δ = Some (false, ownT t (fill K' e) K (dK K (fill K' e))) →
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') (dK (comp_ectx K K') e))) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
rewrite ownT_focus //= ?right_id. by rewrite wand_elim_r.
Qed.
Lemma tac_refine_unbind Δ Δ' k t e K K' P :
envs_lookup k Δ = Some (false, ownT t e (comp_ectx K K') (dK (comp_ectx K K') e)) →
envs_simple_replace k false (Esnoc Enil k (ownT t (fill K' e) K (dK K (fill K' e)))) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
by rewrite -ownT_fill //= ?right_id wand_elim_r.
Qed.
Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_bind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) constr(K') "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ j _ _ K K';
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ _ _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_focus" open_constr(efoc) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
chan_lang.tactics.reshape_expr e ltac:(fun K' e' ⇒
match e' with
| efoc ⇒ idtac K';
unify e' efoc;
refine_bind K' at j
end) || fail "refine_focus: cannot find" efoc "in" e
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_unfocus" :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (comp_ectx ?K0 ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (?K0 ++ ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
refine_unbind empty_ectx K at j; simpl_subst
| _ ⇒ fail "refine_unocus: could not find ownT"
end.
Instance: Params (@val_equiv_pre) 1.
Lemma ClosedSubst_subseteq_hsubst S1 S2 l:
ClosedSubst l S1 →
S2 ⊆ S1 →
ClosedSubst l S2.
Proof.
intros. eapply ClosedSubst_subseteq; eauto.
rewrite /subst2hl' /subst2hl. apply fmap_subseteq; auto.
Qed.
Lemma ClosedSubst_subseteq_csubst S1 S2 l:
chan_lang.substitution.ClosedSubst l S1 →
S2 ⊆ S1 →
chan_lang.substitution.ClosedSubst l S2.
Proof.
intros. eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
rewrite /subst2cl' /subst2cl. apply fmap_subseteq; auto.
Qed.
Lemma subst2typ_insert2_bigM x y s1 s2 (Φ: subst_tuple → iProp) S:
x ≠ y →
subst2typ S !! x = None →
subst2typ S !! y = None →
([★ map] z↦P ∈ <[x:=s1]>(<[y := s2]>S), Φ P)
⊣⊢ Φ s1 ★ Φ s2 ★ ([★ map] z↦P ∈ S, Φ P)%I.
Proof.
intros Hneq Hl1 Hl2.
rewrite big_sepM_insert; last first.
- rewrite lookup_insert_ne; auto.
× move:Hl1. rewrite /subst2typ lookup_fmap.
case_eq (S !! x).
** intros s Heq. rewrite Heq. inversion 1.
** intros s Heq. auto.
- rewrite big_sepM_insert; last first.
× move:Hl2. rewrite /subst2typ lookup_fmap.
case_eq (S !! y).
** intros s Heq. rewrite Heq. inversion 1.
** intros s Heq. auto.
× done.
Qed.
Lemma elem_of_dom_insert_mono {A A'} (x y: string) (s1: A) (s2: A')
(S1: gmap string A) (S2: gmap string A'):
(x ∈ dom (gset string) S1 → x ∈ dom (gset string) S2) →
(x ∈ dom (gset string) (<[y := s1]>S1) → x ∈ dom (gset string) (<[y := s2]>S2)).
Proof.
rewrite ?dom_insert. intros ? [Hy|HS2]%elem_of_union; apply elem_of_union.
- left. auto.
- right. auto.
Qed.
Lemma insert_mono {A} (x: string) (s: A)
(S1 S2: gmap string A):
S1 ⊆ S2 → <[x := s]>S1 ⊆ <[x := s]>S2.
Proof.
rewrite ?map_subseteq_spec. intros Hsub i s'.
case (decide(x = i)).
- intros →. rewrite ?lookup_insert; inversion 1. auto.
- intros Hneq. rewrite ?lookup_insert_ne //. apply Hsub.
Qed.
Lemma fill_val_dK K e1 e2:
is_Some (chan_lang.to_val e1) →
is_Some (chan_lang.to_val e2) →
dK K e1 = dK K e2.
Proof.
intros. rewrite /dK.
rewrite /ectx_language.fill //=.
do 2 case_match; auto.
- exfalso.
specialize (@ectxi_language.fill_val_2 chan_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (chan_lang.fill_item_val_2) K e1 e2);
eauto.
congruence.
- exfalso.
specialize (@ectxi_language.fill_val_2 chan_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (chan_lang.fill_item_val_2) K e2 e1);
eauto.
congruence.
Qed.
Lemma lookup_delete_subst_ctx_1 (S: subst_ctx) (x: string):
delete x S !! x = None.
Proof. apply lookup_delete. Qed.
Lemma lookup_delete_subst_ctx_2 (S: subst_ctx) (x: string):
delete x (subst2cl' S) !! x = None.
Proof. apply lookup_delete. Qed.
Lemma lookup_delete_subst_ctx_3 (S: subst_ctx) (x: string):
delete x (subst2hl' S) !! x = None.
Proof. apply lookup_delete. Qed.
Existing Instance prot_mapsto_affine.
Existing Instance prot_mapsto_proper.
Arguments heap_lang.of_val: simpl never.
Lemma fundamental Γ ty ec:
has_typ Γ ec ty →
ctx_expr_equiv Γ ty (c2h ec) ec.
Proof.
rewrite /ctx_expr_equiv.
intros has_typ.
induction has_typ .
- intros S Herase HcloSh HcloSc.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
eapply subst2typ_inv in Herase as (eh&ec&Hlook); eauto.
rewrite big_sepM_delete; eauto.
rewrite ?lookup_fmap ?Hlook //=.
iIntros "(?&?&?&_)". done.
- intros; iIntros "_". simpl.
rewrite /c2h msubst_msubst' // chan_lang.substitution.msubst_msubst' //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists (chan_lang.LitV (chan_lang.LitBool b)).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists b. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite /c2h msubst_msubst' // chan_lang.substitution.msubst_msubst' //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists (chan_lang.LitV (chan_lang.LitInt n)).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists n. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite /c2h msubst_msubst' // chan_lang.substitution.msubst_msubst' //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_value. iPvsIntro. iExists (chan_lang.LitV (chan_lang.LitUnit)).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_focus (msubst S (c2h e1)).
refine_focus (chan_lang.substitution.msubst S e1)%C.
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
erewrite (chan_lang.substitution.msubst_weaken_2 e1 S1 S); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
rewrite -Herase1. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
erewrite (heap_lang.substitution.msubst_weaken_2 (c2h e1) S1 S); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
rewrite -Herase1. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_focus (msubst S (c2h e2)).
refine_focus (chan_lang.substitution.msubst S e2)%C.
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
erewrite (chan_lang.substitution.msubst_weaken_2 e2 S2 S); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
rewrite -Herase2. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
erewrite (heap_lang.substitution.msubst_weaken_2 (c2h e2) S2 S); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
rewrite -Herase2. intros x Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
refine_unfocus.
wp_value. iPvsIntro. iExists (chan_lang.PairV vc vc').
iFrame.
rewrite ?val_equiv_fix_unfold; simpl.
iIntros "@". iExists vh, vh', vc, vc'.
iFrame. iSplitL; iPureIntro; done.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_focus (msubst S (c2h e)).
refine_focus (chan_lang.substitution.msubst S e)%C.
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
erewrite (chan_lang.substitution.msubst_weaken_2 e S1 S); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
rewrite -Herase1. intros x' Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
erewrite (heap_lang.substitution.msubst_weaken_2 (c2h e) S1 S); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
rewrite -Herase1. intros x' Hin'. apply Hin. move:Hin'. rewrite ?dom_fmap //. }
{ eauto using fmap_subseteq. }
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
subst.
rewrite val_equiv_fix_unfold'.
simpl. iDestruct "Hvequiv" as (vh1 vh2 vc1 vc2) "Hv'".
rewrite affine_elim. iDestruct "Hv'" as "(%&%&Hv1&Hv2)".
subst.
replace (heap_lang.of_val (vh1, vh2)%V) with
(heap_lang.of_val vh1, heap_lang.of_val vh2)%E; auto.
assert (heap_lang.Closed [x; y] (hmsubst (delete x (delete y (subst2hl' S))) (c2h eb))).
{ rewrite /heap_lang.Closed.
rewrite /subst2hl' /subst2hl ?fmap_delete.
eapply msubst_closing_inv_3.
{ apply ClosedSubst_delete; auto. }
eapply heap_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply msubst_closing_inv_3; eauto.
eapply heap_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply msubst_closing_1.
{ apply c2h_closed. eapply typ_context_closed_2; eauto. }
eauto.
intros x'.
intros ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
{ intros →. left. set_solver+. }
intros Hne. move: Helem. rewrite lookup_insert_ne; auto.
case (decide (s = y)).
{ intros →. left. set_solver+. }
intros Hne'. rewrite lookup_insert_ne; auto.
rewrite /subst2typ lookup_fmap.
intros; right. apply elem_of_dom.
rewrite lookup_fmap //=.
case_eq (S2 !! s).
× intros P Hlook%map_subseteq_spec; eauto. rewrite Hlook. eauto.
× intros Hnone. rewrite Hnone in Helem. inversion Helem.
}
assert (chan_lang.Closed [x; y] (cmsubst (delete x (delete y (subst2cl' S))) eb)).
{ rewrite /chan_lang.Closed.
rewrite /subst2cl' /subst2cl ?fmap_delete.
eapply chan_lang.substitution.msubst_closing_inv_3.
{ apply chan_lang.substitution.ClosedSubst_delete; auto. }
eapply chan_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply chan_lang.substitution.msubst_closing_inv_3; eauto.
eapply chan_lang.is_closed_perm; last first.
{ apply perm_swap. }
eapply chan_lang.substitution.msubst_closing_1.
{ eapply typ_context_closed_2; eauto. }
eauto.
intros x'.
intros ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
{ intros →. left. set_solver+. }
intros Hne. move: Helem. rewrite lookup_insert_ne; auto.
case (decide (s = y)).
{ intros →. left. set_solver+. }
intros Hne'. rewrite lookup_insert_ne; auto.
rewrite /subst2typ lookup_fmap.
intros; right. apply elem_of_dom.
rewrite lookup_fmap //=.
case_eq (S2 !! s).
× intros P Hlook%map_subseteq_spec; eauto. rewrite Hlook. eauto.
× intros Hnone. rewrite Hnone in Helem. inversion Helem.
}
wp_letp.
refine_letp (dK K (cmsubst (<[x:=of_val vc1]> (<[y:=of_val vc2]> (subst2cl' S))) eb)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
rewrite -heap_lang.substitution.msubst_insert_2.
rewrite -delete_insert_ne //.
rewrite -heap_lang.substitution.msubst_insert_2.
rewrite -chan_lang.substitution.msubst_insert_2.
rewrite -delete_insert_ne //.
rewrite -chan_lang.substitution.msubst_insert_2.
rewrite insert_commute //.
rewrite {1}(insert_commute _ y x) //.
specialize (IHhas_typ2 (<[x := {| styp := ty1;
hval := vh1;
cval := vc1 |}]>
(<[y := {| styp := ty2;
hval := vh2;
cval := vc2 |}]>S2))).
iPoseProof (IHhas_typ2 with "[Hv1 Hv2 HS2]") as "HS2'".
{ rewrite /subst2typ. subst. rewrite ?fmap_insert //. }
{ rewrite /subst2hl' /subst2hl ?fmap_insert //=.
apply ClosedSubst_insert; last solve_closed.
apply ClosedSubst_insert; last solve_closed.
eapply ClosedSubst_subseteq; eauto.
apply fmap_subseteq; auto.
}
{ rewrite /subst2cl' /subst2cl ?fmap_insert //=.
apply chan_lang.substitution.ClosedSubst_insert; last chan_lang.tactics.solve_closed.
apply chan_lang.substitution.ClosedSubst_insert; last chan_lang.tactics.solve_closed.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; auto.
}
{
iFrame "Hheap". iFrame "Hscheap".
rewrite subst2typ_insert2_bigM //=; auto.
iFrame "HS2".
iSplitL "Hv1"; by iApply val_equiv_expr.
}
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i K).
assert ((cmsubst
(subst2cl'
(<[x:={|
styp := ty1;
hval := heap_lang.of_val vh1;
cval := of_val vc1 |}]>
(<[y:={|
styp := ty2;
hval := heap_lang.of_val vh2;
cval := of_val vc2 |}]> S2))) eb) =
(cmsubst
((<[x:=of_val vc1]>(<[y:= of_val vc2]>(subst2cl' S2))))) eb) as Hsimpl.
{ clear. f_equal. rewrite /subst2cl' /subst2cl.
rewrite ?fmap_insert. auto. }
rewrite Hsimpl. clear Hsimpl.
assert ((hmsubst
(subst2hl'
(<[x:={|
styp := ty1;
hval := heap_lang.of_val vh1;
cval := of_val vc1 |}]>
(<[y:={|
styp := ty2;
hval := heap_lang.of_val vh2;
cval := of_val vc2 |}]> S2))) (c2h eb) =
(hmsubst
((<[x:=heap_lang.of_val vh1]>
(<[y:= heap_lang.of_val vh2]>(subst2hl' S2)))) (c2h eb)))) as Hsimpl.
{ clear. f_equal. rewrite /subst2hl' /subst2hl.
rewrite ?fmap_insert. auto. }
rewrite Hsimpl. clear Hsimpl.
erewrite (chan_lang.substitution.msubst_weaken_2 eb
(<[x:=of_val vc1]>(<[y:=of_val vc2]> (subst2cl' S2)))
(<[x:=of_val vc1]>(<[y:=of_val vc2]> (subst2cl' S)))); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
do 2 apply insert_mono. apply fmap_subseteq; eauto.
apply chan_lang.substitution.ClosedSubst_insert; eauto.
apply chan_lang.substitution.ClosedSubst_insert; eauto.
chan_lang.tactics.solve_closed.
chan_lang.tactics.solve_closed.
erewrite (substitution.msubst_weaken_2 (c2h eb)
(<[x:=heap_lang.of_val vh1]>(<[y:=heap_lang.of_val vh2]> (subst2hl' S2)))
(<[x:=heap_lang.of_val vh1]>(<[y:=heap_lang.of_val vh2]> (subst2hl' S)))); eauto;
last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite /subst2hl' /subst2hl ?dom_insert ?dom_fmap //.
}
do 2 apply insert_mono. apply fmap_subseteq; eauto.
apply ClosedSubst_insert; eauto.
apply ClosedSubst_insert; eauto.
heap_lang.tactics.solve_closed.
heap_lang.tactics.solve_closed.
iApply "HS2'".
done.
apply chan_lang.substitution.ClosedSubst_insert; eauto.
chan_lang.tactics.solve_closed.
apply chan_lang.substitution.ClosedSubst_delete; eauto.
apply heap_lang.substitution.ClosedSubst_insert; eauto.
heap_lang.tactics.solve_closed.
apply heap_lang.substitution.ClosedSubst_delete; eauto.
rewrite /is_Some. eexists. eauto.
rewrite /is_Some. eexists. eauto.
auto.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
erewrite <-(chan_lang.substitution.msubst_weaken_2 e1
(subst2cl' S1)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(chan_lang.substitution.msubst_weaken_2 e2
(subst2cl' S2)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e1)
(subst2hl' S1)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e2)
(subst2hl' S2)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
assert (chan_lang.Closed [] (cmsubst (subst2cl' S1) e1)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (chan_lang.Closed [] (cmsubst (subst2cl' S2) e2)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S1) (c2h e1))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S2) (c2h e2))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
idtac.
wp_focus (hmsubst S2 (c2h e2)).
refine_focus (cmsubst S2 e2).
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_seq. refine_seq (dK K (cmsubst S1 e1)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
iExists vc'. iFrame "Hown". auto.
- intros; iIntros "(#?&#?&HS)". simpl.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
wp_apply wp_fork.
refine_fork (dK K (chan_lang.Lit chan_lang.LitUnit)) i' as "Hown'".
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
iSplitL "Hown".
{ iExists (chan_lang.LitV chan_lang.LitUnit).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
}
iPoseProof (IHhas_typ S with "[HS]") as "HS'"; try assumption.
iFrame. { iSplitL; auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS'" $! i' [] with "Hown'").
iApply wp_wand_l; iFrame "HS'".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc) "(?&?)".
rewrite /dK //= chan_lang.to_of_val.
refine_stopped.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
assert (Hcloc: chan_lang.Closed [x] (cmsubst (delete x (subst2cl' S)) e)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
{ apply chan_lang.substitution.ClosedSubst_delete. eauto. }
intros x' ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
- intros. subst. left. set_solver+.
- intros Hneq; right.
apply elem_of_dom.
move: Helem.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (Hcloh: heap_lang.Closed [x] (hmsubst (delete x (subst2hl' S)) (c2h e))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
{ apply ClosedSubst_delete. eauto. }
intros x' ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
- intros. subst. left. set_solver+.
- intros Hneq; right.
apply elem_of_dom.
move: Helem.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (Hclo1: heap_lang.Closed [] (heap_lang.derived.Lam x (hmsubst (delete x (subst2hl' S))
(c2h e)))).
{ rewrite //=. }
assert (Hclo2: chan_lang.Closed [] (chan_lang.derived.Lam x (cmsubst (delete x (subst2cl' S))
(e)))).
{ rewrite //=. }
assert (heap_lang.to_val ((heap_lang.derived.Lam x (hmsubst (delete x (subst2hl' S))
(c2h e))))
= Some (heap_lang.derived.LamV x (hmsubst (delete x (subst2hl' S))
(c2h e)))).
{ rewrite //=. case_decide; eauto.
- repeat f_equal. apply proof_irrel.
- exfalso; eauto. }
iApply wp_value; eauto.
iExists (LamV (BNamed x) (cmsubst (delete x (subst2cl' S)) e)).
iFrame "Hown".
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iExists x. iExists (hmsubst (delete x (subst2hl' S)) (c2h e)).
iExists Hcloh.
iExists x. iExists (cmsubst (delete x (subst2cl' S)) (e)).
iExists Hcloc.
iSplitR; first auto.
iSplitR; first auto.
iIntros (vh vc). iIntros "@".
iIntros "Hpre".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i' K'). iIntros "@". iIntros "Hown".
pose (S' := (<[x := {| styp := ty1;
hval := heap_lang.of_val vh;
cval := chan_lang.of_val vc|}]>(delete x S))).
specialize (IHhas_typ S').
rewrite /S' in IHhas_typ ×.
iPoseProof (IHhas_typ with "[HS Hpre]") as "HS'".
{ subst. rewrite /subst2typ ?fmap_insert //=.
rewrite fmap_delete insert_delete //. }
{ rewrite /subst2hl' /subst2hl fmap_insert //=.
apply ClosedSubst_insert; auto.
rewrite fmap_delete.
apply ClosedSubst_delete; auto.
solve_closed. }
{ rewrite /subst2cl' /subst2cl fmap_insert //=.
apply chan_lang.substitution.ClosedSubst_insert; auto.
rewrite fmap_delete.
apply chan_lang.substitution.ClosedSubst_delete; auto.
chan_lang.tactics.solve_closed. }
{
rewrite big_sepM_insert //=.
iFrame. iFrame "Hheap". iFrame "Hscheap".
iSplitL "Hpre".
- by iApply val_equiv_expr.
- case (decide (is_Some (S !! x))).
× intros (P&Heq). rewrite big_sepM_delete.
iDestruct "HS" as "(?&?)".
iFrame; eauto. apply Heq.
× intros Hnone. assert (S = delete x S) as Heq.
{ rewrite delete_notin; eauto. apply eq_None_not_Some; eauto. }
rewrite -Heq. eauto.
- apply lookup_delete_subst_ctx_1.
}
idtac.
rewrite /expr_equiv /expr_rel_lift.
wp_let. refine_let (dK K' (cmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) e)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
rewrite -msubst_insert_1.
rewrite -chan_lang.substitution.msubst_insert_1.
assert ((cmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) e) =
(cmsubst (<[x:=chan_lang.of_val vc]> (delete x (subst2cl' S))) e)) as Heqc.
{ f_equal. rewrite /subst2cl' /subst2cl. rewrite ?fmap_insert //=.
rewrite fmap_delete //. }
assert ((hmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) (c2h e)) =
(hmsubst (<[x:=heap_lang.of_val vh]> (delete x (subst2hl' S))) (c2h e))) as Heqh.
{ f_equal. rewrite /subst2hl' /subst2hl. rewrite ?fmap_insert //=.
rewrite fmap_delete //. }
rewrite Heqc Heqh.
iSpecialize ("HS'" $! i' K' with "Hown").
iApply wp_wand_l. iFrame "HS'".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc') ("Hpre'").
iExists vc'.
rewrite val_equiv_fix_unfold'.
auto.
apply chan_lang.substitution.ClosedSubst_delete. eauto.
eapply lookup_delete_subst_ctx_2.
apply heap_lang.substitution.ClosedSubst_delete. eauto.
eapply lookup_delete_subst_ctx_3.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
idtac.
erewrite <-(chan_lang.substitution.msubst_weaken_2 e1
(subst2cl' S1)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(chan_lang.substitution.msubst_weaken_2 e2
(subst2cl' S2)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e1)
(subst2hl' S1)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e2)
(subst2hl' S2)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
assert (chan_lang.Closed [] (cmsubst (subst2cl' S1) e1)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (chan_lang.Closed [] (cmsubst (subst2cl' S2) e2)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S1) (c2h e1))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S2) (c2h e2))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
wp_focus (hmsubst S1 (c2h e1)).
refine_focus (cmsubst S1 e1).
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_focus (hmsubst S2 (c2h e2)).
refine_focus (cmsubst S2 e2).
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_rel_lift.
iDestruct "Hvequiv" as (??????) "(%&%&Hvequiv)".
iSpecialize ("Hvequiv" $! vh' vc' with "[Hvequiv']"); auto.
iSpecialize ("Hvequiv" $! i K with "Hown").
iApply wp_wand_l. iFrame "Hvequiv".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc'') "Hpre'".
iExists vc''.
rewrite ?val_equiv_fix_unfold' //=.
- intros S Herase HcloSh HcloSc.
iIntros "(#Hheap&#Hscheap&_)".
rewrite //=.
assert (hmsubst S alloc = alloc) as →.
{ apply msubst_closed. rewrite /alloc. solve_closed. }
assert (cmsubst S (newch)%C = (newch)%C) as →.
{ apply chan_lang.substitution.msubst_closed. chan_lang.tactics.solve_closed. }
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
iPoseProof (alloc_spec protN _ _ _ p i K (dK K (newch)%C)
(dK K (chan_lang.Lit (LitLoc 1%positive cleft))) with "[Hown]")
as "Hwp".
{ rewrite /dK /dinit /Kd. rewrite //=.
specialize (fill_not_val K (newch)%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone. omega. auto.
}
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ iFrame "Hown". iFrame "Hheap". iFrame "Hscheap".
repeat iSplit; iPureIntro; eauto with ndisj. }
iApply wp_wand_l. iFrame "Hwp".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (l c) "?".
iExists (chan_lang.PairV (chan_lang.LitV $ chan_lang.LitLoc c cleft)
(chan_lang.LitV $ chan_lang.LitLoc c cright)).
iDestruct "Hpre" as "(%&Hleft&Hright&Hown)".
assert (dK K $ chan_lang.PairV
(chan_lang.LitV $ chan_lang.LitLoc c cleft)
(chan_lang.LitV $ chan_lang.LitLoc c cright)
=
dK K $ (chan_lang.Lit $ chan_lang.LitLoc 1%positive cleft)) as <-.
{ eapply fill_val_dK; eauto. }
iFrame "Hown".
iIntros "@". rewrite val_equiv_fix_unfold' //=.
iExists (#l)%V. iExists (#l)%V.
iExists (chan_lang.LitV $ chan_lang.LitLoc c cleft)%V.
iExists (chan_lang.LitV $ chan_lang.LitLoc c cright)%V.
iSplitR; first auto.
iSplitR; first auto.
iSplitL "Hleft".
× iExists l. iExists c. iExists cleft.
iSplitR; first auto.
iSplitR; first auto.
iAssumption.
× iExists l. iExists c. iExists cright.
iSplitR; first auto.
iSplitR; first auto.
iAssumption.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
edestruct (subst_ctx_subseteq S Γ Γ1 Γ2) as (S1&S2&Hsub1&Hsub2&Hdom&Herase1&Herase2); eauto.
edestruct (big_sepM_split (λ _ P, expr_equiv (styp P) (hval P) (cval P)) S S1 S2)
as (m3&Hequiv); eauto.
rewrite Hequiv.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS1&HS2&_)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
erewrite <-(chan_lang.substitution.msubst_weaken_2 e
(subst2cl' S1)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(chan_lang.substitution.msubst_weaken_2 ev
(subst2cl' S2)
(subst2cl' S)); eauto; last first.
{ intros l Hin. eapply typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
rewrite msubst_unfold // //=.
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h e)
(subst2hl' S1)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase1. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
erewrite <-(heap_lang.substitution.msubst_weaken_2 (c2h ev)
(subst2hl' S2)
(subst2hl' S)); eauto; last first.
{ intros l Hin. eapply c2h_closed, typ_context_closed_1; eauto.
intros x' Hin'. apply Hin. move:Hin'.
rewrite -Herase2. rewrite /subst2typ /subst2cl' /subst2cl ?dom_insert ?dom_fmap //.
}
{ apply fmap_subseteq. eauto. }
assert (chan_lang.Closed [] (cmsubst (subst2cl' S1) e)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (chan_lang.Closed [] (cmsubst (subst2cl' S2) ev)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
eapply chan_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S1) (c2h e))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S1 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S2) (c2h ev))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
eapply heap_lang.substitution.ClosedSubst_subseteq; eauto.
apply fmap_subseteq; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S2 !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
wp_focus (hmsubst S1 (c2h e)).
refine_focus (cmsubst S1 e).
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS1'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS1'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_focus (hmsubst S2 (c2h ev)).
refine_focus (cmsubst S2 ev).
iPoseProof (IHhas_typ2 S2 with "[HS2]") as "HS2'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
{ eapply ClosedSubst_subseteq_csubst; eauto. }
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS2'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS2'".
iIntros "@". iIntros (vh') "Hpre".
iDestruct "Hpre" as (vc') "(Hvequiv'&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_rel_lift.
rewrite affine_elim.
assert(
(letp: "l" "v" := (vh, vh')
in hmsubst (delete "l" (delete "v" (subst2hl' S)))
(let: "lnew" := ref SOME #()
in "l" <- heap_lang.InjL ("lnew", "v")
;; "lnew"))%E
= hmsubst S (send vh vh')) as →.
{
rewrite /send.
symmetry.
rewrite msubst_unfold // //=.
rewrite msubst_unfold // //=.
assert (hmsubst S vh = vh) as →.
{ apply msubst_closed. solve_closed. }
assert (hmsubst S vh' = vh') as →.
{ apply msubst_closed. solve_closed. }
trivial.
}
assert (hmsubst S (send vh vh') = send vh vh') as →.
{ apply msubst_closed. rewrite /send. solve_closed. }
iDestruct "Hvequiv" as (l c s) "(%&%&Hmaps)"; subst.
iPoseProof (send_spec protN _ _
(CofeMor (λ ty, (CofeMor (λ vh,
CofeMor (λ vc, ▷ (val_equiv ty vh vc))
))))%I
ty vc' vc' vh' vh' _ c s l i K
(dK K (Lit $ LitLoc c s <- vc'))%C
(dK K (LitV $ LitLoc c s)%C)) as "Hsend".
{ rewrite /dK /dinit /Kd //=; split.
- specialize (fill_not_val K (#(LitLoc c s) <- vc')%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone. omega. auto.
- case_match; omega.
}
{ rewrite /dK /dinit /Kd //=. case_match; omega. }
rewrite chan_lang.to_of_val //=.
rewrite heap_lang.to_of_val //=.
iSpecialize ("Hsend" with "[Hmaps Hvequiv' Hown]").
{ iFrame "Hown". iFrame "Hmaps".
simpl. iIntros "@". iNext.
rewrite val_equiv_fix_unfold'. auto.
}
iApply wp_wand_l. iFrame "Hsend".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (l') "(%&Hprot&Hown)".
iExists (LitV $ LitLoc c s)%C.
iFrame "Hown".
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iExists l'. iExists c. iExists s.
iSplitR; first auto.
iSplitR; first auto.
done.
- intros S Herase HcloSh HcloSc.
iIntros "Hctx". simpl c2h.
rewrite msubst_unfold // chan_lang.substitution.msubst_unfold //=.
iDestruct "Hctx" as "(#Hheap&#Hscheap&HS)".
rewrite /expr_equiv /expr_rel_lift.
iIntros (i K) "@ Hown".
assert (chan_lang.Closed [] (cmsubst (subst2cl' S) e)).
{ rewrite /subst2cl' /subst2cl. eapply chan_lang.substitution.msubst_closing_1; auto.
eapply typ_context_closed_2; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (heap_lang.Closed [] (hmsubst (subst2hl' S) (c2h e))).
{ rewrite /subst2hl' /subst2hl. eapply heap_lang.substitution.msubst_closing_1; auto.
eapply c2h_closed, typ_context_closed_2; eauto.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
idtac.
assert (hmsubst S recv = recv) as →.
{ apply msubst_closed. rewrite /recv. solve_closed. }
rewrite /recv.
wp_focus (hmsubst S (c2h e)).
refine_focus (cmsubst S e).
iPoseProof (IHhas_typ S with "[HS]") as "HS'"; try assumption.
{ iFrame. auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("HS'" $! i _ with "Hown").
iApply wp_wand_l; iFrame "HS'".
iIntros "@". iIntros (vh) "Hpre".
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
rewrite /recv.
assert
(((rec: "recv" "l"
:= match: ! "l" with InjL "x" ⇒ "x" | InjR "_" ⇒
("recv": heap_lang.expr) "l" end)%V vh)%E
= recv vh) as Heq.
{ rewrite /recv. auto. }
rewrite Heq.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_rel_lift.
rewrite affine_elim.
iDestruct "Hvequiv" as (l c s) "(%&%&Hmaps)"; subst.
iPoseProof (recv_spec protN _ _
(CofeMor (λ ty, (CofeMor (λ vh,
CofeMor (λ vc, ▷ (val_equiv ty vh vc))
))))%I
ty
(val_equiv_pre val_equiv ty)
_ c s l i K
(dK K (! (LitV $ LitLoc c s)))%C
(dK K (LitV $ LitLoc c s)%C)) as "Hrecv".
{ rewrite /dK /dinit /Kd //=; split.
- specialize (fill_not_val K (! (LitV $ LitLoc c s))%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone. omega. auto.
- case_match; omega.
}
{ rewrite /dK /dinit /Kd //=. case_match; omega. }
{ intros. simpl. rewrite val_equiv_fix_unfold'. auto. }
iSpecialize ("Hrecv" with "[Hmaps Hown]").
{ iFrame "Hown". iFrame "Hmaps". auto. }
iApply wp_wand_l. iFrame "Hrecv".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (l' vh' vc') "(%&Hprot&Hvequiv&Hown)".
iExists (PairV (LitV $ LitLoc c s) vc')%C.
assert (dK K $ chan_lang.PairV
(chan_lang.LitV $ chan_lang.LitLoc c s)
vc'
=
dK K $ (chan_lang.LitV $ chan_lang.LitLoc c s)) as <-.
{ eapply fill_val_dK; eauto. eauto.
rewrite //=. rewrite to_of_val. eauto.
}
iFrame "Hown".
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iExists (#l')%V. iExists vh'.
iExists (LitV $ LitLoc c s)%C. iExists vc'.
iSplitR; first auto.
iSplitR; first auto.
iFrame "Hvequiv".
iExists l'. iExists c. iExists s.
iSplitR; first auto.
iSplitR; first auto.
idtac.
auto.
- intros. rewrite IHhas_typ; eauto.
rewrite /expr_equiv /expr_rel_lift.
iIntros "Hpre". iIntros (i K) "@ Hown".
iSpecialize ("Hpre" $! i K with "Hown").
iApply wp_wand_l. iFrame "Hpre".
iIntros "@". iIntros (v) "Hpre".
idtac.
iDestruct "Hpre" as (vc) "(Hve&Hown)".
iExists vc. iFrame "Hown".
iIntros "@".
rewrite val_equiv_fix_unfold'.
rewrite val_equiv_fix_unfold'.
rewrite //=.
iDestruct "Hve" as (lh lc s) "(%&%&?)".
iExists lh. iExists lc. iExists s.
iSplitR; first auto.
iSplitR; first auto.
idtac.
rewrite H0.
auto.
Grab Existential Variables.
rewrite /Kd. compute. auto.
rewrite /Kd. compute. auto.
rewrite /Kd. compute. auto.
Qed.
End lr.
Section closed.
Definition Σ : gFunctors := #[ heapGF ; scheapGF ; protGF ;
refineGF (delayed_lang (chan_lang) Kd dinit)
(S Kd × (Kd + 3))].
Lemma Σ_len: projT1 Σ = 5%nat.
Proof. auto. Qed.
Ltac gid_destruct g1 g2 :=
match type of g1 with
| fin ?T ⇒
refine
(match g1 as g' in fin n return ∀ (pf: n = T),
eq_rect n fin g' T pf = g1 →
_ with
| Fin.F1 _ ⇒ _
| FS _ g2 ⇒ _
end Init.Logic.eq_refl Init.Logic.eq_refl);
let pf := fresh "pf" in
intros pf ?; inversion pf; subst; simpl;
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec; clear pf
| _ ⇒ fail g1 "is not a fin."
end.
Tactic Notation "gid_destruct" constr(g1) "as" simple_intropattern(g2) :=
gid_destruct g1 g2.
Instance inGF_refineG : refineG heap_lang Σ (delayed_lang (chan_lang) Kd dinit) (S Kd × (Kd + 3)).
Proof. eapply inGF_refineG. intros g A.
rewrite /gid in g ×.
assert (fin (projT1 Σ) = fin 5) as Hlen.
{ rewrite Σ_len. auto. }
rewrite /projT2 /Σ.
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ intros (?&->); simpl.
intros a a' n i; by done. }
gid_destruct g as g.
{ simpl in ×. intros (?&_). exfalso; eauto. }
inversion g.
Grab Existential Variables.
rewrite /Kd. auto.
Qed.
Instance inGF_scheapG: scheapG heap_lang Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 1%positive. Qed.
Instance inGF_heapG: heapG Σ.
Proof. eauto. split. try apply _; eauto. rewrite /gname. exact 2%positive. Qed.
Instance inGF_protG: protG Σ.
Proof. eauto. split; try apply _; eauto. Qed.
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Local Notation hexprC := (leibnizC (heap_lang.expr)).
Local Notation cexprC := (leibnizC (chan_lang.expr)).
Local Notation hvalC := (leibnizC (heap_lang.val)).
Local Notation cvalC := (leibnizC (chan_lang.val)).
Fixpoint c2h_refine (v: heap_lang.val) (v': chan_lang.val) :=
match v, v' with
| heap_lang.LitV (heap_lang.LitBool b),
chan_lang.LitV (chan_lang.LitBool b') ⇒
b = b'
| heap_lang.LitV (heap_lang.LitInt n),
chan_lang.LitV (chan_lang.LitInt n') ⇒
n = n'
| heap_lang.LitV (heap_lang.LitUnit),
chan_lang.LitV (chan_lang.LitUnit) ⇒
True
| heap_lang.LitV (heap_lang.LitLoc _),
chan_lang.LitV (chan_lang.LitLoc _ _) ⇒
True
| heap_lang.RecV _ _ _ _,
chan_lang.RecV _ _ _ _ ⇒
True
| heap_lang.PairV vh1 vh2,
chan_lang.PairV vc1 vc2⇒
c2h_refine vh1 vc1 ∧ c2h_refine vh2 vc2
| _, _ ⇒ False
end.
Import uPred.
Existing Instance prot_mapsto_affine.
Lemma val_equiv_c2h_refine H1 H2 H3 H4 ty vh vc:
(@val_equiv Σ H1 H2 H3 H4) ty vh vc ⊢ ⧆ ■ c2h_refine vh vc.
Proof.
rewrite val_equiv_fix_unfold'.
revert vh vc.
induction ty; simpl; intros.
- iIntros "HVC".
iDestruct "HVC" as (vh1 vh2 vc1 vc2) "(%&%&Hv1&Hv2)".
subst.
iPoseProof (IHty1 with "Hv1") as "H1". iDestruct "H1" as "%".
iPoseProof (IHty2 with "Hv2") as "H2". iDestruct "H2" as "%".
iPureIntro. split; auto.
- iIntros "HVC".
iDestruct "HVC" as (xh eh1 Hcloh xc ec1 Hcloc) "(%&%&?)".
subst. iPureIntro. rewrite //=.
- iIntros "(%&%)". subst. iPureIntro. rewrite //=.
- iIntros "HVC". iDestruct "HVC" as (n') "(%&%)".
subst. iPureIntro. rewrite //=.
- iIntros "HVC". iDestruct "HVC" as (b') "(%&%)".
subst. iPureIntro. rewrite //=.
- iIntros. iApply False_elim. done.
- iIntros "HVC". iDestruct "HVC" as (lh lc s) "(%&%&_)".
subst. iPureIntro. rewrite //=.
Qed.
Lemma soundness ty eh ec:
(∀ H1 H2 H3 H4 H5, @ctx_expr_equiv H1 H2 H3 H4 H5 ∅ ty eh ec) →
safe_refine (c2h_refine) eh ∅ ec ∅.
Proof.
intros Hpre.
case_eq (chan_lang.to_val ec).
- intros Hv Heqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := 0%nat).
× eapply head_step_det_prim_det, chan_lang.head_step_det.
× apply chan_prim_dec.
×
iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (scheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Heqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown')".
iExists vc.
rewrite {1}/dK //= chan_lang.to_of_val.
iFrame "Hown'".
rewrite affine_elim.
iApply (val_equiv_c2h_refine _ _ _ _ ty vh vc).
iAssumption.
- intros Hneqv.
eapply iris.program_logic.refine_ectx_delay.ht_safe_refine with (d := dinit%nat).
× eapply head_step_det_prim_det, chan_lang.head_step_det.
× apply chan_prim_dec.
× iIntros "_ @ ! (Hown&Hσ&Hsσ)".
iPvs (heap_alloc with "Hσ") as (h) "[#Hheap _]"; first by done.
iPvs (scheap_alloc with "Hsσ") as (h') "[#Hsheap _]"; first by done.
eapply @expr_equiv_empty in Hpre; eauto.
apply relevant_intro in Hpre; last apply _.
iCombine "Hheap" "Hsheap" as "Hheap'".
iPoseProof (@Hpre with "Hheap'") as "Hheap''".
rewrite /expr_equiv /expr_rel_lift.
rewrite relevant_elim.
iSpecialize ("Hheap''" $! 0%nat).
iSpecialize ("Hheap''" $! []).
iSpecialize ("Hheap''" with "[Hown]").
{ rewrite /dK Hneqv. auto. }
iApply wp_wand_l; iFrame "Hheap''".
iIntros "@". iIntros (vh) "HVC"; iDestruct "HVC" as (vc) "(?&Hown1)".
iExists vc.
rewrite {1}/dK //= chan_lang.to_of_val.
iFrame.
rewrite affine_elim.
iApply (val_equiv_c2h_refine _ _ _ _ ty vh vc).
iAssumption.
Qed.
End closed.