From db26bb923b0f19df3285f6e3294be4559ba14ed3 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Sat, 19 Aug 2023 21:29:56 -0500
Subject: [PATCH 01/18] Add combinators for equational reasoning of vector

---
 CHANGELOG.md                                  |  13 ++
 src/Data/Vec/Properties.agda                  | 100 +++++++++----
 .../Binary/Reasoning/Propositional.agda       | 139 ++++++++++++++++++
 3 files changed, 227 insertions(+), 25 deletions(-)
 create mode 100644 src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0485996a5c..3a9288be24 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1765,6 +1765,11 @@ New modules
   Function.Indexed.Bundles
   ```
 
+* Combinators for propositional equational reasoning on vectors with different indices
+  ```
+  Data.Vec.Relation.Binary.Reasoning.Propositional
+  ```
+
 Other minor changes
 -------------------
 
@@ -2673,6 +2678,7 @@ Other minor changes
   last-∷ʳ   : last (xs ∷ʳ x) ≡ x
   cast-∷ʳ   : cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
   ++-∷ʳ     : cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+  ∷ʳ-++     : cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
 
   reverse-∷          : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
   reverse-involutive : Involutive _≡_ reverse
@@ -2692,6 +2698,8 @@ Other minor changes
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
   cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq
+  cast-++ˡ      : cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
+  cast-++ʳ      : cast (cong (m +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
 
@@ -2705,6 +2713,11 @@ Other minor changes
   cast-fromList : cast _ (fromList xs) ≡ fromList ys
   fromList-map  : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs)
   fromList-++   : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
+  fromList-reverse : cast (Listₚ.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
+
+  ∷-ʳ++   : cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+  ++-ʳ++  : cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
+  ʳ++-ʳ++ : cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
   ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 47ff393d0f..5560528820 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -21,6 +21,7 @@ open import Data.Product.Base as Prod
 open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
+open import Data.Vec.Relation.Binary.Reasoning.Propositional as VecReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 open import Function.Base
 -- open import Function.Inverse using (_↔_; inverse)
 open import Function.Bundles using (_↔_; mk↔′)
@@ -493,6 +494,16 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 ++-identityʳ eq []       = refl
 ++-identityʳ eq (x ∷ xs) = cong (x ∷_) (++-identityʳ (cong pred eq) xs)
 
+cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
+           cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
+cast-++ˡ {o = zero}  eq []       {ys} = cast-is-id refl (cast eq [] ++ ys)
+cast-++ˡ {o = suc o} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ˡ (cong pred eq) xs)
+
+cast-++ʳ : ∀ .(eq : n ≡ o) (xs : Vec A m) {ys : Vec A n} →
+           cast (cong (m +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys
+cast-++ʳ {m = zero}  eq []       {ys} = refl
+cast-++ʳ {m = suc m} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ʳ eq xs)
+
 lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i<m : toℕ i < m) →
               lookup (xs ++ ys) i  ≡ lookup xs (Fin.fromℕ< i<m)
@@ -927,6 +938,11 @@ cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq
 ++-∷ʳ {m = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
 ++-∷ʳ {m = suc m} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
 
+∷ʳ-++ : ∀ .(eq : (suc n) + m ≡ n + suc m) a (xs : Vec A n) {ys} →
+        cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
+∷ʳ-++ eq a []       {ys} = cong (a ∷_) (cast-is-id (cong pred eq) ys)
+∷ʳ-++ eq a (x ∷ xs) {ys} = cong (x ∷_) (∷ʳ-++ (cong pred eq) a xs)
+
 ------------------------------------------------------------------------
 -- reverse
 
@@ -1006,34 +1022,24 @@ map-reverse f (x ∷ xs) = begin
 
 reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ {m = zero}  {n = n} eq []       ys = begin
-  cast _ (reverse ys)                ≡˘⟨ cong (cast eq) (++-identityʳ (sym eq) (reverse ys)) ⟩
-  cast _ (cast _ (reverse ys ++ [])) ≡⟨ cast-trans (sym eq) eq (reverse ys ++ []) ⟩
-  cast _ (reverse ys ++ [])          ≡⟨ cast-is-id (trans (sym eq) eq) (reverse ys ++ []) ⟩
-  reverse ys ++ []                   ≡⟨⟩
-  reverse ys ++ reverse []           ∎
-reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
-  cast eq (reverse (x ∷ xs ++ ys))                ≡⟨ cong (cast eq) (reverse-∷ x (xs ++ ys)) ⟩
-  cast eq (reverse (xs ++ ys) ∷ʳ x)               ≡˘⟨ cast-trans eq₂ eq₁ (reverse (xs ++ ys) ∷ʳ x) ⟩
-  (cast eq₁ ∘ cast eq₂) (reverse (xs ++ ys) ∷ʳ x) ≡⟨ cong (cast eq₁) (cast-∷ʳ _ x (reverse (xs ++ ys))) ⟩
-  cast eq₁ ((cast eq₃ (reverse (xs ++ ys))) ∷ʳ x) ≡⟨ cong (cast eq₁) (cong (_∷ʳ x) (reverse-++ _ xs ys)) ⟩
-  cast eq₁ ((reverse ys ++ reverse xs)      ∷ʳ x) ≡⟨ ++-∷ʳ _ x (reverse ys) (reverse xs) ⟩
-  reverse ys ++ (reverse xs ∷ʳ x)                 ≡˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
-  reverse ys ++ (reverse (x ∷ xs))                ∎
-  where
-  eq₁ = sym (+-suc n m)
-  eq₂ = cong suc (+-comm m n)
-  eq₃ = cong pred eq₂
+reverse-++ {m = zero}  {n = n} eq []       ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
+reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin′
+  reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
+  reverse (xs ++ ys) ∷ʳ x             ≈⟨ cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys))
+                                         ≈cong[ (_∷ʳ x) ] reverse-++ _ xs ys ⟩
+  (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
+  reverse ys ++ (reverse xs ∷ʳ x)     ≂˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
+  reverse ys ++ (reverse (x ∷ xs))    ∎′
 
 cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
 cast-reverse {n = zero}  eq []       = refl
-cast-reverse {n = suc n} eq (x ∷ xs) = begin
-  cast eq (reverse (x ∷ xs))              ≡⟨ cong (cast eq) (reverse-∷ x xs) ⟩
-  cast eq (reverse xs ∷ʳ x)               ≡⟨ cast-∷ʳ eq x (reverse xs) ⟩
-  (cast (cong pred eq) (reverse xs)) ∷ʳ x ≡⟨ cong (_∷ʳ x) (cast-reverse (cong pred eq) xs) ⟩
-  (reverse (cast (cong pred eq) xs)) ∷ʳ x ≡˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
-  reverse (x ∷ cast (cong pred eq) xs)    ≡⟨⟩
-  reverse (cast eq (x ∷ xs))              ∎
+cast-reverse {n = suc n} eq (x ∷ xs) = begin′
+  reverse (x ∷ xs)           ≂⟨ reverse-∷ x xs ⟩
+  reverse xs ∷ʳ x            ≈⟨ cast-∷ʳ eq x (reverse xs)
+                                ≈cong[ (_∷ʳ x) ] cast-reverse (cong pred eq) xs ⟩
+  reverse (cast _ xs) ∷ʳ x   ≂˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
+  reverse (x ∷ cast _ xs)    ≈⟨⟩
+  reverse (cast eq (x ∷ xs)) ∎′
 
 ------------------------------------------------------------------------
 -- _ʳ++_
@@ -1062,6 +1068,38 @@ map-ʳ++ {ys = ys} f xs = begin
   reverse (map f xs) ++ map f ys ≡˘⟨ unfold-ʳ++ (map f xs) (map f ys) ⟩
   map f xs ʳ++ map f ys          ∎
 
+∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
+        cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+∷-ʳ++ eq a xs {ys} = begin′
+  (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
+  reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩
+  reverse xs ++ (a ∷ ys)  ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩
+  xs ʳ++ (a ∷ ys)         ∎′
+
+++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
+         cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
+++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin′
+  ((xs ++ ys) ʳ++ zs)              ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
+  reverse (xs ++ ys) ++ zs         ≈⟨ cast-++ˡ (+-comm m n) (reverse (xs ++ ys))
+                                      ≈cong[ (_++ zs) ] reverse-++ (+-comm m n) xs ys ⟩
+  (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩
+  reverse ys ++ (reverse xs ++ zs) ≂˘⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟩
+  reverse ys ++ (xs ʳ++ zs)        ≂˘⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟩
+  ys ʳ++ (xs ʳ++ zs)               ∎′
+
+ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
+          cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
+ʳ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin′
+  (xs ʳ++ ys) ʳ++ zs                         ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
+  (reverse xs ++ ys) ʳ++ zs                  ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
+  reverse (reverse xs ++ ys) ++ zs           ≈⟨ cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys))
+                                                ≈cong[ (_++ zs) ] reverse-++ (+-comm m n) (reverse xs) ys ⟩
+  (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
+  (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
+  reverse ys ++ (xs ++ zs)                   ≂˘⟨ unfold-ʳ++ ys (xs ++ zs) ⟩
+  ys ʳ++ (xs ++ zs)                          ∎′
+
 ------------------------------------------------------------------------
 -- sum
 
@@ -1237,6 +1275,18 @@ fromList-++ : ∀ (xs : List A) {ys : List A} →
 fromList-++ List.[]       {ys} = cast-is-id refl (fromList ys)
 fromList-++ (x List.∷ xs) {ys} = cong (x ∷_) (fromList-++ xs)
 
+fromList-reverse : (xs : List A) → cast (Listₚ.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
+fromList-reverse List.[] = refl
+fromList-reverse (x List.∷ xs) = begin′
+  fromList (List.reverse (x List.∷ xs))         ≈⟨ cast-fromList (Listₚ.ʳ++-defn xs) ⟩
+  fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
+  fromList (List.reverse xs) ++ [ x ]           ≈˘⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟩
+  fromList (List.reverse xs) ∷ʳ x               ≈⟨ cast-∷ʳ (cong suc (Listₚ.length-reverse xs)) _ _
+                                                   ≈cong[ (_∷ʳ x) ] fromList-reverse xs ⟩
+  reverse (fromList xs) ∷ʳ x                    ≂˘⟨ reverse-∷ x (fromList xs) ⟩
+  reverse (x ∷ fromList xs)                     ≈⟨⟩
+  reverse (fromList (x List.∷ xs))              ∎′
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda b/src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda
new file mode 100644
index 0000000000..bbe2984356
--- /dev/null
+++ b/src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda
@@ -0,0 +1,139 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The basic code for equational reasoning with displayed propositional equality over vectors
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Relation.Binary.Reasoning.Propositional {a} {A : Set a} where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat.Properties using (suc-injective)
+open import Data.Vec.Base
+open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Definitions using (Sym; Trans)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; trans; sym; cong; module ≡-Reasoning)
+
+private
+  variable
+    l m n o : ℕ
+    xs ys zs : Vec A n
+
+-- Duplicate definition of cast-is-id and cast-trans to avoid circular dependency
+private
+  cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
+  cast-is-id eq []       = refl
+  cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
+
+  cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
+               cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
+  cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
+  cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
+    cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)
+
+
+
+≈-by : .(eq : n ≡ m) → REL (Vec A n) (Vec A m) _
+≈-by eq xs ys = (cast eq xs ≡ ys)
+
+infix 3 ≈-by
+syntax ≈-by n≡m xs ys = xs ≈[ n≡m ] ys
+
+----------------------------------------------------------------
+-- ≈-by is ‘reflexive’, ‘symmetric’ and ‘transitive’
+
+≈-reflexive : ∀ {n} → _≡_ ⇒ ≈-by {n} refl
+≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq
+
+≈-sym : .{m≡n : m ≡ n} → Sym (≈-by m≡n) (≈-by (sym m≡n))
+≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin
+  cast (sym m≡n) ys             ≡˘⟨ cong (cast (sym m≡n)) xs≈ys ⟩
+  cast (sym m≡n) (cast m≡n xs)  ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩
+  cast (trans m≡n (sym m≡n)) xs ≡⟨ cast-is-id (trans m≡n (sym m≡n)) xs ⟩
+  xs                            ∎
+  where open ≡-Reasoning
+
+≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans (≈-by m≡n) (≈-by n≡o) (≈-by (trans m≡n n≡o))
+≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin
+  cast (trans m≡n n≡o) xs ≡˘⟨ cast-trans m≡n n≡o xs ⟩
+  cast n≡o (cast m≡n xs)  ≡⟨ cong (cast n≡o) xs≈ys ⟩
+  cast n≡o ys             ≡⟨ ys≈zs ⟩
+  zs                      ∎
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Reasoning combinators
+
+begin_ : ∀ .{m≡n : m ≡ n} {xs : Vec A m} {ys} → xs ≈[ m≡n ] ys → cast m≡n xs ≡ ys
+begin xs≈ys = xs≈ys
+
+_∎ : (xs : Vec A n) → cast refl xs ≡ xs
+_∎ xs = ≈-reflexive refl
+
+_≈⟨⟩_ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys} → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡n ] ys)
+xs ≈⟨⟩ xs≈ys = xs≈ys
+
+-- composition of _≈[_]_
+step-≈ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
+         (ys ≈[ trans (sym m≡n) m≡o ] zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡o ] zs)
+step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs
+
+-- composition of the equality type on the right-hand side of _≈[_]_, or escaping to ordinary _≡_
+step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≡ zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡n ] zs)
+step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
+
+-- composition of the equality type on the left-hand side of _≈[_]_
+step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≈[ m≡n ] zs) → (xs ≡ ys) → (xs ≈[ m≡n ] zs)
+step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
+
+-- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong` operation
+≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
+         (ys ≈[ l≡o ] zs) → (xs ≈[ m≡n ] f (cast l≡o ys)) → (xs ≈[ m≡n ] f zs)
+≈-cong f ys≈zs xs≈fys = trans xs≈fys (cong f ys≈zs)
+
+
+-- symmetric version of each of the operator
+step-≈˘ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
+         (ys ≈[ trans n≡m m≡o ] zs) → (ys ≈[ n≡m ] xs) → (xs ≈[ m≡o ] zs)
+step-≈˘ xs ys≈zs ys≈xs = ≈-trans (≈-sym ys≈xs) ys≈zs
+
+step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≡ zs) → (ys ≈[ sym m≡n ] xs) → (xs ≈[ m≡n ] zs)
+step-≃˘ xs ys≡zs ys≈xs = trans (≈-sym ys≈xs) ys≡zs
+
+step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≈[ m≡n ] zs) → (ys ≡ xs) → (xs ≈[ m≡n ] zs)
+step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs)
+
+
+----------------------------------------------------------------
+-- convenient syntax for ‘equational’ reasoning
+
+infix 1 begin_
+infixr 2 step-≃ step-≂ step-≃˘ step-≂˘ step-≈ step-≈˘ _≈⟨⟩_ ≈-cong
+infix 3 _∎
+
+syntax step-≃  xs ys≡zs xs≈ys  = xs ≃⟨  xs≈ys ⟩ ys≡zs
+syntax step-≃˘ xs ys≡zs xs≈ys  = xs ≃˘⟨ xs≈ys ⟩ ys≡zs
+syntax step-≂  xs ys≈zs xs≡ys  = xs ≂⟨  xs≡ys ⟩ ys≈zs
+syntax step-≂˘ xs ys≈zs ys≡xs  = xs ≂˘⟨ ys≡xs ⟩ ys≈zs
+syntax step-≈  xs ys≈zs xs≈ys  = xs ≈⟨  xs≈ys ⟩ ys≈zs
+syntax step-≈˘ xs ys≈zs ys≈xs  = xs ≈˘⟨ ys≈xs ⟩ ys≈zs
+syntax ≈-cong  f  ys≈zs xs≈fys = xs≈fys ≈cong[ f ] ys≈zs
+
+{-
+-- An equational reasoning example, demonstrating nested uses of the cong operator
+
+cast-++ˡ : ∀ .(eq : n ≡ o) (xs : Vec A n) {ys : Vec A m} →
+           cast (cong (_+ m) eq) (xs ++ ys) ≡ cast eq xs ++ ys
+
+example : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) (ys : Vec A n) →
+          cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
+example {m = m} {n} eq a xs ys = begin
+  reverse ((xs ++ [ a ]) ++ ys)       ≈˘⟨ cast-reverse (cong (_+ n) (ℕₚ.+-comm 1 m)) ((xs ∷ʳ a) ++ ys)
+                                          ≈cong[ reverse ] cast-++ˡ (ℕₚ.+-comm 1 m) (xs ∷ʳ a)
+                                                           ≈cong[ (_++ ys) ] unfold-∷ʳ _ a xs ⟩
+  reverse ((xs ∷ʳ a) ++ ys)           ≈⟨ reverse-++ (ℕₚ.+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
+  reverse ys ++ reverse (xs ∷ʳ a)     ≂˘⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟩
+  ys ʳ++ reverse (xs ∷ʳ a)            ∎
+-}

