From 2ca5469ad2ec32b7f020e9faeba755129d0aac9c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 31 Aug 2017 12:42:21 +0200
Subject: [PATCH] More consistent naming, e.g. bare_later -> later_bare_2.

(All the later lemmas are now prefixed by later_, and dito for
laterN, and except_0).
---
 theories/bi/derived.v                | 38 +++++++++++++---------------
 theories/proofmode/class_instances.v | 18 ++++++-------
 theories/proofmode/coq_tactics.v     |  2 +-
 3 files changed, 27 insertions(+), 31 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 0df7d47c3..4b7ccddc9 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1419,15 +1419,13 @@ Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /bi_iff later_and !later_impl. Qed.
 Lemma later_persistently P : ▷ □ P ⊣⊢ □ ▷ P.
-Proof.
-  apply (anti_symm _); auto using later_persistently_1, later_persistently_2.
-Qed.
-Lemma bare_later P : ■ ▷ P ⊢ ▷ ■ P.
+Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
+Lemma later_bare_2 P : ■ ▷ P ⊢ ▷ ■ P.
 Proof. rewrite /bi_bare later_and. auto using later_intro. Qed.
-Lemma bare_persistently_later P : ⬕ ▷ P ⊢ ▷ ⬕ P.
-Proof. by rewrite -later_persistently bare_later. Qed.
-Lemma bare_persistently_if_later p P : ⬕?p ▷ P ⊢ ▷ ⬕?p P.
-Proof. destruct p; simpl; auto using bare_persistently_later. Qed.
+Lemma later_bare_persistently_2 P : ⬕ ▷ P ⊢ ▷ ⬕ P.
+Proof. by rewrite -later_persistently later_bare_2. Qed.
+Lemma later_bare_persistently_if_2 p P : ⬕?p ▷ P ⊢ ▷ ⬕?p P.
+Proof. destruct p; simpl; auto using later_bare_persistently_2. Qed.
 
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
 Proof.
@@ -1490,12 +1488,12 @@ Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
 Lemma laterN_persistently n P : ▷^n □ P ⊣⊢ □ ▷^n P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
-Lemma bare_laterN n P : ■ ▷^n P ⊢ ▷^n ■ P.
+Lemma laterN_bare_2 n P : ■ ▷^n P ⊢ ▷^n ■ P.
 Proof. rewrite /bi_bare laterN_and. auto using laterN_intro. Qed.
-Lemma bare_persistently_laterN n P : ⬕ ▷^n P ⊢ ▷^n ⬕ P.
-Proof. by rewrite -laterN_persistently bare_laterN. Qed.
-Lemma bare_persistently_if_laterN n p P : ⬕?p ▷^n P ⊢ ▷^n ⬕?p P.
-Proof. destruct p; simpl; auto using bare_persistently_laterN. Qed.
+Lemma laterN_bare_persistently_2 n P : ⬕ ▷^n P ⊢ ▷^n ⬕ P.
+Proof. by rewrite -laterN_persistently laterN_bare_2. Qed.
+Lemma laterN_bare_persistently_if_2 n p P : ⬕?p ▷^n P ⊢ ▷^n ⬕?p P.
+Proof. destruct p; simpl; auto using laterN_bare_persistently_2. Qed.
 
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
 Proof. induction n; apply _. Qed.
@@ -1550,15 +1548,13 @@ Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
 Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
-Proof.
-  by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure.
-Qed.
-Lemma bare_except_0 P : ■ ◇ P ⊢ ◇ ■ P.
+Proof. by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure. Qed.
+Lemma except_0_bare_2 P : ■ ◇ P ⊢ ◇ ■ P.
 Proof. rewrite /bi_bare except_0_and. auto using except_0_intro. Qed.
