Commit 204b6c8e by Robbert Krebbers

### Proper instances for mononicity of CMRA op.

parent 2308bb5c
 ... @@ -397,6 +397,13 @@ Proof. intros; etrans; eauto using cmra_monoN_l, cmra_monoN_r. Qed. ... @@ -397,6 +397,13 @@ Proof. intros; etrans; eauto using cmra_monoN_l, cmra_monoN_r. Qed. Lemma cmra_mono x1 x2 y1 y2 : x1 ≼ y1 → x2 ≼ y2 → x1 ⋅ x2 ≼ y1 ⋅ y2. Lemma cmra_mono x1 x2 y1 y2 : x1 ≼ y1 → x2 ≼ y2 → x1 ⋅ x2 ≼ y1 ⋅ y2. Proof. intros; etrans; eauto using cmra_mono_l, cmra_mono_r. Qed. Proof. intros; etrans; eauto using cmra_mono_l, cmra_mono_r. Qed. Global Instance cmra_monoN' n : Proper (includedN n ==> includedN n ==> includedN n) (@op A _). Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_monoN. Qed. Global Instance cmra_mono' : Proper (included ==> included ==> included) (@op A _). Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_mono. Qed. Lemma cmra_included_dist_l n x1 x2 x1' : Lemma cmra_included_dist_l n x1 x2 x1' : x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. Proof. Proof. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!