Skip to content

I
Iris
Commit d6875e7d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Prove fact about exclusive and included.

parent 9f3a376e
Pipeline #2745 passed with stage
    in 9 minutes and 33 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 4 additions and 0 deletions
    algebra/cmra.v
    View file @ d6875e7d
    ......@@ -344,6 +344,10 @@ Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
    Proof. rewrite comm. by apply exclusive_l. Qed.
    Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
    Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
    Lemma exclusive_includedN n x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
    Proof. intros [? ->]. by apply exclusiveN_l. Qed.
    Lemma exclusive_included x `{!Exclusive x} y : x ≼ y → ✓ y → False.
    Proof. intros [? ->]. by apply exclusive_l. Qed.
    (** ** Order *)
    Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
    ......
    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