Add (propositional) equational reasoning combinators for vectors

CHANGELOG.md

@@ -1863,6 +1863,11 @@ New modules
   Function.Indexed.Bundles
   ```
 
+* Combinators for propositional equational reasoning on vectors with different indices
+  ```
+  Data.Vec.Relation.Binary.Equality.Cast
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -2800,6 +2805,7 @@ Additions to existing modules
   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
@@ -2820,6 +2826,8 @@ Additions to existing modules
   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'
 
@@ -2833,6 +2841,11 @@ 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
+  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

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.
 ------------------------------------------------------------------------
 

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
 

README/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -0,0 +1,254 @@
+------------------------------------------------------------------------
+-- 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
+open import Data.Vec.Relation.Binary.Equality.Cast
+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 ])                  ≡⟨ ≈-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 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-≡
+  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 CastReasoning
+
+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

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

src/Data/Vec/Properties.agda

@@ -22,6 +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
+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)
@@ -32,8 +34,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
@@ -364,9 +364,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 eq []       = refl
-cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
+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
 subst-is-cast refl xs = sym (cast-is-id refl xs)
@@ -378,12 +377,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 {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)
-
 ------------------------------------------------------------------------
 -- map
 
@@ -476,6 +469,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)
@@ -752,6 +755,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
 
 ------------------------------------------------------------------------
 -- _⊛*_
@@ -779,6 +783,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) →
@@ -791,6 +796,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 ⟩
@@ -818,6 +824,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
@@ -910,6 +917,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
 
@@ -929,6 +941,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
 
@@ -943,12 +956,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.
 
@@ -957,6 +972,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
 
@@ -965,12 +981,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
 
@@ -984,39 +1002,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 = 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 = zero}  {n = n} eq []       ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
 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 (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
 
 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))              ∎
+  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
 
 ------------------------------------------------------------------------
 -- _ʳ++_
@@ -1044,6 +1055,42 @@ 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
+  (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
+
+++-ʳ++ : ∀ .(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         ≈⟨ ≈-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
+
+ʳ++-ʳ++ : ∀ .(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           ≈⟨ ≈-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) ⟩
+  ys ʳ++ (xs ++ zs)                          ∎
+  where open CastReasoning
 
 ------------------------------------------------------------------------
 -- sum
@@ -1054,6 +1101,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
@@ -1075,6 +1123,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)
@@ -1139,6 +1188,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
@@ -1209,6 +1259,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)
@@ -1220,6 +1271,19 @@ 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               ≈⟨ ≈-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))              ∎
+  where open CastReasoning
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -0,0 +1,129 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- 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 #-}
+
+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)
+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
+
+
+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 _≈[_]_
+
+_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set a
+xs ≈[ eq ] ys = cast eq xs ≡ ys
+
+------------------------------------------------------------------------
+-- _≈[_]_ is ‘reflexive’, ‘symmetric’ and ‘transitive’
+
+≈-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} {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 _≈[ 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 ⟩
+  cast n≡o ys             ≡⟨ ys≈zs ⟩
+  zs                      ∎
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Reasoning combinators
+
+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
+
+  _∎ : (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) →
+           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)
+
+  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