Cosmetic changes to some proofs & a tactic

F_mu_ref_conc/examples/counter.v

@@ -461,24 +461,26 @@ Section CG_Counter.
     iApply (bin_log_related_alloc_r); auto.
     iIntros (cnt') "Hcnt' /=".
 
-    (* establishing the invariant *)
-    iAssert (counter_inv l cnt cnt')
-      with "[Hl Hcnt Hcnt']" as "Hinv".
-    { iExists _. by iFrame. }
-    iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
+    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
+    rewrite /= !Closed_subst_id /=.
+
     unfold FG_counter_body. unlock.
     iApply (bin_log_related_rec_l _ _ []); auto.
     iNext. rewrite /= !Closed_subst_id /=.
 
-    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
-    rewrite /= !Closed_subst_id /=.
     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 /=.
-    
+    rewrite /= !Closed_subst_id /=.    
+
+    (* establishing the invariant *)
+    iAssert (counter_inv l cnt cnt')
+      with "[Hl Hcnt Hcnt']" as "Hinv".
+    { iExists _. by iFrame. }
+    iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
+
     iApply (bin_log_related_pair _ with "[]").
     - iApply (FG_CG_increment_refinement with "Hinv").
     - iApply (counter_read_refinement with "Hinv").

F_mu_ref_conc/soundness_binary.v

@@ -12,7 +12,7 @@ Class heapPreIG Σ := HeapPreIG {
 Lemma logrel_adequate Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
     e e' τ σ :
   (∀ `{heapIG Σ, cfgSG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
-  adequate e σ (λ _, ∃ thp' h v, rtc step ([e'], ∅) (of_val v :: thp', h)).
+  adequate e σ (λ _, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h)).
 Proof.
   intros Hlog.
   eapply (wp_adequacy Σ _); iIntros (Hinv).

F_mu_ref_conc/tactics.v

@@ -905,8 +905,8 @@ Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) "as" con
       | (j ⤇ _)%I => Hj
       | _ => find Γ j
       end
-    | Enil => fail "tp_apply: cannot find " j " ⤇ _ "
-    | _ => fail "tp_apply: unknown error in find"
+    | Enil => fail 2 "tp_apply: cannot find " j " ⤇ _ "
+    | _ => fail 2 "tp_apply: unknown error in find"
     end in
   let rec findSpec Γp Γs :=
     match Γp with
@@ -917,10 +917,10 @@ Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) "as" con
       end
     | Enil =>
       match Γs with
-      | Enil => fail "tp_apply: cannot find spec_ctx _"
+      | Enil => fail 2 "tp_apply: cannot find spec_ctx _"
       | _ => findSpec Γs Enil
       end
-    | _ => fail "tp_apply: unknown error in findSpec"
+    | _ => fail 2 "tp_apply: unknown error in findSpec"
     end in
   match goal with
   | |- of_envs (Envs ?Γp ?Γs) ⊢ ?Q =>
@@ -929,7 +929,7 @@ Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) "as" con
     let pat := eval vm_compute in (appP (sel_pat.parse Hs) Hj Hspec) in
     let pats := print_sel pat in 
     let elim_pats := eval vm_compute in (add_elim_pat Hr Hj) in
-    iMod (lem with pats) as elim_pats; first by solve_ndisj
+    iMod (lem with pats) as elim_pats; first try by solve_ndisj
   | _ => fail "tp_apply: cannot parse the context"
   end.
 
@@ -1016,7 +1016,7 @@ End test.
 Section test2.
 Context `{heapIG Σ, !cfgSG Σ}.
 (* TODO: Coq complains if I make it a section variable *)
-Axiom (steps_release : forall E ρ j K l b,
+Axiom (steps_release_test : forall E ρ j K l b,
     nclose specN ⊆ E →
     spec_ctx ρ -∗ l ↦ₛ (#♭v b) -∗ j ⤇ fill K (App (Lit Unit) (Loc l))
     ={E}=∗ j ⤇ fill K (Lit Unit) ∗ l ↦ₛ (#♭v false)).
@@ -1028,7 +1028,7 @@ Theorem test_apply E ρ j b K l:
   -∗ |={E}=> True.
 Proof.
   iIntros (?) "#Hs Hst Hj".
-  tp_apply j steps_release with "Hst" as "Hl".
+  tp_apply j steps_release_test with "Hst" as "Hl".
   done.
 Qed.