diff --git a/algebra/agree.v b/algebra/agree.v
index 4c786de7929b469753e3bbaec80782e0950e1b31..b21e24653192934e8b7793ca834c895bb7fd1d62 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -33,17 +33,17 @@ Qed.
Definition agree_cofe_mixin : CofeMixin (agree A).
Proof.
split.
- * intros x y; split.
+ - intros x y; split.
+ by intros Hxy n; split; intros; apply Hxy.
+ by intros Hxy; split; intros; apply Hxy with n.
- * split.
+ - split.
+ by split.
+ by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
+ intros x y z Hxy Hyz; split; intros n'; intros.
- - transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
- - transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
- * intros n x y Hxy; split; intros; apply Hxy; auto.
- * intros c n; apply and_wlog_r; intros;
+ * transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
+ * transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
+ - intros n x y Hxy; split; intros; apply Hxy; auto.
+ - intros c n; apply and_wlog_r; intros;
symmetry; apply (chain_cauchy c); naive_solver.
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
@@ -74,8 +74,8 @@ Proof.
intros n x y1 y2 [Hy' Hy]; split; [|done].
split; intros (?&?&Hxy); repeat (intro || split);
try apply Hy'; eauto using agree_valid_le.
- * etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le.
- * etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
+ - etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le.
+ - etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
eauto using agree_valid_le.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
@@ -95,13 +95,13 @@ Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
- * by intros n x1 x2 Hx y1 y2 Hy.
- * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
+ - by intros n x1 x2 Hx y1 y2 Hy.
+ - intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite (Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
- * intros x; apply agree_idemp.
- * by intros x y n [(?&?&?) ?].
- * by intros x y n; rewrite agree_includedN.
+ - intros x; apply agree_idemp.
+ - by intros x y n [(?&?&?) ?].
+ - by intros x y n; rewrite agree_includedN.
Qed.
Lemma agree_op_inv (x1 x2 : agree A) n : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
Proof. intros Hxy; apply Hxy. Qed.
@@ -113,8 +113,8 @@ Qed.
Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Proof.
intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
- * by rewrite agree_idemp.
- * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
+ - by rewrite agree_idemp.
+ - by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
Canonical Structure agreeRA : cmraT :=
CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
diff --git a/algebra/auth.v b/algebra/auth.v
index 9266175dc6a21187657648bf0122003f476b81a6..87c32e81da0a8152b1db3721cee2eacbba8ff4c5 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -39,14 +39,14 @@ Instance auth_compl : Compl (auth A) := λ c,
Definition auth_cofe_mixin : CofeMixin (auth A).
Proof.
split.
- * intros x y; unfold dist, auth_dist, equiv, auth_equiv.
+ - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
rewrite !equiv_dist; naive_solver.
- * intros n; split.
+ - intros n; split.
+ by intros ?; split.
+ by intros ?? [??]; split; symmetry.
+ intros ??? [??] [??]; split; etransitivity; eauto.
- * by intros ? [??] [??] [??]; split; apply dist_S.
- * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
+ - by intros ? [??] [??] [??]; split; apply dist_S.
+ - intros c n; split. apply (conv_compl (chain_map authoritative c) n).
apply (conv_compl (chain_map own c) n).
Qed.
Canonical Structure authC := CofeT auth_cofe_mixin.
@@ -99,24 +99,24 @@ Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
Definition auth_cmra_mixin : CMRAMixin (auth A).
Proof.
split.
- * 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 *;
+ - 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; intros ?; cofe_subst; auto.
- * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
+ - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
- * intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
- * by split; simpl; rewrite assoc.
- * by split; simpl; rewrite comm.
- * by split; simpl; rewrite ?cmra_unit_l.
- * by split; simpl; rewrite ?cmra_unit_idemp.
- * intros n ??; rewrite! auth_includedN; intros [??].
+ - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
+ - by split; simpl; rewrite assoc.
+ - by split; simpl; rewrite comm.
+ - by split; simpl; rewrite ?cmra_unit_l.
+ - by split; simpl; rewrite ?cmra_unit_idemp.
+ - intros n ??; rewrite! auth_includedN; intros [??].
by split; simpl; apply cmra_unit_preservingN.
- * assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
+ - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[a1| |] b1] [[a2| |] b2];
naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
- * by intros n ??; rewrite auth_includedN;
+ - by intros n ??; rewrite auth_includedN;
intros [??]; split; simpl; apply cmra_op_minus.
Qed.
Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A).
@@ -150,9 +150,9 @@ Context `{Empty A, !CMRAIdentity A}.
Global Instance auth_cmra_identity : CMRAIdentity authRA.
Proof.
split; simpl.
- * by apply (@cmra_empty_valid A _).
- * by intros x; constructor; rewrite /= left_id.
- * apply _.
+ - by apply (@cmra_empty_valid A _).
+ - by intros x; constructor; rewrite /= left_id.
+ - apply _.
Qed.
Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
@@ -221,9 +221,9 @@ Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) :
CMRAMonotone f → CMRAMonotone (auth_map f).
Proof.
split.
- * by intros n [x a] [y b]; rewrite !auth_includedN /=;
+ - by intros n [x a] [y b]; rewrite !auth_includedN /=;
intros [??]; split; simpl; apply: includedN_preserving.
- * intros n [[a| |] b]; rewrite /= /cmra_validN;
+ - intros n [[a| |] b]; rewrite /= /cmra_validN;
naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
diff --git a/algebra/cmra.v b/algebra/cmra.v
index f8eff5169163522d4e620d6794f59ecdee2a3f51..a441ce98a6322a7ac2fe038c14d804c7bb8a5c50 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -243,8 +243,8 @@ Qed.
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
split.
- * by intros x; exists (unit x); rewrite cmra_unit_r.
- * intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
+ - by intros x; exists (unit x); rewrite cmra_unit_r.
+ - intros x y z [z1 Hy] [z2 Hz]; exists (z1 â‹… z2).
by rewrite assoc -Hy -Hz.
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
@@ -349,8 +349,8 @@ Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
Proof.
split.
- * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
- * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
+ - by intros Hx z ?; exists y; split; [done|apply (Hx z)].
+ - by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
Qed.
Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
Proof. by intros ? z n ?; exists x. Qed.
@@ -402,8 +402,8 @@ Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f).
Proof.
split.
- * move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
- * move=> n x Hx /=. by apply validN_preserving, validN_preserving.
+ - move=> n x y Hxy /=. by apply includedN_preserving, includedN_preserving.
+ - move=> n x Hx /=. by apply validN_preserving, validN_preserving.
Qed.
Section cmra_monotone.
@@ -527,20 +527,20 @@ Section prod.
Definition prod_cmra_mixin : CMRAMixin (A * B).
Proof.
split; try apply _.
- * by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
- * by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
- * by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
- * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
+ - by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
+ - by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
+ - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
+ - by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
- * by intros n x [??]; split; apply cmra_validN_S.
- * by split; rewrite /= assoc.
- * by split; rewrite /= comm.
- * by split; rewrite /= cmra_unit_l.
- * by split; rewrite /= cmra_unit_idemp.
- * intros n x y; rewrite !prod_includedN.
+ - by intros n x [??]; split; apply cmra_validN_S.
+ - by split; rewrite /= assoc.
+ - by split; rewrite /= comm.
+ - by split; rewrite /= cmra_unit_l.
+ - by split; rewrite /= cmra_unit_idemp.
+ - intros n x y; rewrite !prod_includedN.
by intros [??]; split; apply cmra_unit_preservingN.
- * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
- * intros x y n; rewrite prod_includedN; intros [??].
+ - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
+ - intros x y n; rewrite prod_includedN; intros [??].
by split; apply cmra_op_minus.
Qed.
Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
@@ -556,9 +556,9 @@ Section prod.
CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodRA.
Proof.
split.
- * split; apply cmra_empty_valid.
- * by split; rewrite /=left_id.
- * by intros ? [??]; split; apply (timeless _).
+ - split; apply cmra_empty_valid.
+ - by split; rewrite /=left_id.
+ - by intros ? [??]; split; apply (timeless _).
Qed.
Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
@@ -579,7 +579,7 @@ Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B'
CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g).
Proof.
split.
- * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
+ - intros n x y; rewrite !prod_includedN; intros [??]; simpl.
by split; apply includedN_preserving.
- * by intros n x [??]; split; simpl; apply validN_preserving.
+ - by intros n x [??]; split; simpl; apply validN_preserving.
Qed.
diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 4740440b3b0fb43fe10e6ed7be0cbd618d5652dc..ac9315a5923bb439c0365eaa16faf223a8f7397e 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -21,9 +21,9 @@ Proof. done. Qed.
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 !assoc (comm _ x).
- * by transitivity (big_op xs2).
+ - by rewrite IH.
+ - by rewrite !assoc (comm _ 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.
@@ -35,10 +35,10 @@ Qed.
Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
Proof.
induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
- * by apply cmra_preserving_l.
- * by rewrite !assoc (comm _ y).
- * by transitivity (big_op ys); last apply cmra_included_r.
- * by transitivity (big_op ys).
+ - by apply cmra_preserving_l.
+ - by rewrite !assoc (comm _ y).
+ - by transitivity (big_op ys); last apply cmra_included_r.
+ - by transitivity (big_op ys).
Qed.
Lemma big_op_delete xs i x :
xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 0e6e81a735113d90209b4680fa94b82d101c0c5b..d901ef0465b571113583f5ce56df9013008cbd02 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -97,15 +97,15 @@ Section cofe.
Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
Proof.
split.
- * by intros x; rewrite equiv_dist.
- * by intros x y; rewrite !equiv_dist.
- * by intros x y z; rewrite !equiv_dist; intros; transitivity y.
+ - by intros x; rewrite equiv_dist.
+ - by intros x y; rewrite !equiv_dist.
+ - by intros x y z; rewrite !equiv_dist; intros; transitivity y.
Qed.
Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Proof.
intros x1 x2 ? y1 y2 ?; split; intros.
- * by transitivity x1; [|transitivity y1].
- * by transitivity x2; [|transitivity y2].
+ - by transitivity x1; [|transitivity y1].
+ - by transitivity x2; [|transitivity y2].
Qed.
Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n).
Proof.
@@ -158,8 +158,8 @@ Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
- * apply (contractive_0 f).
- * apply (contractive_S f), IH; auto with omega.
+ - apply (contractive_0 f).
+ - apply (contractive_S f), IH; auto with omega.
Qed.
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
@@ -212,14 +212,14 @@ Section cofe_mor.
Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
Proof.
split.
- * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
+ - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
intros Hfg k; apply equiv_dist; intros n; apply Hfg.
- * intros n; split.
+ - intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x).
- * by intros n f g ? x; apply dist_S.
- * intros c n x; simpl.
+ - by intros n f g ? x; apply dist_S.
+ - intros c n x; simpl.
by rewrite (conv_compl (fun_chain c x) n) /=.
Qed.
Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
@@ -274,11 +274,11 @@ Section product.
Definition prod_cofe_mixin : CofeMixin (A * B).
Proof.
split.
- * intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
+ - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
rewrite !equiv_dist; naive_solver.
- * apply _.
- * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
- * intros c n; split. apply (conv_compl (chain_map fst c) n).
+ - apply _.
+ - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
+ - intros c n; split. apply (conv_compl (chain_map fst c) n).
apply (conv_compl (chain_map snd c) n).
Qed.
Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
@@ -308,10 +308,10 @@ Section discrete_cofe.
Definition discrete_cofe_mixin : CofeMixin A.
Proof.
split.
- * intros x y; split; [done|intros Hn; apply (Hn 0)].
- * done.
- * done.
- * intros c n. rewrite /compl /discrete_compl /=.
+ - intros x y; split; [done|intros Hn; apply (Hn 0)].
+ - done.
+ - done.
+ - intros c n. rewrite /compl /discrete_compl /=.
symmetry; apply (chain_cauchy c 0 (S n)); omega.
Qed.
Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
@@ -347,14 +347,14 @@ Section later.
Definition later_cofe_mixin : CofeMixin (later A).
Proof.
split.
- * intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
+ - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
- * intros [|n]; [by split|split]; unfold dist, later_dist.
+ - intros [|n]; [by split|split]; unfold dist, later_dist.
+ by intros [x].
+ by intros [x] [y].
+ by intros [x] [y] [z] ??; transitivity y.
- * intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
- * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
+ - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
+ - intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
Qed.
Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
Global Instance Next_contractive : Contractive (@Next A).
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 39034e21ff12fd96b9a073519e5403ec7c707bcf..fea15cf597530f3b2ef6818e2810da34d178a02f 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -43,8 +43,8 @@ Qed.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
Proof.
induction k as [|k IH]; simpl.
- * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. apply (contractive_0 map).
- * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. by apply (contractive_S map).
+ - rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. apply (contractive_0 map).
+ - rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. by apply (contractive_S map).
Qed.
Record tower := {
@@ -66,15 +66,15 @@ Qed.
Definition tower_cofe_mixin : CofeMixin tower.
Proof.
split.
- * intros X Y; split; [by intros HXY n k; apply equiv_dist|].
+ - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
intros HXY k; apply equiv_dist; intros n; apply HXY.
- * intros k; split.
+ - intros k; split.
+ by intros X n.
+ by intros X Y ? n.
+ by intros X Y Z ?? n; transitivity (Y n).
- * intros k X Y HXY n; apply dist_S.
+ - intros k X Y HXY n; apply dist_S.
by rewrite -(g_tower X) (HXY (S n)) g_tower.
- * intros c n k; 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_cofe_mixin.
@@ -136,12 +136,12 @@ Lemma g_embed_coerce {k i} (x : A k) :
g i (embed_coerce (S i) x) ≡ embed_coerce i x.
Proof.
unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
- * symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
- * exfalso; lia.
- * assert (i = k) by lia; subst.
+ - 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)))) /= gf.
by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
- * assert (H : 1 + ((i - k) + k) = S i) by lia.
+ - 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.
@@ -156,22 +156,22 @@ Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
Proof.
rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
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) /=.
+ - 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.
+ - 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) /=.
+ - exfalso; lia.
+ - assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
by erewrite coerce_proper by done.
Qed.
Lemma embed_tower k (X : T) : embed (S k) (X (S k)) ≡{k}≡ X.
Proof.
intros i; rewrite /= /embed_coerce.
destruct (le_lt_dec i (S k)) as [H|H]; simpl.
- * rewrite -(gg_tower i (S k - i) X).
+ - rewrite -(gg_tower i (S k - i) X).
apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
- * rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
+ - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
Qed.
Program Definition unfold_chain (X : T) : chain (F T T) :=
@@ -206,7 +206,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
Proof.
apply (Solution F T (CofeMor unfold) (CofeMor fold)).
- * move=> X /=.
+ - move=> X /=.
rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
transitivity (map (ff n, gg n) (X (S (n + k)))).
@@ -228,7 +228,7 @@ Proof.
assert (H: S n + k = n + S k) by lia.
rewrite (map_ff_gg _ _ _ H).
apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
- * intros X; rewrite equiv_dist=> n /=.
+ - intros X; rewrite equiv_dist=> n /=.
rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
rewrite g_S -!map_comp -{2}(map_id _ _ X).
apply (contractive_ne map); split => Y /=.
diff --git a/algebra/dra.v b/algebra/dra.v
index fc1682ff28c40f4059ac642cd74ec85fd312ebe0..db17398f7570ffcbc1851b0c6a4de7cb432a44da 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -57,9 +57,9 @@ Instance validity_equiv : Equiv T := λ x y,
Instance validity_equivalence : Equivalence ((≡) : relation T).
Proof.
split; unfold equiv, validity_equiv.
- * by intros [x px ?]; simpl.
- * intros [x px ?] [y py ?]; naive_solver.
- * intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
+ - by intros [x px ?]; simpl.
+ - intros [x px ?] [y py ?]; naive_solver.
+ - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
split; [|intros; transitivity y]; tauto.
Qed.
Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
@@ -69,8 +69,8 @@ Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
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.
@@ -103,31 +103,31 @@ Solve Obligations with naive_solver auto using dra_minus_valid.
Definition validity_ra : RA (discreteC T).
Proof.
split.
- * intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
+ - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
split; intros (?&?&?); split_ands';
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
- * by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
- * intros ?? [??]; naive_solver.
- * intros x1 x2 [? Hx] y1 y2 [? Hy];
+ - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
+ - intros ?? [??]; naive_solver.
+ - intros x1 x2 [? Hx] y1 y2 [? 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; tauto.
- * intros [x px ?] [y py ?] [z pz ?]; split; simpl;
+ - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
[intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
|by intros; rewrite assoc].
- * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
- * intros [x px ?]; split;
+ - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
+ - intros [x px ?]; split;
naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
- * intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
- * intros x y Hxy; exists (unit y ⩪ unit x).
+ - intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
+ - intros x y Hxy; exists (unit y ⩪ unit x).
destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
assert (py → unit x ≼ unit y)
by intuition eauto 10 using dra_unit_preserving.
constructor; [|symmetry]; simpl in *;
intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid.
- * by intros [x px ?] [y py ?] (?&?&?).
- * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
+ - by intros [x px ?] [y py ?] (?&?&?).
+ - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
Qed.
Definition validityRA : cmraT := discreteRA validity_ra.
diff --git a/algebra/excl.v b/algebra/excl.v
index 221d77a44e61e1da1a1eee41cf01d7c98ebf88fd..177a3c2d09d75cdf5d608d4433205a6814a4650e 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -50,15 +50,15 @@ Instance excl_compl : Compl (excl A) := λ c,
Definition excl_cofe_mixin : CofeMixin (excl A).
Proof.
split.
- * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
+ - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
by intros n; feed inversion (Hxy n).
- * intros n; split.
+ - intros n; split.
+ by intros [x| |]; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
- * by inversion_clear 1; constructor; apply dist_S.
- * intros c n; unfold compl, excl_compl.
+ - by inversion_clear 1; constructor; apply dist_S.
+ - intros c n; unfold compl, excl_compl.
destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
{ assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality').
assert (∃ y, c (S n) = Excl y) as [y Hy].
@@ -102,18 +102,18 @@ Instance excl_minus : Minus (excl A) := λ x y,
Definition excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split.
- * by intros n []; destruct 1; constructor.
- * constructor.
- * by destruct 1; intros ?.
- * by destruct 1; inversion_clear 1; constructor.
- * intros n [?| |]; simpl; auto with lia.
- * by intros [?| |] [?| |] [?| |]; constructor.
- * by intros [?| |] [?| |]; constructor.
- * by intros [?| |]; constructor.
- * constructor.
- * by intros n [?| |] [?| |]; exists ∅.
- * by intros n [?| |] [?| |].
- * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
+ - by intros n []; destruct 1; constructor.
+ - constructor.
+ - by destruct 1; intros ?.
+ - by destruct 1; inversion_clear 1; constructor.
+ - intros n [?| |]; simpl; auto with lia.
+ - by intros [?| |] [?| |] [?| |]; constructor.
+ - by intros [?| |] [?| |]; constructor.
+ - by intros [?| |]; constructor.
+ - constructor.
+ - by intros n [?| |] [?| |]; exists ∅.
+ - by intros n [?| |] [?| |].
+ - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Qed.
Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Proof.
@@ -189,9 +189,9 @@ Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
Proof.
split.
- * intros n x y [z Hy]; exists (excl_map f z); rewrite Hy.
+ - intros n x y [z Hy]; exists (excl_map f z); rewrite Hy.
by destruct x, z; constructor.
- * by intros n [a| |].
+ - by intros n [a| |].
Qed.
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f).
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index b3cfb69eb9396c68e9b6065591e7264cef66df52..33a7852042f364a6a73525468976fed77af0371c 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -16,15 +16,15 @@ Instance map_compl : Compl (gmap K A) := λ c,
Definition map_cofe_mixin : CofeMixin (gmap K A).
Proof.
split.
- * intros m1 m2; split.
+ - intros m1 m2; split.
+ by intros Hm n k; apply equiv_dist.
+ intros Hm k; apply equiv_dist; intros n; apply Hm.
- * intros n; split.
+ - intros n; split.
+ by intros m k.
+ by intros m1 m2 ? k.
+ by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
- * by intros n m1 m2 ? k; apply dist_S.
- * intros c n k; rewrite /compl /map_compl lookup_imap.
+ - by intros n m1 m2 ? k; apply dist_S.
+ - intros c n k; rewrite /compl /map_compl lookup_imap.
feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
@@ -111,36 +111,36 @@ Proof. split; intros Hm ??; apply Hm. Qed.
Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
Proof.
split.
- * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
- * intros Hm; exists (m2 ⩪ m1); intros i.
+ - 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'.
Qed.
Lemma map_includedN_spec (m1 m2 : gmap K A) n :
m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
Proof.
split.
- * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
- * intros Hm; exists (m2 ⩪ m1); intros i.
+ - 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.
Qed.
Definition map_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
- * 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).
- * intros n m Hm i; apply cmra_validN_S, Hm.
- * by intros m1 m2 m3 i; rewrite !lookup_op assoc.
- * by intros m1 m2 i; rewrite !lookup_op comm.
- * by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
- * by intros m i; rewrite !lookup_unit cmra_unit_idemp.
- * intros n x y; rewrite !map_includedN_spec; intros Hm 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).
+ - intros n m Hm i; apply cmra_validN_S, Hm.
+ - by intros m1 m2 m3 i; rewrite !lookup_op assoc.
+ - by intros m1 m2 i; rewrite !lookup_op comm.
+ - by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
+ - by intros m i; rewrite !lookup_unit cmra_unit_idemp.
+ - intros n x y; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_unit; apply cmra_unit_preservingN.
- * intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
+ - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- * intros x y n; rewrite map_includedN_spec=> ? i.
+ - intros x y n; rewrite map_includedN_spec=> ? i.
by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
@@ -152,12 +152,12 @@ Proof.
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; intros i; rewrite /= ?lookup_op !lookup_imap.
- * destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
+ - destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
rewrite -Hx; apply (proj2_sig (f i)).
- * destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
+ - destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
by symmetry; apply option_op_positive_dist_l with (m2 !! i).
- * destruct (m !! i) as [x|] eqn:Hx; simpl; [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 symmetry; apply option_op_positive_dist_r with (m1 !! i).
Qed.
@@ -166,9 +166,9 @@ Canonical Structure mapRA : cmraT :=
Global Instance map_cmra_identity : CMRAIdentity mapRA.
Proof.
split.
- * by intros ? n; rewrite lookup_empty.
- * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- * apply map_empty_timeless.
+ - by intros ? n; rewrite lookup_empty.
+ - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
+ - apply map_empty_timeless.
Qed.
Global Instance mapRA_leibniz : LeibnizEquiv A → LeibnizEquiv mapRA.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
@@ -230,10 +230,10 @@ Lemma singleton_includedN n m i x :
(* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
Proof.
split.
- * move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
+ - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
destruct (m' !! i) as [y|];
[exists (x â‹… y)|exists x]; eauto using cmra_included_l.
- * intros (y&Hi&?); rewrite map_includedN_spec=>j.
+ - intros (y&Hi&?); rewrite map_includedN_spec=>j.
destruct (decide (i = j)); simplify_map_equality.
+ by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
+ apply None_includedN.
@@ -343,9 +343,9 @@ Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
`{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
Proof.
split.
- * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
+ - intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
by rewrite !lookup_fmap; apply: includedN_preserving.
- * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
+ - by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
Qed.
Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
CofeMor (fmap f : mapC K A → mapC K B).
diff --git a/algebra/iprod.v b/algebra/iprod.v
index f6581e250370bd581e3a61c0fb262bcf45e47f1a..3d9fd3d854239b75edc7699ba1fe97e042d142c1 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -30,14 +30,14 @@ Section iprod_cofe.
Definition iprod_cofe_mixin : CofeMixin (iprod B).
Proof.
split.
- * intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
+ - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
intros Hfg k; apply equiv_dist; intros n; apply Hfg.
- * intros n; split.
+ - intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x).
- * intros n f g Hfg x; apply dist_S, Hfg.
- * intros c n x.
+ - intros n f g Hfg x; apply dist_S, Hfg.
+ - intros c n x.
rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n).
apply (chain_cauchy c); lia.
Qed.
@@ -85,9 +85,9 @@ Section iprod_cofe.
Timeless f → Timeless y → Timeless (iprod_insert x y f).
Proof.
intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
- * rewrite iprod_lookup_insert.
+ - rewrite iprod_lookup_insert.
apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert.
- * rewrite iprod_lookup_insert_ne //.
+ - rewrite iprod_lookup_insert_ne //.
apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert_ne.
Qed.
@@ -128,27 +128,27 @@ Section iprod_cmra.
Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x.
Proof.
split.
- * by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
- * intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
+ - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
+ - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
Qed.
Definition iprod_cmra_mixin : CMRAMixin (iprod B).
Proof.
split.
- * by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
- * by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
- * by intros n f1 f2 Hf ? x; rewrite -(Hf x).
- * by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
- * intros n f Hf x; apply cmra_validN_S, Hf.
- * by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
- * by intros f1 f2 x; rewrite iprod_lookup_op comm.
- * by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
- * by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
- * intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x.
+ - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
+ - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
+ - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
+ - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
+ - intros n f Hf x; apply cmra_validN_S, Hf.
+ - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
+ - by intros f1 f2 x; rewrite iprod_lookup_op comm.
+ - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
+ - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
+ - intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x.
by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf.
- * intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- * intros n f1 f2; rewrite iprod_includedN_spec=> Hf x.
+ - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
+ - intros n f1 f2; rewrite iprod_includedN_spec=> Hf x.
by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
Qed.
Definition iprod_cmra_extend_mixin : CMRAExtendMixin (iprod B).
@@ -164,9 +164,9 @@ Section iprod_cmra.
(∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA.
Proof.
intros ?; split.
- * intros n x; apply cmra_empty_valid.
- * by intros f x; rewrite iprod_lookup_op left_id.
- * by apply _.
+ - intros n x; apply cmra_empty_valid.
+ - by intros f x; rewrite iprod_lookup_op left_id.
+ - by apply _.
Qed.
(** Internalized properties *)
@@ -223,8 +223,8 @@ Section iprod_cmra.
iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
Proof.
intros x'; destruct (decide (x' = x)) as [->|].
- * by rewrite iprod_lookup_op !iprod_lookup_singleton.
- * by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
+ - by rewrite iprod_lookup_op !iprod_lookup_singleton.
+ - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
Qed.
Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 :
@@ -245,8 +245,8 @@ Section iprod_cmra.
intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?); first apply Hg.
exists (iprod_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|].
- * by rewrite iprod_lookup_op iprod_lookup_singleton.
- * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
+ - by rewrite iprod_lookup_op iprod_lookup_singleton.
+ - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
Qed.
Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
@@ -277,9 +277,9 @@ Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B
(∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
Proof.
split.
- * intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x.
+ - intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x.
rewrite /iprod_map; apply includedN_preserving, Hf.
- * intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
+ - intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
Qed.
Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
diff --git a/algebra/option.v b/algebra/option.v
index 94eeac7aabf81d9a3a15e8cf21bbfbd9841b48fc..f9959c42db79c94f6204fe617edcf08d213808cd 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -23,15 +23,15 @@ Instance option_compl : Compl (option A) := λ c,
Definition option_cofe_mixin : CofeMixin (option A).
Proof.
split.
- * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
+ - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
by intros n; feed inversion (Hxy n).
- * intros n; split.
+ - intros n; split.
+ by intros [x|]; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
- * by inversion_clear 1; constructor; apply dist_S.
- * intros c n; unfold compl, option_compl.
+ - by inversion_clear 1; constructor; apply dist_S.
+ - intros c n; unfold compl, option_compl.
destruct (Some_dec (c 1)) as [[x Hx]|].
{ assert (is_Some (c (S n))) as [y Hy].
{ feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
@@ -72,12 +72,12 @@ Lemma option_includedN n (mx my : option A) :
mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
Proof.
split.
- * intros [mz Hmz].
+ - intros [mz Hmz].
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
cofe_subst; eauto using cmra_includedN_l.
- * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
+ - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
Lemma None_includedN n (mx : option A) : None ≼{n} mx.
@@ -89,20 +89,20 @@ Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
Definition option_cmra_mixin : CMRAMixin (option A).
Proof.
split.
- * by intros n [x|]; destruct 1; constructor; cofe_subst.
- * by destruct 1; constructor; cofe_subst.
- * by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
- * by destruct 1; inversion_clear 1; constructor; cofe_subst.
- * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- * intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
- * intros [x|] [y|]; constructor; rewrite 1?comm; auto.
- * by intros [x|]; constructor; rewrite cmra_unit_l.
- * by intros [x|]; constructor; rewrite cmra_unit_idemp.
- * intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
+ - by intros n [x|]; destruct 1; constructor; cofe_subst.
+ - by destruct 1; constructor; cofe_subst.
+ - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
+ - by destruct 1; inversion_clear 1; constructor; cofe_subst.
+ - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
+ - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
+ - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
+ - by intros [x|]; constructor; rewrite cmra_unit_l.
+ - by intros [x|]; constructor; rewrite cmra_unit_idemp.
+ - intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
- * intros n [x|] [y|]; rewrite /validN /option_validN /=;
+ - intros n [x|] [y|]; rewrite /validN /option_validN /=;
eauto using cmra_validN_op_l.
- * intros n mx my; rewrite option_includedN.
+ - intros n mx my; rewrite option_includedN.
intros [->|(x&y&->&->&?)]; [by destruct my|].
by constructor; apply cmra_op_minus.
Qed.
@@ -111,12 +111,12 @@ Proof.
intros n mx my1 my2.
destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
try (by exfalso; inversion Hx'; auto).
- * destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
+ - destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
{ by inversion_clear Hx'. }
by exists (Some z1, Some z2); repeat constructor.
- * by exists (Some x,None); inversion Hx'; repeat constructor.
- * by exists (None,Some x); inversion Hx'; repeat constructor.
- * exists (None,None); repeat constructor.
+ - by exists (Some x,None); inversion Hx'; repeat constructor.
+ - by exists (None,Some x); inversion Hx'; repeat constructor.
+ - exists (None,None); repeat constructor.
Qed.
Canonical Structure optionRA :=
CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
@@ -175,9 +175,9 @@ Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f}
CMRAMonotone (fmap f : option A → option B).
Proof.
split.
- * intros n mx my; rewrite !option_includedN.
+ - intros n mx my; rewrite !option_includedN.
intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving.
- * by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
+ - by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
Qed.
Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
CofeMor (fmap f : optionC A → optionC B).
diff --git a/algebra/sts.v b/algebra/sts.v
index 4157739aae4cd981e43cbb73991ff855472afc67..160f13675cca1c6430122611bd9367cd21360b3e 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -90,16 +90,16 @@ Lemma closed_op T1 T2 S1 S2 :
Proof.
intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
- * apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
- * apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
+ - apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
+ - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅.
Proof.
inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
- * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
- * solve_elem_of -Hstep Hs1 Hs2.
+ - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
+ - solve_elem_of -Hstep Hs1 Hs2.
Qed.
(** ** Properties of the closure operators *)
@@ -113,12 +113,12 @@ Lemma closed_up_set S T :
(∀ s, s ∈ S → tok s ∩ T ⊆ ∅) → S ≢ ∅ → closed (up_set S T) T.
Proof.
intros HS Hne; unfold up_set; split.
- * assert (∀ s, s ∈ up s T) by eauto using elem_of_up. solve_elem_of.
- * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
+ - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. solve_elem_of.
+ - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
specialize (HS s' Hs'); clear Hs' Hne S.
induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
inversion_clear Hstep; apply IH; clear IH; auto with sts.
- * intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
+ - intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
split; [eapply rtc_r|]; eauto.
Qed.
Lemma closed_up_set_empty S : S ≢ ∅ → closed (up_set S ∅) ∅.
@@ -201,42 +201,42 @@ Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts.
Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
Proof.
split.
- * by intros []; constructor.
- * by destruct 1; constructor.
- * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+ - by intros []; constructor.
+ - by destruct 1; constructor.
+ - destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
Qed.
Global Instance sts_dra : DRA (car sts).
Proof.
split.
- * apply _.
- * by do 2 destruct 1; constructor; setoid_subst.
- * by destruct 1; constructor; setoid_subst.
- * by destruct 1; simpl; intros ?; setoid_subst.
- * by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
- * by do 2 destruct 1; constructor; setoid_subst.
- * assert (∀ T T' S s,
+ - apply _.
+ - by do 2 destruct 1; constructor; setoid_subst.
+ - by destruct 1; constructor; setoid_subst.
+ - by destruct 1; simpl; intros ?; setoid_subst.
+ - by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
+ - by do 2 destruct 1; constructor; setoid_subst.
+ - assert (∀ T T' S s,
closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
{ intros S T T' s [??]; solve_elem_of. }
destruct 3; simpl in *; auto using closed_op with sts.
- * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
- * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
+ - intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
+ - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
rewrite ?disjoint_union_difference; auto using closed_up with sts.
eapply closed_up_set; eauto 2 using closed_disjoint with sts.
- * intros [] [] []; constructor; rewrite ?assoc; auto with sts.
- * destruct 4; inversion_clear 1; constructor; auto with sts.
- * destruct 4; inversion_clear 1; constructor; auto with sts.
- * destruct 1; constructor; auto with sts.
- * destruct 3; constructor; auto with sts.
- * intros [|S T]; constructor; auto using elem_of_up with sts.
+ - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
+ - destruct 4; inversion_clear 1; constructor; auto with sts.
+ - destruct 4; inversion_clear 1; constructor; auto with sts.
+ - destruct 1; constructor; auto with sts.
+ - destruct 3; constructor; auto with sts.
+ - intros [|S T]; constructor; auto using elem_of_up with sts.
assert (S ⊆ up_set S ∅ ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne.
solve_elem_of.
- * intros [|S T]; constructor; auto with sts.
+ - 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.
+ - intros [s T|S T]; constructor; auto 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.
+ - intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_ands.
+ destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
+ destruct Hxz; inversion_clear Hy; simpl;
auto using closed_up_set_empty, closed_up_empty with sts.
@@ -247,14 +247,14 @@ Proof.
| |- context [ up ?s ?T ] =>
unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
end; auto with sts.
- * intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
+ - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
repeat match goal with
| |- context [ up_set ?S ?T ] =>
unless (S ⊆ up_set S T) by done; pose proof (subseteq_up_set S T)
| |- context [ up ?s ?T ] =>
unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
end; auto with sts.
- * intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
+ - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
inversion Hy; clear Hy; constructor; setoid_subst;
rewrite ?disjoint_union_difference; auto.
split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
diff --git a/algebra/upred.v b/algebra/upred.v
index 08b7a4f9066cbd5a008de2467481a93be79f88fe..fe1f10c1f14f87f44ed46b81bc171a05618cae95 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -35,14 +35,14 @@ Section cofe.
Definition uPred_cofe_mixin : CofeMixin (uPred M).
Proof.
split.
- * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
+ - intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
intros HPQ x n ?; apply HPQ with n; auto.
- * intros n; split.
+ - intros n; split.
+ by intros P x i.
+ by intros P Q HPQ x i ??; symmetry; apply HPQ.
+ by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
- * intros n P Q HPQ x i ??; apply HPQ; auto.
- * intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
+ - intros n P Q HPQ x i ??; apply HPQ; auto.
+ - intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
Qed.
Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
@@ -146,8 +146,8 @@ Next Obligation.
{ destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using cmra_included_l.
apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
- * apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l.
- * apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r.
+ - apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l.
+ - apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r.
Qed.
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
@@ -245,8 +245,8 @@ Global Instance entails_proper :
Proper ((≡) ==> (≡) ==> iff) ((⊑) : relation (uPred M)).
Proof.
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].
+ - by transitivity P1; [|transitivity Q1].
+ - by transitivity P2; [|transitivity Q2].
Qed.
(** Non-expansiveness and setoid morphisms *)
@@ -292,8 +292,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); auto.
- * by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); 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 _.
@@ -512,8 +512,8 @@ Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
Global Instance True_impl : LeftId (≡) True%I (@uPred_impl M).
Proof.
intros P; apply (anti_symm (⊑)).
- * by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
- * by apply impl_intro_l; rewrite left_id.
+ - by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
+ - by apply impl_intro_l; rewrite left_id.
Qed.
Lemma iff_refl Q P : Q ⊑ (P ↔ P).
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
@@ -555,8 +555,8 @@ Qed.
Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
intros P x n Hvalid; split.
- * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
- * by intros ?; exists (unit x), x; rewrite cmra_unit_l.
+ - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
+ - by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Qed.
Global Instance sep_comm : Comm (≡) (@uPred_sep M).
Proof.
@@ -566,10 +566,10 @@ Qed.
Global Instance sep_assoc : Assoc (≡) (@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.
+ - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_ands; auto.
+ by rewrite -(assoc op) -Hy -Hx.
+ by exists x1, y1.
- * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_ands; auto.
+ - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 â‹… x2); split_ands; auto.
+ by rewrite (assoc op) -Hy -Hx.
+ by exists y2, x2.
Qed.
@@ -693,12 +693,12 @@ Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
intros x n ?; split.
- * destruct n as [|n]; simpl.
+ - destruct n as [|n]; simpl.
{ by exists x, (unit x); rewrite cmra_unit_r. }
intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2)
as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
- * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
+ - destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S.
Qed.
@@ -802,9 +802,9 @@ Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
Proof.
intros x n ?; split.
- * intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
+ - intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
- * intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
+ - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
@@ -863,9 +863,9 @@ Proof. done. Qed.
Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.
Proof.
split.
- * intros HP x n ??; induction n as [|n]; auto.
+ - intros HP x n ??; induction n as [|n]; auto.
by destruct (HP x (S n)); auto using cmra_validN_S.
- * move=> HP x [|n] /=; auto; left.
+ - move=> HP x [|n] /=; auto; left.
apply HP, uPred_weaken with x n; eauto using cmra_validN_le.
Qed.
Global Instance const_timeless φ : TimelessP (■φ : uPred M)%I.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 05310f67e8cd5fa2e3acb11265ea65713de4c920..6ca56c2a742f00bd12483985592ea32120321681 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -44,16 +44,16 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance 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 !assoc (comm _ P).
- * etransitivity; eauto.
+ - by rewrite IH.
+ - by rewrite !assoc (comm _ P).
+ - etransitivity; eauto.
Qed.
Global Instance 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 !assoc (comm _ P).
- * etransitivity; eauto.
+ - by rewrite IH.
+ - by rewrite !assoc (comm _ P).
+ - etransitivity; eauto.
Qed.
Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index aae49ccac4700975bf5c51e06da653a8ba814fb1..bfe64007175f966f8856add403f9120ae37dd085 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -142,7 +142,7 @@ Section proof.
apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
(* I think some evars here are better than repeating *everything* *)
eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
- { solve_elem_of+. (* FIXME eauto should do this *) }
+ { solve_elem_of+. (* FIXME eauto should do this *) }
rewrite [(_ ★ sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
apply const_elim_sep_l=>Hs. destruct p; last done.
diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index 276c0e200b3d7bae3a3b51155bd8283e39bb3925..09bbbb8fccbc1b96f12cb78acb657772184eee8c 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -346,10 +346,10 @@ Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
Proof.
split.
- * eauto using heap_lang.fill_not_val.
- * intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
+ - eauto using heap_lang.fill_not_val.
+ - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
- * intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+ - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (heap_lang.step_by_val
K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
rewrite heap_lang.fill_app in Heq1; apply (inj _) in Heq1.
diff --git a/prelude/bsets.v b/prelude/bsets.v
index 56ae4148268da1398c8e3452a8e5e64c0183a8c5..40216c1a3043e7371390de9f7a3ba203bdf9a75a 100644
--- a/prelude/bsets.v
+++ b/prelude/bsets.v
@@ -21,11 +21,11 @@ Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} :
Collection A (bset A).
Proof.
split; [split| |].
- * by intros x ?.
- * by intros x y; rewrite <-(bool_decide_spec (x = y)).
- * split. apply orb_prop_elim. apply orb_prop_intro.
- * split. apply andb_prop_elim. apply andb_prop_intro.
- * intros X Y x; unfold elem_of, bset_elem_of; simpl.
+ - by intros x ?.
+ - by intros x y; rewrite <-(bool_decide_spec (x = y)).
+ - split. apply orb_prop_elim. apply orb_prop_intro.
+ - split. apply andb_prop_elim. apply andb_prop_intro.
+ - intros X Y x; unfold elem_of, bset_elem_of; simpl.
destruct (bset_car X x), (bset_car Y x); simpl; tauto.
Qed.
Instance bset_elem_of_dec {A} x (X : bset A) : Decision (x ∈ X) := _.
diff --git a/prelude/co_pset.v b/prelude/co_pset.v
index 535f0e88bedf5f6a4628181c55f92a022689ca09..df7e39358ed0d2be4a428dc195986e93abb26e1b 100644
--- a/prelude/co_pset.v
+++ b/prelude/co_pset.v
@@ -65,10 +65,10 @@ Lemma coPset_eq t1 t2 :
Proof.
revert t2.
induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *.
- * f_equal; apply (Ht 1).
- * by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1).
- * by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2).
- * f_equal; [apply (Ht 1)| |].
+ - f_equal; apply (Ht 1).
+ - by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1).
+ - by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2).
+ - f_equal; [apply (Ht 1)| |].
+ apply IHl; try apply (λ x, Ht (x~0)); eauto.
+ apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.
@@ -163,13 +163,13 @@ Instance coPset_elem_of_dec (p : positive) (X : coPset) : Decision (p ∈ X) :=
Instance coPset_collection : Collection positive coPset.
Proof.
split; [split| |].
- * by intros ??.
- * intros p q. apply elem_to_Pset_singleton.
- * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
+ - by intros ??.
+ - intros p q. apply elem_to_Pset_singleton.
+ - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
by rewrite elem_to_Pset_union, orb_True.
- * intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
+ - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
by rewrite elem_to_Pset_intersection, andb_True.
- * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
+ - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
by rewrite elem_to_Pset_intersection,
elem_to_Pset_opp, andb_True, negb_True.
Qed.
@@ -192,7 +192,7 @@ Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X).
Proof.
destruct X as [t Ht].
unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
- * induction t as [b|b l IHl r IHr]; simpl.
+ - induction t as [b|b l IHl r IHr]; simpl.
{ destruct b; simpl; [intros [l Hl]|done].
by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. }
intros [ll Hll]; rewrite andb_True; split.
@@ -200,7 +200,7 @@ Proof.
rewrite elem_of_list_omap; intros; exists (i~0); auto.
+ apply IHr; exists (omap (maybe (~1)) ll); intros i.
rewrite elem_of_list_omap; intros; exists (i~1); auto.
- * induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
+ - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto.
exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
@@ -237,8 +237,8 @@ Qed.
Lemma coPpick_elem_of X : ¬set_finite X → coPpick X ∈ X.
Proof.
destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?.
- * by intros; apply coPpick_raw_elem_of.
- * by intros []; apply coPset_finite_spec, coPpick_raw_None.
+ - by intros; apply coPpick_raw_elem_of.
+ - by intros []; apply coPset_finite_spec, coPpick_raw_None.
Qed.
(** * Conversion to psets *)
@@ -270,8 +270,8 @@ Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw :=
Lemma of_Pset_wf t : Pmap_wf t → coPset_wf (of_Pset_raw t).
Proof.
induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
- * intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
- * destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
+ - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
+ - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
Qed.
Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t) ↔ t !! i = Some ().
@@ -327,9 +327,9 @@ Definition coPset_suffixes (p : positive) : coPset :=
Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
Proof.
unfold elem_of, coPset_elem_of; simpl; split.
- * revert p; induction q; intros [?|?|]; simpl;
+ - revert p; induction q; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; naive_solver.
- * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
+ - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
Qed.
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
Proof.
diff --git a/prelude/collections.v b/prelude/collections.v
index b45cd5f9db7974471288e13586a641a31e311c7e..11679fa0039bcc458ba94cba3cffc2c64c89d5b7 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -48,8 +48,8 @@ Section simple_collection.
Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
Proof.
split.
- * intros ??. rewrite elem_of_singleton. by intros ->.
- * intros Ex. by apply (Ex x), elem_of_singleton.
+ - intros ??. rewrite elem_of_singleton. by intros ->.
+ - intros Ex. by apply (Ex x), elem_of_singleton.
Qed.
Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)).
Proof. by repeat intro; subst. Qed.
@@ -59,9 +59,9 @@ Section simple_collection.
Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
Proof.
split.
- * induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
+ - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
- * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+ - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
intros. apply elem_of_union_r; auto.
Qed.
Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅.
@@ -113,9 +113,9 @@ Section of_option_list.
Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l.
Proof.
split.
- * induction l; simpl; [by rewrite elem_of_empty|].
+ - induction l; simpl; [by rewrite elem_of_empty|].
rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
- * induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
+ - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
Qed.
End of_option_list.
@@ -356,11 +356,11 @@ Section collection_ops.
Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
Proof.
split.
- * revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
+ - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
- * intros (xs & y & Hxs & ? & Hx). revert x Hx.
+ - intros (xs & y & Hxs & ? & Hx). revert x Hx.
induction Hxs; intros; simplify_option_equality; [done |].
rewrite elem_of_intersection_with. naive_solver.
Qed.
@@ -389,8 +389,8 @@ Section NoDup.
Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
Proof.
intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
- * rewrite <-E1, <-E2; intuition.
- * rewrite E1, E2; intuition.
+ - rewrite <-E1, <-E2; intuition.
+ - rewrite E1, E2; intuition.
Qed.
Global Instance: Proper ((≡) ==> iff) set_NoDup.
Proof. firstorder. Qed.
@@ -575,8 +575,8 @@ Section collection_monad.
l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
Proof.
split.
- * revert l. induction k; solve_elem_of.
- * induction 1; solve_elem_of.
+ - revert l. induction k; solve_elem_of.
+ - induction 1; solve_elem_of.
Qed.
Lemma collection_mapM_length {A B} (f : A → M B) l k :
l ∈ mapM f k → length l = length k.
diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index db14b64b830e60eb662ef97688d9fba805aefeea..0c213880856d8de264e488eaee98cb3c358e26d5 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -20,9 +20,9 @@ Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
Proof.
intros ?? E. apply NoDup_Permutation.
- * apply NoDup_elements.
- * apply NoDup_elements.
- * intros. by rewrite !elem_of_elements, E.
+ - apply NoDup_elements.
+ - apply NoDup_elements.
+ - intros. by rewrite !elem_of_elements, E.
Qed.
Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _).
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
@@ -45,9 +45,9 @@ Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof.
change (length (elements {[ x ]}) = length [x]).
apply Permutation_length, NoDup_Permutation.
- * apply NoDup_elements.
- * apply NoDup_singleton.
- * intros y.
+ - apply NoDup_elements.
+ - apply NoDup_singleton.
+ - intros y.
by rewrite elem_of_elements, elem_of_singleton, elem_of_list_singleton.
Qed.
Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
@@ -59,8 +59,8 @@ Qed.
Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
Proof.
destruct (elements X) as [|x l] eqn:HX; [right|left].
- * apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
- * exists x. rewrite <-elem_of_elements, HX. by left.
+ - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
+ - exists x. rewrite <-elem_of_elements, HX. by left.
Qed.
Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
@@ -75,17 +75,17 @@ Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
Proof.
intros E. destruct (size_pos_elem_of X); auto with lia.
exists x. apply elem_of_equiv. split.
- * rewrite elem_of_singleton. eauto using size_singleton_inv.
- * solve_elem_of.
+ - rewrite elem_of_singleton. eauto using size_singleton_inv.
+ - solve_elem_of.
Qed.
Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
Proof.
intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
- * apply NoDup_elements.
- * apply NoDup_app; repeat split; try apply NoDup_elements.
+ - apply NoDup_elements.
+ - apply NoDup_app; repeat split; try apply NoDup_elements.
intros x; rewrite !elem_of_elements; solve_elem_of.
- * intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
+ - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
Proof.
@@ -129,9 +129,9 @@ Proof.
intros ? Hemp Hadd. apply well_founded_induction with (⊂).
{ apply collection_wf. }
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
- * rewrite (union_difference {[ x ]} X) by solve_elem_of.
+ - rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH; solve_elem_of.
- * by rewrite HX.
+ - by rewrite HX.
Qed.
Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
Proper ((=) ==> (≡) ==> iff) P →
@@ -143,9 +143,9 @@ Proof.
{ intros help ?. apply help; [apply NoDup_elements|].
symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl.
- * intros X HX. setoid_rewrite elem_of_nil in HX.
+ - intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. solve_elem_of.
- * intros X HX. setoid_rewrite elem_of_cons in HX.
+ - intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH. solve_elem_of.
Qed.
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index bf5d5d49ea1e0bf80d89d0416cf1995340b8d967..5df84b2883e8098896000b727a2738f88011d7b0 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -121,9 +121,9 @@ Section setoid.
Global Instance map_equivalence : Equivalence ((≡) : relation (M A)).
Proof.
split.
- * by intros m i.
- * by intros m1 m2 ? i.
- * by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
+ - by intros m i.
+ - by intros m1 m2 ? i.
+ - by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
Qed.
Global Instance lookup_proper (i : K) :
Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
@@ -258,9 +258,9 @@ Proof.
{ by rewrite lookup_partial_alter_ne,
!lookup_partial_alter, lookup_partial_alter_ne. }
destruct (decide (jj = i)) as [->|?].
- * by rewrite lookup_partial_alter,
+ - by rewrite lookup_partial_alter,
!lookup_partial_alter_ne, lookup_partial_alter by congruence.
- * by rewrite !lookup_partial_alter_ne by congruence.
+ - by rewrite !lookup_partial_alter_ne by congruence.
Qed.
Lemma partial_alter_self_alt {A} (m : M A) i x :
x = m !! i → partial_alter (λ _, x) i m = m.
@@ -307,8 +307,8 @@ Lemma lookup_alter_Some {A} (f : A → A) m i j y :
(i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠j ∧ m !! j = Some y).
Proof.
destruct (decide (i = j)) as [->|?].
- * rewrite lookup_alter. naive_solver (simplify_option_equality; eauto).
- * rewrite lookup_alter_ne by done. naive_solver.
+ - rewrite lookup_alter. naive_solver (simplify_option_equality; eauto).
+ - rewrite lookup_alter_ne by done. naive_solver.
Qed.
Lemma lookup_alter_None {A} (f : A → A) m i j :
alter f i m !! j = None ↔ m !! j = None.
@@ -333,9 +333,9 @@ Lemma lookup_delete_Some {A} (m : M A) i j y :
delete i m !! j = Some y ↔ i ≠j ∧ m !! j = Some y.
Proof.
split.
- * destruct (decide (i = j)) as [->|?];
+ - destruct (decide (i = j)) as [->|?];
rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
- * intros [??]. by rewrite lookup_delete_ne.
+ - intros [??]. by rewrite lookup_delete_ne.
Qed.
Lemma lookup_delete_is_Some {A} (m : M A) i j :
is_Some (delete i m !! j) ↔ i ≠j ∧ is_Some (m !! j).
@@ -412,9 +412,9 @@ Lemma lookup_insert_Some {A} (m : M A) i j x y :
<[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠j ∧ m !! j = Some y).
Proof.
split.
- * destruct (decide (i = j)) as [->|?];
+ - destruct (decide (i = j)) as [->|?];
rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
- * intros [[-> ->]|[??]]; [apply lookup_insert|]. by rewrite lookup_insert_ne.
+ - intros [[-> ->]|[??]]; [apply lookup_insert|]. by rewrite lookup_insert_ne.
Qed.
Lemma lookup_insert_is_Some {A} (m : M A) i j x :
is_Some (<[i:=x]>m !! j) ↔ i = j ∨ i ≠j ∧ is_Some (m !! j).
@@ -435,8 +435,8 @@ Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
(∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
Proof.
intros ? j; destruct (decide (i = j)) as [->|].
- * rewrite lookup_insert. destruct (m !! j); simpl; eauto.
- * rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
+ - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
+ - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
Qed.
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]>m.
Proof. apply partial_alter_subseteq. Qed.
@@ -462,8 +462,8 @@ Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x :
Proof.
rewrite !map_subseteq_spec.
intros Hix Hi j y Hj. destruct (decide (i = j)) as [->|?].
- * rewrite lookup_insert. congruence.
- * rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
+ - rewrite lookup_insert. congruence.
+ - rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
Qed.
Lemma insert_delete_subset {A} (m1 m2 : M A) i x :
m1 !! i = None → <[i:=x]> m1 ⊂ m2 → m1 ⊂ delete i m2.
@@ -477,10 +477,10 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
Proof.
intros Hi Hm1m2. exists (delete i m2). split_ands.
- * rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
+ - rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
by rewrite lookup_insert.
- * eauto using insert_delete_subset.
- * by rewrite lookup_delete.
+ - eauto using insert_delete_subset.
+ - by rewrite lookup_delete.
Qed.
Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}.
Proof. done. Qed.
@@ -510,8 +510,8 @@ Qed.
Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i := x]} = {[i := f x]}.
Proof.
intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?].
- * by rewrite lookup_alter, !lookup_singleton.
- * by rewrite lookup_alter_ne, !lookup_singleton_ne.
+ - by rewrite lookup_alter, !lookup_singleton.
+ - by rewrite lookup_alter_ne, !lookup_singleton_ne.
Qed.
Lemma alter_singleton_ne {A} (f : A → A) i j x :
i ≠j → alter f i {[j := x]} = {[j := x]}.
@@ -528,15 +528,15 @@ Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma fmap_insert {A B} (f: A → B) m i x: f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
- * by rewrite lookup_fmap, !lookup_insert.
- * by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
+ - by rewrite lookup_fmap, !lookup_insert.
+ - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
Lemma omap_insert {A B} (f : A → option B) m i x y :
f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
Proof.
intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
- * by rewrite lookup_omap, !lookup_insert.
- * by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
+ - by rewrite lookup_omap, !lookup_insert.
+ - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
Qed.
Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
Proof.
@@ -585,8 +585,8 @@ Proof.
setoid_rewrite elem_of_cons.
intros [?|?] Hdup; simplify_equality; [by rewrite lookup_insert|].
destruct (decide (i = j)) as [->|].
- * rewrite lookup_insert; f_equal; eauto.
- * rewrite lookup_insert_ne by done; eauto.
+ - rewrite lookup_insert; f_equal; eauto.
+ - rewrite lookup_insert_ne by done; eauto.
Qed.
Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
NoDup (l.*1) → (i,x) ∈ l → map_of_list l !! i = Some x.
@@ -617,8 +617,8 @@ Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
Proof.
induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
- * by rewrite lookup_insert.
- * by rewrite lookup_insert_ne; intuition.
+ - by rewrite lookup_insert.
+ - by rewrite lookup_insert_ne; intuition.
Qed.
Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i :
i ∉ l.*1 ↔ map_of_list l !! i = None.
@@ -665,11 +665,11 @@ Lemma map_to_list_insert {A} (m : M A) i x :
m !! i = None → map_to_list (<[i:=x]>m) ≡ₚ (i,x) :: map_to_list m.
Proof.
intros. apply map_of_list_inj; csimpl.
- * apply NoDup_fst_map_to_list.
- * constructor; auto using NoDup_fst_map_to_list.
+ - apply NoDup_fst_map_to_list.
+ - constructor; auto using NoDup_fst_map_to_list.
rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
rewrite elem_of_map_to_list in Hlookup. congruence.
- * by rewrite !map_of_to_list.
+ - by rewrite !map_of_to_list.
Qed.
Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
Proof. done. Qed.
@@ -702,13 +702,13 @@ Lemma lookup_imap {A B} (f : K → A → option B) m i :
map_imap f m !! i = m !! i ≫= f i.
Proof.
unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl.
- * destruct (m !! i) as [x|] eqn:?; simplify_equality'.
+ - destruct (m !! i) as [x|] eqn:?; simplify_equality'.
apply elem_of_map_of_list_1_help.
{ apply elem_of_list_omap; exists (i,x); split;
[by apply elem_of_map_to_list|by simplify_option_equality]. }
intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?).
by rewrite elem_of_map_to_list in Hi'; simplify_option_equality.
- * apply not_elem_of_map_of_list; rewrite elem_of_list_fmap.
+ - apply not_elem_of_map_of_list; rewrite elem_of_list_fmap.
intros ([i' x]&->&Hi'); simplify_equality'.
rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
rewrite elem_of_map_to_list in Hj; simplify_option_equality.
@@ -726,8 +726,8 @@ Proof.
by intros (?&?&?&?&?); simplify_option_equality. }
unfold map_of_collection; rewrite <-elem_of_map_of_list by done.
rewrite elem_of_list_omap. setoid_rewrite elem_of_elements; split.
- * intros (?&?&?); simplify_option_equality; eauto.
- * intros [??]; exists i; simplify_option_equality; eauto.
+ - intros (?&?&?); simplify_option_equality; eauto.
+ - intros [??]; exists i; simplify_option_equality; eauto.
Qed.
(** ** Induction principles *)
@@ -741,8 +741,8 @@ Proof.
{ apply map_to_list_empty_inv_alt in Hml. by subst. }
inversion_clear Hnodup.
apply map_to_list_insert_inv in Hml; subst m. apply Hins.
- * by apply not_elem_of_map_of_list_1.
- * apply IH; auto using map_to_of_list.
+ - by apply not_elem_of_map_of_list_1.
+ - apply IH; auto using map_to_of_list.
Qed.
Lemma map_to_list_length {A} (m1 m2 : M A) :
m1 ⊂ m2 → length (map_to_list m1) < length (map_to_list m2).
@@ -759,8 +759,8 @@ Qed.
Lemma map_wf {A} : wf (strict (@subseteq (M A) _)).
Proof.
apply (wf_projected (<) (length ∘ map_to_list)).
- * by apply map_to_list_length.
- * by apply lt_wf.
+ - by apply map_to_list_length.
+ - by apply lt_wf.
Qed.
(** ** Properties of the [map_Forall] predicate *)
@@ -770,8 +770,8 @@ Context {A} (P : K → A → Prop).
Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m).
Proof.
rewrite Forall_forall. split.
- * intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
- * intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
+ - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
+ - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
Qed.
Lemma map_Forall_empty : map_Forall P ∅.
Proof. intros i x. by rewrite lookup_empty. Qed.
@@ -874,24 +874,24 @@ Lemma partial_alter_merge g g1 g2 m1 m2 i :
merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
Proof.
intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
- * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
- * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma partial_alter_merge_l g g1 m1 m2 i :
g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) →
partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
Proof.
intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
- * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
- * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma partial_alter_merge_r g g2 m1 m2 i :
g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) →
partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
Proof.
intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
- * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
- * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma insert_merge m1 m2 i x y z :
f (Some y) (Some z) = Some x →
@@ -928,10 +928,10 @@ Lemma map_relation_alt (m1 : M A) (m2 : M B) :
map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
Proof.
split.
- * intros Hm i P'; rewrite lookup_merge by done; intros.
+ - intros Hm i P'; rewrite lookup_merge by done; intros.
specialize (Hm i). destruct (m1 !! i), (m2 !! i);
simplify_equality'; auto using bool_decide_pack.
- * intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
+ - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
destruct (m1 !! i), (m2 !! i); simplify_equality'; auto;
by eapply bool_decide_unpack, Hm.
Qed.
@@ -950,10 +950,10 @@ Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
Proof.
split.
- * rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
+ - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
rewrite lookup_merge in Hm by done.
destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
- * unfold map_relation, option_relation.
+ - unfold map_relation, option_relation.
by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
specialize (Hm i); simplify_option_equality.
Qed.
@@ -1003,9 +1003,9 @@ Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ⊥ₘ m ↔ m !! i = None.
Proof.
split; [|rewrite !map_disjoint_spec].
- * intro. apply (map_disjoint_Some_l {[i := x]} _ _ x);
+ - intro. apply (map_disjoint_Some_l {[i := x]} _ _ x);
auto using lookup_singleton.
- * intros ? j y1 y2. destruct (decide (i = j)) as [->|].
+ - intros ? j y1 y2. destruct (decide (i = j)) as [->|].
+ rewrite lookup_singleton. intuition congruence.
+ by rewrite lookup_singleton_ne.
Qed.
@@ -1238,8 +1238,8 @@ Proof.
apply map_eq. intros j. apply option_eq. intros y.
rewrite lookup_union_Some_raw.
destruct (decide (i = j)); subst.
- * rewrite !lookup_singleton, lookup_insert. intuition congruence.
- * rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence.
+ - rewrite !lookup_singleton, lookup_insert. intuition congruence.
+ - rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence.
Qed.
Lemma insert_union_singleton_r {A} (m : M A) i x :
m !! i = None → <[i:=x]>m = m ∪ {[i := x]}.
@@ -1290,8 +1290,8 @@ Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
⋃ ms ⊥ₘ m ↔ Forall (.⊥ₘ m) ms.
Proof.
split.
- * induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
- * induction 1; simpl; [apply map_disjoint_empty_l |].
+ - induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
+ - induction 1; simpl; [apply map_disjoint_empty_l |].
by rewrite map_disjoint_union_l.
Qed.
Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) :
@@ -1342,8 +1342,8 @@ Lemma map_disjoint_of_list_l {A} (m : M A) ixs :
map_of_list ixs ⊥ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
Proof.
split.
- * induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
- * induction 1; simpl; [apply map_disjoint_empty_l|].
+ - induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
+ - induction 1; simpl; [apply map_disjoint_empty_l|].
rewrite map_disjoint_insert_l. auto.
Qed.
Lemma map_disjoint_of_list_r {A} (m : M A) ixs :
diff --git a/prelude/finite.v b/prelude/finite.v
index 98a5602cd74596153fe40d7051f8fb334437875c..d9aba281389179eed16458a6a89868cd3de7838f 100644
--- a/prelude/finite.v
+++ b/prelude/finite.v
@@ -30,8 +30,8 @@ Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
- * destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
- * destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
+ - destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
+ - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed.
Lemma encode_decode A `{finA: Finite A} i :
i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i.
@@ -80,8 +80,8 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
`{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
Proof.
intros. apply contains_Permutation_length_eq.
- * by rewrite fmap_length.
- * by apply finite_inj_contains.
+ - by rewrite fmap_length.
+ - by apply finite_inj_contains.
Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
`{!Inj (=) (=) f} : card A = card B → Surj (=) f.
@@ -103,20 +103,20 @@ Lemma finite_inj A `{Finite A} B `{Finite B} :
card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f.
Proof.
split.
- * intros. destruct (decide (card A = 0)) as [HA|?].
+ - intros. destruct (decide (card A = 0)) as [HA|?].
{ exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
- * intros [f ?]. unfold card. rewrite <-(fmap_length f).
+ - intros [f ?]. unfold card. rewrite <-(fmap_length f).
by apply contains_length, (finite_inj_contains f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f.
Proof.
split.
- * intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
+ - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
exists f; auto using (finite_inj_surj f).
- * intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ by exists f.
+ destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
Qed.
@@ -193,8 +193,8 @@ Program Instance option_finite `{Finite A} : Finite (option A) :=
{| enum := None :: Some <$> enum A |}.
Next Obligation.
constructor.
- * rewrite elem_of_list_fmap. by intros (?&?&?).
- * apply (NoDup_fmap_2 _); auto using NoDup_enum.
+ - rewrite elem_of_list_fmap. by intros (?&?&?).
+ - apply (NoDup_fmap_2 _); auto using NoDup_enum.
Qed.
Next Obligation.
intros ??? [x|]; [right|left]; auto.
@@ -221,9 +221,9 @@ Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
{| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
intros. apply NoDup_app; split_ands.
- * apply (NoDup_fmap_2 _). by apply NoDup_enum.
- * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
- * apply (NoDup_fmap_2 _). by apply NoDup_enum.
+ - apply (NoDup_fmap_2 _). by apply NoDup_enum.
+ - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
+ - apply (NoDup_fmap_2 _). by apply NoDup_enum.
Qed.
Next Obligation.
intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
@@ -238,20 +238,20 @@ Next Obligation.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. }
apply NoDup_app; split_ands.
- * by apply (NoDup_fmap_2 _), NoDup_enum.
- * intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
+ - by apply (NoDup_fmap_2 _), NoDup_enum.
+ - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
{ rewrite elem_of_nil. tauto. }
rewrite elem_of_app, elem_of_list_fmap.
intros [(?&?&?)|?]; simplify_equality.
+ destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto.
- * done.
+ - done.
Qed.
Next Obligation.
intros ?????? [x y]. induction (elem_of_enum x); simpl.
- * rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
- * rewrite elem_of_app; eauto.
+ - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
+ - rewrite elem_of_app; eauto.
Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
@@ -272,13 +272,13 @@ Next Obligation.
revert IH. generalize (list_enum (enum A) n). intros l Hl.
induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
apply NoDup_app; split_ands.
- * by apply (NoDup_fmap_2 _).
- * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
+ - by apply (NoDup_fmap_2 _).
+ - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. destruct Hx. revert Hxk2.
induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
intros [([??]&?&?)|?]; simplify_equality'; auto.
- * apply IH.
+ - apply IH.
Qed.
Next Obligation.
intros ???? [l Hl]. revert l Hl.
@@ -286,9 +286,9 @@ Next Obligation.
{ apply elem_of_list_singleton. by apply (sig_eq_pi _). }
revert IH. generalize (list_enum (enum A) n). intros k Hk.
induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
- * rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
+ - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
eexists (l↾Hl'). split. by apply (sig_eq_pi _). done.
- * rewrite elem_of_app. eauto.
+ - rewrite elem_of_app. eauto.
Qed.
Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
Proof.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index 77a83e6c23a16b2e25e7f60cbc54eb6b2e0dc480..38f1e7067760d557c4f10bfce6a0ac13f7808094 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -37,8 +37,8 @@ Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
gmap_wf m → gmap_wf (partial_alter f (encode i) m).
Proof.
intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
- * rewrite decode_encode; eauto.
- * rewrite lookup_partial_alter_ne by done. by apply Hm.
+ - rewrite decode_encode; eauto.
+ - rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed.
Instance gmap_partial_alter `{Countable K} {A} :
PartialAlter K A (gmap K A) := λ f i m,
@@ -78,7 +78,7 @@ Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
Proof.
split.
- * unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
+ - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
apply gmap_eq, map_eq; intros i; simpl in *.
apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
apply option_eq; intros x; split; intros Hi.
@@ -86,12 +86,12 @@ Proof.
by destruct (decode i); simplify_equality'; rewrite <-Hm.
+ pose proof (Hm2 i x Hi); simpl in *.
by destruct (decode i); simplify_equality'; rewrite Hm.
- * done.
- * intros A f [m Hm] i; apply (lookup_partial_alter f m).
- * intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
+ - done.
+ - intros A f [m Hm] i; apply (lookup_partial_alter f m).
+ - intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
by contradict Hs; apply (inj encode).
- * intros A B f [m Hm] i; apply (lookup_fmap f m).
- * intros A [m Hm]; unfold map_to_list; simpl.
+ - intros A B f [m Hm] i; apply (lookup_fmap f m).
+ - intros A [m Hm]; unfold map_to_list; simpl.
apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
induction (NoDup_map_to_list m) as [|[p x] l Hpx];
inversion 1 as [|??? Hm']; simplify_equality'; [by constructor|].
@@ -99,15 +99,15 @@ Proof.
rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_equality'.
feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
by destruct (decode p') as [i'|]; simplify_equality'.
- * intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
+ - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
apply bool_decide_unpack in Hm; rewrite elem_of_list_omap; split.
+ intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
feed pose proof (Hm p' x'); simpl in *; auto.
by destruct (decode p') as [i'|] eqn:?; simplify_equality'.
+ intros; exists (encode i,x); simpl.
by rewrite elem_of_map_to_list, decode_encode.
- * intros A B f [m Hm] i; apply (lookup_omap f m).
- * intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
+ - intros A B f [m Hm] i; apply (lookup_omap f m).
+ - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
Qed.
@@ -130,8 +130,8 @@ Instance gset_positive_fresh : Fresh positive (gset positive) := λ X,
Instance gset_positive_fresh_spec : FreshSpec positive (gset positive).
Proof.
split.
- * apply _.
- * by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
- * intros [[m Hm]]; unfold fresh; simpl.
+ - apply _.
+ - by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
+ - intros [[m Hm]]; unfold fresh; simpl.
by intros ?; apply (is_fresh (dom Pset m)), elem_of_dom_2 with ().
Qed.
diff --git a/prelude/hashset.v b/prelude/hashset.v
index b6f3f85f9547d4e3f1b9330b7364feedad559ff5..d368b5cc8d2e1f0e6ce9ccd6dc2d661da7b7d80b 100644
--- a/prelude/hashset.v
+++ b/prelude/hashset.v
@@ -63,12 +63,12 @@ Instance hashset_elems: Elements A (hashset hash) := λ m,
Global Instance: FinCollection A (hashset hash).
Proof.
split; [split; [split| |]| |].
- * intros ? (?&?&?); simplify_map_equality'.
- * unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
+ - intros ? (?&?&?); simplify_map_equality'.
+ - unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
intros x y. setoid_rewrite lookup_singleton_Some. split.
{ by intros (?&[? <-]&?); decompose_elem_of_list. }
intros ->; eexists [y]. by rewrite elem_of_list_singleton.
- * unfold elem_of, hashset_elem_of, union, hashset_union.
+ - unfold elem_of, hashset_elem_of, union, hashset_union.
intros [m1 Hm1] [m2 Hm2] x; simpl; setoid_rewrite lookup_union_with_Some.
split.
{ intros (?&[[]|[[]|(l&k&?&?&?)]]&Hx); simplify_equality'; eauto.
@@ -78,7 +78,7 @@ Proof.
exists (list_union l k). rewrite elem_of_list_union. naive_solver.
+ destruct (m1 !! hash x) as [l|]; eauto 6.
exists (list_union l k). rewrite elem_of_list_union. naive_solver.
- * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
+ - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
intros [m1 ?] [m2 ?] x; simpl.
setoid_rewrite lookup_intersection_with_Some. split.
{ intros (?&(l&k&?&?&?)&Hx); simplify_option_equality.
@@ -87,7 +87,7 @@ Proof.
by (by rewrite elem_of_list_intersection).
exists (list_intersection l k); split; [exists l, k|]; split_ands; auto.
by rewrite option_guard_True by eauto using elem_of_not_nil.
- * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
+ - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
intros [m1 ?] [m2 ?] x; simpl.
setoid_rewrite lookup_difference_with_Some. split.
{ intros (l'&[[??]|(l&k&?&?&?)]&Hx); simplify_option_equality;
@@ -97,13 +97,13 @@ Proof.
assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto.
by rewrite option_guard_True by eauto using elem_of_not_nil.
- * unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
+ - unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
{ intros ([n l]&Hx&Hn); simpl in *; rewrite elem_of_map_to_list in Hn.
cut (hash x = n); [intros <-; eauto|].
eapply (Forall_forall (λ x, hash x = n) l); eauto. eapply Hm; eauto. }
intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
- * unfold elements, hashset_elems. intros [m Hm]; simpl.
+ - unfold elements, hashset_elems. intros [m Hm]; simpl.
rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
induction Hm as [|[n l] m' [??]];
csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
@@ -152,10 +152,10 @@ Proof.
unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
rewrite elem_of_elements; split.
- * revert x. induction l as [|y l IH]; intros x; simpl.
+ - revert x. induction l as [|y l IH]; intros x; simpl.
{ by rewrite elem_of_empty. }
rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
- * induction 1; solve_elem_of.
+ - induction 1; solve_elem_of.
Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof.
diff --git a/prelude/lexico.v b/prelude/lexico.v
index c36833b9cbbae3c529d83929c4ee40db4b746b73..7acbb0c868e978bb436007eada50d6b16161ddba 100644
--- a/prelude/lexico.v
+++ b/prelude/lexico.v
@@ -49,9 +49,9 @@ Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
`{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
Proof.
split.
- * intros [x y]. apply prod_lexico_irreflexive.
+ - intros [x y]. apply prod_lexico_irreflexive.
by apply (irreflexivity lexico y).
- * intros [??] [??] [??] ??.
+ - intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply transitivity.
Qed.
Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
@@ -119,8 +119,8 @@ Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _).
Proof.
split.
- * intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
- * intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
+ - intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
+ - intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
eapply prod_lexico_transitive; eauto.
Qed.
Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
@@ -142,8 +142,8 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof.
unfold lexico, sig_lexico. split.
- * intros [x ?] ?. by apply (irreflexivity lexico x).
- * intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2.
+ - intros [x ?] ?. by apply (irreflexivity lexico x).
+ - intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2.
Qed.
Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
diff --git a/prelude/list.v b/prelude/list.v
index 54fcb80194676f93f9bc8f586500fb8a6931ef63..036b02c952d43eaee3173094213d22e51c02bfaf 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -370,9 +370,9 @@ Section setoid.
Global Instance map_equivalence : Equivalence ((≡) : relation (list A)).
Proof.
split.
- * intros l; induction l; constructor; auto.
- * induction 1; constructor; auto.
- * intros l1 l2 l3 Hl; revert l3.
+ - intros l; induction l; constructor; auto.
+ - induction 1; constructor; auto.
+ - intros l1 l2 l3 Hl; revert l3.
induction Hl; inversion_clear 1; constructor; try etransitivity; eauto.
Qed.
Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
@@ -409,10 +409,10 @@ Proof. done. Qed.
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
revert l2. induction l1; intros [|??] H.
- * done.
- * discriminate (H 0).
- * discriminate (H 0).
- * f_equal; [by injection (H 0)|]. apply (IHl1 _ $ λ i, H (S i)).
+ - done.
+ - discriminate (H 0).
+ - discriminate (H 0).
+ - f_equal; [by injection (H 0)|]. apply (IHl1 _ $ λ i, H (S i)).
Qed.
Global Instance list_eq_dec {dec : ∀ x y, Decision (x = y)} : ∀ l k,
Decision (l = k) := list_eq_dec dec.
@@ -455,10 +455,10 @@ Lemma list_eq_same_length l1 l2 n :
(∀ i x y, i < n → l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2.
Proof.
intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx.
- * destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
+ - destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
{ rewrite Hlen; eauto using lookup_lt_Some. }
rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some.
- * by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
+ - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
Qed.
Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
@@ -472,10 +472,10 @@ Lemma lookup_app_Some l1 l2 i x :
l1 !! i = Some x ∨ length l1 ≤ i ∧ l2 !! (i - length l1) = Some x.
Proof.
split.
- * revert i. induction l1 as [|y l1 IH]; intros [|i] ?;
+ - revert i. induction l1 as [|y l1 IH]; intros [|i] ?;
simplify_equality'; auto with lia.
destruct (IH i) as [?|[??]]; auto with lia.
- * intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r.
+ - intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r.
Qed.
Lemma list_lookup_middle l1 l2 x n :
n = length l1 → (l1 ++ x :: l2) !! n = Some x.
@@ -505,10 +505,10 @@ Lemma list_lookup_insert_Some l i x j y :
Proof.
destruct (decide (i = j)) as [->|];
[split|rewrite list_lookup_insert_ne by done; tauto].
- * intros Hy. assert (j < length l).
+ - intros Hy. assert (j < length l).
{ rewrite <-(insert_length l j x); eauto using lookup_lt_Some. }
rewrite list_lookup_insert in Hy by done; naive_solver.
- * intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
+ - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
Qed.
Lemma list_insert_commute l i j x y :
i ≠j → <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
@@ -517,8 +517,8 @@ Lemma list_lookup_other l i x :
length l ≠1 → l !! i = Some x → ∃ j y, j ≠i ∧ l !! j = Some y.
Proof.
intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'.
- * by exists 1, x1.
- * by exists 0, x0.
+ - by exists 1, x1.
+ - by exists 0, x0.
Qed.
Lemma alter_app_l f l1 l2 i :
i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2.
@@ -594,10 +594,10 @@ Proof.
destruct (decide (i + length k ≤ j)).
{ rewrite list_lookup_inserts_ge by done; intuition lia. }
split.
- * intros Hy. assert (j < length l).
+ - intros Hy. assert (j < length l).
{ rewrite <-(inserts_length l i k); eauto using lookup_lt_Some. }
rewrite list_lookup_inserts in Hy by lia. intuition lia.
- * intuition. by rewrite list_lookup_inserts by lia.
+ - intuition. by rewrite list_lookup_inserts by lia.
Qed.
Lemma list_insert_inserts_lt l i j x k :
i < j → <[i:=x]>(list_inserts j k l) = list_inserts j k (<[i:=x]>l).
@@ -622,8 +622,8 @@ Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
Proof.
induction l1.
- * split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
- * simpl. rewrite !elem_of_cons, IHl1. tauto.
+ - split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
+ - simpl. rewrite !elem_of_cons, IHl1. tauto.
Qed.
Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed.
@@ -651,9 +651,9 @@ Lemma elem_of_list_omap {B} (f : A → option B) l (y : B) :
y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
Proof.
split.
- * induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
+ - induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
setoid_rewrite elem_of_cons; naive_solver.
- * intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
+ - intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
simplify_equality; try constructor; auto.
Qed.
@@ -671,17 +671,17 @@ Proof. constructor. apply not_elem_of_nil. constructor. Qed.
Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
Proof.
induction l; simpl.
- * rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
- * rewrite !NoDup_cons.
+ - rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
+ - rewrite !NoDup_cons.
setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Qed.
Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
Proof.
induction 1 as [|x l k Hlk IH | |].
- * by rewrite !NoDup_nil.
- * by rewrite !NoDup_cons, IH, Hlk.
- * rewrite !NoDup_cons, !elem_of_cons. intuition.
- * intuition.
+ - by rewrite !NoDup_nil.
+ - by rewrite !NoDup_cons, IH, Hlk.
+ - rewrite !NoDup_cons, !elem_of_cons. intuition.
+ - intuition.
Qed.
Lemma NoDup_lookup l i j x :
NoDup l → l !! i = Some x → l !! j = Some x → i = j.
@@ -696,9 +696,9 @@ Lemma NoDup_alt l :
Proof.
split; eauto using NoDup_lookup.
induction l as [|x l IH]; intros Hl; constructor.
- * rewrite elem_of_list_lookup. intros [i ?].
+ - rewrite elem_of_list_lookup. intros [i ?].
by feed pose proof (Hl (S i) 0 x); auto.
- * apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
+ - apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
Qed.
Section no_dup_dec.
@@ -740,9 +740,9 @@ Section list_set.
Lemma NoDup_list_difference l k : NoDup l → NoDup (list_difference l k).
Proof.
induction 1; simpl; try case_decide.
- * constructor.
- * done.
- * constructor. rewrite elem_of_list_difference; intuition. done.
+ - constructor.
+ - done.
+ - constructor. rewrite elem_of_list_difference; intuition. done.
Qed.
Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
Proof.
@@ -752,9 +752,9 @@ Section list_set.
Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k).
Proof.
intros. apply NoDup_app. repeat split.
- * by apply NoDup_list_difference.
- * intro. rewrite elem_of_list_difference. intuition.
- * done.
+ - by apply NoDup_list_difference.
+ - intro. rewrite elem_of_list_difference. intuition.
+ - done.
Qed.
Lemma elem_of_list_intersection l k x :
x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
@@ -765,23 +765,23 @@ Section list_set.
Lemma NoDup_list_intersection l k : NoDup l → NoDup (list_intersection l k).
Proof.
induction 1; simpl; try case_decide.
- * constructor.
- * constructor. rewrite elem_of_list_intersection; intuition. done.
- * done.
+ - constructor.
+ - constructor. rewrite elem_of_list_intersection; intuition. done.
+ - done.
Qed.
Lemma elem_of_list_intersection_with f l k x :
x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
Proof.
split.
- * induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
+ - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
intros Hx. setoid_rewrite elem_of_cons.
cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
∨ x ∈ list_intersection_with f l k); [naive_solver|].
clear IH. revert Hx. generalize (list_intersection_with f l k).
induction k; simpl; [by auto|].
case_match; setoid_rewrite elem_of_cons; naive_solver.
- * intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+ - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+ generalize (list_intersection_with f l k).
induction Hx2; simpl; [by rewrite Hx; left |].
case_match; simpl; try setoid_rewrite elem_of_cons; auto.
@@ -917,14 +917,14 @@ Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
Lemma take_alter f l n i : n ≤ i → take n (alter f i l) = take n l.
Proof.
intros. apply list_eq. intros j. destruct (le_lt_dec n j).
- * by rewrite !lookup_take_ge.
- * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
+ - by rewrite !lookup_take_ge.
+ - by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
Lemma take_insert l n i x : n ≤ i → take n (<[i:=x]>l) = take n l.
Proof.
intros. apply list_eq. intros j. destruct (le_lt_dec n j).
- * by rewrite !lookup_take_ge.
- * by rewrite !lookup_take, !list_lookup_insert_ne by lia.
+ - by rewrite !lookup_take_ge.
+ - by rewrite !lookup_take, !list_lookup_insert_ne by lia.
Qed.
(** ** Properties of the [drop] function *)
@@ -988,8 +988,8 @@ Lemma lookup_replicate n x y i :
replicate n x !! i = Some y ↔ y = x ∧ i < n.
Proof.
split.
- * revert i. induction n; intros [|?]; naive_solver auto with lia.
- * intros [-> Hi]. revert i Hi.
+ - revert i. induction n; intros [|?]; naive_solver auto with lia.
+ - intros [-> Hi]. revert i Hi.
induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma lookup_replicate_1 n x y i :
@@ -1000,8 +1000,8 @@ Proof. by rewrite lookup_replicate. Qed.
Lemma lookup_replicate_None n x i : n ≤ i ↔ replicate n x !! i = None.
Proof.
rewrite eq_None_not_Some, Nat.le_ngt. split.
- * intros Hin [x' Hx']; destruct Hin. rewrite lookup_replicate in Hx'; tauto.
- * intros Hx ?. destruct Hx. exists x; auto using lookup_replicate_2.
+ - intros Hin [x' Hx']; destruct Hin. rewrite lookup_replicate in Hx'; tauto.
+ - intros Hx ?. destruct Hx. exists x; auto using lookup_replicate_2.
Qed.
Lemma insert_replicate x n i : <[i:=x]>(replicate n x) = replicate n x.
Proof. revert i. induction n; intros [|?]; f_equal'; auto. Qed.
@@ -1025,8 +1025,8 @@ Lemma replicate_as_elem_of x n l :
Proof.
split; [intros <-; eauto using elem_of_replicate_inv, replicate_length|].
intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal'.
- * apply Hl. by left.
- * apply IH. intros ??. apply Hl. by right.
+ - apply Hl. by left.
+ - apply IH. intros ??. apply Hl. by right.
Qed.
Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
Proof.
@@ -1060,8 +1060,8 @@ Lemma resize_plus l n m x :
resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
revert n m. induction l; intros [|?] [|?]; f_equal'; auto.
- * by rewrite Nat.add_0_r, (right_id_L [] (++)).
- * by rewrite replicate_plus.
+ - by rewrite Nat.add_0_r, (right_id_L [] (++)).
+ - by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq l n m x :
length l = n → resize (n + m) x l = l ++ replicate m x.
@@ -1086,8 +1086,8 @@ Proof. revert m. induction n; intros [|?]; f_equal'; auto. Qed.
Lemma resize_resize l n m x : n ≤ m → resize n x (resize m x l) = resize n x l.
Proof.
revert n m. induction l; simpl.
- * intros. by rewrite !resize_nil, resize_replicate.
- * intros [|?] [|?] ?; f_equal'; auto with lia.
+ - intros. by rewrite !resize_nil, resize_replicate.
+ - intros [|?] [|?] ?; f_equal'; auto with lia.
Qed.
Lemma resize_idemp l n x : resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.
@@ -1109,8 +1109,8 @@ Lemma drop_resize_le l n m x :
n ≤ m → drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
revert n m. induction l; simpl.
- * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
- * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
+ - intros. by rewrite drop_nil, !resize_nil, drop_replicate.
+ - intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus l n m x :
drop n (resize (n + m) x l) = resize m x (drop n l).
@@ -1118,8 +1118,8 @@ Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
Proof.
intros ??. destruct (decide (n < length l)).
- * by rewrite resize_le, lookup_take by lia.
- * by rewrite resize_ge, lookup_app_l by lia.
+ - by rewrite resize_le, lookup_take by lia.
+ - by rewrite resize_ge, lookup_app_l by lia.
Qed.
Lemma lookup_resize_new l n x i :
length l ≤ i → i < n → resize n x l !! i = Some x.
@@ -1205,14 +1205,14 @@ Lemma sublist_lookup_reshape l i n m :
reshape (replicate m n) l !! i = sublist_lookup (i * n) n l.
Proof.
intros Hn Hl. unfold sublist_lookup. apply option_eq; intros x; split.
- * intros Hx. case_option_guard as Hi.
+ - intros Hx. case_option_guard as Hi.
{ f_equal. clear Hi. revert i l Hl Hx.
induction m as [|m IH]; intros [|i] l ??; simplify_equality'; auto.
rewrite <-drop_drop. apply IH; rewrite ?drop_length; auto with lia. }
destruct Hi. rewrite Hl, <-Nat.mul_succ_l.
apply Nat.mul_le_mono_r, Nat.le_succ_l. apply lookup_lt_Some in Hx.
by rewrite reshape_length, replicate_length in Hx.
- * intros Hx. case_option_guard as Hi; simplify_equality'.
+ - intros Hx. case_option_guard as Hi; simplify_equality'.
revert i l Hl Hi. induction m as [|m IH]; [auto with lia|].
intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop.
rewrite IH; rewrite ?drop_length; auto with lia.
@@ -1347,8 +1347,8 @@ Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Comm (≡ₚ) (@app A).
Proof.
intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
- * by rewrite (right_id_L [] (++)).
- * rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
+ - by rewrite (right_id_L [] (++)).
+ - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::).
Proof. red. eauto using Permutation_cons_inv. Qed.
@@ -1364,8 +1364,8 @@ Qed.
Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
Proof.
intros Hl. apply replicate_as_elem_of. split.
- * by rewrite <-Hl, replicate_length.
- * intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
+ - by rewrite <-Hl, replicate_length.
+ - intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
Qed.
Lemma reverse_Permutation l : reverse l ≡ₚ l.
Proof.
@@ -1382,8 +1382,8 @@ Qed.
Global Instance: PreOrder (@prefix_of A).
Proof.
split.
- * intros ?. eexists []. by rewrite (right_id_L [] (++)).
- * intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
+ - intros ?. eexists []. by rewrite (right_id_L [] (++)).
+ - intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
Qed.
Lemma prefix_of_nil l : [] `prefix_of` l.
Proof. by exists l. Qed.
@@ -1415,8 +1415,8 @@ Proof. intros [??]. discriminate_list_equality. Qed.
Global Instance: PreOrder (@suffix_of A).
Proof.
split.
- * intros ?. by eexists [].
- * intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
+ - intros ?. by eexists [].
+ - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
Qed.
Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
@@ -1488,9 +1488,9 @@ Section prefix_ops.
Proof.
intros Hl ->. destruct (prefix_of_snoc_not k3 x2).
eapply max_prefix_of_max_alt; eauto.
- * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
+ - rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
apply prefix_of_app, prefix_of_cons, prefix_of_nil.
- * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
+ - rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
apply prefix_of_app, prefix_of_cons, prefix_of_nil.
Qed.
End prefix_ops.
@@ -1499,8 +1499,8 @@ Lemma prefix_suffix_reverse l1 l2 :
l1 `prefix_of` l2 ↔ reverse l1 `suffix_of` reverse l2.
Proof.
split; intros [k E]; exists (reverse k).
- * by rewrite E, reverse_app.
- * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
+ - by rewrite E, reverse_app.
+ - by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Qed.
Lemma suffix_prefix_reverse l1 l2 :
l1 `suffix_of` l2 ↔ reverse l1 `prefix_of` reverse l2.
@@ -1626,9 +1626,9 @@ Section max_suffix_of.
Proof.
intros Hl ->. destruct (suffix_of_cons_not x2 k3).
eapply max_suffix_of_max_alt; eauto.
- * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
+ - rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
by apply (suffix_of_app [x2]), suffix_of_app_r.
- * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
+ - rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
by apply (suffix_of_app [x2]), suffix_of_app_r.
Qed.
End max_suffix_of.
@@ -1654,37 +1654,37 @@ Lemma sublist_cons_l x l k :
x :: l `sublist` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist` k2.
Proof.
split.
- * intros Hlk. induction k as [|y k IH]; inversion Hlk.
+ - intros Hlk. induction k as [|y k IH]; inversion Hlk.
+ eexists [], k. by repeat constructor.
+ destruct IH as (k1&k2&->&?); auto. by exists (y :: k1), k2.
- * intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
+ - intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
Qed.
Lemma sublist_app_r l k1 k2 :
l `sublist` k1 ++ k2 ↔
∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
Proof.
split.
- * revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
+ - revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
{ eexists [], l. by repeat constructor. }
rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst.
+ destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst.
exists l1, l2. auto using sublist_cons.
+ destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
exists (y :: l1), l2. auto using sublist_skip.
- * intros (?&?&?&?&?); subst. auto using sublist_app.
+ - intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_l l1 l2 k :
l1 ++ l2 `sublist` k ↔
∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
Proof.
split.
- * revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
+ - revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
{ eexists [], k. by repeat constructor. }
rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst.
destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst.
exists (k1 ++ x :: h1), h2. rewrite <-(assoc_L (++)).
auto using sublist_inserts_l, sublist_skip.
- * intros (?&?&?&?&?); subst. auto using sublist_app.
+ - intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
Proof.
@@ -1707,14 +1707,14 @@ Qed.
Global Instance: PartialOrder (@sublist A).
Proof.
split; [split|].
- * intros l. induction l; constructor; auto.
- * intros l1 l2 l3 Hl12. revert l3. induction Hl12.
+ - intros l. induction l; constructor; auto.
+ - intros l1 l2 l3 Hl12. revert l3. induction Hl12.
+ auto using sublist_nil_l.
+ intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
eauto using sublist_inserts_l, sublist_skip.
+ intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
eauto using sublist_inserts_l, sublist_cons.
- * intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
+ - intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
induction Hl12; f_equal'; auto with arith.
apply sublist_length in Hl12. lia.
Qed.
@@ -1735,10 +1735,10 @@ Proof.
intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is).
{ intros help. apply (help []). }
induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
- * by eexists [].
- * destruct (IH (k ++ [x])) as [is His]. exists is.
+ - by eexists [].
+ - destruct (IH (k ++ [x])) as [is His]. exists is.
by rewrite <-!(assoc_L (++)) in His.
- * destruct (IH k) as [is His]. exists (is ++ [length k]).
+ - destruct (IH k) as [is His]. exists (is ++ [length k]).
rewrite fold_right_app. simpl. by rewrite delete_middle.
Qed.
Lemma Permutation_sublist l1 l2 l3 :
@@ -1746,16 +1746,16 @@ Lemma Permutation_sublist l1 l2 l3 :
Proof.
intros Hl1l2. revert l3.
induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2].
- * intros l3. by exists l3.
- * intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
+ - intros l3. by exists l3.
+ - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4).
split. by apply sublist_inserts_l, sublist_skip. by rewrite Hl4.
- * intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
+ - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst.
exists (l3' ++ y :: l5' ++ x :: l5''). split.
- - by do 2 apply sublist_inserts_l, sublist_skip.
- - by rewrite !Permutation_middle, Permutation_swap.
- * intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
+ + by do 2 apply sublist_inserts_l, sublist_skip.
+ + by rewrite !Permutation_middle, Permutation_swap.
+ - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
split. done. etransitivity; eauto.
Qed.
@@ -1764,19 +1764,19 @@ Lemma sublist_Permutation l1 l2 l3 :
Proof.
intros Hl1l2 Hl2l3. revert l1 Hl1l2.
induction Hl2l3 as [|x l2 l3 ? IH|x y l2|l2 l2' l3 ? IH1 ? IH2].
- * intros l1. by exists l1.
- * intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
+ - intros l1. by exists l1.
+ - intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
{ destruct (IH l1) as (l4&?&?); trivial.
exists l4. split. done. by constructor. }
destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
split. by constructor. by constructor.
- * intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
+ - intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
{ exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
rewrite sublist_cons_r in Hl1. destruct Hl1 as [?|(l1''&?&?)]; subst.
+ exists (y :: l1'). by repeat constructor.
+ exists (x :: y :: l1''). by repeat constructor.
- * intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
+ - intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''.
split; [|done]. etransitivity; eauto.
Qed.
@@ -1794,8 +1794,8 @@ Qed.
Global Instance: PreOrder (@contains A).
Proof.
split.
- * intros l. induction l; constructor; auto.
- * red. apply contains_trans.
+ - intros l. induction l; constructor; auto.
+ - red. apply contains_trans.
Qed.
Lemma Permutation_contains l1 l2 : l1 ≡ₚ l2 → l1 `contains` l2.
Proof. induction 1; econstructor; eauto. Qed.
@@ -1805,18 +1805,18 @@ Lemma contains_Permutation l1 l2 : l1 `contains` l2 → ∃ k, l2 ≡ₚ l1 ++ k
Proof.
induction 1 as
[|x y l ? [k Hk]| |x l1 l2 ? [k Hk]|l1 l2 l3 ? [k Hk] ? [k' Hk']].
- * by eexists [].
- * exists k. by rewrite Hk.
- * eexists []. rewrite (right_id_L [] (++)). by constructor.
- * exists (x :: k). by rewrite Hk, Permutation_middle.
- * exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
+ - by eexists [].
+ - exists k. by rewrite Hk.
+ - eexists []. rewrite (right_id_L [] (++)). by constructor.
+ - exists (x :: k). by rewrite Hk, Permutation_middle.
+ - exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
Qed.
Lemma contains_Permutation_length_le l1 l2 :
length l2 ≤ length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
Proof.
intros Hl21 Hl12. destruct (contains_Permutation l1 l2) as [[|??] Hk]; auto.
- * by rewrite Hk, (right_id_L [] (++)).
- * rewrite Hk, app_length in Hl21; simpl in Hl21; lia.
+ - by rewrite Hk, (right_id_L [] (++)).
+ - rewrite Hk, app_length in Hl21; simpl in Hl21; lia.
Qed.
Lemma contains_Permutation_length_eq l1 l2 :
length l2 = length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
@@ -1824,9 +1824,9 @@ Proof. intro. apply contains_Permutation_length_le. lia. Qed.
Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@contains A).
Proof.
intros l1 l2 ? k1 k2 ?. split; intros.
- * transitivity l1. by apply Permutation_contains.
+ - transitivity l1. by apply Permutation_contains.
transitivity k1. done. by apply Permutation_contains.
- * transitivity l2. by apply Permutation_contains.
+ - transitivity l2. by apply Permutation_contains.
transitivity k2. done. by apply Permutation_contains.
Qed.
Global Instance: AntiSymm (≡ₚ) (@contains A).
@@ -1844,11 +1844,11 @@ Lemma contains_sublist_l l1 l3 :
Proof.
split.
{ intros Hl13. elim Hl13; clear l1 l3 Hl13.
- * by eexists [].
- * intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
- * intros x y l. exists (y :: x :: l). by repeat constructor.
- * intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
- * intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
+ - by eexists [].
+ - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
+ - intros x y l. exists (y :: x :: l). by repeat constructor.
+ - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
+ - intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
exists l3'. split; etransitivity; eauto. }
intros (l2&?&?).
@@ -1877,41 +1877,41 @@ Lemma contains_cons_r x l k :
l `contains` x :: k ↔ l `contains` k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' `contains` k.
Proof.
split.
- * rewrite contains_sublist_r. intros (l'&E&Hl').
+ - rewrite contains_sublist_r. intros (l'&E&Hl').
rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst.
+ left. rewrite E. eauto using sublist_contains.
+ right. eauto using sublist_contains.
- * intros [?|(?&E&?)]; [|rewrite E]; by constructor.
+ - intros [?|(?&E&?)]; [|rewrite E]; by constructor.
Qed.
Lemma contains_cons_l x l k :
x :: l `contains` k ↔ ∃ k', k ≡ₚ x :: k' ∧ l `contains` k'.
Proof.
split.
- * rewrite contains_sublist_l. intros (l'&Hl'&E).
+ - rewrite contains_sublist_l. intros (l'&Hl'&E).
rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst.
exists (k1 ++ k2). split; eauto using contains_inserts_l, sublist_contains.
by rewrite Permutation_middle.
- * intros (?&E&?). rewrite E. by constructor.
+ - intros (?&E&?). rewrite E. by constructor.
Qed.
Lemma contains_app_r l k1 k2 :
l `contains` k1 ++ k2 ↔ ∃ l1 l2,
l ≡ₚ l1 ++ l2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
split.
- * rewrite contains_sublist_r. intros (l'&E&Hl').
+ - rewrite contains_sublist_r. intros (l'&E&Hl').
rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
exists l1, l2. eauto using sublist_contains.
- * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
+ - intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_l l1 l2 k :
l1 ++ l2 `contains` k ↔ ∃ k1 k2,
k ≡ₚ k1 ++ k2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
split.
- * rewrite contains_sublist_l. intros (l'&Hl'&E).
+ - rewrite contains_sublist_l. intros (l'&Hl'&E).
rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
exists k1, k2. split. done. eauto using sublist_contains.
- * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
+ - intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_inv_l l1 l2 k :
k ++ l1 `contains` k ++ l2 → l1 `contains` l2.
@@ -1947,8 +1947,8 @@ Lemma Permutation_alt l1 l2 :
l1 ≡ₚ l2 ↔ length l1 = length l2 ∧ l1 `contains` l2.
Proof.
split.
- * by intros Hl; rewrite Hl.
- * intros [??]; auto using contains_Permutation_length_eq.
+ - by intros Hl; rewrite Hl.
+ - intros [??]; auto using contains_Permutation_length_eq.
Qed.
Lemma NoDup_contains l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l `contains` k.
@@ -1976,12 +1976,12 @@ Section contains_dec.
Proof.
intros Hl. revert k1. induction Hl
as [|y l1 l2 ? IH|y1 y2 l|l1 l2 l3 ? IH1 ? IH2]; simpl; intros k1 Hk1.
- * done.
- * case_decide; simplify_equality; eauto.
+ - done.
+ - case_decide; simplify_equality; eauto.
destruct (list_remove x l1) as [l|] eqn:?; simplify_equality.
destruct (IH l) as (?&?&?); simplify_option_equality; eauto.
- * simplify_option_equality; eauto using Permutation_swap.
- * destruct (IH1 k1) as (k2&?&?); trivial.
+ - simplify_option_equality; eauto using Permutation_swap.
+ - destruct (IH1 k1) as (k2&?&?); trivial.
destruct (IH2 k2) as (k3&?&?); trivial.
exists k3. split; eauto. by transitivity k2.
Qed.
@@ -1994,20 +1994,20 @@ Section contains_dec.
l ≡ₚ x :: k → ∃ k', list_remove x l = Some k' ∧ k ≡ₚ k'.
Proof.
intros. destruct (list_remove_Permutation (x :: k) l k x) as (k'&?&?).
- * done.
- * simpl; by case_decide.
- * by exists k'.
+ - done.
+ - simpl; by case_decide.
+ - by exists k'.
Qed.
Lemma list_remove_list_contains l1 l2 :
l1 `contains` l2 ↔ is_Some (list_remove_list l1 l2).
Proof.
split.
- * revert l2. induction l1 as [|x l1 IH]; simpl.
+ - revert l2. induction l1 as [|x l1 IH]; simpl.
{ intros l2 _. by exists l2. }
intros l2. rewrite contains_cons_l. intros (k&Hk&?).
destruct (list_remove_Some_inv l2 k x) as (k2&?&Hk2); trivial.
simplify_option_equality. apply IH. by rewrite <-Hk2.
- * intros [k Hk]. revert l2 k Hk.
+ - intros [k Hk]. revert l2 k Hk.
induction l1 as [|x l1 IH]; simpl; intros l2 k.
{ intros. apply contains_nil_l. }
destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_equality.
@@ -2168,8 +2168,8 @@ Section Forall_Exists.
Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
Proof.
split.
- * induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
- * intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
+ - induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
+ - intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
inversion Hin; subst. by left. right; auto.
Qed.
Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
@@ -2177,8 +2177,8 @@ Section Forall_Exists.
Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
Proof.
split.
- * induction l1; inversion 1; intuition.
- * intros [H|H]; [induction H | induction l1]; simpl; intuition.
+ - induction l1; inversion 1; intuition.
+ - intros [H|H]; [induction H | induction l1]; simpl; intuition.
Qed.
Lemma Exists_impl (Q : A → Prop) l :
Exists P l → (∀ x, P x → Q x) → Exists Q l.
@@ -2238,9 +2238,9 @@ Lemma Forall_seq (P : nat → Prop) i n :
Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
Proof.
rewrite Forall_lookup. split.
- * intros H j [??]. apply (H (j - i)).
+ - intros H j [??]. apply (H (j - i)).
rewrite lookup_seq; auto with f_equal lia.
- * intros H j x Hj. apply lookup_seq_inv in Hj.
+ - intros H j x Hj. apply lookup_seq_inv in Hj.
destruct Hj; subst. auto with lia.
Qed.
@@ -2441,8 +2441,8 @@ Section Forall2.
Proof.
unfold sublist_lookup. intros Hlk Hl.
exists (take i (drop n k)); simplify_option_equality.
- * auto using Forall2_take, Forall2_drop.
- * apply Forall2_length in Hlk; lia.
+ - auto using Forall2_take, Forall2_drop.
+ - apply Forall2_length in Hlk; lia.
Qed.
Lemma Forall2_sublist_lookup_r l k n i k' :
Forall2 P l k → sublist_lookup n i k = Some k' →
@@ -2540,9 +2540,9 @@ Section Forall3.
k = k1 ++ k2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
revert k k'. induction l1 as [|x l1 IH]; simpl; inversion_clear 1.
- * by repeat eexists; eauto.
- * by repeat eexists; eauto.
- * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+ - by repeat eexists; eauto.
+ - by repeat eexists; eauto.
+ - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
Qed.
Lemma Forall3_cons_inv_m l y k k' :
Forall3 P l (y :: k) k' → ∃ x l2 z k2',
@@ -2553,9 +2553,9 @@ Section Forall3.
l = l1 ++ l2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
revert l k'. induction k1 as [|x k1 IH]; simpl; inversion_clear 1.
- * by repeat eexists; eauto.
- * by repeat eexists; eauto.
- * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+ - by repeat eexists; eauto.
+ - by repeat eexists; eauto.
+ - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
Qed.
Lemma Forall3_cons_inv_r l k z k' :
Forall3 P l k (z :: k') → ∃ x l2 y k2,
@@ -2566,9 +2566,9 @@ Section Forall3.
l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
revert l k. induction k1' as [|x k1' IH]; simpl; inversion_clear 1.
- * by repeat eexists; eauto.
- * by repeat eexists; eauto.
- * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+ - by repeat eexists; eauto.
+ - by repeat eexists; eauto.
+ - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
Qed.
Lemma Forall3_impl (Q : A → B → C → Prop) l k k' :
Forall3 P l k k' → (∀ x y z, P x y z → Q x y z) → Forall3 Q l k k'.
@@ -2682,8 +2682,8 @@ Section fmap.
Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
Proof.
induction l as [|y l IH]; simpl; inversion_clear 1.
- * exists y. split; [done | by left].
- * destruct IH as [z [??]]. done. exists z. split; [done | by right].
+ - exists y. split; [done | by left].
+ - destruct IH as [z [??]]. done. exists z. split; [done | by right].
Qed.
Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
Proof.
@@ -2750,10 +2750,10 @@ Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
(∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (l.*1).
Proof.
intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor.
- * rewrite elem_of_list_fmap.
+ - rewrite elem_of_list_fmap.
intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
- * apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto.
+ - apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto.
Qed.
Section bind.
@@ -2773,17 +2773,17 @@ Section bind.
Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
Proof.
induction 1; csimpl; auto.
- * by apply contains_app.
- * by rewrite !(assoc_L (++)), (comm (++) (f _)).
- * by apply contains_inserts_l.
- * etransitivity; eauto.
+ - by apply contains_app.
+ - by rewrite !(assoc_L (++)), (comm (++) (f _)).
+ - by apply contains_inserts_l.
+ - etransitivity; eauto.
Qed.
Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
Proof.
induction 1; csimpl; auto.
- * by f_equiv.
- * by rewrite !(assoc_L (++)), (comm (++) (f _)).
- * etransitivity; eauto.
+ - by f_equiv.
+ - by rewrite !(assoc_L (++)), (comm (++) (f _)).
+ - etransitivity; eauto.
Qed.
Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
Proof. done. Qed.
@@ -2795,18 +2795,18 @@ Section bind.
x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
Proof.
split.
- * induction l as [|y l IH]; csimpl; [inversion 1|].
+ - induction l as [|y l IH]; csimpl; [inversion 1|].
rewrite elem_of_app. intros [?|?].
+ exists y. split; [done | by left].
+ destruct IH as [z [??]]. done. exists z. split; [done | by right].
- * intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
+ - intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
Qed.
Lemma Forall_bind (P : B → Prop) l :
Forall P (l ≫= f) ↔ Forall (Forall P ∘ f) l.
Proof.
split.
- * induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
- * induction 1; csimpl; rewrite ?Forall_app; auto.
+ - induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
+ - induction 1; csimpl; rewrite ?Forall_app; auto.
Qed.
Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
@@ -2858,8 +2858,8 @@ Section mapM.
Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
Proof.
revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
- * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
- * destruct (f x) eqn:?; intros; simplify_option_equality; auto.
+ - destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
+ - destruct (f x) eqn:?; intros; simplify_option_equality; auto.
Qed.
Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
Proof.
@@ -2916,8 +2916,8 @@ Section permutations.
Lemma interleave_Permutation x l l' : l' ∈ interleave x l → l' ≡ₚ x :: l.
Proof.
revert l'. induction l as [|y l IH]; intros l'; simpl.
- * rewrite elem_of_list_singleton. by intros ->.
- * rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|].
+ - rewrite elem_of_list_singleton. by intros ->.
+ - rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|].
rewrite (IH _ H). constructor.
Qed.
Lemma permutations_refl l : l ∈ permutations l.
@@ -2931,8 +2931,8 @@ Section permutations.
Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
Proof.
simpl. apply elem_of_list_bind. exists (y :: l). split; simpl.
- * destruct l; csimpl; rewrite !elem_of_cons; auto.
- * apply elem_of_list_bind. simpl.
+ - destruct l; csimpl; rewrite !elem_of_cons; auto.
+ - apply elem_of_list_bind. simpl.
eauto using interleave_cons, permutations_refl.
Qed.
Lemma permutations_nil l : l ∈ permutations [] ↔ l = [].
@@ -2947,12 +2947,12 @@ Section permutations.
by rewrite (comm (++)), elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [??]]]; simplify_equality'.
- * rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
+ - rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
+ exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+ exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+ exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
- * rewrite elem_of_cons, elem_of_list_fmap in Hl1.
+ - rewrite elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [l1' [??]]]; subst.
+ exists (x1 :: y :: l3). csimpl.
rewrite !elem_of_cons, !elem_of_list_fmap.
@@ -2970,9 +2970,9 @@ Section permutations.
by rewrite elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [? Hl2']]]; simplify_equality'.
- * rewrite elem_of_list_bind in Hl1.
+ - rewrite elem_of_list_bind in Hl1.
destruct Hl1 as [l1' [??]]. by exists l1'.
- * rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind.
+ - rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind.
destruct Hl1 as [l1' [??]]. destruct (IH l1' l2') as (l1''&?&?); auto.
destruct (interleave_interleave_toggle y x l1 l1' l1'') as (?&?&?); eauto.
Qed.
@@ -2980,19 +2980,19 @@ Section permutations.
l1 ∈ permutations l2 → l2 ∈ permutations l3 → l1 ∈ permutations l3.
Proof.
revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
- * rewrite !elem_of_list_singleton. intros Hl1 ->; simpl in *.
+ - rewrite !elem_of_list_singleton. intros Hl1 ->; simpl in *.
by rewrite elem_of_list_singleton in Hl1.
- * rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
+ - rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
Qed.
Lemma permutations_Permutation l l' : l' ∈ permutations l ↔ l ≡ₚ l'.
Proof.
split.
- * revert l'. induction l; simpl; intros l''.
+ - revert l'. induction l; simpl; intros l''.
+ rewrite elem_of_list_singleton. by intros ->.
+ rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
rewrite (interleave_Permutation _ _ _ Hl''). constructor; auto.
- * induction 1; eauto using permutations_refl,
+ - induction 1; eauto using permutations_refl,
permutations_skip, permutations_swap, permutations_trans.
Qed.
End permutations.
@@ -3195,11 +3195,11 @@ Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
split.
- * revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
+ - revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
{ by eexists [], k, z. }
destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |].
eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(assoc_L (++)).
- * intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
+ - intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
intros l; right. by rewrite reverse_cons, <-!(assoc_L (++)).
Qed.
Section zipped_list_ind.
@@ -3276,9 +3276,9 @@ Section eval.
Lemma eval_alt t : eval E t = to_list t ≫= from_option [] ∘ (E !!).
Proof.
induction t; csimpl.
- * done.
- * by rewrite (right_id_L [] (++)).
- * rewrite bind_app. by f_equal.
+ - done.
+ - by rewrite (right_id_L [] (++)).
+ - rewrite bind_app. by f_equal.
Qed.
Lemma eval_eq t1 t2 : to_list t1 = to_list t2 → eval E t1 = eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
diff --git a/prelude/listset.v b/prelude/listset.v
index d405dd4d19d2d3a8a5b6a191c8d26024fadeabdc..0b50e34efc3fdda303e8bb32d49c9e5db9931332 100644
--- a/prelude/listset.v
+++ b/prelude/listset.v
@@ -21,9 +21,9 @@ Global Opaque listset_singleton listset_empty.
Global Instance: SimpleCollection A (listset A).
Proof.
split.
- * by apply not_elem_of_nil.
- * by apply elem_of_list_singleton.
- * intros [?] [?]. apply elem_of_app.
+ - by apply not_elem_of_nil.
+ - by apply elem_of_list_singleton.
+ - intros [?] [?]. apply elem_of_app.
Qed.
Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
Proof.
@@ -50,24 +50,24 @@ Instance listset_filter: Filter A (listset A) := λ P _ l,
Instance: Collection A (listset A).
Proof.
split.
- * apply _.
- * intros [?] [?]. apply elem_of_list_intersection.
- * intros [?] [?]. apply elem_of_list_difference.
+ - apply _.
+ - intros [?] [?]. apply elem_of_list_intersection.
+ - intros [?] [?]. apply elem_of_list_difference.
Qed.
Instance listset_elems: Elements A (listset A) := remove_dups ∘ listset_car.
Global Instance: FinCollection A (listset A).
Proof.
split.
- * apply _.
- * intros. apply elem_of_remove_dups.
- * intros. apply NoDup_remove_dups.
+ - apply _.
+ - intros. apply elem_of_remove_dups.
+ - intros. apply NoDup_remove_dups.
Qed.
Global Instance: CollectionOps A (listset A).
Proof.
split.
- * apply _.
- * intros ? [?] [?]. apply elem_of_list_intersection_with.
- * intros [?] ??. apply elem_of_list_filter.
+ - apply _.
+ - intros ? [?] [?]. apply elem_of_list_intersection_with.
+ - intros [?] ??. apply elem_of_list_filter.
Qed.
End listset.
@@ -102,10 +102,10 @@ Instance listset_join: MJoin listset := λ A, mbind id.
Instance: CollectionMonad listset.
Proof.
split.
- * intros. apply _.
- * intros ??? [?] ?. apply elem_of_list_bind.
- * intros. apply elem_of_list_ret.
- * intros ??? [?]. apply elem_of_list_fmap.
- * intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
+ - intros. apply _.
+ - intros ??? [?] ?. apply elem_of_list_bind.
+ - intros. apply elem_of_list_ret.
+ - intros ??? [?]. apply elem_of_list_fmap.
+ - intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
simpl. by rewrite elem_of_list_bind.
Qed.
diff --git a/prelude/listset_nodup.v b/prelude/listset_nodup.v
index b1094d4533e7dda687dde6c962b05aa38b97f4a4..f6d9c1971f15712d76d62e3d4438ffaf33d1f009 100644
--- a/prelude/listset_nodup.v
+++ b/prelude/listset_nodup.v
@@ -39,11 +39,11 @@ Instance listset_nodup_filter: Filter A C := λ P _ l,
Instance: Collection A C.
Proof.
split; [split | | ].
- * by apply not_elem_of_nil.
- * by apply elem_of_list_singleton.
- * intros [??] [??] ?. apply elem_of_list_union.
- * intros [??] [??] ?. apply elem_of_list_intersection.
- * intros [??] [??] ?. apply elem_of_list_difference.
+ - by apply not_elem_of_nil.
+ - by apply elem_of_list_singleton.
+ - intros [??] [??] ?. apply elem_of_list_union.
+ - intros [??] [??] ?. apply elem_of_list_intersection.
+ - intros [??] [??] ?. apply elem_of_list_difference.
Qed.
Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
@@ -52,11 +52,11 @@ Proof. split. apply _. done. by intros [??]. Qed.
Global Instance: CollectionOps A C.
Proof.
split.
- * apply _.
- * intros ? [??] [??] ?. unfold intersection_with, elem_of,
+ - apply _.
+ - intros ? [??] [??] ?. unfold intersection_with, elem_of,
listset_nodup_intersection_with, listset_nodup_elem_of; simpl.
rewrite elem_of_remove_dups. by apply elem_of_list_intersection_with.
- * intros [??] ???. apply elem_of_list_filter.
+ - intros [??] ???. apply elem_of_list_filter.
Qed.
End list_collection.
diff --git a/prelude/mapset.v b/prelude/mapset.v
index e0f3dff018cdff898a2e084e665348d47711173a..d1c7425670a82e59ac224bf691489b7bb87bf15a 100644
--- a/prelude/mapset.v
+++ b/prelude/mapset.v
@@ -47,19 +47,19 @@ Proof. solve_decision. Defined.
Instance: Collection K (mapset M).
Proof.
split; [split | | ].
- * unfold empty, elem_of, mapset_empty, mapset_elem_of.
+ - unfold empty, elem_of, mapset_empty, mapset_elem_of.
simpl. intros. by simpl_map.
- * unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
+ - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
simpl. by split; intros; simplify_map_equality.
- * unfold union, elem_of, mapset_union, mapset_elem_of.
+ - unfold union, elem_of, mapset_union, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
destruct (m1 !! x) as [[]|]; tauto.
- * unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
+ - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
{ split; eauto. by intros [[] ?]. }
naive_solver.
- * unfold difference, elem_of, mapset_difference, mapset_elem_of.
+ - unfold difference, elem_of, mapset_difference, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
@@ -68,12 +68,12 @@ Proof. split; try apply _. intros ????. apply mapset_eq. intuition. Qed.
Global Instance: FinCollection K (mapset M).
Proof.
split.
- * apply _.
- * unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
+ - apply _.
+ - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
intros [m] x. simpl. rewrite elem_of_list_fmap. split.
+ intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
+ intros. exists (x, ()). by rewrite elem_of_map_to_list.
- * unfold elements, mapset_elems. intros [m]. simpl.
+ - unfold elements, mapset_elems. intros [m]. simpl.
apply NoDup_fst_map_to_list.
Qed.
@@ -101,8 +101,8 @@ Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
Proof.
unfold mapset_dom_with, elem_of, mapset_elem_of.
simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|].
- * destruct (Is_true_reflect (f a)); naive_solver.
- * naive_solver.
+ - destruct (Is_true_reflect (f a)); naive_solver.
+ - naive_solver.
Qed.
Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset M).
diff --git a/prelude/natmap.v b/prelude/natmap.v
index 9f7b0a5f53af629cd0877663b4517c2faf8e2e5b..c22f7993616ce3b76554b9cda342a621ac6687e7 100644
--- a/prelude/natmap.v
+++ b/prelude/natmap.v
@@ -160,15 +160,15 @@ Lemma natmap_elem_of_to_list_raw_aux {A} j (l : natmap_raw A) i x :
(i,x) ∈ natmap_to_list_raw j l ↔ ∃ i', i = i' + j ∧ mjoin (l !! i') = Some x.
Proof.
split.
- * revert j. induction l as [|[y|] l IH]; intros j; simpl.
+ - revert j. induction l as [|[y|] l IH]; intros j; simpl.
+ by rewrite elem_of_nil.
+ rewrite elem_of_cons. intros [?|?]; simplify_equality.
- - by exists 0.
- - destruct (IH (S j)) as (i'&?&?); auto.
+ * by exists 0.
+ * destruct (IH (S j)) as (i'&?&?); auto.
exists (S i'); simpl; auto with lia.
+ intros. destruct (IH (S j)) as (i'&?&?); auto.
exists (S i'); simpl; auto with lia.
- * intros (i'&?&Hi'). subst. revert i' j Hi'.
+ - intros (i'&?&Hi'). subst. revert i' j Hi'.
induction l as [|[y|] l IH]; intros i j ?; simpl.
+ done.
+ destruct i as [|i]; simplify_equality'; [left|].
@@ -210,7 +210,7 @@ Instance natmap_map: FMap natmap := λ A B f m,
Instance: FinMap nat natmap.
Proof.
split.
- * unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
+ - unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
apply natmap_eq. revert l2 Hl1 Hl2 E. simpl.
induction l1 as [|[x|] l1 IH]; intros [|[y|] l2] Hl1 Hl2 E; simpl in *.
+ done.
@@ -223,14 +223,14 @@ Proof.
+ destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
+ by specialize (E 0).
+ f_equal. apply IH; eauto using natmap_wf_inv. intros i. apply (E (S i)).
- * done.
- * intros ?? [??] ?. apply natmap_lookup_alter_raw.
- * intros ?? [??] ??. apply natmap_lookup_alter_raw_ne.
- * intros ??? [??] ?. apply natmap_lookup_map_raw.
- * intros ? [??]. by apply natmap_to_list_raw_nodup.
- * intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
- * intros ??? [??] ?. by apply natmap_lookup_omap_raw.
- * intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
+ - done.
+ - intros ?? [??] ?. apply natmap_lookup_alter_raw.
+ - intros ?? [??] ??. apply natmap_lookup_alter_raw_ne.
+ - intros ??? [??] ?. apply natmap_lookup_map_raw.
+ - intros ? [??]. by apply natmap_to_list_raw_nodup.
+ - intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
+ - intros ??? [??] ?. by apply natmap_lookup_omap_raw.
+ - intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
Qed.
Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=
@@ -353,8 +353,8 @@ Lemma natmap_push_pop {A} (m : natmap A) :
natmap_push (m !! 0) (natmap_pop m) = m.
Proof.
apply map_eq. intros i. destruct i.
- * by rewrite lookup_natmap_push_O.
- * by rewrite lookup_natmap_push_S, lookup_natmap_pop.
+ - by rewrite lookup_natmap_push_O.
+ - by rewrite lookup_natmap_push_S, lookup_natmap_pop.
Qed.
Lemma natmap_pop_push {A} o (m : natmap A) : natmap_pop (natmap_push o m) = m.
Proof. apply natmap_eq. by destruct o, m as [[|??]]. Qed.
diff --git a/prelude/nmap.v b/prelude/nmap.v
index 85d518d50f2ead89535480611ce37cbb62bbedd2..4854ad099a72445930a1f908a1c2a0f085d9cd02 100644
--- a/prelude/nmap.v
+++ b/prelude/nmap.v
@@ -49,34 +49,34 @@ Instance Nfmap: FMap Nmap := λ A B f t,
Instance: FinMap N Nmap.
Proof.
split.
- * intros ? [??] [??] H. f_equal; [apply (H 0)|].
+ - intros ? [??] [??] H. f_equal; [apply (H 0)|].
apply map_eq. intros i. apply (H (Npos i)).
- * by intros ? [|?].
- * intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
- * intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
+ - by intros ? [|?].
+ - intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
+ - intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
intros. apply lookup_partial_alter_ne. congruence.
- * intros ??? [??] []; simpl. done. apply lookup_fmap.
- * intros ? [[x|] t]; unfold map_to_list; simpl.
+ - intros ??? [??] []; simpl. done. apply lookup_fmap.
+ - intros ? [[x|] t]; unfold map_to_list; simpl.
+ constructor.
- - rewrite elem_of_list_fmap. by intros [[??] [??]].
- - by apply (NoDup_fmap _), NoDup_map_to_list.
+ * rewrite elem_of_list_fmap. by intros [[??] [??]].
+ * by apply (NoDup_fmap _), NoDup_map_to_list.
+ apply (NoDup_fmap _), NoDup_map_to_list.
- * intros ? t i x. unfold map_to_list. split.
+ - intros ? t i x. unfold map_to_list. split.
+ destruct t as [[y|] t]; simpl.
- - rewrite elem_of_cons, elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_list_fmap.
intros [? | [[??] [??]]]; simplify_equality'; [done |].
by apply elem_of_map_to_list.
- - rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
+ * rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
by apply elem_of_map_to_list.
+ destruct t as [[y|] t]; simpl.
- - rewrite elem_of_cons, elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_list_fmap.
destruct i as [|i]; simpl; [intuition congruence |].
intros. right. exists (i, x). by rewrite elem_of_map_to_list.
- - rewrite elem_of_list_fmap.
+ * rewrite elem_of_list_fmap.
destruct i as [|i]; simpl; [done |].
intros. exists (i, x). by rewrite elem_of_map_to_list.
- * intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
- * intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
+ - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
+ - intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
Qed.
(** * Finite sets *)
@@ -96,8 +96,8 @@ Instance Nset_fresh : Fresh N Nset := λ X,
Instance Nset_fresh_spec : FreshSpec N Nset.
Proof.
split.
- * apply _.
- * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
- * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+ - apply _.
+ - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+ - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
by rewrite Nfresh_fresh.
Qed.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 2c9cf5673342a55aefa273d5e7cf7c7e809fe41e..71ec892b677cbc702cc5af3289ad46a752f29357 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -45,10 +45,10 @@ Proof.
assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
y = y' → eq_dep nat (le x) y p y' q) as aux.
{ fix 3. intros x ? [|y p] ? [|y' q].
- * done.
- * clear nat_le_pi. intros; exfalso; auto with lia.
- * clear nat_le_pi. intros; exfalso; auto with lia.
- * injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
+ - done.
+ - clear nat_le_pi. intros; exfalso; auto with lia.
+ - clear nat_le_pi. intros; exfalso; auto with lia.
+ - injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
intros x y p q.
by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Qed.
@@ -153,8 +153,8 @@ Proof.
cut (∀ p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1).
{ by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
- * apply (IH _ (_~1)).
- * apply (IH _ (_~0)).
+ - apply (IH _ (_~1)).
+ - apply (IH _ (_~0)).
Qed.
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
Proof. unfold Preverse. by rewrite Preverse_go_app. Qed.
@@ -283,11 +283,11 @@ Qed.
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
Proof.
split.
- * rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
+ - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
destruct (decide (0 ≤ i)%Z).
{ by rewrite Z2Nat.inj_mul, Nat2Z.id by lia. }
by rewrite !Z_to_nat_nonpos by auto using Z.mul_nonpos_nonneg with lia.
- * intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
+ - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Qed.
Lemma Z2Nat_divide n m :
0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
@@ -360,8 +360,8 @@ Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y.
Proof.
split; intros.
- * by apply Qcplus_le_compat.
- * replace x with ((0 - z) + (z + x)) by ring.
+ - by apply Qcplus_le_compat.
+ - replace x with ((0 - z) + (z + x)) by ring.
replace y with ((0 - z) + (z + y)) by ring.
by apply Qcplus_le_compat.
Qed.
diff --git a/prelude/option.v b/prelude/option.v
index ac0b1ed7104f593ac9668f62a17f263f0c353236..131150a31bbdba317e56916095f3b44131cace53 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -94,9 +94,9 @@ Section setoids.
Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
Proof.
split.
- * by intros []; constructor.
- * by destruct 1; constructor.
- * destruct 1; inversion 1; constructor; etransitivity; eauto.
+ - by intros []; constructor.
+ - by destruct 1; constructor.
+ - destruct 1; inversion 1; constructor; etransitivity; eauto.
Qed.
Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
Proof. by constructor. Qed.
diff --git a/prelude/orders.v b/prelude/orders.v
index 100ae33527bcc9b58d413ace322ad3564a6d0466..2f01940f1a627efc18470cfeaf7e274c8e97e43b 100644
--- a/prelude/orders.v
+++ b/prelude/orders.v
@@ -49,8 +49,8 @@ Section orders.
Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠Y.
Proof.
split.
- * intros [? HYX]. split. done. by intros <-.
- * intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
+ - intros [? HYX]. split. done. by intros <-.
+ - intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
Qed.
Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} (X Y : A) :
Decision (X = Y).
@@ -242,8 +242,8 @@ Section merge_sort_correct.
revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
repeat case_decide; auto.
- * by rewrite (right_id_L [] (++)).
- * by rewrite IH2, Permutation_middle.
+ - by rewrite (right_id_L [] (++)).
+ - by rewrite IH2, Permutation_middle.
Qed.
Local Notation stack := (list (option (list A))).
@@ -292,8 +292,8 @@ Section merge_sort_correct.
merge_sort_aux R st l ≡ₚ merge_stack_flatten st ++ l.
Proof.
revert st. induction l as [|?? IH]; simpl; intros.
- * by rewrite (right_id_L [] (++)), merge_stack_Permutation.
- * rewrite IH, merge_list_to_stack_Permutation; simpl.
+ - by rewrite (right_id_L [] (++)), merge_stack_Permutation.
+ - rewrite IH, merge_list_to_stack_Permutation; simpl.
by rewrite Permutation_middle.
Qed.
Lemma Sorted_merge_sort l : Sorted R (merge_sort R l).
@@ -317,21 +317,21 @@ Section preorder.
Instance preorder_equivalence: @Equivalence A (≡).
Proof.
split.
- * done.
- * by intros ?? [??].
- * by intros X Y Z [??] [??]; split; transitivity Y.
+ - done.
+ - by intros ?? [??].
+ - by intros X Y Z [??] [??]; split; transitivity Y.
Qed.
Global Instance: Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation A).
Proof.
unfold equiv, preorder_equiv. intros X1 Y1 ? X2 Y2 ?. split; intro.
- * transitivity X1. tauto. transitivity X2; tauto.
- * transitivity Y1. tauto. transitivity Y2; tauto.
+ - transitivity X1. tauto. transitivity X2; tauto.
+ - transitivity Y1. tauto. transitivity Y2; tauto.
Qed.
Lemma subset_spec (X Y : A) : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
Proof.
split.
- * intros [? HYX]. split. done. contradict HYX. by rewrite <-HYX.
- * intros [? HXY]. split. done. by contradict HXY.
+ - intros [? HYX]. split. done. contradict HYX. by rewrite <-HYX.
+ - intros [? HXY]. split. done. by contradict HXY.
Qed.
Section dec.
@@ -435,15 +435,15 @@ Section join_semi_lattice.
Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
Proof.
split.
- * intros HXY. split; apply equiv_empty;
+ - intros HXY. split; apply equiv_empty;
by transitivity (X ∪ Y); [auto | rewrite HXY].
- * intros [HX HY]. by rewrite HX, HY, (left_id _ _).
+ - intros [HX HY]. by rewrite HX, HY, (left_id _ _).
Qed.
Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
Proof.
split.
- * induction Xs; simpl; rewrite ?empty_union; intuition.
- * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
+ - induction Xs; simpl; rewrite ?empty_union; intuition.
+ - induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
Qed.
Section leibniz.
@@ -562,20 +562,20 @@ Section lattice.
split; [apply union_least|apply lattice_distr].
{ apply intersection_greatest; auto using union_subseteq_l. }
apply intersection_greatest.
- * apply union_subseteq_r_transitive, intersection_subseteq_l.
- * apply union_subseteq_r_transitive, intersection_subseteq_r.
+ - apply union_subseteq_r_transitive, intersection_subseteq_l.
+ - apply union_subseteq_r_transitive, intersection_subseteq_r.
Qed.
Lemma union_intersection_r (X Y Z : A) : (X ∩ Y) ∪ Z ≡ (X ∪ Z) ∩ (Y ∪ Z).
Proof. by rewrite !(comm _ _ Z), union_intersection_l. Qed.
Lemma intersection_union_l (X Y Z : A) : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z).
Proof.
split.
- * rewrite union_intersection_l.
+ - rewrite union_intersection_l.
apply intersection_greatest.
{ apply union_subseteq_r_transitive, intersection_subseteq_l. }
rewrite union_intersection_r.
apply intersection_preserving; auto using union_subseteq_l.
- * apply intersection_greatest.
+ - apply intersection_greatest.
{ apply union_least; auto using intersection_subseteq_l. }
apply union_least.
+ apply intersection_subseteq_r_transitive, union_subseteq_l.
diff --git a/prelude/pmap.v b/prelude/pmap.v
index 700b3df162754d74c8db018ca1123161f97a6adf..5796e4f78d28605ff3dbb0ad02f654e0e95abc86 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -117,9 +117,9 @@ Lemma Pmap_wf_eq {A} (t1 t2 : Pmap_raw A) :
Proof.
revert t2.
induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
- * discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
- * discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
- * f_equal; [apply (Ht 1)| |].
+ - discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
+ - discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
+ - f_equal; [apply (Ht 1)| |].
+ apply IHl; try apply (λ x, Ht (x~0)); eauto.
+ apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.
@@ -133,8 +133,8 @@ Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
Pmap_wf t → Pmap_wf (Ppartial_alter_raw f i t).
Proof.
revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
- * destruct (f None); auto using Psingleton_wf.
- * destruct i; simpl; eauto.
+ - destruct (f None); auto using Psingleton_wf.
+ - destruct i; simpl; eauto.
Qed.
Lemma Pfmap_wf {A B} (f : A → B) t : Pmap_wf t → Pmap_wf (Pfmap_raw f t).
Proof.
@@ -157,15 +157,15 @@ Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
Ppartial_alter_raw f i t !! i = f (t !! i).
Proof.
revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
- * by destruct (f None); rewrite ?Plookup_singleton.
- * destruct i; simpl; rewrite PNode_lookup; simpl; auto.
+ - by destruct (f None); rewrite ?Plookup_singleton.
+ - destruct i; simpl; rewrite PNode_lookup; simpl; auto.
Qed.
Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
i ≠j → Ppartial_alter_raw f i t !! j = t !! j.
Proof.
revert i j; induction t as [|o l IHl r IHr]; simpl.
- * by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
- * by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
+ - by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
+ - by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
Qed.
Lemma Plookup_fmap {A B} (f : A → B) t i : (Pfmap_raw f t) !! i = f <$> t !! i.
Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
@@ -175,14 +175,14 @@ Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
Proof.
split.
{ revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
- * by right.
- * rewrite elem_of_cons. intros [?|?]; simplify_equality.
+ - by right.
+ - rewrite elem_of_cons. intros [?|?]; simplify_equality.
{ left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
{ left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
- * intros.
+ - intros.
destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
{ left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
@@ -193,14 +193,14 @@ Proof.
simpl; rewrite ?elem_of_cons; auto. }
intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
induction t as [|[y|] l IHl r IHr]; intros j i acc ?; simpl.
- * done.
- * rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
+ - done.
+ - rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
+ right. apply help. specialize (IHr (j~1) i).
rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ right. specialize (IHl (j~0) i).
rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+ left. by rewrite (left_id_L 1 (++))%positive.
- * destruct i as [i|i|]; simplify_equality'.
+ - destruct i as [i|i|]; simplify_equality'.
+ apply help. specialize (IHr (j~1) i).
rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ specialize (IHl (j~0) i).
@@ -211,8 +211,8 @@ Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
NoDup acc → NoDup (Pto_list_raw j t acc).
Proof.
revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
- * done.
- * repeat constructor.
+ - done.
+ - repeat constructor.
{ rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
{ apply (f_equal Plength) in Hi.
rewrite Preverse_xO, !Papp_length in Hi; simpl in *; lia. }
@@ -221,20 +221,20 @@ Proof.
rewrite Preverse_xI, !Papp_length in Hi; simpl in *; lia. }
specialize (Hin 1 y). rewrite (left_id_L 1 (++))%positive in Hin.
discriminate (Hin Hj). }
- apply IHl.
- { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
- + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
- by apply (inj (++ _)) in Hi.
- + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
- apply IHr; auto. intros i x Hi.
- apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
- * apply IHl.
- { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
- + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
- by apply (inj (++ _)) in Hi.
- + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
- apply IHr; auto. intros i x Hi.
- apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+ apply IHl.
+ { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+ by apply (inj (++ _)) in Hi.
+ + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+ apply IHr; auto. intros i x Hi.
+ apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+ - apply IHl.
+ { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+ by apply (inj (++ _)) in Hi.
+ + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+ apply IHr; auto. intros i x Hi.
+ apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
Qed.
Lemma Pomap_lookup {A B} (f : A → option B) t i :
Pomap_raw f t !! i = t !! i ≫= f.
@@ -250,9 +250,9 @@ Proof.
{ rewrite Pomap_lookup. by destruct (t2 !! i). }
unfold compose, flip.
destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
- * by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
+ - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
match goal with |- ?o ≫= _ = _ => destruct o end.
- * destruct i; rewrite ?Pomap_lookup; simpl; auto.
+ - destruct i; rewrite ?Pomap_lookup; simpl; auto.
Qed.
(** Packed version and instance of the finite map type class *)
@@ -288,18 +288,18 @@ Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
Instance Pmap_finmap : FinMap positive Pmap.
Proof.
split.
- * by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
- * by intros ? [].
- * intros ?? [??] ?. by apply Plookup_alter.
- * intros ?? [??] ??. by apply Plookup_alter_ne.
- * intros ??? [??]. by apply Plookup_fmap.
- * intros ? [??]. apply Pto_list_nodup; [|constructor].
+ - by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
+ - by intros ? [].
+ - intros ?? [??] ?. by apply Plookup_alter.
+ - intros ?? [??] ??. by apply Plookup_alter_ne.
+ - intros ??? [??]. by apply Plookup_fmap.
+ - intros ? [??]. apply Pto_list_nodup; [|constructor].
intros ??. by rewrite elem_of_nil.
- * intros ? [??] i x; unfold map_to_list, Pto_list.
+ - intros ? [??] i x; unfold map_to_list, Pto_list.
rewrite Pelem_of_to_list, elem_of_nil.
split. by intros [(?&->&?)|]. by left; exists i.
- * intros ?? ? [??] ?. by apply Pomap_lookup.
- * intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
+ - intros ?? ? [??] ?. by apply Pomap_lookup.
+ - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
Qed.
(** * Finite sets *)
@@ -365,8 +365,8 @@ Instance Pset_fresh : Fresh positive Pset := λ X,
Instance Pset_fresh_spec : FreshSpec positive Pset.
Proof.
split.
- * apply _.
- * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
- * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+ - apply _.
+ - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+ - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
by rewrite Pfresh_fresh.
Qed.
diff --git a/prelude/relations.v b/prelude/relations.v
index 776da9914d86a464472a2fad2074911705932764..bf964b8feb46a84d555cec438c10c87a13e3b46a 100644
--- a/prelude/relations.v
+++ b/prelude/relations.v
@@ -142,9 +142,9 @@ Section rtc.
intros n p1 H. rewrite <-plus_n_Sm.
apply (IH (S n)); [by eauto using bsteps_r |].
intros [|m'] [??]; [lia |]. apply Pstep with x'.
- * apply bsteps_weaken with n; intuition lia.
- * done.
- * apply H; intuition lia.
+ - apply bsteps_weaken with n; intuition lia.
+ - done.
+ - apply H; intuition lia.
Qed.
Lemma tc_transitive x y z : tc R x y → tc R y z → tc R x z.
diff --git a/prelude/streams.v b/prelude/streams.v
index cb8a1590304145d682fac5769b15e4f86c4ca230..30959748e8337fc8f2d6f5292187c54c32fc9f77 100644
--- a/prelude/streams.v
+++ b/prelude/streams.v
@@ -40,9 +40,9 @@ Proof. by constructor. Qed.
Global Instance equal_equivalence : Equivalence (@equiv (stream A) _).
Proof.
split.
- * now cofix; intros [??]; constructor.
- * now cofix; intros ?? [??]; constructor.
- * cofix; intros ??? [??] [??]; constructor; etransitivity; eauto.
+ - now cofix; intros [??]; constructor.
+ - now cofix; intros ?? [??]; constructor.
+ - cofix; intros ??? [??] [??]; constructor; etransitivity; eauto.
Qed.
Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).
Proof. by constructor. Qed.
diff --git a/prelude/vector.v b/prelude/vector.v
index b39ca4e45cab9ce9479562bf2ab4c16be6d29964..084fe0be0024be8bf598329a7cb3853f92adea37 100644
--- a/prelude/vector.v
+++ b/prelude/vector.v
@@ -87,8 +87,8 @@ Fixpoint fin_enum (n : nat) : list (fin n) :=
Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Next Obligation.
intros n. induction n; simpl; constructor.
- * rewrite elem_of_list_fmap. by intros (?&?&?).
- * by apply (NoDup_fmap _).
+ - rewrite elem_of_list_fmap. by intros (?&?&?).
+ - by apply (NoDup_fmap _).
Qed.
Next Obligation.
intros n i. induction i as [|n i IH]; simpl;
@@ -148,8 +148,8 @@ Proof. apply vcons_inj. Qed.
Lemma vec_eq {A n} (v w : vec A n) : (∀ i, v !!! i = w !!! i) → v = w.
Proof.
vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal.
- * apply (Hi 0%fin).
- * apply IH. intros i. apply (Hi (FS i)).
+ - apply (Hi 0%fin).
+ - apply IH. intros i. apply (Hi (FS i)).
Qed.
Instance vec_dec {A} {dec : ∀ x y : A, Decision (x = y)} {n} :
@@ -238,8 +238,8 @@ Proof.
rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
pose proof (vec_to_list_inj1 _ _ H); subst.
apply vec_to_list_inj2 in H; subst. induction l. simpl.
- * eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
- * destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
+ - eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
+ - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
Qed.
Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
drop i v = v !!! i :: drop (S i) v.
@@ -252,10 +252,10 @@ Lemma elem_of_vlookup {A n} (v : vec A n) x :
x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
Proof.
split.
- * induction v; simpl; [by rewrite elem_of_nil |].
+ - induction v; simpl; [by rewrite elem_of_nil |].
inversion 1; subst; [by eexists 0%fin|].
destruct IHv as [i ?]; trivial. by exists (FS i).
- * intros [i ?]; subst. induction v as [|??? IH]; inv_fin i; [by left|].
+ - intros [i ?]; subst. induction v as [|??? IH]; inv_fin i; [by left|].
right; apply IH.
Qed.
Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
@@ -275,10 +275,10 @@ Lemma Forall2_vlookup {A B} (P : A → B → Prop) {n}
Forall2 P (vec_to_list v1) (vec_to_list v2) ↔ ∀ i, P (v1 !!! i) (v2 !!! i).
Proof.
split.
- * vec_double_ind v1 v2; [intros _ i; inv_fin i |].
+ - vec_double_ind v1 v2; [intros _ i; inv_fin i |].
intros n v1 v2 IH a b; simpl. inversion_clear 1.
intros i. inv_fin i; simpl; auto.
- * vec_double_ind v1 v2; [constructor|].
+ - vec_double_ind v1 v2; [constructor|].
intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
Qed.
diff --git a/prelude/zmap.v b/prelude/zmap.v
index ebffda33390616d1987ba64cc3d0da9a40525f65..59503550a0885a355946e1275f2d6f4e555711c9 100644
--- a/prelude/zmap.v
+++ b/prelude/zmap.v
@@ -52,16 +52,16 @@ Instance Nfmap: FMap Zmap := λ A B f t,
Instance: FinMap Z Zmap.
Proof.
split.
- * intros ? [??] [??] H. f_equal.
+ - intros ? [??] [??] H. f_equal.
+ apply (H 0).
+ apply map_eq. intros i. apply (H (Zpos i)).
+ apply map_eq. intros i. apply (H (Zneg i)).
- * by intros ? [].
- * intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter.
- * intros ? f [] [|?|?] [|?|?]; simpl; intuition congruence ||
+ - by intros ? [].
+ - intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter.
+ - intros ? f [] [|?|?] [|?|?]; simpl; intuition congruence ||
intros; apply lookup_partial_alter_ne; congruence.
- * intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
- * intros ? [o t t']; unfold map_to_list; simpl.
+ - intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
+ - intros ? [o t t']; unfold map_to_list; simpl.
assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
prod_map Z.neg id <$> map_to_list t')).
{ apply NoDup_app; split_ands.
@@ -70,24 +70,24 @@ Proof.
- apply (NoDup_fmap_2 _), NoDup_map_to_list. }
destruct o; simpl; auto. constructor; auto.
rewrite elem_of_app, !elem_of_list_fmap. naive_solver.
- * intros ? t i x. unfold map_to_list. split.
+ - intros ? t i x. unfold map_to_list. split.
+ destruct t as [[y|] t t']; simpl.
- - rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
intros [?|[[[??][??]]|[[??][??]]]]; simplify_equality'; [done| |];
by apply elem_of_map_to_list.
- - rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
+ * rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
simplify_equality'; by apply elem_of_map_to_list.
+ destruct t as [[y|] t t']; simpl.
- - rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
destruct i as [|i|i]; simpl; [intuition congruence| |].
{ right; left. exists (i, x). by rewrite elem_of_map_to_list. }
right; right. exists (i, x). by rewrite elem_of_map_to_list.
- - rewrite elem_of_app, !elem_of_list_fmap.
+ * rewrite elem_of_app, !elem_of_list_fmap.
destruct i as [|i|i]; simpl; [done| |].
{ left; exists (i, x). by rewrite elem_of_map_to_list. }
right; exists (i, x). by rewrite elem_of_map_to_list.
- * intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
- * intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
+ - intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
+ - intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
Qed.
(** * Finite sets *)
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index e36aa14a529b88ea3e4e694e5b799ed77d2c41e3..caa5cc9b7258882180efbf3fd55d7b21fea42aa0 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -36,7 +36,7 @@ Proof.
destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
revert Hwsat; rewrite big_op_app right_id_L=>Hwsat.
destruct ef as [e'|].
- * destruct (IH (Qs1 ++ Q :: Qs2 ++ [λ _, True%I])
+ - destruct (IH (Qs1 ++ Q :: Qs2 ++ [λ _, True%I])
(rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Qs'&?&?).
{ apply Forall3_app, Forall3_cons,
Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. }
@@ -44,7 +44,7 @@ Proof.
(comm (++)) /= assoc big_op_app. }
exists rs', ([λ _, True%I] ++ Qs'); split; auto.
by rewrite (assoc _ _ _ Qs') -(assoc _ Qs1).
- * apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
+ - apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 â‹… r2' :: rs2)).
{ rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le.
apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
@@ -73,9 +73,9 @@ Proof.
eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
{ by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_ands.
- * by rewrite Res_op ?left_id ?right_id.
- * by rewrite /uPred_holds /=.
- * by apply ownG_spec.
+ - by rewrite Res_op ?left_id ?right_id.
+ - by rewrite /uPred_holds /=.
+ - by apply ownG_spec.
Qed.
Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
✓ m →
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index de694e3994d17dd6720a09d59f99c35b690ec708..62578f262065005aa615188e8aa4bdb8a8edb146 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -54,9 +54,9 @@ Instance inG_empty_spec `{Empty A} :
CMRAIdentity A → CMRAIdentity (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))).
Proof.
split.
- * apply cmra_transport_valid, cmra_empty_valid.
- * intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
- * apply _.
+ - apply cmra_transport_valid, cmra_empty_valid.
+ - intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
+ - apply _.
Qed.
(** * Properties of own *)
@@ -91,10 +91,10 @@ Lemma own_alloc_strong a E (G : gset gname) :
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■(∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
- * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty inG_id);
+ - eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty inG_id);
first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
naive_solver.
- * apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
+ - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv.
Qed.
Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own γ a).
@@ -108,10 +108,10 @@ Lemma own_updateP P γ a E :
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■(∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
- * eapply pvs_ownG_updateP, iprod_singleton_updateP;
+ - eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
naive_solver.
- * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
+ - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.
@@ -120,10 +120,10 @@ Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
Proof.
intros Hemp.
rewrite -(pvs_mono _ _ (∃ m, ■(∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
- * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
+ - eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
naive_solver.
- * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
+ - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index dfc971bb65bb9e1c7e1bc7a29d21d9b40023b618..48100a9d90311939a7ef34cdcd5fce0299d82557 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -62,11 +62,11 @@ Proof.
apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
apply and_intro; [|apply and_intro; [|done]].
- * rewrite -vs_impl; apply (always_intro _ _),impl_intro_l; rewrite and_elim_l.
+ - rewrite -vs_impl; apply (always_intro _ _),impl_intro_l; rewrite and_elim_l.
rewrite !assoc; apply sep_mono; last done.
rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
by repeat apply and_intro; try apply const_intro.
- * apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
+ - apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
rewrite -(of_to_val e2 v) // -wp_value'; [].
rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
@@ -110,10 +110,10 @@ Proof.
intros ? Hsafe Hdet.
rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
- * apply (always_intro' _ _), impl_intro_l.
+ - apply (always_intro' _ _), impl_intro_l.
rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
by rewrite /ht always_elim impl_elim_r.
- * destruct ef' as [e'|]; simpl; [|by apply const_intro].
+ - destruct ef' as [e'|]; simpl; [|by apply const_intro].
apply (always_intro _ _), impl_intro_l.
rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
by rewrite /= /ht always_elim impl_elim_r.
diff --git a/program_logic/model.v b/program_logic/model.v
index d4f3eb610c981410bf13263ad66528bc4aff8bf2..037d39b32a70be69bdfe6766a15b6e88a8d030bd 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -17,14 +17,14 @@ Definition map {Λ : language} {Σ : iFunctor} {A1 A2 B1 B2 : cofeT}
Definition result Λ Σ : solution (F Λ Σ).
Proof.
apply (solver.result _ (@map Λ Σ)).
- * intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
+ - intros A B P. rewrite /map /= -{2}(uPred_map_id P). apply uPred_map_ext=> r.
rewrite /= -{2}(res_map_id r); apply res_map_ext=>{r} r /=.
by rewrite later_map_id.
- * intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
+ - intros A1 A2 A3 B1 B2 B3 f g f' g' P. rewrite /map /=.
rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
by rewrite -later_map_compose.
- * intros A1 A2 B1 B2 n f f' Hf P [???].
+ - intros A1 A2 B1 B2 n f f' Hf P [???].
apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
by intros i ?; apply Hf.
Qed.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index c13c8fea387a372421012a4097e30a31400ab7ca..2f96898b78eb1b0b98126342a70fe8cab9277481 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -72,10 +72,10 @@ Lemma ownI_spec r n i P :
(ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))).
Proof.
intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
- * intros [(P'&Hi&HP) _]; rewrite Hi.
+ - intros [(P'&Hi&HP) _]; rewrite Hi.
by apply Some_dist, symmetry, agree_valid_includedN,
(cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
- * intros ?; split_ands; try apply cmra_empty_leastN; eauto.
+ - intros ?; split_ands; try apply cmra_empty_leastN; eauto.
Qed.
Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡{n}≡ Excl σ.
Proof.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 1bc285f97a079412b5fcd51d38fddfe1650d58ed..41d2b5e188f69c06cd57d90b66889336aa8d7b13 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -92,10 +92,10 @@ Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
Proof.
intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
rewrite left_id; apply wsat_close with P r.
- * apply ownI_spec, uPred_weaken with r (S n); auto.
- * solve_elem_of +HE.
- * by rewrite -(left_id_L ∅ (∪) Ef).
- * apply uPred_weaken with r n; auto.
+ - apply ownI_spec, uPred_weaken with r (S n); auto.
+ - solve_elem_of +HE.
+ - by rewrite -(left_id_L ∅ (∪) Ef).
+ - apply uPred_weaken with r n; auto.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■P m' ∧ ownG m').
diff --git a/program_logic/resources.v b/program_logic/resources.v
index a868bdf7c829fc1b2f8cb6651f19c8aa8460de2c..c64a460620da38d6a5ba77d1c8caccf77e847e15 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -53,15 +53,15 @@ Instance res_compl : Compl (res Λ Σ A) := λ c,
Definition res_cofe_mixin : CofeMixin (res Λ Σ A).
Proof.
split.
- * intros w1 w2; split.
+ - intros w1 w2; split.
+ by destruct 1; constructor; apply equiv_dist.
+ by intros Hw; constructor; apply equiv_dist=>n; destruct (Hw n).
- * intros n; split.
+ - intros n; split.
+ done.
+ by destruct 1; constructor.
+ do 2 destruct 1; constructor; etransitivity; eauto.
- * by destruct 1; constructor; apply dist_S.
- * intros c n; constructor.
+ - by destruct 1; constructor; apply dist_S.
+ - intros c n; constructor.
+ apply (conv_compl (chain_map wld c) n).
+ apply (conv_compl (chain_map pst c) n).
+ apply (conv_compl (chain_map gst c) n).
@@ -97,21 +97,21 @@ Qed.
Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
Proof.
split.
- * by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
- * by intros n [???] ? [???]; constructor; simpl in *; cofe_subst.
- * by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
- * by intros n [???] ? [???] [???] ? [???];
+ - by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
+ - by intros n [???] ? [???]; constructor; simpl in *; cofe_subst.
+ - by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
+ - by intros n [???] ? [???] [???] ? [???];
constructor; simpl in *; cofe_subst.
- * by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
- * by intros ???; constructor; rewrite /= assoc.
- * by intros ??; constructor; rewrite /= comm.
- * by intros ?; constructor; rewrite /= cmra_unit_l.
- * by intros ?; constructor; rewrite /= cmra_unit_idemp.
- * intros n r1 r2; rewrite !res_includedN.
+ - by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
+ - by intros ???; constructor; rewrite /= assoc.
+ - by intros ??; constructor; rewrite /= comm.
+ - by intros ?; constructor; rewrite /= cmra_unit_l.
+ - by intros ?; constructor; rewrite /= cmra_unit_idemp.
+ - intros n r1 r2; rewrite !res_includedN.
by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
- * intros n r1 r2 (?&?&?);
+ - intros n r1 r2 (?&?&?);
split_ands'; simpl in *; eapply cmra_validN_op_l; eauto.
- * intros n r1 r2; rewrite res_includedN; intros (?&?&?).
+ - intros n r1 r2; rewrite res_includedN; intros (?&?&?).
by constructor; apply cmra_op_minus.
Qed.
Definition res_cmra_extend_mixin : CMRAExtendMixin (res Λ Σ A).
@@ -127,9 +127,9 @@ Canonical Structure resRA : cmraT :=
Global Instance res_cmra_identity : CMRAIdentity resRA.
Proof.
split.
- * intros n; split_ands'; apply cmra_empty_valid.
- * by split; rewrite /= left_id.
- * apply _.
+ - intros n; split_ands'; apply cmra_empty_valid.
+ - by split; rewrite /= left_id.
+ - apply _.
Qed.
Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
@@ -179,34 +179,34 @@ Proof. by intros Hf n [] ? [???]; constructor; simpl in *; cofe_subst. Qed.
Lemma res_map_id {Λ Σ A} (r : res Λ Σ A) : res_map cid r ≡ r.
Proof.
constructor; simpl; [|done|].
- * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
+ - rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
by rewrite -{2}(agree_map_id y); apply agree_map_ext.
- * rewrite -{2}(option_fmap_id (gst r)); apply option_fmap_setoid_ext=> m /=.
+ - rewrite -{2}(option_fmap_id (gst r)); apply option_fmap_setoid_ext=> m /=.
by rewrite -{2}(ifunctor_map_id Σ m); apply ifunctor_map_ext.
Qed.
Lemma res_map_compose {Λ Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Λ Σ A) :
res_map (g ◎ f) r ≡ res_map g (res_map f r).
Proof.
constructor; simpl; [|done|].
- * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
+ - rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
by rewrite -agree_map_compose; apply agree_map_ext.
- * rewrite -option_fmap_compose; apply option_fmap_setoid_ext=> m /=.
+ - rewrite -option_fmap_compose; apply option_fmap_setoid_ext=> m /=.
by rewrite -ifunctor_map_compose; apply ifunctor_map_ext.
Qed.
Lemma res_map_ext {Λ Σ A B} (f g : A -n> B) (r : res Λ Σ A) :
(∀ x, f x ≡ g x) → res_map f r ≡ res_map g r.
Proof.
intros Hfg; split; simpl; auto.
- * by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
- * by apply option_fmap_setoid_ext=>m; apply ifunctor_map_ext.
+ - by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
+ - by apply option_fmap_setoid_ext=>m; apply ifunctor_map_ext.
Qed.
Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
CMRAMonotone (@res_map Λ Σ _ _ f).
Proof.
split.
- * by intros n r1 r2; rewrite !res_includedN;
+ - by intros n r1 r2; rewrite !res_includedN;
intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
- * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
+ - by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
Qed.
Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).
@@ -214,8 +214,8 @@ Instance resC_map_ne {Λ Σ A B} n :
Proper (dist n ==> dist n) (@resC_map Λ Σ A B).
Proof.
intros f g Hfg r; split; simpl; auto.
- * by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
- * by apply optionC_map_ne, ifunctor_map_ne.
+ - by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
+ - by apply optionC_map_ne, ifunctor_map_ne.
Qed.
Program Definition resF {Λ Σ} : iFunctor := {|
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index e7c84c044a8c79a3062c9ef3b176228a4fcf6ae4..137aa6adb9d9b68658b170adc4b033142067ea8e 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -41,8 +41,8 @@ Next Obligation.
intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
destruct 1 as [|n1 r1 e1 ? Hgo].
- * constructor; eauto using uPred_weaken.
- * intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
+ - constructor; eauto using uPred_weaken.
+ - intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep];
rewrite ?assoc -?Hr; auto; constructor; [done|].
intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
@@ -143,8 +143,8 @@ Proof.
apply pvs_trans in Hvs'; auto.
destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto.
exists r3, r2'; split_ands; last done.
- * by rewrite -assoc.
- * constructor; apply pvs_intro; auto.
+ - by rewrite -assoc.
+ - constructor; apply pvs_intro; auto.
Qed.
Lemma wp_frame_r E e Q R : (wp E e Q ★ R) ⊑ wp E e (λ v, Q v ★ R).
Proof.
@@ -159,9 +159,9 @@ Proof.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_ands; auto.
- * by rewrite -(assoc _ r2)
+ - by rewrite -(assoc _ r2)
(comm _ rR) !assoc -(assoc _ _ rR).
- * apply IH; eauto using uPred_weaken.
+ - apply IH; eauto using uPred_weaken.
Qed.
Lemma wp_frame_later_r E e Q R :
to_val e = None → (wp E e Q ★ ▷ R) ⊑ wp E e (λ v, Q v ★ R).
@@ -173,9 +173,9 @@ Proof.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_ands; auto.
- * by rewrite -(assoc _ r2)
+ - by rewrite -(assoc _ r2)
(comm _ rR) !assoc -(assoc _ _ rR).
- * apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
+ - apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
eapply uPred_weaken with rR n; eauto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Q :
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index d25dbd25c30377403ea91f8890bfd8466f03d858..7fa49e5cd91d551282d86a754e8c125da5130b48 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -71,11 +71,11 @@ Qed.
Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) mm).
Proof.
intros Hv. exists ∅; constructor; auto.
- * rewrite big_opM_empty right_id.
+ - rewrite big_opM_empty right_id.
split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
constructor || apply Hv.
- * by intros i; rewrite lookup_empty=>-[??].
- * intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
+ - by intros i; rewrite lookup_empty=>-[??].
+ - intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Qed.
Lemma wsat_open n E σ r i P :
wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
@@ -86,9 +86,9 @@ Proof.
assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_delete. }
exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto.
- * intros j; rewrite lookup_delete_is_Some Hr.
+ - intros j; rewrite lookup_delete_is_Some Hr.
generalize (HE j); solve_elem_of +Hi.
- * intros j P'; rewrite Hr=> Hj ?.
+ - intros j P'; rewrite Hr=> Hj ?.
setoid_rewrite lookup_delete_ne; last (solve_elem_of +Hi Hj).
apply Hwld; [solve_elem_of +Hj|done].
Qed.
@@ -101,10 +101,10 @@ Proof.
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
- * intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ - intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ rewrite !lookup_op HiP !op_is_Some; solve_elem_of +.
+ destruct (HE j) as [Hj Hj']; auto; solve_elem_of +Hj Hj'.
- * intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
+ - intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
+ rewrite !lookup_wld_op_l ?HiP; auto=> HP.
apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
exists rP; split; [rewrite lookup_insert|apply HP]; auto.
@@ -154,17 +154,17 @@ Proof.
assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
- * destruct Hval as (?&?&?); rewrite -assoc Hr.
+ - destruct Hval as (?&?&?); rewrite -assoc Hr.
split_ands'; rewrite /= ?left_id; [|eauto|eauto].
intros j; destruct (decide (j = i)) as [->|].
+ by rewrite !lookup_op Hri HrPi Hrsi !right_id lookup_singleton.
+ by rewrite lookup_op lookup_singleton_ne // left_id.
- * by rewrite -assoc Hr /= left_id.
- * intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
+ - by rewrite -assoc Hr /= left_id.
+ - intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
+ rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi.
+ rewrite lookup_insert_ne //.
rewrite lookup_op lookup_singleton_ne // left_id; eauto.
- * intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
+ - intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
+ rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
exists rP; rewrite lookup_insert; split; [|apply HP]; auto.