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

big_op: make more arguments implicit for the lemmas affected by previous 2 commits

i.e. all `big_op` lemmas that have a `TCOr` side condition.
parent 0ae5ad57
Pipeline #60872 passed with stage
in 7 minutes and 25 seconds
......@@ -12,6 +12,7 @@ lemma.
`Absorbing` instance. This breaks uses where an `Absorbing` instance was
provided without relying on TC search (e.g. in `by apply ...`; a possible fix
is `by apply: ...`).
* Make more arguments implicit for the lemmas in `big_op` assuming a `TCOr`.
**Changes in `proofmode`:**
......
......@@ -186,7 +186,7 @@ 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
Lemma big_sepL_lookup {Φ l} i x
`{!TCOr ( j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
l !! i = Some x ([ list] ky l, Φ k y) Φ i x.
Proof.
......@@ -197,7 +197,7 @@ Section sep_list.
- rewrite big_sepL_lookup_acc // sep_elim_l //.
Qed.
Lemma big_sepL_elem_of (Φ : A PROP) l x
Lemma big_sepL_elem_of {Φ : A PROP} {l} x
`{!TCOr ( y, Affine (Φ y)) (Absorbing (Φ x))} :
x l ([ list] y l, Φ y) Φ x.
Proof.
......@@ -636,7 +636,7 @@ Section sep_list2.
by rewrite !list_insert_id.
Qed.
Lemma big_sepL2_lookup Φ l1 l2 i x1 x2
Lemma big_sepL2_lookup {Φ l1 l2} i x1 x2
`{!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.
......@@ -1335,7 +1335,7 @@ Section sep_map.
([ map] ky <[i:=x]> m, Φ k y) Φ i x [ map] ky delete i m, Φ k y.
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))} :
Φ i x - ([ map] ky m, Φ k y) - [ map] ky <[i:=x]> m, Φ k y.
Proof.
......@@ -1355,7 +1355,7 @@ Section sep_map.
intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
Qed.
Lemma big_sepM_lookup Φ m i x
Lemma big_sepM_lookup {Φ m} i x
`{!TCOr ( j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
m !! i = Some x ([ map] ky m, Φ k y) Φ i x.
Proof.
......@@ -1364,7 +1364,7 @@ Section sep_map.
- rewrite big_sepM_lookup_acc // sep_elim_l //.
Qed.
Lemma big_sepM_lookup_dom (Φ : K PROP) m i
Lemma big_sepM_lookup_dom {Φ : K PROP} {m} i
`{!TCOr ( j, Affine (Φ j)) (Absorbing (Φ i))} :
is_Some (m !! i) ([ map] k_ m, Φ k) Φ i.
Proof. intros [x ?]. destruct select (TCOr _ _); by apply: big_sepM_lookup. Qed.
......@@ -2099,7 +2099,7 @@ Section map2.
by apply wand_intro_l.
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))} :
Φ i x1 x2 -
([ map] ky1;y2 m1;m2, Φ k y1 y2) -
......@@ -2113,7 +2113,7 @@ Section map2.
rewrite (sep_comm (Φ _ _ _)) -sep_assoc. apply sep_mono.
{ apply affinely_mono, pure_mono. intros Hm k.
rewrite !lookup_insert_is_Some. naive_solver. }
rewrite (big_sepM_insert_2 (λ k xx, Φ k xx.1 xx.2) (map_zip m1 m2) i (x1, x2)).
rewrite (big_sepM_insert_2 (Φ := λ k xx, Φ k xx.1 xx.2) (m := map_zip m1 m2) i (x1, x2)).
rewrite map_insert_zip_with. apply wand_elim_r.
Qed.
......@@ -2127,7 +2127,7 @@ Section map2.
rewrite !insert_id //.
Qed.
Lemma big_sepM2_lookup Φ m1 m2 i x1 x2
Lemma big_sepM2_lookup {Φ m1 m2} i x1 x2
`{!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.
......@@ -2136,7 +2136,7 @@ Section map2.
- 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
Lemma big_sepM2_lookup_l {Φ m1 m2} i x1
`{!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)
......@@ -2146,7 +2146,7 @@ Section map2.
f_equiv=> x2. erewrite sep_elim_l; first done.
destruct select (TCOr _ _); exact _.
Qed.
Lemma big_sepM2_lookup_r Φ m1 m2 i x2
Lemma big_sepM2_lookup_r {Φ m1 m2} i x2
`{!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)
......@@ -2562,7 +2562,7 @@ Section gset.
auto.
Qed.
Lemma big_sepS_elem_of Φ X x
Lemma big_sepS_elem_of {Φ X} x
`{!TCOr ( y, Affine (Φ y)) (Absorbing (Φ x))} :
x X ([ set] y X, Φ y) Φ x.
Proof.
......@@ -2825,7 +2825,7 @@ 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
Lemma big_sepMS_elem_of {Φ X} x
`{!TCOr ( y, Affine (Φ y)) (Absorbing (Φ x))} :
x X ([ mset] y X, Φ y) Φ x.
Proof.
......
......@@ -591,7 +591,7 @@ Lemma test_TC_resolution `{!BiAffine PROP} (Φ : nat → PROP) l x :
x l ([ list] y l, Φ y) - Φ x.
Proof.
iIntros (Hp) "HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
iDestruct (big_sepL_elem_of _ Hp with "HT") as "Hp".
done.
Qed.
......
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