From 8759beb58170e7dd7409d8a0df21f1df325493a8 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Fri, 1 Jul 2016 13:12:40 +0200
Subject: [PATCH] New lemma : cmra_update_valid0. This let us prove a FP update
 using the additionnal hypothesis that the source is valid at step 0.

---
 algebra/updates.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/algebra/updates.v b/algebra/updates.v
index 6b5957120..040f563c4 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -125,6 +125,13 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
+Lemma cmra_update_valid0 x y :
+  (✓{0} x → x ~~> y) → x ~~> y.
+Proof.
+  intros H n mz Hmz. apply H, Hmz.
+  apply (cmra_validN_le n); last lia.
+  destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz.
+Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
 Section total_updates.
-- 
GitLab