Commit b2e55982 authored by Dan Frumin's avatar Dan Frumin

Bring some uniformity to [relational_properties]

- Make sure that arguments to the lemmas are in the consistent order:
\Gamma, E1, E2, K, e1, e2, \tau -- from left to right, as you write it
 on paper
- Add masks to all the lemmas
- Add missing rules
- Remove unnecessary closedness conditions
parent a1285d86
......@@ -401,8 +401,8 @@ Section CG_Counter.
iApply (bin_log_related_rec_l _ []); auto.
iNext. simpl.
rel_bind_r (App _ (#cnt')%E).
iApply (bin_log_related_rec_r _ _ ); auto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ [] ); auto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _); auto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _ _ []); auto. simpl. rewrite !Closed_subst_id.
unfold with_lock. unlock.
rel_bind_r (App _ (λ: "l", _))%E.
......@@ -411,7 +411,7 @@ Section CG_Counter.
{ simpl. by rewrite decide_left. }
simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ [] ); eauto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
iApply bin_log_related_arrow.
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
......@@ -434,7 +434,7 @@ Section CG_Counter.
(* simpl. *)
(* iApply bin_log_related_unit. *)
(* Opaque CG_locked_increment with_lock. *)
iApply (bin_log_related_rec_r _ []); eauto. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
iLöb as "IH".
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
rel_bind_l (! #cnt)%E.
......@@ -459,27 +459,27 @@ Section CG_Counter.
rel_bind_r (acquire #l).
iApply (bin_log_related_acquire_r with "Hl"); simpl; eauto. solve_ndisj.
iIntros "Hl".
iApply (bin_log_related_rec_r _ []); simpl; eauto. solve_ndisj.
iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj.
rel_bind_r (App _ #())%E.
iApply (bin_log_related_rec_r _ _); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
rel_bind_r (CG_increment _ _).
iApply (bin_log_related_CG_increment_r with "Hcnt'"). solve_ndisj. simpl.
iIntros "Hcnt'".
iApply (bin_log_related_rec_r _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
rel_bind_r (release #l)%E.
iApply (bin_log_related_release_r with "Hl"). solve_ndisj.
iIntros "Hl". simpl.
iMod ("Hcl" with "[-]").
{ iNext. iExists _. by iFrame. }
iApply (bin_log_related_if_true_l _ _ []). iNext. simpl.
iApply (bin_log_related_rec_r _ []); simpl; eauto.
iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto.
iApply bin_log_related_unit.
- (* CASE [m n], CAS fails *)
iSplitL; last first. iIntros "%". exfalso. apply Hmn. by inversion H1.
iIntros "% Hcnt". simpl.
iMod ("Hcl" with "[-]").
{ iNext. iExists _. by iFrame. }
iApply (bin_log_related_if_false_l _ []). iNext. simpl.
iApply (bin_log_related_if_false_l _ _ []). iNext. simpl.
iApply "IH".
Qed.
......@@ -490,7 +490,7 @@ Section CG_Counter.
rel_bind_r newlock.
iApply (bin_log_related_newlock_r); auto; simpl.
iIntros (l) "Hl".
iApply (bin_log_related_rec_r _ []); auto. rewrite /= !Closed_subst_id /=.
iApply (bin_log_related_rec_r _ _ _ []); auto. rewrite /= !Closed_subst_id /=.
rel_bind_l (Alloc _).
iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
iIntros (cnt) "Hcnt".
......@@ -507,19 +507,19 @@ Section CG_Counter.
iApply (bin_log_related_rec_l _ _ []); auto.
iNext. rewrite /= !Closed_subst_id /=.
iApply (bin_log_related_rec_r _ []); auto. simpl.
iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
rewrite /= !Closed_subst_id /=.
rel_bind_r (CG_counter_body _).
unfold CG_counter_body. unlock.
iApply (bin_log_related_rec_r _ _); auto.
rewrite /= !Closed_subst_id /=.
iApply (bin_log_related_rec_r _ []); auto.
iApply (bin_log_related_rec_r _ _ _ []); auto.
rewrite /= !Closed_subst_id /=.
iApply (bin_log_related_pair _ with "[]"); last first.
- Transparent counter_read.
unfold counter_read. unlock.
iApply (bin_log_related_rec_r _ []); auto. simpl.
iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.
iApply bin_log_related_rec; simpl. iAlways. cbn.
iApply (bin_log_related_load_l _ _ _ []).
......
......@@ -48,8 +48,9 @@ Section properties.
Qed.
(** ** Reductions on the left *)
(** Lifting of the pure reductions *)
Lemma bin_log_pure_l (Γ : stringmap type) (E : coPset) (τ : type) e e' t K'
(** *** Lifting of the pure reductions *)
Lemma bin_log_pure_l (Γ : stringmap type) (E : coPset)
(K' : list ectx_item) (e e' t : expr) (τ : type)
(Hclosed : Closed e)
(Hclosed' : Closed e')
(Hsafe : σ, head_reducible e σ) :
......@@ -79,7 +80,8 @@ Section properties.
iApply (fupd_mask_mono E); auto.
Qed.
Lemma bin_log_pure_masked_l Γ E1 E2 K' τ (e e' : expr) t
Lemma bin_log_pure_masked_l (Γ : stringmap type) (E1 E2 : coPset)
(K' : list ectx_item) (e e' t : expr) (τ : type)
(Hclosed : Closed e)
(Hclosed' : Closed e')
(Hsafe : σ, head_reducible e σ) :
......@@ -109,9 +111,9 @@ Section properties.
done.
Qed.
Lemma bin_log_related_fst_l Γ K e v1 v2 τ :
(Γ (fill K (of_val v1)) log e : τ)
Γ (fill K (Fst (Pair (of_val v1) (of_val v2)))) log e : τ.
Lemma bin_log_related_fst_l Γ E K v1 v2 e τ :
({E,E;Γ} (fill K (of_val v1)) log e : τ)
{E,E;Γ} (fill K (Fst (Pair (of_val v1) (of_val v2)))) log e : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -119,9 +121,9 @@ Section properties.
- by inversion H1.
Qed.
Lemma bin_log_related_snd_l Γ K e v1 v2 τ :
(Γ (fill K (of_val v2)) log e : τ)
Γ (fill K (Snd (Pair (of_val v1) (of_val v2)))) log e : τ.
Lemma bin_log_related_snd_l Γ E K v1 v2 e τ :
({E,E;Γ} (fill K (of_val v2)) log e : τ)
{E,E;Γ} (fill K (Snd (Pair (of_val v1) (of_val v2)))) log e : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -129,7 +131,7 @@ Section properties.
- by inversion H1.
Qed.
Lemma bin_log_related_rec_l Γ E K f x e e' v t τ
Lemma bin_log_related_rec_l Γ E K (f x : binder) e e' v t τ
(Hclosed : Closed (x :b: f :b: ) e) :
(to_val e' = Some v)
({E,E;Γ} (fill K (subst' f (Rec f x e) (subst' x e' e))) log t : τ)
......@@ -152,10 +154,10 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_tlam_l Γ K e t τ
Lemma bin_log_related_tlam_l Γ E K e t τ
(Hclosed : Closed e) :
(Γ fill K e log t : τ)
Γ (fill K (TApp (TLam e))) log t : τ.
({E,E;Γ} fill K e log t : τ)
{E,E;Γ} (fill K (TApp (TLam e))) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -165,11 +167,10 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_fold_l Γ K e v t τ
(Hclosed : Closed e) :
Lemma bin_log_related_fold_l Γ E K e v t τ :
(to_val e = Some v)
(Γ fill K e log t : τ)
Γ (fill K (Unfold (Fold e))) log t : τ.
({E,E;Γ} fill K e log t : τ)
{E,E;Γ} (fill K (Unfold (Fold e))) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -179,12 +180,11 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_pack_l Γ K e e' v t τ
(Hclosed : Closed e)
Lemma bin_log_related_pack_l Γ E K e e' v t τ
(Hclosed' : Closed e') :
(to_val e = Some v)
(Γ fill K (App e' e) log t : τ)
Γ (fill K (Unpack (Pack e) e')) log t : τ.
({E,E;Γ} fill K (App e' e) log t : τ)
{E,E;Γ} (fill K (Unpack (Pack e) e')) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -194,13 +194,12 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_case_inl_l Γ K e e1 e2 v t τ
(Hclosed : Closed e)
Lemma bin_log_related_case_inl_l Γ E K e v e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
(to_val e = Some v)
(Γ fill K (App e1 e) log t : τ)
Γ (fill K (Case (InjL e) e1 e2)) log t : τ.
({E,E;Γ} fill K (App e1 e) log t : τ)
{E,E;Γ} (fill K (Case (InjL e) e1 e2)) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -210,13 +209,12 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_case_inr_l Γ K e e1 e2 v t τ
(Hclosed : Closed e)
Lemma bin_log_related_case_inr_l Γ E K e v e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
(to_val e = Some v)
(Γ fill K (App e2 e) log t : τ)
Γ (fill K (Case (InjR e) e1 e2)) log t : τ.
({E,E;Γ} fill K (App e2 e) log t : τ)
{E,E;Γ} (fill K (Case (InjR e) e1 e2)) log t : τ.
Proof.
iIntros (?) "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
......@@ -240,33 +238,33 @@ Section properties.
end. done.
Qed.
Lemma bin_log_related_if_false_l Γ K e1 e2 t τ
Lemma bin_log_related_if_true_masked_l Γ E1 E2 K e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
(Γ fill K e2 log t : τ)
Γ (fill K (If (# false) e1 e2)) log t : τ.
({E1,E2;Γ} fill K e1 log t : τ)
{E1,E2;Γ} (fill K (If (# true) e1 e2)) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
iApply (bin_log_pure_masked_l with "Hlog"); auto.
- do 3 eexists. econstructor; eauto.
- by inversion 1.
Qed.
Lemma bin_log_related_if_true_masked_l Γ E1 E2 (K : list ectx_item) (e1 e2 : expr) t τ
Lemma bin_log_related_if_false_l Γ E K e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
({E1,E2;Γ} fill K e1 log t : τ)
{E1,E2;Γ} (fill K (If (# true) e1 e2)) log t : τ.
({E,E;Γ} fill K e2 log t : τ)
{E,E;Γ} (fill K (If (# false) e1 e2)) log t : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_masked_l with "Hlog"); auto.
- do 3 eexists. econstructor; eauto.
- by inversion 1.
iApply (bin_log_pure_l with "Hlog"); auto; intros; simpl.
- do 3 eexists. econstructor; eauto.
- match goal with
| H : head_step _ _ _ _ _ |- _ => inversion H
end. done.
Qed.
Lemma bin_log_related_if_false_masked_l Γ E1 E2 (K : list ectx_item) (e1 e2 : expr) t τ
Lemma bin_log_related_if_false_masked_l Γ E1 E2 K e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2) :
({E1,E2;Γ} fill K e2 log t : τ)
......@@ -290,29 +288,29 @@ Section properties.
end. done.
Qed.
(** Stateful reductions *)
Lemma bin_log_related_step_l Φ K Γ E1 e1 e2 τ
(** *** Stateful reductions *)
Lemma bin_log_related_step_l Φ Γ E K e1 e2 τ
(Hclosed1 : Closed e1) :
(|={E1}=> WP e1 @ E1 {{ Φ }}) -
( v, Φ v - {E1,E1;Γ} fill K (of_val v) log e2 : τ) -
{E1,E1;Γ} fill K e1 log e2 : τ.
(|={E}=> WP e1 @ E {{ Φ }}) -
( v, Φ v - {E,E;Γ} fill K (of_val v) log e2 : τ) -
{E,E;Γ} fill K e1 log e2 : τ.
Proof.
iIntros "He Hlog".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
rewrite /env_subst fill_subst /=.
iApply (wp_bind (subst_ctx _ K)).
iMod "He". iModIntro.
iApply (wp_mask_mono E1); auto.
iApply (wp_mask_mono E); auto.
rewrite Closed_subst_p_id.
iApply (wp_wand with "He").
iIntros (v) "Hv".
iSpecialize ("Hlog" $! v with "Hv Hs [HΓ]"); first by iFrame.
iSpecialize ("Hlog" with "Hj"). simpl.
rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
iApply fupd_wp. iApply (fupd_mask_mono E1); auto.
iApply fupd_wp. iApply (fupd_mask_mono E); auto.
Qed.
Lemma bin_log_related_wp_atomic_l K Γ (E1 E2 : coPset) e1 e2 τ
Lemma bin_log_related_wp_atomic_l Γ (E1 E2 : coPset) K e1 e2 τ
(Hatomic : atomic e1)
(Hclosed1 : Closed e1) :
(|={E1,E2}=> WP e1 @ E2 {{ v,
......@@ -335,7 +333,7 @@ Section properties.
by iMod "Hlog".
Qed.
Lemma bin_log_related_bind_l K Γ E e1 e2 τ
Lemma bin_log_related_bind_l Γ E K e1 e2 τ
(Hclosed1 : Closed e1) :
(WP e1 @ E {{ v,
{E,E;Γ} fill K (of_val v) log e2 : τ }})%I -
......@@ -355,7 +353,7 @@ Section properties.
done.
Qed.
Lemma bin_log_related_step_atomic_l {A} (Φ : A val iProp Σ) K Γ E1 E2 e1 e2 τ
Lemma bin_log_related_step_atomic_l {A} (Φ : A val iProp Σ) Γ E1 E2 K e1 e2 τ
(Hatomic : atomic e1)
(Hclosed1 : Closed e1) :
(|={E1,E2}=> (a : A), WP e1 @ E2 {{ v, Φ a v }}
......@@ -390,11 +388,11 @@ Section properties.
end;
try done.
Lemma bin_log_related_fork_l (Γ : stringmap type) K E1 (e t : expr) (τ : type)
Lemma bin_log_related_fork_l Γ E K (e t : expr) (τ : type)
(Hclosed : Closed e) :
(WP e {{ _, True }}) -
{E1,E1;Γ} fill K (Lit Unit) log t : τ -
{E1,E1;Γ} fill K (Fork e) log t : τ.
{E,E;Γ} fill K (Lit Unit) log t : τ -
{E,E;Γ} fill K (Fork e) log t : τ.
Proof.
iIntros "Hsafe Hlog".
pose (Φ:=(fun w => w = UnitV)%I : val -> iProp Σ).
......@@ -425,7 +423,7 @@ Section properties.
iApply ("Hlog" $! l with "Hl").
Qed.
Lemma bin_log_related_alloc_l' Γ K E e v t τ
Lemma bin_log_related_alloc_l' Γ E K e v t τ
(Heval : to_val e = Some v) :
( (l : loc), l ↦ᵢ v - {E,E;Γ} fill K (Loc l) log t : τ)%I
- {E,E;Γ} fill K (Alloc e) log t : τ.
......@@ -434,7 +432,7 @@ Section properties.
iApply (bin_log_related_alloc_l); auto. assumption.
Qed.
Lemma bin_log_related_load_l E1 E2 Γ K l t τ :
Lemma bin_log_related_load_l Γ E1 E2 K l t τ :
(|={E1,E2}=> v',
(l ↦ᵢ v')
(l ↦ᵢ v' - ({ E2,E1; Γ } fill K (of_val v') log t : τ)))%I
......@@ -453,7 +451,7 @@ Section properties.
iApply "Hlog". done.
Qed.
Lemma bin_log_related_load_l' Γ K E1 l v' t τ :
Lemma bin_log_related_load_l' Γ E1 K l v' t τ :
(l ↦ᵢ v') -
(l ↦ᵢ v' - {E1,E1;Γ} fill K (of_val v') log t : τ)
- {E1,E1;Γ} fill K (Load (Loc l)) log t : τ.
......@@ -465,7 +463,7 @@ Section properties.
by iFrame.
Qed.
Lemma bin_log_related_store_l Γ K E1 E2 l e v' t τ :
Lemma bin_log_related_store_l Γ E1 E2 K l e v' t τ :
(to_val e = Some v')
(|={E1,E2}=> v, (l ↦ᵢ v)
(l ↦ᵢ v' - {E2,E1;Γ} fill K (Lit Unit) log t : τ))
......@@ -485,7 +483,7 @@ Section properties.
iApply ("Hlog" with "Hl").
Qed.
Lemma bin_log_related_store_l' Γ K E l e v v' t τ :
Lemma bin_log_related_store_l' Γ E K l e v v' t τ :
(to_val e = Some v')
(l ↦ᵢ v) -
(l ↦ᵢ v' - {E,E;Γ} fill K (Lit Unit) log t : τ)
......@@ -496,7 +494,7 @@ Section properties.
iModIntro. iExists v. iFrame.
Qed.
Lemma bin_log_related_cas_l Γ K E1 E2 l e1 e2 v1 v2 t τ :
Lemma bin_log_related_cas_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
(to_val e1 = Some v1)
(to_val e2 = Some v2)
(|={E1,E2}=> v', (l ↦ᵢ v')
......@@ -534,7 +532,7 @@ Section properties.
iApply ("Hlog_fail" with "[] Hl"); auto.
Qed.
Lemma bin_log_related_cas_fail_l Γ K E1 E2 l e1 e2 v1 v2 t τ :
Lemma bin_log_related_cas_fail_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
(to_val e1 = Some v1)
(to_val e2 = Some v2)
(|={E1,E2}=> v', (l ↦ᵢ v') v' v1
......@@ -555,7 +553,7 @@ Section properties.
iApply ("Hlog" with "Hl").
Qed.
Lemma bin_log_related_cas_fail_l' Γ K E l e1 e2 v1 v2 v' t τ :
Lemma bin_log_related_cas_fail_l' Γ E K l e1 e2 v1 v2 v' t τ :
(to_val e1 = Some v1)
(to_val e2 = Some v2)
(v' v1)
......@@ -568,7 +566,7 @@ Section properties.
iModIntro. iExists v'. iFrame "Hl Hlog". eauto.
Qed.
Lemma bin_log_related_cas_suc_l Γ K E1 E2 l e1 e2 v1 v2 t τ :
Lemma bin_log_related_cas_suc_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
(to_val e1 = Some v1)
(to_val e2 = Some v2)
(|={E1,E2}=> (l ↦ᵢ v1)
......@@ -589,13 +587,13 @@ Section properties.
iApply ("Hlog" with "Hl").
Qed.
Lemma bin_log_related_cas_suc_l' Γ K l e1 e2 v1 v2 v' t τ :
Lemma bin_log_related_cas_suc_l' Γ E K l e1 e2 v1 v2 v' t τ :
(to_val e1 = Some v1)
(to_val e2 = Some v2)
(v' = v1)
(l ↦ᵢ v') -
(l ↦ᵢ v2 - Γ fill K (# true) log t : τ)
- Γ fill K (CAS (Loc l) e1 e2) log t : τ.
(l ↦ᵢ v2 - {E,E;Γ} fill K (# true) log t : τ)
- {E,E;Γ} fill K (CAS (Loc l) e1 e2) log t : τ.
Proof.
iIntros (???) "Hl Hlog". subst.
iApply bin_log_related_cas_suc_l; eauto.
......@@ -622,7 +620,7 @@ Section properties.
iDestruct ("Hlog" with "Hs [HΓ] Hj") as "Hlog"; auto.
Qed.
Lemma bin_log_related_rec_r Γ K E1 E2 f x e e' t v' τ
Lemma bin_log_related_rec_r Γ E1 E2 K f x e e' t v' τ
(Hspec : nclose specN E1)
(Hclosed : Closed (x :b: f :b: ) e) :
(to_val e' = Some v')
......@@ -641,12 +639,41 @@ Section properties.
{ econstructor; eauto. }
Qed.
(* TODO *)
(* Lemma bin_log_related_tlam_r Γ K e e' v' τ *)
(* Lemma bin_log_related_Fold_r Γ K e e' v' τ *)
(* Lemma bin_log_related_Pack_r Γ K e e' v' τ *)
Lemma bin_log_related_tlam_r Γ E1 E2 K e t τ
(Hclosed : Closed e)
(Hspec : nclose specN E1) :
{E1,E2;Γ} t log fill K e : τ
{E1,E2;Γ} t log fill K (TApp (TLam e)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Lemma bin_log_related_fold_r Γ E1 E2 K e v t τ
(Hval : to_val e = Some v)
(Hspec : nclose specN E1) :
{E1,E2;Γ} t log fill K e : τ
{E1,E2;Γ} t log fill K (Unfold (Fold e)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Lemma bin_log_related_fst_r Γ K E1 E2 e v1 v2 τ
Lemma bin_log_related_pack_r Γ E1 E2 K e e' v t τ
(Hclosed : Closed e')
(Hval : to_val e = Some v)
(Hspec : nclose specN E1) :
{E1,E2;Γ} t log fill K (App e' e) : τ
{E1,E2;Γ} t log fill K (Unpack (Pack e) e') : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Lemma bin_log_related_fst_r Γ E1 E2 K e v1 v2 τ
(Hspec : nclose specN E1) :
{E1,E2;Γ} e log (fill K (of_val v1)) : τ
{E1,E2;Γ} e log (fill K (Fst (Pair (of_val v1) (of_val v2)))) : τ.
......@@ -656,7 +683,7 @@ Section properties.
{ econstructor; eauto. }
Qed.
Lemma bin_log_related_snd_r Γ K E1 E2 e v1 v2 τ
Lemma bin_log_related_snd_r Γ E1 E2 K e v1 v2 τ
(Hspec : nclose specN E1) :
{E1,E2;Γ} e log (fill K (of_val v2)) : τ
{E1,E2;Γ} e log (fill K (Snd (Pair (of_val v1) (of_val v2)))) : τ.
......@@ -666,9 +693,31 @@ Section properties.
{ econstructor; eauto. }
Qed.
(* TODO *)
(* Lemma bin_log_related_inl_r Γ K e e' v' τ *)
(* Lemma bin_log_related_inr_r Γ K e e' v' τ *)
Lemma bin_log_related_inl_r Γ E1 E2 K e v e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2)
(Hval : to_val e = Some v)
(Hspec : nclose specN E1) :
{E1,E2;Γ} t log (fill K (App e1 e)) : τ
{E1,E2;Γ} t log (fill K (Case (InjL e) e1 e2)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Lemma bin_log_related_inr_r Γ E1 E2 K e v e1 e2 t τ
(Hclosed1 : Closed e1)
(Hclosed2 : Closed e2)
(Hval : to_val e = Some v)
(Hspec : nclose specN E1) :
{E1,E2;Γ} t log (fill K (App e2 e)) : τ
{E1,E2;Γ} t log (fill K (Case (InjR e) e1 e2)) : τ.
Proof.
iIntros "Hlog".
iApply (bin_log_pure_r with "Hlog"); auto; intros.
{ econstructor; eauto. }
Qed.
Lemma bin_log_related_if_true_r Γ K E1 E2 e e1 e2 τ
(Hspec : nclose specN E1)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment