diff --git a/channel/heap_lang.v b/channel/heap_lang.v
index b1bc26f03feb1c28747688c5675f60eb80a0e7cb..70a1bc1a96cd42af68954074dfdb84de416325e5 100644
--- a/channel/heap_lang.v
+++ b/channel/heap_lang.v
@@ -1,4 +1,3 @@
-Require Import mathcomp.ssreflect.ssreflect.
Require Import Autosubst.Autosubst.
Require Import prelude.option prelude.gmap iris.language.
diff --git a/modures/agree.v b/modures/agree.v
index 22aabb5f1a604da016eb8f875eefa2d00c1a3930..3020bf8c83d863cca8759ee0c829cb533c49b170 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -71,7 +71,7 @@ Proof.
eauto using agree_valid_le.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) op.
-Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy,!(commutative _ _ y2), Hx. Qed.
+Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
Instance: Associative (≡) (@op (agree A) _).
Proof.
@@ -82,19 +82,20 @@ Qed.
Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ={n}= x ⋅ y.
Proof.
split; [|by intros ?; exists y].
- by intros [z Hz]; rewrite Hz, (associative _), agree_idempotent.
+ by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
Qed.
Global Instance agree_cmra : CMRA (agree A).
Proof.
split; try (apply _ || done).
* intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
- rewrite <-(proj2 Hxy n'), (Hx n') by eauto using agree_valid_le.
+ rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le.
by apply dist_le with n; try apply Hxy.
* by intros n x1 x2 Hx y1 y2 Hy.
* intros x; split; [apply agree_valid_0|].
by intros n'; rewrite Nat.le_0_r; intros ->.
* intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
- rewrite (Hx n') by auto; symmetry; apply dist_le with n; try apply Hx; auto.
+ rewrite (Hx n'); last auto.
+ symmetry; apply dist_le with n; try apply Hx; auto.
* intros x; apply agree_idempotent.
* by intros x y n [(?&?&?) ?].
* by intros x y n; rewrite agree_includedN.
@@ -106,7 +107,7 @@ Global Instance agree_extend : CMRAExtend (agree A).
Proof.
intros n x y1 y2 ? Hx; exists (x,x); simpl; split.
* by rewrite agree_idempotent.
- * by rewrite Hx, (agree_op_inv x y1 y2), agree_idempotent by done.
+ * by rewrite Hx (agree_op_inv x y1 y2) // agree_idempotent.
Qed.
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
@@ -120,7 +121,7 @@ Proof. by intros ? [? Hx]; apply Hx. Qed.
Lemma agree_to_agree_inj (x y : agree A) a n :
✓{n} x → x ={n}= to_agree a ⋅ y → x n ={n}= a.
Proof.
- by intros; transitivity ((to_agree a â‹… y) n); [by apply agree_car_ne|].
+ by intros; transitivity ((to_agree a â‹… y) n); first apply agree_car_ne.
Qed.
End agree.
@@ -141,7 +142,7 @@ Section agree_map.
Proof.
split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
- split; [split; simpl; try tauto|done].
+ split; last done; split; simpl; last tauto.
by intros (?&?&Hxy); repeat split; intros;
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Qed.
@@ -157,6 +158,6 @@ Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
CofeMor (agree_map f : agreeRA A → agreeRA B).
Instance agreeRA_map_ne A B n : Proper (dist n ==> dist n) (@agreeRA_map A B).
Proof.
- intros f g Hfg x; split; simpl; intros; [done|].
+ intros f g Hfg x; split; simpl; intros; first done.
by apply dist_le with n; try apply Hfg.
Qed.
diff --git a/modures/auth.v b/modures/auth.v
index bc13913a40df336f882beade0d4cf130e9f9572b..44f63688500c3fe76a07f9f7c17e61ef7a01c984 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -86,15 +86,15 @@ Instance auth_cmra `{CMRA A} : CMRA (auth A).
Proof.
split.
* apply _.
- * by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
- * by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
+ * by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
+ * by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* intros n [x a] [y b] [Hx Ha]; simpl in *;
destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
* by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
- split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
+ split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
* by intros [[] ?]; simpl.
* intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
- * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN,
+ * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN
?cmra_valid_validN; [naive_solver|naive_solver|].
split; [done|intros Hn; discriminate (Hn 1)].
* by split; simpl; rewrite (associative _).
diff --git a/modures/base.v b/modures/base.v
new file mode 100644
index 0000000000000000000000000000000000000000..daca953991be97e2d08d06ae875329258e789c7a
--- /dev/null
+++ b/modures/base.v
@@ -0,0 +1,3 @@
+Require Export mathcomp.ssreflect.ssreflect.
+Require Export prelude.prelude.
+Global Set Bullet Behavior "Strict Subproofs".
diff --git a/modures/cmra.v b/modures/cmra.v
index 2e541ababa5237977d93c7bbaee8a3932a247607..d974534afd84b53fe927ce579ef87da602dc7141 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -110,7 +110,7 @@ Global Instance cmra_ra : RA A.
Proof.
split; try by (destruct cmra;
eauto using ne_proper, ne_proper_2 with typeclass_instances).
- * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite <-Hx.
+ * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
* intros x y; rewrite !cmra_included_includedN.
eauto using cmra_unit_preserving.
* intros x y; rewrite !cmra_valid_validN; intros ? n.
@@ -125,10 +125,10 @@ Proof. induction 2; eauto using cmra_valid_S. Qed.
Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (â‹…).
Proof.
intros x1 x2 Hx y1 y2 Hy.
- by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2).
+ by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Qed.
Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x).
-Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
+Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
(** * Timeless *)
Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
@@ -136,7 +136,7 @@ Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
Proof.
intros ?? [x' ?].
destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
- by exists z'; rewrite Hy, (timeless x z) by done.
+ by exists z'; rewrite Hy (timeless x z).
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{1} y → x ≼{n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
@@ -145,8 +145,8 @@ Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
Proof.
intros ??? z Hz.
destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
- { by rewrite <-?Hz; apply cmra_valid_validN. }
- by rewrite Hz', (timeless x1 y1), (timeless x2 y2).
+ { by rewrite -?Hz; apply cmra_valid_validN. }
+ by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
(** * Included *)
@@ -176,17 +176,17 @@ Proof.
split.
* by intros x; exists (unit x); rewrite ra_unit_r.
* intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite (associative _), <-Hy, <-Hz.
+ by rewrite (associative _) -Hy -Hz.
Qed.
Lemma cmra_valid_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
-Proof. intros Hyv [z Hy]; rewrite Hy in Hyv; eauto using cmra_valid_op_l. Qed.
+Proof. intros Hyv [z Hy]; revert Hyv; rewrite Hy; apply cmra_valid_op_l. Qed.
Lemma cmra_valid_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed.
Lemma cmra_included_dist_l x1 x2 x1' n :
x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
Proof.
intros [z Hx2] Hx1; exists (x1' â‹… z); split; auto using ra_included_l.
- by rewrite Hx1, Hx2.
+ by rewrite Hx1 Hx2.
Qed.
(** * Properties of [(â‡)] relation *)
@@ -281,11 +281,11 @@ Qed.
Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B).
Proof.
split; try apply _.
- * by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1, ?Hy2.
- * by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1, ?Hy2.
- * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite <-?Hy1, <-?Hy2.
+ * by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
+ * by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
+ * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite -?Hy1 -?Hy2.
* by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
- split; simpl in *; rewrite ?Hx1, ?Hx2, ?Hy1, ?Hy2.
+ split; simpl in *; rewrite ?Hx1 ?Hx2 ?Hy1 ?Hy2.
* split; apply cmra_valid_0.
* by intros n x [??]; split; apply cmra_valid_S.
* intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
diff --git a/modures/cofe.v b/modures/cofe.v
index 25eb6e1a9cf4904d22b635cb18b026d680e84ca9..bca6b342113729ea2cc88ba4bf69f7b709fb7a83 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -1,4 +1,4 @@
-Require Export prelude.prelude.
+Require Export modures.base.
(** Unbundeled version *)
Class Dist A := dist : nat → relation A.
@@ -75,8 +75,7 @@ Section cofe.
Qed.
Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (dist n).
Proof.
- intros x1 x2 Hx y1 y2 Hy.
- by rewrite equiv_dist in Hx, Hy; rewrite (Hx n), (Hy n).
+ by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Qed.
Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
@@ -90,10 +89,10 @@ Section cofe.
Proper ((≡) ==> (≡) ==> (≡)) f | 100.
Proof.
unfold Proper, respectful; setoid_rewrite equiv_dist.
- by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n), (Hy n).
+ by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n → compl c1 ={n}= compl c2.
- Proof. intros. by rewrite (conv_compl c1 n), (conv_compl c2 n). Qed.
+ Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
Global Instance contractive_ne `{Cofe B} (f : A → B) `{!Contractive f} n :
@@ -118,7 +117,7 @@ Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Next Obligation.
intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
- destruct i as [|i]; simpl; try lia; apply contractive, IH; auto with lia.
+ destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
Qed.
Program Definition fixpoint `{Cofe A, Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
@@ -129,14 +128,14 @@ Section fixpoint.
Proof.
apply equiv_dist; intros n; unfold fixpoint.
rewrite (conv_compl (fixpoint_chain f) n).
- by rewrite (chain_cauchy (fixpoint_chain f) n (S n)) at 1 by lia.
+ by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ={n}= g z) → fixpoint f ={n}= fixpoint g.
Proof.
intros Hfg; unfold fixpoint.
- rewrite (conv_compl (fixpoint_chain f) n),(conv_compl (fixpoint_chain g) n).
- induction n as [|n IH]; simpl in *; [done|].
+ rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
+ induction n as [|n IH]; simpl in *; first done.
rewrite Hfg; apply contractive, IH; auto using dist_S.
Qed.
Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
@@ -166,8 +165,8 @@ Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c,
{| cofe_mor_car x := compl (fun_chain c x) |}.
Next Obligation.
intros A B c n x y Hxy.
- rewrite (conv_compl (fun_chain c x) n), (conv_compl (fun_chain c y) n).
- simpl; rewrite Hxy; apply (chain_cauchy c); lia.
+ rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hxy.
+ apply (chain_cauchy c); lia.
Qed.
Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B).
Proof.
@@ -204,7 +203,7 @@ Instance: Params (@ccompose) 3.
Infix "â—Ž" := ccompose (at level 40, left associativity).
Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
f1 ={n}= f2 → g1 ={n}= g2 → f1 ◎ g1 ={n}= f2 ◎ g2.
-Proof. by intros Hf Hg x; simpl; rewrite (Hg x), (Hf (g2 x)). Qed.
+Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
(** Pre-composition as a functor *)
Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n :
diff --git a/modures/cofe_solver.v b/modures/cofe_solver.v
index 9517223b5b2fd03a9eb368c00fff2087ff025f95..d9dd6166ec057b6231dc391090a85ce8569734ba 100644
--- a/modures/cofe_solver.v
+++ b/modures/cofe_solver.v
@@ -17,7 +17,7 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT}
(f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) x x' :
(∀ x, f x ≡ f' x) → (∀ y, g y ≡ g' y) → x ≡ x' →
map (f,g) x ≡ map (f',g') x'.
-Proof. by rewrite <-!cofe_mor_ext; intros Hf Hg Hx; rewrite Hf, Hg, Hx. Qed.
+Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
Fixpoint A (k : nat) : cofeT :=
match k with 0 => CofeT unit | S k => F (A k) (A k) end.
@@ -30,13 +30,13 @@ Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
Lemma gf {k} (x : A k) : g (f x) ≡ x.
Proof.
induction k as [|k IH]; simpl in *; [by destruct x|].
- rewrite <-map_comp; rewrite <-(map_id _ _ x) at 2; by apply map_ext.
+ rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Qed.
Lemma fg {n k} (x : A (S k)) : n ≤ k → f (g x) ={n}= x.
Proof.
intros Hnk; apply dist_le with k; auto; clear Hnk.
induction k as [|k IH]; simpl; [apply dist_0|].
- rewrite <-(map_id _ _ x) at 2; rewrite <-map_comp; by apply map_contractive.
+ rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive.
Qed.
Arguments A _ : simpl never.
Arguments f {_} : simpl never.
@@ -56,8 +56,7 @@ Program Instance tower_compl : Compl tower := λ c,
Next Obligation.
intros c k; apply equiv_dist; intros n.
rewrite (conv_compl (tower_chain c k) n).
- rewrite (conv_compl (tower_chain c (S k)) n); simpl.
- by rewrite (g_tower (c n) k).
+ by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
Qed.
Instance tower_cofe : Cofe tower.
Proof.
@@ -69,9 +68,9 @@ Proof.
+ by intros X Y ? n.
+ by intros X Y Z ?? n; transitivity (Y n).
* intros k X Y HXY n; apply dist_S.
- by rewrite <-(g_tower X), (HXY (S n)), g_tower.
+ by rewrite -(g_tower X) (HXY (S n)) g_tower.
* intros X Y k; apply dist_0.
- * intros c n k; simpl; rewrite (conv_compl (tower_chain c k) n).
+ * intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
apply (chain_cauchy c); lia.
Qed.
Definition T : cofeT := CofeT tower.
@@ -81,16 +80,16 @@ Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
match i with 0 => cid | S i => gg i â—Ž g end.
Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x.
-Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)),IH]. Qed.
+Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
Lemma f_tower {n k} (X : tower) : n ≤ k → f (X k) ={n}= X (S k).
-Proof. intros. by rewrite <-(fg (X (S k))), <-(g_tower X). Qed.
+Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed.
Lemma ff_tower {n} k i (X : tower) : n ≤ k → ff i (X k) ={n}= X (i + k).
Proof.
intros; induction i as [|i IH]; simpl; [done|].
- by rewrite IH, (f_tower X) by lia.
+ by rewrite IH (f_tower X); last lia.
Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
-Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower, IH]. Qed.
+Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k).
Proof. by intros X Y HX. Qed.
@@ -114,14 +113,14 @@ Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
Proof.
assert (i = i2 + i1) by lia; simplify_equality'. revert j x H1.
induction i2 as [|i2 IH]; intros j X H1; simplify_equality';
- [by rewrite coerce_id|by rewrite g_coerce, IH].
+ [by rewrite coerce_id|by rewrite g_coerce IH].
Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof.
assert (i = i1 + i2) by lia; simplify_equality'.
induction i1 as [|i1 IH]; simplify_equality';
- [by rewrite coerce_id|by rewrite coerce_f, IH].
+ [by rewrite coerce_id|by rewrite coerce_f IH].
Qed.
Definition embed' {k} (i : nat) : A k -n> A i :=
@@ -135,10 +134,10 @@ Proof.
* symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
* exfalso; lia.
* assert (i = k) by lia; subst.
- rewrite (ff_ff _ (eq_refl (1 + (0 + k)))); simpl; rewrite gf.
+ rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf.
by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
- * assert (H : 1 + ((i - k) + k) = S i) by lia; rewrite (ff_ff _ H); simpl.
- rewrite <-(gf (ff (i - k) x)) at 2; rewrite g_coerce.
+ * assert (H : 1 + ((i - k) + k) = S i) by lia.
+ rewrite (ff_ff _ H) /= -{2}(gf (ff (i - k) x)) g_coerce.
by erewrite coerce_proper by done.
Qed.
Program Definition embed_inf (k : nat) (x : A k) : T :=
@@ -152,21 +151,21 @@ Proof.
rewrite equiv_dist; intros n i.
unfold embed_inf, embed; simpl; unfold embed'.
destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
- * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H); simpl.
+ * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=.
by erewrite g_coerce, gf, coerce_proper by done.
* assert (S k = 0 + (0 + i)) as H by lia.
rewrite (gg_gg _ H); simplify_equality'.
by rewrite (ff_ff _ (eq_refl (1 + (0 + k)))).
* exfalso; lia.
- * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H); simpl.
+ * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
by erewrite coerce_proper by done.
Qed.
Lemma embed_tower j n (X : T) : n ≤ j → embed j (X j) ={n}= X.
Proof.
intros Hn i; simpl; unfold embed'; destruct (le_lt_dec i j) as [H|H]; simpl.
- * rewrite <-(gg_tower i (j - i) X).
+ * rewrite -(gg_tower i (j - i) X).
apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
- * rewrite (ff_tower j (i-j) X) by lia; by destruct (Nat.sub_add _ _ _).
+ * rewrite (ff_tower j (i-j) X); last lia. by destruct (Nat.sub_add _ _ _).
Qed.
Program Definition unfold_chain (X : T) : chain (F T T) :=
@@ -175,14 +174,14 @@ Next Obligation.
intros X n i Hi.
assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
induction k as [|k Hk]; simpl; [done|].
- rewrite Hk, (f_tower X), f_S, <-map_comp by lia.
+ rewrite Hk (f_tower X); last lia; rewrite f_S -map_comp.
apply dist_S, map_contractive.
split; intros Y; symmetry; apply equiv_dist; [apply g_tower|apply embed_f].
Qed.
Definition unfold' (X : T) : F T T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold'.
Proof.
- by intros n X Y HXY; unfold unfold'; apply compl_ne; simpl; rewrite (HXY n).
+ by intros n X Y HXY; unfold unfold'; apply compl_ne; rewrite /= (HXY n).
Qed.
Definition unfold : T -n> F T T := CofeMor unfold'.
@@ -190,7 +189,7 @@ Program Definition fold' (X : F T T) : T :=
{| tower_car n := g (map (embed n,project n) X) |}.
Next Obligation.
intros X k; apply (_ : Proper ((≡) ==> (≡)) g).
- rewrite <-(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g).
+ rewrite -(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g).
apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
Qed.
Instance fold_ne : Proper (dist n ==> dist n) fold'.
@@ -202,14 +201,14 @@ Proof.
assert (map_ff_gg : ∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
map (ff i, gg i) x ≡ gg i (coerce H x)).
{ intros i; induction i as [|i IH]; intros k x H; simpl.
- { by rewrite coerce_id, map_id. }
- rewrite map_comp, g_coerce; apply IH. }
+ { by rewrite coerce_id map_id. }
+ rewrite map_comp g_coerce; apply IH. }
rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
- rewrite <-g_tower, <-(gg_tower _ n); apply (_ : Proper (_ ==> _) g).
+ rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) g).
transitivity (map (ff n, gg n) (X (S (n + k)))).
{ unfold unfold'; rewrite (conv_compl (unfold_chain X) n).
- rewrite (chain_cauchy (unfold_chain X) n (n + k)) by lia; simpl.
- rewrite (f_tower X), <-map_comp by lia.
+ rewrite (chain_cauchy (unfold_chain X) n (n + k)) /=; last lia.
+ rewrite (f_tower X); last lia; rewrite -map_comp.
apply dist_S. apply map_contractive; split; intros x; simpl; unfold embed'.
* destruct (le_lt_dec _ _); simpl.
{ assert (n = 0) by lia; subst. apply dist_0. }
@@ -221,12 +220,12 @@ Proof.
Qed.
Definition unfold_fold X : unfold (fold X) ≡ X.
Proof.
- rewrite equiv_dist; intros n; unfold unfold; simpl.
- unfold unfold'; rewrite (conv_compl (unfold_chain (fold X)) n); simpl.
- rewrite (fg (map (embed _,project n) X)),
- <-map_comp by lia; rewrite <-(map_id _ _ X) at 2.
+ rewrite equiv_dist; intros n.
+ rewrite /(unfold) /= /(unfold') (conv_compl (unfold_chain (fold X)) n) /=.
+ rewrite (fg (map (embed _,project n) X)); last lia.
+ rewrite -map_comp -{2}(map_id _ _ X).
apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia.
Qed.
End solver.
-Global Opaque cofe_solver.T cofe_solver.fold cofe_solver.unfold.
+Global Opaque T fold unfold.
diff --git a/modures/dra.v b/modures/dra.v
index 20d73cb0a72b26a2184627da9a964ca2fa647916..3bf9e306a24135b777f5d026cbf55373b9ed4510 100644
--- a/modures/dra.v
+++ b/modures/dra.v
@@ -67,19 +67,17 @@ Hint Immediate dra_op_proper : typeclass_instances.
Instance: Proper ((≡) ==> (≡) ==> iff) (⊥).
Proof.
intros x1 x2 Hx y1 y2 Hy; split.
- * by rewrite Hy, (symmetry_iff (⊥) x1), (symmetry_iff (⊥) x2), Hx.
- * by rewrite <-Hy, (symmetry_iff (⊥) x2), (symmetry_iff (⊥) x1), <-Hx.
+ * by rewrite Hy (symmetry_iff (⊥) x1) (symmetry_iff (⊥) x2) Hx.
+ * by rewrite -Hy (symmetry_iff (⊥) x2) (symmetry_iff (⊥) x1) -Hx.
Qed.
Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
-Proof.
- intros ????. rewrite dra_commutative by done. by apply dra_disjoint_ll.
-Qed.
+Proof. intros ????. rewrite dra_commutative //. by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_move_r x y z :
✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
Proof.
- intros; symmetry; rewrite dra_commutative by eauto using dra_disjoint_rl.
+ intros; symmetry; rewrite dra_commutative; eauto using dra_disjoint_rl.
apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
Qed.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
@@ -100,20 +98,21 @@ Program Instance validity_minus : Minus T := λ x y,
Validity (validity_car x ⩪ validity_car y)
(✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _.
Solve Obligations with naive_solver auto using dra_minus_valid.
+
Instance validity_ra : RA T.
Proof.
split.
* apply _.
* intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_ands';
- first [by rewrite ?Heq by tauto|by rewrite <-?Heq by tauto|tauto].
+ first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
* by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
- * by intros ?? Heq ?; rewrite <-Heq.
+ * by intros ?? -> ?.
* intros x1 x2 [? Hx] y1 y2 [? Hy];
- split; simpl; [|by intros (?&?&?); rewrite Hx, Hy].
+ split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
split; intros (?&?&z&?&?); split_ands'; try tauto.
- + exists z. by rewrite <-Hy, <-Hx.
- + exists z. by rewrite Hx, Hy by tauto.
+ + exists z. by rewrite -Hy // -Hx.
+ + exists z. by rewrite Hx ?Hy; tauto.
* intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
|intros; apply (associative _)].
diff --git a/modures/excl.v b/modures/excl.v
index dd6c4d71f849d44b25f758757658452cfe9fe2fe..1014ece16e034d961b3671a701390819ea802aa9 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -61,13 +61,15 @@ Proof.
feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
destruct (c 1); simplify_equality'.
Qed.
-Instance Excl_timeless `{Equiv A, Dist A} (x : excl A) :
- Timeless x → Timeless (Excl x).
+Instance Excl_timeless `{Equiv A, Dist A} (x:A) :Timeless x → Timeless (Excl x).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Instance ExclUnit_timeless `{Equiv A, Dist A} : Timeless (@ExclUnit A).
Proof. by inversion_clear 1; constructor. Qed.
Instance ExclBot_timeless `{Equiv A, Dist A} : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
+Instance excl_timeless `{Equiv A, Dist A} :
+ (∀ x : A, Timeless x) → ∀ x : excl A, Timeless x.
+Proof. intros ? []; apply _. Qed.
(* CMRA *)
Instance excl_valid {A} : Valid (excl A) := λ x,
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index 65267bb0fb95ff152a0df3d66a465cc2c2773339..9c25aa3320fd3775a3e96b6d9398963d5f3f35c2 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -56,15 +56,16 @@ Global Instance map_lookup_timeless `{Cofe A} (m : gmap K A) i :
Timeless m → Timeless (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
- rewrite (timeless m (<[i:=x]>m)), lookup_insert; auto.
- by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id.
+ assert (m ={1}= <[i:=x]> m)
+ by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
+ by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
Qed.
Global Instance map_ra_insert_timeless `{Cofe A} (m : gmap K A) i x :
Timeless x → Timeless m → Timeless (<[i:=x]>m).
Proof.
intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
- { by apply (timeless _); rewrite <-Hm, lookup_insert. }
- by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done.
+ { by apply (timeless _); rewrite -Hm lookup_insert. }
+ by apply (timeless _); rewrite -Hm lookup_insert_ne.
Qed.
Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
Timeless x → Timeless ({[ i ↦ x ]} : gmap K A) := _.
@@ -78,7 +79,7 @@ Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
Global Instance mapC_map_ne {A B} n :
Proper (dist n ==> dist n) (@mapC_map A B).
Proof.
- intros f g Hf m k; simpl; rewrite !lookup_fmap.
+ intros f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
@@ -99,59 +100,58 @@ Lemma map_included_spec `{CMRA A} (m1 m2 : gmap K A) :
m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
Proof.
split.
- * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
+ * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
* intros Hm; exists (m2 ⩪ m1); intros i.
- by rewrite lookup_op, lookup_minus, ra_op_minus.
+ by rewrite lookup_op lookup_minus ra_op_minus.
Qed.
Lemma map_includedN_spec `{CMRA A} (m1 m2 : gmap K A) n :
m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
Proof.
split.
- * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm.
+ * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
* intros Hm; exists (m2 ⩪ m1); intros i.
- by rewrite lookup_op, lookup_minus, cmra_op_minus.
+ by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
Global Instance map_cmra `{CMRA A} : CMRA (gmap K A).
Proof.
split.
* apply _.
- * by intros n m1 m2 m3 Hm i; rewrite !lookup_op, (Hm i).
- * by intros n m1 m2 Hm i; rewrite !lookup_unit, (Hm i).
- * by intros n m1 m2 Hm ? i; rewrite <-(Hm i).
- * intros n m1 m1' Hm1 m2 m2' Hm2 i.
- by rewrite !lookup_minus, (Hm1 i), (Hm2 i).
+ * by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
+ * by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
+ * by intros n m1 m2 Hm ? i; rewrite -(Hm i).
+ * by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
* by intros m i.
* intros n m Hm i; apply cmra_valid_S, Hm.
* intros m; split; [by intros Hm n i; apply cmra_valid_validN|].
intros Hm i; apply cmra_valid_validN; intros n; apply Hm.
- * by intros m1 m2 m3 i; rewrite !lookup_op, (associative _).
- * by intros m1 m2 i; rewrite !lookup_op, (commutative _).
- * by intros m i; rewrite lookup_op, !lookup_unit, ra_unit_l.
- * by intros m i; rewrite !lookup_unit, ra_unit_idempotent.
+ * by intros m1 m2 m3 i; rewrite !lookup_op (associative _).
+ * by intros m1 m2 i; rewrite !lookup_op (commutative _).
+ * by intros m i; rewrite lookup_op !lookup_unit ra_unit_l.
+ * by intros m i; rewrite !lookup_unit ra_unit_idempotent.
* intros n x y; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_unit; apply cmra_unit_preserving.
* intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i).
- by rewrite <-lookup_op.
+ by rewrite -lookup_op.
* intros x y n; rewrite map_includedN_spec; intros ? i.
- by rewrite lookup_op, lookup_minus, cmra_op_minus by done.
+ by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
Global Instance map_ra_empty `{RA A} : RAIdentity (gmap K A).
Proof.
split.
* by intros ?; rewrite lookup_empty.
- * by intros m i; simpl; rewrite lookup_op, lookup_empty; destruct (m !! i).
+ * by intros m i; rewrite /= lookup_op lookup_empty; destruct (m !! i).
Qed.
Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (gmap K A).
Proof.
intros n m m1 m2 Hm Hm12.
assert (∀ i, m !! i ={n}= m1 !! i ⋅ m2 !! i) as Hm12'
- by (by intros i; rewrite <-lookup_op).
+ by (by intros i; rewrite -lookup_op).
set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
set (f_proj i := proj1_sig (f i)).
exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
- repeat split; simpl; intros i; rewrite ?lookup_op, !lookup_imap.
+ repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
* destruct (m !! i) as [x|] eqn:Hx; simpl; [|constructor].
- rewrite <-Hx; apply (proj2_sig (f i)).
+ rewrite -Hx; apply (proj2_sig (f i)).
* destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
@@ -176,7 +176,7 @@ Qed.
Global Instance map_ra_singleton_valid_timeless `{Valid A, ValidN A} (i : K) x :
ValidTimeless x → ValidTimeless ({[ i ↦ x ]} : gmap K A).
Proof.
- intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl.
+ intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _).
by rewrite lookup_empty.
Qed.
Lemma map_insert_valid `{ValidN A} (m : gmap K A) n i x :
@@ -210,7 +210,7 @@ Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma map_dom_op `{Op A} (m1 m2 : gmap K A) :
dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
Proof.
- apply elem_of_equiv; intros i; rewrite elem_of_union, !elem_of_dom.
+ apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
unfold is_Some; setoid_rewrite lookup_op.
destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
@@ -219,10 +219,10 @@ Lemma map_update_alloc `{CMRA A} (m : gmap K A) x :
Proof.
intros ? mf n Hm. set (i := fresh (dom (gset K) (m â‹… mf))).
assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [??].
- { rewrite <-not_elem_of_union, <-map_dom_op; apply is_fresh. }
+ { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. }
exists (<[i:=x]>m); split; [exists i; split; [done|]|].
* by apply not_elem_of_dom.
- * rewrite <-map_insert_op by (by apply not_elem_of_dom).
+ * rewrite -map_insert_op; last by apply not_elem_of_dom.
by apply map_insert_valid; [apply cmra_valid_validN|].
Qed.
End map.
diff --git a/modures/logic.v b/modures/logic.v
index 442ae8144af04267b2f87f6e49d02089b0911199..c717b2b87505e6c09527e6c0e150011df064c7b1 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -67,7 +67,7 @@ Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
`{!CMRAMonotone f, !CMRAMonotone g} n :
f ={n}= g → uPredC_map f ={n}= uPredC_map g.
Proof.
- by intros Hfg P y n' ??; simpl; rewrite (dist_le _ _ _ _(Hfg y)) by lia.
+ by intros Hfg P y n' ??; rewrite /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.
(** logical entailement *)
@@ -123,13 +123,13 @@ Next Obligation.
Qed.
Next Obligation. by intros M P Q x; exists x, x. Qed.
Next Obligation.
- intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ? Hvalid.
+ intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
{ destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using ra_included_l.
- apply dist_le with n1; auto. by rewrite (associative op), <-Hx, Hy. }
- rewrite Hy in Hvalid; exists x1, x2'; split_ands; auto.
- * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
- * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
+ apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
+ exists x1, x2'; split_ands; [done| |].
+ * cofe_subst y; apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
+ * cofe_subst y; apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
Qed.
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
@@ -137,7 +137,7 @@ Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Next Obligation.
intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
- rewrite <-(dist_le _ _ _ _ Hx) by done; apply HPQ; auto.
+ rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
by rewrite (dist_le _ _ _ n2 Hx).
Qed.
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
@@ -165,11 +165,11 @@ Qed.
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
-Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite <-Hx. Qed.
+Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Next Obligation. by intros M a x; exists x. Qed.
Next Obligation.
intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
- exists (a' â‹… x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx.
+ exists (a' â‹… x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx.
Qed.
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
@@ -231,9 +231,9 @@ Qed.
Global Instance entails_proper :
Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation (uPred M)).
Proof.
- intros P1 P2 HP Q1 Q2 HQ; rewrite equiv_spec in HP, HQ; split; intros.
- * by rewrite (proj2 HP), <-(proj1 HQ).
- * by rewrite (proj1 HP), <-(proj2 HQ).
+ move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
+ * by transitivity P1; [|transitivity Q1].
+ * by transitivity P2; [|transitivity Q2].
Qed.
(** Non-expansiveness and setoid morphisms *)
@@ -261,8 +261,8 @@ Global Instance impl_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_impl M) := ne_proper_2 _.
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Proof.
- intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?);
- exists x1, x2; rewrite Hx in Hx'; split_ands; try apply HP; try apply HQ;
+ intros P P' HP Q Q' HQ x n' ??; split; intros (x1&x2&?&?&?); cofe_subst x;
+ exists x1, x2; split_ands; try (apply HP || apply HQ);
eauto using cmra_valid_op_l, cmra_valid_op_r.
Qed.
Global Instance sep_proper :
@@ -279,8 +279,8 @@ Global Instance eq_ne (A : cofeT) n :
Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Proof.
intros x x' Hx y y' Hy z n'; split; intros; simpl in *.
- * by rewrite <-(dist_le _ _ _ _ Hx), <-(dist_le _ _ _ _ Hy) by auto.
- * by rewrite (dist_le _ _ _ _ Hx), (dist_le _ _ _ _ Hy) by auto.
+ * by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
+ * by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.
Global Instance eq_proper (A : cofeT) :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
@@ -314,7 +314,8 @@ Global Instance always_proper :
Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_own M).
Proof.
by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
- [rewrite <-(dist_le _ _ _ _ Ha) by lia|rewrite (dist_le _ _ _ _ Ha) by lia].
+ [rewrite -(dist_le _ _ _ _ Ha); last lia
+ |rewrite (dist_le _ _ _ _ Ha); last lia].
Qed.
Global Instance own_proper : Proper ((≡) ==> (≡)) (@uPred_own M) := ne_proper _.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
@@ -377,9 +378,9 @@ Proof. by intros HPQ x [|n] ?; [|split; intros; apply HPQ with x (S n)]. Qed.
(* Derived logical stuff *)
Lemma and_elim_l' P Q R : P ⊆ R → (P ∧ Q)%I ⊆ R.
-Proof. by rewrite and_elim_l. Qed.
+Proof. by rewrite ->and_elim_l. Qed.
Lemma and_elim_r' P Q R : Q ⊆ R → (P ∧ Q)%I ⊆ R.
-Proof. by rewrite and_elim_r. Qed.
+Proof. by rewrite ->and_elim_r. Qed.
Lemma or_intro_l' P Q R : P ⊆ Q → P ⊆ (Q ∨ R)%I.
Proof. intros ->; apply or_intro_l. Qed.
Lemma or_intro_r' P Q R : P ⊆ R → P ⊆ (Q ∨ R)%I.
@@ -443,7 +444,7 @@ Qed.
Lemma exist_mono {A} (P Q : A → uPred M) :
(∀ a, P a ⊆ Q a) → (∃ a, P a)%I ⊆ (∃ a, Q a)%I.
Proof.
- intros HPQ. apply exist_elim; intros a; rewrite (HPQ a); apply exist_intro.
+ intros HPQ. apply exist_elim; intros a; rewrite ->(HPQ a); apply exist_intro.
Qed.
Global Instance const_mono' : Proper (impl ==> (⊆)) (@uPred_const M).
@@ -473,14 +474,13 @@ Qed.
(* BI connectives *)
Lemma sep_mono P P' Q Q' : P ⊆ Q → P' ⊆ Q' → (P ★ P')%I ⊆ (Q ★ Q')%I.
Proof.
- intros HQ HQ' x n' Hx' (x1&x2&Hx&?&?); exists x1, x2;
- rewrite Hx in Hx'; eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
+ intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
+ eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
Qed.
Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
intros P x n Hvalid; split.
- * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *.
- eauto using uPred_weaken, ra_included_r.
+ * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, ra_included_r.
* by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Qed.
Global Instance sep_commutative : Commutative (≡) (@uPred_sep M).
@@ -492,10 +492,10 @@ Global Instance sep_associative : Associative (≡) (@uPred_sep M).
Proof.
intros P Q R x n ?; split.
* intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_ands; auto.
- + by rewrite <-(associative op), <-Hy, <-Hx.
+ + by rewrite -(associative op) -Hy -Hx.
+ by exists x1, y1.
* intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_ands; auto.
- + by rewrite (associative op), <-Hy, <-Hx.
+ + by rewrite (associative op) -Hy -Hx.
+ by exists y2, x2.
Qed.
Lemma wand_intro P Q R : (R ★ P)%I ⊆ Q → R ⊆ (P -★ Q)%I.
@@ -505,9 +505,7 @@ Proof.
eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Qed.
Lemma wand_elim P Q : ((P -★ Q) ★ P)%I ⊆ Q.
-Proof.
- by intros x n Hvalid (x1&x2&Hx&HPQ&?); rewrite Hx in Hvalid |- *; apply HPQ.
-Qed.
+Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
Lemma or_sep_distr P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
Proof.
split; [by intros (x1&x2&Hx&[?|?]&?); [left|right]; exists x1, x2|].
@@ -526,16 +524,14 @@ Hint Resolve sep_mono.
Global Instance sep_mono' : Proper ((⊆) ==> (⊆) ==> (⊆)) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Lemma wand_mono P P' Q Q' : Q ⊆ P → P' ⊆ Q' → (P -★ P')%I ⊆ (Q -★ Q')%I.
-Proof.
- intros HP HQ; apply wand_intro; rewrite HP, <-HQ; apply wand_elim.
-Qed.
+Proof. intros HP HQ; apply wand_intro; rewrite ->HP, <-HQ; apply wand_elim. Qed.
Global Instance wand_mono' : Proper (flip (⊆) ==> (⊆) ==> (⊆)) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
Global Instance sep_True : RightId (≡) True%I (@uPred_sep M).
-Proof. by intros P; rewrite (commutative _), (left_id _ _). Qed.
+Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
Lemma sep_elim_l P Q : (P ★ Q)%I ⊆ P.
-Proof. by rewrite (True_intro Q), (right_id _ _). Qed.
+Proof. by rewrite ->(True_intro Q), (right_id _ _). Qed.
Lemma sep_elim_r P Q : (P ★ Q)%I ⊆ Q.
Proof. by rewrite (commutative (★))%I; apply sep_elim_l. Qed.
Lemma sep_elim_l' P Q R : P ⊆ R → (P ★ Q)%I ⊆ R.
@@ -555,7 +551,7 @@ Lemma and_sep_distr P Q R : ((P ∧ Q) ★ R)%I ⊆ ((P ★ R) ∧ (Q ★ R))%I.
Proof. auto. Qed.
Lemma forall_sep_distr `(P : A → uPred M) Q :
((∀ a, P a) ★ Q)%I ⊆ (∀ a, P a ★ Q)%I.
-Proof. by apply forall_intro; intros a; rewrite forall_elim. Qed.
+Proof. by apply forall_intro; intros a; rewrite ->forall_elim. Qed.
(* Later *)
Lemma later_mono P Q : P ⊆ Q → (▷ P)%I ⊆ (▷ Q)%I.
@@ -587,7 +583,7 @@ Proof.
* destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
destruct (cmra_extend_op n x x1 x2)
as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
- exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
+ exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
* destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using (dist_S (A:=M)).
Qed.
@@ -630,7 +626,7 @@ Qed.
Lemma always_and_sep_l P Q : (□ P ∧ Q)%I ⊆ (□ P ★ Q)%I.
Proof.
intros x n ? [??]; exists (unit x), x; simpl in *.
- by rewrite ra_unit_l, ra_unit_idempotent.
+ by rewrite ra_unit_l ra_unit_idempotent.
Qed.
Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
Proof. done. Qed.
@@ -641,7 +637,7 @@ Proof.
apply (anti_symmetric (⊆)); auto using always_elim, always_intro.
Qed.
Lemma always_mono P Q : P ⊆ Q → (□ P)%I ⊆ (□ Q)%I.
-Proof. intros. apply always_intro. by rewrite always_elim. Qed.
+Proof. intros. apply always_intro. by rewrite ->always_elim. Qed.
Hint Resolve always_mono.
Global Instance always_mono' : Proper ((⊆) ==> (⊆)) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
@@ -676,7 +672,7 @@ Lemma always_wand_impl P Q : (□ (P -★ Q))%I ≡ (□ (P → Q))%I.
Proof.
apply (anti_symmetric (⊆)); [|by rewrite <-impl_wand].
apply always_intro, impl_intro.
- by rewrite always_and_sep_l, always_elim, wand_elim.
+ by rewrite ->always_and_sep_l, always_elim, wand_elim.
Qed.
(* Own *)
@@ -687,13 +683,13 @@ Proof.
* intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (associative op)|].
split. by exists (unit a1); rewrite ra_unit_r. by exists z.
* intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
- rewrite (associative op), <-(commutative op z1), <-!(associative op), <-Hy2.
- by rewrite (associative op), (commutative op z1), <-Hy1.
+ by rewrite (associative op _ z1) -(commutative op z1) (associative op z1)
+ -(associative op _ a2) (commutative op z1) -Hy1 -Hy2.
Qed.
Lemma box_own_unit (a : M) : (□ uPred_own (unit a))%I ≡ uPred_own (unit a).
Proof.
intros x n; split; [by apply always_elim|intros [a' Hx]]; simpl.
- rewrite <-(ra_unit_idempotent a), Hx.
+ rewrite -(ra_unit_idempotent a) Hx.
apply cmra_unit_preserving, cmra_included_l.
Qed.
Lemma box_own (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
@@ -701,9 +697,7 @@ Proof. by intros <-; rewrite box_own_unit. Qed.
Lemma own_empty `{Empty M, !RAIdentity M} : True%I ⊆ uPred_own ∅.
Proof. intros x [|n] ??; [done|]. by exists x; rewrite (left_id _ _). Qed.
Lemma own_valid (a : M) : uPred_own a ⊆ (✓ a)%I.
-Proof.
- intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l.
-Qed.
+Proof. move => x n Hv [a' ?]; cofe_subst; eauto using cmra_valid_op_l. Qed.
Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True%I ⊆ (✓ a : uPred M)%I.
Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
Lemma valid_elim_timeless {A : cmraT} (a : A) :
@@ -715,32 +709,32 @@ Qed.
(* Big ops *)
Global Instance uPred_big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; simpl; rewrite ?HPQ, ?IH. Qed.
+Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance uPred_big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; simpl; rewrite ?HPQ, ?IH. Qed.
+Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance uPred_big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH.
- * by rewrite !(associative _), (commutative _ P).
+ * by rewrite !(associative _) (commutative _ P).
* etransitivity; eauto.
Qed.
Global Instance uPred_big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH.
- * by rewrite !(associative _), (commutative _ P).
+ * by rewrite !(associative _) (commutative _ P).
* etransitivity; eauto.
Qed.
Lemma uPred_big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
Proof.
by induction Ps as [|P Ps IH];
- simpl; rewrite ?(left_id _ _), <-?(associative _), ?IH.
+ rewrite /= ?(left_id _ _) -?(associative _) ?IH.
Qed.
Lemma uPred_big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
Proof.
by induction Ps as [|P Ps IH];
- simpl; rewrite ?(left_id _ _), <-?(associative _), ?IH.
+ rewrite /= ?(left_id _ _) -?(associative _) ?IH.
Qed.
Lemma uPred_big_sep_and Ps : (Π★ Ps)%I ⊆ (Π∧ Ps)%I.
Proof. by induction Ps as [|P Ps IH]; simpl; auto. Qed.
@@ -768,9 +762,9 @@ Global Instance sep_timeless P Q :
Proof.
intros ?? x [|n] Hvalid (x1&x2&Hx12&?&?); [done|].
destruct (cmra_extend_op 1 x x1 x2) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *.
- rewrite Hx12 in Hvalid; exists y1, y2; split_ands; [by rewrite Hx| |].
- * apply timelessP; rewrite Hy1; eauto using cmra_valid_op_l.
- * apply timelessP; rewrite Hy2; eauto using cmra_valid_op_r.
+ exists y1, y2; split_ands; [by apply equiv_dist| |].
+ * cofe_subst x; apply timelessP; rewrite Hy1; eauto using cmra_valid_op_l.
+ * cofe_subst x; apply timelessP; rewrite Hy2; eauto using cmra_valid_op_r.
Qed.
Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
@@ -787,7 +781,7 @@ Proof. by intros ? x [|n] ?; [|intros [a ?]; exists a; apply timelessP]. Qed.
Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
Proof. intros ? x n ??; simpl; apply timelessP; auto using cmra_unit_valid. Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
- Timeless a → TimelessP (a ≡ b : uPred M).
+ Timeless a → TimelessP (a ≡ b : uPred M)%I.
Proof. by intros ? x n ??; apply equiv_dist, timeless. Qed.
(** Timeless elements *)
diff --git a/modures/ra.v b/modures/ra.v
index 86dde1644fbc37d30d19674dbfbe3f0965747469..bbda7ad82bf097ae07da204e46b28a22a66e2b0d 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -1,4 +1,5 @@
Require Export prelude.collections prelude.relations prelude.fin_maps.
+Require Export modures.base.
Class Valid (A : Type) := valid : A → Prop.
Instance: Params (@valid) 2.
@@ -80,20 +81,20 @@ Proof. by intros ???; split; apply ra_valid_proper. Qed.
Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (⋅).
Proof.
intros x1 x2 Hx y1 y2 Hy.
- by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2).
+ by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Qed.
Lemma ra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed.
(** ** Units *)
Lemma ra_unit_r x : x ⋅ unit x ≡ x.
-Proof. by rewrite (commutative _ x), ra_unit_l. Qed.
+Proof. by rewrite (commutative _ x) ra_unit_l. Qed.
Lemma ra_unit_unit x : unit x ⋅ unit x ≡ unit x.
-Proof. by rewrite <-(ra_unit_idempotent x) at 2; rewrite ra_unit_r. Qed.
+Proof. by rewrite -{2}(ra_unit_idempotent x) ra_unit_r. Qed.
(** ** Order *)
Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> impl) (≼).
-Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite <-Hy, Hz, Hx. Qed.
+Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite -Hy Hz Hx. Qed.
Global Instance ra_included_proper : Proper ((≡) ==> (≡) ==> iff) (≼).
Proof. by split; apply ra_included_proper'. Qed.
Lemma ra_included_l x y : x ≼ x ⋅ y.
@@ -102,25 +103,24 @@ Lemma ra_included_r x y : y ≼ x ⋅ y.
Proof. rewrite (commutative op); apply ra_included_l. Qed.
Global Instance: PreOrder included.
Proof.
- split.
- * by intros x; exists (unit x); rewrite ra_unit_r.
- * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
- by rewrite (associative _), <-Hy, <-Hz.
+ split; first by intros x; exists (unit x); rewrite ra_unit_r.
+ intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+ by rewrite (associative _) -Hy -Hz.
Qed.
Lemma ra_included_unit x : unit x ≼ x.
Proof. by exists x; rewrite ra_unit_l. Qed.
Lemma ra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1, (associative (â‹…)). Qed.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative (â‹…)). Qed.
Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
-Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed.
+Proof. by intros; rewrite -!(commutative _ z); apply ra_preserving_l. Qed.
(** ** RAs with empty element *)
Context `{Empty A, !RAIdentity A}.
Global Instance ra_empty_r : RightId (≡) ∅ (⋅).
-Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed.
+Proof. by intros x; rewrite (commutative op) (left_id _ _). Qed.
Lemma ra_unit_empty : unit ∅ ≡ ∅.
-Proof. by rewrite <-(ra_unit_l ∅) at 2; rewrite (right_id _ _). Qed.
+Proof. by rewrite -{2}(ra_unit_l ∅) (right_id _ _). Qed.
Lemma ra_empty_least x : ∅ ≼ x.
Proof. by exists x; rewrite (left_id _ _). Qed.
@@ -129,15 +129,15 @@ Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
Proof.
induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
* by rewrite IH.
- * by rewrite !(associative _), (commutative _ x).
+ * by rewrite !(associative _) (commutative _ x).
* by transitivity (big_op xs2).
Qed.
Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
Proof.
- induction xs as [|x xs IH]; simpl; [by rewrite ?(left_id _ _)|].
- by rewrite IH, (associative _).
+ induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
+ by rewrite IH (associative _).
Qed.
Context `{FinMap K M}.
@@ -145,20 +145,21 @@ Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
Lemma big_opM_insert (m : M A) i x :
m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
-Proof. intros ?; unfold big_opM. by rewrite map_to_list_insert by done. Qed.
+Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
Proof.
- rewrite <-insert_empty, big_opM_insert by auto using lookup_empty; simpl.
- by rewrite big_opM_empty, (right_id _ _).
+ rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
+ by rewrite big_opM_empty (right_id _ _).
Qed.
Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
Proof.
intros m1; induction m1 as [|i x m1 ? IH] using map_ind.
- { by intros m2; rewrite (symmetry_iff (≡)), map_equiv_empty; intros ->. }
- intros m2 Hm2; rewrite big_opM_insert by done.
- rewrite (IH (delete i m2)) by (by rewrite <-Hm2, delete_insert).
+ { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
+ intros m2 Hm2; rewrite big_opM_insert //.
+ rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
as (y&?&Hxy); auto using lookup_insert.
- by rewrite Hxy, <-big_opM_insert, insert_delete by auto using lookup_delete.
+ rewrite Hxy -big_opM_insert; last auto using lookup_delete.
+ by rewrite insert_delete.
Qed.
End ra.
diff --git a/modures/sts.v b/modures/sts.v
index aee7969f19e3489f00bb31958771b5f08346dd6b..5770768f6b3dff44b6fabf9bf5920e2f41ca3466 100644
--- a/modures/sts.v
+++ b/modures/sts.v
@@ -81,7 +81,7 @@ Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts. Qed.
Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
Proof.
intros ?? HT ?? HS; destruct 1;
- constructor; intros until 0; rewrite <-?HS, <-?HT; eauto.
+ constructor; intros until 0; rewrite -?HS -?HT; eauto.
Qed.
Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
@@ -103,7 +103,7 @@ Qed.
Instance up_proper : Proper ((≡) ==> (=) ==> (≡)) up.
Proof. by intros ?? [??] ???; split; apply up_preserving. Qed.
Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
-Proof. by intros T1 T2 HT S1 S2 HS; unfold up_set; rewrite HS, HT. Qed.
+Proof. by intros T1 T2 HT S1 S2 HS; rewrite /up_set HS HT. Qed.
Lemma elem_of_up s T : s ∈ up T s.
Proof. constructor. Qed.
Lemma subseteq_up_set S T : S ⊆ up_set T S.
@@ -124,7 +124,7 @@ Lemma closed_up_set_empty S : S ≢ ∅ → closed ∅ (up_set ∅ S).
Proof. eauto using closed_up_set with sts. Qed.
Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed T (up T s).
Proof.
- intros; rewrite <-(collection_bind_singleton (up T) s).
+ intros; rewrite -(collection_bind_singleton (up T) s).
apply closed_up_set; esolve_elem_of.
Qed.
Lemma closed_up_empty s : closed ∅ (up ∅ s).
@@ -162,9 +162,9 @@ Proof.
* intros [|S T]; constructor; auto with sts.
assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts.
* intros [s T|S T]; constructor; auto with sts.
- + by rewrite (up_closed (up _ _)) by auto using closed_up with sts.
- + by rewrite (up_closed (up_set _ _))
- by eauto using closed_up_set, closed_ne with sts.
+ + rewrite (up_closed (up _ _)); auto using closed_up with sts.
+ + rewrite (up_closed (up_set _ _));
+ eauto using closed_up_set, closed_ne with sts.
* intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_ands.
+ destruct Hxz;inversion_clear Hy;constructor;unfold up_set;esolve_elem_of.
+ destruct Hxz; inversion_clear Hy; simpl;
@@ -185,7 +185,7 @@ Proof.
end; auto with sts.
* intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
inversion Hy; clear Hy; constructor; setoid_subst;
- rewrite ?disjoint_union_difference by done; auto.
+ rewrite ?disjoint_union_difference; auto.
split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
apply intersection_greatest; [auto with sts|].
intros s2; rewrite elem_of_intersection.