From b4f29dc02c95b282aa4eb8f1253784c40b37cf38 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 4 Sep 2021 22:37:17 -0400
Subject: [PATCH] tweak comments; changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b87bae3..d859ddc6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -158,6 +158,9 @@ API-breaking change is listed.
   application term.
 - Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
   `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
+- Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
+  `Forall2_cons_2` being the original one-directional versions (matching
+  `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -210,6 +213,8 @@ s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
 # map_filter_insert
 s/\bmap_filter_insert\b/map_filter_insert_True/g
 s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
+# Forall2
+s/\bForall2_cons_inv\b/Forall2_cons_1/g
 EOF
 ```
 
diff --git a/theories/list.v b/theories/list.v
index 19068bc9..c6e0aeb4 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2712,7 +2712,8 @@ Proof.
   end); clear go; intuition.
 Defined.
 
-(** Export the Coq stdlib constructors under different names. *)
+(** Export the Coq stdlib constructors under different names,
+because we use Forall_nil and Forall_cons for a version with a biimplication. *)
 Definition Forall_nil_2 := @Forall_nil A.
 Definition Forall_cons_2 := @Forall_cons A.
 Global Instance Forall_proper:
@@ -2984,7 +2985,8 @@ Lemma Forall2_Forall {A} P (l1 l2 : list A) :
   Forall2 P l1 l2 → Forall (uncurry P) (zip l1 l2).
 Proof. induction 1; constructor; auto. Qed.
 
-(** Export the Coq stdlib constructors under a different name *)
+(** Export the Coq stdlib constructors under a different name,
+because we use Forall_nil and Forall_cons for a version with a biimplication. *)
 Definition Forall2_nil_2 := @Forall2_nil.
 Definition Forall2_cons_2 := @Forall2_cons.
 Section Forall2.
-- 
GitLab