From 6d2f758b3b440ffd450b8247e94b4c61401d0818 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 4 Nov 2020 11:05:49 -0600
Subject: [PATCH] Address review feedback
---
theories/algebra/cmra.v | 10 +++++-----
theories/algebra/coPset.v | 2 +-
theories/algebra/gmultiset.v | 5 ++++-
theories/algebra/ofe.v | 4 +++-
theories/bi/derived_laws.v | 8 ++++----
theories/bi/derived_laws_later.v | 2 +-
theories/bi/monpred.v | 20 ++++++++++++++++----
7 files changed, 34 insertions(+), 17 deletions(-)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b1304e739..4a7325f8b 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1425,7 +1425,7 @@ Section option.
Instance option_unit : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
- Proof. split; [ done | by intros [] | done ]. Qed.
+ Proof. split; [done| |done]. by intros []. Qed.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
(** Misc *)
@@ -1456,13 +1456,13 @@ Section option.
Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
✓{n} (Some a ⋅ mb) → mb = None.
- Proof. destruct mb; [|done]. move=> /(exclusiveN_l _ a) []. Qed.
+ Proof. destruct mb; last done. move=> /(exclusiveN_l _ a) []. Qed.
Lemma exclusiveN_Some_r n a `{!Exclusive a} mb :
✓{n} (mb ⋅ Some a) → mb = None.
Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
Lemma exclusive_Some_l a `{!Exclusive a} mb : ✓ (Some a ⋅ mb) → mb = None.
- Proof. destruct mb; [|done]. move=> /(exclusive_l a) []. Qed.
+ Proof. destruct mb; last done. move=> /(exclusive_l a) []. Qed.
Lemma exclusive_Some_r a `{!Exclusive a} mb : ✓ (mb ⋅ Some a) → mb = None.
Proof. rewrite comm. by apply exclusive_Some_l. Qed.
@@ -1474,9 +1474,9 @@ Section option.
Proof. rewrite Some_included; eauto. Qed.
Lemma Some_includedN_total `{CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
- Proof. rewrite Some_includedN. split; [|eauto]. by intros [->|?]. Qed.
+ Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
Lemma Some_included_total `{CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
- Proof. rewrite Some_included. split; [|eauto]. by intros [->|?]. Qed.
+ Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
Some a ≼{n} Some b → ✓{n} b → a ≡{n}≡ b.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 0250c6922..dcd07527b 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -56,7 +56,7 @@ Section coPset.
Proof.
intros (Z&->&?)%subseteq_disjoint_union_L.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
- split; [done|]. rewrite coPset_op_union. set_solver.
+ split; first done. rewrite coPset_op_union. set_solver.
Qed.
End coPset.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 27f1eab67..822a952e3 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -47,7 +47,10 @@ Section gmultiset.
Proof. apply discrete_cmra_discrete. Qed.
Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
- Proof. split; [done | | done]. intros X. by rewrite gmultiset_op_disj_union left_id_L. Qed.
+ Proof.
+ split; [done | | done]. intros X.
+ by rewrite gmultiset_op_disj_union left_id_L.
+ Qed.
Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
Global Instance gmultiset_cancelable X : Cancelable X.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 8a7f5cb70..0b0963f54 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -281,7 +281,9 @@ Section limit_preserving.
LimitPreserving (λ x, P1 x ∧ P2 x).
Proof.
intros Hlim1 Hlim2 c Hc.
- split; [ apply Hlim1, Hc | apply Hlim2, Hc ].
+ split.
+ - apply Hlim1, Hc.
+ - apply Hlim2, Hc.
Qed.
Lemma limit_preserving_impl (P1 P2 : A → Prop) :
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index f8bc17d88..13926381f 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1565,19 +1565,19 @@ Qed.
Global Instance bi_persistently_sep_weak_homomorphism `{BiPositive PROP} :
WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
-Proof. split; try apply _. apply persistently_sep. Qed.
+Proof. split; [by apply _ ..|]. apply persistently_sep. Qed.
Global Instance bi_persistently_sep_homomorphism `{BiAffine PROP} :
MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
-Proof. split; try apply _. apply persistently_emp. Qed.
+Proof. split; [by apply _ ..|]. apply persistently_emp. Qed.
Global Instance bi_persistently_sep_entails_weak_homomorphism :
WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
-Proof. split; try apply _. intros P Q; by rewrite persistently_sep_2. Qed.
+Proof. split; [by apply _ ..|]. intros P Q; by rewrite persistently_sep_2. Qed.
Global Instance bi_persistently_sep_entails_homomorphism :
MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
-Proof. split; try apply _. simpl. apply persistently_emp_intro. Qed.
+Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.
(* Limits *)
Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A → PROP) :
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index d693e22e0..1af9dd81e 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -118,7 +118,7 @@ Proof.
Qed.
Lemma löb_alt_strong : BiLöb PROP ↔ ∀ P, (▷ P → P) ⊢ P.
-Proof. split; intros HLöb P; [apply löb|]. by intros ->%entails_impl_True. Qed.
+Proof. split; intros HLöb P; [by apply löb|]. by intros ->%entails_impl_True. Qed.
(** Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
Their [Ψ] is called [Q] in our proof. *)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index bb30eb594..f2bb21e9a 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -520,14 +520,20 @@ Qed.
Lemma monPred_objectively_and P Q : <obj> (P ∧ Q) ⊣⊢ <obj> P ∧ <obj> Q.
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=.
- - apply bi.and_intro; do 2 f_equiv; [apply bi.and_elim_l | apply bi.and_elim_r ].
+ - apply bi.and_intro; do 2 f_equiv.
+ + apply bi.and_elim_l.
+ + apply bi.and_elim_r.
- apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
Qed.
Lemma monPred_objectively_exist {A} (Φ : A → monPred) :
(∃ x, <obj> (Φ x)) ⊢ <obj> (∃ x, (Φ x)).
Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
Lemma monPred_objectively_or P Q : <obj> P ∨ <obj> Q ⊢ <obj> (P ∨ Q).
-Proof. apply bi.or_elim; f_equiv; [apply bi.or_intro_l | apply bi.or_intro_r]. Qed.
+Proof.
+ apply bi.or_elim; f_equiv.
+ - apply bi.or_intro_l.
+ - apply bi.or_intro_r.
+Qed.
Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
@@ -554,7 +560,11 @@ Lemma monPred_subjectively_forall {A} (Φ : A → monPred) :
(<subj> (∀ x, Φ x)) ⊢ ∀ x, <subj> (Φ x).
Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
Lemma monPred_subjectively_and P Q : <subj> (P ∧ Q) ⊢ <subj> P ∧ <subj> Q.
-Proof. apply bi.and_intro; f_equiv; [apply bi.and_elim_l | apply bi.and_elim_r]. Qed.
+Proof.
+ apply bi.and_intro; f_equiv.
+ - apply bi.and_elim_l.
+ - apply bi.and_elim_r.
+Qed.
Lemma monPred_subjectively_exist {A} (Φ : A → monPred) : <subj> (∃ x, Φ x) ⊣⊢ ∃ x, <subj> (Φ x).
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=;
@@ -564,7 +574,9 @@ Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj>
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=.
- apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
- - apply bi.or_elim; do 2 f_equiv; [apply bi.or_intro_l | apply bi.or_intro_r].
+ - apply bi.or_elim; do 2 f_equiv.
+ + apply bi.or_intro_l.
+ + apply bi.or_intro_r.
Qed.
Lemma monPred_subjectively_sep P Q : <subj> (P ∗ Q) ⊢ <subj> P ∗ <subj> Q.
--
GitLab