From 1bce0e36fee3a2f206f506f7456c172225b72703 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 28 Jan 2021 11:20:58 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20`Forall=5FForall2`=20=E2=86=92=20`Fora?=
 =?UTF-8?q?ll=5FForall2=5Fdiag`=20to=20be=20consistent=20with=20the=20name?=
 =?UTF-8?q?s=20for=20big=20operators=20in=20Iris.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md    | 3 +++
 theories/list.v | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 25e3b0cd..0399e0d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -51,6 +51,8 @@ Coq 8.8 and 8.9 are no longer supported.
   versions of the lemmas for the specific cases.
 - Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes
   are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
+- Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the
+  names for big operators in Iris.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -80,6 +82,7 @@ s/\bmap_Forall_insert_11\b/map_Forall_insert_1_1/g
 s/\bmap_Forall_insert_12\b/map_Forall_insert_1_2/g
 s/\bmap_Forall_union_11\b/map_Forall_union_1_1/g
 s/\bmap_Forall_union_12\b/map_Forall_union_1_2/g
+s/\bForall_Forall2\b/Forall_Forall2_diag/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/list.v b/theories/list.v
index 4222076b..d859626e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2735,7 +2735,7 @@ Proof.
 Qed.
 
 (** ** Properties of the [Forall2] predicate *)
-Lemma Forall_Forall2 {A} (Q : A → A → Prop) l :
+Lemma Forall_Forall2_diag {A} (Q : A → A → Prop) l :
   Forall (λ x, Q x x) l → Forall2 Q l l.
 Proof. induction 1; constructor; auto. Qed.
 
@@ -4645,7 +4645,7 @@ Ltac decompose_Forall := repeat
   | |- Forall _ (_ ++ _) => apply Forall_app_2
   | |- Forall _ (_ <$> _) => apply Forall_fmap
   | |- Forall _ (_ ≫= _) => apply Forall_bind
-  | |- Forall2 _ _ _ => apply Forall_Forall2
+  | |- Forall2 _ _ _ => apply Forall_Forall2_diag
   | |- Forall2 _ [] [] => constructor
   | |- Forall2 _ (_ :: _) (_ :: _) => constructor
   | |- Forall2 _ (_ ++ _) (_ ++ _) => first
-- 
GitLab