From 64b1650cfdea1ed73b0d987a14e476a70309edb0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 8 Jun 2017 13:11:43 +0200 Subject: [PATCH] Some step-indexed properties for CMRAs that were missing. --- theories/algebra/cmra.v | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index cad2236b..fde8e5ce 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -1251,6 +1251,21 @@ Section option. + exists (Some z); by constructor. Qed. + Lemma option_includedN n (mx my : option A) : + mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y). + Proof. + split. + - intros [mz Hmz]. + destruct mx as [x|]; [right|by left]. + destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. + destruct mz as [z|]; inversion_clear Hmz; split_and?; auto; + ofe_subst; eauto using cmra_includedN_l. + - intros [->|(x&y&->&->&[Hz|[z Hz]])]. + + exists my. by destruct my. + + exists None; by constructor. + + exists (Some z); by constructor. + Qed. + Lemma option_cmra_mixin : CMRAMixin (option A). Proof. apply cmra_total_mixin. @@ -1317,16 +1332,27 @@ Section option. Lemma exclusive_Some_r x `{!Exclusive x} my : ✓ (my ⋅ Some x) → my = None. Proof. rewrite comm. by apply exclusive_Some_l. Qed. + Lemma Some_includedN n x y : Some x ≼{n} Some y ↔ x ≡{n}≡ y ∨ x ≼{n} y. + Proof. rewrite option_includedN; naive_solver. Qed. Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y. Proof. rewrite option_included; naive_solver. Qed. Lemma Some_included_2 x y : x ≼ y → Some x ≼ Some y. Proof. rewrite Some_included; eauto. Qed. + + Lemma Some_includedN_total `{CMRATotal A} n x y : Some x ≼{n} Some y ↔ x ≼{n} y. + Proof. rewrite Some_includedN. split. by intros [->|?]. eauto. Qed. Lemma Some_included_total `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≼ y. Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed. + + Lemma Some_includedN_exclusive n x `{!Exclusive x} y : + Some x ≼{n} Some y → ✓{n} y → x ≡{n}≡ y. + Proof. move=> /Some_includedN [//|/exclusive_includedN]; tauto. Qed. Lemma Some_included_exclusive x `{!Exclusive x} y : Some x ≼ Some y → ✓ y → x ≡ y. Proof. move=> /Some_included [//|/exclusive_included]; tauto. Qed. + Lemma is_Some_includedN n mx my : mx ≼{n} my → is_Some mx → is_Some my. + Proof. rewrite -!not_eq_None_Some option_includedN. naive_solver. Qed. Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my. Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed. @@ -1348,7 +1374,18 @@ Arguments optionUR : clear implicits. Section option_prod. Context {A B : cmraT}. - Lemma Some_pair_included (x1 x2 : A) (y1 y2 : B) : + + Lemma Some_pair_includedN n (x1 x2 : A) (y1 y2 : B) : + Some (x1,y1) ≼{n} Some (x2,y2) → Some x1 ≼{n} Some x2 ∧ Some y1 ≼{n} Some y2. + Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed. + Lemma Some_pair_includedN_total_1 `{CMRATotal A} n (x1 x2 : A) (y1 y2 : B) : + Some (x1,y1) ≼{n} Some (x2,y2) → x1 ≼{n} x2 ∧ Some y1 ≼{n} Some y2. + Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ x1). Qed. + Lemma Some_pair_includedN_total_2 `{CMRATotal B} n (x1 x2 : A) (y1 y2 : B) : + Some (x1,y1) ≼{n} Some (x2,y2) → Some x1 ≼{n} Some x2 ∧ y1 ≼{n} y2. + Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ y1). Qed. + + Lemma Some_pair_included (x1 x2 : A) (y1 y2 : B) : Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ Some y1 ≼ Some y2. Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed. Lemma Some_pair_included_total_1 `{CMRATotal A} (x1 x2 : A) (y1 y2 : B) : -- GitLab