From 87957de901362c44bd860f96db4c7f05dcf9c5c9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Feb 2016 20:54:07 +0100
Subject: [PATCH] Stronger version of auth_update w.r.t. step indexes.
---
algebra/auth.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/algebra/auth.v b/algebra/auth.v
index 29760ee65..0397b82dc 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -148,11 +148,11 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_update a a' b b' :
- (∀ n af, ✓{n} a → a ={n}= a' ⋅ af → b ={n}= b' ⋅ af ∧ ✓{n} b) →
+ (∀ n af, ✓{S n} a → a ={S n}= a' ⋅ af → b ={S n}= b' ⋅ af ∧ ✓{S n} b) →
â— a â‹… â—¯ a' ~~> â— b â‹… â—¯ b'.
Proof.
- move=> Hab [[] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
- destruct (Hab (S n) (bf1 â‹… bf2)) as [Ha' ?]; auto.
+ move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
+ destruct (Hab n (bf1 â‹… bf2)) as [Ha' ?]; auto.
{ by rewrite Ha left_id associative. }
split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
Qed.
--
GitLab