diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v index b9f814a95ffc1cd57573911a5f9532e519dbd686..940225e09853528cb43eaa8c0fcc5b3d87e373a3 100644 --- a/algebra/cmra_big_op.v +++ b/algebra/cmra_big_op.v @@ -185,7 +185,6 @@ Section list. Qed. End list. - (** ** Big ops over finite maps *) Section gmap. Context `{Countable K} {A : Type}. @@ -371,3 +370,64 @@ Section gset. Qed. End gset. End big_op. + +Lemma big_opL_commute {M1 M2 : ucmraT} {A} (h : M1 → M2) + `{!Proper ((≡) ==> (≡)) h} (f : nat → A → M1) l : + h ∅ ≡ ∅ → + (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) → + h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)). +Proof. + intros ??. revert f. induction l as [|x l IH]=> f. + - by rewrite !big_opL_nil. + - by rewrite !big_opL_cons -IH. +Qed. +Lemma big_opL_commute1 {M1 M2 : ucmraT} {A} (h : M1 → M2) + `{!Proper ((≡) ==> (≡)) h} (f : nat → A → M1) l : + (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) → + l ≠ [] → + h ([⋅ list] k↦x ∈ l, f k x) ≡ ([⋅ list] k↦x ∈ l, h (f k x)). +Proof. + intros ??. revert f. induction l as [|x [|x' l'] IH]=> f //. + - by rewrite !big_opL_singleton. + - by rewrite !(big_opL_cons _ x) -IH. +Qed. + +Lemma big_opM_commute {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2) + `{!Proper ((≡) ==> (≡)) h} (f : K → A → M1) m : + h ∅ ≡ ∅ → + (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) → + h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)). +Proof. + intros. rewrite /big_opM. + induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite -?IH; auto. +Qed. +Lemma big_opM_commute1 {M1 M2 : ucmraT} `{Countable K} {A} (h : M1 → M2) + `{!Proper ((≡) ==> (≡)) h} (f : K → A → M1) m : + (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) → + m ≠ ∅ → + h ([⋅ map] k↦x ∈ m, f k x) ≡ ([⋅ map] k↦x ∈ m, h (f k x)). +Proof. + rewrite -map_to_list_empty' /big_opM=> ??. + induction (map_to_list m) as [|[i x] [|i' x'] IH]; + csimpl in *; rewrite ?right_id -?IH //. +Qed. + +Lemma big_opS_commute {M1 M2 : ucmraT} `{Countable A} (h : M1 → M2) + `{!Proper ((≡) ==> (≡)) h} (f : A → M1) X : + h ∅ ≡ ∅ → + (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) → + h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)). +Proof. + intros. rewrite /big_opS. + induction (elements X) as [|x l IH]; csimpl; rewrite -?IH; auto. +Qed. +Lemma big_opS_commute1 {M1 M2 : ucmraT} `{Countable A} (h : M1 → M2) + `{!Proper ((≡) ==> (≡)) h} (f : A → M1) X : + (∀ x y, h (x ⋅ y) ≡ h x ⋅ h y) → + X ≢ ∅ → + h ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, h (f x)). +Proof. + rewrite -elements_empty' /big_opS=> ??. + induction (elements X) as [|x [|x' l] IH]; + csimpl in *; rewrite ?right_id -?IH //. +Qed. diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v index 64aed4cf4d46b75483e867ba68fb4d0316f739ba..5a268321e429e059ff9fe7c2b2e988cdbb861e7a 100644 --- a/algebra/upred_big_op.v +++ b/algebra/upred_big_op.v @@ -1,4 +1,4 @@ -From iris.algebra Require Export upred list. +From iris.algebra Require Export upred list cmra_big_op. From iris.prelude Require Import gmap fin_collections functions. Import uPred. @@ -267,21 +267,41 @@ Section list. by rewrite -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc. Qed. - Lemma big_sepL_later Φ l : - ▷ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, ▷ Φ k x). + Lemma big_sepL_commute (Ψ: uPred M → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} Φ l : + Ψ True ⊣⊢ True → + (∀ P Q, Ψ (P ★ Q) ⊣⊢ Ψ P ★ Ψ Q) → + Ψ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, Ψ (Φ k x)). Proof. - revert Φ. induction l as [|x l IH]=> Φ. - { by rewrite !big_sepL_nil later_True. } - by rewrite !big_sepL_cons later_sep IH. + intros ??. revert Φ. induction l as [|x l IH]=> Φ //. + by rewrite !big_sepL_cons -IH. Qed. + Lemma big_sepL_op_commute {B : ucmraT} + (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : nat → A → B) l : + Ψ ∅ ⊣⊢ True → + (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) → + Ψ ([⋅ list] k↦x ∈ l, f k x) ⊣⊢ ([★ list] k↦x ∈ l, Ψ (f k x)). + Proof. + intros ??. revert f. induction l as [|x l IH]=> f //. + by rewrite big_sepL_cons big_opL_cons -IH. + Qed. + Lemma big_sepL_op_commute1 {B : ucmraT} + (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : nat → A → B) l : + (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) → + l ≠ [] → + Ψ ([⋅ list] k↦x ∈ l, f k x) ⊣⊢ ([★ list] k↦x ∈ l, Ψ (f k x)). + Proof. + intros ??. revert f. induction l as [|x [|x' l'] IH]=> f //. + { by rewrite big_sepL_singleton big_opL_singleton. } + by rewrite big_sepL_cons big_opL_cons -IH. + Qed. + + Lemma big_sepL_later Φ l : + ▷ ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, ▷ Φ k x). + Proof. apply (big_sepL_commute _); auto using later_True, later_sep. Qed. Lemma big_sepL_always Φ l : (□ [★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □ Φ k x). - Proof. - revert Φ. induction l as [|x l IH]=> Φ. - { by rewrite !big_sepL_nil always_pure. } - by rewrite !big_sepL_cons always_sep IH. - Qed. + Proof. apply (big_sepL_commute _); auto using always_pure, always_sep. Qed. Lemma big_sepL_always_if p Φ l : □?p ([★ list] k↦x ∈ l, Φ k x) ⊣⊢ ([★ list] k↦x ∈ l, □?p Φ k x). @@ -430,21 +450,41 @@ Section gmap. by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc. Qed. - Lemma big_sepM_later Φ m : - ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). + Lemma big_sepM_commute (Ψ: uPred M → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} Φ m : + Ψ True ⊣⊢ True → + (∀ P Q, Ψ (P ★ Q) ⊣⊢ Ψ P ★ Ψ Q) → + Ψ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, Ψ (Φ k x)). Proof. - rewrite /uPred_big_sepM. - induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //. - by rewrite later_sep IH. + intros ??. rewrite /uPred_big_sepM. + induction (map_to_list m) as [|[i x] l IH]; rewrite //= -?IH; auto. + Qed. + Lemma big_sepM_op_commute {B : ucmraT} + (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : K → A → B) m : + Ψ ∅ ⊣⊢ True → + (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) → + Ψ ([⋅ map] k↦x ∈ m, f k x) ⊣⊢ ([★ map] k↦x ∈ m, Ψ (f k x)). + Proof. + intros ??. rewrite /big_opM /uPred_big_sepM. + induction (map_to_list m) as [|[i x] l IH]; rewrite //= -?IH; auto. + Qed. + Lemma big_sepM_op_commute1 {B : ucmraT} + (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : K → A → B) m : + (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) → + m ≠ ∅ → + Ψ ([⋅ map] k↦x ∈ m, f k x) ⊣⊢ ([★ map] k↦x ∈ m, Ψ (f k x)). + Proof. + rewrite -map_to_list_empty'. intros ??. rewrite /big_opM /uPred_big_sepM. + induction (map_to_list m) as [|[i x] [|i' x'] IH]; + csimpl in *; rewrite ?right_id -?IH //. Qed. + Lemma big_sepM_later Φ m : + ▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x). + Proof. apply (big_sepM_commute _); auto using later_True, later_sep. Qed. + Lemma big_sepM_always Φ m : (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x). - Proof. - rewrite /uPred_big_sepM. - induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_pure //. - by rewrite always_sep IH. - Qed. + Proof. apply (big_sepM_commute _); auto using always_pure, always_sep. Qed. Lemma big_sepM_always_if p Φ m : □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x). @@ -569,20 +609,40 @@ Section gset. by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc. Qed. - Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). + Lemma big_sepS_commute (Ψ: uPred M → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} Φ X : + Ψ True ⊣⊢ True → + (∀ P Q, Ψ (P ★ Q) ⊣⊢ Ψ P ★ Ψ Q) → + Ψ ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ X, Ψ (Φ x)). Proof. - rewrite /uPred_big_sepS. - induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True. - by rewrite later_sep IH. + intros ??. rewrite /uPred_big_sepS. + induction (elements X) as [|x l IH]; rewrite //= -?IH; auto. Qed. - - Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y). + Lemma big_sepS_op_commute {B : ucmraT} + (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : A → B) X : + Ψ ∅ ⊣⊢ True → + (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) → + Ψ ([⋅ set] x ∈ X, f x) ⊣⊢ ([★ set] x ∈ X, Ψ (f x)). Proof. - rewrite /uPred_big_sepS. - induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_pure. - by rewrite always_sep IH. + intros ??. rewrite /big_opS /uPred_big_sepS. + induction (elements X) as [|x l IH]; rewrite //= -?IH; auto. + Qed. + Lemma big_sepS_op_commute1 {B : ucmraT} + (Ψ: B → uPred M) `{!Proper ((≡) ==> (≡)) Ψ} (f : A → B) X : + (∀ x y, Ψ (x ⋅ y) ⊣⊢ Ψ x ★ Ψ y) → + X ≢ ∅ → + Ψ ([⋅ set] x ∈ X, f x) ⊣⊢ ([★ set] x ∈ X, Ψ (f x)). + Proof. + rewrite -elements_empty'. intros ??. rewrite /big_opS /uPred_big_sepS. + induction (elements X) as [|x [|x' l] IH]; + csimpl in *; rewrite ?right_id -?IH //. Qed. + Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y). + Proof. apply (big_sepS_commute _); auto using later_True, later_sep. Qed. + + Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y). + Proof. apply (big_sepS_commute _); auto using always_pure, always_sep. Qed. + Lemma big_sepS_always_if q Φ X : □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y). Proof. destruct q; simpl; auto using big_sepS_always. Qed.