From 48f12f4526b23a0cd53e4c52aef0b245bdd3d976 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 18 Sep 2023 15:19:31 -0500
Subject: [PATCH 02/18] review: rename module

---
 CHANGELOG.md                                                    | 2 +-
 src/Data/Vec/Properties.agda                                    | 2 +-
 .../Binary/{Reasoning/Propositional.agda => Equality/Cast.agda} | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)
 rename src/Data/Vec/Relation/Binary/{Reasoning/Propositional.agda => Equality/Cast.agda} (98%)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3a9288be24..191bb7b3cc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1767,7 +1767,7 @@ New modules
 
 * Combinators for propositional equational reasoning on vectors with different indices
   ```
-  Data.Vec.Relation.Binary.Reasoning.Propositional
+  Data.Vec.Relation.Binary.Equality.Cast
   ```
 
 Other minor changes
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 5560528820..f95176324d 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -21,7 +21,7 @@ open import Data.Product.Base as Prod
 open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
-open import Data.Vec.Relation.Binary.Reasoning.Propositional as VecReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+open import Data.Vec.Relation.Binary.Equality.Cast as CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 open import Function.Base
 -- open import Function.Inverse using (_↔_; inverse)
 open import Function.Bundles using (_↔_; mk↔′)
diff --git a/src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
similarity index 98%
rename from src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda
rename to src/Data/Vec/Relation/Binary/Equality/Cast.agda
index bbe2984356..1eaaad4493 100644
--- a/src/Data/Vec/Relation/Binary/Reasoning/Propositional.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.Vec.Relation.Binary.Reasoning.Propositional {a} {A : Set a} where
+module Data.Vec.Relation.Binary.Equality.Cast {a} {A : Set a} where
 
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Nat.Properties using (suc-injective)

From 31f791745323f3f29f163ea5479c8769dc97433d Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 18 Sep 2023 15:19:56 -0500
Subject: [PATCH 03/18] review: wrap comments

---
 src/Data/Vec/Relation/Binary/Equality/Cast.agda | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index 1eaaad4493..8d9b01f0b0 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -1,7 +1,8 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The basic code for equational reasoning with displayed propositional equality over vectors
+-- The basic code for equational reasoning about vectors with
+-- different indices using cast
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -41,7 +42,7 @@ private
 infix 3 ≈-by
 syntax ≈-by n≡m xs ys = xs ≈[ n≡m ] ys
 
-----------------------------------------------------------------
+------------------------------------------------------------------------
 -- ≈-by is ‘reflexive’, ‘symmetric’ and ‘transitive’
 
 ≈-reflexive : ∀ {n} → _≡_ ⇒ ≈-by {n} refl
@@ -80,7 +81,8 @@ step-≈ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n
          (ys ≈[ trans (sym m≡n) m≡o ] zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡o ] zs)
 step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs
 
--- composition of the equality type on the right-hand side of _≈[_]_, or escaping to ordinary _≡_
+-- composition of the equality type on the right-hand side of _≈[_]_,
+-- or escaping to ordinary _≡_
 step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≡ zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡n ] zs)
 step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
 
@@ -88,7 +90,8 @@ step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
 step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≈[ m≡n ] zs) → (xs ≡ ys) → (xs ≈[ m≡n ] zs)
 step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
 
--- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong` operation
+-- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong`
+-- operation
 ≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
          (ys ≈[ l≡o ] zs) → (xs ≈[ m≡n ] f (cast l≡o ys)) → (xs ≈[ m≡n ] f zs)
 ≈-cong f ys≈zs xs≈fys = trans xs≈fys (cong f ys≈zs)
@@ -106,7 +109,7 @@ step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≈[ m≡n ]
 step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs)
 
 
-----------------------------------------------------------------
+------------------------------------------------------------------------
 -- convenient syntax for ‘equational’ reasoning
 
 infix 1 begin_

From da40fb82556b0aa23cb61e0692223f475795b0df Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 18 Sep 2023 15:21:14 -0500
Subject: [PATCH 04/18] review: only open CastReasoning locally

