Commit fad29a90 authored by Glen Mével's avatar Glen Mével Committed by Glen Mével
Browse files

big_op: weaken all Absorbing conditions using TCOr and Affine

For all big_op lemmas which had an `Absorbing` condition, the condition
has now become an alternative between `Affine` and `Absorbing`. Thus the
lemmas are made more general. This is spreading the use of the `TCOr
(Affine _) (Absorbing _)` pattern.
parent 255341dd
Pipeline #58006 canceled with stage
in 2 minutes and 29 seconds
......@@ -186,14 +186,23 @@ Section sep_list.
([ list] ky l, Φ k y) Φ i x (Φ i x - ([ list] ky l, Φ k y)).
Proof. intros. by rewrite {1}big_sepL_insert_acc // (forall_elim x) list_insert_id. Qed.
Lemma big_sepL_lookup Φ l i x `{!Absorbing (Φ i x)} :
Lemma big_sepL_lookup Φ l i x
{Haff : TCOr ( j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
l !! i = Some x ([ list] ky l, Φ k y) Φ i x.
Proof. intros. rewrite big_sepL_lookup_acc //. by rewrite sep_elim_l. Qed.
Proof.
intros Hi. destruct Haff.
{ rewrite -(take_drop_middle l i x) // big_sepL_app /= take_length.
apply lookup_lt_Some in Hi. rewrite (_ : _ + 0 = i); last lia.
rewrite sep_elim_r sep_elim_l //. }
{ rewrite big_sepL_lookup_acc // sep_elim_l //. }
Qed.
Lemma big_sepL_elem_of (Φ : A PROP) l x `{!Absorbing (Φ x)} :
Lemma big_sepL_elem_of (Φ : A PROP) l x
{Haff : TCOr ( y, Affine (Φ y)) (Absorbing (Φ x))} :
x l ([ list] y l, Φ y) Φ x.
Proof.
intros [i ?]%elem_of_list_lookup. by eapply (big_sepL_lookup (λ _, Φ)).
intros [i ?]%elem_of_list_lookup. eapply (big_sepL_lookup (λ _, Φ)); last done.
destruct Haff; exact _.
Qed.
Lemma big_sepL_fmap {B} (f : A B) (Φ : nat B PROP) l :
......@@ -627,10 +636,19 @@ Section sep_list2.
by rewrite !list_insert_id.
Qed.
Lemma big_sepL2_lookup Φ l1 l2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
Lemma big_sepL2_lookup Φ l1 l2 i x1 x2
{Haff : TCOr ( j y1 y2, Affine (Φ j y1 y2)) (Absorbing (Φ i x1 x2))} :
l1 !! i = Some x1 l2 !! i = Some x2
([ list] ky1;y2 l1;l2, Φ k y1 y2) Φ i x1 x2.
Proof. intros. rewrite big_sepL2_lookup_acc //. by rewrite sep_elim_l. Qed.
Proof.
intros Hx1 Hx2. destruct Haff.
{ rewrite -(take_drop_middle l1 i x1) // -(take_drop_middle l2 i x2) //.
apply lookup_lt_Some in Hx1. apply lookup_lt_Some in Hx2.
rewrite big_sepL2_app_same_length /= 2?take_length; last lia.
rewrite (_ : _ + 0 = i); last lia.
rewrite sep_elim_r sep_elim_l //. }
{ rewrite big_sepL2_lookup_acc // sep_elim_l //. }
Qed.
Lemma big_sepL2_fmap_l {A'} (f : A A') (Φ : nat A' B PROP) l1 l2 :
([ list] ky1;y2 f <$> l1; l2, Φ k y1 y2)
......@@ -1337,13 +1355,22 @@ Section sep_map.
intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
Qed.
Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
Lemma big_sepM_lookup Φ m i x
{Haff : TCOr ( j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
m !! i = Some x ([ map] ky m, Φ k y) Φ i x.
Proof. intros. rewrite big_sepM_lookup_acc //. by rewrite sep_elim_l. Qed.
Proof.
intros Hi. destruct Haff.
{ rewrite big_sepM_delete // sep_elim_l //. }
{ rewrite big_sepM_lookup_acc // sep_elim_l //. }
Qed.
Lemma big_sepM_lookup_dom (Φ : K PROP) m i `{!Absorbing (Φ i)} :
Lemma big_sepM_lookup_dom (Φ : K PROP) m i
{Haff : TCOr ( j, Affine (Φ j)) (Absorbing (Φ i))} :
is_Some (m !! i) ([ map] k_ m, Φ k) Φ i.
Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
Proof.
intros [x ?]. eapply (big_sepM_lookup (λ i x, Φ i)); last done.
destruct Haff; exact _.
Qed.
Lemma big_sepM_singleton Φ i x : ([ map] ky {[i:=x]}, Φ k y) Φ i x.
Proof. by rewrite big_opM_singleton. Qed.
......@@ -2103,25 +2130,32 @@ Section map2.
rewrite !insert_id //.
Qed.
Lemma big_sepM2_lookup Φ m1 m2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
Lemma big_sepM2_lookup Φ m1 m2 i x1 x2
{Haff : TCOr ( j y1 y2, Affine (Φ j y1 y2)) (Absorbing (Φ i x1 x2))} :
m1 !! i = Some x1 m2 !! i = Some x2
([ map] ky1;y2 m1;m2, Φ k y1 y2) Φ i x1 x2.
Proof. intros. rewrite big_sepM2_lookup_acc //. by rewrite sep_elim_l. Qed.
Lemma big_sepM2_lookup_l Φ m1 m2 i x1 `{! x2, Absorbing (Φ i x1 x2)} :
Proof.
intros Hx1 Hx2. destruct Haff.
{ rewrite big_sepM2_delete // sep_elim_l //. }
{ rewrite big_sepM2_lookup_acc // sep_elim_l //. }
Qed.
Lemma big_sepM2_lookup_l Φ m1 m2 i x1
{Haff : TCOr ( j y1 y2, Affine (Φ j y1 y2)) ( x2, Absorbing (Φ i x1 x2))} :
m1 !! i = Some x1
([ map] ky1;y2 m1;m2, Φ k y1 y2)
x2, m2 !! i = Some x2 Φ i x1 x2.
Proof.
intros Hm1. rewrite big_sepM2_delete_l //.
f_equiv=> x2. by rewrite sep_elim_l.
f_equiv=> x2. erewrite sep_elim_l; first done. destruct Haff; exact _.
Qed.
Lemma big_sepM2_lookup_r Φ m1 m2 i x2 `{! x1, Absorbing (Φ i x1 x2)} :
Lemma big_sepM2_lookup_r Φ m1 m2 i x2
{Haff : TCOr ( j y1 y2, Affine (Φ j y1 y2)) ( x1, Absorbing (Φ i x1 x2))} :
m2 !! i = Some x2
([ map] ky1;y2 m1;m2, Φ k y1 y2)
x1, m1 !! i = Some x1 Φ i x1 x2.
Proof.
intros Hm2. rewrite big_sepM2_delete_r //.
f_equiv=> x1. by rewrite sep_elim_l.
f_equiv=> x1. erewrite sep_elim_l; first done. destruct Haff; exact _.
Qed.
Lemma big_sepM2_singleton Φ i x1 x2 :
......@@ -2529,9 +2563,13 @@ Section gset.
auto.
Qed.
Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} :
Lemma big_sepS_elem_of Φ X x
{Haff : TCOr ( y, Affine (Φ y)) (Absorbing (Φ x))} :
x X ([ set] y X, Φ y) Φ x.
Proof. intros. rewrite big_sepS_delete //. by rewrite sep_elim_l. Qed.
Proof.
intros. rewrite big_sepS_delete //. erewrite sep_elim_l; first done.
destruct Haff; exact _.
Qed.
Lemma big_sepS_elem_of_acc Φ X x :
x X
......@@ -2788,9 +2826,13 @@ Section gmultiset.
x X ([ mset] y X, Φ y) Φ x [ mset] y X {[+ x +]}, Φ y.
Proof. apply big_opMS_delete. Qed.
Lemma big_sepMS_elem_of Φ X x `{!Absorbing (Φ x)} :
Lemma big_sepMS_elem_of Φ X x
{Haff : TCOr ( y, Affine (Φ y)) (Absorbing (Φ x))} :
x X ([ mset] y X, Φ y) Φ x.
Proof. intros. rewrite big_sepMS_delete //. by rewrite sep_elim_l. Qed.
Proof.
intros. rewrite big_sepMS_delete //. erewrite sep_elim_l; first done.
destruct Haff; exact _.
Qed.
Lemma big_sepMS_elem_of_acc Φ X x :
x X
......
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