diff --git a/comments.org b/comments.org new file mode 100644 index 0000000000000000000000000000000000000000..8983079caf6d68bff453fa6ffdc4d32391e22c38 --- /dev/null +++ b/comments.org @@ -0,0 +1,56 @@ +* Rules that didn't make it +** A binding rule for the semantic judgment that /nearly/ works. +A rule that we would like to have +#+BEGIN_SRC +WP e {{ v, {E,E;Γ} ⊧ K[v] ≤ e₂ : τ }} +----------------------------------------- +{E,E;Γ} ⊧ K[e₁] ≤ e₂ : τ +#+END_SRC +However, this rule is too weak. Consider a derivation where =e₁= is +atomic and we want to open an invariant to symbolically execute it. +#+BEGIN_SRC +|={E1,E2}=> WP e {{ v, |={E2,E1}=> {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ }} +---------------------------------------------------------------- wp-atomic +WP e {{ v, {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ }}_E1 +----------------------------------------- +{E1,E1;Γ} ⊧ K[e₁] ≤ e₂ : τ +#+END_SRC +After employing such reasoning we can open up an invariant, and +symbolically execute =e₁=. But then we are left with +#+BEGIN_SRC +|={E2,E1}=> {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ +#+END_SRC +which means that we have to close the invariant *now*. However, it +might be the case that we need to symbolically execute =e₂= in order +to restore the invariant before closing it. +* Assorted +** Why do we have a single =bin_log_related_cas_l=? +=bin_log_related_cas_l= is a rule in [[file:F_mu_ref_conc/relational_properties.v]] + +We already have =bin_log_related_cas_suc_l= and +=bin_log_related_cas_fail_l=. However, those rules are not sufficient +for our purposes, as we might not know whether the CAS succeeds +/before/ we open the invariant. + +Example: proof of =bin_log_FG_increment_logatomic= in counter.v +** subst_p_rec with binders +#+BEGIN_SRC + Lemma subst_p_rec (x f : binder) e1 e2 e `{Closed ∅ e2} : + subst_p (<[x:=e2]>{[f:=(Rec f x e1)]}) e = + subst' f (Rec f x e1) (subst' x e2 e). +#+END_SRC +We need a version of this lemma with x and f binders +in order to prove the compatibility lemma for lambdas + +#+BEGIN_SRC +□ (<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ) ⊨ e ≤log≤ e' : τ2) -∗ +Γ ⊨ Rec f x e ≤log≤ Rec f x e' : TArrow τ1 τ2. +#+END_SRC + +To show tht (rec f x e, rec f x e') are related, we use the definition +of the arrow type, so we have some values (v, v') related at τ1. Then +we would like to use the hypothesis by inserting (v, v') in the +environment substitution. But then we have =subst_p (<[x:=(v,v')]> +...) e=. You would like to convert that to =subst' x ..= so that one +can actually use the hypothesis. +