Commit 3f2ae145 by Dan Frumin

### Tweak the logrel notation

```Γ ⊧ e1 ≤ e2 : τ now means
∀ Δ, {⊤,⊤;Δ;Γ} ⊧ e1 ≤ e2 : τ```
parent 8b94528d
 ... ... @@ -277,17 +277,17 @@ Section bin_log_related_under_typed_ctx. (Closed (dom _ Γ) e) → (Closed (dom _ Γ) e') → typed_ctx K Γ τ Γ' τ' → (□ (∀ Δ, ({⊤,⊤;Δ;Γ} ⊨ e ≤log≤ e' : τ)) -∗ ∀ Δ, □ ({⊤,⊤;Δ;Γ'} ⊨ fill_ctx K e ≤log≤ fill_ctx K e' : τ'))%I. (□ (Γ ⊨ e ≤log≤ e' : τ) -∗ Γ' ⊨ fill_ctx K e ≤log≤ fill_ctx K e' : τ')%I. Proof. revert Γ τ Γ' τ' e e'. induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl. - inversion_clear 1; trivial. iIntros "#H". iIntros (Δ) "!#". by iApply "H". iIntros (Δ). by iApply "H". - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. specialize (IHK _ _ _ _ e e' H1 H2 Hx2). inversion Hx1; subst; simpl; try fold_interp; iIntros "#Hrel"; iIntros (Δ) "!#". iIntros (Δ). + iApply (bin_log_related_rec with "[-]"); auto; rewrite ?cons_binder_union. replace ({[x]} ∪ ({[f]} ∪ dom (gset string) _)) ... ...
 ... ... @@ -375,7 +375,9 @@ Section bin_log_def. Context `{logrelG Σ}. Notation D := (prodC valC valC -n> iProp Σ). Definition bin_log_related_def (E1 E2 : coPset) (Δ : list D) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := (∀ (vvs : stringmap (val * val)) ρ, Definition bin_log_related_def (E1 E2 : coPset) (Δ : list D) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := (∀ (vvs : stringmap (val * val)) ρ, spec_ctx ρ -∗ □ interp_env Γ ⊤ ⊤ Δ vvs -∗ interp_expr E1 E2 (interp ⊤ ⊤ τ) Δ ... ... @@ -389,8 +391,6 @@ End bin_log_def. 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). 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). (* Notation "Δ ',' Γ ⊨ e '≤log≤' e' : τ" := *) (* (bin_log_related ⊤ ⊤ [] Γ e e' τ) (at level 74, e, e', τ at next level). *) (∀ Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I (at level 74, E1,E2, e, e', τ at next level). Notation "Γ ⊨ e '≤log≤' e' : τ" := (bin_log_related ⊤ ⊤ [] Γ e%E e'%E τ) (at level 74, e, e', τ at next level). (∀ Δ, bin_log_related ⊤ ⊤ Δ Γ e%E e'%E τ)%I (at level 74, e, e', τ at next level).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!