From 0b7e25c2fda6925b0ecabaf3c497df74b14b6f76 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 10 Feb 2016 21:35:52 +0100
Subject: [PATCH] make auth_closing less stupid

---
 algebra/auth.v       |  6 +++++-
 program_logic/auth.v | 11 ++---------
 2 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index 7860affe8..754cf3060 100644
--- a/algebra/auth.v
+++ b/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 *.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 0424bacab..d47582c20 100644
--- a/program_logic/auth.v
+++ b/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.
-- 
GitLab