---
 src/Data/Vec/Properties.agda | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index f95176324d..6289353b56 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -21,7 +21,7 @@ open import Data.Product.Base as Prod
 open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
-open import Data.Vec.Relation.Binary.Equality.Cast as CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+import Data.Vec.Relation.Binary.Equality.Cast as CastReasoning
 open import Function.Base
 -- open import Function.Inverse using (_↔_; inverse)
 open import Function.Bundles using (_↔_; mk↔′)
@@ -1022,7 +1022,7 @@ map-reverse f (x ∷ xs) = begin
 
 reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ {m = zero}  {n = n} eq []       ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
+reverse-++ {m = zero}  {n = n} eq []       ys = CastReasoning.≈-sym (++-identityʳ (sym eq) (reverse ys))
 reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin′
   reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
   reverse (xs ++ ys) ∷ʳ x             ≈⟨ cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys))
@@ -1030,6 +1030,7 @@ reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin′
   (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
   reverse ys ++ (reverse (x ∷ xs))    ∎′
+  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 
 cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
 cast-reverse {n = zero}  eq []       = refl
@@ -1040,6 +1041,7 @@ cast-reverse {n = suc n} eq (x ∷ xs) = begin′
   reverse (cast _ xs) ∷ʳ x   ≂˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
   reverse (x ∷ cast _ xs)    ≈⟨⟩
   reverse (cast eq (x ∷ xs)) ∎′
+  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 
 ------------------------------------------------------------------------
 -- _ʳ++_
@@ -1076,6 +1078,7 @@ map-ʳ++ {ys = ys} f xs = begin
   (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩
   reverse xs ++ (a ∷ ys)  ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩
   xs ʳ++ (a ∷ ys)         ∎′
+  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 
 ++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
@@ -1087,6 +1090,7 @@ map-ʳ++ {ys = ys} f xs = begin
   reverse ys ++ (reverse xs ++ zs) ≂˘⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟩
   reverse ys ++ (xs ʳ++ zs)        ≂˘⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟩
   ys ʳ++ (xs ʳ++ zs)               ∎′
+  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 
 ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
           cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
@@ -1099,6 +1103,7 @@ map-ʳ++ {ys = ys} f xs = begin
   (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂˘⟨ unfold-ʳ++ ys (xs ++ zs) ⟩
   ys ʳ++ (xs ++ zs)                          ∎′
+  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 
 ------------------------------------------------------------------------
 -- sum
@@ -1286,6 +1291,7 @@ fromList-reverse (x List.∷ xs) = begin′
   reverse (fromList xs) ∷ʳ x                    ≂˘⟨ reverse-∷ x (fromList xs) ⟩
   reverse (x ∷ fromList xs)                     ≈⟨⟩
   reverse (fromList (x List.∷ xs))              ∎′
+  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

From bef3328e373d8e0fb639322a60f577e3feef7eab Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 18 Sep 2023 15:21:48 -0500
Subject: [PATCH 05/18] Remove duplicate definition of cast-{is-id,trans}

---
 src/Data/Vec/Properties.agda                    | 7 ++-----
 src/Data/Vec/Relation/Binary/Equality/Cast.agda | 2 --
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 6289353b56..9c286494ef 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -390,17 +390,14 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 -- cast
 
 cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
-cast-is-id eq []       = refl
-cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
+cast-is-id _ _ = CastReasoning.≈-reflexive refl
 
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
 
 cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
-cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
-cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
-  cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)
+cast-trans eq₁ _ _ = sym (CastReasoning.≈-trans (cong (cast eq₁) refl) refl)
 
 ------------------------------------------------------------------------
 -- map
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index 8d9b01f0b0..a1902d91bb 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -22,8 +22,6 @@ private
     l m n o : ℕ
     xs ys zs : Vec A n
 
--- Duplicate definition of cast-is-id and cast-trans to avoid circular dependency
-private
   cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
   cast-is-id eq []       = refl
   cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)

From 22a8d7ed0c1b4aa1bbfa187f90d6916bfd93d6c6 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Tue, 19 Sep 2023 15:53:18 -0500
Subject: [PATCH 06/18] =?UTF-8?q?review:=20use=20=5F=E2=89=88[=5F]=5F=20as?=
 =?UTF-8?q?=20the=20name=20of=20the=20equality?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Vec/Relation/Binary/Equality/Cast.agda | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index a1902d91bb..7f6699e9e4 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -34,19 +34,18 @@ private
 
 
 
-≈-by : .(eq : n ≡ m) → REL (Vec A n) (Vec A m) _
-≈-by eq xs ys = (cast eq xs ≡ ys)
+infix 3 _≈[_]_
 
-infix 3 ≈-by
-syntax ≈-by n≡m xs ys = xs ≈[ n≡m ] ys
+_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set a
+xs ≈[ eq ] ys = cast eq xs ≡ ys
 
 ------------------------------------------------------------------------
--- ≈-by is ‘reflexive’, ‘symmetric’ and ‘transitive’
+-- _≈[_]_ is ‘reflexive’, ‘symmetric’ and ‘transitive’
 
-≈-reflexive : ∀ {n} → _≡_ ⇒ ≈-by {n} refl
+≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys)
 ≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq
 
-≈-sym : .{m≡n : m ≡ n} → Sym (≈-by m≡n) (≈-by (sym m≡n))
+≈-sym : .{m≡n : m ≡ n} → Sym (_≈[ m≡n ]_) (_≈[ sym m≡n ]_)
 ≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin
   cast (sym m≡n) ys             ≡˘⟨ cong (cast (sym m≡n)) xs≈ys ⟩
   cast (sym m≡n) (cast m≡n xs)  ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩
@@ -54,7 +53,7 @@ syntax ≈-by n≡m xs ys = xs ≈[ n≡m ] ys
   xs                            ∎
   where open ≡-Reasoning
 
-≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans (≈-by m≡n) (≈-by n≡o) (≈-by (trans m≡n n≡o))
+≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans (_≈[ m≡n ]_) (_≈[ n≡o ]_) (_≈[ trans m≡n n≡o ]_)
 ≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin
   cast (trans m≡n n≡o) xs ≡˘⟨ cast-trans m≡n n≡o xs ⟩
   cast n≡o (cast m≡n xs)  ≡⟨ cong (cast n≡o) xs≈ys ⟩

From 4275945109edafae30611b8840bc0bf473b1346c Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Tue, 19 Sep 2023 15:59:32 -0500
Subject: [PATCH 07/18] review: remove extra parenthesis

---
 .../Vec/Relation/Binary/Equality/Cast.agda    | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index 7f6699e9e4..b6c780b4cb 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -45,7 +45,7 @@ xs ≈[ eq ] ys = cast eq xs ≡ ys
 ≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys)
 ≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq
 
-≈-sym : .{m≡n : m ≡ n} → Sym (_≈[ m≡n ]_) (_≈[ sym m≡n ]_)
+≈-sym : .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_
 ≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin
   cast (sym m≡n) ys             ≡˘⟨ cong (cast (sym m≡n)) xs≈ys ⟩
   cast (sym m≡n) (cast m≡n xs)  ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩
@@ -53,7 +53,7 @@ xs ≈[ eq ] ys = cast eq xs ≡ ys
   xs                            ∎
   where open ≡-Reasoning
 
-≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans (_≈[ m≡n ]_) (_≈[ n≡o ]_) (_≈[ trans m≡n n≡o ]_)
+≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
 ≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin
   cast (trans m≡n n≡o) xs ≡˘⟨ cast-trans m≡n n≡o xs ⟩
   cast n≡o (cast m≡n xs)  ≡⟨ cong (cast n≡o) xs≈ys ⟩
@@ -70,39 +70,39 @@ begin xs≈ys = xs≈ys
 _∎ : (xs : Vec A n) → cast refl xs ≡ xs
 _∎ xs = ≈-reflexive refl
 
-_≈⟨⟩_ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys} → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡n ] ys)
+_≈⟨⟩_ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys} → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] ys
 xs ≈⟨⟩ xs≈ys = xs≈ys
 
 -- composition of _≈[_]_
 step-≈ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
-         (ys ≈[ trans (sym m≡n) m≡o ] zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡o ] zs)
+         ys ≈[ trans (sym m≡n) m≡o ] zs → xs ≈[ m≡n ] ys → xs ≈[ m≡o ] zs
 step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs
 
 -- composition of the equality type on the right-hand side of _≈[_]_,
 -- or escaping to ordinary _≡_
-step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≡ zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡n ] zs)
+step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] zs
 step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
 
 -- composition of the equality type on the left-hand side of _≈[_]_
