From 4d31feda42198f011eb73e254a019b1bee7ab180 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 00:26:07 +0200
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ad6707e0..22af9f20 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,6 +73,13 @@ API-breaking change is listed.
     similar to `tail`.
   + Declare `tail` as `simpl nomatch`.
   + Add lemmas about `head` and `tail`.
+- Add and extend equivalences between closure operators:
+  - Add `↔` lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps`.
+  - Rename `→` lemmas `rtc_nsteps` → `rtc_nsteps_1`,
+    `nsteps_rtc` → `rtc_nsteps_2`, `rtc_bsteps` → `rtc_bsteps_1`, and
+    `bsteps_rtc` → `rtc_bsteps_2`.
+  - Add lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps` to path
+    representations as lists.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -90,6 +97,11 @@ s/\bmap_union_filter\b/map_filter_union_complement/g
 # mbind
 s/\boption_mbind_proper\b/option_bind_proper/g
 s/\boption_mjoin_proper\b/option_join_proper/g
+# relations
+s/\brtc_nsteps\b/rtc_nsteps_1/g
+s/\bnsteps_rtc\b/rtc_nsteps_2/g
+s/\brtc_bsteps\b/rtc_bsteps_1/g
+s/\bbsteps_rtc\b/rtc_bsteps_2/g
 ' $(find theories -name "*.v")
 ```
 
-- 
GitLab