Skip to content
Snippets Groups Projects
Commit d9247945 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added [cmra_update_included] lemma

parent 1e9db5bd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
iris/algebra/updates.v
+ 3
− 0
View file @ d9247945
......@@ -107,6 +107,9 @@ Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
Lemma cmra_update_op_r x y : x ⋅ y ~~> y.
Proof. rewrite comm. apply cmra_update_op_l. Qed.
Lemma cmra_update_included x y : x ≼ y → y ~~> x.
Proof. intros [z ->]. apply cmra_update_op_l. Qed.
Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
Proof.
intros H n mz Hmz. apply H, Hmz.
......
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