-step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≈[ m≡n ] zs) → (xs ≡ ys) → (xs ≈[ m≡n ] zs)
+step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → xs ≡ ys → xs ≈[ m≡n ] zs
 step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
 
 -- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong`
 -- operation
 ≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
-         (ys ≈[ l≡o ] zs) → (xs ≈[ m≡n ] f (cast l≡o ys)) → (xs ≈[ m≡n ] f zs)
+         ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f (cast l≡o ys) → xs ≈[ m≡n ] f zs
 ≈-cong f ys≈zs xs≈fys = trans xs≈fys (cong f ys≈zs)
 
 
 -- symmetric version of each of the operator
 step-≈˘ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
-         (ys ≈[ trans n≡m m≡o ] zs) → (ys ≈[ n≡m ] xs) → (xs ≈[ m≡o ] zs)
+         ys ≈[ trans n≡m m≡o ] zs → ys ≈[ n≡m ] xs → xs ≈[ m≡o ] zs
 step-≈˘ xs ys≈zs ys≈xs = ≈-trans (≈-sym ys≈xs) ys≈zs
 
-step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≡ zs) → (ys ≈[ sym m≡n ] xs) → (xs ≈[ m≡n ] zs)
+step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → ys ≈[ sym m≡n ] xs → xs ≈[ m≡n ] zs
 step-≃˘ xs ys≡zs ys≈xs = trans (≈-sym ys≈xs) ys≡zs
 
-step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → (ys ≈[ m≡n ] zs) → (ys ≡ xs) → (xs ≈[ m≡n ] zs)
+step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → ys ≡ xs → xs ≈[ m≡n ] zs
 step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs)
 
 

From eca0dfb98e078f2d61a192de420ae31b91ddb79a Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Tue, 19 Sep 2023 16:02:05 -0500
Subject: [PATCH 08/18] slightly cleanup the symmetric combinators

---
 src/Data/Vec/Relation/Binary/Equality/Cast.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index b6c780b4cb..6b76b43f8f 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -97,10 +97,10 @@ step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
 -- symmetric version of each of the operator
 step-≈˘ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
          ys ≈[ trans n≡m m≡o ] zs → ys ≈[ n≡m ] xs → xs ≈[ m≡o ] zs
-step-≈˘ xs ys≈zs ys≈xs = ≈-trans (≈-sym ys≈xs) ys≈zs
+step-≈˘ xs ys≈zs ys≈xs = step-≈ xs ys≈zs (≈-sym ys≈xs)
 
 step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → ys ≈[ sym m≡n ] xs → xs ≈[ m≡n ] zs
-step-≃˘ xs ys≡zs ys≈xs = trans (≈-sym ys≈xs) ys≡zs
+step-≃˘ xs ys≡zs ys≈xs = step-≃ xs ys≡zs (≈-sym ys≈xs)
 
 step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → ys ≡ xs → xs ≈[ m≡n ] zs
 step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs)

From e11cbc578be238c23cd2f243583ad1d01de22fa5 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Tue, 19 Sep 2023 17:58:38 -0500
Subject: [PATCH 09/18] Fixup of bef3328: cong _ refl is refl

---
 src/Data/Vec/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 5cee99d444..a7dd888a25 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -350,7 +350,7 @@ subst-is-cast refl xs = sym (cast-is-id refl xs)
 
 cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
-cast-trans eq₁ _ _ = sym (CastReasoning.≈-trans (cong (cast eq₁) refl) refl)
+cast-trans _ _ _ = sym (CastReasoning.≈-trans refl refl)
 
 ------------------------------------------------------------------------
 -- map

From db5c229b5a93d78bb71d1455321a4e3cfbf5078a Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 2 Oct 2023 15:38:39 -0500
Subject: [PATCH 10/18] Add README for the library

---
 README.agda                                   |   2 +-
 README/Data.agda                              |   5 +
 .../Vec/Relation/Binary/Equality/Cast.agda    | 259 ++++++++++++++++++
 .../Vec/Relation/Binary/Equality/Cast.agda    |  30 +-
 4 files changed, 273 insertions(+), 23 deletions(-)
 create mode 100644 README/Data/Vec/Relation/Binary/Equality/Cast.agda

diff --git a/README.agda b/README.agda
index 6fee0aeffa..97b8ab3903 100644
--- a/README.agda
+++ b/README.agda
@@ -15,7 +15,7 @@ module README where
 -- James McKinna, Sergei Meshveliani, Eric Mertens, Darin Morrison,
 -- Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa,
 -- Nicolas Pouillard, Andrés Sicard-Ramírez, Lex van der Stoep,
--- Sandro Stucki, Milo Turner, Noam Zeilberger
+-- Sandro Stucki, Milo Turner, Noam Zeilberger, Shu-Hung You
 -- and other anonymous contributors.
 ------------------------------------------------------------------------
 
diff --git a/README/Data.agda b/README/Data.agda
index be35a5bfc4..e7d8a13886 100644
--- a/README/Data.agda
+++ b/README/Data.agda
@@ -209,6 +209,11 @@ import README.Data.Record
 
 import README.Data.Trie.NonDependent
 
+-- Examples of equational reasoning about vectors of non-definitionally
+-- equal lengths.
+
+import README.Data.Vec.Relation.Binary.Equality.Cast
+
 -- Examples how (indexed) containers and constructions over them (free
 -- monad, least fixed point, etc.) can be used
 
diff --git a/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
new file mode 100644
index 0000000000..65a9c45414
--- /dev/null
+++ b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -0,0 +1,259 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An equational reasoning library for propositional equality over
+-- vectors of different indices using cast.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Vec.Relation.Binary.Equality.Cast where
+
+open import Agda.Primitive
+open import Data.List.Base as L using (List)
+import Data.List.Properties as Lₚ
+open import Data.Nat.Base
+open import Data.Nat.Properties
+open import Data.Vec.Base
+open import Data.Vec.Properties
+import Data.Vec.Relation.Binary.Equality.Cast as CastReasoning
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; trans; sym; cong; subst; module ≡-Reasoning)
+
+private variable
+  a : Level
+  A : Set a
+  l m n o : ℕ
+  xs ys zs ws : Vec A n
+
+
+-- To see example usages of this library, scroll to the combinators
+-- section.
+
+
+------------------------------------------------------------------------
+--
+-- Motivation
+--
+-- The `cast` function is the computational variant of `subst` for
+-- vectors. Since `cast` computes under vector constructors, it
+-- enables reasoning about vectors with non-definitionally equal indices
+-- by induction. See, e.g., Jacques Carette's comment in issue #1668.
+-- <https://github.com/agda/agda-stdlib/pull/1668#issuecomment-1003449509>
+--
+-- Suppose we want to prove that ‘xs ++ [] ≡ xs’. Because `xs ++ []`
+-- has type `Vec A (n + 0)` while `xs` has type `Vec A n`, they cannot
+-- be directly related by homogeneous equality.
+-- To resolve the issue, `++-right-identity` uses `cast` to recast
+-- `xs ++ []` as a vector in `Vec A n`.
+--
+++-right-identity : ∀ .(eq : n + 0 ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
+++-right-identity eq []       = refl
+++-right-identity eq (x ∷ xs) = cong (x ∷_) (++-right-identity (cong pred eq) xs)
+--
+-- When the input is `x ∷ xs`, because `cast eq (x ∷ _)` equals
+-- `x ∷ cast (cong pred eq) _`, the proof obligation
+--     cast eq (x ∷ xs ++ []) ≡ x ∷ xs
+-- simplifies to
+--     x :: cast (cong pred eq) (xs ++ []) ≡ x ∷ xs
+
+
+-- Although `cast` makes it possible to prove vector identities by ind-
+-- uction, the explicit type-casting nature poses a significant barrier
+-- to code reuse in larger proofs. For example, consider the identity
+-- ‘fromList (xs L.∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `L._∷ʳ_` is the
+-- snoc function of lists. We have
+--
+--     fromList (xs L.∷ʳ x)            : Vec A (L.length (xs L.∷ʳ x))
+--   =   {- by definition -}
+--     fromList (xs L.++ L.[ x ])      : Vec A (L.length (xs L.++ L.[ x ]))
+--   =   {- by fromList-++ -}
+--     fromList xs ++ fromList L.[ x ] : Vec A (L.length xs + L.length [ x ])
+--   =   {- by definition -}
+--     fromList xs ++ [ x ]            : Vec A (L.length xs + 1)
+--   =   {- by unfold-∷ʳ -}
+--     fromList xs ∷ʳ x                : Vec A (suc (L.length xs))
+-- where
+--     fromList-++ : cast _ (fromList (xs L.++ ys)) ≡ fromList xs ++ fromList ys
+--     unfold-∷ʳ   : cast _ (xs ∷ʳ x) ≡ xs ++ [ x ]
+--
+-- Although the identity itself is simple, the reasoning process changes
+-- the index in the type twice. Consequently, its Agda translation must
+-- insert two `cast`s in the proof. Moreover, the proof first has to
+-- rearrange (the Agda version of) the identity into one with two
+-- `cast`s, resulting in lots of boilerplate code as demonstrated by
+-- `example1a-fromList-∷ʳ`.
+example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
+                        cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
+example1a-fromList-∷ʳ x xs eq = begin
+  cast eq (fromList (xs L.∷ʳ x))                   ≡⟨⟩
+  cast eq (fromList (xs L.++ L.[ x ]))             ≡˘⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟩
+  cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
+  cast eq₂ (fromList xs ++ [ x ])                  ≡⟨ CastReasoning.≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
+  fromList xs ∷ʳ x                                 ∎
+  where
+  open ≡-Reasoning
+  eq₁ = Lₚ.length-++ xs {L.[ x ]}
+  eq₂ = +-comm (L.length xs) 1
+
+-- The `cast`s are irrelevant to core of the proof. At the same time,
+-- they can be inferred from the lemmas used during the reasoning steps
+-- (e.g. `fromList-++` and `unfold-∷ʳ`). To eliminate the boilerplate,
+-- this library provides a set of equational reasoning combinators for
+-- equality of the form `cast eq xs ≡ ys`.
+example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
+                        cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
+example1b-fromList-∷ʳ x xs eq = begin
+  fromList (xs L.∷ʳ x)       ≈⟨⟩
+  fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ [ x ]       ≈˘⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟩
+  fromList xs ∷ʳ x           ∎
+  where open CastReasoning
+
+
+
+
+------------------------------------------------------------------------
+--
+-- Combinators
+--
+-- Let `xs ≈[ m≡n ] ys` denote `cast m≡n xs ≡ ys`. We have reflexivity,
+-- symmetry and transitivity:
+--     ≈-reflexive : xs ≈[ refl ] xs
+--     ≈-sym       : xs ≈[ m≡n ] ys → ys ≈[ sym m≡n ] xs
+--     ≈-trans     : xs ≈[ m≡n ] ys → ys ≈[ n≡o ] zs → xs ≈[ trans m≡n n≡o ] zs
+-- Accordingly, `_≈[_]_` admits the standard set of equational reasoning
+-- combinators. Suppose `≈-eqn : xs ≈[ m≡n ] ys`,
+--     xs ≈⟨ ≈-eqn  ⟩   -- `_≈⟨_⟩_` takes a `_≈[_]_` step, adjusting
+--     ys               -- the index at the same time
+--
+--     ys ≈˘⟨ ≈-eqn ⟩   -- `_≈˘⟨_⟩_` takes a symmetric `_≈[_]_` step
+--     xs
+example2a : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
+            cast eq ((reverse xs ∷ʳ a) ++ ys) ≡ reverse xs ++ (a ∷ ys)
+example2a eq xs a ys = begin
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n
+  reverse xs ++ (a ∷ ys)  ∎                            -- index: m + suc n
+  where open CastReasoning
+
+-- To interoperate with `_≡_`, this library provides `_≂⟨_⟩_` (\-~) for
+-- taking a `_≡_` step during equational reasoning.
+-- Let `≡-eqn : xs ≡ ys`, then
+--     xs ≂⟨ ≡-eqn  ⟩    -- Takes a `_≡_` step; no change to the index
+--     ys
+--
+--     ys ≂˘⟨ ≡-eqn ⟩    -- Takes a symmetric `_≡_` step
+--     xs
+-- Equivalently, `≈-reflexive` injects `_≡_` into `_≈[_]_`. That is,
+-- `xs ≂⟨ ≡-eqn ⟩ ys` is the same as `xs ≈⟨ ≈-reflexive ≡-eqn ⟩ ys`.
+-- Extending `example2a`, we have:
+example2b : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
+            cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
+example2b eq xs a ys = begin
+  (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩          -- index: suc m + n
+  reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩  -- index: suc m + n
+  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩         -- index: suc m + n
+  reverse xs ++ (a ∷ ys)  ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩         -- index: m + suc n
+  xs ʳ++ (a ∷ ys)         ∎                                    -- index: m + suc n
+  where open CastReasoning
+
+-- Oftentimes index-changing identities apply to only part of the proof
+-- term. When reasoning about `_≡_`, `cong` shifts the focus to the
+-- subterm of interest. In this library, `≈-cong` does a similar job.
+-- Suppose `f : A → B`, `xs : B`, `ys zs : A`, `ys≈zs : ys ≈[ _ ] zs`
+-- and `xs≈f⟨c·ys⟩ : xs ≈[ _ ] f (cast _ ys)`, we have
+--     xs ≈⟨ ≈-cong f xs≈f⟨c·ys⟩ ys≈zs ⟩
+--     f zs
+-- The reason for having the extra argument `xs≈f⟨c·ys⟩` is to expose
+-- `cast` in the subterm in order to apply the step `ys≈zs`. When using
+-- ordinary `cong` the proof has to explicitly push `cast` inside:
+--     xs            ≈⟨ xs≈f⟨c·ys⟩ ⟩
+--     f (cast _ ys) ≂⟨ cong f ys≈zs ⟩
+--     f zs
+-- Note. Technically, `A` and `B` should be vectors of different length
+-- and that `ys`, `zs` are vectors of non-definitionally equal index.
+example3a-fromList-++-++ : {xs ys zs : List A} →
+                           .(eq : L.length (xs L.++ ys L.++ zs) ≡
+                                  L.length xs + (L.length ys + L.length zs)) →
+                           cast eq (fromList (xs L.++ ys L.++ zs)) ≡
+                                   fromList xs ++ fromList ys ++ fromList zs
+example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin
+  fromList (xs L.++ ys L.++ zs)             ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ fromList (ys L.++ zs)      ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (Lₚ.length-++ ys) (fromList xs))
+                                                      (fromList-++ ys) ⟩
+  fromList xs ++ fromList ys ++ fromList zs ∎
+  where open CastReasoning
+
+-- As an alternative, one can manually apply `cast-++ʳ` to expose `cast`
+-- in the subterm. However, this unavoidably duplicates the proof term.
+example3b-fromList-++-++′ : {xs ys zs : List A} →
+                            .(eq : L.length (xs L.++ ys L.++ zs) ≡
+                                   L.length xs + (L.length ys + L.length zs)) →
+                            cast eq (fromList (xs L.++ ys L.++ zs)) ≡
+                                    fromList xs ++ fromList ys ++ fromList zs
+example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
+  fromList (xs L.++ ys L.++ zs)                 ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ fromList (ys L.++ zs)          ≈⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
+  fromList xs ++ cast _ (fromList (ys L.++ zs)) ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
+  fromList xs ++ fromList ys ++ fromList zs     ∎
+  where open CastReasoning
+
+-- `≈-cong` can be chained together much like how `cong` can be nested.
+-- In this example, `unfold-∷ʳ` is applied to the term `xs ++ [ a ]`
+-- in `(_++ ys)` inside of `reverse`. Thus the proof employs two
+-- `≈-cong`.
+example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys →
+          cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
+example4-cong² {m = m} {n} eq a xs ys = begin
+  reverse ((xs ++ [ a ]) ++ ys)   ≈˘⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
+                                             (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
+                                                     (unfold-∷ʳ _ a xs)) ⟩
+  reverse ((xs ∷ʳ a) ++ ys)       ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
+  reverse ys ++ reverse (xs ∷ʳ a) ≂˘⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟩
+  ys ʳ++ reverse (xs ∷ʳ a)        ∎
+  where open CastReasoning
+
+------------------------------------------------------------------------
+--
+-- Interoperation between `_≈[_]_` and `_≡_`
+--
+-- This library is designed to interoperate with `_≡_`. Examples in the
+-- combinators section showed how to apply `_≂⟨_⟩_` to take an `_≡_`
+-- step during equational reasoning about `_≈[_]_`. Recall that
+-- `xs ≈[ m≡n ] ys` is a shorthand for `cast m≡n xs ≡ ys`, the
+-- combinator is essentially the composition of `_≡_` on the left-hand
+-- side of `_≈[_]_`. Dually, the combinator `_≃⟨_⟩_` composes `_≡_` on
+-- the right-hand side of `_≈[_]_`. Thus `_≃⟨_⟩_` intuitively ends the
+-- reasoning system of `_≈[_]_` and switches back to the reasoning
+-- system of `_≡_`.
+example5-fromList-++-++′ : {xs ys zs : List A} →
+                           .(eq : L.length (xs L.++ ys L.++ zs) ≡
+                                  L.length xs + (L.length ys + L.length zs)) →
+                           cast eq (fromList (xs L.++ ys L.++ zs)) ≡
+                                   fromList xs ++ fromList ys ++ fromList zs
+example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin′
+  fromList (xs L.++ ys L.++ zs)                 ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ fromList (ys L.++ zs)          ≃⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
+  fromList xs ++ cast _ (fromList (ys L.++ zs)) ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
+  fromList xs ++ fromList ys ++ fromList zs     ∎
+  where open ≡-Reasoning; open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+
+-- Of course, it is possible to start with the reasoning system of `_≡_`
+-- and then switch to the reasoning system of `_≈[_]_`.
+example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
+example6a-reverse-∷ʳ {n = n} x xs = begin
+  reverse (xs ∷ʳ x)     ≡˘⟨ ≈-reflexive refl ⟩
+  reverse (xs ∷ʳ x)     ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
+  reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
+  x ∷ reverse xs        ∎′
+  where open ≡-Reasoning; open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+
+example6b-reverse-∷ʳ-by-induction : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
+example6b-reverse-∷ʳ-by-induction x []       = refl
+example6b-reverse-∷ʳ-by-induction x (y ∷ xs) = begin
+  reverse (y ∷ (xs ∷ʳ x)) ≡⟨ reverse-∷ y (xs ∷ʳ x) ⟩
+  reverse (xs ∷ʳ x) ∷ʳ y  ≡⟨ cong (_∷ʳ y) (example6b-reverse-∷ʳ-by-induction x xs) ⟩
+  (x ∷ reverse xs) ∷ʳ y   ≡⟨⟩
+  x ∷ (reverse xs ∷ʳ y)   ≡˘⟨ cong (x ∷_) (reverse-∷ y xs) ⟩
+  x ∷ reverse (y ∷ xs)    ∎
+  where open ≡-Reasoning
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index 6b76b43f8f..b948f1ba45 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -1,8 +1,11 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The basic code for equational reasoning about vectors with
--- different indices using cast
+-- An equational reasoning library for propositional equality over
+-- vectors of different indices using cast.
+--
+-- See README.Data.Vec.Relation.Binary.Equality.Cast for
+-- documentation and examples.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -90,8 +93,8 @@ step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
 -- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong`
 -- operation
 ≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
