Commit 608e43fe authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung
Browse files

strengthen big_sepS_union_2

parent 75700c31
Pipeline #65713 passed with stage
in 16 minutes and 16 seconds
...@@ -2553,15 +2553,18 @@ Section gset. ...@@ -2553,15 +2553,18 @@ Section gset.
Φ x - ([ set] y X, Φ y) - ([ set] y X {[ x ]}, Φ y). Φ x - ([ set] y X, Φ y) - ([ set] y X {[ x ]}, Φ y).
Proof. rewrite comm_L. by apply big_sepS_insert_2. Qed. Proof. rewrite comm_L. by apply big_sepS_insert_2. Qed.
Lemma big_sepS_union_2 {Φ} X Y `{! x, Affine (Φ x)} : Lemma big_sepS_union_2 {Φ} X Y
`{! x, TCOr (Affine (Φ x)) (Absorbing (Φ x))} :
([ set] y X, Φ y) - ([ set] y Y, Φ y) - ([ set] y X Y, Φ y). ([ set] y X, Φ y) - ([ set] y Y, Φ y) - ([ set] y X Y, Φ y).
Proof. Proof.
apply wand_intro_r. apply wand_intro_r. induction X as [|x X ? IH] using set_ind_L.
rewrite -difference_union_L. { by rewrite left_id_L big_sepS_empty left_id. }
rewrite big_sepS_union; last set_solver. rewrite big_sepS_insert // -assoc IH -assoc_L.
apply sep_mono_l. destruct (decide (x Y)).
apply big_sepS_subseteq; first done. { replace ({[x]} (X Y)) with (X Y) by set_solver.
set_solver. rewrite (big_sepS_delete _ _ x); last set_solver.
by rewrite assoc sep_elim_r. }
by rewrite big_sepS_insert; last set_solver.
Qed. Qed.
Lemma big_sepS_delete_2 {Φ X} x : Lemma big_sepS_delete_2 {Φ X} x :
......
Supports Markdown
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