Commit 8759beb5 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

New lemma : cmra_update_valid0. This let us prove a FP update using the...

New lemma : cmra_update_valid0. This let us prove a FP update using the additionnal hypothesis that the source is valid at step 0.
parent ba4e086e
Pipeline #1857 passed with stage
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment