• Dan Frumin's avatar
    Strengthen `related_bind` · bf3aca9a
    Dan Frumin authored
    We define a stronger rule `related_bind_up`, in which there is a baked
    in semantic type `R`. The idea here is that we don't actually require
    the expressions that we bind to have the same syntactic type.
    
    ```
      {E;R::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ
    ∗ (∀ vv, ⟦ τ ⟧ (R::Δ) vv -∗ {E;Δ;Γ} ⊨ K[v1] ≤log≤ K'[v2] : τ')
    ____________________________________________________________
      {E;Δ;Γ} ⊨ K[e1] ≤log≤ K'[e2] : τ'
    ```
    
    We can then use `bin_log_related_weaken_2` to prove the original
    binding rule.
    
    The advantages of the new rule is that it allows us to prove the
    following compatibility rule for seq:
    
    ```
    {E;(R::Δ);⤉Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
    {E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
    {E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
    ```
    
    The idea here is that we can also pick any *semantic* type to related
    e1 and e1'. For instance, if both e1 and e1' are expressions of type
    Nat then it is not necessarily the case that we can relate them at
    that type -- they might reduce to two different numerals -- but
    it *should* be the case that we can relate their effects, if it makes
    sense. E.g.
    
    ((#l <- #1;; #0) ;; e) ≤ ((#l <- #1;; #1) ;; e)
    bf3aca9a
Name
Last commit
Last update
docs Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
comments.org Loading commit data...