make auth_closing less stupid

algebra/auth.v

@@ -147,8 +147,12 @@ Proof. done. Qed.
 Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
+(* FIXME tentative name. Or maybe remove this notion entirely. *)
+Definition auth_step a a' b b' :=
+  ∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b.
+
 Lemma auth_update a a' b b' :
-  (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
+  auth_step a a' b b' →
   ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'.
 Proof.
   move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.

program_logic/auth.v

@@ -58,14 +58,8 @@ Section auth.
     by rewrite sep_elim_l.
   Qed.
 
-  (* TODO: This notion should probably be defined in algebra/,
-     with instances proven for the important constructions. *)
-  Definition auth_step a b :=
-    (∀ n a' af, ✓{n} (a ⋅ a') → a ⋅ a' ≡{n}≡ af ⋅ a →
-                b ⋅ a' ≡{n}≡ b ⋅ af ∧ ✓{n} (b ⋅ a')).
-
   Lemma auth_closing a a' b γ :
-    auth_step a b →
+    auth_step (a ⋅ a') a (b ⋅ a') b →
     (φ (b ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
       ⊑ pvs N N (auth_inv γ ★ auth_own γ b).
   Proof.
@@ -73,8 +67,7 @@ Section auth.
     rewrite [(_ ★ φ _)%I]commutative -associative.
     rewrite -pvs_frame_l. apply sep_mono; first done.
     rewrite -own_op. apply own_update.
-    apply auth_update=>n af Ha Heq. apply Hstep; first done.
-    by rewrite [af ⋅ _]commutative.
+    by apply auth_update.
   Qed.
 
 End auth.