-         ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f (cast l≡o ys) → xs ≈[ m≡n ] f zs
-≈-cong f ys≈zs xs≈fys = trans xs≈fys (cong f ys≈zs)
+         xs ≈[ m≡n ] f (cast l≡o ys) → ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f zs
+≈-cong f xs≈fys ys≈zs = trans xs≈fys (cong f ys≈zs)
 
 
 -- symmetric version of each of the operator
@@ -119,21 +122,4 @@ syntax step-≂  xs ys≈zs xs≡ys  = xs ≂⟨  xs≡ys ⟩ ys≈zs
 syntax step-≂˘ xs ys≈zs ys≡xs  = xs ≂˘⟨ ys≡xs ⟩ ys≈zs
 syntax step-≈  xs ys≈zs xs≈ys  = xs ≈⟨  xs≈ys ⟩ ys≈zs
 syntax step-≈˘ xs ys≈zs ys≈xs  = xs ≈˘⟨ ys≈xs ⟩ ys≈zs
-syntax ≈-cong  f  ys≈zs xs≈fys = xs≈fys ≈cong[ f ] ys≈zs
-
-{-
--- An equational reasoning example, demonstrating nested uses of the cong operator
-
-cast-++ˡ : ∀ .(eq : n ≡ o) (xs : Vec A n) {ys : Vec A m} →
-           cast (cong (_+ m) eq) (xs ++ ys) ≡ cast eq xs ++ ys
-
-example : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) (ys : Vec A n) →
-          cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
-example {m = m} {n} eq a xs ys = begin
-  reverse ((xs ++ [ a ]) ++ ys)       ≈˘⟨ cast-reverse (cong (_+ n) (ℕₚ.+-comm 1 m)) ((xs ∷ʳ a) ++ ys)
-                                          ≈cong[ reverse ] cast-++ˡ (ℕₚ.+-comm 1 m) (xs ∷ʳ a)
-                                                           ≈cong[ (_++ ys) ] unfold-∷ʳ _ a xs ⟩
-  reverse ((xs ∷ʳ a) ++ ys)           ≈⟨ reverse-++ (ℕₚ.+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
-  reverse ys ++ reverse (xs ∷ʳ a)     ≂˘⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟩
-  ys ʳ++ reverse (xs ∷ʳ a)            ∎
--}
+syntax ≈-cong  f xs≈fys ys≈zs = xs≈fys ≈cong[ f ] ys≈zs

From ec17b4572cccb961af494cef6ab874d8607cfab3 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 2 Oct 2023 15:42:42 -0500
Subject: [PATCH 11/18] =?UTF-8?q?Remove=20the=20syntax=20declaration=20of?=
 =?UTF-8?q?=20`=5F=E2=89=88cong[=5F]=5F`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Vec/Properties.agda                  | 20 +++++++++----------
 .../Vec/Relation/Binary/Equality/Cast.agda    |  1 -
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index a7dd888a25..fa34670da3 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -975,8 +975,8 @@ reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
 reverse-++ {m = zero}  {n = n} eq []       ys = CastReasoning.≈-sym (++-identityʳ (sym eq) (reverse ys))
 reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin′
   reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
