Commit 4daa00cb authored by Robbert Krebbers's avatar Robbert Krebbers

Big ops distribute over and.

parent aca09e1e
......@@ -246,6 +246,11 @@ Section list.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_opL. Qed.
Lemma big_sepL_and Φ Ψ l :
([ list] kx l, Φ k x Ψ k x)
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. auto using big_sepL_mono with I. Qed.
Lemma big_sepL_later Φ l :
([ list] kx l, Φ k x) ([ list] kx l, Φ k x).
Proof. apply (big_opL_commute _). Qed.
......@@ -382,6 +387,11 @@ Section gmap.
([ map] kx m, Φ k x) ([ map] kx m, Ψ k x).
Proof. apply: big_opM_opM. Qed.
Lemma big_sepM_and Φ Ψ m :
([ map] kx m, Φ k x Ψ k x)
([ map] kx m, Φ k x) ([ map] kx m, Ψ k x).
Proof. auto using big_sepM_mono with I. Qed.
Lemma big_sepM_later Φ m :
([ map] kx m, Φ k x) ([ map] kx m, Φ k x).
Proof. apply (big_opM_commute _). Qed.
......@@ -520,6 +530,10 @@ Section gset.
([ set] y X, Φ y Ψ y) ([ set] y X, Φ y) ([ set] y X, Ψ y).
Proof. apply: big_opS_opS. Qed.
Lemma big_sepS_and Φ Ψ X :
([ set] y X, Φ y Ψ y) ([ set] y X, Φ y) ([ set] y X, Ψ y).
Proof. auto using big_sepS_mono with I. Qed.
Lemma big_sepS_later Φ X : ([ set] y X, Φ y) ([ set] y X, Φ y).
Proof. apply (big_opS_commute _). Qed.
......@@ -622,6 +636,10 @@ Section gmultiset.
([ mset] y X, Φ y Ψ y) ([ mset] y X, Φ y) ([ mset] y X, Ψ y).
Proof. apply: big_opMS_opMS. Qed.
Lemma big_sepMS_and Φ Ψ X :
([ mset] y X, Φ y Ψ y) ([ mset] y X, Φ y) ([ mset] y X, Ψ y).
Proof. auto using big_sepMS_mono with I. Qed.
Lemma big_sepMS_later Φ X : ([ mset] y X, Φ y) ([ mset] y X, Φ y).
Proof. apply (big_opMS_commute _). Qed.
......
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