Commit ab35b735 by Dan Frumin

### Simplify the notation for the relational judements

```{E,E;Δ,Γ} ⊨ ... => {E;Δ,Γ} ⊨ ...
{⊤,⊤;Δ,Γ} ⊨ ... => {Δ,Γ} ⊨ ...```
parent cd3dd884
 ... ... @@ -121,8 +121,8 @@ Section heapify_refinement. Lemma heapify_refinement_ez Γ E1 b1 b2 : ↑logrelN ⊆ E1 → {E1,E1;Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗ {E1,E1;Δ;Γ} ⊨ heapify b1 ≤log≤ heapify b2 : bitτ. {E1;Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗ {E1;Δ;Γ} ⊨ heapify b1 ≤log≤ heapify b2 : bitτ. Proof. iIntros (?) "Hb1b2". iApply bin_log_related_app; eauto. ... ...
 ... ... @@ -77,8 +77,8 @@ Section CG_Counter. Lemma bin_log_FG_increment_l Γ K E x (n : nat) t τ : x ↦ᵢ #n -∗ (x ↦ᵢ # (S n) -∗ {E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ) -∗ {E,E;Δ;Γ} ⊨ fill K (FG_increment #x #()) ≤log≤ t : τ. (x ↦ᵢ # (S n) -∗ {E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ) -∗ {E;Δ;Γ} ⊨ fill K (FG_increment #x #()) ≤log≤ t : τ. Proof. iIntros "Hx Hlog". iApply bin_log_related_wp_l. ... ... @@ -146,7 +146,7 @@ Section CG_Counter. ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧ (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗ {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ)) -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment \$/ LitV (Loc x)) #()) ≤log≤ t : τ). -∗ ({E1;Δ;Γ} ⊨ fill K ((FG_increment \$/ LitV (Loc x)) #()) ≤log≤ t : τ). Proof. iIntros "HP #H". iLöb as "IH". ... ... @@ -189,7 +189,7 @@ Section CG_Counter. ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧ (∀ m : nat, x ↦ᵢ #m ∗ R m -∗ {E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)) -∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read \$/ LitV (Loc x)) #()) ≤log≤ t : τ. -∗ {E1;Δ;Γ} ⊨ fill K ((counter_read \$/ LitV (Loc x)) #()) ≤log≤ t : τ. Proof. iIntros "#H". unfold counter_read. unlock. simpl. ... ... @@ -205,7 +205,7 @@ Section CG_Counter. (* TODO: try to use with_lock rules *) Lemma FG_CG_increment_refinement l cnt cnt' Γ : inv counterN (counter_inv l cnt cnt') -∗ {⊤,⊤;Δ;Γ} ⊨ FG_increment \$/ LitV (Loc cnt) ≤log≤ CG_increment \$/ LitV (Loc cnt') \$/ LitV (Loc l) : TArrow TUnit TUnit. {Δ;Γ} ⊨ FG_increment \$/ LitV (Loc cnt) ≤log≤ CG_increment \$/ LitV (Loc cnt') \$/ LitV (Loc l) : TArrow TUnit TUnit. Proof. iIntros "#Hinv". iApply bin_log_related_arrow_val. ... ... @@ -236,7 +236,7 @@ Section CG_Counter. Lemma counter_read_refinement l cnt cnt' Γ : inv counterN (counter_inv l cnt cnt') -∗ {⊤,⊤;Δ;Γ} ⊨ counter_read \$/ LitV (Loc cnt) ≤log≤ counter_read \$/ LitV (Loc cnt') : TArrow TUnit TNat. {Δ;Γ} ⊨ counter_read \$/ LitV (Loc cnt) ≤log≤ counter_read \$/ LitV (Loc cnt') : TArrow TUnit TNat. Proof. iIntros "#Hinv". iApply bin_log_related_arrow_val. ... ... @@ -262,7 +262,7 @@ Section CG_Counter. Qed. Lemma FG_CG_counter_refinement : {⊤,⊤;Δ;∅} ⊨ FG_counter ≤log≤ CG_counter : {Δ;∅} ⊨ FG_counter ≤log≤ CG_counter : TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)). Proof. unfold FG_counter, CG_counter. ... ...
 ... ... @@ -38,8 +38,8 @@ Section Refinement. Lemma rand_l Δ Γ E1 K ρ t τ : ↑choiceN ⊆ E1 → spec_ctx ρ -∗ (∀ b : bool, {E1,E1;Δ;Γ} ⊨ fill K #b ≤log≤ t : τ) -∗ {E1,E1;Δ;Γ} ⊨ fill K (rand #()) ≤log≤ t : τ. spec_ctx ρ -∗ (∀ b : bool, {E1;Δ;Γ} ⊨ fill K #b ≤log≤ t : τ) -∗ {E1;Δ;Γ} ⊨ fill K (rand #()) ≤log≤ t : τ. Proof. iIntros (?) "#Hs Hlog". unfold rand. unlock. simpl. ... ...
 ... ... @@ -72,8 +72,8 @@ Section lockG_rules. Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ E K t τ : R -∗ ▷(∀ (lk : loc) γ, is_lock γ #lk R -∗ ({E,E;Δ;Γ} ⊨ fill K #lk ≤log≤ t: τ)) -∗ {E,E;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t: τ. -∗ ({E;Δ;Γ} ⊨ fill K #lk ≤log≤ t: τ)) -∗ {E;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t: τ. Proof. iIntros "HR Hlog". iApply bin_log_related_wp_l. ... ... @@ -90,8 +90,8 @@ Section lockG_rules. is_lock γ #lk R -∗ locked γ -∗ R -∗ ▷({E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗ {E,E;Δ;Γ} ⊨ fill K (release #lk) ≤log≤ t: τ. ▷({E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗ {E;Δ;Γ} ⊨ fill K (release #lk) ≤log≤ t: τ. Proof. iIntros (?) "Hlock Hlocked HR Hlog". iDestruct "Hlock" as (l) "[% #?]"; simplify_eq. ... ... @@ -109,8 +109,8 @@ Section lockG_rules. Lemma bin_log_related_acquire_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ : ↑N ⊆ E → is_lock γ #lk R -∗ ▷(locked γ -∗ R -∗ {E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗ {E,E;Δ;Γ} ⊨ fill K (acquire #lk) ≤log≤ t: τ. ▷(locked γ -∗ R -∗ {E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗ {E;Δ;Γ} ⊨ fill K (acquire #lk) ≤log≤ t: τ. Proof. iIntros (?) "#Hlock Hlog". iLöb as "IH". ... ... @@ -167,8 +167,8 @@ Section lock_rules_r. Qed. Lemma bin_log_related_newlock_l_simp Γ K t τ : (∀ l : loc, l ↦ᵢ #false -∗ {E1,E1;Δ;Γ} ⊨ fill K #l ≤log≤ t : τ) -∗ {E1,E1;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t : τ. (∀ l : loc, l ↦ᵢ #false -∗ {E1;Δ;Γ} ⊨ fill K #l ≤log≤ t : τ) -∗ {E1;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t : τ. Proof. iIntros "Hlog". unfold newlock. unlock. ... ... @@ -209,8 +209,8 @@ Section lock_rules_r. Lemma bin_log_related_acquire_suc_l Γ K l t τ : l ↦ᵢ #false -∗ (l ↦ᵢ #true -∗ {E1,E1;Δ;Γ} ⊨ fill K (#()) ≤log≤ t : τ) -∗ {E1,E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ. (l ↦ᵢ #true -∗ {E1;Δ;Γ} ⊨ fill K (#()) ≤log≤ t : τ) -∗ {E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ. Proof. iIntros "Hl Hlog". unfold acquire. unlock. ... ... @@ -226,8 +226,8 @@ Section lock_rules_r. Lemma bin_log_related_acquire_fail_l Γ K l t τ : l ↦ᵢ #true -∗ (l ↦ᵢ #false -∗ {E1,E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ) -∗ {E1,E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ. (l ↦ᵢ #false -∗ {E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ) -∗ {E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ. Proof. iIntros "Hl Hlog". iLöb as "IH". ... ...
 ... ... @@ -36,9 +36,9 @@ Section contents. Lemma bin_log_related_or Δ Γ E e1 e2 e1' e2' : ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or e1 e2 ≤log≤ or e1' e2' : TUnit. {E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ or e1 e2 ≤log≤ or e1' e2' : TUnit. Proof. iIntros (?) "He1 He2". iApply (bin_log_related_app with "[He1] He2"). ... ... @@ -48,8 +48,8 @@ Section contents. Lemma bin_log_or_choice_1_r_val Δ Γ E (v1 v1' v2 : val) : ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1' v2 : TUnit. {E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1' v2 : TUnit. Proof. iIntros (?) "Hlog". unlock or. repeat rel_rec_r. ... ... @@ -64,7 +64,7 @@ Section contents. Lemma bin_log_or_choice_1_r_val_typed Δ Γ E (v1 v2 : val) : ↑logrelN ⊆ E → Γ ⊢ₜ v1 : TArrow TUnit TUnit → {E,E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit. {E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit. Proof. iIntros (??). iApply bin_log_or_choice_1_r_val; eauto. ... ... @@ -73,8 +73,8 @@ Section contents. Lemma bin_log_or_choice_1_r Δ Γ E (e1 e1' : expr) (v2 : val) : ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ e1 #() ≤log≤ or e1' v2 : TUnit. {E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ e1 #() ≤log≤ or e1' v2 : TUnit. Proof. iIntros (?) "Hlog". rel_bind_l e1. ... ... @@ -90,7 +90,7 @@ Section contents. ↑logrelN ⊆ E → Closed ∅ e1 → Γ ⊢ₜ e1 : TUnit → {E,E;Δ;Γ} ⊨ e1 ≤log≤ or (λ: <>, e1) v2 : TUnit. {E;Δ;Γ} ⊨ e1 ≤log≤ or (λ: <>, e1) v2 : TUnit. Proof. iIntros (???). unlock or. repeat rel_rec_r. ... ... @@ -118,9 +118,9 @@ Section contents. Lemma bin_log_or_commute Δ Γ E (v1 v1' v2 v2' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1' v2' : TUnit. {E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1' v2' : TUnit. Proof. iIntros (??) "Hv1 Hv2". unlock or. repeat rel_rec_r. repeat rel_rec_l. ... ... @@ -155,8 +155,8 @@ Section contents. Lemma bin_log_or_idem_r Δ Γ E (v v' : val) : ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v #() ≤log≤ or v' v' : TUnit. {E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ v #() ≤log≤ or v' v' : TUnit. Proof. iIntros (?) "Hlog". by iApply bin_log_or_choice_1_r_val. ... ... @@ -166,7 +166,7 @@ Section contents. Closed ∅ e → ↑logrelN ⊆ E → Γ ⊢ₜ e : TUnit → {E,E;Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) (λ: <>, e) : TUnit. {E;Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) (λ: <>, e) : TUnit. Proof. iIntros (???). iPoseProof (bin_log_or_choice_1_r_body Δ _ _ e (λ: <>, e)) as "HZ"; eauto. ... ... @@ -176,8 +176,8 @@ Section contents. Lemma bin_log_or_idem_l Δ Γ E (v v' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or v v ≤log≤ v' #() : TUnit. {E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ or v v ≤log≤ v' #() : TUnit. Proof. iIntros (??) "Hlog". unlock or. repeat rel_rec_l. ... ... @@ -203,8 +203,8 @@ Section contents. Lemma bin_log_or_bot_l Δ Γ E (v v' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or v bot ≤log≤ v' #() : TUnit. {E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ or v bot ≤log≤ v' #() : TUnit. Proof. iIntros (??) "Hlog". unlock or. repeat rel_rec_l. ... ... @@ -228,8 +228,8 @@ Section contents. Lemma bin_log_or_bot_r Δ Γ E (v v' : val) : ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v #() ≤log≤ or v' bot : TUnit. {E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ v #() ≤log≤ or v' bot : TUnit. Proof. iIntros (?) "Hlog". iApply bin_log_or_choice_1_r_val; eauto. ... ... @@ -238,10 +238,10 @@ Section contents. Lemma bin_log_or_assoc1 Δ Γ E (v1 v1' v2 v2' v3 v3' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v3 ≤log≤ v3' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or v1 (λ: <>, or v2 v3) ≤log≤ or (λ: <>, or v1' v2') v3' : TUnit. {E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ v3 ≤log≤ v3' : TArrow TUnit TUnit -∗ {E;Δ;Γ} ⊨ or v1 (λ: <>, or v2 v3) ≤log≤ or (λ: <>, or v1' v2') v3' : TUnit. Proof. iIntros (??) "Hv1 Hv2 Hv3". unlock or. simpl. ... ... @@ -304,7 +304,7 @@ Section contents. Closed {["x"]} e → ↑logrelN ⊆ E → Γ ⊢ₜ subst "x" v e : τ → {E,E;Δ;Γ} ⊨ let: "x" := v in e ≤log≤ subst "x" v e : τ. {E;Δ;Γ} ⊨ let: "x" := v in e ≤log≤ subst "x" v e : τ. Proof. iIntros (?? Hτ). assert (Closed ∅ (Rec BAnon "x" e)). ... ... @@ -317,7 +317,7 @@ Section contents. Closed {["x"]} e → ↑logrelN ⊆ E → Γ ⊢ₜ subst "x" v e : τ → {E,E;Δ;Γ} ⊨ subst "x" v e ≤log≤ (let: "x" := v in e) : τ. {E;Δ;Γ} ⊨ subst "x" v e ≤log≤ (let: "x" := v in e) : τ. Proof. iIntros (?? Hτ). assert (Closed ∅ (Rec BAnon "x" e)). ... ...
 ... ... @@ -26,9 +26,9 @@ Section compatibility. Lemma bin_log_related_par Δ Γ E e1 e2 e1' e2' τ1 τ2 : ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit τ1 -∗ {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit τ2 -∗ {E,E;Δ;Γ} ⊨ par e1 e2 ≤log≤ par e1' e2' : TProd τ1 τ2. {E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit τ1 -∗ {E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit τ2 -∗ {E;Δ;Γ} ⊨ par e1 e2 ≤log≤ par e1' e2' : TProd τ1 τ2. Proof. iIntros (?) "He1 He2". iApply (bin_log_related_app with "[He1] He2"). ... ...
 ... ... @@ -199,8 +199,8 @@ Section refinement. Definition bot : val := rec: "bot" <> := "bot" #(). Lemma bot_l ϕ Δ Γ E K t τ : (ϕ -∗ {E,E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗ {E,E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ. (ϕ -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗ {E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ. Proof. iIntros "Hlog". iLöb as "IH". ... ... @@ -320,7 +320,7 @@ Section refinement. Lemma profiled_g `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ : inv shootN (i6 c1 c2 γ γ') -∗ ⟦ τg ⟧ Δ (g1, g2) -∗ {⊤,⊤;Δ;Γ} ⊨ {Δ;Γ} ⊨ (FG_increment #c1 #() ;; g1 #()) ≤log≤ (FG_increment #c2 #() ;; g2 #()) : TUnit. ... ... @@ -405,7 +405,7 @@ Section refinement. Lemma profiled_g' `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ : inv shootN (i6 c1 c2 γ γ') -∗ ⟦ τg ⟧ Δ (g1, g2) -∗ {⊤,⊤;Δ;Γ} ⊨ {Δ;Γ} ⊨ (λ: <>, FG_increment #c1 #() ;; g1 #()) ≤log≤ (λ: <>, FG_increment #c2 #() ;; g2 #()) : τg. ... ...
This diff is collapsed.
 ... ... @@ -36,12 +36,17 @@ Notation "⟦ Γ ⟧*" := (interp_env Γ). Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" := (bin_log_related E1 E2 Δ Γ e%E e'%E τ) (at level 74, E1,E2, e, e', τ at next level, format "'[hv' '{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'"). Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" := (∀ Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I (at level 74, E1,E2, e, e', τ at next level, format "'[hv' '{' E1 ',' E2 ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'"). (at level 74, E1 at level 50, E2 at next level, Δ at next level, Γ at next level, e, e', τ at next level, format "'[hv' '{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'"). Notation "'{' E ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" := (bin_log_related E E Δ Γ e%E e'%E τ) (at level 74, E at level 50, Δ at next level, Γ at next level, e, e', τ at next level, format "'[hv' '{' E ';' Δ ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'"). Notation "'{' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" := (bin_log_related ⊤ ⊤ Δ Γ e%E e'%E τ) (at level 74, Δ at level 50, Γ at next level, e, e', τ at next level, format "'[hv' '{' Δ ';' Γ '}' ⊨ '/ ' e '/' '≤log≤' '/ ' e' : τ ']'"). Notation "Γ ⊨ e '≤log≤' e' : τ" := (∀ Δ, bin_log_related ⊤ ⊤ Δ Γ e%E e'%E τ)%I (at level 74, e, e', τ at next level, ... ... @@ -163,7 +168,7 @@ Section related_facts. (* We need this to be able to open and closed invariants in front of logrels *) Lemma fupd_logrel E1 E2 Δ Γ e e' τ : ((|={E1,E2}=> ({E2,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)) ((|={E1,E2}=> ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)) -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I. Proof. rewrite bin_log_related_eq. ... ... @@ -186,7 +191,7 @@ Section related_facts. Global Instance elim_modal_logrel E1 E2 Δ Γ e e' P τ : ElimModal (|={E1,E2}=> P) P ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E2,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) | 10. ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) | 10. Proof. rewrite /ElimModal. iIntros "[HP HI]". iApply fupd_logrel. ... ... @@ -203,8 +208,8 @@ Section related_facts. Qed. Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 τ : {⊤,⊤;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗ {⊤,⊤;τi::Δ;Autosubst_Classes.subst (ren (+1)) <\$>Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)]. {Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗ {τi::Δ;Autosubst_Classes.subst (ren (+1)) <\$>Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)]. Proof. rewrite bin_log_related_eq /bin_log_related_def. iIntros "Hlog" (vvs ρ) "#Hs #HΓ". ... ... @@ -227,7 +232,7 @@ Section monadic. Context `{logrelG Σ}. Lemma related_ret E1 E2 Δ Γ e1 e2 τ `{Closed ∅ e1} `{Closed ∅ e2} : interp_expr E1 E1 ⟦ τ ⟧ Δ (e1,e2) -∗ {E2,E2;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ%I. interp_expr E1 E1 ⟦ τ ⟧ Δ (e1,e2) -∗ {E2;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ%I. Proof. iIntros "Hτ". rewrite bin_log_related_eq /bin_log_related_def. ... ... @@ -239,9 +244,9 @@ Section monadic. Qed. Lemma related_bind E Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) : ({E,E;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ) -∗ (∀ vv, ⟦ τ ⟧ Δ vv -∗ {E,E;Δ;Γ} ⊨ fill K (of_val (vv.1)) ≤log≤ fill K' (of_val (vv.2)) : τ') -∗ ({E,E;Δ;Γ} ⊨ fill K e1 ≤log≤ fill K' e2 : τ'). ({E;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ) -∗ (∀ vv, ⟦ τ ⟧ Δ vv -∗ {E;Δ;Γ} ⊨ fill K (of_val (vv.1)) ≤log≤ fill K' (of_val (vv.2)) : τ') -∗ ({E;Δ;Γ} ⊨ fill K e1 ≤log≤ fill K' e2 : τ'). Proof. iIntros "Hm Hf". rewrite bin_log_related_eq /bin_log_related_def. ... ...
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!