-  reverse (xs ++ ys) ∷ʳ x             ≈⟨ cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys))
-                                         ≈cong[ (_∷ʳ x) ] reverse-++ _ xs ys ⟩
+  reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys)))
+                                                (reverse-++ _ xs ys) ⟩
   (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
   reverse ys ++ (reverse (x ∷ xs))    ∎′
@@ -986,8 +986,8 @@ cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ r
 cast-reverse {n = zero}  eq []       = refl
 cast-reverse {n = suc n} eq (x ∷ xs) = begin′
   reverse (x ∷ xs)           ≂⟨ reverse-∷ x xs ⟩
-  reverse xs ∷ʳ x            ≈⟨ cast-∷ʳ eq x (reverse xs)
-                                ≈cong[ (_∷ʳ x) ] cast-reverse (cong pred eq) xs ⟩
+  reverse xs ∷ʳ x            ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ eq x (reverse xs))
+                                       (cast-reverse (cong pred eq) xs) ⟩
   reverse (cast _ xs) ∷ʳ x   ≂˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
   reverse (x ∷ cast _ xs)    ≈⟨⟩
   reverse (cast eq (x ∷ xs)) ∎′
@@ -1034,8 +1034,8 @@ map-ʳ++ {ys = ys} f xs = begin
          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
 ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin′
   ((xs ++ ys) ʳ++ zs)              ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
-  reverse (xs ++ ys) ++ zs         ≈⟨ cast-++ˡ (+-comm m n) (reverse (xs ++ ys))
-                                      ≈cong[ (_++ zs) ] reverse-++ (+-comm m n) xs ys ⟩
+  reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys)))
+                                             (reverse-++ (+-comm m n) xs ys) ⟩
   (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩
   reverse ys ++ (reverse xs ++ zs) ≂˘⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟩
   reverse ys ++ (xs ʳ++ zs)        ≂˘⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟩
@@ -1047,8 +1047,8 @@ map-ʳ++ {ys = ys} f xs = begin
 ʳ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin′
   (xs ʳ++ ys) ʳ++ zs                         ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
   (reverse xs ++ ys) ʳ++ zs                  ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
-  reverse (reverse xs ++ ys) ++ zs           ≈⟨ cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys))
-                                                ≈cong[ (_++ zs) ] reverse-++ (+-comm m n) (reverse xs) ys ⟩
+  reverse (reverse xs ++ ys) ++ zs           ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys)))
+                                                       (reverse-++ (+-comm m n) (reverse xs) ys) ⟩
   (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
   (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂˘⟨ unfold-ʳ++ ys (xs ++ zs) ⟩
@@ -1236,8 +1236,8 @@ fromList-reverse (x List.∷ xs) = begin′
   fromList (List.reverse (x List.∷ xs))         ≈⟨ cast-fromList (Listₚ.ʳ++-defn xs) ⟩
   fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
   fromList (List.reverse xs) ++ [ x ]           ≈˘⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟩
-  fromList (List.reverse xs) ∷ʳ x               ≈⟨ cast-∷ʳ (cong suc (Listₚ.length-reverse xs)) _ _
-                                                   ≈cong[ (_∷ʳ x) ] fromList-reverse xs ⟩
+  fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (Listₚ.length-reverse xs)) _ _)
+                                                          (fromList-reverse xs) ⟩
   reverse (fromList xs) ∷ʳ x                    ≂˘⟨ reverse-∷ x (fromList xs) ⟩
   reverse (x ∷ fromList xs)                     ≈⟨⟩
   reverse (fromList (x List.∷ xs))              ∎′
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index b948f1ba45..ce88f72d0d 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -122,4 +122,3 @@ syntax step-≂  xs ys≈zs xs≡ys  = xs ≂⟨  xs≡ys ⟩ ys≈zs
 syntax step-≂˘ xs ys≈zs ys≡xs  = xs ≂˘⟨ ys≡xs ⟩ ys≈zs
 syntax step-≈  xs ys≈zs xs≈ys  = xs ≈⟨  xs≈ys ⟩ ys≈zs
 syntax step-≈˘ xs ys≈zs ys≈xs  = xs ≈˘⟨ ys≈xs ⟩ ys≈zs
-syntax ≈-cong  f xs≈fys ys≈zs = xs≈fys ≈cong[ f ] ys≈zs

From 9da2ed342c2830c6ceac5cfacecb613a127c00b5 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Mon, 2 Oct 2023 15:46:08 -0500
Subject: [PATCH 12/18] delete git merge annotations

---
 CHANGELOG.md | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2729021aa4..c36648e6f9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2841,19 +2841,16 @@ Additions to existing modules
   cast-fromList : cast _ (fromList xs) ≡ fromList ys
   fromList-map  : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs)
   fromList-++   : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
-<<<<<<< HEAD
   fromList-reverse : cast (Listₚ.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
 
   ∷-ʳ++   : cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
   ++-ʳ++  : cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
   ʳ++-ʳ++ : cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-=======
 
   truncate≡take       : .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs)
   take≡truncate       : take m xs ≡ truncate (m≤m+n m n) xs
   lookup-truncate     : lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n)
   lookup-take-inject≤ : lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n))
->>>>>>> master
   ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:

From 47d0ff3be81db2e1a77d5601e0a0b72b4685cb22 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Tue, 3 Oct 2023 02:53:23 -0500
Subject: [PATCH 13/18] =?UTF-8?q?review:=20open=20=E2=89=A1-Reasoning=20lo?=
 =?UTF-8?q?cally=20to=20avoid=20renaming=20CastReasoning?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Vec/Properties.agda | 54 +++++++++++++++++++++++-------------
 1 file changed, 34 insertions(+), 20 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 0002391076..3a6c5772c3 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -33,8 +33,6 @@ open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′)
 open import Relation.Nullary.Negation.Core using (contradiction)
 
-open ≡-Reasoning
-
 private
   variable
     a b c d p : Level
@@ -760,6 +758,7 @@ zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (zipWith-is-⊛ f xs ys)
   diagonal (map (flip map xs) fs)                  ≡⟨⟩
   diagonal (map (tail ∘ flip map (x ∷ xs)) fs)     ≡⟨ cong diagonal (map-∘ _ _ _) ⟩
   diagonal (map tail (map (flip map (x ∷ xs)) fs)) ∎
+  where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- _⊛*_
@@ -787,6 +786,7 @@ foldl-universal B f e h base step (x ∷ xs) = begin
   h (B ∘ suc) f (f e x) xs     ≡⟨ foldl-universal _ f (f e x) h base step xs ⟩
   foldl (B ∘ suc) f (f e x) xs ≡⟨⟩
   foldl B f e (x ∷ xs)         ∎
+  where open ≡-Reasoning
 
 foldl-fusion : ∀ {B : ℕ → Set b} {C : ℕ → Set c}
                (h : ∀ {n} → B n → C n) →
@@ -799,6 +799,7 @@ foldl-fusion h {f} {d} {g} {e} base fuse []       = base
 foldl-fusion h {f} {d} {g} {e} base fuse (x ∷ xs) =
   foldl-fusion h eq fuse xs
   where
+    open ≡-Reasoning
     eq : h (f d x) ≡ g e x
     eq = begin
       h (f d x) ≡⟨ fuse d x ⟩
@@ -826,6 +827,7 @@ module _ (B : ℕ → Set b) (f : FoldrOp A B) {e : B zero} where
     h (x ∷ xs)           ≡⟨ step x xs ⟩
     f x (h xs)           ≡⟨ cong (f x) (foldr-universal h base step xs) ⟩
     f x (foldr B f e xs) ∎
+    where open ≡-Reasoning
 
   foldr-[] : foldr B f e [] ≡ e
   foldr-[] = refl
@@ -942,6 +944,7 @@ foldl-reverse B f {e} (x ∷ xs) = begin
   f (foldl B f e (reverse xs)) x ≡⟨ cong (flip f x) (foldl-reverse B f xs) ⟩
   f (foldr B (flip f) e xs) x    ≡⟨⟩
   foldr B (flip f) e (x ∷ xs)    ∎
+  where open ≡-Reasoning
 
 -- foldr after a reverse is a foldl
 
@@ -956,12 +959,14 @@ reverse-involutive xs = begin
   reverse (reverse xs)    ≡⟨  foldl-reverse (Vec _) (flip _∷_) xs ⟩
   foldr (Vec _) _∷_ [] xs ≡˘⟨ id-is-foldr xs ⟩
   xs                      ∎
+  where open ≡-Reasoning
 
 reverse-reverse : reverse xs ≡ ys → reverse ys ≡ xs
 reverse-reverse {xs = xs} {ys} eq =  begin
   reverse ys           ≡˘⟨ cong reverse eq ⟩
   reverse (reverse xs) ≡⟨  reverse-involutive xs ⟩
   xs                   ∎
+  where open ≡-Reasoning
 
 -- reverse is injective.
 
@@ -970,6 +975,7 @@ reverse-injective {xs = xs} {ys} eq = begin
   xs                   ≡˘⟨ reverse-reverse eq ⟩
   reverse (reverse ys) ≡⟨  reverse-involutive ys ⟩
   ys                   ∎
+  where open ≡-Reasoning
 
 -- init and last of reverse
 
@@ -978,12 +984,14 @@ init-reverse (x ∷ xs) = begin
   init (reverse (x ∷ xs))   ≡⟨ cong init (reverse-∷ x xs) ⟩
   init (reverse xs ∷ʳ x)    ≡⟨ init-∷ʳ x (reverse xs) ⟩
   reverse xs                ∎
+  where open ≡-Reasoning
 
 last-reverse : last ∘ reverse ≗ head {A = A} {n = n}
 last-reverse (x ∷ xs) = begin
   last (reverse (x ∷ xs))   ≡⟨ cong last (reverse-∷ x xs) ⟩
   last (reverse xs ∷ʳ x)    ≡⟨ last-∷ʳ x (reverse xs) ⟩
   x                         ∎
+  where open ≡-Reasoning
 
 -- map and reverse
 
@@ -997,31 +1005,32 @@ map-reverse f (x ∷ xs) = begin
   reverse (map f xs) ∷ʳ f x ≡˘⟨ reverse-∷ (f x) (map f xs) ⟩
   reverse (f x ∷ map f xs)  ≡⟨⟩
   reverse (map f (x ∷ xs))  ∎
+  where open ≡-Reasoning
 
 -- append and reverse
 
 reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
 reverse-++ {m = zero}  {n = n} eq []       ys = CastReasoning.≈-sym (++-identityʳ (sym eq) (reverse ys))
-reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin′
+reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
   reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
   reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys)))
                                                 (reverse-++ _ xs ys) ⟩
   (reverse ys ++ reverse xs) ∷ʳ x     ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
   reverse ys ++ (reverse xs ∷ʳ x)     ≂˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
-  reverse ys ++ (reverse (x ∷ xs))    ∎′
-  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  reverse ys ++ (reverse (x ∷ xs))    ∎
+  where open CastReasoning
 
 cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
 cast-reverse {n = zero}  eq []       = refl
