Commit 0ae5ad57 authored by Glen Mével's avatar Glen Mével
Browse files

big_op: make all TCOr side-conditions implicit

parent 5e346fc5
...@@ -1335,14 +1335,14 @@ Section sep_map. ...@@ -1335,14 +1335,14 @@ Section sep_map.
([ map] ky <[i:=x]> m, Φ k y) Φ i x [ map] ky delete i m, Φ k y. ([ map] ky <[i:=x]> m, Φ k y) Φ i x [ map] ky delete i m, Φ k y.
Proof. apply big_opM_insert_delete. Qed. Proof. apply big_opM_insert_delete. Qed.
Lemma big_sepM_insert_2 Φ m i x : Lemma big_sepM_insert_2 Φ m i x
TCOr ( y, Affine (Φ i y)) (Absorbing (Φ i x)) `{!TCOr ( y, Affine (Φ i y)) (Absorbing (Φ i x))} :
Φ i x - ([ map] ky m, Φ k y) - [ map] ky <[i:=x]> m, Φ k y. Φ i x - ([ map] ky m, Φ k y) - [ map] ky <[i:=x]> m, Φ k y.
Proof. Proof.
intros Ha. apply wand_intro_r. destruct (m !! i) as [y|] eqn:Hi; last first. apply wand_intro_r. destruct (m !! i) as [y|] eqn:Hi; last first.
{ by rewrite -big_sepM_insert. } { by rewrite -big_sepM_insert. }
assert (TCOr (Affine (Φ i y)) (Absorbing (Φ i x))). assert (TCOr (Affine (Φ i y)) (Absorbing (Φ i x))).
{ destruct Ha; try apply _. } { destruct select (TCOr _ _); try apply _. }
rewrite big_sepM_delete // assoc. rewrite big_sepM_delete // assoc.
rewrite (sep_elim_l (Φ i x)) -big_sepM_insert ?lookup_delete //. rewrite (sep_elim_l (Φ i x)) -big_sepM_insert ?lookup_delete //.
by rewrite insert_delete_insert. by rewrite insert_delete_insert.
...@@ -2099,15 +2099,15 @@ Section map2. ...@@ -2099,15 +2099,15 @@ Section map2.
by apply wand_intro_l. by apply wand_intro_l.
Qed. Qed.
Lemma big_sepM2_insert_2 Φ m1 m2 i x1 x2 : Lemma big_sepM2_insert_2 Φ m1 m2 i x1 x2
TCOr ( x y, Affine (Φ i x y)) (Absorbing (Φ i x1 x2)) `{!TCOr ( x y, Affine (Φ i x y)) (Absorbing (Φ i x1 x2))} :
Φ i x1 x2 - Φ i x1 x2 -
([ map] ky1;y2 m1;m2, Φ k y1 y2) - ([ map] ky1;y2 m1;m2, Φ k y1 y2) -
([ map] ky1;y2 <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2). ([ map] ky1;y2 <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2).
Proof. Proof.
intros Ha. rewrite big_sepM2_eq /big_sepM2_def. rewrite big_sepM2_eq /big_sepM2_def.
assert (TCOr ( x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))). assert (TCOr ( x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
{ destruct Ha; try apply _. } { destruct select (TCOr _ _); try apply _. }
apply wand_intro_r. apply wand_intro_r.
rewrite !persistent_and_affinely_sep_l /=. rewrite !persistent_and_affinely_sep_l /=.
rewrite (sep_comm (Φ _ _ _)) -sep_assoc. apply sep_mono. rewrite (sep_comm (Φ _ _ _)) -sep_assoc. apply sep_mono.
...@@ -2538,11 +2538,11 @@ Section gset. ...@@ -2538,11 +2538,11 @@ Section gset.
x X ([ set] y X, Φ y) Φ x [ set] y X {[ x ]}, Φ y. x X ([ set] y X, Φ y) Φ x [ set] y X {[ x ]}, Φ y.
Proof. apply big_opS_delete. Qed. Proof. apply big_opS_delete. Qed.
Lemma big_sepS_insert_2 {Φ X} x : Lemma big_sepS_insert_2 {Φ X} x
TCOr (Affine (Φ x)) (Absorbing (Φ x)) `{!TCOr (Affine (Φ x)) (Absorbing (Φ x))} :
Φ x - ([ set] y X, Φ y) - ([ set] y {[ x ]} X, Φ y). Φ x - ([ set] y X, Φ y) - ([ set] y {[ x ]} X, Φ y).
Proof. Proof.
intros Haff. apply wand_intro_r. destruct (decide (x X)); last first. apply wand_intro_r. destruct (decide (x X)); last first.
{ rewrite -big_sepS_insert //. } { rewrite -big_sepS_insert //. }
rewrite big_sepS_delete // assoc. rewrite big_sepS_delete // assoc.
rewrite (sep_elim_l (Φ x)) -big_sepS_insert; last set_solver. rewrite (sep_elim_l (Φ x)) -big_sepS_insert; last set_solver.
......
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