Initial import of tactics for logrels

F_mu_ref_conc/examples/counter.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
 From iris.base_logic Require Import lib.auth.
 From iris_logrel.F_mu_ref_conc Require Export examples.lock.
-From iris_logrel.F_mu_ref_conc Require Import tactics soundness_binary relational_properties.
+From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
 From iris.program_logic Require Import adequacy.
 
 From iris_logrel.F_mu_ref_conc Require Import hax.
@@ -68,16 +68,15 @@ Section CG_Counter.
     {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (CG_increment (Loc x)) Unit) : τ.
   Proof.
     iIntros (?) "Hx Hlog".
-    rel_bind_r (CG_increment (#x))%E.
     unfold CG_increment. unlock. 
-    iApply bin_log_related_rec_r; auto. simpl.
-    iApply bin_log_related_rec_r; auto. simpl.
+    rel_rec_r.
+    rel_rec_r.
     rel_bind_r (Load (Loc x)).
     iApply (bin_log_related_load_r with "Hx");auto.
     iIntros "Hx". simpl.
-    rel_bind_r (BinOp Add _ _).
-    iApply (bin_log_related_binop_r); auto. simpl.
-    iApply (bin_log_related_store_r with "Hx"); auto.
+    rel_op_r.
+    rel_store_r.
+    by iApply "Hlog".
   Qed.
   
   Global Opaque CG_increment.
@@ -125,29 +124,20 @@ Section CG_Counter.
     (x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) -∗
     (x ↦ₛ (#nv S n) -∗ l ↦ₛ (#♭v false) -∗
       ({E1,E2;Γ} ⊨ t ≤log≤ fill K (Lit Unit) : τ)) -∗
-    {E1,E2;Γ} ⊨ t ≤log≤ fill K ((lamsubst (lamsubst CG_locked_increment (LocV x)) (LocV l)) Unit) : τ)%I.
+    {E1,E2;Γ} ⊨ t ≤log≤ fill K (((CG_locked_increment $/ (LocV x)) $/ (LocV l)) Unit)%E : τ)%I.
   Proof. 
     iIntros (?) "Hx Hl Hlog".
     unfold CG_locked_increment. unlock. simpl.
     rewrite !Closed_subst_id.
-    (* rel_bind_r (App _ (#x))%E. *)
-    (* iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id. *)
-    (* rel_bind_r (App _ (#l))%E. *)
-    (* iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.   *)
-    iApply bin_log_related_rec_r; eauto. simpl.
+    rel_rec_r.
     rel_bind_r (acquire #l).
     iApply (bin_log_related_acquire_r with "Hl"); eauto. iIntros "Hl". simpl.
-    iApply bin_log_related_rec_r; eauto. simpl.
+    rel_rec_r.
     rel_bind_r (CG_increment #x #())%E.
     iApply (bin_log_related_CG_increment_r with "Hx"); auto. simpl. iIntros "Hx".
-    iApply bin_log_related_rec_r; eauto. simpl.    
+    rel_rec_r.
     iApply (bin_log_related_release_r with "Hl"); eauto.
     by iApply "Hlog".
-    (* iApply (bin_log_related_with_lock_r Γ K E1 E2 (x ↦ₛ (#nv S n)) _ Unit Unit with "[Hx] Hl"); eauto.  *)
-    (* - simpl. by rewrite decide_left. *)
-    (* - iIntros (K') "Hlog". *)
-    (*   iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id. *)
-    (*   iApply (bin_log_related_CG_increment_r with "Hx"); auto. *)
   Qed.
  
   Global Opaque CG_locked_increment.
@@ -274,7 +264,7 @@ Section CG_Counter.
   Proof.
     iIntros "Hx Hlog".
     Transparent counter_read. unfold counter_read. unlock. simpl.
-    iApply bin_log_related_rec_r; auto. simpl.
+    rel_rec_r.    
     iApply (bin_log_related_load_r with "Hx"); auto.
     Opaque counter_read.
   Qed.
@@ -362,21 +352,11 @@ Section CG_Counter.
 
     iApply (bin_log_related_rec_l _ ⊤ []); auto.
     iNext. simpl.
-    rel_bind_r (App _ (#cnt')%E).
 
     Transparent CG_locked_increment.
     unfold CG_locked_increment. unlock.
-    iApply (bin_log_related_rec_r _ _); auto. simpl. rewrite !Closed_subst_id.
-    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl. rewrite !Closed_subst_id.
-
-    (* rel_bind_r (App _ (λ: "l", _))%E. *)
-
-    (* Transparent with_lock. unfold with_lock. unlock.     *)
-    (* iApply (bin_log_related_rec_r Γ); eauto. *)
-    (* { simpl. by rewrite decide_left. } *)
-    (* simpl. rewrite !Closed_subst_id. *)
-
-    (* iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id. *)
+    rel_rec_r.
+    rel_rec_r.
 
     iApply bin_log_related_arrow.
     iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
@@ -419,8 +399,8 @@ Section CG_Counter.
     iIntros "#Hinv".
     Transparent counter_read.
     unfold counter_read. unlock.
-    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
-    iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.
+    rel_rec_r.
+    rel_rec_l.
     iApply bin_log_related_arrow. iAlways.
     iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
     (* :( *)
@@ -453,27 +433,19 @@ 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 /=.
+    rel_rec_r.
+    rel_alloc_r as cnt' "Hcnt'".
     rel_bind_l (Alloc _).
     iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
     iIntros (cnt) "Hcnt".        
-    rel_bind_r (Alloc _).
-    iApply (bin_log_related_alloc_r); auto.
-    iIntros (cnt') "Hcnt' /=".
 
-    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
-    rewrite /= !Closed_subst_id /=.
+    rel_rec_r.
 
     unfold FG_counter_body. unlock.
-    iApply (bin_log_related_rec_l _ _ []); auto.
-    iNext. rewrite /= !Closed_subst_id /=.
+    rel_rec_l.
 
-    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. 
-    rewrite /= !Closed_subst_id /=.    
+    do 2 rel_rec_r.
 
     (* establishing the invariant *)
     iAssert (counter_inv l cnt cnt')

F_mu_ref_conc/examples/lateearlychoice.v

@@ -2,16 +2,11 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
 From iris.base_logic Require Import lib.auth.
 From iris_logrel.F_mu_ref_conc Require Export examples.lock.
-From iris_logrel.F_mu_ref_conc Require Import tactics soundness_binary relational_properties.
+From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
 From iris.program_logic Require Import adequacy.
 
 From iris_logrel.F_mu_ref_conc Require Import hax.
 
-Notation "'let:' x := e1 'in' e2" := (Let x%bind e1%E e2%E)
-  (at level 102, x at level 1, e1, e2 at level 200,
-   format "'[' '[hv' 'let:'  x  :=  '[' e1 ']'  'in'  ']' '/' e2 ']'") : expr_scope.
-Notation "e $! v" := (lamsubst e%E v%V) (at level 80) : expr_scope.
-
 Definition rand : val := λ: <>,
   let: "y" := (ref (#♭ false))
   in Fork ("y" <- #♭ true);;

F_mu_ref_conc/examples/lock.v

 From iris.proofmode Require Import tactics.
-From iris_logrel.F_mu_ref_conc Require Import tactics.
+From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics.
 From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary relational_properties notation.
 From iris.base_logic Require Import namespaces.
 
@@ -73,7 +73,8 @@ Section proof.
   Proof.
     iIntros "Hlog".
     unfold newlock.
-    iApply (bin_log_related_alloc_r); auto.
+    rel_alloc_r as l "Hl".
+    iApply ("Hlog" with "Hl").
   Qed.
 
   Global Opaque newlock.
@@ -100,11 +101,11 @@ Section proof.
   Proof.
     iIntros "Hl Hlog".
     unfold acquire.
-    iApply bin_log_related_rec_r; eauto. simpl.
+    rel_rec_r.
     rel_bind_r (CAS _ _ _).
     iApply (bin_log_related_cas_suc_r with "Hl"); auto.
-    iIntros "Hl". rewrite fill_app /=.
-    iApply bin_log_related_if_true_r; auto.
+    iIntros "Hl". simpl.
+    rel_if_r.
     by iApply "Hlog".
   Qed.
   
@@ -130,8 +131,9 @@ Section proof.
   Proof.
     iIntros "Hl Hlog".
     unfold release.
-    iApply (bin_log_related_rec_r); auto. simpl.
-    iApply (bin_log_related_store_r with "Hl"); auto.
+    rel_rec_r.
+    rel_store_r.
+    by iApply "Hlog".
   Qed.
 
   Global Opaque release.
@@ -187,7 +189,7 @@ Section proof.
     iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id.
     iApply (bin_log_related_rec_r); eauto. simpl. rewrite !Closed_subst_id.
     rel_bind_r (App acquire (Loc l)).
-    iApply (bin_log_related_acquire_r Γ (_ ++ K) l with "Hl"); auto.
+    iApply (bin_log_related_acquire_r Γ (_ :: K) l with "Hl"); auto.
     iIntros "Hl". simpl.
     iApply (bin_log_related_rec_r); eauto. simpl.
     rel_bind_r (App e ew).

F_mu_ref_conc/hax.v

@@ -9,6 +9,8 @@ Definition lamsubst (e : expr) (v : val) : expr :=
   | _ => e
   end.
 
+Notation "e $/ v" := (lamsubst e%E v%V) (at level 80) : expr_scope.
+
 Ltac inv_head_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)

F_mu_ref_conc/notation.v

@@ -67,4 +67,8 @@ Notation "'Λ:' e" := (TLam e%E)
 Notation "'Λ:' e" := (TLamV e%E)
   (at level 102, e at level 200) : val_scope.
 
+Notation "'let:' x := e1 'in' e2" := (Let x%bind e1%E e2%E)
+  (at level 102, x at level 1, e1, e2 at level 200,
+   format "'[' '[hv' 'let:'  x  :=  '[' e1 ']'  'in'  ']' '/' e2 ']'") : expr_scope.
+
 Coercion of_val : val >-> expr.

F_mu_ref_conc/rel_tactics.v

+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import coq_tactics sel_patterns.
+From iris.proofmode Require Export tactics.
+From iris_logrel.F_mu_ref_conc Require Import rules rules_binary.
+From iris_logrel.F_mu_ref_conc Require Export lang tactics logrel_binary relational_properties.
+Set Default Proof Using "Type".
+Import lang.
+
+
+Lemma tac_rel_bind_gen `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e e' t t' τ :
+  e = e' →
+  t = t' →
+  (Δ ⊢ bin_log_related E1 E2 Γ e' t' τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ e t τ).
+Proof.
+  intros. subst t e. assumption.
+Qed.
+
+Lemma tac_rel_bind_l `{heapIG Σ, !cfgSG Σ} e' K Δ E1 E2 Γ e t τ :
+  e = fill K e' →
+  (Δ ⊢ bin_log_related E1 E2 Γ (fill K e') t τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ e t τ).
+Proof. intros. eapply tac_rel_bind_gen; eauto. Qed.
+
+Lemma tac_rel_bind_r `{heapIG Σ, !cfgSG Σ} t' K Δ E1 E2 Γ e t τ :
+  t = fill K t' →
+  (Δ ⊢ bin_log_related E1 E2 Γ e (fill K t') τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ e t τ).
+Proof. intros. eapply tac_rel_bind_gen; eauto. Qed.
+
+Local Ltac tac_bind_helper :=
+  rewrite ?fill_app /=;
+  lazymatch goal with   
+  | |- fill ?K ?e = fill _ ?efoc =>
+     reshape_expr e ltac:(fun K' e' =>
+       unify e' efoc;
+       let K'' := eval cbn[app] in (K' ++ K) in
+       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
+  | |- ?e = fill _ ?efoc =>
+     reshape_expr e ltac:(fun K' e' =>
+       unify e' efoc;
+       replace e with (fill K' e') by (by rewrite ?fill_app))
+  end; reflexivity.
+
+Tactic Notation "rel_bind_l" open_constr(efoc) :=
+  iStartProof;
+  eapply (tac_rel_bind_l efoc);
+  [ tac_bind_helper
+  | (* new goal *) 
+  ].
+
+Tactic Notation "rel_bind_r" open_constr(efoc) :=
+  iStartProof;
+  eapply (tac_rel_bind_r efoc);
+  [ tac_bind_helper
+  | (* new goal *) 
+  ].
+
+Lemma tac_rel_store_l `{heapIG Σ, !cfgSG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e' v' K' Γ e t τ :
+  nclose N ⊆ E1 →
+  envs_lookup i1 Δ1 = Some (p, inv N P) →
+  E2 = E1 ∖ ↑N →
+  e = fill K' (Store (Loc l) e') →
+  to_val e' = Some v' →
+  envs_lookup nam Δ1 = None →
+  envs_lookup nam_cl Δ1 = None →
+  nam_cl ≠ nam →
+  Δ2 = envs_snoc (envs_snoc Δ1 false nam (▷ P)%I) false nam_cl (▷ P ={E1 ∖ ↑N,E1}=∗ True)%I →
+  (Δ2 ⊢ |={E2}=> ∃ v, ▷ (l ↦ᵢ v) ∗
+     (l ↦ᵢ v' -∗ bin_log_related E2 E1 Γ (fill K' (Lit Unit)) t τ)) →
+  (Δ1 ⊢ bin_log_related E1 E1 Γ e t τ).
+Proof.
+  intros ??????????.
+  rewrite -(idemp uPred_and Δ1).
+  rewrite {1}envs_lookup_sound'. 2: eassumption.
+  rewrite uPred.sep_elim_l uPred.always_and_sep_l.
+  rewrite inv_open. 2: eassumption.
+  subst e.
+  rewrite -(bin_log_related_store_l Γ E1 E2). 2: eassumption.
+  rewrite fupd_frame_r.
+  rewrite -(fupd_trans E1 E2 E2).
+  subst E2.
+  apply fupd_mono.  
+  rewrite -H9.
+  subst Δ2.
+  rewrite (envs_snoc_sound Δ1 false nam (▷P)) /=. 2: eassumption.
+  rewrite comm.
+  rewrite assoc.
+  rewrite uPred.wand_elim_l.
+  rewrite (envs_snoc_sound (envs_snoc Δ1 false nam (▷ P)) false nam_cl (▷ P ={E1 ∖ ↑N,E1}=∗ True)) //;
+          last first.
+  { rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
+  rewrite uPred.wand_elim_l.
+  done.
+Qed.
+
+Tactic Notation "rel_store_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
+  iStartProof;
+  eapply (tac_rel_store_l nam nam_cl);
+    [solve_ndisj || fail "rel_store_l: cannot prove 'nclose " N " ⊆ ?'"
+    |iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?" 
+    |try fast_done (* E2 = E1 \ ↑N *)
+    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
+    |try fast_done (* to_val e' = Some v *)
+    |try fast_done (* nam fresh *)
+    |try fast_done (* nam_cl fresh *)
+    |eauto (* nam =/= nam_cl *)
+    |env_cbv; reflexivity || fail "rel_store_l: this should not happen"
+    |(* new goal *)].
+
+Lemma tac_rel_store_r `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 E1 E2 i1 l t' v' K' Γ e t τ v :
+  nclose specN ⊆ E1 →
+  t = fill K' (Store (Loc l) t') →
+  to_val t' = Some v' →
+  envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I →
+  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) Δ1 = Some Δ2 →
+  (Δ2 ⊢ bin_log_related E1 E2 Γ e (fill K' (Lit Unit)) τ) →
+  (Δ1 ⊢ bin_log_related E1 E2 Γ e t τ).
+Proof.
+  intros ??????.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+  subst t.
+  rewrite (bin_log_related_store_r Γ K' E1 E2 l); [ | eassumption | eassumption ].
+  rewrite H5. 
+  apply uPred.wand_elim_l.
+Qed.
+
+Tactic Notation "rel_store_r" :=
+  iStartProof;
+  eapply (tac_rel_store_r);
+    [solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
+    |try fast_done (* to_val e' = Some v *)
+    |iAssumptionCore || fail "rel_store_l: cannot find ? ↦ₛ ?" 
+    |env_cbv; reflexivity || fail "rel_store_r: this should not happen"
+    |(* new goal *)].
+
+Lemma tac_rel_alloc_r `{heapIG Σ, !cfgSG Σ} Δ1 E1 E2  t' v' K' Γ e t τ :
+  nclose specN ⊆ E1 →
+  t = fill K' (Alloc t') →
+  to_val t' = Some v' →
+  (Δ1 ⊢ ∀ l, l ↦ₛ v' -∗ bin_log_related E1 E2 Γ e (fill K' (Loc l)) τ) →
+  (Δ1 ⊢ bin_log_related E1 E2 Γ e t τ).
+Proof.
+  intros ????.
+  subst t.
+  rewrite -(bin_log_related_alloc_r Γ K' E1 E2); eassumption.
+Qed.
+
+Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
+  iStartProof;
+  eapply (tac_rel_alloc_r);
+    [solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
+    |try fast_done (* to_val t' = Some v' *)
+    |simpl; iIntros (l) H (* new goal *)].
+
+Tactic Notation "rel_alloc_r" :=
+  let l := fresh in
+  let H := iFresh "H" in
+  rel_alloc_r as l H.
+
+
+Lemma tac_rel_rec_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e K' f x ef e' efbody v eres t τ :
+  e = fill K' (App ef e') →
+  ef = Rec f x efbody →
+  Closed (x :b: f :b: ∅) efbody →
+  to_val e' = Some v →
+  eres = subst' f ef (subst' x e' efbody) →
+  (Δ ⊢ ▷ bin_log_related E1 E1 Γ (fill K' eres) t τ) →
+  (Δ ⊢ bin_log_related E1 E1 Γ e t τ).
+Proof.
+  intros ??????.
+  subst e ef eres.
+  rewrite -(bin_log_related_rec_l Γ E1); eassumption.
+Qed.
+
+Tactic Notation "rel_rec_l" :=
+  iStartProof;
+  eapply (tac_rel_rec_l);
+    [tac_bind_helper (* e = fill K' _ *)
+    |try fast_done
+    |solve_closed       
+    |try fast_done (* to_val e' = Some v *)
+    |try fast_done (* eres = subst ... *)
+    |iNext; simpl; rewrite ?Closed_subst_id (* new goal *)].
+
+Lemma tac_rel_rec_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' f x ef e' efbody v eres t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (App (Rec f x efbody) e') →
+  ef = Rec f x efbody →
+  Closed (x :b: f :b: ∅) efbody →
+  to_val e' = Some v →
+  eres = subst' f ef (subst' x e' efbody) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' eres) τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ???????.
+  subst e ef eres.
+  rewrite -(bin_log_related_rec_r Γ E1 E2); eassumption.
+Qed.
+
+Tactic Notation "rel_rec_r" :=
+  iStartProof;
+  eapply (tac_rel_rec_r);
+    [solve_ndisj || fail "rel_rec_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper (* e = fill K' _ *)
+    |simpl; fast_done
+    |solve_closed
+    |try fast_done (* to_val e' = Some v *)
+    |try fast_done (* eres = subst ... *)
+    |simpl; rewrite ?Closed_subst_id (* new goal *)].
+
+Tactic Notation "rel_seq_r" := rel_rec_r.
+Tactic Notation "rel_let_r" := rel_rec_r.
+
+Lemma tac_rel_fst_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e1 e2 v1 v2 t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (Fst (Pair e1 e2)) →
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' e1) τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ?????.
+  subst e. 
+  rewrite -(of_to_val e1 v1); [| eassumption].
+  rewrite -(of_to_val e2 v2); [| eassumption].
+  rewrite -(bin_log_related_fst_r Γ E1 E2); [| eassumption].
+  rewrite (of_to_val e1); eauto.
+Qed.
+
+Tactic Notation "rel_fst_r" :=
+  iStartProof;
+  eapply (tac_rel_fst_r);
+    [solve_ndisj || fail "rel_fst_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper (* e = fill K' _ *)
+    |try fast_done (* to_val e1 = Some .. *)
+    |try fast_done (* to_val e2 = Some .. *)
+    |simpl (* new goal *)].
+
+Lemma tac_rel_snd_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e1 e2 v1 v2 t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (Snd (Pair e1 e2)) →
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' e2) τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ?????.
+  subst e. 
+  rewrite -(of_to_val e1 v1); [| eassumption].
+  rewrite -(of_to_val e2 v2); [| eassumption].
+  rewrite -(bin_log_related_snd_r Γ E1 E2); [| eassumption].
+  rewrite (of_to_val e2); eauto.
+Qed.
+
+Tactic Notation "rel_snd_r" :=
+  iStartProof;
+  eapply (tac_rel_snd_r);
+    [solve_ndisj || fail "rel_snd_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper (* e = fill K' _ *)
+    |try fast_done (* to_val e1 = Some .. *)
+    |try fast_done (* to_val e2 = Some .. *)
+    |simpl (* new goal *)].
+
+Lemma tac_rel_tlam_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e' t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (TApp (TLam e')) →
+  Closed ∅ e' →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' e') τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ????.
+  subst e. 
+  rewrite -(bin_log_related_tlam_r Γ E1 E2); eassumption.
+Qed.
+
+Tactic Notation "rel_tlam_r" :=
+  iStartProof;
+  eapply (tac_rel_tlam_r);
+    [solve_ndisj || fail "rel_tlam_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper || fail "rel_tlam_r: cannot find '(Λ.e)[]'"
+    |solve_closed
+    |simpl (* new goal *)].
+
+Lemma tac_rel_fold_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e' v t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (Unfold (Fold e')) →
+  to_val e' = Some v →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' e') τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ????.
+  subst e.
+  rewrite -(bin_log_related_fold_r Γ E1 E2); eassumption.
+Qed.
+
+Tactic Notation "rel_fold_r" :=
+  iStartProof;
+  eapply (tac_rel_fold_r);
+    [solve_ndisj || fail "rel_fold_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper || fail "rel_fold_r: cannot find 'Unfold (Fold e)'"
+    |try fast_done (* to_val e' = Some .. *)
+    |simpl (* new goal *)].
+
+Lemma tac_rel_case_inl_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e0 e1 e2 v t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (Case (InjL e0) e1 e2) →
+  Closed ∅ e1 →
+  Closed ∅ e2 →
+  to_val e0 = Some v →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' (App e1 e0)) τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ??????.
+  subst e.
+  rewrite -(bin_log_related_case_inl_r Γ E1 E2); eassumption.
+Qed.
+
+Tactic Notation "rel_case_inl_r" :=
+  iStartProof;
+  eapply (tac_rel_case_inl_r);
+    [solve_ndisj || fail "rel_case_inl_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper || fail "rel_case_inl_r: cannot find 'match InjL e with ..'"
+    |solve_closed
+    |solve_closed
+    |try fast_done (* to_val e0 = Some .. *)
+    |simpl (* new goal *)].
+
+Lemma tac_rel_case_inr_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e0 e1 e2 v t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (Case (InjR e0) e1 e2) →
+  Closed ∅ e1 →
+  Closed ∅ e2 →
+  to_val e0 = Some v →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' (App e2 e0)) τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ??????.
+  subst e.
+  rewrite -(bin_log_related_case_inr_r Γ E1 E2); eassumption.
+Qed.
+
+Tactic Notation "rel_case_inr_r" :=
+  iStartProof;
+  eapply (tac_rel_case_inr_r);
+    [solve_ndisj || fail "rel_case_inr_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper || fail "rel_case_inr_r: cannot find 'match InjR e with ..'"
+    |solve_closed
+    |solve_closed
+    |try fast_done (* to_val e0 = Some .. *)
+    |simpl (* new goal *)].
+
+Tactic Notation "rel_case_r" := rel_case_inl_r || rel_case_inr_r.
+
+Lemma tac_rel_if_true_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' e1 e2 t τ :
+  nclose specN ⊆ E1 →
+  e = fill K' (If (#♭ true) e1 e2) →
+  Closed ∅ e1 →
+  Closed ∅ e2 →
+  (Δ ⊢ bin_log_related E1 E2 Γ t (fill K' e1) τ) →
+  (Δ ⊢ bin_log_related E1 E2 Γ t e τ).
+Proof.
+  intros ?????.
+  subst e.
+  rewrite -(bin_log_related_if_true_r Γ); eassumption.
+Qed.
+
+Tactic Notation "rel_if_true_r" :=
+  iStartProof;
+  eapply (tac_rel_if_true_r);
+    [solve_ndisj || fail "rel_if_true_r: cannot prove 'nclose specN ⊆ ?'"
+    |tac_bind_helper || fail "rel_if_true_r: cannot find 'if true ..'"
+    |solve_closed
+    |solve_closed