-cast-reverse {n = suc n} eq (x ∷ xs) = begin′
+cast-reverse {n = suc n} eq (x ∷ xs) = begin
   reverse (x ∷ xs)           ≂⟨ reverse-∷ x xs ⟩
   reverse xs ∷ʳ x            ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ eq x (reverse xs))
                                        (cast-reverse (cong pred eq) xs) ⟩
   reverse (cast _ xs) ∷ʳ x   ≂˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
   reverse (x ∷ cast _ xs)    ≈⟨⟩
-  reverse (cast eq (x ∷ xs)) ∎′
-  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  reverse (cast eq (x ∷ xs)) ∎
+  where open CastReasoning
 
 ------------------------------------------------------------------------
 -- _ʳ++_
@@ -1049,32 +1058,33 @@ map-ʳ++ {ys = ys} f xs = begin
   map f (reverse xs) ++ map f ys ≡⟨  cong (_++ map f ys) (map-reverse f xs) ⟩
   reverse (map f xs) ++ map f ys ≡˘⟨ unfold-ʳ++ (map f xs) (map f ys) ⟩
   map f xs ʳ++ map f ys          ∎
+  where open ≡-Reasoning
 
 ∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
         cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
-∷-ʳ++ eq a xs {ys} = begin′
+∷-ʳ++ eq a xs {ys} = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
   (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩
   reverse xs ++ (a ∷ ys)  ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩
-  xs ʳ++ (a ∷ ys)         ∎′
-  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  xs ʳ++ (a ∷ ys)         ∎
+  where open CastReasoning
 
 ++-ʳ++ : ∀ .(eq : m + n + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
          cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
-++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin′
+++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
   ((xs ++ ys) ʳ++ zs)              ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
   reverse (xs ++ ys) ++ zs         ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys)))
                                              (reverse-++ (+-comm m n) xs ys) ⟩
   (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩
   reverse ys ++ (reverse xs ++ zs) ≂˘⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟩
   reverse ys ++ (xs ʳ++ zs)        ≂˘⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟩
-  ys ʳ++ (xs ʳ++ zs)               ∎′
-  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  ys ʳ++ (xs ʳ++ zs)               ∎
+  where open CastReasoning
 
 ʳ++-ʳ++ : ∀ .(eq : (m + n) + o ≡ n + (m + o)) (xs : Vec A m) {ys : Vec A n} {zs} →
           cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
-ʳ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin′
+ʳ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin
   (xs ʳ++ ys) ʳ++ zs                         ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
   (reverse xs ++ ys) ʳ++ zs                  ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
   reverse (reverse xs ++ ys) ++ zs           ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys)))
@@ -1082,8 +1092,8 @@ map-ʳ++ {ys = ys} f xs = begin
   (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
   (reverse ys ++ xs) ++ zs                   ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩
   reverse ys ++ (xs ++ zs)                   ≂˘⟨ unfold-ʳ++ ys (xs ++ zs) ⟩
-  ys ʳ++ (xs ++ zs)                          ∎′
-  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  ys ʳ++ (xs ++ zs)                          ∎
+  where open CastReasoning
 
 ------------------------------------------------------------------------
 -- sum
@@ -1094,6 +1104,7 @@ sum-++ {ys = ys} (x ∷ xs) = begin
   x + sum (xs ++ ys)     ≡⟨  cong (x +_) (sum-++ xs) ⟩
   x + (sum xs + sum ys)  ≡˘⟨ +-assoc x (sum xs) (sum ys) ⟩
   sum (x ∷ xs) + sum ys  ∎
+  where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- replicate
@@ -1115,6 +1126,7 @@ transpose-replicate {n = suc n} xs = begin
   (replicate _∷_ ⊛ xs ⊛ transpose (replicate xs)) ≡⟨ cong₂ _⊛_ (sym (map-is-⊛ _∷_ xs)) (transpose-replicate xs) ⟩
   (map _∷_ xs ⊛ map replicate xs)                 ≡⟨ map-⊛ _∷_ replicate xs ⟩
   map replicate xs                                ∎
+  where open ≡-Reasoning
 
 zipWith-replicate : ∀ (_⊕_ : A → B → C) (x : A) (y : B) →
                     zipWith {n = n} _⊕_ (replicate x) (replicate y) ≡ replicate (x ⊕ y)
@@ -1179,6 +1191,7 @@ map-lookup-allFin {n = n} xs = begin
   map (lookup xs) (allFin n) ≡˘⟨ tabulate-∘ (lookup xs) id ⟩
   tabulate (lookup xs)       ≡⟨ tabulate∘lookup xs ⟩
   xs                         ∎
+  where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- count
@@ -1249,6 +1262,7 @@ cast-fromList {xs = x List.∷ xs} {ys = y List.∷ ys} eq =
   x ∷ cast (cong (pred ∘ List.length) eq) (fromList xs) ≡⟨ cong (_ ∷_) (cast-fromList xs≡ys) ⟩
   x ∷ fromList ys                                       ≡⟨ cong (_∷ _) x≡y ⟩
   y ∷ fromList ys                                       ∎
+  where open ≡-Reasoning
 
 fromList-map : ∀ (f : A → B) (xs : List A) →
                cast (Listₚ.length-map f xs) (fromList (List.map f xs)) ≡ map f (fromList xs)
@@ -1262,7 +1276,7 @@ fromList-++ (x List.∷ xs) {ys} = cong (x ∷_) (fromList-++ xs)
 
 fromList-reverse : (xs : List A) → cast (Listₚ.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
 fromList-reverse List.[] = refl
-fromList-reverse (x List.∷ xs) = begin′
+fromList-reverse (x List.∷ xs) = begin
   fromList (List.reverse (x List.∷ xs))         ≈⟨ cast-fromList (Listₚ.ʳ++-defn xs) ⟩
   fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
   fromList (List.reverse xs) ++ [ x ]           ≈˘⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟩
@@ -1270,8 +1284,8 @@ fromList-reverse (x List.∷ xs) = begin′
                                                           (fromList-reverse xs) ⟩
   reverse (fromList xs) ∷ʳ x                    ≂˘⟨ reverse-∷ x (fromList xs) ⟩
   reverse (x ∷ fromList xs)                     ≈⟨⟩
-  reverse (fromList (x List.∷ xs))              ∎′
-  where open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  reverse (fromList (x List.∷ xs))              ∎
+  where open CastReasoning
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

From 01d7b1b2beed0134ef96bf37358fc5d52768466e Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 4 Oct 2023 23:06:21 -0500
Subject: [PATCH 14/18] review: re-export cast-is-id and cast-trans

Subsumes bef3328.
---
 src/Data/Vec/Properties.agda                    |  8 ++------
 src/Data/Vec/Relation/Binary/Equality/Cast.agda | 16 ++++++++--------
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 3a6c5772c3..81421843f2 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -363,8 +363,8 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 ------------------------------------------------------------------------
 -- cast
 
-cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
-cast-is-id _ _ = CastReasoning.≈-reflexive refl
+open CastReasoning public
+  using (cast-is-id; cast-trans)
 
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
@@ -376,10 +376,6 @@ cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs[eq]≡yys =
   let x≡y , xs[eq]≡ys = ∷-injective xxs[eq]≡yys
   in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs[eq]≡ys)
 
-cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
-             cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
-cast-trans _ _ _ = sym (CastReasoning.≈-trans refl refl)
-
 ------------------------------------------------------------------------
 -- map
 
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index ce88f72d0d..c4f596f4bc 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -25,16 +25,16 @@ private
     l m n o : ℕ
     xs ys zs : Vec A n
 
-  cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
-  cast-is-id eq []       = refl
-  cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
 
-  cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
-               cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
-  cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
-  cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
-    cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)
+cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
+cast-is-id eq []       = refl
+cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
 
+cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
+             cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
+cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
+cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
+  cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)
 
 
 infix 3 _≈[_]_

From 90a124db143d5d2e8f97d59ef5bcfd673711181f Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 4 Oct 2023 23:15:46 -0500
Subject: [PATCH 15/18] review: place reasoning combinators in a module

---
 .../Vec/Relation/Binary/Equality/Cast.agda    |  4 +-
 src/Data/Vec/Properties.agda                  |  7 +-
 .../Vec/Relation/Binary/Equality/Cast.agda    | 88 ++++++++++---------
 3 files changed, 51 insertions(+), 48 deletions(-)

diff --git a/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
index 65a9c45414..3f7ffc1799 100644
--- a/README/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -16,7 +16,7 @@ open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Vec.Base
 open import Data.Vec.Properties
-import Data.Vec.Relation.Binary.Equality.Cast as CastReasoning
+open import Data.Vec.Relation.Binary.Equality.Cast
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; trans; sym; cong; subst; module ≡-Reasoning)
 
@@ -89,7 +89,7 @@ example1a-fromList-∷ʳ x xs eq = begin
   cast eq (fromList (xs L.∷ʳ x))                   ≡⟨⟩
   cast eq (fromList (xs L.++ L.[ x ]))             ≡˘⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟩
   cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
-  cast eq₂ (fromList xs ++ [ x ])                  ≡⟨ CastReasoning.≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
+  cast eq₂ (fromList xs ++ [ x ])                  ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
   fromList xs ∷ʳ x                                 ∎
   where
   open ≡-Reasoning
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 81421843f2..dd42ee30fb 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -22,7 +22,8 @@ open import Data.Product.Base as Prod
 open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
-import Data.Vec.Relation.Binary.Equality.Cast as CastReasoning
+open import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+  using (_≈[_]_; ≈-sym; module CastReasoning)
 open import Function.Base
 open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
@@ -363,7 +364,7 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 ------------------------------------------------------------------------
 -- cast
 
-open CastReasoning public
+open VecCast public
   using (cast-is-id; cast-trans)
 
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
@@ -1007,7 +1008,7 @@ map-reverse f (x ∷ xs) = begin
 
 reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ {m = zero}  {n = n} eq []       ys = CastReasoning.≈-sym (++-identityʳ (sym eq) (reverse ys))
+reverse-++ {m = zero}  {n = n} eq []       ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
 reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
   reverse (x ∷ xs ++ ys)              ≂⟨ reverse-∷ x (xs ++ ys) ⟩
   reverse (xs ++ ys) ∷ʳ x             ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys)))
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index c4f596f4bc..8d9cf2866a 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -67,58 +67,60 @@ xs ≈[ eq ] ys = cast eq xs ≡ ys
 ------------------------------------------------------------------------
 -- Reasoning combinators
 