-Lemma bare_persistently_except_0 P : ⬕ ◇ P ⊢ ◇ ⬕ P.
-Proof. by rewrite -except_0_persistently bare_except_0. Qed.
-Lemma bare_persistently_if_except_0 p P : ⬕?p ◇ P ⊢ ◇ ⬕?p P.
-Proof. destruct p; simpl; auto using bare_persistently_except_0. Qed.
+Lemma except_0_bare_persistently_2 P : ⬕ ◇ P ⊢ ◇ ⬕ P.
+Proof. by rewrite -except_0_persistently except_0_bare_2. Qed.
+Lemma except_0_bare_persistently_if_2 p P : ⬕?p ◇ P ⊢ ◇ ⬕?p P.
+Proof. destruct p; simpl; auto using except_0_bare_persistently_2. Qed.
 
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7c9b492a5..636692cad 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -682,27 +682,27 @@ Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
 Global Instance into_wand_later p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
 Proof.
-  rewrite /IntoWand /= => HR. by rewrite !bare_persistently_if_later -later_wand HR.
+  rewrite /IntoWand /= => HR. by rewrite !later_bare_persistently_if_2 -later_wand HR.
 Qed.
 
 Global Instance into_wand_later_args p q R P Q :
   IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !bare_persistently_if_later (later_intro (⬕?p R)%I) -later_wand HR.
+  by rewrite !later_bare_persistently_if_2 (later_intro (⬕?p R)%I) -later_wand HR.
 Qed.
 
 Global Instance into_wand_laterN n p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
 Proof.
-  rewrite /IntoWand /= => HR. by rewrite !bare_persistently_if_laterN -laterN_wand HR.
+  rewrite /IntoWand /= => HR. by rewrite !laterN_bare_persistently_if_2 -laterN_wand HR.
 Qed.
 
 Global Instance into_wand_laterN_args n p q R P Q :
   IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !bare_persistently_if_laterN (laterN_intro _ (⬕?p R)%I) -laterN_wand HR.
+  by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (⬕?p R)%I) -laterN_wand HR.
 Qed.
 
 (* FromAnd *)
@@ -732,19 +732,19 @@ Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
 Proof.
   rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_later HP bare_persistently_if_elim later_and.
+  by rewrite later_bare_persistently_if_2 HP bare_persistently_if_elim later_and.
 Qed.
 Global Instance into_and_laterN n p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
 Proof.
   rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_laterN HP bare_persistently_if_elim laterN_and.
+  by rewrite laterN_bare_persistently_if_2 HP bare_persistently_if_elim laterN_and.
 Qed.
 Global Instance into_and_except_0 p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (◇ P) (◇ Q1) (◇ Q2).
 Proof.
   rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_except_0 HP bare_persistently_if_elim except_0_and.
+  by rewrite except_0_bare_persistently_if_2 HP bare_persistently_if_elim except_0_and.
 Qed.
 
 (* IntoSep *)
@@ -860,7 +860,7 @@ Global Instance frame_later p R R' P Q Q' :
   IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
 Proof.
   rewrite /Frame /MakeLater /IntoLaterN=>-> <- <- /=.
-  by rewrite bare_persistently_if_later later_sep.
+  by rewrite later_bare_persistently_if_2 later_sep.
 Qed.
 
 Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ▷^n P ⊣⊢ lP.
@@ -875,7 +875,7 @@ Global Instance frame_laterN p n R R' P Q Q' :
   IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /IntoLaterN=>-> <- <-.
-  by rewrite bare_persistently_if_laterN laterN_sep.
+  by rewrite laterN_bare_persistently_if_2 laterN_sep.
 Qed.
 
 Class MakeExcept0 (P Q : PROP) := make_except_0 : ◇ P ⊣⊢ Q.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 7f28831a7..9aabeb627 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1044,7 +1044,7 @@ Lemma into_laterN_env_sound n Δ1 Δ2 :
   IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n (Δ2 : bi_car _).
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !laterN_and !laterN_sep.
-  rewrite -{1}laterN_intro -bare_persistently_laterN.
+  rewrite -{1}laterN_intro -laterN_bare_persistently_2.
   apply and_mono, sep_mono.
   - apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-- 
GitLab