Add (propositional) equational reasoning combinators for vectors

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`:

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

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)            ∎
+-}