-begin_ : ∀ .{m≡n : m ≡ n} {xs : Vec A m} {ys} → xs ≈[ m≡n ] ys → cast m≡n xs ≡ ys
-begin xs≈ys = xs≈ys
+module CastReasoning where
 
-_∎ : (xs : Vec A n) → cast refl xs ≡ xs
-_∎ xs = ≈-reflexive refl
+  begin_ : ∀ .{m≡n : m ≡ n} {xs : Vec A m} {ys} → xs ≈[ m≡n ] ys → cast m≡n xs ≡ ys
+  begin xs≈ys = xs≈ys
 
-_≈⟨⟩_ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys} → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] ys
-xs ≈⟨⟩ xs≈ys = xs≈ys
+  _∎ : (xs : Vec A n) → cast refl xs ≡ xs
+  _∎ xs = ≈-reflexive refl
 
--- composition of _≈[_]_
-step-≈ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
-         ys ≈[ trans (sym m≡n) m≡o ] zs → xs ≈[ m≡n ] ys → xs ≈[ m≡o ] zs
-step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs
+  _≈⟨⟩_ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys} → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] ys
+  xs ≈⟨⟩ xs≈ys = xs≈ys
 
--- composition of the equality type on the right-hand side of _≈[_]_,
--- or escaping to ordinary _≡_
-step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] zs
-step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
+  -- composition of _≈[_]_
+  step-≈ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
+           ys ≈[ trans (sym m≡n) m≡o ] zs → xs ≈[ m≡n ] ys → xs ≈[ m≡o ] zs
+  step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs
 
--- composition of the equality type on the left-hand side of _≈[_]_
-step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → xs ≡ ys → xs ≈[ m≡n ] zs
-step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
+  -- composition of the equality type on the right-hand side of _≈[_]_,
+  -- or escaping to ordinary _≡_
+  step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] zs
+  step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
 
--- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong`
--- operation
-≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
-         xs ≈[ m≡n ] f (cast l≡o ys) → ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f zs
-≈-cong f xs≈fys ys≈zs = trans xs≈fys (cong f ys≈zs)
+  -- composition of the equality type on the left-hand side of _≈[_]_
+  step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → xs ≡ ys → xs ≈[ m≡n ] zs
+  step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
 
+  -- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong`
+  -- operation
+  ≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
+           xs ≈[ m≡n ] f (cast l≡o ys) → ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f zs
+  ≈-cong f xs≈fys ys≈zs = trans xs≈fys (cong f ys≈zs)
 
--- symmetric version of each of the operator
-step-≈˘ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
-         ys ≈[ trans n≡m m≡o ] zs → ys ≈[ n≡m ] xs → xs ≈[ m≡o ] zs
-step-≈˘ xs ys≈zs ys≈xs = step-≈ xs ys≈zs (≈-sym ys≈xs)
 
-step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → ys ≈[ sym m≡n ] xs → xs ≈[ m≡n ] zs
-step-≃˘ xs ys≡zs ys≈xs = step-≃ xs ys≡zs (≈-sym ys≈xs)
+  -- symmetric version of each of the operator
+  step-≈˘ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} →
+           ys ≈[ trans n≡m m≡o ] zs → ys ≈[ n≡m ] xs → xs ≈[ m≡o ] zs
+  step-≈˘ xs ys≈zs ys≈xs = step-≈ xs ys≈zs (≈-sym ys≈xs)
 
-step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → ys ≡ xs → xs ≈[ m≡n ] zs
-step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs)
+  step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → ys ≈[ sym m≡n ] xs → xs ≈[ m≡n ] zs
+  step-≃˘ xs ys≡zs ys≈xs = step-≃ xs ys≡zs (≈-sym ys≈xs)
 
+  step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → ys ≡ xs → xs ≈[ m≡n ] zs
+  step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs)
 
-------------------------------------------------------------------------
--- convenient syntax for ‘equational’ reasoning
-
-infix 1 begin_
-infixr 2 step-≃ step-≂ step-≃˘ step-≂˘ step-≈ step-≈˘ _≈⟨⟩_ ≈-cong
-infix 3 _∎
-
-syntax step-≃  xs ys≡zs xs≈ys  = xs ≃⟨  xs≈ys ⟩ ys≡zs
-syntax step-≃˘ xs ys≡zs xs≈ys  = xs ≃˘⟨ xs≈ys ⟩ ys≡zs
-syntax step-≂  xs ys≈zs xs≡ys  = xs ≂⟨  xs≡ys ⟩ ys≈zs
-syntax step-≂˘ xs ys≈zs ys≡xs  = xs ≂˘⟨ ys≡xs ⟩ ys≈zs
-syntax step-≈  xs ys≈zs xs≈ys  = xs ≈⟨  xs≈ys ⟩ ys≈zs
-syntax step-≈˘ xs ys≈zs ys≈xs  = xs ≈˘⟨ ys≈xs ⟩ ys≈zs
+
+  ------------------------------------------------------------------------
+  -- convenient syntax for ‘equational’ reasoning
+
+  infix 1 begin_
+  infixr 2 step-≃ step-≂ step-≃˘ step-≂˘ step-≈ step-≈˘ _≈⟨⟩_ ≈-cong
+  infix 3 _∎
+
+  syntax step-≃  xs ys≡zs xs≈ys  = xs ≃⟨  xs≈ys ⟩ ys≡zs
+  syntax step-≃˘ xs ys≡zs xs≈ys  = xs ≃˘⟨ xs≈ys ⟩ ys≡zs
+  syntax step-≂  xs ys≈zs xs≡ys  = xs ≂⟨  xs≡ys ⟩ ys≈zs
+  syntax step-≂˘ xs ys≈zs ys≡xs  = xs ≂˘⟨ ys≡xs ⟩ ys≈zs
+  syntax step-≈  xs ys≈zs xs≈ys  = xs ≈⟨  xs≈ys ⟩ ys≈zs
+  syntax step-≈˘ xs ys≈zs ys≈xs  = xs ≈˘⟨ ys≈xs ⟩ ys≈zs

From 1b7777dc0e77e100e6ea45e0dff4200510a3d6fb Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 4 Oct 2023 23:18:17 -0500
Subject: [PATCH 16/18] cosmetic changes: fix README empty lines

---
 README/Data/Vec/Relation/Binary/Equality/Cast.agda | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
index 3f7ffc1799..38bacbcb0c 100644
--- a/README/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -32,7 +32,6 @@ private variable
 
 
 ------------------------------------------------------------------------
---
 -- Motivation
 --
 -- The `cast` function is the computational variant of `subst` for
@@ -111,10 +110,7 @@ example1b-fromList-∷ʳ x xs eq = begin
   where open CastReasoning
 
 
-
-
 ------------------------------------------------------------------------
---
 -- Combinators
 --
 -- Let `xs ≈[ m≡n ] ys` denote `cast m≡n xs ≡ ys`. We have reflexivity,
@@ -214,7 +210,6 @@ example4-cong² {m = m} {n} eq a xs ys = begin
   where open CastReasoning
 
 ------------------------------------------------------------------------
---
 -- Interoperation between `_≈[_]_` and `_≡_`
 --
 -- This library is designed to interoperate with `_≡_`. Examples in the

From 2be93c951ac5ce115c334d34403e436a13038591 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 4 Oct 2023 23:30:35 -0500
Subject: [PATCH 17/18] review: re-export ==-Reasoning

---
 README/Data/Vec/Relation/Binary/Equality/Cast.agda | 12 ++++++------
 src/Data/Vec/Relation/Binary/Equality/Cast.agda    |  3 +++
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
index 38bacbcb0c..fb76544ed7 100644
--- a/README/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -226,22 +226,22 @@ example5-fromList-++-++′ : {xs ys zs : List A} →
                                   L.length xs + (L.length ys + L.length zs)) →
                            cast eq (fromList (xs L.++ ys L.++ zs)) ≡
                                    fromList xs ++ fromList ys ++ fromList zs
-example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin′
+example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
   fromList (xs L.++ ys L.++ zs)                 ≈⟨ fromList-++ xs ⟩
   fromList xs ++ fromList (ys L.++ zs)          ≃⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
   fromList xs ++ cast _ (fromList (ys L.++ zs)) ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
-  fromList xs ++ fromList ys ++ fromList zs     ∎
-  where open ≡-Reasoning; open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  fromList xs ++ fromList ys ++ fromList zs     ≡-∎
+  where open CastReasoning
 
 -- Of course, it is possible to start with the reasoning system of `_≡_`
 -- and then switch to the reasoning system of `_≈[_]_`.
 example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
-example6a-reverse-∷ʳ {n = n} x xs = begin
+example6a-reverse-∷ʳ {n = n} x xs = begin-≡
   reverse (xs ∷ʳ x)     ≡˘⟨ ≈-reflexive refl ⟩
   reverse (xs ∷ʳ x)     ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
   reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
-  x ∷ reverse xs        ∎′
-  where open ≡-Reasoning; open CastReasoning renaming (begin_ to begin′_; _∎ to _∎′)
+  x ∷ reverse xs        ∎
+  where open CastReasoning
 
 example6b-reverse-∷ʳ-by-induction : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
 example6b-reverse-∷ʳ-by-induction x []       = refl
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
index 8d9cf2866a..adca0a42f2 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -69,6 +69,9 @@ xs ≈[ eq ] ys = cast eq xs ≡ ys
 
 module CastReasoning where
 
+  open ≡-Reasoning public
+    renaming (begin_ to begin-≡_; _∎ to _≡-∎)
+
   begin_ : ∀ .{m≡n : m ≡ n} {xs : Vec A m} {ys} → xs ≈[ m≡n ] ys → cast m≡n xs ≡ ys
   begin xs≈ys = xs≈ys
 

From 7cb75599ec5bb3f07d27567a06d2aaad8abe34c0 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 4 Oct 2023 23:35:51 -0500
Subject: [PATCH 18/18] Add pointers to the README before cast

---
 src/Data/Vec/Base.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 507ac05463..954a28887b 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -93,6 +93,8 @@ xs [ i ]≔ y = xs [ i ]%= const y
 ------------------------------------------------------------------------
 -- Operations for transforming vectors
 
+-- See README.Data.Vec.Relation.Binary.Equality.Cast for the reasoning
+-- system of `cast`-ed equality.
 cast : .(eq : m ≡ n) → Vec A m → Vec A n
 cast {n = zero}  eq []       = []
 cast {n = suc _} eq (x ∷ xs) = x ∷ cast (cong pred eq) xs